let M be Cardinal; :: thesis: ( not M is finite implies M is limit_ordinal )
assume not M is finite ; :: 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:42;
( ( omega <> M & omega c= M ) iff omega c< M ) by XBOOLE_0:def 8;
then ( omega = succ A or omega in succ A ) by A1, A2, CARD_1:14, ORDINAL1:21;
then A3: omega c= A by Lm5, ORDINAL1:34, ORDINAL1:42;
card (A +^ 1) = (card 1) +` (card A) by CARD_2:24
.= card (1 +^ A) by CARD_2:24
.= card A by A3, Th116 ;
then card (succ A) = card A by ORDINAL2:48;
then A4: A, succ A are_equipotent by CARD_1:21;
A5: not succ A c= A by ORDINAL1:7, ORDINAL1:10;
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