proposition: Remark R4' : forall khi, In U khi -> f khi <= f (sup U).
proof: Proof. intros khi H ; case f_ord;intros H0 H1 H2 H3 . case (R4 H). - intro; subst khi;left;auto with schutte. - right;auto. apply H3;auto with schutte. apply A_closed;auto. Qed.
imports: ZornsLemma(CountableTypes)