let X be set ; :: thesis: ( X is infinite & X c= omega implies card X = omega )
assume ( X is infinite & 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