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