theorem Th15: :: INTEGRA3:16

for r being Real
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))) )