theorem Th24: :: INTEGRA4:24

for a being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st ( for x, y being Real st x in A & y in A holds
|.((f . x) - (f . y)).| <= a ) holds
(upper_bound (rng f)) - (lower_bound (rng f)) <= a