theorem :: CARDFIL3:22

for PM being MetrStruct holds the carrier of (TopSpaceMetr PM) = the carrier of TopStruct(# the carrier of PM,(Family_open_set PM) #) by PCOMPS_1:def 5;