let I be Interval; :: thesis: diameter I <= OS_Meas . I
A1: I in { I where I is Interval : verum } ;

per cases ( I = {} or ( I <> {} & diameter I = +infty ) or ( I <> {} & diameter I <> +infty ) ) ;

suppose A2: I = {} ; :: thesis: diameter I <= OS_Meas . I

OS_Meas is zeroed by MEASURE4:def 1;
then OS_Meas . I = 0 by A2, VALUED_0:def 19;
hence diameter I <= OS_Meas . I by A2, MEASURE5:def 6; :: thesis: verum

end;

suppose ( I <> {} & diameter I = +infty ) ; :: thesis: diameter I <= OS_Meas . I

hence diameter I <= OS_Meas . I by A1, Lm21, MEASUR10:def 1; :: thesis: verum

end;

suppose A3: ( I <> {} & diameter I <> +infty ) ; :: thesis: diameter I <= OS_Meas . I

( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) by MEASURE5:1;
hence diameter I <= OS_Meas . I by A1, A3, Lm15, Lm16, Lm17, Lm20, XXREAL_0:4, MEASUR10:def 1; :: thesis: verum

end;

end;