theorem Th55: :: LPSPACE1:55

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g)))