theorem Th15: :: MEASURE7:15

for F being sequence of (bool REAL)
for G being Interval_Covering of F holds inf (Svc (union (rng F))) <= SUM (vol G)