let a, b be R_eal; :: thesis: ( ( a <= b implies diameter [.a,b.] = b - a ) & ( b < a implies diameter [.a,b.] = 0. ) )

hereby :: thesis: ( b < a implies diameter [.a,b.] = 0. )

assume A1: a <= b ; :: thesis: diameter [.a,b.] = b - a
then A2: sup [.a,b.] = b by XXREAL_2:29;
( [.a,b.] <> {} & inf [.a,b.] = a ) by A1, XXREAL_1:30, XXREAL_2:25;
hence diameter [.a,b.] = b - a by A2, Def6; :: thesis: verum

end;

assume b < a ; :: thesis: diameter [.a,b.] = 0.
then [.a,b.] = {} by XXREAL_1:29;
hence diameter [.a,b.] = 0. by Def6; :: thesis: verum