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:2;
hence card X = omega by CARD_1:5, CARD_1:47; :: thesis: verum