proposition: Lemma Im_id {X : Type} (U : Ensemble X) : Im U id = U.
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - inversion H; subst; clear H. assumption. - exists x; auto. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(FunctionProperties)