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

per cases ( I = {} or I <> {} ) ;

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

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

end;

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

( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) by A1, MEASURE5:1;
hence OS_Meas . I <= diameter I by A3, Th42, Th43, Lm10, Lm11; :: thesis: verum

end;

end;