fact: Record filter_subbasis {X:Type} (F:Filter X) (B:Family X) : Prop := { filter_subbasis_elements: Included B (filter_family F); filter_subbasis_cond: forall S:Ensemble X, In (filter_family F) S -> exists J:Type, FiniteT J /\ exists T:J->Ensemble X, (forall j:J, In B (T j)) /\ Included (IndexedIntersection T) S }.
imports: ZornsLemma(DecidableDec FiniteIntersections FunctionProperties)