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 ext-real number st r in rng (C_Meas M) holds
0 <= r

proof

let r be ext-real number ; :: thesis: ( r in rng (C_Meas M) implies 0 <= r )
assume r in rng (C_Meas M) ; :: thesis: 0 <= r
then consider A being set such that
A1: ( A in bool X & (C_Meas M) . A = r ) by FUNCT_2:17;
reconsider A = A as Subset of X by A1;

now

let p be ext-real number ; :: 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 Def8;
hence 0 <= p by Th13, MEASURE6:2; :: thesis: verum

end;

then 0 is LowerBound of Svc M,A by XXREAL_2:def 2;
then 0 <= inf (Svc M,A) by XXREAL_2:def 4;
hence 0 <= r by A1, Def10; :: thesis: verum

end;

then for r being R_eal st r in rng (C_Meas M) holds
0 <= r ;
then rng (C_Meas M) is nonnegative by SUPINF_2:def 15;
hence C_Meas M is nonnegative by SUPINF_2:def 22; :: thesis: verum