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

assume A1: A c= B ; :: thesis: diameter A <= diameter B

assume A1: A c= B ; :: thesis: diameter A <= diameter B

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

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;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