theorem Th29: :: COUSIN:32

for a, b being Real_Sequence
for S being SetSequence of (Euclid 1) st a . 0 = b . 0 & S = IntervalSequence (a,b) & ( 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 holds
( a . i = a . 0 & b . i = b . 0 & (diameter S) . i = 0 )