proposition: Corollary Th13_8_1 alpha : A_ alpha = ordinal.
proof: Proof. destruct Th13_8 with alpha. eapply A_full with (succ alpha). - intros; apply Lemma5. - auto with schutte. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)