fact: Definition normal_sep (X:TopologicalSpace) : Prop := T1_sep X /\ forall (F G:Ensemble (point_set X)), closed F -> closed G -> Intersection F G = Empty_set -> exists U:Ensemble (point_set X), exists V:Ensemble (point_set X), open U /\ open V /\ Included F U /\ Included G V /\ Intersection U V = Empty_set.
imports: Coq(Program.Subset) Topology(Homeomorphisms SubspaceTopology)