no goals
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
⊢ T0Space α ↔ ∀ (x y : α), x ≠ y → ∃ U, IsOpen U ∧ Xor' (x ∈ U) (y ∈ U)
simp only [t0Space_iff_not_inseparable, xor_iff_not_iff, not_forall, exists_prop,
  inseparable_iff_forall_open]