let X be non empty set ; :: thesis: 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))

let S be SigmaField of X; :: thesis: 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))

let M be sigma_Measure of S; :: thesis: 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))

let E be Element of S; :: thesis: 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))

let f, g be PartFunc of X,ExtREAL; :: thesis: ( 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 ) implies Integral (M,(g | E)) <= Integral (M,(f | E)) )

assume that
A1: E c= dom f and
A2: E c= dom g and
A3: ( f is E -measurable & g is E -measurable ) and
A4: f is nonpositive and
A5: for x being Element of X st x in E holds
g . x <= f . x ; :: thesis: Integral (M,(g | E)) <= Integral (M,(f | E))
set f1 = - f;
set g1 = - g;
A6: ( E c= dom (- f) & E c= dom (- g) ) by ;
A7: ( - f is E -measurable & - g is E -measurable ) by ;
A11: for x being Element of X st x in E holds
(- f) . x <= (- g) . x
proof
let x be Element of X; :: thesis: ( x in E implies (- f) . x <= (- g) . x )
assume A9: x in E ; :: thesis: (- f) . x <= (- g) . x
then ( (- f) . x = - (f . x) & (- g) . x = - (g . x) ) by ;
hence (- f) . x <= (- g) . x by ; :: thesis: verum
end;
A12: ( (dom f) /\ E = E & (dom g) /\ E = E ) by ;
A14: ( E = dom (f | E) & E = dom (g | E) ) by ;
( (- f) | E = - (f | E) & (- g) | E = - (g | E) ) by Th3;
then ( Integral (M,((- f) | E)) = - (Integral (M,(f | E))) & Integral (M,((- g) | E)) = - (Integral (M,(g | E))) ) by ;
hence Integral (M,(g | E)) <= Integral (M,(f | E)) by ; :: thesis: verum