let A be Ordinal; :: thesis: ( not A is finite iff omega c= A )
( ( omega c= A implies not A in omega ) & ( not A in omega implies omega c= A ) & ( A is finite implies A in omega ) & ( A in omega implies A is finite ) ) by CARD_1:103, ORDINAL1:26;
hence ( not A is finite iff omega c= A ) ; :: thesis: verum