theorem Th9: :: CARDFIL3:23

for PM being MetrStruct holds the carrier of (TopSpaceMetr PM) = the carrier of PM