theorem Th25: :: INTEGRA4:25

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