let a, b be Real_Sequence; :: thesis: ( a . 0 <= b . 0 & ( 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 not meet (IntervalSequence (a,b)) is empty )
assume that
A1: a . 0 <= b . 0 and
A2: 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: not meet (IntervalSequence (a,b)) is empty
IntervalSequence (a,b) is SetSequence of (Euclid 1) by Th17;
then A3: for i being Nat holds
( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i ) by A1, A2, Th28;
reconsider S = IntervalSequence (a,b) as non-empty pointwise_bounded closed SetSequence of (Euclid 1) by A3, Th22;
A4: S is non-ascending by A3, Th23;
lim (diameter S) = 0 by A1, A2, Th31;
then not meet S is empty by A4, COMPL_SP:10;
hence not meet (IntervalSequence (a,b)) is empty ; :: thesis: verum