theorem Th12: :: INTEGRA3:12

for r being Real
for i, j being Element of NAT
for A being non empty 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 non empty 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 )