let A, B be Interval; :: thesis: ( A c= B implies diameter A <= diameter B )
assume A1: A c= B ; :: thesis: diameter A <= diameter B

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

suppose A = {} ; :: thesis: diameter A <= diameter B

then diameter A = 0 by Def6;
hence diameter A <= diameter B by Lm1; :: thesis: verum

end;

suppose A2: A <> {} ; :: thesis: diameter A <= diameter B

then B <> {} by A1;
then A3: diameter B = (sup B) - (inf B) by Def6;
A4: ( sup A <= sup B & inf B <= inf A ) by A1, XXREAL_2:59, XXREAL_2:60;
diameter A = (sup A) - (inf A) by A2, Def6;
hence diameter A <= diameter B by A3, A4, XXREAL_3:37; :: thesis: verum

end;

end;