proposition: Lemma Hausdorff_impl_T1_sep: forall X:TopologicalSpace, Hausdorff X -> T1_sep X.
proof: Proof. intros X H x. replace (Singleton x) with (closure (Singleton x)). { apply closure_closed. } extensionality_ensembles; [ | now apply closure_inflationary ]. replace x0 with x. { constructor. } apply NNPP. intro. pose proof (H x x0 H1). destruct H2 as [U [V [? [? [? [? ?]]]]]]. assert (In (interior (Complement (Singleton x))) x0). { exists V; trivial. constructor; split; trivial. red; intros. intro. destruct H8. eapply Noone_in_empty. erewrite <- H6. econstructor; eassumption. } rewrite interior_complement in H7. now contradiction H7. Qed.
imports: Coq(Program.Subset) Topology(Homeomorphisms SubspaceTopology)