proposition: Lemma filter_finite_intersection {X : Type} (F : Filter X) (S : Family X) : Included S (filter_family F) -> Included (finite_intersections S) (filter_family F).
proof: Proof. intros HS U HU. induction HU. - apply filter_full. - auto. - apply filter_intersection; assumption. Qed.
imports: ZornsLemma(DecidableDec FiniteIntersections FunctionProperties)