let X be set ; :: thesis: for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X
for n being natural number
for Cvr being Covering of Sets,F holds 0 <= (Volume M,Cvr) . n
let F be Field_Subset of X; :: thesis: for M being Measure of F
for Sets being SetSequence of X
for n being natural number
for Cvr being Covering of Sets,F holds 0 <= (Volume M,Cvr) . n
let M be Measure of F; :: thesis: for Sets being SetSequence of X
for n being natural number
for Cvr being Covering of Sets,F holds 0 <= (Volume M,Cvr) . n
let Sets be SetSequence of X; :: thesis: for n being natural number
for Cvr being Covering of Sets,F holds 0 <= (Volume M,Cvr) . n
let n be natural number ; :: thesis: for Cvr being Covering of Sets,F holds 0 <= (Volume M,Cvr) . n
let Cvr be Covering of Sets,F; :: thesis: 0 <= (Volume M,Cvr) . n
A1: (Volume M,Cvr) . n = SUM (vol M,(Cvr . n)) by Def7;
for k being Element of NAT holds 0 <= (vol M,(Cvr . n)) . k

proof

let k be Element of NAT ; :: thesis: 0 <= (vol M,(Cvr . n)) . k
0 <= M . ((Cvr . n) . k) by SUPINF_2:70;
hence 0 <= (vol M,(Cvr . n)) . k by Def4; :: thesis: verum

end;

then vol M,(Cvr . n) is nonnegative by SUPINF_2:58;
hence 0 <= (Volume M,Cvr) . n by A1, MEASURE6:2; :: thesis: verum