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

proof

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

suppose A40: (f /. i1) `2 = (f /. (i1 + 1)) `2 ; :: thesis: ex n being Nat st
( j <= n & n <= k & G * (n,i) = p )

(G * (j,io)) `2 = (G * (1,io)) `2 by A6, A19, A37, GOBOARD5:1
.= (G * (jo,io)) `2 by A30, A38, A37, GOBOARD5:1
.= p `2 by A26, A29, A40, GOBOARD7:6
.= (G * (j,i)) `2 by A20, A9, GOBOARD7:6 ;
then ( io <= i & io >= i ) by A6, A19, A14, A37, GOBOARD5:4;
then A41: i = io by XXREAL_0:1;
(G * (j,i0)) `2 = (G * (1,i0)) `2 by A6, A19, A35, GOBOARD5:1
.= (G * (j0,i0)) `2 by A34, A36, A35, GOBOARD5:1
.= p `2 by A26, A33, A40, GOBOARD7:6
.= (G * (j,i)) `2 by A20, A9, GOBOARD7:6 ;
then ( i0 <= i & i0 >= i ) by A6, A19, A14, A35, GOBOARD5:4;
then A42: i = i0 by XXREAL_0:1;
thus ex n being Nat st
( j <= n & n <= k & G * (n,i) = p ) :: thesis: verum

proof

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

suppose A43: (f /. i1) `1 <= (f /. (i1 + 1)) `1 ; :: thesis: ex n being Nat st
( j <= n & n <= k & G * (n,i) = p )

thus ex n being Nat st
( j <= n & n <= k & G * (n,i) = p ) :: thesis: verum

proof

per cases ( f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) or not f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) ) ;

suppose A44: f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) ; :: thesis: ex n being Nat st
( j <= n & n <= k & G * (n,i) = p )

1 + 1 <= i1 + 1 by A24, XREAL_1:6;
then f /. i1 in L~ f by A25, A31, GOBOARD1:1, XXREAL_0:2;
then f /. i1 in X1 by A44, XBOOLE_0:def 4;
then A45: p `1 <= (f /. i1) `1 by A10, A12, PSCOMP_1:24;
take n = j0; :: thesis: ( j <= n & n <= k & G * (n,i) = p )
A46: p in LSeg ((G * (j,i)),(G * (k,i))) by A8, XBOOLE_0:def 4;
p `1 >= (f /. i1) `1 by A26, A43, TOPREAL1:3;
then p `1 = (f /. i1) `1 by A45, XXREAL_0:1;
then A47: p `1 = (G * (j0,1)) `1 by A33, A34, A36, A35, GOBOARD5:2
.= (G * (n,i)) `1 by A14, A34, A36, GOBOARD5:2 ;
A48: (G * (j,i)) `1 <= (G * (k,i)) `1 by A5, A6, A14, A15, SPRECT_3:13;
then (G * (j,i)) `1 <= (G * (n,i)) `1 by A46, A47, TOPREAL1:3;
hence j <= n by A19, A14, A34, GOBOARD5:3; :: thesis: ( n <= k & G * (n,i) = p )
(G * (n,i)) `1 <= (G * (k,i)) `1 by A46, A47, A48, TOPREAL1:3;
hence n <= k by A11, A13, A36, GOBOARD5:3; :: thesis: G * (n,i) = p
p `2 = (G * (j,i)) `2 by A20, A46, GOBOARD7:6
.= (G * (1,i)) `2 by A6, A19, A14, GOBOARD5:1
.= (G * (n,i)) `2 by A14, A34, A36, GOBOARD5:1 ;
hence G * (n,i) = p by A47, TOPREAL3:6; :: thesis: verum

end;

suppose A49: not f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) ; :: thesis: ex n being Nat st
( j <= n & n <= k & G * (n,i) = p )

A50: (f /. i1) `2 = p `2 by A26, A40, GOBOARD7:6
.= (G * (j,i)) `2 by A20, A9, GOBOARD7:6 ;
thus ex n being Nat st
( j <= n & n <= k & G * (n,i) = p ) :: thesis: verum

proof

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

suppose A51: (f /. i1) `1 < (G * (j,i)) `1 ; :: thesis: ex n being Nat st
( j <= n & n <= k & G * (n,i) = p )

p `1 <= (G * (jo,io)) `1 by A26, A29, A43, TOPREAL1:3;
then p `1 <= (G * (jo,1)) `1 by A30, A38, A37, GOBOARD5:2;
then p `1 <= (G * (jo,i)) `1 by A14, A30, A38, GOBOARD5:2;
then (G * (j,i)) `1 <= (G * (jo,i)) `1 by A17, XXREAL_0:2;
then A52: j <= jo by A19, A14, A30, GOBOARD5:3;
|.(i0 - io).| + |.(j0 - jo).| = 1 by A1, A31, A27, A32, A33, A28, A29, GOBOARD1:def 9;
then 0 + |.(j0 - jo).| = 1 by A42, A41, ABSVALUE:2;
then A53: |.(- (j0 - jo)).| = 1 by COMPLEX1:52;
j0 <= jo + 0 by A33, A29, A36, A35, A30, A42, A41, A43, GOBOARD5:3;
then j0 - jo <= 0 by XREAL_1:20;
then jo - j0 = 1 by A53, ABSVALUE:def 1;
then A54: j0 + 1 = jo + 0 ;
( (G * (j0,i)) `1 < (G * (j,i)) `1 & j0 <= j ) by A33, A6, A14, A36, A42, A51, GOBOARD5:3;
then j0 < j by XXREAL_0:1;
then jo <= j by A54, NAT_1:13;
then A55: j = jo by A52, XXREAL_0:1;
take n = jo; :: thesis: ( j <= n & n <= k & G * (n,i) = p )
A56: p `2 = (G * (j,i)) `2 by A20, A9, GOBOARD7:6
.= (G * (1,i)) `2 by A6, A19, A14, GOBOARD5:1
.= (G * (n,i)) `2 by A14, A30, A38, GOBOARD5:1 ;
p `1 <= (G * (jo,io)) `1 by A26, A29, A43, TOPREAL1:3;
then p `1 <= (G * (jo,1)) `1 by A30, A38, A37, GOBOARD5:2;
then p `1 <= (G * (jo,i)) `1 by A14, A30, A38, GOBOARD5:2;
then p `1 = (G * (j,i)) `1 by A17, A55, XXREAL_0:1;
hence ( j <= n & n <= k & G * (n,i) = p ) by A5, A55, A56, TOPREAL3:6; :: thesis: verum

end;

suppose A57: (f /. i1) `1 > (G * (k,i)) `1 ; :: thesis: ex n being Nat st
( j <= n & n <= k & G * (n,i) = p )

p `1 >= (f /. i1) `1 by A26, A43, TOPREAL1:3;
hence ex n being Nat st
( j <= n & n <= k & G * (n,i) = p ) by A18, A57, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose A58: (f /. i1) `1 > (f /. (i1 + 1)) `1 ; :: thesis: ex n being Nat st
( j <= n & n <= k & G * (n,i) = p )

thus ex n being Nat st
( j <= n & n <= k & G * (n,i) = p ) :: thesis: verum

proof

per cases ( f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) or not f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) ) ;

suppose A59: f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) ; :: thesis: ex n being Nat st
( j <= n & n <= k & G * (n,i) = p )

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

end;

suppose A64: not f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) ; :: thesis: ex n being Nat st
( j <= n & n <= k & G * (n,i) = p )

A65: (f /. (i1 + 1)) `2 = p `2 by A26, A40, GOBOARD7:6
.= (G * (j,i)) `2 by A20, A9, GOBOARD7:6 ;
thus ex n being Nat st
( j <= n & n <= k & G * (n,i) = p ) :: thesis: verum

proof

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

suppose A66: (f /. (i1 + 1)) `1 < (G * (j,i)) `1 ; :: thesis: ex n being Nat st
( j <= n & n <= k & G * (n,i) = p )

p `1 <= (G * (j0,i0)) `1 by A26, A33, A58, TOPREAL1:3;
then p `1 <= (G * (j0,1)) `1 by A34, A36, A35, GOBOARD5:2;
then p `1 <= (G * (j0,i)) `1 by A14, A34, A36, GOBOARD5:2;
then (G * (j,i)) `1 <= (G * (j0,i)) `1 by A17, XXREAL_0:2;
then A67: j <= j0 by A19, A14, A34, GOBOARD5:3;
jo <= j0 + 0 by A33, A29, A34, A35, A38, A42, A41, A58, GOBOARD5:3;
then jo - j0 <= 0 by XREAL_1:20;
then A68: - (jo - j0) >= - 0 ;
|.(i0 - io).| + |.(j0 - jo).| = 1 by A1, A31, A27, A32, A33, A28, A29, GOBOARD1:def 9;
then 0 + |.(j0 - jo).| = 1 by A42, A41, ABSVALUE:2;
then j0 - jo = 1 by A68, ABSVALUE:def 1;
then A69: jo + 1 = j0 - 0 ;
( (G * (jo,i)) `1 < (G * (j,i)) `1 & jo <= j ) by A29, A6, A14, A38, A41, A66, GOBOARD5:3;
then jo < j by XXREAL_0:1;
then j0 <= j by A69, NAT_1:13;
then A70: j = j0 by A67, XXREAL_0:1;
take n = j0; :: thesis: ( j <= n & n <= k & G * (n,i) = p )
A71: p `2 = (G * (j,i)) `2 by A20, A9, GOBOARD7:6
.= (G * (1,i)) `2 by A6, A19, A14, GOBOARD5:1
.= (G * (n,i)) `2 by A14, A34, A36, GOBOARD5:1 ;
p `1 <= (G * (j0,i0)) `1 by A26, A33, A58, TOPREAL1:3;
then p `1 <= (G * (j0,1)) `1 by A34, A36, A35, GOBOARD5:2;
then p `1 <= (G * (j0,i)) `1 by A14, A34, A36, GOBOARD5:2;
then p `1 = (G * (j,i)) `1 by A17, A70, XXREAL_0:1;
hence ( j <= n & n <= k & G * (n,i) = p ) by A5, A70, A71, TOPREAL3:6; :: thesis: verum

end;

suppose A72: (f /. (i1 + 1)) `1 > (G * (k,i)) `1 ; :: thesis: ex n being Nat st
( j <= n & n <= k & G * (n,i) = p )

p `1 >= (f /. (i1 + 1)) `1 by A26, A58, TOPREAL1:3;
hence ex n being Nat st
( j <= n & n <= k & G * (n,i) = p ) by A18, A72, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

suppose A73: (f /. i1) `1 = (f /. (i1 + 1)) `1 ; :: thesis: ex n being Nat st
( j <= n & n <= k & G * (n,i) = p )

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

end;

end;

end;

hence ex n being Nat st
( j <= n & n <= k & (G * (n,i)) `1 = lower_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) ) by A12; :: thesis: verum