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,ExtREAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & 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,ExtREAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & 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,ExtREAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B holds
integral+ M,(f | A) <= integral+ M,(f | B)
let f be PartFunc of X,ExtREAL ; :: thesis: for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B holds
integral+ M,(f | A) <= integral+ M,(f | B)
let A, B be Element of S; :: thesis: ( ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B implies integral+ M,(f | A) <= integral+ M,(f | B) )
assume A1: ( ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B ) ; :: thesis: integral+ M,(f | A) <= integral+ M,(f | B)
set A' = A /\ B;
set B' = B \ A;
A2: ( 0 <= integral+ M,(f | ((A /\ B) \/ (B \ A))) & 0 <= integral+ M,(f | (A /\ B)) & 0 <= integral+ M,(f | (B \ A)) & integral+ M,(f | ((A /\ B) \/ (B \ A))) = (integral+ M,(f | (A /\ B))) + (integral+ M,(f | (B \ A))) ) by A1, Th86, Th87, XBOOLE_1:89;
( A /\ B = A & (A /\ B) \/ (B \ A) = B ) by A1, XBOOLE_1:28, XBOOLE_1:51;
hence integral+ M,(f | A) <= integral+ M,(f | B) by A2, XXREAL_3:42; :: thesis: verum