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