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
( diameter S is convergent & lim (diameter S) = 0 )