theorem Th28: :: COUSIN:31

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 <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i & (diameter S) . i = (b . i) - (a . i) )