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