theorem Th3: :: RANDOM_1:3

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S
for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
f . x <= a ) holds
Integral (M,(f | E)) <= a * (M . E)