theorem :: MEASURE5:13

for A being Interval holds 0. <= diameter A by Lm1;