theorem Th11: :: INTEGRA3:11

for x being Real
for A being non empty closed_interval Subset of REAL
for D1, D2 being Division of A
for g being Function of A,REAL st x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded holds
(Sum (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)