proposition: Lemma EnsembleProduct_Empty_r {X Y : Type} U : @EnsembleProduct X Y U Empty_set = Empty_set.
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - destruct x. destruct H. destruct H0. - destruct H. Qed.
imports: ZornsLemma(EnsemblesImplicit InverseImage)