let Y be Subset of X; :: thesis: Y is countable
A1: card Y c= card X by CARD_1:27;
card X c= omega by Def15;
hence card Y c= omega by A1, XBOOLE_1:1; :: according to CARD_3:def 15 :: thesis: verum