proposition: Lemma T3_sep_impl_Hausdorff: forall X:TopologicalSpace, T3_sep X -> Hausdorff X.
proof: Proof. intros. destruct H. red; intros. pose proof (H0 x (Singleton y)). match type of H2 with | ?A -> ?B -> ?C => assert C end. - apply H2. + apply H. + intro. now destruct H3. - destruct H3 as [U [V [? [? [? [? ?]]]]]]. exists U, V. auto 6 with sets. Qed.
imports: Coq(Program.Subset) Topology(Homeomorphisms SubspaceTopology)