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