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 Lm2, 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, Th31 ;
then ( card (succ A) = card A & A in succ A ) by ORDINAL1:10, ORDINAL2:48;
then ( A, succ A are_equipotent & not succ A c= A & 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:21, CARD_1:def 1, ORDINAL1:7;
hence contradiction ; :: thesis: verum