let X, Y be set ; :: thesis: ( X is countable & Y is countable implies [:X,Y:] is countable )
assume ( card X c= omega & card Y c= omega ) ; :: according to CARD_3:def 14 :: thesis: [:X,Y:] is countable
then [:(card X),(card Y):] c= [:omega,omega:] by ZFMISC_1:96;
then card [:(card X),(card Y):] c= card [:omega,omega:] by CARD_1:11;
then card [:(card X),(card Y):] c= omega *` omega by CARD_2:def 2;
hence card [:X,Y:] c= omega by Th6, CARD_2:7; :: according to CARD_3:def 14 :: thesis: verum