let A be Interval; :: thesis: diameter A >= 0

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: diameter A >= 0

hence diameter A >= 0 by Def6; :: thesis: verum

end;

suppose not A is empty ; :: thesis: diameter A >= 0

then inf A <= sup A by XXREAL_2:40;
then (sup A) - (inf A) >= 0 by XXREAL_3:40;
hence diameter A >= 0 by Def6; :: thesis: verum

end;

end;