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 )
assume that
A1: W is closed and
A2: W is finite ; :: thesis: union W is closed
reconsider C = COMPLEMENT W as Subset-Family of GX ;
( COMPLEMENT W is open & COMPLEMENT W is finite ) by A1, A2, Th13, Th16;
then A3: meet C is open by Th27;

A4: now

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

end;

now

assume W = {} ; :: thesis: union W is closed
then union W = {} GX by ZFMISC_1:2;
hence union W is closed ; :: thesis: verum

end;

hence union W is closed by A4; :: thesis: verum