let I be Element of Family_of_Intervals ; :: thesis: ( I <> {} & I is closed_interval implies OS_Meas . I <= diameter I )
assume that
A1: I <> {} and
A2: I is closed_interval ; :: thesis: OS_Meas . I <= diameter I
consider a, b being Real such that
A3: I = [.a,b.] by A2, MEASURE5:def 3;
reconsider a1 = a, b1 = b as R_eal by XXREAL_0:def 1;
A4: diameter I = b1 - a1 by A1, A3, XXREAL_1:29, MEASURE5:6;
then A5: diameter I = b - a by Lm9;
reconsider DI = diameter I as Real by A4;
A6: 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 A7: ( a - (e / 2) < a & b < b + (e / 2) ) by XREAL_1:29, XREAL_1:44, XREAL_1:215;
reconsider p = a - (e / 2), q = b + (e / 2) as R_eal by XXREAL_0:def 1;
reconsider J = ].p,q.[ as Subset of REAL ;
A8: 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
A9: ( F . 0 = J & ( for n being Nat st n <> 0 holds
F . n = {} ) & union (rng F) = J & SUM (F vol) = diameter J ) by A8, Th36;
reconsider F1 = F as Open_Interval_Covering of I by A3, A7, Th38, XXREAL_1:47;
a <= b by A1, A3, XXREAL_1:29;
then a - (e / 2) < b by A7, XXREAL_0:2;
then a - (e / 2) < b + (e / 2) by A7, XXREAL_0:2;
then diameter J = q - p by MEASURE5:5;
then A10: diameter J = (b + (e / 2)) - (a - (e / 2)) by Lm9;
F vol = F1 vol by Th39;
then vol F1 = diameter J by A9, 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 inf (Svc I) <= diameter J by A12, XXREAL_0:2;
hence OS_Meas . I <= DI + e by A5, A10, MEASURE7:def 10; :: thesis: verum

end;

then A13: OS_Meas . I <= DI + 1 ;
A14: ( 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 A14, A13, XXREAL_0:45;
then reconsider LI = OS_Meas . I as Real ;
for e being Real st 0 < e holds
LI <= DI + e by A6;
hence OS_Meas . I <= diameter I by XREAL_1:41; :: thesis: verum