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 and
A2: f is alternating and
A3: 1 <= i and
A4: 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 )
A5: i + (1 + 1) = (i + 1) + 1 ;
i + 1 <= i + 2 by XREAL_1:8;
then A6: i + 1 <= len f by A4, XXREAL_0:2;
A7: 1 <= i + 1 by NAT_1:11;
set p1 = f /. i;
set p0 = f /. (i + 1);
set p2 = f /. (i + 2);
assume A8: ( f /. (i + 1) in LSeg p,q & LSeg p,q c= (LSeg f,i) \/ (LSeg f,(i + 1)) ) ; :: thesis: ( f /. (i + 1) = p or f /. (i + 1) = q )
A9: ( p in LSeg p,q & q in LSeg p,q ) by RLTOPSP1:69;

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 A8, A9, 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 A3, A6, TOPREAL1:def 5;
then A10: LSeg p,q c= LSeg (f /. i),(f /. (i + 1)) by TOPREAL1:12;
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 A8, A10, Def1; :: thesis: verum

end;

case A11: ( 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 A3, A6, TOPREAL1:def 5;
then consider s being Real such that
A12: p = ((1 - s) * (f /. i)) + (s * (f /. (i + 1))) and
( 0 <= s & s <= 1 ) ;
A13: p `1 = (((1 - s) * (f /. i)) `1 ) + ((s * (f /. (i + 1))) `1 ) by A12, TOPREAL3:7
.= ((1 - s) * ((f /. i) `1 )) + ((s * (f /. (i + 1))) `1 ) by TOPREAL3:9
.= ((1 - s) * ((f /. i) `1 )) + (s * ((f /. (i + 1)) `1 )) by TOPREAL3:9 ;
A14: p `2 = (((1 - s) * (f /. i)) `2 ) + ((s * (f /. (i + 1))) `2 ) by A12, TOPREAL3:7
.= ((1 - s) * ((f /. i) `2 )) + ((s * (f /. (i + 1))) `2 ) by TOPREAL3:9
.= ((1 - s) * ((f /. i) `2 )) + (s * ((f /. (i + 1)) `2 )) by TOPREAL3:9 ;
q in LSeg (f /. (i + 1)),(f /. (i + 2)) by A4, A5, A7, A11, TOPREAL1:def 5;
then consider s1 being Real such that
A15: q = ((1 - s1) * (f /. (i + 1))) + (s1 * (f /. (i + 2))) and
( 0 <= s1 & s1 <= 1 ) ;
A16: q `1 = (((1 - s1) * (f /. (i + 1))) `1 ) + ((s1 * (f /. (i + 2))) `1 ) by A15, TOPREAL3:7
.= ((1 - s1) * ((f /. (i + 1)) `1 )) + ((s1 * (f /. (i + 2))) `1 ) by TOPREAL3:9
.= ((1 - s1) * ((f /. (i + 1)) `1 )) + (s1 * ((f /. (i + 2)) `1 )) by TOPREAL3:9 ;
A17: q `2 = (((1 - s1) * (f /. (i + 1))) `2 ) + ((s1 * (f /. (i + 2))) `2 ) by A15, TOPREAL3:7
.= ((1 - s1) * ((f /. (i + 1)) `2 )) + ((s1 * (f /. (i + 2))) `2 ) by TOPREAL3:9
.= ((1 - s1) * ((f /. (i + 1)) `2 )) + (s1 * ((f /. (i + 2)) `2 )) by TOPREAL3:9 ;

now

A18: ( 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, A4, A18, Th52;

case A19: ( (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
A20: f /. (i + 1) = ((1 - r) * p) + (r * q) and
( 0 <= r & r <= 1 ) by A8;
(f /. (i + 1)) `1 = (((1 - r) * p) `1 ) + ((r * q) `1 ) by A20, TOPREAL3:7
.= ((1 - r) * (p `1 )) + ((r * q) `1 ) by TOPREAL3:9
.= ((1 - r) * ((f /. (i + 1)) `1 )) + (r * (q `1 )) by A13, A19, TOPREAL3:9 ;
then r * (((f /. (i + 1)) `1 ) - (q `1 )) = 0 ;
then A21: ( 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 A21;

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 A20, EUCLID:33
.= 1 * p by EUCLID:31
.= p by EUCLID:33 ;
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 A22: ( 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 A22;

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 A15, EUCLID:33
.= 1 * (f /. (i + 1)) by EUCLID:31
.= f /. (i + 1) by EUCLID:33 ;
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 A19; :: 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 A23: ( (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
A24: f /. (i + 1) = ((1 - r) * p) + (r * q) and
( 0 <= r & r <= 1 ) by A8;
(f /. (i + 1)) `2 = (((1 - r) * p) `2 ) + ((r * q) `2 ) by A24, TOPREAL3:7
.= ((1 - r) * (p `2 )) + ((r * q) `2 ) by TOPREAL3:9
.= ((1 - r) * ((f /. (i + 1)) `2 )) + (r * (q `2 )) by A14, A23, TOPREAL3:9 ;
then r * (((f /. (i + 1)) `2 ) - (q `2 )) = 0 ;
then A25: ( 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 A25;

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 A24, EUCLID:33
.= 1 * p by EUCLID:31
.= p by EUCLID:33 ;
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 A17;
then A26: ( 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 A26;

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 A15, EUCLID:33
.= 1 * (f /. (i + 1)) by EUCLID:31
.= f /. (i + 1) by EUCLID:33 ;
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 A23; :: 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 A27: ( 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 A3, A6, TOPREAL1:def 5;
then consider s being Real such that
A28: q = ((1 - s) * (f /. i)) + (s * (f /. (i + 1))) and
( 0 <= s & s <= 1 ) ;
A29: q `1 = (((1 - s) * (f /. i)) `1 ) + ((s * (f /. (i + 1))) `1 ) by A28, TOPREAL3:7
.= ((1 - s) * ((f /. i) `1 )) + ((s * (f /. (i + 1))) `1 ) by TOPREAL3:9
.= ((1 - s) * ((f /. i) `1 )) + (s * ((f /. (i + 1)) `1 )) by TOPREAL3:9 ;
A30: q `2 = (((1 - s) * (f /. i)) `2 ) + ((s * (f /. (i + 1))) `2 ) by A28, TOPREAL3:7
.= ((1 - s) * ((f /. i) `2 )) + ((s * (f /. (i + 1))) `2 ) by TOPREAL3:9
.= ((1 - s) * ((f /. i) `2 )) + (s * ((f /. (i + 1)) `2 )) by TOPREAL3:9 ;
p in LSeg (f /. (i + 1)),(f /. (i + 2)) by A4, A5, A7, A27, TOPREAL1:def 5;
then consider s1 being Real such that
A31: p = ((1 - s1) * (f /. (i + 1))) + (s1 * (f /. (i + 2))) and
( 0 <= s1 & s1 <= 1 ) ;
A32: p `1 = (((1 - s1) * (f /. (i + 1))) `1 ) + ((s1 * (f /. (i + 2))) `1 ) by A31, TOPREAL3:7
.= ((1 - s1) * ((f /. (i + 1)) `1 )) + ((s1 * (f /. (i + 2))) `1 ) by TOPREAL3:9
.= ((1 - s1) * ((f /. (i + 1)) `1 )) + (s1 * ((f /. (i + 2)) `1 )) by TOPREAL3:9 ;
A33: p `2 = (((1 - s1) * (f /. (i + 1))) `2 ) + ((s1 * (f /. (i + 2))) `2 ) by A31, TOPREAL3:7
.= ((1 - s1) * ((f /. (i + 1)) `2 )) + ((s1 * (f /. (i + 2))) `2 ) by TOPREAL3:9
.= ((1 - s1) * ((f /. (i + 1)) `2 )) + (s1 * ((f /. (i + 2)) `2 )) by TOPREAL3:9 ;

now

A34: ( 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, A4, A34, Th52;

case A35: ( (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 A8;
then consider r being Real such that
A36: f /. (i + 1) = ((1 - r) * q) + (r * p) and
( 0 <= r & r <= 1 ) ;
(f /. (i + 1)) `1 = (((1 - r) * q) `1 ) + ((r * p) `1 ) by A36, TOPREAL3:7
.= ((1 - r) * (q `1 )) + ((r * p) `1 ) by TOPREAL3:9
.= ((1 - r) * ((f /. (i + 1)) `1 )) + (r * (p `1 )) by A29, A35, TOPREAL3:9 ;
then r * (((f /. (i + 1)) `1 ) - (p `1 )) = 0 ;
then A37: ( 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 A37;

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 A36, EUCLID:33
.= 1 * q by EUCLID:31
.= q by EUCLID:33 ;
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 A38: ( 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 A38;

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 A31, EUCLID:33
.= 1 * (f /. (i + 1)) by EUCLID:31
.= f /. (i + 1) by EUCLID:33 ;
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 A35; :: 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 A39: ( (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 A8;
then consider r being Real such that
A40: f /. (i + 1) = ((1 - r) * q) + (r * p) and
( 0 <= r & r <= 1 ) ;
(f /. (i + 1)) `2 = (((1 - r) * q) `2 ) + ((r * p) `2 ) by A40, TOPREAL3:7
.= ((1 - r) * (q `2 )) + ((r * p) `2 ) by TOPREAL3:9
.= ((1 - r) * ((f /. (i + 1)) `2 )) + (r * (p `2 )) by A30, A39, TOPREAL3:9 ;
then r * (((f /. (i + 1)) `2 ) - (p `2 )) = 0 ;
then A41: ( 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 A41;

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 A40, EUCLID:33
.= 1 * q by EUCLID:31
.= q by EUCLID:33 ;
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 A33;
then A42: ( 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 A42;

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 A31, EUCLID:33
.= 1 * (f /. (i + 1)) by EUCLID:31
.= f /. (i + 1) by EUCLID:33 ;
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 A39; :: 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 A4, A5, A7, TOPREAL1:def 5;
then A43: LSeg p,q c= LSeg (f /. (i + 1)),(f /. (i + 2)) by TOPREAL1:12;
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 A8, A43, Def1; :: thesis: verum

end;

end;

end;

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