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