proposition: Lemma Lemma5_04 : exists gamma, In (Cr alpha) gamma /\ beta < gamma.
proof: Proof. exists gamma; split. apply Lemma5_03. apply Lemma5_01. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)