proposition: Lemma indexed_to_family_intersection: IndexedIntersection F = FamilyIntersection ImageFamily.
proof: Proof. apply Extensionality_Ensembles. unfold Same_set. unfold Included. intuition. - constructor. intros. destruct H. destruct H0. rewrite H1. apply H. - constructor. intro. destruct H. apply H. apply Im_intro with a; auto with sets. Qed.
imports: ZornsLemma(EnsemblesImplicit FunctionProperties)