let a, b be Real; ( a > b implies ( B-Meas . [.a,b.] = 0 & B-Meas . [.a,b.[ = 0 & B-Meas . ].a,b.] = 0 & B-Meas . ].a,b.[ = 0 & L-Meas . [.a,b.] = 0 & L-Meas . [.a,b.[ = 0 & L-Meas . ].a,b.] = 0 & L-Meas . ].a,b.[ = 0 ) )
assume A1:
a > b
; ( B-Meas . [.a,b.] = 0 & B-Meas . [.a,b.[ = 0 & B-Meas . ].a,b.] = 0 & B-Meas . ].a,b.[ = 0 & L-Meas . [.a,b.] = 0 & L-Meas . [.a,b.[ = 0 & L-Meas . ].a,b.] = 0 & L-Meas . ].a,b.[ = 0 )
reconsider a1 = a, b1 = b as R_eal by XXREAL_0:def 1;
( B-Meas . [.a,b.] = diameter [.a1,b1.] & 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.] & L-Meas . ].a,b.[ = diameter ].a1,b1.[ )
by MEASUR12:71, MEASUR12:76;
hence
( B-Meas . [.a,b.] = 0 & B-Meas . [.a,b.[ = 0 & B-Meas . ].a,b.] = 0 & B-Meas . ].a,b.[ = 0 & L-Meas . [.a,b.] = 0 & L-Meas . [.a,b.[ = 0 & L-Meas . ].a,b.] = 0 & L-Meas . ].a,b.[ = 0 )
by A1, MEASURE5:5, MEASURE5:6, MEASURE5:7, MEASURE5:8; verum