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
proof
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;
now :: thesis: for p being ExtReal st p in Svc (M,A) holds
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;
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 ExtReal st r in rng (C_Meas M) holds
0 <= r ;
then rng (C_Meas M) is nonnegative ;
hence C_Meas M is nonnegative ; :: thesis: verum