proposition: Remark im_U_f : (image U f : Ensemble Ord) = M.
proof: Proof. eapply Extensionality_Ensembles; split. red;destruct 1; unfold U in H; case H. intros; case H0;intros. subst x;auto. red; intros. exists (inv_fun inh_Ord A B f x); split. red;red; generalize (Ordering_bijection f_ord). intros; split. case (inv_fun_bij inh_Ord H0). auto. intros; destruct H0. rewrite inv_composeR; auto with schutte. apply fbij. apply inc;auto. rewrite inv_composeR; auto with schutte. apply fbij. apply inc;auto. Qed.
imports: ZornsLemma(CountableTypes)