proposition: Theorem Th13_8 alpha : normal (phi alpha) (Cr alpha).
proof: Proof. eapply TH_13_6R with (A_ alpha). apply ord_ok. apply Closed_Cr. apply Unbounded_Cr. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)