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 15 :: thesis: [:X,Y:] is countable
then [:(card X),(card Y):] c= [:omega,omega:] by ZFMISC_1:119;
then card [:(card X),(card Y):] c= card [:omega,omega:] by CARD_1:27;
then card [:(card X),(card Y):] c= omega *` omega by CARD_2:def 2;
hence card [:X,Y:] c= omega by Th54, CARD_2:14; :: according to CARD_3:def 15 :: thesis: verum