let I be Element of Family_of_Intervals ; :: thesis: ( not I is empty & I is left_open_interval & diameter I < +infty implies diameter I <= OS_Meas . I )
assume that
A1: ( not I is empty & I is left_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 V115() 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 a1 being R_eal, r2 being Real such that
A4: I = ].a1,r2.] by A1, MEASURE5:def 5;
reconsider a2 = r2 as R_eal by XXREAL_0:def 1;
A5: now :: thesis: not a1 = -infty
assume a1 = -infty ; :: thesis: contradiction
then diameter I = a2 - -infty by A1, A4, XXREAL_1:26, MEASURE5:8;
then diameter I = r2 + +infty by XXREAL_3:5, XXREAL_3:def 4;
hence contradiction by A2, XXREAL_3:def 2; :: thesis: verum
end;
a1 <> +infty by A1, A4, XXREAL_1:26, XXREAL_0:3;
then a1 in REAL by A5, XXREAL_0:14;
then reconsider r1 = a1 as Real ;
DI = a2 - a1 by A1, A4, XXREAL_1:26, MEASURE5:8;
then A6: DI = r2 - r1 by Lm9;
then 0 < DI by A1, A4, XXREAL_1:26, 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);
min ((DI / 2),e) > 0 by A7, A8, XXREAL_0:21;
then A9: ( r1 < r1 + ((min ((DI / 2),e)) / 2) & r2 - ((min ((DI / 2),e)) / 2) < r2 ) by XREAL_1:29, XREAL_1:44, XREAL_1:215;
( 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;
J c= I by A4, A9, XXREAL_1:39;
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