theorem :: MESFUN11:66

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f, g being PartFunc of X,ExtREAL st E c= dom f & E c= dom g & f is E -measurable & g is E -measurable & f is nonpositive & ( for x being Element of X st x in E holds
g . x <= f . x ) holds
Integral (M,(g | E)) <= Integral (M,(f | E))