fact: Record subbasis : Prop := { subbasis_elements: forall U:Ensemble X, In SB U -> open U; subbasis_cover: forall (U:Ensemble X) (x:X), In U x -> open U -> exists V, In V x /\ In (finite_intersections SB) V /\ Included V U; }.
imports: ZornsLemma(FiniteIntersections)