let GX be TopSpace; :: thesis: for W being Subset-Family of GX st W is closed & W is finite holds
union W is closed
let W be Subset-Family of GX; :: thesis: ( W is closed & W is finite implies union W is closed )
reconsider C = COMPLEMENT W as Subset-Family of GX ;
assume ( W is closed & W is finite ) ; :: thesis: union W is closed
then ( COMPLEMENT W is open & COMPLEMENT W is finite ) by Th8, Th9;
then A1: meet C is open by Th20;
now :: thesis: ( W <> {} implies union W is closed )
assume W <> {} ; :: thesis: union W is closed
then meet (COMPLEMENT W) = (union W) ` by Th6;
hence union W is closed by A1; :: thesis: verum
end;
hence union W is closed by ZFMISC_1:2; :: thesis: verum