for M being MetrStruct
for A being Subset of M
for A9 being Subset of (TopSpaceMetr M) st A9 = A holds
( ( A is open implies A9 is open ) & ( A9 is open implies A is open ) & ( A is closed implies A9 is closed ) & ( A9 is closed implies A is closed ) )