proposition: Lemma EnsembleProduct_Included {X Y : Type} (U0 U1 : Ensemble X) (V0 V1 : Ensemble Y) : Included U0 U1 -> Included V0 V1 -> Included (EnsembleProduct U0 V0) (EnsembleProduct U1 V1).
proof: Proof. intros. red; intros. destruct x; destruct H1. split; auto. Qed.
imports: ZornsLemma(EnsemblesImplicit InverseImage)