theorem :: MEASURE5:6

for a, b being R_eal holds
( ( a <= b implies diameter [.a,b.] = b - a ) & ( b < a implies diameter [.a,b.] = 0. ) )