let a, b be Real; :: thesis: ( a <= b implies diameter [.a,b.] = b - a )
reconsider a1 = a, b1 = b as R_eal by XXREAL_0:def 1;
assume a <= b ; :: thesis: diameter [.a,b.] = b - a
then diameter [.a,b.] = b1 - a1 by MEASURE5:6;
hence diameter [.a,b.] = b - a by Lm9; :: thesis: verum