no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a✝ : α
s : Set α
a b : α
⊢ a ⤳ b ↔ b ⤳ a
simp only [← (disjoint_nhds_nhds_iff_not_specializes (α := α)).not_left, disjoint_comm]