fact: Record open_basis : Prop := { open_basis_elements : forall V:Ensemble X, In B V -> open V; open_basis_cover : forall (x:X) (U:Ensemble X), open U -> In U x -> exists V:Ensemble X, In B V /\ Included V U /\ In V x }.
imports: Coq(ClassicalChoice) ZornsLemma(CardinalsEns)