no goals
ι : Type ?u.28417
α : Type u_1
β : Type ?u.28423
γ : Type ?u.28426
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
U : Opens α
⊢ U ≠ ⊥ ↔ Set.Nonempty ↑U
rw [Ne.def, ← not_nonempty_iff_eq_bot, not_not]