let I be Element of Family_of_Intervals ; :: thesis: pre-Meas . I = diameter I
I in { J where J is Interval : verum } by MEASUR10:def 1;
then A1: ex J being Interval st I = J ;
pre-Meas . I = OS_Meas . I by FUNCT_1:49;
hence pre-Meas . I = diameter I by A1, Th57; :: thesis: verum