theorem Th16: :: INTEGRA3:17

for x being Real
for A being non empty closed_interval Subset of REAL
for D being Division of A st x in rng D holds
( D . 1 <= x & x <= D . (len D) )