theorem Th7: :: INTEGRA6:7

for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st A c= dom f & f is_integrable_on A & f | A is bounded holds
( abs f is_integrable_on A & |.(integral (f,A)).| <= integral ((abs f),A) )