let a, b be Real_Sequence; :: thesis: 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) )
let S be SetSequence of (Euclid 1); :: thesis: ( 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 ) ) ) implies 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) ) )
assume that
A1: a . 0 <= b . 0 and
A2: S = IntervalSequence (a,b) and
A3: 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 ) ) ; :: thesis: 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) )
A4: for i being Nat holds
( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i )

proof

let i be Nat; :: thesis: ( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i )
thus A6: a . i <= b . i by Th27, A1, A3; :: thesis: ( a . i <= a . (i + 1) & b . (i + 1) <= b . i )
thus a . i <= a . (i + 1) :: thesis: b . (i + 1) <= b . i

proof

( a . (i + 1) = a . i or a . (i + 1) = ((a . i) + (b . i)) / 2 ) by A3;
hence a . i <= a . (i + 1) by A6, Th8; :: thesis: verum

end;

thus b . (i + 1) <= b . i :: thesis: verum

proof

( b . (i + 1) = b . i or b . (i + 1) = ((a . i) + (b . i)) / 2 ) by A3;
hence b . (i + 1) <= b . i by A6, Th8; :: thesis: verum

end;

end;

now :: thesis: for i being Nat holds (diameter S) . i = (b . i) - (a . i)

let i be Nat; :: thesis: (diameter S) . i = (b . i) - (a . i)
A7: IntervalSequence (a,b) is SetSequence of (Euclid 1) by Th17;
reconsider IntervalSequence1 = (IntervalSequence (a,b)) . i as Subset of (Euclid 1) by ORDINAL1:def 12, A7, FUNCT_2:5;
S . i = product <*[.(a . i),(b . i).]*> by A2, Def1;
then reconsider IntervalSequence2 = product <*[.(a . i),(b . i).]*> as Subset of (Euclid 1) ;
diameter (S . i) = diameter IntervalSequence2 by A2, Def1
.= (b . i) - (a . i) by A4, Th25 ;
hence (diameter S) . i = (b . i) - (a . i) by COMPL_SP:def 2; :: thesis: verum

end;

hence 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) ) by A4; :: thesis: verum