for M being MetrStruct
for S being SetSequence of M
for S9 being SetSequence of (TopSpaceMetr M) st S9 = S holds
( ( S is open implies S9 is open ) & ( S9 is open implies S is open ) & ( S is closed implies S9 is closed ) & ( S9 is closed implies S is closed ) )