let A be Ordinal; :: thesis: ( not A is empty & A is limit_ordinal implies A is infinite )
assume A1: ( not A is empty & A is limit_ordinal ) ; :: thesis: A is infinite
assume A is finite ; :: thesis: contradiction
then A2: A in omega by CARD_1:61;
{} in A by A1, ORDINAL1:16, XBOOLE_1:3;
then omega c= A by A1, ORDINAL1:def 11;
then A in A by A2;
hence contradiction ; :: thesis: verum