let I be Element of Family_of_Intervals ; :: thesis: ( I <> {} & I is right_open_interval implies OS_Meas . I <= diameter I )
assume that
A1: I <> {} and
A2: I is right_open_interval ; :: thesis: OS_Meas . I <= diameter I
consider a being Real, b being R_eal such that
A3: I = [.a,b.[ by A2, MEASURE5:def 4;
A4: a < b by A1, A3, XXREAL_1:27;
reconsider a1 = a as R_eal by XXREAL_0:def 1;

per cases ( b = +infty or b <> +infty ) ;

suppose b = +infty ; :: thesis: OS_Meas . I <= diameter I

then diameter I = +infty - a1 by A1, A3, XXREAL_1:27, MEASURE5:7
.= +infty by XXREAL_3:13 ;
hence OS_Meas . I <= diameter I by XXREAL_0:3; :: thesis: verum

end;

suppose A5: b <> +infty ; :: thesis: OS_Meas . I <= diameter I

-infty < a by XXREAL_0:12, XREAL_0:def 1;
then b in REAL by A4, A5, XXREAL_0:14;
then reconsider rb = b as Real ;
A6: diameter I = b - a1 by A1, A3, XXREAL_1:27, MEASURE5:7
.= rb - a 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 A8: 0 < e ; :: thesis: OS_Meas . I <= DI + e
reconsider c = a - e as R_eal by XXREAL_0:def 1;
reconsider J = ].c,b.[ 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;
A11: c < a by A8, XREAL_1:44;
then reconsider F1 = F as Open_Interval_Covering of I by A3, Th38, XXREAL_1:48;
F vol = F1 vol by Th39;
then vol F1 = diameter J by A10, MEASURE7:def 6;
then A12: diameter J in Svc2 I by Def7;
inf (Svc2 I) is LowerBound of Svc2 I by XXREAL_2:def 4;
then A13: inf (Svc2 I) <= diameter J by A12, XXREAL_2:def 2;
inf (Svc I) <= inf (Svc2 I) by Th30;
then A14: inf (Svc I) <= diameter J by A13, XXREAL_0:2;
c < b by A1, A3, XXREAL_1:27, A11, XXREAL_0:2;
then diameter J = b - c by MEASURE5:5;
then diameter J = rb - (a - e) by Lm9;
hence OS_Meas . I <= DI + e by A6, A14, MEASURE7:def 10; :: thesis: verum

end;

then A15: OS_Meas . I <= DI + 1 ;
A16: ( 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, A16, 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;