let j, i, k be Element of 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 Element of NAT st
( j <= n & n <= k & (G * n,i) `1 = sup (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 Element of NAT st
( j <= n & n <= k & (G * n,i) `1 = sup (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 Element of NAT st
( j <= n & n <= k & (G * n,i) `1 = sup (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 & [k,i] in Indices G ) and
A4: j <= k ; :: thesis: ex n being Element of NAT st
( j <= n & n <= k & (G * n,i) `1 = sup (proj1 .: ((LSeg (G * j,i),(G * k,i)) /\ (L~ f))) )
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:162;
then A5: sup (proj1 .: ((LSeg (G * j,i),(G * k,i)) /\ (L~ f))) = sup ((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 10
.= E-bound ((LSeg (G * j,i),(G * k,i)) /\ (L~ f)) ;
ex x being set 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 PSCOMP_1:64, XBOOLE_0:def 4;
consider p being set such that
A6: p in E-most X1 by XBOOLE_0:def 1;
reconsider p = p as Point of (TOP-REAL 2) by A6;
A7: p `1 = (E-min ((LSeg (G * j,i),(G * k,i)) /\ (L~ f))) `1 by A6, PSCOMP_1:108
.= sup (proj1 .: ((LSeg (G * j,i),(G * k,i)) /\ (L~ f))) by A5, EUCLID:56 ;
A8: p in (LSeg (G * j,i),(G * k,i)) /\ (L~ f) by A6, XBOOLE_0:def 4;
then p in L~ f by 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
A9: p in Y and
A10: 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
A11: Y = LSeg f,i1 and
A12: 1 <= i1 and
A13: i1 + 1 <= len f by A10;
A14: p in LSeg (f /. i1),(f /. (i1 + 1)) by A9, A11, A12, A13, TOPREAL1:def 5;
i1 <= len f by A13, NAT_1:13;
then i1 in Seg (len f) by A12, FINSEQ_1:3;
then A15: i1 in dom f by FINSEQ_1:def 3;
then A16: f is special by A1, JORDAN8:7, RELAT_1:60;
1 < i1 + 1 by A12, NAT_1:13;
then i1 + 1 in Seg (len f) by A13, FINSEQ_1:3;
then A17: i1 + 1 in dom f by FINSEQ_1:def 3;
consider j0, i0 being Element of NAT such that
A18: ( [j0,i0] in Indices G & f /. i1 = G * j0,i0 ) by A1, A15, GOBOARD1:def 11;
consider jo, io being Element of NAT such that
A19: ( [jo,io] in Indices G & f /. (i1 + 1) = G * jo,io ) by A1, A17, GOBOARD1:def 11;
A20: ( 1 <= j & j <= len G & 1 <= i & i <= width G ) by A3, MATRIX_1:39;
A21: ( 1 <= k & k <= len G & 1 <= i & i <= width G ) by A3, MATRIX_1:39;
A22: ( 1 <= j0 & j0 <= len G & 1 <= i0 & i0 <= width G ) by A18, MATRIX_1:39;
A23: ( 1 <= jo & jo <= len G & 1 <= io & io <= width G ) by A19, MATRIX_1:39;
A24: (G * j,i) `2 = (G * 1,i) `2 by A20, GOBOARD5:2
.= (G * k,i) `2 by A21, GOBOARD5:2 ;
A25: p in LSeg (G * j,i),(G * k,i) by A8, XBOOLE_0:def 4;
(G * j,i) `1 <= (G * k,i) `1 by A4, A20, A21, SPRECT_3:25;
then A26: ( (G * j,i) `1 <= p `1 & p `1 <= (G * k,i) `1 ) by A25, TOPREAL1:9;
ex n being Element of 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 A12, A13, A16, TOPREAL1:def 7;

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

(G * j,i0) `2 = (G * 1,i0) `2 by A20, A22, GOBOARD5:2
.= (G * j0,i0) `2 by A22, GOBOARD5:2
.= p `2 by A14, A18, A27, GOBOARD7:6
.= (G * j,i) `2 by A24, A25, GOBOARD7:6 ;
then A28: ( i0 <= i & i0 >= i ) by A20, A22, GOBOARD5:5;
then A29: i = i0 by XXREAL_0:1;
(G * j,io) `2 = (G * 1,io) `2 by A20, A23, GOBOARD5:2
.= (G * jo,io) `2 by A23, GOBOARD5:2
.= p `2 by A14, A19, A27, GOBOARD7:6
.= (G * j,i) `2 by A24, A25, GOBOARD7:6 ;
then A30: ( io <= i & io >= i ) by A20, A23, GOBOARD5:5;
then A31: i = io by XXREAL_0:1;
thus ex n being Element of 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 A32: (f /. i1) `1 <= (f /. (i1 + 1)) `1 ; :: thesis: ex n being Element of NAT st
( j <= n & n <= k & G * n,i = p )

thus ex n being Element of 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 A33: f /. (i1 + 1) in LSeg (G * j,i),(G * k,i) ; :: thesis: ex n being Element of NAT st
( j <= n & n <= k & G * n,i = p )

1 + 1 <= i1 + 1 by A12, XREAL_1:8;
then f /. (i1 + 1) in L~ f by A13, A17, GOBOARD1:16, XXREAL_0:2;
then f /. (i1 + 1) in X1 by A33, XBOOLE_0:def 4;
then A34: p `1 >= (f /. (i1 + 1)) `1 by A5, A7, PSCOMP_1:71;
p `1 <= (f /. (i1 + 1)) `1 by A14, A32, TOPREAL1:9;
then A35: p `1 = (f /. (i1 + 1)) `1 by A34, XXREAL_0:1;
take n = jo; :: thesis: ( j <= n & n <= k & G * n,i = p )
A36: p in LSeg (G * j,i),(G * k,i) by A8, XBOOLE_0:def 4;
then A37: p `2 = (G * j,i) `2 by A24, GOBOARD7:6
.= (G * 1,i) `2 by A20, GOBOARD5:2
.= (G * n,i) `2 by A20, A23, GOBOARD5:2 ;
A38: p `1 = (G * jo,1) `1 by A19, A23, A35, GOBOARD5:3
.= (G * n,i) `1 by A20, A23, GOBOARD5:3 ;
(G * j,i) `1 <= (G * k,i) `1 by A4, A20, A21, SPRECT_3:25;
then A39: ( (G * j,i) `1 <= (G * n,i) `1 & (G * n,i) `1 <= (G * k,i) `1 ) by A36, A38, TOPREAL1:9;
hence j <= n by A20, A23, GOBOARD5:4; :: thesis: ( n <= k & G * n,i = p )
thus n <= k by A21, A23, A39, GOBOARD5:4; :: thesis: G * n,i = p
thus G * n,i = p by A37, A38, TOPREAL3:11; :: thesis: verum

end;

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

A41: (f /. (i1 + 1)) `2 = p `2 by A14, A27, GOBOARD7:6
.= (G * j,i) `2 by A24, A25, GOBOARD7:6 ;
thus ex n being Element of NAT st
( j <= n & n <= k & G * n,i = p ) :: thesis: verum

proof

per cases ( (f /. (i1 + 1)) `1 > (G * k,i) `1 or (f /. (i1 + 1)) `1 < (G * j,i) `1 ) by A24, A40, A41, GOBOARD7:9;

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

then A43: (G * jo,i) `1 > (G * k,i) `1 by A19, A30, XXREAL_0:1;
jo >= k by A19, A21, A23, A31, A42, GOBOARD5:4;
then A44: jo > k by A43, XXREAL_0:1;
j0 <= jo + 0 by A18, A19, A22, A23, A29, A31, A32, GOBOARD5:4;
then j0 - jo <= 0 by XREAL_1:22;
then A45: - (j0 - jo) >= - 0 ;
(abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A15, A17, A18, A19, GOBOARD1:def 11;
then 0 + (abs (j0 - jo)) = 1 by A29, A31, ABSVALUE:7;
then abs (- (j0 - jo)) = 1 by COMPLEX1:138;
then jo - j0 = 1 by A45, ABSVALUE:def 1;
then j0 + 1 = jo + 0 ;
then A46: j0 >= k by A44, NAT_1:13;
p `1 >= (G * j0,i0) `1 by A14, A18, A32, TOPREAL1:9;
then p `1 >= (G * j0,1) `1 by A22, GOBOARD5:3;
then p `1 >= (G * j0,i) `1 by A20, A22, GOBOARD5:3;
then (G * k,i) `1 >= (G * j0,i) `1 by A26, XXREAL_0:2;
then k >= j0 by A21, A22, GOBOARD5:4;
then A47: k = j0 by A46, XXREAL_0:1;
take n = j0; :: thesis: ( j <= n & n <= k & G * n,i = p )
A48: p `2 = (G * j,i) `2 by A24, A25, GOBOARD7:6
.= (G * 1,i) `2 by A20, GOBOARD5:2
.= (G * n,i) `2 by A20, A22, GOBOARD5:2 ;
p `1 >= (G * j0,i0) `1 by A14, A18, A32, TOPREAL1:9;
then p `1 >= (G * j0,1) `1 by A22, GOBOARD5:3;
then p `1 >= (G * j0,i) `1 by A20, A22, GOBOARD5:3;
then p `1 = (G * k,i) `1 by A26, A47, XXREAL_0:1;
hence ( j <= n & n <= k & G * n,i = p ) by A4, A47, A48, TOPREAL3:11; :: thesis: verum

end;

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

p `1 <= (f /. (i1 + 1)) `1 by A14, A32, TOPREAL1:9;
hence ex n being Element of NAT st
( j <= n & n <= k & G * n,i = p ) by A26, A49, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

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

thus ex n being Element of 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 A51: f /. i1 in LSeg (G * j,i),(G * k,i) ; :: thesis: ex n being Element of NAT st
( j <= n & n <= k & G * n,i = p )

1 + 1 <= i1 + 1 by A12, XREAL_1:8;
then f /. i1 in L~ f by A13, A15, GOBOARD1:16, XXREAL_0:2;
then f /. i1 in X1 by A51, XBOOLE_0:def 4;
then A52: p `1 >= (f /. i1) `1 by A5, A7, PSCOMP_1:71;
p `1 <= (f /. i1) `1 by A14, A50, TOPREAL1:9;
then A53: p `1 = (f /. i1) `1 by A52, XXREAL_0:1;
take n = j0; :: thesis: ( j <= n & n <= k & G * n,i = p )
A54: p in LSeg (G * j,i),(G * k,i) by A8, XBOOLE_0:def 4;
then A55: p `2 = (G * j,i) `2 by A24, GOBOARD7:6
.= (G * 1,i) `2 by A20, GOBOARD5:2
.= (G * n,i) `2 by A20, A22, GOBOARD5:2 ;
A56: p `1 = (G * j0,1) `1 by A18, A22, A53, GOBOARD5:3
.= (G * n,i) `1 by A20, A22, GOBOARD5:3 ;
(G * j,i) `1 <= (G * k,i) `1 by A4, A20, A21, SPRECT_3:25;
then A57: ( (G * j,i) `1 <= (G * n,i) `1 & (G * n,i) `1 <= (G * k,i) `1 ) by A54, A56, TOPREAL1:9;
hence j <= n by A20, A22, GOBOARD5:4; :: thesis: ( n <= k & G * n,i = p )
thus n <= k by A21, A22, A57, GOBOARD5:4; :: thesis: G * n,i = p
thus G * n,i = p by A55, A56, TOPREAL3:11; :: thesis: verum

end;

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

A59: (f /. i1) `2 = p `2 by A14, A27, GOBOARD7:6
.= (G * j,i) `2 by A24, A25, GOBOARD7:6 ;
thus ex n being Element of NAT st
( j <= n & n <= k & G * n,i = p ) :: thesis: verum

proof

per cases ( (f /. i1) `1 > (G * k,i) `1 or (f /. i1) `1 < (G * j,i) `1 ) by A24, A58, A59, GOBOARD7:9;

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

then A61: (G * j0,i) `1 > (G * k,i) `1 by A18, A28, XXREAL_0:1;
j0 >= k by A18, A21, A22, A29, A60, GOBOARD5:4;
then A62: j0 > k by A61, XXREAL_0:1;
jo <= j0 + 0 by A18, A19, A22, A23, A29, A31, A50, GOBOARD5:4;
then jo - j0 <= 0 by XREAL_1:22;
then A63: - (jo - j0) >= - 0 ;
(abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A15, A17, A18, A19, GOBOARD1:def 11;
then 0 + (abs (j0 - jo)) = 1 by A29, A31, ABSVALUE:7;
then j0 - jo = 1 by A63, ABSVALUE:def 1;
then jo + 1 = j0 - 0 ;
then A64: jo >= k by A62, NAT_1:13;
p `1 >= (G * jo,io) `1 by A14, A19, A50, TOPREAL1:9;
then p `1 >= (G * jo,1) `1 by A23, GOBOARD5:3;
then p `1 >= (G * jo,i) `1 by A20, A23, GOBOARD5:3;
then (G * k,i) `1 >= (G * jo,i) `1 by A26, XXREAL_0:2;
then k >= jo by A21, A23, GOBOARD5:4;
then A65: k = jo by A64, XXREAL_0:1;
take n = jo; :: thesis: ( j <= n & n <= k & G * n,i = p )
A66: p `2 = (G * j,i) `2 by A24, A25, GOBOARD7:6
.= (G * 1,i) `2 by A20, GOBOARD5:2
.= (G * n,i) `2 by A20, A23, GOBOARD5:2 ;
p `1 >= (G * jo,io) `1 by A14, A19, A50, TOPREAL1:9;
then p `1 >= (G * jo,1) `1 by A23, GOBOARD5:3;
then p `1 >= (G * jo,i) `1 by A20, A23, GOBOARD5:3;
then p `1 = (G * k,i) `1 by A26, A65, XXREAL_0:1;
hence ( j <= n & n <= k & G * n,i = p ) by A4, A65, A66, TOPREAL3:11; :: thesis: verum

end;

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

p `1 <= (f /. i1) `1 by A14, A50, TOPREAL1:9;
hence ex n being Element of NAT st
( j <= n & n <= k & G * n,i = p ) by A26, A67, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

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

then A68: p `1 = (f /. i1) `1 by A14, GOBOARD7:5;
take n = j0; :: thesis: ( j <= n & n <= k & G * n,i = p )
A69: p `2 = (G * j,i) `2 by A24, A25, GOBOARD7:6
.= (G * 1,i) `2 by A20, GOBOARD5:2
.= (G * n,i) `2 by A20, A22, GOBOARD5:2 ;
A70: p `1 = (G * j0,1) `1 by A18, A22, A68, GOBOARD5:3
.= (G * n,i) `1 by A20, A22, GOBOARD5:3 ;
(G * j,i) `1 <= (G * k,i) `1 by A4, A20, A21, SPRECT_3:25;
then A71: ( (G * j,i) `1 <= (G * n,i) `1 & (G * n,i) `1 <= (G * k,i) `1 ) by A25, A70, TOPREAL1:9;
hence j <= n by A20, A22, GOBOARD5:4; :: thesis: ( n <= k & G * n,i = p )
thus n <= k by A21, A22, A71, GOBOARD5:4; :: thesis: G * n,i = p
thus G * n,i = p by A69, A70, TOPREAL3:11; :: thesis: verum

end;

end;

end;

hence ex n being Element of NAT st
( j <= n & n <= k & (G * n,i) `1 = sup (proj1 .: ((LSeg (G * j,i),(G * k,i)) /\ (L~ f))) ) by A7; :: thesis: verum