fact: Definition ultrafilter {X:Type} (F:Filter X) : Prop := forall S:Ensemble X, In (filter_family F) S \/ In (filter_family F) (Ensembles.Complement S).
imports: ZornsLemma(DecidableDec FiniteIntersections FunctionProperties) ZornsLemma(FiniteIntersections)