let S be Subset of M; :: thesis: ( S is empty implies S is closed )
assume S is empty ; :: thesis: S is closed
then A2: [#] M = S ` ;
[#] M in Family_open_set M by PCOMPS_1:30;
then [#] M is open ;
hence S is closed by A2; :: thesis: verum