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