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)) & len (mid D,i,j) = (j - i) + 1 & 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)) & len (mid D,i,j) = (j - i) + 1 & 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)) & len (mid D,i,j) = (j - i) + 1 & 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)) & len (mid D,i,j) = (j - i) + 1 & 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)) & len (mid D,i,j) = (j - i) + 1 & 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)) & len (mid D,i,j) = (j - i) + 1 & mid D,i,j is Division of B ) )
assume A3: 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)) & len (mid D,i,j) = (j - i) + 1 & mid D,i,j is Division of B ) )
assume A4: 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)) & len (mid D,i,j) = (j - i) + 1 & mid D,i,j is Division of B )
consider C being closed-interval Subset of REAL such that
A5: ( lower_bound C = (mid D,i,j) . 1 & upper_bound C = (mid D,i,j) . (len (mid D,i,j)) & len (mid D,i,j) = (j - i) + 1 & mid D,i,j is Division of C ) by A1, A2, A3, INTEGRA1:38;
consider a, b being Real such that
A6: ( a <= b & a = lower_bound C & b = upper_bound C ) by INTEGRA1:4;
r <= upper_bound C by A4, A5, A6, XXREAL_0:2;
then reconsider B = [.r,(upper_bound C).] as closed-interval Subset of REAL by INTEGRA1:def 1;
reconsider MD = mid D,i,j as non empty increasing FinSequence of REAL by A5;
B = [.(lower_bound B),(upper_bound B).] by INTEGRA1:5;
then A7: ( lower_bound B = r & upper_bound B = upper_bound C ) by INTEGRA1:6;
A8: ( rng (mid D,i,j) c= C & (mid D,i,j) . (len (mid D,i,j)) = upper_bound C ) by A5, INTEGRA1:def 2;
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 x in C ; :: thesis: x in B
then ( lower_bound C <= x & x <= upper_bound C ) by INTEGRA2:1;
then ( r <= x & x <= upper_bound C ) by A4, A5, XXREAL_0:2;
hence x in B by A7, INTEGRA2:1; :: thesis: verum

end;

then C c= B by SUBSET_1:7;
then rng (mid D,i,j) c= B by A8, XBOOLE_1:1;
then MD is Division of B by A5, A7, 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)) & len (mid D,i,j) = (j - i) + 1 & mid D,i,j is Division of B ) by A5, A7; :: thesis: verum