let I be Element of Family_of_Intervals ; :: thesis: ( not I is empty & I is right_open_interval & diameter I < +infty implies diameter I <= OS_Meas . I )
assume that
A1: ( not I is empty & I is right_open_interval ) and
A2: diameter I < +infty ; :: thesis: diameter I <= OS_Meas . I
0 <= diameter I by A1, MEASURE5:13;
then diameter I in REAL by A2, XXREAL_0:14;
then reconsider DI = diameter I as Real ;
A3: OS_Meas . I <= diameter I by A1, Th44;
OS_Meas is nonnegative by MEASURE4:def 1;
then ( -infty < 0 & 0 <= OS_Meas . I ) by SUPINF_2:51;
then OS_Meas . I in REAL by A2, A3, XXREAL_0:14;
then reconsider LI = OS_Meas . I as Real ;
consider r1 being Real, a2 being R_eal such that
A4: I = [.r1,a2.[ by A1, MEASURE5:def 4;
reconsider a1 = r1 as R_eal by XXREAL_0:def 1;

A5: now :: thesis: not a2 = +infty

assume a2 = +infty ; :: thesis: contradiction
then diameter I = +infty - a1 by A1, A4, XXREAL_1:27, MEASURE5:7;
then diameter I = +infty + (- a1) by XXREAL_3:def 4;
hence contradiction by A2, XXREAL_3:def 2; :: thesis: verum

end;

a2 <> -infty by A1, A4, XXREAL_1:27, XXREAL_0:5;
then a2 in REAL by A5, XXREAL_0:14;
then reconsider r2 = a2 as Real ;
DI = a2 - a1 by A1, A4, XXREAL_1:27, MEASURE5:7;
then A6: DI = r2 - r1 by Lm9;
then 0 < DI by A1, A4, XXREAL_1:27, XREAL_1:50;
then A7: ( DI / 2 < DI & 0 < DI / 2 ) by XREAL_1:215, XREAL_1:216;
for e being Real st 0 < e holds
DI <= LI + e

proof

let e be Real; :: thesis: ( 0 < e implies DI <= LI + e )
assume A8: 0 < e ; :: thesis: DI <= LI + e
set e1 = min ((DI / 2),e);
A9: min ((DI / 2),e) > 0 by A7, A8, XXREAL_0:21;
( min ((DI / 2),e) <= DI / 2 & min ((DI / 2),e) <= e ) by XXREAL_0:17;
then A10: min ((DI / 2),e) < DI by A7, XXREAL_0:2;
set J = [.(r1 + ((min ((DI / 2),e)) / 2)),(r2 - ((min ((DI / 2),e)) / 2)).];
(r2 - ((min ((DI / 2),e)) / 2)) - (r1 + ((min ((DI / 2),e)) / 2)) = DI - (min ((DI / 2),e)) by A6;
then (r2 - ((min ((DI / 2),e)) / 2)) - (r1 + ((min ((DI / 2),e)) / 2)) > 0 by A10, XREAL_1:50;
then A11: r1 + ((min ((DI / 2),e)) / 2) < r2 - ((min ((DI / 2),e)) / 2) by XREAL_1:47;
then reconsider J = [.(r1 + ((min ((DI / 2),e)) / 2)),(r2 - ((min ((DI / 2),e)) / 2)).] as non empty closed_interval Subset of REAL by MEASURE5:14;
reconsider j1 = r1 + ((min ((DI / 2),e)) / 2), j2 = r2 - ((min ((DI / 2),e)) / 2) as R_eal by XXREAL_0:def 1;
A12: diameter J = j2 - j1 by A11, MEASURE5:6;
then reconsider DJ = diameter J as Real ;
diameter J = (r2 - ((min ((DI / 2),e)) / 2)) - (r1 + ((min ((DI / 2),e)) / 2)) by A12, Lm9;
then DI = DJ + (min ((DI / 2),e)) by A6;
then A13: DI <= DJ + e by XXREAL_0:17, XREAL_1:6;
J in { I where I is Interval : verum } ;
then A14: diameter J <= OS_Meas . J by Lm14, MEASUR10:def 1;
( r1 < r1 + ((min ((DI / 2),e)) / 2) & r2 - ((min ((DI / 2),e)) / 2) < r2 ) by A9, XREAL_1:29, XREAL_1:44, XREAL_1:215;
then J c= I by A4, XXREAL_1:43;
then OS_Meas . J <= LI by MEASURE4:def 1;
then DJ <= LI by A14, XXREAL_0:2;
then DJ + e <= LI + e by XREAL_1:6;
hence DI <= LI + e by A13, XXREAL_0:2; :: thesis: verum

end;

hence diameter I <= OS_Meas . I by XREAL_1:41; :: thesis: verum