α : Type u_1
β : Type ?u.19944
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
x : α
⊢ x ∈ {a | IsAtom a} ↔ x ∈ {a | IsAtom a ∧ a ≤ ⊤}
α : Type u_1
β : Type ?u.19944
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
⊢ sSup {a | IsAtom a} = ⊤
refine' Eq.trans (congr rfl (Set.ext fun x => _)) (sSup_atoms_le_eq ⊤)
no goals
α : Type u_1
β : Type ?u.19944
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
x : α
⊢ x ∈ {a | IsAtom a} ↔ x ∈ {a | IsAtom a ∧ a ≤ ⊤}
exact (and_iff_left le_top).symm