no goals
ι : Type ?u.24447
α : Type u_1
β : Type ?u.24453
γ : Type ?u.24456
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
Us : Set (Opens α)
x : α
⊢ x ∈ sSup Us ↔ ∃ u, u ∈ Us ∧ x ∈ u
simp_rw [sSup_eq_iSup, mem_iSup, exists_prop]