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 \/ Y) c= (card X) +` (card Y) & omega +` omega = omega & (card X) +` (card Y) c= omega +` omega ) by Th33, Th41, CARD_2:47;
hence card (X \/ Y) c= omega by XBOOLE_1:1; :: according to CARD_3:def 15 :: thesis: verum