theorem Th19: :: INTEGRA3:20

for i being Element of NAT
for A being non empty closed_interval Subset of REAL
for D being Division of A
for f being Function of A,REAL st f | A is bounded & i in dom D holds
upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f)