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
F vol is nonnegative

proof

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:63; :: thesis: verum

end;

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

end;

hence F vol is nonnegative ; :: thesis: verum