let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A c= B holds
Integral (M,(f | A)) >= Integral (M,(f | B))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A c= B holds
Integral (M,(f | A)) >= Integral (M,(f | B))
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL
for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A c= B holds
Integral (M,(f | A)) >= Integral (M,(f | B))
let f be PartFunc of X,REAL; :: thesis: for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A c= B holds
Integral (M,(f | A)) >= Integral (M,(f | B))
let A, B, E be Element of S; :: thesis: ( E = dom f & f is E -measurable & f is nonpositive & A c= B implies Integral (M,(f | A)) >= Integral (M,(f | B)) )
assume that
A1: E = dom f and
A2: f is E -measurable and
A3: f is nonpositive and
A4: A c= B ; :: thesis: Integral (M,(f | A)) >= Integral (M,(f | B))
A5: E = dom (R_EAL f) by A1, MESFUNC5:def 7;
A6: R_EAL f is E -measurable by A2, MESFUNC6:def 1;
for x being set st x in dom (R_EAL f) holds
(R_EAL f) . x <= 0

proof

let x be set ; :: thesis: ( x in dom (R_EAL f) implies (R_EAL f) . x <= 0 )
assume x in dom (R_EAL f) ; :: thesis: (R_EAL f) . x <= 0
f . x <= 0 by A3, MESFUNC6:53;
hence (R_EAL f) . x <= 0 by MESFUNC5:def 7; :: thesis: verum

end;

then Integral (M,((R_EAL f) | A)) >= Integral (M,((R_EAL f) | B)) by A5, A6, A4, MESFUNC5:9, MESFUN11:64;
then Integral (M,(R_EAL (f | A))) >= Integral (M,((R_EAL f) | B)) by Th16;
then Integral (M,(R_EAL (f | A))) >= Integral (M,(R_EAL (f | B))) by Th16;
then Integral (M,(f | A)) >= Integral (M,(R_EAL (f | B))) by MESFUNC6:def 3;
hence Integral (M,(f | A)) >= Integral (M,(f | B)) by MESFUNC6:def 3; :: thesis: verum