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:8;
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: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 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 5;
then A9: 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 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 5;
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: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 ;
q in LSeg (f /. (i + 1)),(f /. (i + 2)) by A3, A5, A10, TOPREAL1:def 5;
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: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 ;
A15: p `2 = (((1 - s) * (f /. i)) `2 ) + ((s * (f /. (i + 1))) `2 ) by A11, 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 ;
A16: q `1 = (((1 - s1) * (f /. (i + 1))) `1 ) + ((s1 * (f /. (i + 2))) `1 ) by A13, 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 ;

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:7
.= ((1 - r) * (p `1 )) + ((r * q) `1 ) by TOPREAL3:9
.= ((1 - r) * ((f /. (i + 1)) `1 )) + (r * (q `1 )) by A12, A18, TOPREAL3:9 ;
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: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 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: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 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:7
.= ((1 - r) * (p `2 )) + ((r * q) `2 ) by TOPREAL3:9
.= ((1 - r) * ((f /. (i + 1)) `2 )) + (r * (q `2 )) by A15, A22, TOPREAL3:9 ;
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: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 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: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 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 5;
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: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 ;
p in LSeg (f /. (i + 1)),(f /. (i + 2)) by A3, A5, A26, TOPREAL1:def 5;
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: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 ;
A31: q `2 = (((1 - s) * (f /. i)) `2 ) + ((s * (f /. (i + 1))) `2 ) by A27, 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 ;
A32: p `1 = (((1 - s1) * (f /. (i + 1))) `1 ) + ((s1 * (f /. (i + 2))) `1 ) by A29, 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 ;

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:7
.= ((1 - r) * (q `1 )) + ((r * p) `1 ) by TOPREAL3:9
.= ((1 - r) * ((f /. (i + 1)) `1 )) + (r * (p `1 )) by A28, A34, TOPREAL3:9 ;
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: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 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: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 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:7
.= ((1 - r) * (q `2 )) + ((r * p) `2 ) by TOPREAL3:9
.= ((1 - r) * ((f /. (i + 1)) `2 )) + (r * (p `2 )) by A31, A38, TOPREAL3:9 ;
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: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 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: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 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 5;
then A42: 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 A6, A42, Def1; :: thesis: verum

end;

end;

end;

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