proposition: Remark R4'' : |_| (image U f) <= f (sup U).
proof: Proof. apply sup_least_upper_bound. - apply R1. - intros y H; destruct H; destruct H;subst y; apply ordering_function_mono_weak with A B; auto. + apply A_closed. + apply sup_upper_bound;auto. Qed.
imports: ZornsLemma(CountableTypes)