fact: Definition open_basis_cond := forall U V:Ensemble X, In B U -> In B V -> forall x:X, In (Intersection U V) x -> exists W:Ensemble X, In B W /\ In W x /\ Included W (Intersection U V).
imports: Coq(ClassicalChoice) ZornsLemma(CardinalsEns)