proposition: Lemma EnsembleProduct_Intersection {X Y : Type} (U0 U1 : Ensemble X) (V0 V1 : Ensemble Y) : Intersection (EnsembleProduct U0 V0) (EnsembleProduct U1 V1) = EnsembleProduct (Intersection U0 U1) (Intersection V0 V1).
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - destruct H. destruct x. destruct H, H0. split; split; assumption. - destruct H. inversion H; subst; clear H. inversion H0; subst; clear H0. split; constructor; assumption. Qed.
imports: ZornsLemma(EnsemblesImplicit InverseImage)