proposition: Lemma A_closed : In A (sup U).
proof: Proof. assert (H: segment A) by (eapply SA2; eauto). case R7. - intros H3; rewrite H3; apply alpha_A. - intros;red. eapply H with alpha_ ;auto with schutte. Qed.
imports: ZornsLemma(CountableTypes)