theorem Th34: :: MEASUR12:34

for H being sequence of [:NAT,NAT:] st H is one-to-one & rng H = [:NAT,NAT:] holds
for k being Nat ex m being Element of NAT st
for F being sequence of (bool REAL)
for G being Open_Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m