let I be Element of Family_of_Intervals ; :: thesis: ( diameter I = +infty implies diameter I <= OS_Meas . I )
assume A1: diameter I = +infty ; :: thesis: diameter I <= OS_Meas . I

A2: now :: thesis: not inf I = sup I

assume inf I = sup I ; :: thesis: contradiction
then diameter I = (sup I) - (sup I) by A1, MEASURE5:def 6;
then diameter I = (sup I) + (- (sup I)) by XXREAL_3:def 4;
hence contradiction by A1, XXREAL_3:7; :: thesis: verum

end;

I in { I where I is Interval : verum } by MEASUR10:def 1;
then A3: ex L being Interval st I = L ;
A4: for R being Real holds R <= OS_Meas . I

proof

let R be Real; :: thesis: R <= OS_Meas . I

per cases ( R <= 0 or R > 0 ) ;

suppose A5: R <= 0 ; :: thesis: R <= OS_Meas . I

OS_Meas is nonnegative by MEASURE4:def 1;
hence R <= OS_Meas . I by A5, SUPINF_2:51; :: thesis: verum

end;

suppose A6: R > 0 ; :: thesis: R <= OS_Meas . I

ex J being non empty closed_interval Subset of REAL st
( R = OS_Meas . J & J c= I )

proof

per cases ( ( sup I = +infty & inf I = -infty ) or ( sup I = +infty & inf I <> -infty ) or ( sup I <> +infty & inf I = -infty ) ) by A1, Lm19;

suppose A7: ( sup I = +infty & inf I = -infty ) ; :: thesis: ex J being non empty closed_interval Subset of REAL st
( R = OS_Meas . J & J c= I )

reconsider J = [.0,R.] as non empty closed_interval Subset of REAL by A6, MEASURE5:14;
take J ; :: thesis: ( R = OS_Meas . J & J c= I )

A8: now :: thesis: for r being Real st r in J holds
r in I

let r be Real; :: thesis: ( r in J implies r in I )
assume r in J ; :: thesis: r in I
( inf I < r & r < sup I ) by A7, XXREAL_0:4, XXREAL_0:6;
hence r in I by A3, XXREAL_2:83; :: thesis: verum

end;

diameter J = R - 0 by A6, Lm18;
hence ( R = OS_Meas . J & J c= I ) by A8, Lm20; :: thesis: verum

end;

suppose A9: ( sup I = +infty & inf I <> -infty ) ; :: thesis: ex J being non empty closed_interval Subset of REAL st
( R = OS_Meas . J & J c= I )

then inf I in REAL by A2, XXREAL_0:14;
then reconsider r = inf I as Real ;
A10: ( r < r + 1 & r + 1 < (r + 1) + R ) by A6, XREAL_1:29;
then reconsider J = [.(r + 1),((r + 1) + R).] as non empty closed_interval Subset of REAL by MEASURE5:14;
take J ; :: thesis: ( R = OS_Meas . J & J c= I )

A11: now :: thesis: for p being Real st p in J holds
p in I

let p be Real; :: thesis: ( p in J implies p in I )
assume p in J ; :: thesis: p in I
then ( r + 1 <= p & p <= (r + 1) + R ) by XXREAL_1:1;
then ( inf I < p & p < sup I ) by A9, A10, XXREAL_0:2, XXREAL_0:4;
hence p in I by A3, XXREAL_2:83; :: thesis: verum

end;

diameter J = ((r + 1) + R) - (r + 1) by A10, Lm18;
hence ( R = OS_Meas . J & J c= I ) by A11, Lm20; :: thesis: verum

end;

suppose A12: ( sup I <> +infty & inf I = -infty ) ; :: thesis: ex J being non empty closed_interval Subset of REAL st
( R = OS_Meas . J & J c= I )

then sup I in REAL by A2, XXREAL_0:14;
then reconsider r = sup I as Real ;
A13: ( (r - 1) - R < r - 1 & r - 1 < r ) by A6, XREAL_1:44;
then reconsider J = [.((r - 1) - R),(r - 1).] as non empty closed_interval Subset of REAL by MEASURE5:14;
take J ; :: thesis: ( R = OS_Meas . J & J c= I )

A14: now :: thesis: for p being Real st p in J holds
p in I

let p be Real; :: thesis: ( p in J implies p in I )
assume p in J ; :: thesis: p in I
then ( (r - 1) - R <= p & p <= r - 1 ) by XXREAL_1:1;
then ( inf I < p & p < sup I ) by A12, A13, XXREAL_0:2, XXREAL_0:6;
hence p in I by A3, XXREAL_2:83; :: thesis: verum

end;

diameter J = (r - 1) - ((r - 1) - R) by A13, Lm18
.= R ;
hence ( R = OS_Meas . J & J c= I ) by A14, Lm20; :: thesis: verum

end;

end;

end;

hence R <= OS_Meas . I by MEASURE4:def 1; :: thesis: verum

end;

end;

end;

now :: thesis: not OS_Meas . I <> +infty

assume A15: OS_Meas . I <> +infty ; :: thesis: contradiction
OS_Meas is nonnegative by MEASURE4:def 1;
then OS_Meas . I >= 0 by SUPINF_2:51;
then OS_Meas . I in REAL by A15, XXREAL_0:14;
then reconsider R0 = OS_Meas . I as Real ;
R0 < R0 + 1 by XREAL_1:29;
hence contradiction by A4; :: thesis: verum

end;

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