theorem Th7: :: INTEGRA3:7

for i, j being Element of NAT
for A being non empty closed_interval Subset of REAL
for D, D1 being Division of A st D <= D1 & i in dom D & j in dom D & i <= j holds
( indx (D1,D,i) <= indx (D1,D,j) & indx (D1,D,i) in dom D1 )