theorem Th8: :: INTEGRA3:8

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)