for A being non empty closed_interval Subset of REAL
for D1, D2 being Division of A st D1 <= D2 holds
for j being Nat st j in dom D2 holds
ex i being Nat st
( i in dom D1 & divset (D2,j) c= divset (D1,i) )