for I being Element of Family_of_Intervals st I is Interval holds
OS_Meas . I <= diameter I