let X be set ; :: thesis: ( X is countable & ( for Y being set st Y in X holds
Y is countable ) implies union X is countable )
assume A1: ( card X c= omega & ( for Y being set st Y in X holds
Y is countable ) ) ; :: according to CARD_3:def 15 :: thesis: union X is countable

now

let Y be set ; :: thesis: ( Y in X implies card Y c= omega )
assume Y in X ; :: thesis: card Y c= omega
then Y is countable by A1;
hence card Y c= omega by CARD_3:def 15; :: thesis: verum

end;

hence card (union X) c= omega by A1, Th54, CARD_3:133; :: according to CARD_3:def 15 :: thesis: verum