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