proposition: Remark inh_U : Inhabited U.
proof: Proof. case ne;intros. exists (inv_fun inh_Ord A B f x). red; unfold U; rewrite inv_composeR. - split;auto. generalize (Ordering_bijection f_ord); intros; generalize (inv_fun_bij inh_Ord H0). intros; destruct H1. apply H1. apply inc;auto. - apply fbij. - apply inc;auto. Qed.
imports: ZornsLemma(CountableTypes)