theorem Th41: :: MEASUR12:41

for A being non empty closed_interval Subset of REAL
for F being FinSequence of bool REAL st A c= union (rng F) & ( for n being Nat st n in dom F holds
A meets F . n ) & ( for n being Nat st n in dom F holds
F . n is open_interval Subset of REAL ) holds
ex G being FinSequence of bool REAL st
( F,G are_fiberwise_equipotent & ( for n being Nat st 1 <= n & n < len G holds
union (rng (G | n)) meets G . (n + 1) ) )