theorem Th1: :: RANDOM_1:1

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
a <= f . x ) holds
a * (M . E) <= Integral (M,(f | E))