no goals
α : Type u_1
β : Type ?u.2539
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x y : α
S U Z : Set α
h : IsGenericPoint x S
hZ : IsClosed Z
⊢ x ∈ Z ↔ S ⊆ Z
rw [← h.def, hZ.closure_subset_iff, singleton_subset_iff]