:: JORDAN1F semantic presentation begin theorem Th1: :: JORDAN1F:1 for i, j, k being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) for G being Go-board st f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds 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))) ) proof let i, j, 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 * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds 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))) ) 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 * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds 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))) ) let G be Go-board; ::_thesis: ( f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k implies 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))) ) ) 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: 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))) ) A6: ( 1 <= i & i <= len G ) by A3, MATRIX_1:38; 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:129; 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_5 .= S-bound ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f)) ; A11: 1 <= k by A4, MATRIX_1:38; A12: p `2 = (S-min ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) `2 by A7, PSCOMP_1:55 .= lower_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) by A10, EUCLID:52 ; A13: ( 1 <= i & i <= len G ) by A3, MATRIX_1:38; A14: 1 <= j by A3, MATRIX_1:38; A15: k <= width G by A4, MATRIX_1:38; then A16: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A14, SPRECT_3:12; then A17: (G * (i,j)) `2 <= p `2 by A9, TOPREAL1:4; A18: p `2 <= (G * (i,k)) `2 by A9, A16, TOPREAL1:4; A19: j <= width G by A3, MATRIX_1:38; then A20: (G * (i,j)) `1 = (G * (i,1)) `1 by A6, A14, GOBOARD5:2 .= (G * (i,k)) `1 by A13, A11, A15, GOBOARD5:2 ; 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_4; 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_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 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_9; A30: ( 1 <= io & io <= len G ) by A28, MATRIX_1:38; A31: 1 <= jo by A28, MATRIX_1:38; i1 <= len f by A25, NAT_1:13; then i1 in Seg (len f) by A24, FINSEQ_1:1; 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_9; A35: ( 1 <= i0 & i0 <= len G ) by A33, MATRIX_1:38; A36: 1 <= j0 by A33, MATRIX_1:38; A37: j0 <= width G by A33, MATRIX_1:38; A38: jo <= width G by A28, MATRIX_1:38; A39: f is special by A1, A32, JORDAN8:4, RELAT_1:38; ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) proof percases ( (f /. i1) `1 = (f /. (i1 + 1)) `1 or (f /. i1) `2 = (f /. (i1 + 1)) `2 ) by A24, A25, A39, TOPREAL1:def_5; supposeA40: (f /. i1) `1 = (f /. (i1 + 1)) `1 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) (G * (io,j)) `1 = (G * (io,1)) `1 by A14, A19, A30, GOBOARD5:2 .= (G * (io,jo)) `1 by A30, A31, A38, GOBOARD5:2 .= 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:3; then A41: i = io by XXREAL_0:1; (G * (i0,j)) `1 = (G * (i0,1)) `1 by A14, A19, A35, GOBOARD5:2 .= (G * (i0,j0)) `1 by A35, A36, A37, GOBOARD5:2 .= 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:3; then A42: i = i0 by XXREAL_0:1; thus ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum proof percases ( (f /. i1) `2 <= (f /. (i1 + 1)) `2 or (f /. i1) `2 > (f /. (i1 + 1)) `2 ) ; supposeA43: (f /. i1) `2 <= (f /. (i1 + 1)) `2 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) thus ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum proof percases ( f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) or not f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) ) ; supposeA44: f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) 1 + 1 <= i1 + 1 by A24, XREAL_1:6; then f /. i1 in L~ f by A25, A32, GOBOARD1:1, XXREAL_0:2; then f /. i1 in X1 by A44, XBOOLE_0:def_4; then A45: p `2 <= (f /. i1) `2 by A10, A12, PSCOMP_1:24; take n = j0; ::_thesis: ( j <= n & n <= k & G * (i,n) = p ) A46: p in LSeg ((G * (i,j)),(G * (i,k))) by A8, XBOOLE_0:def_4; p `2 >= (f /. i1) `2 by A26, A43, TOPREAL1:4; then p `2 = (f /. i1) `2 by A45, XXREAL_0:1; then A47: p `2 = (G * (1,j0)) `2 by A34, A35, A36, A37, GOBOARD5:1 .= (G * (i,n)) `2 by A6, A36, A37, GOBOARD5:1 ; A48: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A14, A15, SPRECT_3:12; then (G * (i,j)) `2 <= (G * (i,n)) `2 by A46, A47, TOPREAL1:4; hence j <= n by A6, A19, A36, GOBOARD5:4; ::_thesis: ( n <= k & G * (i,n) = p ) (G * (i,n)) `2 <= (G * (i,k)) `2 by A46, A47, A48, TOPREAL1:4; hence n <= k by A13, A11, A37, GOBOARD5:4; ::_thesis: G * (i,n) = p p `1 = (G * (i,j)) `1 by A20, A46, GOBOARD7:5 .= (G * (i,1)) `1 by A6, A14, A19, GOBOARD5:2 .= (G * (i,n)) `1 by A6, A36, A37, GOBOARD5:2 ; hence G * (i,n) = p by A47, TOPREAL3:6; ::_thesis: verum end; supposeA49: not f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) A50: (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: verum proof percases ( (f /. i1) `2 < (G * (i,j)) `2 or (f /. i1) `2 > (G * (i,k)) `2 ) by A20, A49, A50, GOBOARD7:7; supposeA51: (f /. i1) `2 < (G * (i,j)) `2 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) p `2 <= (G * (io,jo)) `2 by A26, A29, A43, TOPREAL1:4; then p `2 <= (G * (1,jo)) `2 by A30, A31, A38, GOBOARD5:1; then p `2 <= (G * (i,jo)) `2 by A6, A31, A38, GOBOARD5:1; then (G * (i,j)) `2 <= (G * (i,jo)) `2 by A17, XXREAL_0:2; then A52: j <= jo by A6, A19, A31, GOBOARD5:4; (abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A32, A27, A33, A34, A28, A29, GOBOARD1:def_9; then 0 + (abs (j0 - jo)) = 1 by A42, A41, ABSVALUE:2; then A53: abs (- (j0 - jo)) = 1 by COMPLEX1:52; j0 <= jo + 0 by A34, A29, A35, A37, A31, A42, A41, A43, GOBOARD5:4; then j0 - jo <= 0 by XREAL_1:20; then jo - j0 = 1 by A53, ABSVALUE:def_1; then A54: j0 + 1 = jo + 0 ; ( (G * (i,j0)) `2 < (G * (i,j)) `2 & j0 <= j ) by A34, A6, A14, A37, A42, A51, GOBOARD5:4; 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 * (i,n) = p ) A56: p `1 = (G * (i,j)) `1 by A20, A9, GOBOARD7:5 .= (G * (i,1)) `1 by A6, A14, A19, GOBOARD5:2 .= (G * (i,n)) `1 by A6, A31, A38, GOBOARD5:2 ; p `2 <= (G * (io,jo)) `2 by A26, A29, A43, TOPREAL1:4; then p `2 <= (G * (1,jo)) `2 by A30, A31, A38, GOBOARD5:1; then p `2 <= (G * (i,jo)) `2 by A6, A31, A38, GOBOARD5:1; then p `2 = (G * (i,j)) `2 by A17, A55, XXREAL_0:1; hence ( j <= n & n <= k & G * (i,n) = p ) by A5, A55, A56, TOPREAL3:6; ::_thesis: verum end; supposeA57: (f /. i1) `2 > (G * (i,k)) `2 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) p `2 >= (f /. i1) `2 by A26, A43, TOPREAL1:4; hence ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) by A18, A57, XXREAL_0:2; ::_thesis: verum end; end; end; end; end; end; end; supposeA58: (f /. i1) `2 > (f /. (i1 + 1)) `2 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) thus ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum proof percases ( f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) or not f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) ) ; supposeA59: f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = 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 `2 <= (f /. (i1 + 1)) `2 by A10, A12, PSCOMP_1:24; take n = jo; ::_thesis: ( j <= n & n <= k & G * (i,n) = p ) A61: p in LSeg ((G * (i,j)),(G * (i,k))) by A8, XBOOLE_0:def_4; p `2 >= (f /. (i1 + 1)) `2 by A26, A58, TOPREAL1:4; then p `2 = (f /. (i1 + 1)) `2 by A60, XXREAL_0:1; then A62: p `2 = (G * (1,jo)) `2 by A29, A30, A31, A38, GOBOARD5:1 .= (G * (i,n)) `2 by A6, A31, A38, GOBOARD5:1 ; A63: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A14, A15, SPRECT_3:12; then (G * (i,j)) `2 <= (G * (i,n)) `2 by A61, A62, TOPREAL1:4; hence j <= n by A6, A19, A31, GOBOARD5:4; ::_thesis: ( n <= k & G * (i,n) = p ) (G * (i,n)) `2 <= (G * (i,k)) `2 by A61, A62, A63, TOPREAL1:4; hence n <= k by A13, A11, A38, GOBOARD5:4; ::_thesis: G * (i,n) = p p `1 = (G * (i,j)) `1 by A20, A61, GOBOARD7:5 .= (G * (i,1)) `1 by A6, A14, A19, GOBOARD5:2 .= (G * (i,n)) `1 by A6, A31, A38, GOBOARD5:2 ; hence G * (i,n) = p by A62, TOPREAL3:6; ::_thesis: verum end; supposeA64: not f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) A65: (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: verum proof percases ( (f /. (i1 + 1)) `2 < (G * (i,j)) `2 or (f /. (i1 + 1)) `2 > (G * (i,k)) `2 ) by A20, A64, A65, GOBOARD7:7; supposeA66: (f /. (i1 + 1)) `2 < (G * (i,j)) `2 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) p `2 <= (G * (i0,j0)) `2 by A26, A34, A58, TOPREAL1:4; then p `2 <= (G * (1,j0)) `2 by A35, A36, A37, GOBOARD5:1; then p `2 <= (G * (i,j0)) `2 by A6, A36, A37, GOBOARD5:1; then (G * (i,j)) `2 <= (G * (i,j0)) `2 by A17, XXREAL_0:2; then A67: j <= j0 by A6, A19, A36, GOBOARD5:4; jo <= j0 + 0 by A34, A29, A35, A36, A38, A42, A41, A58, GOBOARD5:4; then jo - j0 <= 0 by XREAL_1:20; then A68: - (jo - j0) >= - 0 ; (abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A32, A27, A33, A34, A28, A29, GOBOARD1:def_9; then 0 + (abs (j0 - jo)) = 1 by A42, A41, ABSVALUE:2; then j0 - jo = 1 by A68, ABSVALUE:def_1; then A69: jo + 1 = j0 - 0 ; ( (G * (i,jo)) `2 < (G * (i,j)) `2 & jo <= j ) by A29, A6, A14, A38, A41, A66, GOBOARD5:4; 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 * (i,n) = p ) A71: p `1 = (G * (i,j)) `1 by A20, A9, GOBOARD7:5 .= (G * (i,1)) `1 by A6, A14, A19, GOBOARD5:2 .= (G * (i,n)) `1 by A6, A36, A37, GOBOARD5:2 ; p `2 <= (G * (i0,j0)) `2 by A26, A34, A58, TOPREAL1:4; then p `2 <= (G * (1,j0)) `2 by A35, A36, A37, GOBOARD5:1; then p `2 <= (G * (i,j0)) `2 by A6, A36, A37, GOBOARD5:1; then p `2 = (G * (i,j)) `2 by A17, A70, XXREAL_0:1; hence ( j <= n & n <= k & G * (i,n) = p ) by A5, A70, A71, TOPREAL3:6; ::_thesis: verum end; supposeA72: (f /. (i1 + 1)) `2 > (G * (i,k)) `2 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) p `2 >= (f /. (i1 + 1)) `2 by A26, A58, TOPREAL1:4; hence ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) by A18, A72, XXREAL_0:2; ::_thesis: verum end; end; end; end; end; end; end; end; end; end; supposeA73: (f /. i1) `2 = (f /. (i1 + 1)) `2 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) take n = j0; ::_thesis: ( j <= n & n <= k & G * (i,n) = p ) p `2 = (f /. i1) `2 by A26, A73, GOBOARD7:6; then A74: p `2 = (G * (1,j0)) `2 by A34, A35, A36, A37, GOBOARD5:1 .= (G * (i,n)) `2 by A6, A36, A37, GOBOARD5:1 ; A75: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A14, A15, SPRECT_3:12; then (G * (i,j)) `2 <= (G * (i,n)) `2 by A9, A74, TOPREAL1:4; hence j <= n by A6, A19, A36, GOBOARD5:4; ::_thesis: ( n <= k & G * (i,n) = p ) (G * (i,n)) `2 <= (G * (i,k)) `2 by A9, A74, A75, TOPREAL1:4; hence n <= k by A13, A11, A37, GOBOARD5:4; ::_thesis: G * (i,n) = p p `1 = (G * (i,j)) `1 by A20, A9, GOBOARD7:5 .= (G * (i,1)) `1 by A6, A14, A19, GOBOARD5:2 .= (G * (i,n)) `1 by A6, A36, A37, GOBOARD5:2 ; hence G * (i,n) = p by A74, TOPREAL3:6; ::_thesis: verum end; end; 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: verum end; theorem :: JORDAN1F:2 for i, j, k being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) for G being Go-board st f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds ex n being Element of NAT st ( j <= n & n <= k & (G * (i,n)) `2 = upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) ) proof let i, j, 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 * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds ex n being Element of NAT st ( j <= n & n <= k & (G * (i,n)) `2 = upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (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 * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds ex n being Element of NAT st ( j <= n & n <= k & (G * (i,n)) `2 = upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) ) let G be Go-board; ::_thesis: ( f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k implies ex n being Element of NAT st ( j <= n & n <= k & (G * (i,n)) `2 = upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) ) ) 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: ex n being Element of NAT st ( j <= n & n <= k & (G * (i,n)) `2 = upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) ) A6: ( 1 <= i & i <= len G ) by A3, MATRIX_1:38; 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 N-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; 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_4; then consider Y being set such that A10: p in Y and A11: 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 A12: Y = LSeg (f,i1) and A13: 1 <= i1 and A14: i1 + 1 <= len f by A11; A15: p in LSeg ((f /. i1),(f /. (i1 + 1))) by A10, A12, A13, A14, TOPREAL1:def_3; 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:129; then A16: upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) = upper_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_5 .= N-bound ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f)) ; A17: 1 <= k by A4, MATRIX_1:38; A18: 1 <= j by A3, MATRIX_1:38; 1 < i1 + 1 by A13, NAT_1:13; then i1 + 1 in Seg (len f) by A14, FINSEQ_1:1; then A19: i1 + 1 in dom f by FINSEQ_1:def_3; then consider io, jo being Element of NAT such that A20: [io,jo] in Indices G and A21: f /. (i1 + 1) = G * (io,jo) by A1, GOBOARD1:def_9; A22: ( 1 <= io & io <= len G ) by A20, MATRIX_1:38; A23: 1 <= jo by A20, MATRIX_1:38; A24: p `2 = (N-min ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) `2 by A7, PSCOMP_1:39 .= upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) by A16, EUCLID:52 ; A25: ( 1 <= i & i <= len G ) by A3, MATRIX_1:38; A26: k <= width G by A4, MATRIX_1:38; then A27: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A18, SPRECT_3:12; then A28: (G * (i,j)) `2 <= p `2 by A9, TOPREAL1:4; A29: p `2 <= (G * (i,k)) `2 by A9, A27, TOPREAL1:4; A30: j <= width G by A3, MATRIX_1:38; then A31: (G * (i,j)) `1 = (G * (i,1)) `1 by A6, A18, GOBOARD5:2 .= (G * (i,k)) `1 by A25, A17, A26, GOBOARD5:2 ; A32: jo <= width G by A20, MATRIX_1:38; i1 <= len f by A14, NAT_1:13; then i1 in Seg (len f) by A13, FINSEQ_1:1; then A33: i1 in dom f by FINSEQ_1:def_3; then consider i0, j0 being Element of NAT such that A34: [i0,j0] in Indices G and A35: f /. i1 = G * (i0,j0) by A1, GOBOARD1:def_9; A36: ( 1 <= i0 & i0 <= len G ) by A34, MATRIX_1:38; A37: 1 <= j0 by A34, MATRIX_1:38; A38: j0 <= width G by A34, MATRIX_1:38; A39: f is special by A1, A33, JORDAN8:4, RELAT_1:38; ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) proof percases ( (f /. i1) `1 = (f /. (i1 + 1)) `1 or (f /. i1) `2 = (f /. (i1 + 1)) `2 ) by A13, A14, A39, TOPREAL1:def_5; supposeA40: (f /. i1) `1 = (f /. (i1 + 1)) `1 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) (G * (io,j)) `1 = (G * (io,1)) `1 by A18, A30, A22, GOBOARD5:2 .= (G * (io,jo)) `1 by A22, A23, A32, GOBOARD5:2 .= p `1 by A15, A21, A40, GOBOARD7:5 .= (G * (i,j)) `1 by A31, A9, GOBOARD7:5 ; then ( io <= i & io >= i ) by A6, A18, A30, A22, GOBOARD5:3; then A41: i = io by XXREAL_0:1; (G * (i0,j)) `1 = (G * (i0,1)) `1 by A18, A30, A36, GOBOARD5:2 .= (G * (i0,j0)) `1 by A36, A37, A38, GOBOARD5:2 .= p `1 by A15, A35, A40, GOBOARD7:5 .= (G * (i,j)) `1 by A31, A9, GOBOARD7:5 ; then ( i0 <= i & i0 >= i ) by A6, A18, A30, A36, GOBOARD5:3; then A42: i = i0 by XXREAL_0:1; thus ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum proof percases ( (f /. i1) `2 <= (f /. (i1 + 1)) `2 or (f /. i1) `2 > (f /. (i1 + 1)) `2 ) ; supposeA43: (f /. i1) `2 <= (f /. (i1 + 1)) `2 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) thus ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum proof percases ( f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) or not f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) ) ; supposeA44: f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) 1 + 1 <= i1 + 1 by A13, XREAL_1:6; then f /. (i1 + 1) in L~ f by A14, A19, GOBOARD1:1, XXREAL_0:2; then f /. (i1 + 1) in X1 by A44, XBOOLE_0:def_4; then A45: p `2 >= (f /. (i1 + 1)) `2 by A16, A24, PSCOMP_1:24; take n = jo; ::_thesis: ( j <= n & n <= k & G * (i,n) = p ) A46: p in LSeg ((G * (i,j)),(G * (i,k))) by A8, XBOOLE_0:def_4; p `2 <= (f /. (i1 + 1)) `2 by A15, A43, TOPREAL1:4; then p `2 = (f /. (i1 + 1)) `2 by A45, XXREAL_0:1; then A47: p `2 = (G * (1,jo)) `2 by A21, A22, A23, A32, GOBOARD5:1 .= (G * (i,n)) `2 by A6, A23, A32, GOBOARD5:1 ; A48: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A18, A26, SPRECT_3:12; then (G * (i,j)) `2 <= (G * (i,n)) `2 by A46, A47, TOPREAL1:4; hence j <= n by A6, A30, A23, GOBOARD5:4; ::_thesis: ( n <= k & G * (i,n) = p ) (G * (i,n)) `2 <= (G * (i,k)) `2 by A46, A47, A48, TOPREAL1:4; hence n <= k by A25, A17, A32, GOBOARD5:4; ::_thesis: G * (i,n) = p p `1 = (G * (i,j)) `1 by A31, A46, GOBOARD7:5 .= (G * (i,1)) `1 by A6, A18, A30, GOBOARD5:2 .= (G * (i,n)) `1 by A6, A23, A32, GOBOARD5:2 ; hence G * (i,n) = p by A47, TOPREAL3:6; ::_thesis: verum end; supposeA49: not f /. (i1 + 1) in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) A50: (f /. (i1 + 1)) `1 = p `1 by A15, A40, GOBOARD7:5 .= (G * (i,j)) `1 by A31, A9, GOBOARD7:5 ; thus ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum proof percases ( (f /. (i1 + 1)) `2 > (G * (i,k)) `2 or (f /. (i1 + 1)) `2 < (G * (i,j)) `2 ) by A31, A49, A50, GOBOARD7:7; supposeA51: (f /. (i1 + 1)) `2 > (G * (i,k)) `2 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) p `2 >= (G * (i0,j0)) `2 by A15, A35, A43, TOPREAL1:4; then p `2 >= (G * (1,j0)) `2 by A36, A37, A38, GOBOARD5:1; then p `2 >= (G * (i,j0)) `2 by A6, A37, A38, GOBOARD5:1; then (G * (i,k)) `2 >= (G * (i,j0)) `2 by A29, XXREAL_0:2; then A52: k >= j0 by A25, A17, A38, GOBOARD5:4; (abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A33, A19, A34, A35, A20, A21, GOBOARD1:def_9; then 0 + (abs (j0 - jo)) = 1 by A42, A41, ABSVALUE:2; then A53: abs (- (j0 - jo)) = 1 by COMPLEX1:52; j0 <= jo + 0 by A35, A21, A36, A38, A23, A42, A41, A43, GOBOARD5:4; then j0 - jo <= 0 by XREAL_1:20; then jo - j0 = 1 by A53, ABSVALUE:def_1; then A54: j0 + 1 = jo + 0 ; ( (G * (i,jo)) `2 > (G * (i,k)) `2 & jo >= k ) by A21, A25, A26, A23, A41, A51, GOBOARD5:4; then jo > k by XXREAL_0:1; then j0 >= k by A54, NAT_1:13; then A55: k = j0 by A52, XXREAL_0:1; take n = j0; ::_thesis: ( j <= n & n <= k & G * (i,n) = p ) A56: p `1 = (G * (i,j)) `1 by A31, A9, GOBOARD7:5 .= (G * (i,1)) `1 by A6, A18, A30, GOBOARD5:2 .= (G * (i,n)) `1 by A6, A37, A38, GOBOARD5:2 ; p `2 >= (G * (i0,j0)) `2 by A15, A35, A43, TOPREAL1:4; then p `2 >= (G * (1,j0)) `2 by A36, A37, A38, GOBOARD5:1; then p `2 >= (G * (i,j0)) `2 by A6, A37, A38, GOBOARD5:1; then p `2 = (G * (i,k)) `2 by A29, A55, XXREAL_0:1; hence ( j <= n & n <= k & G * (i,n) = p ) by A5, A55, A56, TOPREAL3:6; ::_thesis: verum end; supposeA57: (f /. (i1 + 1)) `2 < (G * (i,j)) `2 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) p `2 <= (f /. (i1 + 1)) `2 by A15, A43, TOPREAL1:4; hence ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) by A28, A57, XXREAL_0:2; ::_thesis: verum end; end; end; end; end; end; end; supposeA58: (f /. i1) `2 > (f /. (i1 + 1)) `2 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) thus ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum proof percases ( f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) or not f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) ) ; supposeA59: f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) 1 + 1 <= i1 + 1 by A13, XREAL_1:6; then f /. i1 in L~ f by A14, A33, GOBOARD1:1, XXREAL_0:2; then f /. i1 in X1 by A59, XBOOLE_0:def_4; then A60: p `2 >= (f /. i1) `2 by A16, A24, PSCOMP_1:24; take n = j0; ::_thesis: ( j <= n & n <= k & G * (i,n) = p ) A61: p in LSeg ((G * (i,j)),(G * (i,k))) by A8, XBOOLE_0:def_4; p `2 <= (f /. i1) `2 by A15, A58, TOPREAL1:4; then p `2 = (f /. i1) `2 by A60, XXREAL_0:1; then A62: p `2 = (G * (1,j0)) `2 by A35, A36, A37, A38, GOBOARD5:1 .= (G * (i,n)) `2 by A6, A37, A38, GOBOARD5:1 ; A63: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A18, A26, SPRECT_3:12; then (G * (i,j)) `2 <= (G * (i,n)) `2 by A61, A62, TOPREAL1:4; hence j <= n by A6, A30, A37, GOBOARD5:4; ::_thesis: ( n <= k & G * (i,n) = p ) (G * (i,n)) `2 <= (G * (i,k)) `2 by A61, A62, A63, TOPREAL1:4; hence n <= k by A25, A17, A38, GOBOARD5:4; ::_thesis: G * (i,n) = p p `1 = (G * (i,j)) `1 by A31, A61, GOBOARD7:5 .= (G * (i,1)) `1 by A6, A18, A30, GOBOARD5:2 .= (G * (i,n)) `1 by A6, A37, A38, GOBOARD5:2 ; hence G * (i,n) = p by A62, TOPREAL3:6; ::_thesis: verum end; supposeA64: not f /. i1 in LSeg ((G * (i,j)),(G * (i,k))) ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) A65: (f /. i1) `1 = p `1 by A15, A40, GOBOARD7:5 .= (G * (i,j)) `1 by A31, A9, GOBOARD7:5 ; thus ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) ::_thesis: verum proof percases ( (f /. i1) `2 > (G * (i,k)) `2 or (f /. i1) `2 < (G * (i,j)) `2 ) by A31, A64, A65, GOBOARD7:7; supposeA66: (f /. i1) `2 > (G * (i,k)) `2 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) p `2 >= (G * (io,jo)) `2 by A15, A21, A58, TOPREAL1:4; then p `2 >= (G * (1,jo)) `2 by A22, A23, A32, GOBOARD5:1; then p `2 >= (G * (i,jo)) `2 by A6, A23, A32, GOBOARD5:1; then (G * (i,k)) `2 >= (G * (i,jo)) `2 by A29, XXREAL_0:2; then A67: k >= jo by A25, A17, A32, GOBOARD5:4; jo <= j0 + 0 by A35, A21, A36, A37, A32, A42, A41, A58, GOBOARD5:4; then jo - j0 <= 0 by XREAL_1:20; then A68: - (jo - j0) >= - 0 ; (abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A33, A19, A34, A35, A20, A21, GOBOARD1:def_9; then 0 + (abs (j0 - jo)) = 1 by A42, A41, ABSVALUE:2; then j0 - jo = 1 by A68, ABSVALUE:def_1; then A69: jo + 1 = j0 - 0 ; ( (G * (i,j0)) `2 > (G * (i,k)) `2 & j0 >= k ) by A35, A25, A26, A37, A42, A66, GOBOARD5:4; then j0 > k by XXREAL_0:1; then jo >= k by A69, NAT_1:13; then A70: k = jo by A67, XXREAL_0:1; take n = jo; ::_thesis: ( j <= n & n <= k & G * (i,n) = p ) A71: p `1 = (G * (i,j)) `1 by A31, A9, GOBOARD7:5 .= (G * (i,1)) `1 by A6, A18, A30, GOBOARD5:2 .= (G * (i,n)) `1 by A6, A23, A32, GOBOARD5:2 ; p `2 >= (G * (io,jo)) `2 by A15, A21, A58, TOPREAL1:4; then p `2 >= (G * (1,jo)) `2 by A22, A23, A32, GOBOARD5:1; then p `2 >= (G * (i,jo)) `2 by A6, A23, A32, GOBOARD5:1; then p `2 = (G * (i,k)) `2 by A29, A70, XXREAL_0:1; hence ( j <= n & n <= k & G * (i,n) = p ) by A5, A70, A71, TOPREAL3:6; ::_thesis: verum end; supposeA72: (f /. i1) `2 < (G * (i,j)) `2 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) p `2 <= (f /. i1) `2 by A15, A58, TOPREAL1:4; hence ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) by A28, A72, XXREAL_0:2; ::_thesis: verum end; end; end; end; end; end; end; end; end; end; supposeA73: (f /. i1) `2 = (f /. (i1 + 1)) `2 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (i,n) = p ) take n = j0; ::_thesis: ( j <= n & n <= k & G * (i,n) = p ) p `2 = (f /. i1) `2 by A15, A73, GOBOARD7:6; then A74: p `2 = (G * (1,j0)) `2 by A35, A36, A37, A38, GOBOARD5:1 .= (G * (i,n)) `2 by A6, A37, A38, GOBOARD5:1 ; A75: (G * (i,j)) `2 <= (G * (i,k)) `2 by A5, A6, A18, A26, SPRECT_3:12; then (G * (i,j)) `2 <= (G * (i,n)) `2 by A9, A74, TOPREAL1:4; hence j <= n by A6, A30, A37, GOBOARD5:4; ::_thesis: ( n <= k & G * (i,n) = p ) (G * (i,n)) `2 <= (G * (i,k)) `2 by A9, A74, A75, TOPREAL1:4; hence n <= k by A25, A17, A38, GOBOARD5:4; ::_thesis: G * (i,n) = p p `1 = (G * (i,j)) `1 by A31, A9, GOBOARD7:5 .= (G * (i,1)) `1 by A6, A18, A30, GOBOARD5:2 .= (G * (i,n)) `1 by A6, A37, A38, GOBOARD5:2 ; hence G * (i,n) = p by A74, TOPREAL3:6; ::_thesis: verum end; end; end; hence ex n being Element of NAT st ( j <= n & n <= k & (G * (i,n)) `2 = upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) ) by A24; ::_thesis: verum end; theorem :: JORDAN1F:3 for j, i, k being Element of NAT 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 = lower_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) ) proof 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 = 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 Element of 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 Element of 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 Element of 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_1:38; 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 XBOOLE_0:def_4; consider p being set 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_1:38; 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_1:38; A14: ( 1 <= i & i <= width G ) by A3, MATRIX_1:38; A15: k <= len G by A4, MATRIX_1:38; 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_1:38; 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 Element of 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 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_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 Element of 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_1:38; 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 Element of 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_1:38; A35: ( 1 <= i0 & i0 <= width G ) by A32, MATRIX_1:38; A36: j0 <= len G by A32, MATRIX_1:38; A37: ( 1 <= io & io <= width G ) by A28, MATRIX_1:38; A38: jo <= len G by A28, MATRIX_1:38; A39: f is special by A1, A31, JORDAN8:4, RELAT_1:38; ex n being Element of NAT st ( j <= n & n <= k & G * (n,i) = p ) proof percases ( (f /. i1) `2 = (f /. (i1 + 1)) `2 or (f /. i1) `1 = (f /. (i1 + 1)) `1 ) by A24, A25, A39, TOPREAL1:def_5; supposeA40: (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,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 Element of NAT st ( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum proof percases ( (f /. i1) `1 <= (f /. (i1 + 1)) `1 or (f /. i1) `1 > (f /. (i1 + 1)) `1 ) ; supposeA43: (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 percases ( f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) or not f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) ) ; supposeA44: 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 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; supposeA49: 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 ) A50: (f /. i1) `2 = p `2 by A26, A40, GOBOARD7:6 .= (G * (j,i)) `2 by A20, A9, GOBOARD7:6 ; thus ex n being Element of NAT st ( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum proof percases ( (f /. i1) `1 < (G * (j,i)) `1 or (f /. i1) `1 > (G * (k,i)) `1 ) by A20, A49, A50, GOBOARD7:8; supposeA51: (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 <= (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; (abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A31, A27, A32, A33, A28, A29, GOBOARD1:def_9; then 0 + (abs (j0 - jo)) = 1 by A42, A41, ABSVALUE:2; then A53: abs (- (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; supposeA57: (f /. i1) `1 > (G * (k,i)) `1 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (n,i) = p ) p `1 >= (f /. i1) `1 by A26, A43, TOPREAL1:3; hence ex n being Element of 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; supposeA58: (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 percases ( f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) or not f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) ) ; supposeA59: 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 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; supposeA64: 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 ) 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 Element of NAT st ( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum proof percases ( (f /. (i1 + 1)) `1 < (G * (j,i)) `1 or (f /. (i1 + 1)) `1 > (G * (k,i)) `1 ) by A20, A64, A65, GOBOARD7:8; supposeA66: (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 <= (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 ; (abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A31, A27, A32, A33, A28, A29, GOBOARD1:def_9; then 0 + (abs (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; supposeA72: (f /. (i1 + 1)) `1 > (G * (k,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 A26, A58, TOPREAL1:3; hence ex n being Element of 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; supposeA73: (f /. i1) `1 = (f /. (i1 + 1)) `1 ; ::_thesis: ex n being Element of 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 Element of 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 end; theorem :: JORDAN1F:4 for j, i, k being Element of NAT 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 = upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) ) proof 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 = upper_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 Element of NAT st ( j <= n & n <= k & (G * (n,i)) `1 = upper_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 Element of NAT st ( j <= n & n <= k & (G * (n,i)) `1 = upper_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 Element of NAT st ( j <= n & n <= k & (G * (n,i)) `1 = upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) ) A6: 1 <= j by A3, MATRIX_1:38; 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 XBOOLE_0:def_4; consider p being set such that A7: p in E-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: upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) = upper_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 .= E-bound ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f)) ; A11: ( 1 <= i & i <= width G ) by A3, MATRIX_1:38; A12: p `1 = (E-min ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) `1 by A7, PSCOMP_1:47 .= upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) by A10, EUCLID:52 ; A13: 1 <= k by A4, MATRIX_1:38; A14: ( 1 <= i & i <= width G ) by A3, MATRIX_1:38; A15: k <= len G by A4, MATRIX_1:38; 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_1:38; then A20: (G * (j,i)) `2 = (G * (1,i)) `2 by A6, A14, GOBOARD5:1 .= (G * (k,i)) `2 by A13, A15, A11, GOBOARD5:1 ; 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_4; 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_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 Element of 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_1:38; 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 Element of 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_1:38; A35: ( 1 <= i0 & i0 <= width G ) by A32, MATRIX_1:38; A36: j0 <= len G by A32, MATRIX_1:38; A37: ( 1 <= io & io <= width G ) by A28, MATRIX_1:38; A38: jo <= len G by A28, MATRIX_1:38; A39: f is special by A1, A31, JORDAN8:4, RELAT_1:38; ex n being Element of NAT st ( j <= n & n <= k & G * (n,i) = p ) proof percases ( (f /. i1) `2 = (f /. (i1 + 1)) `2 or (f /. i1) `1 = (f /. (i1 + 1)) `1 ) by A24, A25, A39, TOPREAL1:def_5; supposeA40: (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,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 Element of NAT st ( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum proof percases ( (f /. i1) `1 <= (f /. (i1 + 1)) `1 or (f /. i1) `1 > (f /. (i1 + 1)) `1 ) ; supposeA43: (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 percases ( f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) or not f /. (i1 + 1) in LSeg ((G * (j,i)),(G * (k,i))) ) ; supposeA44: 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 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 A44, XBOOLE_0:def_4; then A45: p `1 >= (f /. (i1 + 1)) `1 by A10, A12, PSCOMP_1:24; take n = jo; ::_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)) `1 by A26, A43, TOPREAL1:3; then p `1 = (f /. (i1 + 1)) `1 by A45, XXREAL_0:1; then A47: p `1 = (G * (jo,1)) `1 by A29, A30, A38, A37, GOBOARD5:2 .= (G * (n,i)) `1 by A14, A30, A38, 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, A30, 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 A13, A11, A38, 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, A30, A38, GOBOARD5:1 ; hence G * (n,i) = p by A47, TOPREAL3:6; ::_thesis: verum end; supposeA49: 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 ) A50: (f /. (i1 + 1)) `2 = p `2 by A26, A40, GOBOARD7:6 .= (G * (j,i)) `2 by A20, A9, GOBOARD7:6 ; thus ex n being Element of NAT st ( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum proof percases ( (f /. (i1 + 1)) `1 > (G * (k,i)) `1 or (f /. (i1 + 1)) `1 < (G * (j,i)) `1 ) by A20, A49, A50, GOBOARD7:8; supposeA51: (f /. (i1 + 1)) `1 > (G * (k,i)) `1 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (n,i) = p ) p `1 >= (G * (j0,i0)) `1 by A26, A33, A43, 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 * (k,i)) `1 >= (G * (j0,i)) `1 by A18, XXREAL_0:2; then A52: k >= j0 by A13, A11, A36, GOBOARD5:3; (abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A31, A27, A32, A33, A28, A29, GOBOARD1:def_9; then 0 + (abs (j0 - jo)) = 1 by A42, A41, ABSVALUE:2; then A53: abs (- (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 * (jo,i)) `1 > (G * (k,i)) `1 & jo >= k ) by A29, A15, A11, A30, A41, A51, GOBOARD5:3; then jo > k by XXREAL_0:1; then j0 >= k by A54, NAT_1:13; then A55: k = j0 by A52, XXREAL_0:1; take n = j0; ::_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, A34, A36, GOBOARD5:1 ; p `1 >= (G * (j0,i0)) `1 by A26, A33, A43, 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 * (k,i)) `1 by A18, A55, XXREAL_0:1; hence ( j <= n & n <= k & G * (n,i) = p ) by A5, A55, A56, TOPREAL3:6; ::_thesis: verum end; supposeA57: (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 A26, A43, TOPREAL1:3; hence ex n being Element of NAT st ( j <= n & n <= k & G * (n,i) = p ) by A17, A57, XXREAL_0:2; ::_thesis: verum end; end; end; end; end; end; end; supposeA58: (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 percases ( f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) or not f /. i1 in LSeg ((G * (j,i)),(G * (k,i))) ) ; supposeA59: 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 A24, XREAL_1:6; then f /. i1 in L~ f by A25, A31, GOBOARD1:1, XXREAL_0:2; then f /. i1 in X1 by A59, XBOOLE_0:def_4; then A60: p `1 >= (f /. i1) `1 by A10, A12, PSCOMP_1:24; take n = j0; ::_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 by A26, A58, TOPREAL1:3; then p `1 = (f /. i1) `1 by A60, XXREAL_0:1; then A62: p `1 = (G * (j0,1)) `1 by A33, A34, A36, A35, GOBOARD5:2 .= (G * (n,i)) `1 by A14, A34, A36, 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, A34, 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 A13, A11, A36, 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, A34, A36, GOBOARD5:1 ; hence G * (n,i) = p by A62, TOPREAL3:6; ::_thesis: verum end; supposeA64: 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 ) A65: (f /. i1) `2 = p `2 by A26, A40, GOBOARD7:6 .= (G * (j,i)) `2 by A20, A9, GOBOARD7:6 ; thus ex n being Element of NAT st ( j <= n & n <= k & G * (n,i) = p ) ::_thesis: verum proof percases ( (f /. i1) `1 > (G * (k,i)) `1 or (f /. i1) `1 < (G * (j,i)) `1 ) by A20, A64, A65, GOBOARD7:8; supposeA66: (f /. i1) `1 > (G * (k,i)) `1 ; ::_thesis: ex n being Element of NAT st ( j <= n & n <= k & G * (n,i) = p ) p `1 >= (G * (jo,io)) `1 by A26, A29, A58, 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 * (k,i)) `1 >= (G * (jo,i)) `1 by A18, XXREAL_0:2; then A67: k >= jo by A13, A11, A38, 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 ; (abs (i0 - io)) + (abs (j0 - jo)) = 1 by A1, A31, A27, A32, A33, A28, A29, GOBOARD1:def_9; then 0 + (abs (j0 - jo)) = 1 by A42, A41, ABSVALUE:2; then j0 - jo = 1 by A68, ABSVALUE:def_1; then A69: jo + 1 = j0 - 0 ; ( (G * (j0,i)) `1 > (G * (k,i)) `1 & j0 >= k ) by A33, A15, A11, A34, A42, A66, GOBOARD5:3; then j0 > k by XXREAL_0:1; then jo >= k by A69, NAT_1:13; then A70: k = jo by A67, XXREAL_0:1; take n = jo; ::_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, A30, A38, GOBOARD5:1 ; p `1 >= (G * (jo,io)) `1 by A26, A29, A58, 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 * (k,i)) `1 by A18, A70, XXREAL_0:1; hence ( j <= n & n <= k & G * (n,i) = p ) by A5, A70, A71, TOPREAL3:6; ::_thesis: verum end; supposeA72: (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 A26, A58, TOPREAL1:3; hence ex n being Element of NAT st ( j <= n & n <= k & G * (n,i) = p ) by A17, A72, XXREAL_0:2; ::_thesis: verum end; end; end; end; end; end; end; end; end; end; supposeA73: (f /. i1) `1 = (f /. (i1 + 1)) `1 ; ::_thesis: ex n being Element of 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 A13, A11, 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 Element of NAT st ( j <= n & n <= k & (G * (n,i)) `1 = upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) ) by A12; ::_thesis: verum end; theorem Th5: :: JORDAN1F:5 for C being compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT holds (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) proof let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) let n be Element of NAT ; ::_thesis: (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46; then ( Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) & E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ) by FINSEQ_6:90, JORDAN1E:def_1, SPRECT_2:43; then ( W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) & (Upper_Seq (C,n)) /. 1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 ) by FINSEQ_5:44, SPRECT_2:43; hence (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by FINSEQ_6:92; ::_thesis: verum end; theorem Th6: :: JORDAN1F:6 for C being compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT holds (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n))) proof let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n))) let n be Element of NAT ; ::_thesis: (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n))) Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))) by JORDAN1E:def_2; hence (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n))) by FINSEQ_5:53; ::_thesis: verum end; theorem Th7: :: JORDAN1F:7 for C being compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT holds (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n))) proof let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n))) let n be Element of NAT ; ::_thesis: (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n))) A1: ( Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) & rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = rng (Cage (C,n)) ) by FINSEQ_6:90, JORDAN1E:def_1, SPRECT_2:43; then len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_5:42, SPRECT_2:46; hence (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n))) by A1, FINSEQ_5:45, SPRECT_2:46; ::_thesis: verum end; theorem Th8: :: JORDAN1F:8 for C being compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT holds (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n))) proof let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n))) let n be Element of NAT ; ::_thesis: (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n))) A1: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43; E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46; then ( Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))) & E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ) by FINSEQ_6:90, JORDAN1E:def_2, SPRECT_2:43; hence (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by FINSEQ_5:54 .= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by FINSEQ_6:def_1 .= W-min (L~ (Cage (C,n))) by A1, FINSEQ_6:92 ; ::_thesis: verum end; theorem Th9: :: JORDAN1F:9 for C being compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT holds ( ( L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) ) or ( L~ (Upper_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) ) ) proof let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds ( ( L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) ) or ( L~ (Upper_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) ) ) let n be Element of NAT ; ::_thesis: ( ( L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) ) or ( L~ (Upper_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) ) ) set WC = W-min (L~ (Cage (C,n))); set EC = E-max (L~ (Cage (C,n))); A1: ( Lower_Arc (L~ (Cage (C,n))) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) & (Upper_Arc (L~ (Cage (C,n)))) \/ (Lower_Arc (L~ (Cage (C,n)))) = L~ (Cage (C,n)) ) by JORDAN6:50; ( (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) & (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n))) ) by Th5, Th7; then A2: L~ (Upper_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) by TOPREAL1:25; ( (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n))) & (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n))) ) by Th6, Th8; then A3: L~ (Lower_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) by JORDAN5B:14, TOPREAL1:25; ( (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n))) = L~ (Cage (C,n)) & Upper_Arc (L~ (Cage (C,n))) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) ) by JORDAN1E:13, JORDAN6:50; hence ( ( L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) ) or ( L~ (Upper_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) ) ) by A2, A3, A1, JORDAN6:48; ::_thesis: verum end; theorem Th10: :: JORDAN1F:10 for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT holds Upper_Seq (C,n) is_sequence_on Gauge (C,n) proof let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds Upper_Seq (C,n) is_sequence_on Gauge (C,n) let n be Element of NAT ; ::_thesis: Upper_Seq (C,n) is_sequence_on Gauge (C,n) Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then A1: Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) is_sequence_on Gauge (C,n) by REVROT_1:34; Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) by JORDAN1E:def_1 .= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) | ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by FINSEQ_5:def_1 ; hence Upper_Seq (C,n) is_sequence_on Gauge (C,n) by A1, GOBOARD1:22; ::_thesis: verum end; theorem Th11: :: JORDAN1F:11 for G being Go-board for p being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Element of NAT st ( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G * (i1,j1) & f /. 1 = G * (i2,j2) holds (abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) holds <*p*> ^ f is_sequence_on G proof let G be Go-board; ::_thesis: for p being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Element of NAT st ( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G * (i1,j1) & f /. 1 = G * (i2,j2) holds (abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) holds <*p*> ^ f is_sequence_on G let p be Point of (TOP-REAL 2); ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Element of NAT st ( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G * (i1,j1) & f /. 1 = G * (i2,j2) holds (abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) holds <*p*> ^ f is_sequence_on G let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G & ex i, j being Element of NAT st ( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G * (i1,j1) & f /. 1 = G * (i2,j2) holds (abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) implies <*p*> ^ f is_sequence_on G ) assume that A1: f is_sequence_on G and A2: ex i, j being Element of NAT st ( [i,j] in Indices G & p = G * (i,j) ) and A3: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G * (i1,j1) & f /. 1 = G * (i2,j2) holds (abs (i2 - i1)) + (abs (j2 - j1)) = 1 ; ::_thesis: <*p*> ^ f is_sequence_on G A4: now__::_thesis:_for_m,_k,_i,_j_being_Element_of_NAT_st_[m,k]_in_Indices_G_&_[i,j]_in_Indices_G_&_<*p*>_/._(len_<*p*>)_=_G_*_(m,k)_&_f_/._1_=_G_*_(i,j)_&_len_<*p*>_in_dom_<*p*>_&_1_in_dom_f_holds_ 1_=_(abs_(m_-_i))_+_(abs_(k_-_j)) let m, k, i, j be Element of NAT ; ::_thesis: ( [m,k] in Indices G & [i,j] in Indices G & <*p*> /. (len <*p*>) = G * (m,k) & f /. 1 = G * (i,j) & len <*p*> in dom <*p*> & 1 in dom f implies 1 = (abs (m - i)) + (abs (k - j)) ) assume that A5: ( [m,k] in Indices G & [i,j] in Indices G & <*p*> /. (len <*p*>) = G * (m,k) & f /. 1 = G * (i,j) ) and A6: len <*p*> in dom <*p*> and 1 in dom f ; ::_thesis: 1 = (abs (m - i)) + (abs (k - j)) len <*p*> = 1 by FINSEQ_1:40; then <*p*> . (len <*p*>) = p by FINSEQ_1:40; then <*p*> /. (len <*p*>) = p by A6, PARTFUN1:def_6; then (abs (i - m)) + (abs (j - k)) = 1 by A3, A5; hence 1 = (abs (m - i)) + (abs (j - k)) by UNIFORM1:11 .= (abs (m - i)) + (abs (k - j)) by UNIFORM1:11 ; ::_thesis: verum end; A7: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_(<*p*>_^_f)_holds_ ex_i,_j_being_Element_of_NAT_st_ (_[i,j]_in_Indices_G_&_(<*p*>_^_f)_/._n_=_G_*_(i,j)_) let n be Element of NAT ; ::_thesis: ( n in dom (<*p*> ^ f) implies ex i, j being Element of NAT st ( [j,b3] in Indices G & (<*p*> ^ f) /. i = G * (j,b3) ) ) assume A8: n in dom (<*p*> ^ f) ; ::_thesis: ex i, j being Element of NAT st ( [j,b3] in Indices G & (<*p*> ^ f) /. i = G * (j,b3) ) percases ( n in dom <*p*> or ex l being Nat st ( l in dom f & n = (len <*p*>) + l ) ) by A8, FINSEQ_1:25; supposeA9: n in dom <*p*> ; ::_thesis: ex i, j being Element of NAT st ( [j,b3] in Indices G & (<*p*> ^ f) /. i = G * (j,b3) ) consider i, j being Element of NAT such that A10: [i,j] in Indices G and A11: p = G * (i,j) by A2; take i = i; ::_thesis: ex j being Element of NAT st ( [i,j] in Indices G & (<*p*> ^ f) /. n = G * (i,j) ) take j = j; ::_thesis: ( [i,j] in Indices G & (<*p*> ^ f) /. n = G * (i,j) ) thus [i,j] in Indices G by A10; ::_thesis: (<*p*> ^ f) /. n = G * (i,j) n in Seg 1 by A9, FINSEQ_1:38; then ( 1 <= n & n <= 1 ) by FINSEQ_1:1; then n = 1 by XXREAL_0:1; then <*p*> . n = p by FINSEQ_1:40; then <*p*> /. n = p by A9, PARTFUN1:def_6; hence (<*p*> ^ f) /. n = G * (i,j) by A9, A11, FINSEQ_4:68; ::_thesis: verum end; suppose ex l being Nat st ( l in dom f & n = (len <*p*>) + l ) ; ::_thesis: ex i, j being Element of NAT st ( [j,b3] in Indices G & (<*p*> ^ f) /. i = G * (j,b3) ) then consider l being Nat such that A12: l in dom f and A13: n = (len <*p*>) + l ; consider i, j being Element of NAT such that A14: [i,j] in Indices G and A15: f /. l = G * (i,j) by A1, A12, GOBOARD1:def_9; take i = i; ::_thesis: ex j being Element of NAT st ( [i,j] in Indices G & (<*p*> ^ f) /. n = G * (i,j) ) take j = j; ::_thesis: ( [i,j] in Indices G & (<*p*> ^ f) /. n = G * (i,j) ) thus [i,j] in Indices G by A14; ::_thesis: (<*p*> ^ f) /. n = G * (i,j) thus (<*p*> ^ f) /. n = G * (i,j) by A12, A13, A15, FINSEQ_4:69; ::_thesis: verum end; end; end; A16: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_<*p*>_&_n_+_1_in_dom_<*p*>_holds_ for_m,_k,_i,_j_being_Element_of_NAT_st_[m,k]_in_Indices_G_&_[i,j]_in_Indices_G_&_<*p*>_/._n_=_G_*_(m,k)_&_<*p*>_/._(n_+_1)_=_G_*_(i,j)_holds_ (abs_(m_-_i))_+_(abs_(k_-_j))_=_1 let n be Element of NAT ; ::_thesis: ( n in dom <*p*> & n + 1 in dom <*p*> implies for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & <*p*> /. n = G * (m,k) & <*p*> /. (n + 1) = G * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 ) assume that A17: n in dom <*p*> and A18: n + 1 in dom <*p*> ; ::_thesis: for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & <*p*> /. n = G * (m,k) & <*p*> /. (n + 1) = G * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 n + 1 <= len <*p*> by A18, FINSEQ_3:25; then A19: n + 1 <= 1 by FINSEQ_1:39; 1 <= n by A17, FINSEQ_3:25; then 1 + 1 <= n + 1 by XREAL_1:6; hence for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & <*p*> /. n = G * (m,k) & <*p*> /. (n + 1) = G * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 by A19, XXREAL_0:2; ::_thesis: verum end; for n being Element of NAT st n in dom f & n + 1 in dom f holds for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & f /. n = G * (m,k) & f /. (n + 1) = G * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 by A1, GOBOARD1:def_9; then for n being Element of NAT st n in dom (<*p*> ^ f) & n + 1 in dom (<*p*> ^ f) holds for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & (<*p*> ^ f) /. n = G * (m,k) & (<*p*> ^ f) /. (n + 1) = G * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 by A16, A4, GOBOARD1:24; hence <*p*> ^ f is_sequence_on G by A7, GOBOARD1:def_9; ::_thesis: verum end; theorem Th12: :: JORDAN1F:12 for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT holds Lower_Seq (C,n) is_sequence_on Gauge (C,n) proof let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds Lower_Seq (C,n) is_sequence_on Gauge (C,n) let n be Element of NAT ; ::_thesis: Lower_Seq (C,n) is_sequence_on Gauge (C,n) consider j being Element of NAT such that A1: ( 1 <= j & j <= width (Gauge (C,n)) ) and A2: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by JORDAN1D:25; set E1 = ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1; set i = len (Gauge (C,n)); A3: Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))) by JORDAN1E:def_2 .= <*(E-max (L~ (Cage (C,n))))*> ^ ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by FINSEQ_5:def_2 ; A4: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) is_sequence_on Gauge (C,n) by REVROT_1:34; then A5: (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) is_sequence_on Gauge (C,n) by JORDAN8:2; A6: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (Gauge (C,n)) & [i2,j2] in Indices (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i1,j1) & ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1 = (Gauge (C,n)) * (i2,j2) holds (abs (i2 - i1)) + (abs (j2 - j1)) = 1 proof set en = (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)); let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( [i1,j1] in Indices (Gauge (C,n)) & [i2,j2] in Indices (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i1,j1) & ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1 = (Gauge (C,n)) * (i2,j2) implies (abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) assume A7: ( [i1,j1] in Indices (Gauge (C,n)) & [i2,j2] in Indices (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i1,j1) & ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1 = (Gauge (C,n)) * (i2,j2) ) ; ::_thesis: (abs (i2 - i1)) + (abs (j2 - j1)) = 1 (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by SPRECT_5:16; then ( 1 <= ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 & ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) ) by NAT_1:11, NAT_1:13; then A8: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by FINSEQ_3:25; A9: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43; A10: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32; then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:71; then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A10, SPRECT_2:72, XXREAL_0:2; then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A10, SPRECT_2:73, XXREAL_0:2; then A11: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A10, SPRECT_2:74, XXREAL_0:2; then A12: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by NAT_1:13; A13: (len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) > 0 by SPRECT_5:20, XREAL_1:50; then A14: (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) + ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) >= 0 + 0 ; A15: E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46; then 1 <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by FINSEQ_4:21; then A16: 1 < ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by NAT_1:13; E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A15, FINSEQ_6:90, SPRECT_2:43; then A17: (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_4:21; now__::_thesis:_not_(E-max_(L~_(Cage_(C,n))))_.._(Rotate_((Cage_(C,n)),(W-min_(L~_(Cage_(C,n))))))_=_len_(Rotate_((Cage_(C,n)),(W-min_(L~_(Cage_(C,n)))))) assume (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ; ::_thesis: contradiction then (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = len (Cage (C,n)) by REVROT_1:14; then len (Upper_Seq (C,n)) = len (Cage (C,n)) by JORDAN1E:8; then (len (Cage (C,n))) + (len (Lower_Seq (C,n))) = (len (Cage (C,n))) + 1 by JORDAN1E:10; hence contradiction by JORDAN1E:15; ::_thesis: verum end; then (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A17, XXREAL_0:1; then ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:13; then (1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:9; then 1 <= len ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by A17, RFINSEQ:def_1; then 1 in dom ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by FINSEQ_3:25; then ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + 1) by FINSEQ_5:27 .= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((((len (Cage (C,n))) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1) by A15, A9, A11, SPRECT_5:9 .= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))) + 1) .= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + ((len (Cage (C,n))) -' ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))) + 1) by A13, XREAL_0:def_2 .= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) + ((len (Cage (C,n))) -' ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))) .= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) + ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))) by A13, XREAL_0:def_2 .= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) + (len (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) .= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (((((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) + (len (Cage (C,n)))) -' ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A14, XREAL_0:def_2 ; then A18: ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /^ ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) /. 1 = (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) by A9, A16, A12, REVROT_1:13; ( E-max (L~ (Cage (C,n))) = (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) & (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) in dom (Cage (C,n)) ) by A15, FINSEQ_4:20, FINSEQ_5:38; then (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A4, A7, A8, A18, GOBOARD1:def_9; then (abs (i1 - i2)) + (abs (j2 - j1)) = 1 by UNIFORM1:11; hence (abs (i2 - i1)) + (abs (j2 - j1)) = 1 by UNIFORM1:11; ::_thesis: verum end; len (Gauge (C,n)) >= 4 by JORDAN8:10; then 1 <= len (Gauge (C,n)) by XXREAL_0:2; then [(len (Gauge (C,n))),j] in Indices (Gauge (C,n)) by A1, MATRIX_1:36; hence Lower_Seq (C,n) is_sequence_on Gauge (C,n) by A5, A2, A6, A3, Th11; ::_thesis: verum end; theorem :: JORDAN1F:13 for i being Element of NAT for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) holds ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) ) proof let i be Element of NAT ; ::_thesis: for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) holds ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) ) let C be non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) holds ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) ) let p be Point of (TOP-REAL 2); ::_thesis: ( p `1 = ((W-bound C) + (E-bound C)) / 2 & p `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) implies ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) ) ) assume that A1: p `1 = ((W-bound C) + (E-bound C)) / 2 and A2: p `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) ; ::_thesis: ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) ) percases ( ( L~ (Upper_Seq (C,(i + 1))) = Upper_Arc (L~ (Cage (C,(i + 1)))) & L~ (Lower_Seq (C,(i + 1))) = Lower_Arc (L~ (Cage (C,(i + 1)))) ) or ( L~ (Upper_Seq (C,(i + 1))) = Lower_Arc (L~ (Cage (C,(i + 1)))) & L~ (Lower_Seq (C,(i + 1))) = Upper_Arc (L~ (Cage (C,(i + 1)))) ) ) by Th9; supposeA3: ( L~ (Upper_Seq (C,(i + 1))) = Upper_Arc (L~ (Cage (C,(i + 1)))) & L~ (Lower_Seq (C,(i + 1))) = Lower_Arc (L~ (Cage (C,(i + 1)))) ) ; ::_thesis: ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) ) A4: 1 <= Center (Gauge (C,1)) by JORDAN1B:11; set k = width (Gauge (C,(i + 1))); set l = Center (Gauge (C,(i + 1))); set G = Gauge (C,(i + 1)); set f = Upper_Seq (C,(i + 1)); A5: 1 <= Center (Gauge (C,(i + 1))) by JORDAN1B:11; A6: width (Gauge (C,(i + 1))) = len (Gauge (C,(i + 1))) by JORDAN8:def_1; then width (Gauge (C,(i + 1))) >= 4 by JORDAN8:10; then A7: 1 <= width (Gauge (C,(i + 1))) by XXREAL_0:2; then A8: Center (Gauge (C,(i + 1))) <= len (Gauge (C,(i + 1))) by A6, JORDAN1B:12; then A9: ( [(Center (Gauge (C,(i + 1)))),1] in Indices (Gauge (C,(i + 1))) & [(Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))] in Indices (Gauge (C,(i + 1))) ) by A7, A5, MATRIX_1:36; A10: width (Gauge (C,1)) = len (Gauge (C,1)) by JORDAN8:def_1; then width (Gauge (C,1)) >= 4 by JORDAN8:10; then A11: 1 <= width (Gauge (C,1)) by XXREAL_0:2; then A12: Center (Gauge (C,1)) <= len (Gauge (C,1)) by A10, JORDAN1B:12; A13: (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) c= (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) or a in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) ) A14: Upper_Arc (L~ (Cage (C,(i + 1)))) c= L~ (Cage (C,(i + 1))) by JORDAN6:61; assume A15: a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) ; ::_thesis: a in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) then reconsider a1 = a as Point of (TOP-REAL 2) ; A16: a1 in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1)))))) by A15, XBOOLE_0:def_4; a1 in Upper_Arc (L~ (Cage (C,(i + 1)))) by A3, A15, XBOOLE_0:def_4; then A17: a1 `2 <= N-bound (L~ (Cage (C,(i + 1)))) by A14, PSCOMP_1:24; Cage (C,(i + 1)) is_sequence_on Gauge (C,(i + 1)) by JORDAN9:def_1; then ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `2 >= N-bound (L~ (Cage (C,(i + 1)))) by A6, A7, A5, JORDAN1A:20, JORDAN1B:12; then A18: a1 `2 <= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `2 by A17, XXREAL_0:2; a1 in Upper_Arc (L~ (Cage (C,(i + 1)))) by A3, A15, XBOOLE_0:def_4; then A19: a1 `2 >= S-bound (L~ (Cage (C,(i + 1)))) by A14, PSCOMP_1:24; Cage (C,(i + 1)) is_sequence_on Gauge (C,(i + 1)) by JORDAN9:def_1; then ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `2 <= S-bound (L~ (Cage (C,(i + 1)))) by A6, A7, A5, JORDAN1A:22, JORDAN1B:12; then A20: a1 `2 >= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `2 by A19, XXREAL_0:2; A21: a1 in L~ (Upper_Seq (C,(i + 1))) by A15, XBOOLE_0:def_4; ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 = ((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))) `1 by A11, A12, A4, GOBOARD5:2; then A22: a1 `1 = ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 by A16, GOBOARD7:5 .= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `1 by A6, A10, A7, A11, JORDAN1A:36 ; then a1 `1 = ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `1 by A7, A8, A5, GOBOARD5:2; then a1 in LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))))) by A22, A20, A18, GOBOARD7:7; hence a in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) by A21, XBOOLE_0:def_4; ::_thesis: verum end; 1 <= i + 1 by NAT_1:11; then (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) c= (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) by A6, A10, JORDAN1A:44, XBOOLE_1:26; then A23: (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) = (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1)))) by A13, XBOOLE_0:def_10; LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))))) meets L~ (Upper_Seq (C,(i + 1))) by A3, A6, A7, A5, JORDAN1B:12, JORDAN1B:29; then consider n being Element of NAT such that A24: ( 1 <= n & n <= width (Gauge (C,(i + 1))) ) and A25: ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)) `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Upper_Seq (C,(i + 1)))))) by A7, A9, Th1, Th10; take n ; ::_thesis: ( 1 <= n & n <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n) ) thus ( 1 <= n & n <= width (Gauge (C,(i + 1))) ) by A24; ::_thesis: p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n) len (Gauge (C,1)) >= 4 by JORDAN8:10; then A26: 1 <= len (Gauge (C,1)) by XXREAL_0:2; then p `1 = ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 by A1, JORDAN1A:38 .= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)) `1 by A6, A24, A26, JORDAN1A:36 ; hence p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n) by A2, A3, A25, A23, TOPREAL3:6; ::_thesis: verum end; supposeA27: ( L~ (Upper_Seq (C,(i + 1))) = Lower_Arc (L~ (Cage (C,(i + 1)))) & L~ (Lower_Seq (C,(i + 1))) = Upper_Arc (L~ (Cage (C,(i + 1)))) ) ; ::_thesis: ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) ) A28: 1 <= Center (Gauge (C,1)) by JORDAN1B:11; set k = width (Gauge (C,(i + 1))); set l = Center (Gauge (C,(i + 1))); set G = Gauge (C,(i + 1)); set f = Lower_Seq (C,(i + 1)); A29: 1 <= Center (Gauge (C,(i + 1))) by JORDAN1B:11; A30: width (Gauge (C,(i + 1))) = len (Gauge (C,(i + 1))) by JORDAN8:def_1; then width (Gauge (C,(i + 1))) >= 4 by JORDAN8:10; then A31: 1 <= width (Gauge (C,(i + 1))) by XXREAL_0:2; then A32: Center (Gauge (C,(i + 1))) <= len (Gauge (C,(i + 1))) by A30, JORDAN1B:12; then A33: ( [(Center (Gauge (C,(i + 1)))),1] in Indices (Gauge (C,(i + 1))) & [(Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))] in Indices (Gauge (C,(i + 1))) ) by A31, A29, MATRIX_1:36; A34: width (Gauge (C,1)) = len (Gauge (C,1)) by JORDAN8:def_1; then width (Gauge (C,1)) >= 4 by JORDAN8:10; then A35: 1 <= width (Gauge (C,1)) by XXREAL_0:2; then A36: Center (Gauge (C,1)) <= len (Gauge (C,1)) by A34, JORDAN1B:12; A37: (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) c= (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) or a in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) ) A38: Upper_Arc (L~ (Cage (C,(i + 1)))) c= L~ (Cage (C,(i + 1))) by JORDAN6:61; assume A39: a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) ; ::_thesis: a in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) then reconsider a1 = a as Point of (TOP-REAL 2) ; A40: a1 in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1)))))) by A39, XBOOLE_0:def_4; a1 in Upper_Arc (L~ (Cage (C,(i + 1)))) by A27, A39, XBOOLE_0:def_4; then A41: a1 `2 <= N-bound (L~ (Cage (C,(i + 1)))) by A38, PSCOMP_1:24; Cage (C,(i + 1)) is_sequence_on Gauge (C,(i + 1)) by JORDAN9:def_1; then ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `2 >= N-bound (L~ (Cage (C,(i + 1)))) by A30, A31, A29, JORDAN1A:20, JORDAN1B:12; then A42: a1 `2 <= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `2 by A41, XXREAL_0:2; a1 in Upper_Arc (L~ (Cage (C,(i + 1)))) by A27, A39, XBOOLE_0:def_4; then A43: a1 `2 >= S-bound (L~ (Cage (C,(i + 1)))) by A38, PSCOMP_1:24; Cage (C,(i + 1)) is_sequence_on Gauge (C,(i + 1)) by JORDAN9:def_1; then ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `2 <= S-bound (L~ (Cage (C,(i + 1)))) by A30, A31, A29, JORDAN1A:22, JORDAN1B:12; then A44: a1 `2 >= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `2 by A43, XXREAL_0:2; A45: a1 in L~ (Lower_Seq (C,(i + 1))) by A39, XBOOLE_0:def_4; ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 = ((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))) `1 by A35, A36, A28, GOBOARD5:2; then A46: a1 `1 = ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 by A40, GOBOARD7:5 .= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)) `1 by A30, A34, A31, A35, JORDAN1A:36 ; then a1 `1 = ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `1 by A31, A32, A29, GOBOARD5:2; then a1 in LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))))) by A46, A44, A42, GOBOARD7:7; hence a in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) by A45, XBOOLE_0:def_4; ::_thesis: verum end; 1 <= i + 1 by NAT_1:11; then (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) c= (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) by A30, A34, JORDAN1A:44, XBOOLE_1:26; then A47: (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) = (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1)))) by A37, XBOOLE_0:def_10; LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1))))))) meets L~ (Lower_Seq (C,(i + 1))) by A27, A30, A31, A29, JORDAN1B:12, JORDAN1B:29; then consider n being Element of NAT such that A48: ( 1 <= n & n <= width (Gauge (C,(i + 1))) ) and A49: ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)) `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))))) /\ (L~ (Lower_Seq (C,(i + 1)))))) by A31, A33, Th1, Th12; take n ; ::_thesis: ( 1 <= n & n <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n) ) thus ( 1 <= n & n <= width (Gauge (C,(i + 1))) ) by A48; ::_thesis: p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n) len (Gauge (C,1)) >= 4 by JORDAN8:10; then A50: 1 <= len (Gauge (C,1)) by XXREAL_0:2; then p `1 = ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 by A1, JORDAN1A:38 .= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)) `1 by A30, A48, A50, JORDAN1A:36 ; hence p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n) by A2, A27, A49, A47, TOPREAL3:6; ::_thesis: verum end; end; end;