let i, j be Element of NAT ; :: thesis: for A, B being closed-interval Subset of REAL
for D being Division of A st i in dom D & j in dom D & i <= j & D . i >= lower_bound B & D . j = upper_bound B holds
mid D,i,j is Division of B
let A, B be closed-interval Subset of REAL ; :: thesis: for D being Division of A st i in dom D & j in dom D & i <= j & D . i >= lower_bound B & D . j = upper_bound B holds
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 & D . i >= lower_bound B & D . j = upper_bound B implies mid D,i,j is Division of B )
assume that
A1: i in dom D and
A2: j in dom D and
A3: i <= j and
A4: D . i >= lower_bound B and
A5: D . j = upper_bound B ; :: thesis: mid D,i,j is Division of B
consider A1 being closed-interval Subset of REAL such that
A6: lower_bound A1 = (mid D,i,j) . 1 and
A7: upper_bound A1 = (mid D,i,j) . (len (mid D,i,j)) and
A8: len (mid D,i,j) = (j - i) + 1 and
A9: mid D,i,j is Division of A1 by A1, A2, A3, Th38;
i in Seg (len D) by A1, FINSEQ_1:def 3;
then A10: 1 <= i by FINSEQ_1:3;
j in Seg (len D) by A2, FINSEQ_1:def 3;
then A11: j <= len D by FINSEQ_1:3;
0 <= j - i by A3, XREAL_1:50;
then A12: 0 + 1 <= (j - i) + 1 by XREAL_1:8;
A13: (1 + i) - 1 = i ;
A14: (((j - i) + 1) + i) - 1 = j ;
A15: A1 c= B

proof

for x being Real st x in A1 holds
x in B

proof

let x be Real; :: thesis: ( x in A1 implies x in B )
assume x in A1 ; :: thesis: x in B
then x in [.(lower_bound A1),(upper_bound A1).] by Th5;
then x in { a where a is Real : ( lower_bound A1 <= a & a <= upper_bound A1 ) } by RCOMP_1:def 1;
then ex a being Real st
( x = a & lower_bound A1 <= a & a <= upper_bound A1 ) ;
then ( D . i <= x & x <= D . j ) by A3, A6, A7, A8, A10, A11, A12, A13, A14, JORDAN3:31;
then ( lower_bound B <= x & x <= upper_bound B ) by A4, A5, XXREAL_0:2;
then x in { a where a is Real : ( lower_bound B <= a & a <= upper_bound B ) } ;
then x in [.(lower_bound B),(upper_bound B).] by RCOMP_1:def 1;
hence x in B by Th5; :: thesis: verum

end;

hence A1 c= B by SUBSET_1:7; :: thesis: verum

end;

rng (mid D,i,j) c= A1 by A9, Def2;
then A16: rng (mid D,i,j) c= B by A15, XBOOLE_1:1;
(mid D,i,j) . (len (mid D,i,j)) = D . j by A3, A8, A10, A11, A12, A14, JORDAN3:31;
then mid D,i,j is Division of B by A5, A9, A16, Def2;
hence mid D,i,j is Division of B ; :: thesis: verum