let M be Cardinal; ( M is infinite implies M is limit_ordinal )
assume
M is infinite
; M is limit_ordinal
then A1:
not M in omega
;
assume
not M is limit_ordinal
; contradiction
then consider A being Ordinal such that
A2:
M = succ A
by ORDINAL1:29;
( omega = succ A or omega in succ A )
by A1, A2, CARD_1:4;
then A3:
omega c= A
by Lm9, ORDINAL1:22, ORDINAL1:29;
card (A +^ 1) =
(card 1) +` (card A)
by Th12
.=
card (1 +^ A)
by Th12
.=
card A
by A3, Th73
;
then
card (succ A) = card A
by ORDINAL2:31;
then A4:
A, succ A are_equipotent
by CARD_1:5;
A5:
not succ A c= A
by ORDINAL1:5, ORDINAL1:6;
ex B being Ordinal st
( succ A = B & ( for A being Ordinal st A,B are_equipotent holds
B c= A ) )
by A2, CARD_1:def 1;
hence
contradiction
by A4, A5; verum