theorem Th14: :: MESFUN13:16

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 being b₄ -measurable PartFunc of X,ExtREAL
for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds
er * (M . (great_eq_dom (f,er))) <= Integral (M,f)