let I be Element of Family_of_Intervals ; :: thesis: ( I <> {} & I is left_open_interval implies OS_Meas . I <= diameter I )
assume that
A1: I <> {} and
A2: I is left_open_interval ; :: thesis: OS_Meas . I <= diameter I
consider a being R_eal, b being Real such that
A3: I = ].a,b.] by A2, MEASURE5:def 5;
A4: a < b by A1, A3, XXREAL_1:26;
A5: b < +infty by XXREAL_0:9, XREAL_0:def 1;
reconsider b1 = b as R_eal by XXREAL_0:def 1;

per cases ( a = -infty or a <> -infty ) ;

suppose a = -infty ; :: thesis: OS_Meas . I <= diameter I

then diameter I = b1 - -infty by A1, A3, XXREAL_1:26, MEASURE5:8
.= +infty by XXREAL_3:14 ;
hence OS_Meas . I <= diameter I by XXREAL_0:3; :: thesis: verum

end;

suppose a <> -infty ; :: thesis: OS_Meas . I <= diameter I

then a in REAL by A4, A5, XXREAL_0:14;
then reconsider ra = a as Real ;
diameter I = b1 - a by A1, A3, XXREAL_1:26, MEASURE5:8;
then A6: diameter I = b - ra by Lm9;
then reconsider DI = diameter I as Real ;
A7: for e being Real st 0 < e holds
OS_Meas . I <= DI + e

proof

let e be Real; :: thesis: ( 0 < e implies OS_Meas . I <= DI + e )
assume 0 < e ; :: thesis: OS_Meas . I <= DI + e
then A8: b < b + e by XREAL_1:29;
reconsider c = b + e as R_eal by XXREAL_0:def 1;
reconsider J = ].a,c.[ as Subset of REAL ;
A9: J in Family_of_Intervals by MEASUR10:def 1;
J is open_interval by MEASURE5:def 2;
then consider F being Open_Interval_Covering of J such that
A10: ( F . 0 = J & ( for n being Nat st n <> 0 holds
F . n = {} ) & union (rng F) = J & SUM (F vol) = diameter J ) by A9, Th36;
reconsider F1 = F as Open_Interval_Covering of I by A3, A8, Th38, XXREAL_1:49;
F vol = F1 vol by Th39;
then vol F1 = diameter J by A10, MEASURE7:def 6;
then A11: diameter J in Svc2 I by Def7;
inf (Svc2 I) is LowerBound of Svc2 I by XXREAL_2:def 4;
then A12: inf (Svc2 I) <= diameter J by A11, XXREAL_2:def 2;
inf (Svc I) <= inf (Svc2 I) by Th30;
then A13: inf (Svc I) <= diameter J by A12, XXREAL_0:2;
a < b + e by A1, A3, A8, XXREAL_1:26, XXREAL_0:2;
then diameter J = c - a by MEASURE5:5;
then diameter J = (b + e) - ra by Lm9;
hence OS_Meas . I <= DI + e by A6, A13, MEASURE7:def 10; :: thesis: verum

end;

then A14: OS_Meas . I <= DI + 1 ;
A15: ( 0 in REAL & DI + 1 in REAL ) by XREAL_0:def 1;
OS_Meas is nonnegative by MEASURE4:def 1;
then 0 <= OS_Meas . I by SUPINF_2:51;
then OS_Meas . I in REAL by A15, A14, XXREAL_0:45;
then reconsider LI = OS_Meas . I as Real ;
for e being Real st 0 < e holds
LI <= DI + e by A7;
hence OS_Meas . I <= diameter I by XREAL_1:41; :: thesis: verum

end;

end;