let X be set ; :: thesis: for F being Field_Subset of X
for M being Measure of F
for FSets being Set_Sequence of F holds vol M,FSets is nonnegative
let F be Field_Subset of X; :: thesis: for M being Measure of F
for FSets being Set_Sequence of F holds vol M,FSets is nonnegative
let M be Measure of F; :: thesis: for FSets being Set_Sequence of F holds vol M,FSets is nonnegative
let FSets be Set_Sequence of F; :: thesis: vol M,FSets is nonnegative
for n being Element of NAT holds 0 <= (vol M,FSets) . n

proof

let n be Element of NAT ; :: thesis: 0 <= (vol M,FSets) . n
A1: (vol M,FSets) . n = M . (FSets . n) by Def4;
( {} c= FSets . n & {} in F ) by XBOOLE_1:2, PROB_1:10;
then M . {} <= (vol M,FSets) . n by A1, MEASURE1:25;
hence 0 <= (vol M,FSets) . n by VALUED_0:def 19; :: thesis: verum

end;

hence vol M,FSets is nonnegative by SUPINF_2:58; :: thesis: verum