∀ {β : Type u_1} [inst : Lattice β] [inst_1 : BoundedOrder β] {P : β → Prop} (Pbot : P ⊥) (Ptop : P ⊤)
  (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)),
  (LatticeHom.subtypeVal Psup Pinf).toFun ⊤ = ⊤