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 ) )
A c= bool (union A) by ZFMISC_1:82;
hence A is finite by A1; :: thesis: for X being set st X in A holds
X is finite
let X be set ; :: thesis: ( X in A implies X is finite )
assume X in A ; :: thesis: X is finite
then X c= union A by ZFMISC_1:74;
hence X is finite by A1; :: thesis: verum
end;