proposition: Lemma inverse_image_intersection: forall {X Y:Type} (f:X->Y) (T1 T2:Ensemble Y), inverse_image f (Intersection T1 T2) = Intersection (inverse_image f T1) (inverse_image f T2).
proof: Proof. intros. apply Extensionality_Ensembles; split; red; intros. - destruct H. inversion H. constructor; constructor; trivial. - destruct H as [? [] []]. constructor; constructor; trivial. Qed.
imports: ZornsLemma(IndexedFamilies Powerset_facts)