let r be Real; :: thesis: for i, j being Element of NAT
for A being non empty closed_interval Subset of REAL
for D1, D2 being Division of A st i in dom D1 & j in dom D1 & i <= j & D1 <= D2 & r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 holds
ex B being non empty closed_interval Subset of REAL ex MD1, MD2 being Division of B st
( r = lower_bound B & upper_bound B = MD2 . (len MD2) & upper_bound B = MD1 . (len MD1) & MD1 <= MD2 & MD1 = mid (D1,i,j) & MD2 = mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) )

let i, j be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL
for D1, D2 being Division of A st i in dom D1 & j in dom D1 & i <= j & D1 <= D2 & r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 holds
ex B being non empty closed_interval Subset of REAL ex MD1, MD2 being Division of B st
( r = lower_bound B & upper_bound B = MD2 . (len MD2) & upper_bound B = MD1 . (len MD1) & MD1 <= MD2 & MD1 = mid (D1,i,j) & MD2 = mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) )

let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A st i in dom D1 & j in dom D1 & i <= j & D1 <= D2 & r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 holds
ex B being non empty closed_interval Subset of REAL ex MD1, MD2 being Division of B st
( r = lower_bound B & upper_bound B = MD2 . (len MD2) & upper_bound B = MD1 . (len MD1) & MD1 <= MD2 & MD1 = mid (D1,i,j) & MD2 = mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) )

let D1, D2 be Division of A; :: thesis: ( i in dom D1 & j in dom D1 & i <= j & D1 <= D2 & r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 implies ex B being non empty closed_interval Subset of REAL ex MD1, MD2 being Division of B st
( r = lower_bound B & upper_bound B = MD2 . (len MD2) & upper_bound B = MD1 . (len MD1) & MD1 <= MD2 & MD1 = mid (D1,i,j) & MD2 = mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) ) )

set MD1 = mid (D1,i,j);
set MD2 = mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)));
assume A1: i in dom D1 ; :: thesis: ( not j in dom D1 or not i <= j or not D1 <= D2 or not r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 or ex B being non empty closed_interval Subset of REAL ex MD1, MD2 being Division of B st
( r = lower_bound B & upper_bound B = MD2 . (len MD2) & upper_bound B = MD1 . (len MD1) & MD1 <= MD2 & MD1 = mid (D1,i,j) & MD2 = mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) ) )

then A2: 1 <= i by FINSEQ_3:25;
assume A3: j in dom D1 ; :: thesis: ( not i <= j or not D1 <= D2 or not r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 or ex B being non empty closed_interval Subset of REAL ex MD1, MD2 being Division of B st
( r = lower_bound B & upper_bound B = MD2 . (len MD2) & upper_bound B = MD1 . (len MD1) & MD1 <= MD2 & MD1 = mid (D1,i,j) & MD2 = mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) ) )

assume A4: i <= j ; :: thesis: ( not D1 <= D2 or not r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 or ex B being non empty closed_interval Subset of REAL ex MD1, MD2 being Division of B st
( r = lower_bound B & upper_bound B = MD2 . (len MD2) & upper_bound B = MD1 . (len MD1) & MD1 <= MD2 & MD1 = mid (D1,i,j) & MD2 = mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) ) )

then j - i >= 0 by XREAL_1:48;
then A5: (j - i) + 1 >= 0 + 1 by XREAL_1:6;
A6: j <= len D1 by ;
then A7: (mid (D1,i,j)) . 1 = D1 . ((1 + i) - 1) by
.= D1 . i ;
assume A8: D1 <= D2 ; :: thesis: ( not r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 or ex B being non empty closed_interval Subset of REAL ex MD1, MD2 being Division of B st
( r = lower_bound B & upper_bound B = MD2 . (len MD2) & upper_bound B = MD1 . (len MD1) & MD1 <= MD2 & MD1 = mid (D1,i,j) & MD2 = mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) ) )

then A9: D2 . (indx (D2,D1,i)) = D1 . i by ;
A10: D2 . (indx (D2,D1,j)) = D1 . j by ;
A11: indx (D2,D1,i) in dom D2 by ;
then A12: 1 <= indx (D2,D1,i) by FINSEQ_3:25;
A13: indx (D2,D1,j) in dom D2 by ;
then A14: indx (D2,D1,j) <= len D2 by FINSEQ_3:25;
D1 . i <= D1 . j by ;
then A15: indx (D2,D1,i) <= indx (D2,D1,j) by ;
assume A16: r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 ; :: thesis: ex B being non empty closed_interval Subset of REAL ex MD1, MD2 being Division of B st
( r = lower_bound B & upper_bound B = MD2 . (len MD2) & upper_bound B = MD1 . (len MD1) & MD1 <= MD2 & MD1 = mid (D1,i,j) & MD2 = mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) )

then consider B being non empty closed_interval Subset of REAL such that
A17: r = lower_bound B and
A18: upper_bound B = (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . (len (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))))) and
A19: mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) is Division of B by ;
A20: len (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) = ((indx (D2,D1,j)) - (indx (D2,D1,i))) + 1 by ;
reconsider MD2 = mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) as Division of B by A19;
(indx (D2,D1,j)) - (indx (D2,D1,i)) >= 0 by ;
then A21: ((indx (D2,D1,j)) - (indx (D2,D1,i))) + 1 >= 0 + 1 by XREAL_1:6;
then A22: MD2 . (len MD2) = D2 . (((((indx (D2,D1,j)) - (indx (D2,D1,i))) + 1) - 1) + (indx (D2,D1,i))) by
.= D1 . j by ;
MD2 . 1 = D2 . ((1 + (indx (D2,D1,i))) - 1) by
.= D1 . i by ;
then consider C being non empty closed_interval Subset of REAL such that
A23: r = lower_bound C and
A24: upper_bound C = (mid (D1,i,j)) . (len (mid (D1,i,j))) and
A25: mid (D1,i,j) is Division of C by A1, A3, A4, A16, A7, Th12;
len (mid (D1,i,j)) = (j - i) + 1 by ;
then A26: (mid (D1,i,j)) . (len (mid (D1,i,j))) = D1 . ((((j - i) + 1) - 1) + i) by
.= D1 . j ;
A27: B = [.(),().] by INTEGRA1:4
.= C by ;
then reconsider MD1 = mid (D1,i,j) as Division of B by A25;
A28: rng MD1 c= rng MD2
proof
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in rng MD1 or x1 in rng MD2 )
A29: rng MD1 c= rng D1 by FINSEQ_6:119;
assume A30: x1 in rng MD1 ; :: thesis: x1 in rng MD2
then consider k1 being Element of NAT such that
A31: k1 in dom MD1 and
A32: MD1 . k1 = x1 by PARTFUN1:3;
rng D1 c= rng D2 by ;
then rng MD1 c= rng D2 by A29;
then consider k2 being Element of NAT such that
A33: k2 in dom D2 and
A34: D2 . k2 = x1 by ;
A35: k1 <= len MD1 by ;
A36: 1 <= k1 by ;
then 1 <= len MD1 by ;
then 1 in dom MD1 by FINSEQ_3:25;
then MD1 . 1 <= MD1 . k1 by ;
then A37: indx (D2,D1,i) <= k2 by ;
then consider k3 being Nat such that
A38: k2 + 1 = (indx (D2,D1,i)) + k3 by ;
len MD1 in dom MD1 by FINSEQ_5:6;
then MD1 . k1 <= MD1 . (len MD1) by ;
then k2 <= indx (D2,D1,j) by ;
then k2 + 1 <= (indx (D2,D1,j)) + 1 by XREAL_1:6;
then A39: (k2 + 1) - (indx (D2,D1,i)) <= ((indx (D2,D1,j)) + 1) - (indx (D2,D1,i)) by XREAL_1:9;
(indx (D2,D1,i)) + 1 <= k2 + 1 by ;
then A40: 1 <= (k2 + 1) - (indx (D2,D1,i)) by XREAL_1:19;
then A41: k3 in dom MD2 by ;
MD2 . k3 = D2 . ((k3 + (indx (D2,D1,i))) - 1) by ;
hence x1 in rng MD2 by ; :: thesis: verum
end;
A42: card (rng MD2) = len MD2 by FINSEQ_4:62;
card (rng MD1) = len MD1 by FINSEQ_4:62;
then len MD1 <= len MD2 by ;
then MD1 <= MD2 by ;
hence ex B being non empty closed_interval Subset of REAL ex MD1, MD2 being Division of B st
( r = lower_bound B & upper_bound B = MD2 . (len MD2) & upper_bound B = MD1 . (len MD1) & MD1 <= MD2 & MD1 = mid (D1,i,j) & MD2 = mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) ) by A17, A18, A24, A27; :: thesis: verum