theorem Th56: :: MEASUR12:56

for A being non empty Subset of REAL
for F being Interval_Covering of A
for G being one-to-one FinSequence of bool REAL
for H being FinSequence of ExtREAL st rng G c= rng F & dom G = dom H & ( for n being Nat holds H . n = diameter (G . n) ) holds
Sum H <= vol F