proposition: Remark R1_aux : Countable (image U f).
proof: Proof. apply countable_bij_fun with Ord U f. - case (Ordering_bijection f_ord); intros H H0 H1; split. + intros u u_In_U; exists u; auto. + intros u u_In_img; case u_In_img; intros x Hx. exists x; assumption. + intros u1 u2 u1_In_U u2_In_U Heq; apply H1; try apply U_inc_A; assumption. - assumption. Qed.
imports: ZornsLemma(CountableTypes)