proposition: Lemma Lemma5_01 : beta < gamma.
proof: Proof. unfold omega_limit in gamma. apply lt_le_trans with (gamma_ 0). simpl; auto with schutte. unfold gamma; apply sup_upper_bound. apply seq_range_countable. now exists 0. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)