proposition: Lemma FamilyIntersection_Finite (X : Type) (F : Family X) : (exists U, In F U /\ Finite U) -> Finite (FamilyIntersection F).
proof: Proof. intros. destruct H as [U [? ?]]. apply Finite_downward_closed with U; auto. red; intros. destruct H1. apply H1. assumption. Qed.
imports: Coq(Classical Lia) ZornsLemma(DecidableDec EnsemblesImplicit Families FiniteImplicit FunctionPropertiesEns Powerset_facts Image InverseImage ReverseMath.AddSubtract)