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 Th9;
then A1: union C is open by Th19;

A2: now :: thesis: ( W <> {} implies meet W is closed )

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

end;

now :: thesis: ( W = {} implies meet W is closed )

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