proposition: Lemma EnsembleProduct_Union {X Y : Type} (U0 U1 : Ensemble X) (V0 V1 : Ensemble Y) : Included (Union (EnsembleProduct U0 V0) (EnsembleProduct U1 V1)) (EnsembleProduct (Union U0 U1) (Union V0 V1)).
proof: Proof. intros x H. destruct H as [|]; destruct x; destruct H. - split; left; assumption. - split; right; assumption. Qed.
imports: ZornsLemma(EnsemblesImplicit InverseImage)