theorem Th10: :: SRINGS_5:12

for n being Nat
for O1 being Subset of (TOP-REAL n)
for O2 being Subset of (TopSpaceMetr (Euclid n)) st O1 = O2 holds
( O1 is open iff O2 is open )