let i, j, k be Element of NAT ; :: thesis:
let f be FinSequence of the carrier of (TOP-REAL 2); :: thesis:
let G be Go-board; :: thesis:
set X = (LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f);
assume that
A1: f is_sequence_on G and
A2: LSeg ((G * (i,j)),(G * (i,k))) meets L~ f and
A3: [i,j] in Indices G and
A4: [i,k] in Indices G and
A5: j <= k ; :: thesis:
A6: ( 1 <= i & i <= len G ) by A3, MATRIX_1:39;
ex x being set st
( x in LSeg ((G * (i,j)),(G * (i,k))) & x in L~ f ) by A2, XBOOLE_0:3;
then reconsider X1 = (LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f) as non empty compact Subset of (TOP-REAL 2) by XBOOLE_0:def 4;
consider p being set such that
A7: p in S-most X1 by XBOOLE_0:def 1;
reconsider p = p as Point of (TOP-REAL 2) by A7;
A8: p in (LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f) by A7, XBOOLE_0:def 4;
then A9: p in LSeg ((G * (i,j)),(G * (i,k))) by XBOOLE_0:def 4;
proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f)) = (proj2 | ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f)) by RELAT_1:162;
then A10: lower_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) = lower_bound ((proj2 | ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) .: ([#] ((TOP-REAL 2) | ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))))) by PRE_TOPC:def 10
.= S-bound ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f)) ;
A11: 1 <= k by A4, MATRIX_1:39;
A12: p `2 = (S-min ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) `2 by A7, PSCOMP_1:118
.= lower_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) by A10, EUCLID:56 ;
A13: ( 1 <= i & i <= len G ) by A3, MATRIX_1:39;
A14: 1 <= j by A3, MATRIX_1:39;
A15: k <= width G by A4, MATRIX_1:39;
then A16: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A14, SPRECT_3:24;
then A17: (G * (i,j)) `2 <= p `2 by A9, TOPREAL1:10;
A18: p `2 <= (G * (i,k)) `2 by A9, A16, TOPREAL1:10;
A19: j <= width G by A3, MATRIX_1:39;
then A20: (G * (i,j)) `1 = (G * (i,1)) `1 by A6, A14, GOBOARD5:3
.= (G * (i,k)) `1 by A13, A11, A15, GOBOARD5:3 ;
p in L~ f by A8, XBOOLE_0:def 4;
then p in union { (LSeg (f,k1)) where k1 is Element of NAT : ( 1 <= k1 & k1 + 1 <= len f ) } by TOPREAL1:def 6;
then consider Y being set such that
A21: p in Y and
A22: Y in { (LSeg (f,k1)) where k1 is Element of NAT : ( 1 <= k1 & k1 + 1 <= len f ) } by TARSKI:def 4;
consider i1 being Element of NAT such that
A23: Y = LSeg (f,i1) and
A24: 1 <= i1 and
A25: i1 + 1 <= len f by A22;
A26: p in LSeg ((f /. i1),(f /. (i1 + 1))) by A21, A23, A24, A25, TOPREAL1:def 5;
1 < i1 + 1 by A24, NAT_1:13;
then i1 + 1 in Seg (len f) by A25, FINSEQ_1:3;
then A27: i1 + 1 in dom f by FINSEQ_1:def 3;
then consider io, jo being Element of NAT such that
A28: [io,jo] in Indices G and
A29: f /. (i1 + 1) = G * (io,jo) by A1, GOBOARD1:def 11;
A30: ( 1 <= io & io <= len G ) by A28, MATRIX_1:39;
A31: 1 <= jo by A28, MATRIX_1:39;
i1 <= len f by A25, NAT_1:13;
then i1 in Seg (len f) by A24, FINSEQ_1:3;
then A32: i1 in dom f by FINSEQ_1:def 3;
then consider i0, j0 being Element of NAT such that
A33: [i0,j0] in Indices G and
A34: f /. i1 = G * (i0,j0) by A1, GOBOARD1:def 11;
A35: ( 1 <= i0 & i0 <= len G ) by A33, MATRIX_1:39;
A36: 1 <= j0 by A33, MATRIX_1:39;
A37: j0 <= width G by A33, MATRIX_1:39;
A38: jo <= width G by A28, MATRIX_1:39;
A39: f is special by A1, A32, JORDAN8:7, RELAT_1:60;
ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p )

proof

per cases ) `1 = (f /. (i1 + 1)) `1 or (f /. i1) `2 = (f /. (i1 + 1)) `2 ) by A24, A25, A39, TOPREAL1:def 7;

suppose A40: (f /. i1) `1 = (f /. (i1 + 1)) `1 ; :: thesis:

(G * (io,j)) `1 = (G * (io,1)) `1 by A14, A19, A30, GOBOARD5:3
.= (G * (io,jo)) `1 by A30, A31, A38, GOBOARD5:3
.= p `1 by A26, A29, A40, GOBOARD7:5
.= (G * (i,j)) `1 by A20, A9, GOBOARD7:5 ;
then ( io <= i & io >= i ) by A6, A14, A19, A30, GOBOARD5:4;
then A42: i = io by XXREAL_0:1;
(G * (i0,j)) `1 = (G * (i0,1)) `1 by A14, A19, A35, GOBOARD5:3
.= (G * (i0,j0)) `1 by A35, A36, A37, GOBOARD5:3
.= p `1 by A26, A34, A40, GOBOARD7:5
.= (G * (i,j)) `1 by A20, A9, GOBOARD7:5 ;
then ( i0 <= i & i0 >= i ) by A6, A14, A19, A35, GOBOARD5:4;
then A44: i = i0 by XXREAL_0:1;
thus ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) :: thesis:

proof

per cases ) `2 <= (f /. (i1 + 1)) `2 or (f /. i1) `2 > (f /. (i1 + 1)) `2 ) ;

suppose A45: (f /. i1) `2 <= (f /. (i1 + 1)) `2 ; :: thesis:

thus ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) :: thesis:

proof

per cases ;

suppose A46: f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) ; :: thesis:

1 + 1 <= i1 + 1 by A24, XREAL_1:8;
then f /. i1 in L~ f by A25, A32, GOBOARD1:16, XXREAL_0:2;
then f /. i1 in X1 by A46, XBOOLE_0:def 4;
then A47: p `2 <= (f /. i1) `2 by A10, A12, PSCOMP_1:71;
take n = j0; :: thesis:
A48: p in LSeg ((G * (i,j)),(G * (i,k))) by A8, XBOOLE_0:def 4;
p `2 >= (f /. i1) `2 by A26, A45, TOPREAL1:10;
then p `2 = (f /. i1) `2 by A47, XXREAL_0:1;
then A49: p `2 = (G * (1,j0)) `2 by A34, A35, A36, A37, GOBOARD5:2
.= (G * (i,n)) `2 by A6, A36, A37, GOBOARD5:2 ;
A50: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A14, A15, SPRECT_3:24;
then (G * (i,j)) `2 <= (G * (i,n)) `2 by A48, A49, TOPREAL1:10;
hence j <= n by A6, A19, A36, GOBOARD5:5; :: thesis:
(G * (i,n)) `2 <= (G * (i,k)) `2 by A48, A49, A50, TOPREAL1:10;
hence n <= k by A13, A11, A37, GOBOARD5:5; :: thesis:
p `1 = (G * (i,j)) `1 by A20, A48, GOBOARD7:5
.= (G * (i,1)) `1 by A6, A14, A19, GOBOARD5:3
.= (G * (i,n)) `1 by A6, A36, A37, GOBOARD5:3 ;
hence G * (i,n) = p by A49, TOPREAL3:11; :: thesis:

end;

suppose A51: not f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) ; :: thesis:

A52: (f /. i1) `1 = p `1 by A26, A40, GOBOARD7:5
.= (G * (i,j)) `1 by A20, A9, GOBOARD7:5 ;
thus ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) :: thesis:

proof

per cases ) `2 < (G * (i,j)) `2 or (f /. i1) `2 > (G * (i,k)) `2 ) by A20, A51, A52, GOBOARD7:8;

suppose A53: (f /. i1) `2 < (G * (i,j)) `2 ; :: thesis:

p `2 <= (G * (io,jo)) `2 by A26, A29, A45, TOPREAL1:10;
then p `2 <= (G * (1,jo)) `2 by A30, A31, A38, GOBOARD5:2;
then p `2 <= (G * (i,jo)) `2 by A6, A31, A38, GOBOARD5:2;
then (G * (i,j)) `2 <= (G * (i,jo)) `2 by A17, XXREAL_0:2;
then A54: j <= jo by A6, A19, A31, GOBOARD5:5;
(abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A32, A27, A33, A34, A28, A29, GOBOARD1:def 11;
then 0 + (abs (j0 - jo)) = 1 by A44, A42, ABSVALUE:7;
then A55: abs (- (j0 - jo)) = 1 by COMPLEX1:138;
j0 <= jo + 0 by A34, A29, A35, A37, A31, A44, A42, A45, GOBOARD5:5;
then j0 - jo <= 0 by XREAL_1:22;
then jo - j0 = 1 by A55, ABSVALUE:def 1;
then A56: j0 + 1 = jo + 0 ;
( (G * (i,j0)) `2 < (G * (i,j)) `2 & j0 <= j ) by A34, A6, A14, A37, A44, A53, GOBOARD5:5;
then j0 < j by XXREAL_0:1;
then jo <= j by A56, NAT_1:13;
then A57: j = jo by A54, XXREAL_0:1;
take n = jo; :: thesis:
A58: p `1 = (G * (i,j)) `1 by A20, A9, GOBOARD7:5
.= (G * (i,1)) `1 by A6, A14, A19, GOBOARD5:3
.= (G * (i,n)) `1 by A6, A31, A38, GOBOARD5:3 ;
p `2 <= (G * (io,jo)) `2 by A26, A29, A45, TOPREAL1:10;
then p `2 <= (G * (1,jo)) `2 by A30, A31, A38, GOBOARD5:2;
then p `2 <= (G * (i,jo)) `2 by A6, A31, A38, GOBOARD5:2;
then p `2 = (G * (i,j)) `2 by A17, A57, XXREAL_0:1;
hence ( j <= n & n <= k & G * (i,n) = p ) by A5, A57, A58, TOPREAL3:11; :: thesis:

end;

suppose A59: (f /. i1) `2 > (G * (i,k)) `2 ; :: thesis:

p `2 >= (f /. i1) `2 by A26, A45, TOPREAL1:10;
hence ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) by A18, A59, XXREAL_0:2; :: thesis:

end;

suppose A60: (f /. i1) `2 > (f /. (i1 + 1)) `2 ; :: thesis:

thus ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) :: thesis:

proof

per cases ;

suppose A61: f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) ; :: thesis:

1 + 1 <= i1 + 1 by A24, XREAL_1:8;
then f /. (i1 + 1) in L~ f by A25, A27, GOBOARD1:16, XXREAL_0:2;
then f /. (i1 + 1) in X1 by A61, XBOOLE_0:def 4;
then A62: p `2 <= (f /. (i1 + 1)) `2 by A10, A12, PSCOMP_1:71;
take n = jo; :: thesis:
A63: p in LSeg ((G * (i,j)),(G * (i,k))) by A8, XBOOLE_0:def 4;
p `2 >= (f /. (i1 + 1)) `2 by A26, A60, TOPREAL1:10;
then p `2 = (f /. (i1 + 1)) `2 by A62, XXREAL_0:1;
then A64: p `2 = (G * (1,jo)) `2 by A29, A30, A31, A38, GOBOARD5:2
.= (G * (i,n)) `2 by A6, A31, A38, GOBOARD5:2 ;
A65: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A14, A15, SPRECT_3:24;
then (G * (i,j)) `2 <= (G * (i,n)) `2 by A63, A64, TOPREAL1:10;
hence j <= n by A6, A19, A31, GOBOARD5:5; :: thesis:
(G * (i,n)) `2 <= (G * (i,k)) `2 by A63, A64, A65, TOPREAL1:10;
hence n <= k by A13, A11, A38, GOBOARD5:5; :: thesis:
p `1 = (G * (i,j)) `1 by A20, A63, GOBOARD7:5
.= (G * (i,1)) `1 by A6, A14, A19, GOBOARD5:3
.= (G * (i,n)) `1 by A6, A31, A38, GOBOARD5:3 ;
hence G * (i,n) = p by A64, TOPREAL3:11; :: thesis:

end;

suppose A66: not f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) ; :: thesis:

A67: (f /. (i1 + 1)) `1 = p `1 by A26, A40, GOBOARD7:5
.= (G * (i,j)) `1 by A20, A9, GOBOARD7:5 ;
thus ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) :: thesis:

proof

per cases ) `2 < (G * (i,j)) `2 or (f /. (i1 + 1)) `2 > (G * (i,k)) `2 ) by A20, A66, A67, GOBOARD7:8;

suppose A68: (f /. (i1 + 1)) `2 < (G * (i,j)) `2 ; :: thesis:

p `2 <= (G * (i0,j0)) `2 by A26, A34, A60, TOPREAL1:10;
then p `2 <= (G * (1,j0)) `2 by A35, A36, A37, GOBOARD5:2;
then p `2 <= (G * (i,j0)) `2 by A6, A36, A37, GOBOARD5:2;
then (G * (i,j)) `2 <= (G * (i,j0)) `2 by A17, XXREAL_0:2;
then A69: j <= j0 by A6, A19, A36, GOBOARD5:5;
jo <= j0 + 0 by A34, A29, A35, A36, A38, A44, A42, A60, GOBOARD5:5;
then jo - j0 <= 0 by XREAL_1:22;
then A70: - (jo - j0) >= - 0 ;
(abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A32, A27, A33, A34, A28, A29, GOBOARD1:def 11;
then 0 + (abs (j0 - jo)) = 1 by A44, A42, ABSVALUE:7;
then j0 - jo = 1 by A70, ABSVALUE:def 1;
then A71: jo + 1 = j0 - 0 ;
( (G * (i,jo)) `2 < (G * (i,j)) `2 & jo <= j ) by A29, A6, A14, A38, A42, A68, GOBOARD5:5;
then jo < j by XXREAL_0:1;
then j0 <= j by A71, NAT_1:13;
then A72: j = j0 by A69, XXREAL_0:1;
take n = j0; :: thesis:
A73: p `1 = (G * (i,j)) `1 by A20, A9, GOBOARD7:5
.= (G * (i,1)) `1 by A6, A14, A19, GOBOARD5:3
.= (G * (i,n)) `1 by A6, A36, A37, GOBOARD5:3 ;
p `2 <= (G * (i0,j0)) `2 by A26, A34, A60, TOPREAL1:10;
then p `2 <= (G * (1,j0)) `2 by A35, A36, A37, GOBOARD5:2;
then p `2 <= (G * (i,j0)) `2 by A6, A36, A37, GOBOARD5:2;
then p `2 = (G * (i,j)) `2 by A17, A72, XXREAL_0:1;
hence ( j <= n & n <= k & G * (i,n) = p ) by A5, A72, A73, TOPREAL3:11; :: thesis:

end;

suppose A74: (f /. (i1 + 1)) `2 > (G * (i,k)) `2 ; :: thesis:

p `2 >= (f /. (i1 + 1)) `2 by A26, A60, TOPREAL1:10;
hence ex n being Element of NAT st
( j <= n & n <= k & G * (i,n) = p ) by A18, A74, XXREAL_0:2; :: thesis:

end;

suppose A75: (f /. i1) `2 = (f /. (i1 + 1)) `2 ; :: thesis:

take n = j0; :: thesis:
p `2 = (f /. i1) `2 by A26, A75, GOBOARD7:6;
then A76: p `2 = (G * (1,j0)) `2 by A34, A35, A36, A37, GOBOARD5:2
.= (G * (i,n)) `2 by A6, A36, A37, GOBOARD5:2 ;
A77: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A14, A15, SPRECT_3:24;
then (G * (i,j)) `2 <= (G * (i,n)) `2 by A9, A76, TOPREAL1:10;
hence j <= n by A6, A19, A36, GOBOARD5:5; :: thesis:
(G * (i,n)) `2 <= (G * (i,k)) `2 by A9, A76, A77, TOPREAL1:10;
hence n <= k by A13, A11, A37, GOBOARD5:5; :: thesis:
p `1 = (G * (i,j)) `1 by A20, A9, GOBOARD7:5
.= (G * (i,1)) `1 by A6, A14, A19, GOBOARD5:3
.= (G * (i,n)) `1 by A6, A36, A37, GOBOARD5:3 ;
hence G * (i,n) = p by A76, TOPREAL3:11; :: thesis:

end;

hence ex n being Element of NAT st
( j <= n & n <= k & (G * (i,n)) `2 = lower_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) ) by A12; :: thesis: