let X be set ; :: thesis: for F being Field_Subset of X

for M being Measure of F holds C_Meas M is nonnegative

let F be Field_Subset of X; :: thesis: for M being Measure of F holds C_Meas M is nonnegative

let M be Measure of F; :: thesis: C_Meas M is nonnegative

for r being ExtReal st r in rng (C_Meas M) holds

0 <= r

0 <= r ;

then rng (C_Meas M) is nonnegative ;

hence C_Meas M is nonnegative ; :: thesis: verum

for M being Measure of F holds C_Meas M is nonnegative

let F be Field_Subset of X; :: thesis: for M being Measure of F holds C_Meas M is nonnegative

let M be Measure of F; :: thesis: C_Meas M is nonnegative

for r being ExtReal st r in rng (C_Meas M) holds

0 <= r

proof

then
for r being ExtReal st r in rng (C_Meas M) holds
let r be ExtReal; :: thesis: ( r in rng (C_Meas M) implies 0 <= r )

assume r in rng (C_Meas M) ; :: thesis: 0 <= r

then consider A being object such that

A1: A in bool X and

A2: (C_Meas M) . A = r by FUNCT_2:11;

reconsider A = A as Subset of X by A1;

then 0 <= inf (Svc (M,A)) by XXREAL_2:def 4;

hence 0 <= r by A2, Def8; :: thesis: verum

end;assume r in rng (C_Meas M) ; :: thesis: 0 <= r

then consider A being object such that

A1: A in bool X and

A2: (C_Meas M) . A = r by FUNCT_2:11;

reconsider A = A as Subset of X by A1;

now :: thesis: for p being ExtReal st p in Svc (M,A) holds

0 <= p

then
0 is LowerBound of Svc (M,A)
by XXREAL_2:def 2;0 <= p

let p be ExtReal; :: thesis: ( p in Svc (M,A) implies 0 <= p )

assume p in Svc (M,A) ; :: thesis: 0 <= p

then ex G being Covering of A,F st p = SUM (vol (M,G)) by Def7;

hence 0 <= p by Th4, MEASURE6:2; :: thesis: verum

end;assume p in Svc (M,A) ; :: thesis: 0 <= p

then ex G being Covering of A,F st p = SUM (vol (M,G)) by Def7;

hence 0 <= p by Th4, MEASURE6:2; :: thesis: verum

then 0 <= inf (Svc (M,A)) by XXREAL_2:def 4;

hence 0 <= r by A2, Def8; :: thesis: verum

0 <= r ;

then rng (C_Meas M) is nonnegative ;

hence C_Meas M is nonnegative ; :: thesis: verum