proposition: Remark R2 : In B (|_| (image U f)).
proof: Proof. apply B_closed. - red;red; destruct 1. case f_ord. intros H0 H1 H2 H3. case H;intros; subst x; destruct f_ord. decompose [and] H3. apply OF_total0. apply U_inc_A;auto. - case U_non_empty;intros x H; exists (f x);auto. exists x;auto. - apply R1_aux. Qed.
imports: ZornsLemma(CountableTypes)