theorem Th20: :: INTEGR19:20

for A being non empty closed_interval Subset of REAL
for n being non zero Element of NAT
for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded & h is_integrable_on A & |.h.| is_integrable_on A holds
|.(integral (h,A)).| <= integral (|.h.|,A)