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
proof
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;
then A12: C c= 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