theorem Th30: :: PCOMPS_1:30

for PM being MetrStruct holds the carrier of PM in Family_open_set PM