theorem Th13: :: MEASURE7:13

for F being sequence of (bool REAL)
for G being Interval_Covering of F
for n being Element of NAT holds 0. <= (vol G) . n