let S be Subset of M; :: thesis: ( S is empty implies S is closed )
assume Z: S is empty ; :: thesis: S is closed
[#] M in Family_open_set M by PCOMPS_1:34;
then ( [#] M is open & [#] M = (([#] M) ` ) ` & [#] M = S ` ) by Def3, Z;
then ( ([#] M) ` is closed & ([#] M) ` = S ) by Def4;
hence S is closed ; :: thesis: verum