let a, b be Real; :: thesis: ( a <= b implies ( B-Meas . [.a,b.] = b - a & B-Meas . [.a,b.[ = b - a & B-Meas . ].a,b.] = b - a & B-Meas . ].a,b.[ = b - a & L-Meas . [.a,b.] = b - a & L-Meas . [.a,b.[ = b - a & L-Meas . ].a,b.] = b - a & L-Meas . ].a,b.[ = b - a ) )
assume A1: a <= b ; :: thesis: ( B-Meas . [.a,b.] = b - a & B-Meas . [.a,b.[ = b - a & B-Meas . ].a,b.] = b - a & B-Meas . ].a,b.[ = b - a & L-Meas . [.a,b.] = b - a & L-Meas . [.a,b.[ = b - a & L-Meas . ].a,b.] = b - a & L-Meas . ].a,b.[ = b - a )
reconsider a1 = a, b1 = b as R_eal by XXREAL_0:def 1;
( B-Meas . [.a,b.] = diameter [.a,b.] & L-Meas . [.a,b.] = diameter [.a,b.] ) by MEASUR12:71, MEASUR12:76;
then A2: ( B-Meas . [.a,b.] = b1 - a1 & L-Meas . [.a,b.] = b1 - a1 ) by A1, MEASURE5:6;
A3: ( B-Meas . [.a,b.[ = diameter [.a1,b1.[ & B-Meas . ].a,b.] = diameter ].a1,b1.] & B-Meas . ].a,b.[ = diameter ].a1,b1.[ & L-Meas . [.a,b.[ = diameter [.a1,b1.[ & L-Meas . ].a,b.] = diameter ].a1,b1.] & L-Meas . ].a,b.[ = diameter ].a1,b1.[ ) by MEASUR12:71, MEASUR12:76;

now :: thesis: ( a <> b implies ( B-Meas . [.a,b.[ = b - a & B-Meas . ].a,b.] = b - a & B-Meas . ].a,b.[ = b - a & L-Meas . [.a,b.[ = b - a & L-Meas . ].a,b.] = b - a & L-Meas . ].a,b.[ = b - a ) )

assume a <> b ; :: thesis: ( B-Meas . [.a,b.[ = b - a & B-Meas . ].a,b.] = b - a & B-Meas . ].a,b.[ = b - a & L-Meas . [.a,b.[ = b - a & L-Meas . ].a,b.] = b - a & L-Meas . ].a,b.[ = b - a )
then a1 < b1 by A1, XXREAL_0:1;
then ( B-Meas . [.a,b.[ = b1 - a1 & B-Meas . ].a,b.] = b1 - a1 & B-Meas . ].a,b.[ = b1 - a1 & L-Meas . [.a,b.[ = b1 - a1 & L-Meas . ].a,b.] = b1 - a1 & L-Meas . ].a,b.[ = b1 - a1 ) by A3, MEASURE5:5, MEASURE5:7, MEASURE5:8;
hence ( B-Meas . [.a,b.[ = b - a & B-Meas . ].a,b.] = b - a & B-Meas . ].a,b.[ = b - a & L-Meas . [.a,b.[ = b - a & L-Meas . ].a,b.] = b - a & L-Meas . ].a,b.[ = b - a ) by Lm1; :: thesis: verum

end;

hence ( B-Meas . [.a,b.] = b - a & B-Meas . [.a,b.[ = b - a & B-Meas . ].a,b.] = b - a & B-Meas . ].a,b.[ = b - a & L-Meas . [.a,b.] = b - a & L-Meas . [.a,b.[ = b - a & L-Meas . ].a,b.] = b - a & L-Meas . ].a,b.[ = b - a ) by A2, A3, Lm1, MEASURE5:5, MEASURE5:7, MEASURE5:8; :: thesis: verum