let A be Subset of REAL; :: thesis: for F being Interval_Covering of A holds F vol is nonnegative
let F be Interval_Covering of A; :: thesis: F vol is nonnegative
for n being Element of NAT holds 0. <= (F vol) . n

proof

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

end;

hence F vol is nonnegative by SUPINF_2:39; :: thesis: verum