theorem Th27: :: INTEGRA4:27

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 & f is integrable & g | 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
g is integrable