proposition: Lemma topological_property_T1_sep : topological_property T1_sep.
proof: Proof. intros X Y f [g Hcont_f Hcont_g Hgf Hfg] Hsep x. replace (Singleton x) with (inverse_image g (Singleton (g x))). - red. rewrite <- inverse_image_complement. apply Hcont_g. apply Hsep. - apply Extensionality_Ensembles. split; red; intros. + destruct H. inversion H. eapply f_equal in H1. rewrite Hfg, Hfg in H1. subst. constructor. + inversion H. subst. constructor. constructor. Qed.
imports: Coq(Program.Subset) Topology(Homeomorphisms SubspaceTopology)