theorem Th12: :: MEASURE7:12

for A being Subset of REAL
for F being Interval_Covering of A holds F vol is nonnegative