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 ) 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