let r be Real; :: thesis: for i, j being Element of NAT

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D & j in dom D & i <= j & r < (mid (D,i,j)) . 1 holds

ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )

let i, j be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D & j in dom D & i <= j & r < (mid (D,i,j)) . 1 holds

ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )

let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A st i in dom D & j in dom D & i <= j & r < (mid (D,i,j)) . 1 holds

ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )

let D be Division of A; :: thesis: ( i in dom D & j in dom D & i <= j & r < (mid (D,i,j)) . 1 implies ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B ) )

assume A1: i in dom D ; :: thesis: ( not j in dom D or not i <= j or not r < (mid (D,i,j)) . 1 or ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B ) )

assume A2: j in dom D ; :: thesis: ( not i <= j or not r < (mid (D,i,j)) . 1 or ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B ) )

assume i <= j ; :: thesis: ( not r < (mid (D,i,j)) . 1 or ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B ) )

then consider C being non empty closed_interval Subset of REAL such that

A3: lower_bound C = (mid (D,i,j)) . 1 and

A4: upper_bound C = (mid (D,i,j)) . (len (mid (D,i,j))) and

A5: mid (D,i,j) is Division of C by A1, A2, INTEGRA1:36;

reconsider MD = mid (D,i,j) as non empty increasing FinSequence of REAL by A5;

assume A6: r < (mid (D,i,j)) . 1 ; :: thesis: ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )

reconsider rr = r, ub = upper_bound C as Real ;

ex a, b being Real st

( a <= b & a = lower_bound C & b = upper_bound C ) by SEQ_4:11;

then r <= upper_bound C by A6, A3, XXREAL_0:2;

then reconsider B = [.rr,ub.] as non empty closed_interval Subset of REAL by MEASURE5:14;

A7: B = [.(lower_bound B),(upper_bound B).] by INTEGRA1:4;

then A8: lower_bound B = r by INTEGRA1:5;

A9: upper_bound B = upper_bound C by A7, INTEGRA1:5;

for x being Element of REAL st x in C holds

x in B

rng (mid (D,i,j)) c= C by A5, INTEGRA1:def 2;

then rng (mid (D,i,j)) c= B by A12;

then MD is Division of B by A4, A9, INTEGRA1:def 2;

hence ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B ) by A4, A8, A9; :: thesis: verum

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D & j in dom D & i <= j & r < (mid (D,i,j)) . 1 holds

ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )

let i, j be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D & j in dom D & i <= j & r < (mid (D,i,j)) . 1 holds

ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )

let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A st i in dom D & j in dom D & i <= j & r < (mid (D,i,j)) . 1 holds

ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )

let D be Division of A; :: thesis: ( i in dom D & j in dom D & i <= j & r < (mid (D,i,j)) . 1 implies ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B ) )

assume A1: i in dom D ; :: thesis: ( not j in dom D or not i <= j or not r < (mid (D,i,j)) . 1 or ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B ) )

assume A2: j in dom D ; :: thesis: ( not i <= j or not r < (mid (D,i,j)) . 1 or ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B ) )

assume i <= j ; :: thesis: ( not r < (mid (D,i,j)) . 1 or ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B ) )

then consider C being non empty closed_interval Subset of REAL such that

A3: lower_bound C = (mid (D,i,j)) . 1 and

A4: upper_bound C = (mid (D,i,j)) . (len (mid (D,i,j))) and

A5: mid (D,i,j) is Division of C by A1, A2, INTEGRA1:36;

reconsider MD = mid (D,i,j) as non empty increasing FinSequence of REAL by A5;

assume A6: r < (mid (D,i,j)) . 1 ; :: thesis: ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )

reconsider rr = r, ub = upper_bound C as Real ;

ex a, b being Real st

( a <= b & a = lower_bound C & b = upper_bound C ) by SEQ_4:11;

then r <= upper_bound C by A6, A3, XXREAL_0:2;

then reconsider B = [.rr,ub.] as non empty closed_interval Subset of REAL by MEASURE5:14;

A7: B = [.(lower_bound B),(upper_bound B).] by INTEGRA1:4;

then A8: lower_bound B = r by INTEGRA1:5;

A9: upper_bound B = upper_bound C by A7, INTEGRA1:5;

for x being Element of REAL st x in C holds

x in B

proof

then A12:
C c= B
;
let x be Element of REAL ; :: thesis: ( x in C implies x in B )

assume A10: x in C ; :: thesis: x in B

then lower_bound C <= x by INTEGRA2:1;

then A11: r <= x by A6, A3, XXREAL_0:2;

x <= upper_bound C by A10, INTEGRA2:1;

hence x in B by A8, A9, A11, INTEGRA2:1; :: thesis: verum

end;assume A10: x in C ; :: thesis: x in B

then lower_bound C <= x by INTEGRA2:1;

then A11: r <= x by A6, A3, XXREAL_0:2;

x <= upper_bound C by A10, INTEGRA2:1;

hence x in B by A8, A9, A11, INTEGRA2:1; :: thesis: verum

rng (mid (D,i,j)) c= C by A5, INTEGRA1:def 2;

then rng (mid (D,i,j)) c= B by A12;

then MD is Division of B by A4, A9, INTEGRA1:def 2;

hence ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B ) by A4, A8, A9; :: thesis: verum