let M be Cardinal; :: thesis: ( M is infinite implies M is limit_ordinal )
assume M is infinite ; :: thesis: M is limit_ordinal
then A1: not M in omega ;
assume not M is limit_ordinal ; :: thesis: 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; :: thesis: verum