let A be Interval; :: thesis: L-Meas . A = diameter A
A \/ {} = A ;
then L-Meas . A = B-Meas . A by Th73, Th75, MEASURE3:def 5;
hence L-Meas . A = diameter A by Th72; :: thesis: verum