theorem Th34: :: INTEGRA1:36

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 holds
ex B being non empty closed_interval Subset of REAL st
( lower_bound B = (mid (D,i,j)) . 1 & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )