proposition: Lemma T1_sep_impl_T0_sep: forall X:TopologicalSpace, T1_sep X -> T0_sep X.
proof: Proof. intros. red. intros. left. exists (Complement (Singleton y)). repeat split. - apply H. - intro. destruct H1. now contradiction H0. - intro. apply H1. constructor. Qed.
imports: Coq(Program.Subset) Topology(Homeomorphisms SubspaceTopology)