let I be Interval; :: thesis: pre-Meas . I = diameter I
I in { J where J is Interval : verum } ;
hence pre-Meas . I = diameter I by Th58, MEASUR10:def 1; :: thesis: verum