no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a : α
s : Set α
⊢ IsClosed {p | Inseparable p.fst p.snd}
simp only [← specializes_iff_inseparable, isClosed_setOf_specializes]