for I being Element of Family_of_Intervals st I <> {} & I is right_open_interval holds
OS_Meas . I <= diameter I