let X, Y be set ; :: thesis: ( X is countable & Y is countable implies X \/ Y is countable )
assume that
A1: card X c= omega and
A2: card Y c= omega ; :: according to CARD_3:def 14 :: thesis: X \/ Y is countable
A3: card (X \/ Y) c= (card X) +` (card Y) by Th33;
A4: omega +` omega = omega by Th74;
(card X) +` (card Y) c= omega +` omega by A1, A2, Th82;
hence card (X \/ Y) c= omega by A3, A4; :: according to CARD_3:def 14 :: thesis: verum