theorem :: COUSIN:36

for r being Real
for a, b being Real_Sequence st 0 < r & a . 0 <= b . 0 & ( for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) ) ) holds
ex c being Real st
( ( for j being Nat holds
( a . j <= c & c <= b . j ) ) & ex k being Nat st
( c - r < a . k & b . k < c + r ) )