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 Z: a < b ; :: thesis: diameter ].a,b.[ = b - a
then A: ].a,b.[ <> {} by XXREAL_1:33;
( inf ].a,b.[ = a & sup ].a,b.[ = b ) by Z, XXREAL_2:28, XXREAL_2:32;
hence diameter ].a,b.[ = b - a by A, Def10; :: thesis: verum

end;

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