no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T25Space α
x y : α
h : x ≠ y
⊢ ∃ u, x ∈ u ∧ IsOpen u ∧ ∃ v, y ∈ v ∧ IsOpen v ∧ Disjoint (closure u) (closure v)
simpa only [exists_prop, and_assoc] using
  ((nhds_basis_opens x).lift'_closure.disjoint_iff (nhds_basis_opens y).lift'_closure).1
    (disjoint_lift'_closure_nhds.2 h)