let A be set ; :: thesis: ( ( A is finite & ( for X being set st X in A holds
X is finite ) ) iff union A is finite )
thus ( A is finite & ( for X being set st X in A holds
X is finite ) implies union A is finite ) by Lm3; :: thesis: ( union A is finite implies ( A is finite & ( for X being set st X in A holds
X is finite ) ) )
thus ( union A is finite implies ( A is finite & ( for X being set st X in A holds
X is finite ) ) ) :: thesis: verum

proof

assume A1: union A is finite ; :: thesis: ( A is finite & ( for X being set st X in A holds
X is finite ) )
then bool (union A) is finite ;
hence A is finite by Th13, ZFMISC_1:100; :: thesis: for X being set st X in A holds
X is finite
thus for X being set st X in A holds
X is finite by A1, Th13, ZFMISC_1:92; :: thesis: verum

end;