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:31;
( [.a,b.[ <> {} & inf [.a,b.[ = a ) by A1, XXREAL_1:31, XXREAL_2:26;
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:27;
hence diameter [.a,b.[ = 0. by Def6; :: thesis: verum