theorem Th8: :: INTEGRA6:8

for a, b being Real
for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds
|.(integral (f,a,b)).| <= integral ((abs f),a,b)