theorem :: CARDFIL3:20

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