let I be Element of Family_of_Intervals ; :: thesis: ( I is open_interval implies OS_Meas . I <= diameter I )
assume I is open_interval ; :: thesis: OS_Meas . I <= diameter I
then consider F being Open_Interval_Covering of I such that
A1: ( F . 0 = I & ( for n being Nat st n <> 0 holds
F . n = {} ) & union (rng F) = I & SUM (F vol) = diameter I ) by Th36;
vol F = diameter I by A1, MEASURE7:def 6;
then A2: diameter I in Svc2 I by Def7;
inf (Svc2 I) is LowerBound of Svc2 I by XXREAL_2:def 4;
then A3: inf (Svc2 I) <= diameter I by A2, XXREAL_2:def 2;
inf (Svc I) <= inf (Svc2 I) by Th30;
then inf (Svc I) <= diameter I by A3, XXREAL_0:2;
hence OS_Meas . I <= diameter I by MEASURE7:def 10; :: thesis: verum