:: Some Remarks on Finite Sequences on Go-boards :: by Adam Naumowicz :: :: Received August 29, 2001 :: Copyright (c) 2001-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD1, RLTOPSP1, RELAT_1, XBOOLE_0, TOPREAL1, MATRIX_1, XXREAL_0, MCART_1, RCOMP_1, PSCOMP_1, PRE_TOPC, TREES_1, TARSKI, ARYTM_3, PARTFUN1, COMPLEX1, ARYTM_1, CARD_1, SPPOL_1, JORDAN1E, JORDAN9, FINSEQ_6, FINSEQ_5, FINSEQ_4, JORDAN6, TOPREAL2, RELAT_2, JORDAN8, ORDINAL4, FUNCT_1, NAT_1, RFINSEQ, JORDAN1A, SEQ_4; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, COMPLEX1, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, FINSEQ_6, MATRIX_0, SEQ_4, STRUCT_0, PRE_TOPC, COMPTS_1, CONNSP_1, RFINSEQ, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD1, SPPOL_1, PSCOMP_1, JORDAN6, JORDAN8, JORDAN9, JORDAN1A, JORDAN1E; constructors REAL_1, FINSEQ_4, NEWTON, RFINSEQ, FINSEQ_5, CONNSP_1, JORDAN5C, JORDAN6, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, NAT_D, SEQ_4, RELSET_1, PSCOMP_1; registrations XBOOLE_0, RELSET_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_6, STRUCT_0, SPPOL_2, SPRECT_1, SPRECT_2, TOPREAL6, JORDAN8, JORDAN1A, JORDAN1E, FUNCT_1, EUCLID, PSCOMP_1, ORDINAL1; requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM; definitions TARSKI; equalities STRUCT_0, PSCOMP_1; theorems JORDAN8, NAT_1, GOBOARD7, GOBOARD5, SPRECT_3, ABSVALUE, GOBOARD1, JORDAN6, PSCOMP_1, TARSKI, TOPREAL3, SPRECT_2, FINSEQ_6, RELAT_1, FINSEQ_5, TOPREAL1, PRE_TOPC, JORDAN5B, FINSEQ_1, JORDAN1E, JORDAN1A, REVROT_1, JORDAN9, JORDAN1B, FINSEQ_3, UNIFORM1, FINSEQ_4, JORDAN1D, SPRECT_5, RFINSEQ, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, EUCLID, PARTFUN1, MATRIX_0, XREAL_0; begin reserve i,j,k,m,n for Nat, f for FinSequence of the carrier of TOP-REAL 2, G for Go-board; theorem Th1: 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 st j <= n & n <= k & G*(i, n)`2 = lower_bound(proj2.:(LSeg(G*(i,j),G*(i,k)) /\ L~f)) proof 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; A6: 1 <= i & i <= len G by A3,MATRIX_0:32; ex x being object st x in LSeg(G*(i,j),G*(i,k)) & x in L~f by A2,XBOOLE_0:3; then reconsider X1=X as non empty compact Subset of TOP-REAL 2 by XBOOLE_0:def 4; consider p being object such that A7: p in S-most X1 by XBOOLE_0:def 1; reconsider p as Point of TOP-REAL 2 by A7; A8: p in X by A7,XBOOLE_0:def 4; then A9: p in LSeg(G*(i,j),G*(i,k)) by XBOOLE_0:def 4; proj2.:X = (proj2|X).:X by RELAT_1:129; then A10: lower_bound(proj2.:X) = lower_bound((proj2|X).: [#]((TOP-REAL 2)|X)) by PRE_TOPC:def 5 .= S-bound X; A11: 1 <= k by A4,MATRIX_0:32; A12: p`2 = (S-min X)`2 by A7,PSCOMP_1:55 .= lower_bound(proj2.:X) by A10,EUCLID:52; A13: 1 <= i & i <= len G by A3,MATRIX_0:32; A14: 1 <= j by A3,MATRIX_0:32; A15: k <= width G by A4,MATRIX_0:32; 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_0:32; 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 Nat : 1 <= k1 & k1+1 <= len f} by TOPREAL1:def 4; then consider Y being set such that A21: p in Y and A22: Y in { LSeg(f,k1) where k1 is Nat : 1 <= k1 & k1+1 <= len f} by TARSKI:def 4; consider i1 being Nat such that A23: Y = LSeg(f,i1) and A24: 1 <= i1 and A25: i1+1 <= len f by A22; A26: p in LSeg(f/.i1,f/.(i1+1)) by A21,A23,A24,A25,TOPREAL1:def 3; 1 < i1+1 by A24,NAT_1:13; then i1+1 in Seg len f by A25,FINSEQ_1:1; then A27: i1+1 in dom f by FINSEQ_1:def 3; then consider io,jo being 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_0:32; A31: 1 <= jo by A28,MATRIX_0:32; i1 <= len f by A25,NAT_1:13; then i1 in Seg len f by A24,FINSEQ_1:1; then A32: i1 in dom f by FINSEQ_1:def 3; then consider i0,j0 being 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_0:32; A36: 1 <= j0 by A33,MATRIX_0:32; A37: j0 <= width G by A33,MATRIX_0:32; A38: jo <= width G by A28,MATRIX_0:32; A39: f is special by A1,A32,JORDAN8:4,RELAT_1:38; ex n st j <= n & n <= k & G*(i,n) = p proof per cases by A24,A25,A39,TOPREAL1:def 5; suppose A40: (f/.i1)`1 = (f/.(i1+1))`1; 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 thesis proof per cases; suppose A43: (f/.i1)`2 <= (f/.(i1+1))`2; thus thesis proof per cases; suppose A44: (f/.i1) in LSeg(G*(i,j),G*(i,k)); 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; 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; G*(i,n)`2 <= G*(i,k) `2 by A46,A47,A48,TOPREAL1:4; hence n <= k by A13,A11,A37,GOBOARD5:4; 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 thesis by A47,TOPREAL3:6; end; suppose A49: not f/.i1 in LSeg(G*(i,j),G*(i,k)); A50: (f/.i1)`1 = p`1 by A26,A40,GOBOARD7:5 .= G*(i,j)`1 by A20,A9,GOBOARD7:5; thus thesis proof per cases by A20,A49,A50,GOBOARD7:7; suppose A51: (f/.i1)`2 < G*(i,j)`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 G*(i,j)`2 <= G*(i,jo)`2 by A17,XXREAL_0:2; then A52: j<=jo by A6,A19,A31,GOBOARD5:4; |.i0-io.|+|.j0-jo.| = 1 by A1,A32,A27,A33,A34,A28,A29, GOBOARD1:def 9; then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2; then A53: |.-(j0-jo).| = 1 by COMPLEX1:52; j0<=jo+0 by 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 G*(i,k)`2; p`2 >= (f/.i1)`2 by A26,A43,TOPREAL1:4; hence thesis by A18,A57,XXREAL_0:2; end; end; end; end; end; suppose A58: (f/.i1)`2 > (f/.(i1+1))`2; thus thesis proof per cases; suppose A59: (f/.(i1+1)) in LSeg(G*(i,j),G*(i,k)); 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; 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; G*(i,n)`2 <= G*(i,k) `2 by A61,A62,A63,TOPREAL1:4; hence n <= k by A13,A11,A38,GOBOARD5:4; 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 thesis by A62,TOPREAL3:6; end; suppose A64: not f/.(i1+1) in LSeg(G*(i,j),G*(i,k)); A65: (f/.(i1+1))`1 = p`1 by A26,A40,GOBOARD7:5 .= G*(i,j)`1 by A20,A9,GOBOARD7:5; thus thesis proof per cases by A20,A64,A65,GOBOARD7:7; suppose A66: (f/.(i1+1))`2 < G*(i,j)`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 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; |.i0-io.|+|.j0-jo.| = 1 by A1,A32,A27,A33,A34,A28,A29, GOBOARD1:def 9; then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2; then j0-jo = 1 by A68,ABSVALUE:def 1; then A69: jo+1=j0-0; G*(i,jo)`2 < G*(i,j)`2 & jo<=j by A29,A6,A14,A38,A41,A66, GOBOARD5:4 ; then jo G*(i,k)`2; p`2 >= (f/.(i1+1))`2 by A26,A58,TOPREAL1:4; hence thesis by A18,A72,XXREAL_0:2; end; end; end; end; end; end; end; suppose A73: (f/.i1)`2 = (f/.(i1+1))`2; take n=j0; 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; G*(i,n)`2 <= G*(i,k)`2 by A9,A74,A75,TOPREAL1:4; hence n <= k by A13,A11,A37,GOBOARD5:4; 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 thesis by A74,TOPREAL3:6; end; end; hence thesis by A12; end; theorem 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 st j <= n & n <= k & G*(i, n)`2 = upper_bound(proj2.:(LSeg(G*(i,j),G*(i,k)) /\ L~f)) proof 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; A6: 1 <= i & i <= len G by A3,MATRIX_0:32; ex x being object st x in LSeg(G*(i,j),G*(i,k)) & x in L~f by A2,XBOOLE_0:3; then reconsider X1=X as non empty compact Subset of TOP-REAL 2 by XBOOLE_0:def 4; consider p being object such that A7: p in N-most X1 by XBOOLE_0:def 1; reconsider p as Point of TOP-REAL 2 by A7; A8: p in X 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 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 Nat : 1 <= k1 & k1+1 <= len f} by TARSKI:def 4; consider i1 being 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.:X = (proj2|X).:X by RELAT_1:129; then A16: upper_bound(proj2.:X) = upper_bound((proj2|X).: [#]((TOP-REAL 2)|X)) by PRE_TOPC:def 5 .= N-bound X; A17: 1 <= k by A4,MATRIX_0:32; A18: 1 <= j by A3,MATRIX_0:32; 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 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_0:32; A23: 1 <= jo by A20,MATRIX_0:32; A24: p`2 = (N-min X)`2 by A7,PSCOMP_1:39 .= upper_bound(proj2.:X) by A16,EUCLID:52; A25: 1 <= i & i <= len G by A3,MATRIX_0:32; A26: k <= width G by A4,MATRIX_0:32; 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_0:32; 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_0:32; 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 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_0:32; A37: 1 <= j0 by A34,MATRIX_0:32; A38: j0 <= width G by A34,MATRIX_0:32; A39: f is special by A1,A33,JORDAN8:4,RELAT_1:38; ex n st j <= n & n <= k & G*(i,n) = p proof per cases by A13,A14,A39,TOPREAL1:def 5; suppose A40: (f/.i1)`1 = (f/.(i1+1))`1; 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 thesis proof per cases; suppose A43: (f/.i1)`2 <= (f/.(i1+1))`2; thus thesis proof per cases; suppose A44: (f/.(i1+1)) in LSeg(G*(i,j),G*(i,k)); 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; 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; G*(i,n)`2 <= G*(i,k) `2 by A46,A47,A48,TOPREAL1:4; hence n <= k by A25,A17,A32,GOBOARD5:4; 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 thesis by A47,TOPREAL3:6; end; suppose A49: not f/.(i1+1) in LSeg(G*(i,j),G*(i,k)); A50: (f/.(i1+1))`1 = p`1 by A15,A40,GOBOARD7:5 .= G*(i,j)`1 by A31,A9,GOBOARD7:5; thus thesis proof per cases by A31,A49,A50,GOBOARD7:7; suppose A51: (f/.(i1+1))`2 > G*(i,k)`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 G*(i,k)`2 >= G*(i,j0)`2 by A29,XXREAL_0:2; then A52: k>=j0 by A25,A17,A38,GOBOARD5:4; |.i0-io.|+|.j0-jo.| = 1 by A1,A33,A19,A34,A35,A20,A21, GOBOARD1:def 9; then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2; then A53: |.-(j0-jo).| = 1 by COMPLEX1:52; j0<=jo+0 by 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; 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 thesis by A5,A55,A56,TOPREAL3:6; end; suppose A57: (f/.(i1+1))`2 < G*(i,j)`2; p`2 <= (f/.(i1+1))`2 by A15,A43,TOPREAL1:4; hence thesis by A28,A57,XXREAL_0:2; end; end; end; end; end; suppose A58: (f/.i1)`2 > (f/.(i1+1))`2; thus thesis proof per cases; suppose A59: f/.i1 in LSeg(G*(i,j),G*(i,k)); 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; 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; G*(i,n)`2 <= G*(i,k) `2 by A61,A62,A63,TOPREAL1:4; hence n <= k by A25,A17,A38,GOBOARD5:4; 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 thesis by A62,TOPREAL3:6; end; suppose A64: not f/.i1 in LSeg(G*(i,j),G*(i,k)); A65: (f/.i1)`1 = p`1 by A15,A40,GOBOARD7:5 .= G*(i,j)`1 by A31,A9,GOBOARD7:5; thus thesis proof per cases by A31,A64,A65,GOBOARD7:7; suppose A66: (f/.i1)`2 > G*(i,k)`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 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; |.i0-io.|+|.j0-jo.| = 1 by A1,A33,A19,A34,A35,A20,A21, GOBOARD1:def 9; then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2; then j0-jo = 1 by A68,ABSVALUE:def 1; then A69: jo+1=j0-0; G*(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; 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 thesis by A5,A70,A71,TOPREAL3:6; end; suppose A72: (f/.i1)`2 < G*(i,j)`2; p`2 <= (f/.i1)`2 by A15,A58,TOPREAL1:4; hence thesis by A28,A72,XXREAL_0:2; end; end; end; end; end; end; end; suppose A73: (f/.i1)`2 = (f/.(i1+1))`2; take n=j0; 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; G*(i,n)`2 <= G*(i,k)`2 by A9,A74,A75,TOPREAL1:4; hence n <= k by A25,A17,A38,GOBOARD5:4; 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 thesis by A74,TOPREAL3:6; end; end; hence thesis by A24; end; theorem 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 st j <= n & n <= k & G*(n, i)`1 = lower_bound(proj1.:(LSeg(G*(j,i),G*(k,i)) /\ L~f)) proof 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; A6: 1 <= j by A3,MATRIX_0:32; ex x being object st x in LSeg(G*(j,i),G*(k,i)) & x in L~f by A2,XBOOLE_0:3; then reconsider X1=X as non empty compact Subset of TOP-REAL 2 by XBOOLE_0:def 4; consider p being object such that A7: p in W-most X1 by XBOOLE_0:def 1; reconsider p as Point of TOP-REAL 2 by A7; A8: p in X by A7,XBOOLE_0:def 4; then A9: p in LSeg(G*(j,i),G*(k,i)) by XBOOLE_0:def 4; proj1.:X = (proj1|X).:X by RELAT_1:129; then A10: lower_bound(proj1.:X) = lower_bound((proj1|X).: [#]((TOP-REAL 2)|X)) by PRE_TOPC:def 5 .= W-bound X; A11: 1 <= k & 1 <= i by A4,MATRIX_0:32; A12: p`1 = (W-min X)`1 by A7,PSCOMP_1:31 .= lower_bound(proj1.:X) by A10,EUCLID:52; A13: i <= width G by A3,MATRIX_0:32; A14: 1 <= i & i <= width G by A3,MATRIX_0:32; A15: k <= len G by A4,MATRIX_0:32; then A16: G*(j,i)`1 <= G*(k,i)`1 by A5,A6,A14,SPRECT_3:13; then A17: G*(j,i)`1 <= p`1 by A9,TOPREAL1:3; A18: p`1 <= G*(k,i)`1 by A9,A16,TOPREAL1:3; A19: j <= len G by A3,MATRIX_0:32; then A20: G*(j,i)`2 = G*(1,i)`2 by A6,A14,GOBOARD5:1 .= G*(k,i)`2 by A15,A11,A13,GOBOARD5:1; p in L~f by A8,XBOOLE_0:def 4; then p in union { LSeg(f,k1) where k1 is Nat : 1 <= k1 & k1+1 <= len f} by TOPREAL1:def 4; then consider Y being set such that A21: p in Y and A22: Y in { LSeg(f,k1) where k1 is Nat : 1 <= k1 & k1+1 <= len f} by TARSKI:def 4; consider i1 being Nat such that A23: Y = LSeg(f,i1) and A24: 1 <= i1 and A25: i1+1 <= len f by A22; A26: p in LSeg(f/.i1,f/.(i1+1)) by A21,A23,A24,A25,TOPREAL1:def 3; 1 < i1+1 by A24,NAT_1:13; then i1+1 in Seg len f by A25,FINSEQ_1:1; then A27: i1+1 in dom f by FINSEQ_1:def 3; then consider jo,io being Nat such that A28: [jo,io] in Indices G and A29: f/.(i1+1) = G*(jo,io) by A1,GOBOARD1:def 9; A30: 1 <= jo by A28,MATRIX_0:32; i1 <= len f by A25,NAT_1:13; then i1 in Seg len f by A24,FINSEQ_1:1; then A31: i1 in dom f by FINSEQ_1:def 3; then consider j0,i0 being Nat such that A32: [j0,i0] in Indices G and A33: f/.i1 = G*(j0,i0) by A1,GOBOARD1:def 9; A34: 1 <= j0 by A32,MATRIX_0:32; A35: 1 <= i0 & i0 <= width G by A32,MATRIX_0:32; A36: j0 <= len G by A32,MATRIX_0:32; A37: 1 <= io & io <= width G by A28,MATRIX_0:32; A38: jo <= len G by A28,MATRIX_0:32; A39: f is special by A1,A31,JORDAN8:4,RELAT_1:38; ex n st j <= n & n <= k & G*(n,i) = p proof per cases by A24,A25,A39,TOPREAL1:def 5; suppose A40: (f/.i1)`2 = (f/.(i1+1))`2; 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 thesis proof per cases; suppose A43: (f/.i1)`1 <= (f/.(i1+1))`1; thus thesis proof per cases; suppose A44: (f/.i1) in LSeg(G*(j,i),G*(k,i)); 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; 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; G*(n,i)`1 <= G*(k,i) `1 by A46,A47,A48,TOPREAL1:3; hence n <= k by A11,A13,A36,GOBOARD5:3; 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 thesis by A47,TOPREAL3:6; end; suppose A49: not f/.i1 in LSeg(G*(j,i),G*(k,i)); A50: (f/.i1)`2 = p`2 by A26,A40,GOBOARD7:6 .= G*(j,i)`2 by A20,A9,GOBOARD7:6; thus thesis proof per cases by A20,A49,A50,GOBOARD7:8; suppose A51: (f/.i1)`1 < G*(j,i)`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 G*(j,i)`1 <= G*(jo,i)`1 by A17,XXREAL_0:2; then A52: j<=jo by A19,A14,A30,GOBOARD5:3; |.i0-io.|+|.j0-jo.| = 1 by A1,A31,A27,A32,A33,A28,A29, GOBOARD1:def 9; then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2; then A53: |.-(j0-jo).| = 1 by COMPLEX1:52; j0<=jo+0 by A33,A29,A36,A35,A30,A42,A41,A43,GOBOARD5:3; then j0-jo <= 0 by XREAL_1:20; then jo-j0 = 1 by A53,ABSVALUE:def 1; then A54: j0+1=jo+0; G*(j0,i)`1 < G*(j,i)`1 & j0<=j by A33,A6,A14,A36,A42,A51, GOBOARD5:3 ; then j0 G*(k,i)`1; p`1 >= (f/.i1)`1 by A26,A43,TOPREAL1:3; hence thesis by A18,A57,XXREAL_0:2; end; end; end; end; end; suppose A58: (f/.i1)`1 > (f/.(i1+1))`1; thus thesis proof per cases; suppose A59: (f/.(i1+1)) in LSeg(G*(j,i),G*(k,i)); 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; 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; G*(n,i)`1 <= G*(k,i) `1 by A61,A62,A63,TOPREAL1:3; hence n <= k by A11,A13,A38,GOBOARD5:3; 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 thesis by A62,TOPREAL3:6; end; suppose A64: not f/.(i1+1) in LSeg(G*(j,i),G*(k,i)); A65: (f/.(i1+1))`2 = p`2 by A26,A40,GOBOARD7:6 .= G*(j,i)`2 by A20,A9,GOBOARD7:6; thus thesis proof per cases by A20,A64,A65,GOBOARD7:8; suppose A66: (f/.(i1+1))`1 < G*(j,i)`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 G*(j,i)`1 <= G*(j0,i)`1 by A17,XXREAL_0:2; then A67: j<=j0 by A19,A14,A34,GOBOARD5:3; jo<=j0+0 by A33,A29,A34,A35,A38,A42,A41,A58,GOBOARD5:3; then jo-j0 <= 0 by XREAL_1:20; then A68: -(jo-j0) >= -0; |.i0-io.|+|.j0-jo.| = 1 by A1,A31,A27,A32,A33,A28,A29, GOBOARD1:def 9; then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2; then j0-jo = 1 by A68,ABSVALUE:def 1; then A69: jo+1=j0-0; G*(jo,i)`1 < G*(j,i)`1 & jo<=j by A29,A6,A14,A38,A41,A66, GOBOARD5:3 ; then jo G*(k,i)`1; p`1 >= (f/.(i1+1))`1 by A26,A58,TOPREAL1:3; hence thesis by A18,A72,XXREAL_0:2; end; end; end; end; end; end; end; suppose A73: (f/.i1)`1 = (f/.(i1+1))`1; take n=j0; 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; G*(n,i)`1 <= G*(k,i)`1 by A9,A74,A75,TOPREAL1:3; hence n <= k by A11,A13,A36,GOBOARD5:3; 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 thesis by A74,TOPREAL3:6; end; end; hence thesis by A12; end; theorem 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 st j <= n & n <= k & G*(n, i)`1 = upper_bound(proj1.:(LSeg(G*(j,i),G*(k,i)) /\ L~f)) proof 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; A6: 1 <= j by A3,MATRIX_0:32; ex x being object st x in LSeg(G*(j,i),G*(k,i)) & x in L~f by A2,XBOOLE_0:3; then reconsider X1=X as non empty compact Subset of TOP-REAL 2 by XBOOLE_0:def 4; consider p being object such that A7: p in E-most X1 by XBOOLE_0:def 1; reconsider p as Point of TOP-REAL 2 by A7; A8: p in X by A7,XBOOLE_0:def 4; then A9: p in LSeg(G*(j,i),G*(k,i)) by XBOOLE_0:def 4; proj1.:X = (proj1|X).:X by RELAT_1:129; then A10: upper_bound(proj1.:X) = upper_bound((proj1|X).: [#]((TOP-REAL 2)|X)) by PRE_TOPC:def 5 .= E-bound X; A11: 1 <= i & i <= width G by A3,MATRIX_0:32; A12: p`1 = (E-min X)`1 by A7,PSCOMP_1:47 .= upper_bound(proj1.:X) by A10,EUCLID:52; A13: 1 <= k by A4,MATRIX_0:32; A14: 1 <= i & i <= width G by A3,MATRIX_0:32; A15: k <= len G by A4,MATRIX_0:32; then A16: G*(j,i)`1 <= G*(k,i)`1 by A5,A6,A14,SPRECT_3:13; then A17: G*(j,i)`1 <= p`1 by A9,TOPREAL1:3; A18: p`1 <= G*(k,i)`1 by A9,A16,TOPREAL1:3; A19: j <= len G by A3,MATRIX_0:32; then A20: G*(j,i)`2 = G*(1,i)`2 by A6,A14,GOBOARD5:1 .= G*(k,i)`2 by 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 Nat : 1 <= k1 & k1+1 <= len f} by TOPREAL1:def 4; then consider Y being set such that A21: p in Y and A22: Y in { LSeg(f,k1) where k1 is Nat : 1 <= k1 & k1+1 <= len f} by TARSKI:def 4; consider i1 being Nat such that A23: Y = LSeg(f,i1) and A24: 1 <= i1 and A25: i1+1 <= len f by A22; A26: p in LSeg(f/.i1,f/.(i1+1)) by A21,A23,A24,A25,TOPREAL1:def 3; 1 < i1+1 by A24,NAT_1:13; then i1+1 in Seg len f by A25,FINSEQ_1:1; then A27: i1+1 in dom f by FINSEQ_1:def 3; then consider jo,io being Nat such that A28: [jo,io] in Indices G and A29: f/.(i1+1) = G*(jo,io) by A1,GOBOARD1:def 9; A30: 1 <= jo by A28,MATRIX_0:32; i1 <= len f by A25,NAT_1:13; then i1 in Seg len f by A24,FINSEQ_1:1; then A31: i1 in dom f by FINSEQ_1:def 3; then consider j0,i0 being Nat such that A32: [j0,i0] in Indices G and A33: f/.i1 = G*(j0,i0) by A1,GOBOARD1:def 9; A34: 1 <= j0 by A32,MATRIX_0:32; A35: 1 <= i0 & i0 <= width G by A32,MATRIX_0:32; A36: j0 <= len G by A32,MATRIX_0:32; A37: 1 <= io & io <= width G by A28,MATRIX_0:32; A38: jo <= len G by A28,MATRIX_0:32; A39: f is special by A1,A31,JORDAN8:4,RELAT_1:38; ex n st j <= n & n <= k & G*(n,i) = p proof per cases by A24,A25,A39,TOPREAL1:def 5; suppose A40: (f/.i1)`2 = (f/.(i1+1))`2; 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 thesis proof per cases; suppose A43: (f/.i1)`1 <= (f/.(i1+1))`1; thus thesis proof per cases; suppose A44: (f/.(i1+1)) in LSeg(G*(j,i),G*(k,i)); 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; 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; G*(n,i)`1 <= G*(k,i) `1 by A46,A47,A48,TOPREAL1:3; hence n <= k by A13,A11,A38,GOBOARD5:3; 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 thesis by A47,TOPREAL3:6; end; suppose A49: not f/.(i1+1) in LSeg(G*(j,i),G*(k,i)); A50: (f/.(i1+1))`2 = p`2 by A26,A40,GOBOARD7:6 .= G*(j,i)`2 by A20,A9,GOBOARD7:6; thus thesis proof per cases by A20,A49,A50,GOBOARD7:8; suppose A51: (f/.(i1+1))`1 > G*(k,i)`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 G*(k,i)`1 >= G*(j0,i)`1 by A18,XXREAL_0:2; then A52: k>=j0 by A13,A11,A36,GOBOARD5:3; |.i0-io.|+|.j0-jo.| = 1 by A1,A31,A27,A32,A33,A28,A29, GOBOARD1:def 9; then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2; then A53: |.-(j0-jo).| = 1 by COMPLEX1:52; j0<=jo+0 by A33,A29,A36,A35,A30,A42,A41,A43,GOBOARD5:3; then j0-jo <= 0 by XREAL_1:20; then jo-j0 = 1 by A53,ABSVALUE:def 1; then A54: j0+1=jo+0; G*(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; 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 thesis by A5,A55,A56,TOPREAL3:6; end; suppose A57: (f/.(i1+1))`1 < G*(j,i)`1; p`1 <= (f/.(i1+1))`1 by A26,A43,TOPREAL1:3; hence thesis by A17,A57,XXREAL_0:2; end; end; end; end; end; suppose A58: (f/.i1)`1 > (f/.(i1+1))`1; thus thesis proof per cases; suppose A59: f/.i1 in LSeg(G*(j,i),G*(k,i)); 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; 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; G*(n,i)`1 <= G*(k,i) `1 by A61,A62,A63,TOPREAL1:3; hence n <= k by A13,A11,A36,GOBOARD5:3; 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 thesis by A62,TOPREAL3:6; end; suppose A64: not f/.i1 in LSeg(G*(j,i),G*(k,i)); A65: (f/.i1)`2 = p`2 by A26,A40,GOBOARD7:6 .= G*(j,i)`2 by A20,A9,GOBOARD7:6; thus thesis proof per cases by A20,A64,A65,GOBOARD7:8; suppose A66: (f/.i1)`1 > G*(k,i)`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 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; |.i0-io.|+|.j0-jo.| = 1 by A1,A31,A27,A32,A33,A28,A29, GOBOARD1:def 9; then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2; then j0-jo = 1 by A68,ABSVALUE:def 1; then A69: jo+1=j0-0; G*(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; 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 thesis by A5,A70,A71,TOPREAL3:6; end; suppose A72: (f/.i1)`1 < G*(j,i)`1; p`1 <= (f/.i1)`1 by A26,A58,TOPREAL1:3; hence thesis by A17,A72,XXREAL_0:2; end; end; end; end; end; end; end; suppose A73: (f/.i1)`1 = (f/.(i1+1))`1; take n=j0; 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; G*(n,i)`1 <= G*(k,i)`1 by A9,A74,A75,TOPREAL1:3; hence n <= k by A13,A11,A36,GOBOARD5:3; 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 thesis by A74,TOPREAL3:6; end; end; hence thesis by A12; end; theorem Th5: for C being compact non vertical non horizontal Subset of TOP-REAL 2 for n being Nat holds Upper_Seq(C,n)/.1 = W-min(L~Cage(C, n)) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; 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 thesis by FINSEQ_6:92; end; theorem Th6: for C be compact non vertical non horizontal Subset of TOP-REAL 2 for n be Nat holds Lower_Seq(C,n)/.1 = E-max L~Cage(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; 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 thesis by FINSEQ_5:53; end; theorem Th7: for C being compact non vertical non horizontal Subset of TOP-REAL 2 for n being Nat holds Upper_Seq(C,n)/. len Upper_Seq(C,n) = E-max(L~Cage(C,n)) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; 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 thesis by A1,FINSEQ_5:45,SPRECT_2:46; end; theorem Th8: for C be compact non vertical non horizontal Subset of TOP-REAL 2 for n be Nat holds Lower_Seq(C,n)/.(len Lower_Seq(C,n)) = W-min L~ Cage(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; 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; end; theorem Th9: for C being compact non vertical non horizontal Subset of TOP-REAL 2 for n being 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 vertical non horizontal Subset of TOP-REAL 2; let n be Nat; 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 WC,EC & Upper_Arc(L~Cage(C,n)) \/ Lower_Arc(L~Cage(C,n))=L~Cage(C,n) by JORDAN6:50; Upper_Seq(C,n)/.1 = WC & Upper_Seq(C,n)/. len Upper_Seq(C,n) = EC by Th5,Th7; then A2: L~Upper_Seq(C,n) is_an_arc_of WC,EC by TOPREAL1:25; Lower_Seq(C,n)/.1 = EC & Lower_Seq(C,n)/. len Lower_Seq(C,n) = WC by Th6,Th8; then A3: L~Lower_Seq(C,n) is_an_arc_of WC,EC 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 WC,EC by JORDAN1E:13,JORDAN6:50; hence thesis by A2,A3,A1,JORDAN6:48; end; reserve C for compact non vertical non horizontal non empty being_simple_closed_curve Subset of TOP-REAL 2, p for Point of TOP-REAL 2, i1, j1,i2,j2 for Nat; theorem Th10: for C being connected compact non vertical non horizontal Subset of TOP-REAL 2 for n being Nat holds Upper_Seq(C,n) is_sequence_on Gauge(C,n) proof let C be connected compact non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; 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 thesis by A1,GOBOARD1:22; end; theorem Th11: :: symmetric to JORDAN8:9 for f being FinSequence of TOP-REAL 2 st f is_sequence_on G & ( ex i,j st [i,j] in Indices G & p = G*(i,j)) & (for i1,j1,i2,j2 st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G*(i1,j1) & f/.1 = G*(i2,j2) holds |.i2-i1.|+|.j2-j1.| = 1) holds <*p*>^f is_sequence_on G proof let f be FinSequence of TOP-REAL 2 such that A1: f is_sequence_on G and A2: ex i,j st [i,j] in Indices G & p = G*(i,j) and A3: for i1,j1,i2,j2 st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G*(i1,j1) & f/.1 = G*(i2,j2) holds |.i2-i1.|+|.j2-j1.| = 1; A4: now let m,k,i,j such 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; 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 |.i-m.|+|.j-k.|=1 by A3,A5; hence 1 = |.m-i.|+|.j-k.| by UNIFORM1:11 .= |.m-i.|+|.k-j.| by UNIFORM1:11; end; A7: now let n such that A8: n in dom(<*p*>^f); per cases by A8,FINSEQ_1:25; suppose A9: n in dom <*p*>; consider i,j such that A10: [i,j] in Indices G and A11: p = G*(i,j) by A2; take i,j; thus [i,j] in Indices G by A10; 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; end; suppose ex l be Nat st l in dom f & n = (len <*p*>) + l; then consider l be Nat such that A12: l in dom f and A13: n = (len <*p*>) + l; consider i,j such that A14: [i,j] in Indices G and A15: f/.l = G*(i,j) by A1,A12,GOBOARD1:def 9; take i,j; thus [i,j] in Indices G by A14; thus (<*p*>^f)/.n = G*(i,j) by A12,A13,A15,FINSEQ_4:69; end; end; A16: now let n; assume that A17: n in dom <*p*> and A18: n+1 in dom <*p*>; 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 st [m,k] in Indices G & [i,j] in Indices G & <*p*>/.n=G*( m,k) & <*p*>/.(n+1)=G*(i,j) holds |.m-i.|+|.k-j.|=1 by A19,XXREAL_0:2; end; for n st n in dom f & n+1 in dom f holds for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G & f/.n=G*(m,k) & f/.(n+1)=G*(i,j) holds |.m-i.|+|.k-j.|=1 by A1,GOBOARD1:def 9; then for n st n in dom(<*p*>^f) & n+1 in dom(<*p*>^f) holds for m,k,i,j 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 |.m-i.|+|.k-j.|=1 by A16,A4,GOBOARD1:24; hence thesis by A7,GOBOARD1:def 9; end; theorem Th12: for C being connected compact non vertical non horizontal Subset of TOP-REAL 2 for n being Nat holds Lower_Seq(C,n) is_sequence_on Gauge(C,n) proof let C be connected compact non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; consider j 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 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) & E1 = Gauge(C,n)*(i2,j2) holds |.i2-i1.|+|.j2-j1.| = 1 proof set en = (E-max L~Cage(C,n))..Cage(C,n); let i1,j1,i2,j2; 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) & E1 = Gauge(C,n)*(i2,j2); en < len Cage(C,n) by SPRECT_5:16; then 1<=en+1 & en+1 <= len Cage(C,n) by NAT_1:11,13; then A8: en+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 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))); then (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) = len Cage (C,n) by FINSEQ_6:179; 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; 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 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) 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: E1=Cage(C,n)/.(en+1) by A9,A16,A12,FINSEQ_6:178; E-max L~Cage(C,n)=Cage(C,n)/.en & en in dom Cage(C,n) by A15,FINSEQ_4:20 ,FINSEQ_5:38; then |.i1-i2.|+|.j1-j2.| = 1 by A4,A7,A8,A18,GOBOARD1:def 9; then |.i1-i2.|+|.j2-j1.| = 1 by UNIFORM1:11; hence thesis by UNIFORM1:11; end; i >=4 by JORDAN8:10; then 1<=i by XXREAL_0:2; then [i,j] in Indices Gauge(C,n) by A1,MATRIX_0:30; hence thesis by A5,A2,A6,A3,Th11; end; theorem 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 st 1 <= j & j <= width Gauge(C,i+1) & p = Gauge(C,i+1)*(Center Gauge(C,i+1),j) proof 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))); per cases by Th9; suppose A3: 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); 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 <= l by JORDAN1B:11; A6: width Gauge(C,i+1) = len Gauge(C,i+1) by JORDAN8:def 1; then k >= 4 by JORDAN8:10; then A7: 1 <= k by XXREAL_0:2; then A8: l <= len G by A6,JORDAN1B:12; then A9: [l,1] in Indices G & [l,k] in Indices G by A7,A5,MATRIX_0:30; 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~f c= LSeg(G*(l,1),G*(l,k)) /\ L~f proof let a be object; 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~f; 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 G by JORDAN9:def 1; then G*(l,k)`2 >= N-bound L~Cage(C,i+1) by A6,A7,A5,JORDAN1A:20 ,JORDAN1B:12; then A18: a1`2 <= G*(l,k)`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 G by JORDAN9:def 1; then G*(l,1)`2 <= S-bound L~Cage(C,i+1) by A6,A7,A5,JORDAN1A:22 ,JORDAN1B:12; then A20: a1`2 >= G*(l,1)`2 by A19,XXREAL_0:2; A21: a1 in L~f 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 .= G*(l,1)`1 by A6,A10,A7,A11,JORDAN1A:36; then a1`1 = G*(l,k)`1 by A7,A8,A5,GOBOARD5:2; then a1 in LSeg(G*(l,1),G*(l,k)) by A22,A20,A18,GOBOARD7:7; hence thesis by A21,XBOOLE_0:def 4; end; 1 <= i+1 by NAT_1:11; then LSeg(G*(l,1),G*(l,k)) /\ L~f c= LSeg(Gauge(C,1)*(Center Gauge(C,1),1) , Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1))) /\ L~f 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~f = LSeg(G*(l,1),G*(l,k)) /\ L~f by A13, XBOOLE_0:def 10; LSeg(G*(l,1),G*(l,k)) meets L~f by A3,A6,A7,A5,JORDAN1B:12,29; then consider n such that A24: 1 <= n & n <= k and A25: G*(l,n)`2 = lower_bound(proj2.:(LSeg(G*(l,1),G*(l,k)) /\ L~f)) by A7,A9,Th1,Th10; take n; thus 1 <= n & n <= width Gauge(C,i+1) by A24; 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 thesis by A2,A3,A25,A23,TOPREAL3:6; end; suppose A27: 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); 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 <= l by JORDAN1B:11; A30: width Gauge(C,i+1) = len Gauge(C,i+1) by JORDAN8:def 1; then k >= 4 by JORDAN8:10; then A31: 1 <= k by XXREAL_0:2; then A32: l <= len G by A30,JORDAN1B:12; then A33: [l,1] in Indices G & [l,k] in Indices G by A31,A29,MATRIX_0:30; 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~f c= LSeg(G*(l,1),G*(l,k)) /\ L~f proof let a be object; 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~f; 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 G by JORDAN9:def 1; then G*(l,k)`2 >= N-bound L~Cage(C,i+1) by A30,A31,A29,JORDAN1A:20 ,JORDAN1B:12; then A42: a1`2 <= G*(l,k)`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 G by JORDAN9:def 1; then G*(l,1)`2 <= S-bound L~Cage(C,i+1) by A30,A31,A29,JORDAN1A:22 ,JORDAN1B:12; then A44: a1`2 >= G*(l,1)`2 by A43,XXREAL_0:2; A45: a1 in L~f 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 .= G*(l,1)`1 by A30,A34,A31,A35,JORDAN1A:36; then a1`1 = G*(l,k)`1 by A31,A32,A29,GOBOARD5:2; then a1 in LSeg(G*(l,1),G*(l,k)) by A46,A44,A42,GOBOARD7:7; hence thesis by A45,XBOOLE_0:def 4; end; 1 <= i+1 by NAT_1:11; then LSeg(G*(l,1),G*(l,k)) /\ L~f c= LSeg(Gauge(C,1)*(Center Gauge(C,1),1), Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1))) /\ L~f 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~f = LSeg(G*(l,1),G*(l,k)) /\ L~f by A37, XBOOLE_0:def 10; LSeg(G*(l,1),G*(l,k)) meets L~f by A27,A30,A31,A29,JORDAN1B:12,29; then consider n such that A48: 1 <= n & n <= k and A49: G*(l,n)`2 = lower_bound(proj2.:(LSeg(G*(l,1),G*(l,k)) /\ L~f)) by A31,A33,Th1,Th12; take n; thus 1 <= n & n <= width Gauge(C,i+1) by A48; 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 thesis by A2,A27,A49,A47,TOPREAL3:6; end; end;