theorem :: JCT_MISC:12

for e, f being Real
for A, B being compact Subset of REAL st A misses B & A c= [.e,f.] & B c= [.e,f.] holds
for S being sequence of (bool REAL) st ( for i being Nat holds
( S . i is interval & S . i meets A & S . i meets B ) ) holds
ex r being Real st
( r in [.e,f.] & not r in A \/ B & ( for i being Nat ex k being Nat st
( i <= k & r in S . k ) ) )