ext a
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
hs : s ≠ ⊥
⊢ ⊤ = indiscrete s hs
case hP
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
hs : s ≠ ⊥
a : α✝
⊢ a ∈ ⊤ ↔ a ∈ indiscrete s hs