let r be Real; :: thesis: for i, j being Element of NAT
for A being 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 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 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 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 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 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 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 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 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 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 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
A6: mid (D,i,j) is Division of C by A1, A2, INTEGRA1:38;
reconsider MD = mid (D,i,j) as non empty increasing FinSequence of REAL by A6;
assume A7: r < (mid (D,i,j)) . 1 ; :: thesis: ex B being 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 )
ex a, b being Real st
( a <= b & a = lower_bound C & b = upper_bound C ) by INTEGRA1:4;
then r <= upper_bound C by A7, A3, XXREAL_0:2;
then reconsider B = [.r,(upper_bound C).] as closed-interval Subset of REAL by INTEGRA1:def 1;
A8: B = [.(lower_bound B),(upper_bound B).] by INTEGRA1:5;
then A9: lower_bound B = r by INTEGRA1:6;
A10: upper_bound B = upper_bound C by A8, INTEGRA1:6;
for x being Real st x in C holds
x in B

proof

let x be Real; :: thesis: ( x in C implies x in B )
assume A11: x in C ; :: thesis: x in B
then lower_bound C <= x by INTEGRA2:1;
then A12: r <= x by A7, A3, XXREAL_0:2;
x <= upper_bound C by A11, INTEGRA2:1;
hence x in B by A9, A10, A12, INTEGRA2:1; :: thesis: verum

end;

then A13: C c= B by SUBSET_1:7;
rng (mid (D,i,j)) c= C by A6, INTEGRA1:def 2;
then rng (mid (D,i,j)) c= B by A13, XBOOLE_1:1;
then MD is Division of B by A4, A10, INTEGRA1:def 2;
hence ex B being 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, A9, A10; :: thesis: verum