let Y be Subset of X; :: thesis: Y is countable
A1: card Y c= card X by CARD_1:11;
card X c= omega by Def14;
hence card Y c= omega by A1; :: according to CARD_3:def 14 :: thesis: verum