proposition: Lemma Complement_FamilyIntersection: forall F:Family T, Complement (FamilyIntersection F) = FamilyUnion (Im F Complement).
proof: Proof. intros. apply Extensionality_Ensembles; split; red; intros. - apply NNPP. red; intro. red in H; red in H. contradict H. constructor. intros. apply NNPP. red; intro. contradict H0. exists (Complement S). + apply Im_def. assumption. + assumption. - destruct H. inversion H; subst; clear H. intros ?. destruct H. firstorder. Qed.
imports: Coq(Classical_Prop) Coq(Classical_sets) Coq(Morphisms) ZornsLemma(Image ImageImplicit) ZornsLemma(EnsemblesImplicit)