theorem Th57: :: MEASUR12:57

for I being Interval holds diameter I = OS_Meas . I