let F be sequence of (bool REAL); :: thesis: for G being Interval_Covering of F
for n being Element of NAT holds 0. <= (vol G) . n
let G be Interval_Covering of F; :: thesis: for n being Element of NAT holds 0. <= (vol G) . n
let n be Element of NAT ; :: thesis: 0. <= (vol G) . n
for k being Element of NAT holds 0. <= ((G . n) vol) . k

proof

let k be Element of NAT ; :: thesis: 0. <= ((G . n) vol) . k
0. <= diameter ((G . n) . k) by MEASURE5:13;
hence 0. <= ((G . n) vol) . k by Def4; :: thesis: verum

end;

then A1: (G . n) vol is nonnegative by SUPINF_2:39;
(vol G) . n = vol (G . n) by Def7;
hence 0. <= (vol G) . n by A1, MEASURE6:2; :: thesis: verum