let i be Element of NAT ; :: thesis: for f being FinSequence of the carrier of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & f /. (i + 1) in LSeg (p,q) & LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & not f /. (i + 1) = p holds
f /. (i + 1) = q
let f be FinSequence of the carrier of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & f /. (i + 1) in LSeg (p,q) & LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & not f /. (i + 1) = p holds
f /. (i + 1) = q
let p, q be Point of (TOP-REAL 2); :: thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f & f /. (i + 1) in LSeg (p,q) & LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & not f /. (i + 1) = p implies f /. (i + 1) = q )
assume that
A1: ( f is special & f is alternating ) and
A2: 1 <= i and
A3: i + 2 <= len f ; :: thesis: ( not f /. (i + 1) in LSeg (p,q) or not LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) or f /. (i + 1) = p or f /. (i + 1) = q )
i + 1 <= i + 2 by XREAL_1:6;
then A4: i + 1 <= len f by A3, XXREAL_0:2;
set p1 = f /. i;
set p0 = f /. (i + 1);
set p2 = f /. (i + 2);
A5: ( i + (1 + 1) = (i + 1) + 1 & 1 <= i + 1 ) by NAT_1:11;
assume that
A6: f /. (i + 1) in LSeg (p,q) and
A7: LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )
A8: ( p in LSeg (p,q) & q in LSeg (p,q) ) by RLTOPSP1:68;

now

per cases ( ( p in LSeg (f,i) & q in LSeg (f,i) ) or ( p in LSeg (f,i) & q in LSeg (f,(i + 1)) ) or ( p in LSeg (f,(i + 1)) & q in LSeg (f,i) ) or ( p in LSeg (f,(i + 1)) & q in LSeg (f,(i + 1)) ) ) by A7, A8, XBOOLE_0:def 3;

case ( p in LSeg (f,i) & q in LSeg (f,i) ) ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then ( p in LSeg ((f /. i),(f /. (i + 1))) & q in LSeg ((f /. i),(f /. (i + 1))) ) by A2, A4, TOPREAL1:def 3;
then A9: LSeg (p,q) c= LSeg ((f /. i),(f /. (i + 1))) by TOPREAL1:6;
f /. (i + 1) is_extremal_in LSeg ((f /. i),(f /. (i + 1))) by Th32;
hence ( f /. (i + 1) = p or f /. (i + 1) = q ) by A6, A9, Def1; :: thesis: verum

end;

case A10: ( p in LSeg (f,i) & q in LSeg (f,(i + 1)) ) ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then p in LSeg ((f /. i),(f /. (i + 1))) by A2, A4, TOPREAL1:def 3;
then consider s being Real such that
A11: p = ((1 - s) * (f /. i)) + (s * (f /. (i + 1))) and
0 <= s and
s <= 1 ;
A12: p `1 = (((1 - s) * (f /. i)) `1) + ((s * (f /. (i + 1))) `1) by A11, TOPREAL3:2
.= ((1 - s) * ((f /. i) `1)) + ((s * (f /. (i + 1))) `1) by TOPREAL3:4
.= ((1 - s) * ((f /. i) `1)) + (s * ((f /. (i + 1)) `1)) by TOPREAL3:4 ;
q in LSeg ((f /. (i + 1)),(f /. (i + 2))) by A3, A5, A10, TOPREAL1:def 3;
then consider s1 being Real such that
A13: q = ((1 - s1) * (f /. (i + 1))) + (s1 * (f /. (i + 2))) and
0 <= s1 and
s1 <= 1 ;
A14: q `2 = (((1 - s1) * (f /. (i + 1))) `2) + ((s1 * (f /. (i + 2))) `2) by A13, TOPREAL3:2
.= ((1 - s1) * ((f /. (i + 1)) `2)) + ((s1 * (f /. (i + 2))) `2) by TOPREAL3:4
.= ((1 - s1) * ((f /. (i + 1)) `2)) + (s1 * ((f /. (i + 2)) `2)) by TOPREAL3:4 ;
A15: p `2 = (((1 - s) * (f /. i)) `2) + ((s * (f /. (i + 1))) `2) by A11, TOPREAL3:2
.= ((1 - s) * ((f /. i) `2)) + ((s * (f /. (i + 1))) `2) by TOPREAL3:4
.= ((1 - s) * ((f /. i) `2)) + (s * ((f /. (i + 1)) `2)) by TOPREAL3:4 ;
A16: q `1 = (((1 - s1) * (f /. (i + 1))) `1) + ((s1 * (f /. (i + 2))) `1) by A13, TOPREAL3:2
.= ((1 - s1) * ((f /. (i + 1)) `1)) + ((s1 * (f /. (i + 2))) `1) by TOPREAL3:4
.= ((1 - s1) * ((f /. (i + 1)) `1)) + (s1 * ((f /. (i + 2)) `1)) by TOPREAL3:4 ;

now

A17: ( f /. (i + 2) = f /. (i + 2) & f /. i = f /. i ) ;

per cases ( ( (f /. i) `1 = (f /. (i + 1)) `1 & (f /. (i + 2)) `1 <> (f /. (i + 1)) `1 ) or ( (f /. i) `2 = (f /. (i + 1)) `2 & (f /. (i + 2)) `2 <> (f /. (i + 1)) `2 ) ) by A1, A2, A3, A17, Th52;

case A18: ( (f /. i) `1 = (f /. (i + 1)) `1 & (f /. (i + 2)) `1 <> (f /. (i + 1)) `1 ) ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

consider r being Real such that
A19: f /. (i + 1) = ((1 - r) * p) + (r * q) and
0 <= r and
r <= 1 by A6;
(f /. (i + 1)) `1 = (((1 - r) * p) `1) + ((r * q) `1) by A19, TOPREAL3:2
.= ((1 - r) * (p `1)) + ((r * q) `1) by TOPREAL3:4
.= ((1 - r) * ((f /. (i + 1)) `1)) + (r * (q `1)) by A12, A18, TOPREAL3:4 ;
then r * (((f /. (i + 1)) `1) - (q `1)) = 0 ;
then A20: ( r = 0 or ((f /. (i + 1)) `1) - (q `1) = 0 ) by XCMPLX_1:6;

now

per cases ( r = 0 or (f /. (i + 1)) `1 = q `1 ) by A20;

case r = 0 ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then f /. (i + 1) = ((1 - 0) * p) + (0. (TOP-REAL 2)) by A19, EUCLID:29
.= 1 * p by EUCLID:27
.= p by EUCLID:29 ;
hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

case (f /. (i + 1)) `1 = q `1 ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then s1 * (((f /. (i + 1)) `1) - ((f /. (i + 2)) `1)) = 0 by A16;
then A21: ( s1 = 0 or ((f /. (i + 1)) `1) - ((f /. (i + 2)) `1) = 0 ) by XCMPLX_1:6;

now

per cases ( s1 = 0 or (f /. (i + 1)) `1 = (f /. (i + 2)) `1 ) by A21;

case s1 = 0 ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then q = ((1 - 0) * (f /. (i + 1))) + (0. (TOP-REAL 2)) by A13, EUCLID:29
.= 1 * (f /. (i + 1)) by EUCLID:27
.= f /. (i + 1) by EUCLID:29 ;
hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

case (f /. (i + 1)) `1 = (f /. (i + 2)) `1 ; :: thesis: contradiction

hence contradiction by A18; :: thesis: verum

end;

end;

end;

hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

end;

end;

hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

case A22: ( (f /. i) `2 = (f /. (i + 1)) `2 & (f /. (i + 2)) `2 <> (f /. (i + 1)) `2 ) ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

consider r being Real such that
A23: f /. (i + 1) = ((1 - r) * p) + (r * q) and
0 <= r and
r <= 1 by A6;
(f /. (i + 1)) `2 = (((1 - r) * p) `2) + ((r * q) `2) by A23, TOPREAL3:2
.= ((1 - r) * (p `2)) + ((r * q) `2) by TOPREAL3:4
.= ((1 - r) * ((f /. (i + 1)) `2)) + (r * (q `2)) by A15, A22, TOPREAL3:4 ;
then r * (((f /. (i + 1)) `2) - (q `2)) = 0 ;
then A24: ( r = 0 or ((f /. (i + 1)) `2) - (q `2) = 0 ) by XCMPLX_1:6;

now

per cases ( r = 0 or (f /. (i + 1)) `2 = q `2 ) by A24;

case r = 0 ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then f /. (i + 1) = ((1 - 0) * p) + (0. (TOP-REAL 2)) by A23, EUCLID:29
.= 1 * p by EUCLID:27
.= p by EUCLID:29 ;
hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

case (f /. (i + 1)) `2 = q `2 ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then s1 * (((f /. (i + 1)) `2) - ((f /. (i + 2)) `2)) = 0 by A14;
then A25: ( s1 = 0 or ((f /. (i + 1)) `2) - ((f /. (i + 2)) `2) = 0 ) by XCMPLX_1:6;

now

per cases ( s1 = 0 or (f /. (i + 1)) `2 = (f /. (i + 2)) `2 ) by A25;

case s1 = 0 ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then q = ((1 - 0) * (f /. (i + 1))) + (0. (TOP-REAL 2)) by A13, EUCLID:29
.= 1 * (f /. (i + 1)) by EUCLID:27
.= f /. (i + 1) by EUCLID:29 ;
hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

case (f /. (i + 1)) `2 = (f /. (i + 2)) `2 ; :: thesis: contradiction

hence contradiction by A22; :: thesis: verum

end;

end;

end;

hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

end;

end;

hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

end;

end;

hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

case A26: ( p in LSeg (f,(i + 1)) & q in LSeg (f,i) ) ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then q in LSeg ((f /. i),(f /. (i + 1))) by A2, A4, TOPREAL1:def 3;
then consider s being Real such that
A27: q = ((1 - s) * (f /. i)) + (s * (f /. (i + 1))) and
0 <= s and
s <= 1 ;
A28: q `1 = (((1 - s) * (f /. i)) `1) + ((s * (f /. (i + 1))) `1) by A27, TOPREAL3:2
.= ((1 - s) * ((f /. i) `1)) + ((s * (f /. (i + 1))) `1) by TOPREAL3:4
.= ((1 - s) * ((f /. i) `1)) + (s * ((f /. (i + 1)) `1)) by TOPREAL3:4 ;
p in LSeg ((f /. (i + 1)),(f /. (i + 2))) by A3, A5, A26, TOPREAL1:def 3;
then consider s1 being Real such that
A29: p = ((1 - s1) * (f /. (i + 1))) + (s1 * (f /. (i + 2))) and
0 <= s1 and
s1 <= 1 ;
A30: p `2 = (((1 - s1) * (f /. (i + 1))) `2) + ((s1 * (f /. (i + 2))) `2) by A29, TOPREAL3:2
.= ((1 - s1) * ((f /. (i + 1)) `2)) + ((s1 * (f /. (i + 2))) `2) by TOPREAL3:4
.= ((1 - s1) * ((f /. (i + 1)) `2)) + (s1 * ((f /. (i + 2)) `2)) by TOPREAL3:4 ;
A31: q `2 = (((1 - s) * (f /. i)) `2) + ((s * (f /. (i + 1))) `2) by A27, TOPREAL3:2
.= ((1 - s) * ((f /. i) `2)) + ((s * (f /. (i + 1))) `2) by TOPREAL3:4
.= ((1 - s) * ((f /. i) `2)) + (s * ((f /. (i + 1)) `2)) by TOPREAL3:4 ;
A32: p `1 = (((1 - s1) * (f /. (i + 1))) `1) + ((s1 * (f /. (i + 2))) `1) by A29, TOPREAL3:2
.= ((1 - s1) * ((f /. (i + 1)) `1)) + ((s1 * (f /. (i + 2))) `1) by TOPREAL3:4
.= ((1 - s1) * ((f /. (i + 1)) `1)) + (s1 * ((f /. (i + 2)) `1)) by TOPREAL3:4 ;

now

A33: ( f /. (i + 2) = f /. (i + 2) & f /. i = f /. i ) ;

per cases ( ( (f /. i) `1 = (f /. (i + 1)) `1 & (f /. (i + 2)) `1 <> (f /. (i + 1)) `1 ) or ( (f /. i) `2 = (f /. (i + 1)) `2 & (f /. (i + 2)) `2 <> (f /. (i + 1)) `2 ) ) by A1, A2, A3, A33, Th52;

case A34: ( (f /. i) `1 = (f /. (i + 1)) `1 & (f /. (i + 2)) `1 <> (f /. (i + 1)) `1 ) ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

f /. (i + 1) in LSeg (q,p) by A6;
then consider r being Real such that
A35: f /. (i + 1) = ((1 - r) * q) + (r * p) and
0 <= r and
r <= 1 ;
(f /. (i + 1)) `1 = (((1 - r) * q) `1) + ((r * p) `1) by A35, TOPREAL3:2
.= ((1 - r) * (q `1)) + ((r * p) `1) by TOPREAL3:4
.= ((1 - r) * ((f /. (i + 1)) `1)) + (r * (p `1)) by A28, A34, TOPREAL3:4 ;
then r * (((f /. (i + 1)) `1) - (p `1)) = 0 ;
then A36: ( r = 0 or ((f /. (i + 1)) `1) - (p `1) = 0 ) by XCMPLX_1:6;

now

per cases ( r = 0 or (f /. (i + 1)) `1 = p `1 ) by A36;

case r = 0 ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then f /. (i + 1) = ((1 - 0) * q) + (0. (TOP-REAL 2)) by A35, EUCLID:29
.= 1 * q by EUCLID:27
.= q by EUCLID:29 ;
hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

case (f /. (i + 1)) `1 = p `1 ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then s1 * (((f /. (i + 1)) `1) - ((f /. (i + 2)) `1)) = 0 by A32;
then A37: ( s1 = 0 or ((f /. (i + 1)) `1) - ((f /. (i + 2)) `1) = 0 ) by XCMPLX_1:6;

now

per cases ( s1 = 0 or (f /. (i + 1)) `1 = (f /. (i + 2)) `1 ) by A37;

case s1 = 0 ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then p = ((1 - 0) * (f /. (i + 1))) + (0. (TOP-REAL 2)) by A29, EUCLID:29
.= 1 * (f /. (i + 1)) by EUCLID:27
.= f /. (i + 1) by EUCLID:29 ;
hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

case (f /. (i + 1)) `1 = (f /. (i + 2)) `1 ; :: thesis: contradiction

hence contradiction by A34; :: thesis: verum

end;

end;

end;

hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

end;

end;

hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

case A38: ( (f /. i) `2 = (f /. (i + 1)) `2 & (f /. (i + 2)) `2 <> (f /. (i + 1)) `2 ) ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

f /. (i + 1) in LSeg (q,p) by A6;
then consider r being Real such that
A39: f /. (i + 1) = ((1 - r) * q) + (r * p) and
0 <= r and
r <= 1 ;
(f /. (i + 1)) `2 = (((1 - r) * q) `2) + ((r * p) `2) by A39, TOPREAL3:2
.= ((1 - r) * (q `2)) + ((r * p) `2) by TOPREAL3:4
.= ((1 - r) * ((f /. (i + 1)) `2)) + (r * (p `2)) by A31, A38, TOPREAL3:4 ;
then r * (((f /. (i + 1)) `2) - (p `2)) = 0 ;
then A40: ( r = 0 or ((f /. (i + 1)) `2) - (p `2) = 0 ) by XCMPLX_1:6;

now

per cases ( r = 0 or (f /. (i + 1)) `2 = p `2 ) by A40;

case r = 0 ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then f /. (i + 1) = ((1 - 0) * q) + (0. (TOP-REAL 2)) by A39, EUCLID:29
.= 1 * q by EUCLID:27
.= q by EUCLID:29 ;
hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

case (f /. (i + 1)) `2 = p `2 ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then s1 * (((f /. (i + 1)) `2) - ((f /. (i + 2)) `2)) = 0 by A30;
then A41: ( s1 = 0 or ((f /. (i + 1)) `2) - ((f /. (i + 2)) `2) = 0 ) by XCMPLX_1:6;

now

per cases ( s1 = 0 or (f /. (i + 1)) `2 = (f /. (i + 2)) `2 ) by A41;

case s1 = 0 ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then p = ((1 - 0) * (f /. (i + 1))) + (0. (TOP-REAL 2)) by A29, EUCLID:29
.= 1 * (f /. (i + 1)) by EUCLID:27
.= f /. (i + 1) by EUCLID:29 ;
hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

case (f /. (i + 1)) `2 = (f /. (i + 2)) `2 ; :: thesis: contradiction

hence contradiction by A38; :: thesis: verum

end;

end;

end;

hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

end;

end;

hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

end;

end;

hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum

end;

case ( p in LSeg (f,(i + 1)) & q in LSeg (f,(i + 1)) ) ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )

then ( p in LSeg ((f /. (i + 1)),(f /. (i + 2))) & q in LSeg ((f /. (i + 1)),(f /. (i + 2))) ) by A3, A5, TOPREAL1:def 3;
then A42: LSeg (p,q) c= LSeg ((f /. (i + 1)),(f /. (i + 2))) by TOPREAL1:6;
f /. (i + 1) is_extremal_in LSeg ((f /. (i + 1)),(f /. (i + 2))) by Th32;
hence ( f /. (i + 1) = p or f /. (i + 1) = q ) by A6, A42, Def1; :: thesis: verum

end;

end;

end;

hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; :: thesis: verum