proposition: Lemma Complement_FamilyUnion: forall F:Family T, Complement (FamilyUnion F) = FamilyIntersection (Im F Complement).
proof: Proof. intros. apply Extensionality_Ensembles; split; red; intros. - constructor. intros S HS. destruct HS as [U HU S]. subst. intros HUx. apply H. exists U; auto. - destruct H as [x Hx]. intros Hx0. destruct Hx0. specialize (Hx (Complement S)). apply Hx; auto. apply Im_def. assumption. Qed.
imports: Coq(Classical_Prop) Coq(Classical_sets) Coq(Morphisms) ZornsLemma(Image ImageImplicit) ZornsLemma(EnsemblesImplicit)