let i, j be Element of NAT ; :: thesis: 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 )

let A be non empty 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) & indx (D1,D,i) in dom D1 )

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) & indx (D1,D,i) in dom D1 ) )

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) & indx (D1,D,i) in dom D1 )

A5: D . i = D1 . (indx (D1,D,i)) by A1, A2, INTEGRA1:def 19;

A6: indx (D1,D,j) in dom D1 by A1, A3, INTEGRA1:def 19;

A7: D . j = D1 . (indx (D1,D,j)) by A1, A3, INTEGRA1:def 19;

A8: indx (D1,D,i) in dom D1 by A1, A2, INTEGRA1:def 19;

D . i <= D . j by A2, A3, A4, SEQ_4:137;

hence ( indx (D1,D,i) <= indx (D1,D,j) & indx (D1,D,i) in dom D1 ) by A5, A8, A7, A6, SEQM_3:def 1; :: thesis: verum

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 )

let A be non empty 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) & indx (D1,D,i) in dom D1 )

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) & indx (D1,D,i) in dom D1 ) )

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) & indx (D1,D,i) in dom D1 )

A5: D . i = D1 . (indx (D1,D,i)) by A1, A2, INTEGRA1:def 19;

A6: indx (D1,D,j) in dom D1 by A1, A3, INTEGRA1:def 19;

A7: D . j = D1 . (indx (D1,D,j)) by A1, A3, INTEGRA1:def 19;

A8: indx (D1,D,i) in dom D1 by A1, A2, INTEGRA1:def 19;

D . i <= D . j by A2, A3, A4, SEQ_4:137;

hence ( indx (D1,D,i) <= indx (D1,D,j) & indx (D1,D,i) in dom D1 ) by A5, A8, A7, A6, SEQM_3:def 1; :: thesis: verum