proposition: Lemma EnsembleProduct_proj {X Y : Type} (U : Ensemble X) (V : Ensemble Y) : EnsembleProduct U V = Intersection (inverse_image fst U) (inverse_image snd V).
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - destruct x. destruct H. split; constructor; assumption. - destruct H. inversion H. inversion H0. destruct x. split; assumption. Qed.
imports: ZornsLemma(EnsemblesImplicit InverseImage)