theorem Th33: :: PCOMPS_1:33

for PM being MetrStruct holds TopStruct(# the carrier of PM,(Family_open_set PM) #) is TopSpace