fact: Variable normal_sep_fun: forall F U:Ensemble X, closed F -> open U -> Included F U -> { V:Ensemble X | open V /\ Included F V /\ Included (closure V) U }.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals TopologicalSpaces InteriorsClosures Div2 Even Arith RTopology