for PM being MetrStruct
for A being Subset-Family of PM st A c= Family_open_set PM holds
union A in Family_open_set PM