theorem Th4: :: PCOMPS_2:4

for PT being non empty TopSpace
for PM being MetrSpace
for f being Function of [: the carrier of PT, the carrier of PT:],REAL st f is_metric_of the carrier of PT & PM = SpaceMetr ( the carrier of PT,f) holds
the carrier of PM = the carrier of PT