for I being non empty closed_interval Subset of REAL
for D being Division of I holds
( divset (D,1) = [.(lower_bound I),(D . 1).] & ( for j being Nat st j in dom D & j <> 1 holds
divset (D,j) = [.(D . (j - 1)),(D . j).] ) )