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 and
A2: (C_Meas M) . A = r by FUNCT_2:11;
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 Def7;
hence 0 <= p by Th4, 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 A2, Def8; :: 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 9;
hence C_Meas M is nonnegative by SUPINF_2:def 16; :: thesis: verum