proposition: Lemma inverse_image_snd {X Y : Type} (V : Ensemble Y) : inverse_image snd V = EnsembleProduct (@Full_set X) V.
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - do 2 red. destruct H. auto with sets. - destruct H. constructor. auto. Qed.
imports: ZornsLemma(EnsemblesImplicit InverseImage)