proposition: Lemma EnsembleProduct_Full {X Y : Type} : @EnsembleProduct X Y Full_set Full_set = Full_set.
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - constructor. - destruct x. split. all: constructor. Qed.
imports: ZornsLemma(EnsemblesImplicit InverseImage)