for F being FinSequence of bool REAL
for k being Nat st ( for n being Nat st n in dom F holds
F . n is open_interval Subset of REAL ) & ( for n being Nat st 1 <= n & n < len F holds
union (rng (F | n)) meets F . (n + 1) ) holds
union (rng (F | k)) is open_interval Subset of REAL