proposition: Lemma normal_sep_impl_T3_sep: forall X:TopologicalSpace, normal_sep X -> T3_sep X.
proof: Proof. intros. destruct H. split; trivial. intros. pose proof (H0 (Singleton x) F). match type of H3 with | ?A -> ?B -> ?C -> ?D => assert D end. - apply H3; trivial. now extensionality_ensembles. - destruct H4 as [U [V [? [? [? [? ?]]]]]]. exists U, V. auto with sets. Qed.
imports: Coq(Program.Subset) Topology(Homeomorphisms SubspaceTopology)