theorem Th32: :: CARD_LAR:32
for X being set st ( for x being set st x in X holds
ex y being set st
( y in X & x c= y & y is Cardinal ) ) holds
union X is Cardinal