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

then ].a,b.] = {} by XXREAL_1:26;

hence diameter ].a,b.] = 0. by Def6; :: thesis: verum

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

assume
b <= a
; :: thesis: diameter ].a,b.] = 0. assume A1:
a < b
; :: thesis: diameter ].a,b.] = b - a

then A2: sup ].a,b.] = b by XXREAL_2:30;

( ].a,b.] <> {} & inf ].a,b.] = a ) by A1, XXREAL_1:32, XXREAL_2:27;

hence diameter ].a,b.] = b - a by A2, Def6; :: thesis: verum

end;then A2: sup ].a,b.] = b by XXREAL_2:30;

( ].a,b.] <> {} & inf ].a,b.] = a ) by A1, XXREAL_1:32, XXREAL_2:27;

hence diameter ].a,b.] = b - a by A2, Def6; :: thesis: verum

then ].a,b.] = {} by XXREAL_1:26;

hence diameter ].a,b.] = 0. by Def6; :: thesis: verum