proposition: Lemma AP_unbounded_0 : alpha < beta /\ AP beta.
proof: Proof. split. - apply alpha_lt_beta. - split. + apply zero_lt_beta. + intros; apply ksi_plus_beta_eq; eauto with schutte. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)