fact: Definition T0_sep (X:TopologicalSpace) : Prop := forall x y:point_set X, x <> y -> (exists U:Ensemble (point_set X), open U /\ In U x /\ ~ In U y) \/ (exists U:Ensemble (point_set X), open U /\ ~ In U x /\ In U y).
imports: Coq(Program.Subset) Topology(Homeomorphisms SubspaceTopology)