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

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