theorem :: EUCLID:63

for n being Nat
for P being Subset of (TOP-REAL n)
for Q being non empty Subset of (Euclid n) st P = Q holds
(TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q)