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