theorem Th30: :: COUSIN:33

for a, b being Real_Sequence st ( 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
for i being Nat
for r being Real st r = 2 |^ i & r <> 0 holds
(b . i) - (a . i) <= ((b . 0) - (a . 0)) / r