theorem Th7: :: FINSET_1:7

for A being set holds
( ( A is finite & ( for X being set st X in A holds
X is finite ) ) iff union A is finite )