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 st rng G c= rng F holds
ex F1 being Interval_Covering of A st
( ( for n being Nat st n in dom G holds
G . n = F1 . n ) & vol F1 = vol F )