for I being Element of Family_of_Intervals holds pre-Meas . I = diameter I