theorem :: CARDFIL3:21

for PM being MetrStruct holds the carrier of TopStruct(# the carrier of PM,(Family_open_set PM) #) = the carrier of PM ;