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
( (vol (M,FSets)) . n = M . (FSets . n) & {} in F ) by Def5, PROB_1:4;
then M . {} <= (vol (M,FSets)) . n by MEASURE1:8, XBOOLE_1:2;
hence 0 <= (vol (M,FSets)) . n by VALUED_0:def 19; :: thesis: verum
end;
hence vol (M,FSets) is nonnegative by SUPINF_2:39; :: thesis: verum