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 Th13, Th16;
then A1: meet C is open by Th27;

now

assume W <> {} ; :: thesis: union W is closed
then meet (COMPLEMENT W) = (union W) ` by Th11;
hence union W is closed by A1, TOPS_1:3; :: thesis: verum

end;

hence union W is closed by ZFMISC_1:2; :: thesis: verum