let S be Subset of M; :: thesis: ( S is empty implies S is open )
A1: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) ;
assume S is empty ; :: thesis: S is open
then S in Family_open_set M by A1, PRE_TOPC:1;
hence S is open ; :: thesis: verum