fact: Record filter_basis {X:Type} (F:Filter X) (B:Family X) : Prop := { filter_basis_elements: Included B (filter_family F); filter_basis_cond: forall S:Ensemble X, In (filter_family F) S -> exists S':Ensemble X, In B S' /\ Included S' S }.
imports: ZornsLemma(DecidableDec FiniteIntersections FunctionProperties)