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 that
A1: card X c= omega and
A2: for Y being set st Y in X holds
Y is countable ; :: according to CARD_3:def 14 :: thesis: union X is countable
for Y being set st Y in X holds
card Y c= omega by A2, CARD_3:def 14;
hence card (union X) c= omega by A1, Th6, CARD_2:87; :: according to CARD_3:def 14 :: thesis: verum