let X be set ; :: thesis: ( not X is finite & X c= omega implies card X = omega )
assume ( not X is finite & X c= omega ) ; :: thesis: card X = omega
then NAT ,X are_equipotent by WAYBEL12:3;
hence card X = omega by CARD_1:21, CARD_1:84; :: thesis: verum