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