let GX be TopSpace; :: thesis: for W being Subset-Family of GX st W is closed holds
meet W is closed
let W be Subset-Family of GX; :: thesis: ( W is closed implies meet W is closed )
reconsider C = COMPLEMENT W as Subset-Family of GX ;
assume W is closed ; :: thesis: meet W is closed
then COMPLEMENT W is open by Th16;
then A1: union C is open by Th26;

A2: now

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

end;

now

assume W = {} ; :: thesis: meet W is closed
then meet W = {} GX by SETFAM_1:def 1;
hence meet W is closed ; :: thesis: verum

end;

hence meet W is closed by A2; :: thesis: verum