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 E -measurable holds
( Integral (M,(max- f)) = 0 & integral+ (M,(max- f)) = 0 )