let I be non empty closed_interval Subset of REAL; :: thesis: diameter I = OS_Meas . I
I in { I where I is Interval : verum } ;
then ( OS_Meas . I <= diameter I & diameter I <= OS_Meas . I ) by Th44, Lm14, MEASUR10:def 1;
hence diameter I = OS_Meas . I by XXREAL_0:1; :: thesis: verum