proposition: Lemma T1_sep_Subspace {X : TopologicalSpace} (A : Ensemble X) : T1_sep X -> T1_sep (SubspaceTopology A).
proof: Proof. intros HX [x Hx]. apply subspace_closed_char. specialize (HX x). exists (Singleton x). split; auto. apply Extensionality_Ensembles; split. - intros y Hy. destruct Hy. constructor. simpl. constructor. - intros [y Hy] [Hy0]. simpl in Hy0. destruct Hy0. destruct (PI.proof_irrelevance _ Hx Hy). constructor. Qed.
imports: Coq(Program.Subset) Topology(Homeomorphisms SubspaceTopology)