proposition: Lemma Complement_IndexedIntersection {A T : Type} {F : IndexedFamily A T} : Ensembles.Complement (IndexedIntersection F) = IndexedUnion (fun a:A => Ensembles.Complement (F a)).
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - red in H; red in H. apply NNPP. intro. contradict H. constructor. intros. apply NNPP. intro. contradict H0. exists a. assumption. - destruct H. red; red; intro. apply H. destruct H0. apply H0. Qed.
imports: ZornsLemma(EnsemblesImplicit FunctionProperties)