let A be Subset of REAL; :: thesis: for F being Interval_Covering of A holds F vol is V99()
let F be Interval_Covering of A; :: thesis: F vol is V99()
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 V99() by SUPINF_2:39; :: thesis: verum