for A being non empty closed_interval Subset of REAL
for D1, D2 being Division of A st len D1 = 1 holds
D1 <= D2