let i, j be Element of NAT ; :: thesis: for A being 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
let A be closed-interval Subset of REAL ; :: thesis: 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
let D, D1 be Division of A; :: thesis: ( D <= D1 & i in dom D & j in dom D & i < j implies indx D1,D,i < indx D1,D,j )
assume that
A1: D <= D1 and
A2: i in dom D and
A3: j in dom D and
A4: i < j ; :: thesis: indx D1,D,i < indx D1,D,j
A5: D . i = D1 . (indx D1,D,i) by A1, A2, INTEGRA1:def 21;
A6: indx D1,D,j in dom D1 by A1, A3, INTEGRA1:def 21;
A7: D . j = D1 . (indx D1,D,j) by A1, A3, INTEGRA1:def 21;
A8: indx D1,D,i in dom D1 by A1, A2, INTEGRA1:def 21;
D . i < D . j by A2, A3, A4, SEQM_3:def 1;
hence indx D1,D,i < indx D1,D,j by A5, A8, A7, A6, SEQ_4:154; :: thesis: verum