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