theorem :: MESFUN11:53

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being nonnegative PartFunc of X,ExtREAL
for E being Element of S st E = dom f & f is_measurable_on E holds
( Integral (M,(max- f)) = 0 & integral+ (M,(max- f)) = 0 )