for PM being MetrStruct
for V, W being Subset of PM st V in Family_open_set PM & W in Family_open_set PM holds
V /\ W in Family_open_set PM