proposition: Remark R42 : f (sup U) <= |_| (image U f).
proof: Proof. apply le_trans with (f alpha_). - case f_ord;intros H H0 H1 H2. case R7. + intro H5; rewrite H5;auto with schutte. + right;auto. apply H2;auto with schutte. apply A_closed;auto with schutte. - unfold alpha_; apply epsilon_ind. + apply R3. + destruct 1; left; auto. Qed.
imports: ZornsLemma(CountableTypes)