theorem :: MEASURE5:7

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