Copyright (c) 2001 Association of Mizar Users
environ vocabulary REALSET1, FINSEQ_1, BOOLE, RELAT_1, FINSEQ_5, MATRIX_1, GOBOARD1, FINSEQ_4, RFINSEQ, COMPTS_1, RELAT_2, SPPOL_1, EUCLID, JORDAN1E, JORDAN8, JORDAN9, FINSEQ_6, PSCOMP_1, TOPREAL1, GOBOARD5, MCART_1, TREES_1, FUNCT_1, ARYTM_1, CARD_1, PRE_TOPC, ARYTM_3, GROUP_1, JORDAN1A, SPPOL_2, JORDAN3, SPRECT_2, GROUP_2, JORDAN5C, JORDAN6; notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, XREAL_0, REAL_1, NAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_1, REALSET1, FINSEQ_6, STRUCT_0, PRE_TOPC, CARD_1, CARD_4, BINARITH, CONNSP_1, COMPTS_1, EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD5, SPPOL_1, SPPOL_2, JORDAN3, JORDAN8, JORDAN5C, JORDAN6, JORDAN9, JORDAN1A, JORDAN1E; constructors JORDAN8, REALSET1, JORDAN6, REAL_1, CARD_4, PSCOMP_1, BINARITH, CONNSP_1, JORDAN9, JORDAN1A, WSIERP_1, FINSEQ_4, GOBRD13, JORDAN3, RFINSEQ, TOPS_2, TOPMETR, TOPREAL2, JORDAN5C, SPRECT_1, FINSEQ_5, ENUMSET1, FINSOP_1, JORDAN1E, INT_1; clusters XREAL_0, SPRECT_1, TOPREAL6, JORDAN8, REVROT_1, RELSET_1, ARYTM_3, SUBSET_1, FINSEQ_6, SPRECT_3, AMISTD_1, GOBOARD1, FINSEQ_1, FINSEQ_5, SPPOL_2, JORDAN1A, GOBOARD4, JORDAN1E, BINARITH, REALSET1, MEMBERED, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; definitions TARSKI, XBOOLE_0; theorems AXIOMS, BINARITH, EUCLID, JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, REAL_1, GOBOARD5, REAL_2, FINSEQ_1, FINSEQ_2, JORDAN4, JORDAN6, SPRECT_2, FINSEQ_4, FINSEQ_5, FINSEQ_6, GOBOARD7, GOBOARD9, SPPOL_1, SPPOL_2, TOPREAL4, REVROT_1, TOPREAL1, SPRECT_3, BOOLMARK, JORDAN5B, AMI_5, JORDAN3, JORDAN9, ZFMISC_1, GOBOARD1, SPRECT_1, TARSKI, TOPREAL3, FINSEQ_3, RELAT_1, FUNCT_1, TOPREAL5, JORDAN10, GOBOARD2, CARD_1, CARD_2, YELLOW_6, PRE_CIRC, ENUMSET1, GROUP_5, SPRECT_4, JORDAN1B, SPRECT_5, SCMFSA_7, JORDAN5D, JORDAN1E, PARTFUN2, JORDAN1F, JORDAN5C, REALSET1, XBOOLE_0, XBOOLE_1, SQUARE_1, XCMPLX_0, XCMPLX_1, RLVECT_1; schemes BINARITH; begin reserve n for Nat; definition cluster trivial FinSequence; existence proof take {}; thus thesis; end; end; theorem Th1: for f be trivial FinSequence holds f is empty or ex x be set st f = <*x*> proof let f be trivial FinSequence; assume f is non empty; then consider x be set such that A1: f = {x} by REALSET1:def 12; x in {x} by TARSKI:def 1; then consider y,z be set such that A2: x = [y,z] by A1,RELAT_1:def 1; take z; A3: 1 in dom f by A1,FINSEQ_5:6; dom f = {y} by A1,A2,RELAT_1:23; then 1 = y by A3,TARSKI:def 1; hence f = <*z*> by A1,A2,FINSEQ_1:def 5; end; definition let p be non trivial FinSequence; cluster Rev p -> non trivial; coherence proof assume A1: Rev p is trivial; per cases by A1,Th1; suppose Rev p is empty; hence contradiction; suppose ex x be set st Rev p = <*x*>; then consider x be set such that A2: Rev p = <*x*>; p = Rev <*x*> by A2,FINSEQ_6:29 .= <*x*> by FINSEQ_5:63; hence contradiction; end; end; theorem Th2: for D be non empty set for f be FinSequence of D for G be Matrix of D for p be set holds f is_sequence_on G implies f-:p is_sequence_on G proof let D be non empty set; let f be FinSequence of D; let G be Matrix of D; let p be set; assume f is_sequence_on G; then f|(p..f) is_sequence_on G by GOBOARD1:38; hence f-:p is_sequence_on G by FINSEQ_5:def 1; end; theorem Th3: for D be non empty set for f be FinSequence of D for G be Matrix of D for p be Element of D st p in rng f holds f is_sequence_on G implies f:-p is_sequence_on G proof let D be non empty set; let f be FinSequence of D; let G be Matrix of D; let p be Element of D; assume that A1: p in rng f and A2: f is_sequence_on G; consider i be Nat such that i+1 = p..f and A3: f:-p = f/^i by A1,FINSEQ_5:52; thus f:-p is_sequence_on G by A2,A3,JORDAN8:5; end; theorem Th4: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds Upper_Seq(C,n) is_sequence_on Gauge(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; 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 Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n) is_sequence_on Gauge(C,n) by Th2; hence thesis by JORDAN1E:def 1; end; theorem Th5: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds Lower_Seq(C,n) is_sequence_on Gauge(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; A1: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; then A2: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by A1,FINSEQ_6:96; 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 Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n) is_sequence_on Gauge(C,n) by A2,Th3; hence thesis by JORDAN1E:def 2; end; definition let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; cluster Upper_Seq(C,n) -> standard; coherence proof Upper_Seq(C,n) is_sequence_on Gauge(C,n) by Th4; hence thesis by JORDAN8:7; end; cluster Lower_Seq(C,n) -> standard; coherence proof Lower_Seq(C,n) is_sequence_on Gauge(C,n) by Th5; hence thesis by JORDAN8:7; end; end; theorem Th6: for G be Y_equal-in-column Y_increasing-in-line Matrix of TOP-REAL 2 for i1,i2,j1,j2 be Nat st [i1,j1] in Indices G & [i2,j2] in Indices G holds G*(i1,j1)`2 = G*(i2,j2)`2 implies j1 = j2 proof let G be Y_equal-in-column Y_increasing-in-line Matrix of TOP-REAL 2; let i1,i2,j1,j2 be Nat; assume that A1: [i1,j1] in Indices G and A2: [i2,j2] in Indices G and A3: G*(i1,j1)`2 = G*(i2,j2)`2 and A4: j1 <> j2; A5: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A1,GOBOARD5:1; A6: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A2,GOBOARD5:1; then A7: G*(i1,j2)`2 = G*(1,j2)`2 by A5,GOBOARD5:2 .= G*(i2,j2)`2 by A6,GOBOARD5:2; j1 < j2 or j1 > j2 by A4,REAL_1:def 5; hence contradiction by A3,A5,A6,A7,GOBOARD5:5; end; theorem Th7: for G be X_equal-in-line X_increasing-in-column Matrix of TOP-REAL 2 for i1,i2,j1,j2 be Nat st [i1,j1] in Indices G & [i2,j2] in Indices G holds G*(i1,j1)`1 = G*(i2,j2)`1 implies i1 = i2 proof let G be X_equal-in-line X_increasing-in-column Matrix of TOP-REAL 2; let i1,i2,j1,j2 be Nat; assume that A1: [i1,j1] in Indices G and A2: [i2,j2] in Indices G and A3: G*(i1,j1)`1 = G*(i2,j2)`1 and A4: i1 <> i2; A5: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A1,GOBOARD5:1; A6: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A2,GOBOARD5:1; A7: G*(i1,j1)`1 = G*(i1,1)`1 by A5,GOBOARD5:3 .= G*(i1,j2)`1 by A5,A6,GOBOARD5:3; i1 < i2 or i1 > i2 by A4,REAL_1:def 5; hence contradiction by A3,A5,A6,A7,GOBOARD5:4; end; canceled 8; theorem Th16: for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> N-min L~f & f/.len f <> N-min L~f) or (f/.1 <> N-max L~f & f/.len f <> N-max L~f) holds (N-min L~f)`1 < (N-max L~f)`1 proof let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2); set p = N-min L~f; set i = p..f; assume A1: (f/.1 <> N-min L~f & f/.len f <> N-min L~f) or (f/.1 <> N-max L~f & f/.len f <> N-max L~f); A2: len f >= 2 by SPPOL_1:2; A3: p in rng f by SPRECT_2:43; then A4: i in dom f by FINSEQ_4:30; A5: p = f.i by A3,FINSEQ_4:29 .= f/.i by A4,FINSEQ_4:def 4; A6: 1 <= i & i <= len f by A4,FINSEQ_3:27; A7: p`2 = N-bound L~f by PSCOMP_1:94; per cases by A6,REAL_1:def 5; suppose A8: i = 1; p`2 = (N-max L~f)`2 by PSCOMP_1:95; then A9: p`1 <> (N-max L~f)`1 by A1,A5,A8,TOPREAL3:11; p`1 <= (N-max L~f)`1 by PSCOMP_1:97; hence p`1 < (N-max L~f)`1 by A9,REAL_1:def 5; suppose A10: i = len f; p`2 = (N-max L~f)`2 by PSCOMP_1:95; then A11: p`1 <> (N-max L~f)`1 by A1,A5,A10,TOPREAL3:11; p`1 <= (N-max L~f)`1 by PSCOMP_1:97; hence p`1 < (N-max L~f)`1 by A11,REAL_1:def 5; suppose that A12: 1 < i and A13: i < len f; A14: i-'1+1 = i by A12,AMI_5:4; then A15: i-'1 >= 1 by A12,NAT_1:38; i-'1 <= i by A14,NAT_1:29; then i-'1 <= len f by A13,AXIOMS:22; then A16: i-'1 in dom f by A15,FINSEQ_3:27; A17: p in LSeg(f,i-'1) by A5,A13,A14,A15,TOPREAL1:27; A18: i+1 <= len f by A13,NAT_1:38; then A19: p in LSeg(f,i) by A5,A12,TOPREAL1:27; A20: p <> f/.(i-'1) by A4,A5,A14,A16,GOBOARD7:31; i+1 >= 1 by NAT_1:29; then A21: i+1 in dom f by A18,FINSEQ_3:27; then A22: p <> f/.(i+1) by A4,A5,GOBOARD7:31; A23: f/.(i-'1) in LSeg(f,i-'1) by A13,A14,A15,TOPREAL1:27; A24: f/.(i+1) in LSeg(f,i) by A12,A18,TOPREAL1:27; A25: f/.(i-'1) in L~f by A2,A16,GOBOARD1:16; A26: f/.(i+1) in L~f by A2,A21,GOBOARD1:16; A27: not(LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical) proof assume that A28: LSeg(f,i-'1) is vertical and A29: LSeg(f,i) is vertical; A30: i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1; A31: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A12,A18,TOPREAL1:def 5; A32: LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A13,A14,A15,TOPREAL1:def 5; A33: p`1 = (f/.(i+1))`1 & p`1 = (f/.(i-'1))`1 by A17,A19,A23,A24,A28,A29,SPPOL_1:def 3; A34: p`2 >= (f/.(i+1))`2 & p`2 >= (f/.(i-'1))`2 by A7,A25,A26,PSCOMP_1:71; (f/.(i+1))`2 <= (f/.(i-'1))`2 or (f/.(i+1))`2 >= (f/.(i-'1))`2; then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A5,A31,A32,A33,A34,GOBOARD7:8; then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A23,A24,XBOOLE_0:def 3; then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A20,A22,TARSKI:def 1; hence contradiction by A14,A15,A18,A30,TOPREAL1:def 8; end; now per cases by A27,SPPOL_1:41; suppose LSeg(f,i-'1) is horizontal; then A35: p`2 = (f/.(i-'1))`2 by A17,A23,SPPOL_1:def 2; then A36: (f/.(i-'1))`1 <> p`1 by A20,TOPREAL3:11; A37: f/.(i-'1) in N-most L~f by A7,A25,A35,SPRECT_2:14; then (f/.(i-'1))`1 >= p`1 by PSCOMP_1:98; then A38: (f/.(i-'1))`1 > p`1 by A36,REAL_1:def 5; (f/.(i-'1))`1 <= (N-max L~f)`1 by A37,PSCOMP_1:98; hence thesis by A38,AXIOMS:22; suppose LSeg(f,i) is horizontal; then A39: p`2 = (f/.(i+1))`2 by A19,A24,SPPOL_1:def 2; then A40: (f/.(i+1))`1 <> p`1 by A22,TOPREAL3:11; A41: f/.(i+1) in N-most L~f by A7,A26,A39,SPRECT_2:14; then (f/.(i+1))`1 >= p`1 by PSCOMP_1:98; then A42: (f/.(i+1))`1 > p`1 by A40,REAL_1:def 5; (f/.(i+1))`1 <= (N-max L~f)`1 by A41,PSCOMP_1:98; hence thesis by A42,AXIOMS:22; end; hence thesis; end; theorem for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> N-min L~f & f/.len f <> N-min L~f) or (f/.1 <> N-max L~f & f/.len f <> N-max L~f) holds N-min L~f <> N-max L~f proof let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2); assume (f/.1 <> N-min L~f & f/.len f <> N-min L~f) or (f/.1 <> N-max L~f & f/.len f <> N-max L~f); then (N-min L~f)`1 < (N-max L~f)`1 by Th16; hence thesis; end; theorem Th18: for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> S-min L~f & f/.len f <> S-min L~f) or (f/.1 <> S-max L~f & f/.len f <> S-max L~f) holds (S-min L~f)`1 < (S-max L~f)`1 proof let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2); set p = S-min L~f; set i = p..f; assume A1: (f/.1 <> S-min L~f & f/.len f <> S-min L~f) or (f/.1 <> S-max L~f & f/.len f <> S-max L~f); A2: len f >= 2 by SPPOL_1:2; A3: p in rng f by SPRECT_2:45; then A4: i in dom f by FINSEQ_4:30; A5: p = f.i by A3,FINSEQ_4:29 .= f/.i by A4,FINSEQ_4:def 4; A6: 1 <= i & i <= len f by A4,FINSEQ_3:27; A7: p`2 = S-bound L~f by PSCOMP_1:114; per cases by A6,REAL_1:def 5; suppose A8: i = 1; p`2 = (S-max L~f)`2 by PSCOMP_1:115; then A9: p`1 <> (S-max L~f)`1 by A1,A5,A8,TOPREAL3:11; p`1 <= (S-max L~f)`1 by PSCOMP_1:117; hence p`1 < (S-max L~f)`1 by A9,REAL_1:def 5; suppose A10: i = len f; p`2 = (S-max L~f)`2 by PSCOMP_1:115; then A11: p`1 <> (S-max L~f)`1 by A1,A5,A10,TOPREAL3:11; p`1 <= (S-max L~f)`1 by PSCOMP_1:117; hence p`1 < (S-max L~f)`1 by A11,REAL_1:def 5; suppose that A12: 1 < i and A13: i < len f; A14: i-'1+1 = i by A12,AMI_5:4; then A15: i-'1 >= 1 by A12,NAT_1:38; i-'1 <= i by A14,NAT_1:29; then i-'1 <= len f by A13,AXIOMS:22; then A16: i-'1 in dom f by A15,FINSEQ_3:27; A17: p in LSeg(f,i-'1) by A5,A13,A14,A15,TOPREAL1:27; A18: i+1 <= len f by A13,NAT_1:38; then A19: p in LSeg(f,i) by A5,A12,TOPREAL1:27; A20: p <> f/.(i-'1) by A4,A5,A14,A16,GOBOARD7:31; i+1 >= 1 by NAT_1:29; then A21: i+1 in dom f by A18,FINSEQ_3:27; then A22: p <> f/.(i+1) by A4,A5,GOBOARD7:31; A23: f/.(i-'1) in LSeg(f,i-'1) by A13,A14,A15,TOPREAL1:27; A24: f/.(i+1) in LSeg(f,i) by A12,A18,TOPREAL1:27; A25: f/.(i-'1) in L~f by A2,A16,GOBOARD1:16; A26: f/.(i+1) in L~f by A2,A21,GOBOARD1:16; A27: not(LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical) proof assume that A28: LSeg(f,i-'1) is vertical and A29: LSeg(f,i) is vertical; A30: i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1; A31: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A12,A18,TOPREAL1:def 5; A32: LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A13,A14,A15,TOPREAL1:def 5; A33: p`1 = (f/.(i+1))`1 & p`1 = (f/.(i-'1))`1 by A17,A19,A23,A24,A28,A29,SPPOL_1:def 3; A34: p`2 <= (f/.(i+1))`2 & p`2 <= (f/.(i-'1))`2 by A7,A25,A26,PSCOMP_1:71; (f/.(i+1))`2 <= (f/.(i-'1))`2 or (f/.(i+1))`2 >= (f/.(i-'1))`2; then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A5,A31,A32,A33,A34,GOBOARD7:8; then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A23,A24,XBOOLE_0:def 3; then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A20,A22,TARSKI:def 1; hence contradiction by A14,A15,A18,A30,TOPREAL1:def 8; end; now per cases by A27,SPPOL_1:41; suppose LSeg(f,i-'1) is horizontal; then A35: p`2 = (f/.(i-'1))`2 by A17,A23,SPPOL_1:def 2; then A36: (f/.(i-'1))`1 <> p`1 by A20,TOPREAL3:11; A37: f/.(i-'1) in S-most L~f by A7,A25,A35,SPRECT_2:15; then (f/.(i-'1))`1 >= p`1 by PSCOMP_1:118; then A38: (f/.(i-'1))`1 > p`1 by A36,REAL_1:def 5; (f/.(i-'1))`1 <= (S-max L~f)`1 by A37,PSCOMP_1:118; hence thesis by A38,AXIOMS:22; suppose LSeg(f,i) is horizontal; then A39: p`2 = (f/.(i+1))`2 by A19,A24,SPPOL_1:def 2; then A40: (f/.(i+1))`1 <> p`1 by A22,TOPREAL3:11; A41: f/.(i+1) in S-most L~f by A7,A26,A39,SPRECT_2:15; then (f/.(i+1))`1 >= p`1 by PSCOMP_1:118; then A42: (f/.(i+1))`1 > p`1 by A40,REAL_1:def 5; (f/.(i+1))`1 <= (S-max L~f)`1 by A41,PSCOMP_1:118; hence thesis by A42,AXIOMS:22; end; hence thesis; end; theorem for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> S-min L~f & f/.len f <> S-min L~f) or (f/.1 <> S-max L~f & f/.len f <> S-max L~f) holds S-min L~f <> S-max L~f proof let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2); assume (f/.1 <> S-min L~f & f/.len f <> S-min L~f) or (f/.1 <> S-max L~f & f/.len f <> S-max L~f); then (S-min L~f)`1 < (S-max L~f)`1 by Th18; hence thesis; end; theorem Th20: for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> W-min L~f & f/.len f <> W-min L~f) or (f/.1 <> W-max L~f & f/.len f <> W-max L~f) holds (W-min L~f)`2 < (W-max L~f)`2 proof let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2); set p = W-min L~f; set i = p..f; assume A1: (f/.1 <> W-min L~f & f/.len f <> W-min L~f) or (f/.1 <> W-max L~f & f/.len f <> W-max L~f); A2: len f >= 2 by SPPOL_1:2; A3: p in rng f by SPRECT_2:47; then A4: i in dom f by FINSEQ_4:30; A5: p = f.i by A3,FINSEQ_4:29 .= f/.i by A4,FINSEQ_4:def 4; A6: 1 <= i & i <= len f by A4,FINSEQ_3:27; A7: p`1 = W-bound L~f by PSCOMP_1:84; per cases by A6,REAL_1:def 5; suppose A8: i = 1; p`1 = (W-max L~f)`1 by PSCOMP_1:85; then A9: p`2 <> (W-max L~f)`2 by A1,A5,A8,TOPREAL3:11; p`2 <= (W-max L~f)`2 by PSCOMP_1:87; hence p`2 < (W-max L~f)`2 by A9,REAL_1:def 5; suppose A10: i = len f; p`1 = (W-max L~f)`1 by PSCOMP_1:85; then A11: p`2 <> (W-max L~f)`2 by A1,A5,A10,TOPREAL3:11; p`2 <= (W-max L~f)`2 by PSCOMP_1:87; hence p`2 < (W-max L~f)`2 by A11,REAL_1:def 5; suppose that A12: 1 < i and A13: i < len f; A14: i-'1+1 = i by A12,AMI_5:4; then A15: i-'1 >= 1 by A12,NAT_1:38; i-'1 <= i by A14,NAT_1:29; then i-'1 <= len f by A13,AXIOMS:22; then A16: i-'1 in dom f by A15,FINSEQ_3:27; A17: p in LSeg(f,i-'1) by A5,A13,A14,A15,TOPREAL1:27; A18: i+1 <= len f by A13,NAT_1:38; then A19: p in LSeg(f,i) by A5,A12,TOPREAL1:27; A20: p <> f/.(i-'1) by A4,A5,A14,A16,GOBOARD7:31; i+1 >= 1 by NAT_1:29; then A21: i+1 in dom f by A18,FINSEQ_3:27; then A22: p <> f/.(i+1) by A4,A5,GOBOARD7:31; A23: f/.(i-'1) in LSeg(f,i-'1) by A13,A14,A15,TOPREAL1:27; A24: f/.(i+1) in LSeg(f,i) by A12,A18,TOPREAL1:27; A25: f/.(i-'1) in L~f by A2,A16,GOBOARD1:16; A26: f/.(i+1) in L~f by A2,A21,GOBOARD1:16; A27: not(LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal) proof assume that A28: LSeg(f,i-'1) is horizontal and A29: LSeg(f,i) is horizontal; A30: i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1; A31: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A12,A18,TOPREAL1:def 5; A32: LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A13,A14,A15,TOPREAL1:def 5; A33: p`2 = (f/.(i+1))`2 & p`2 = (f/.(i-'1))`2 by A17,A19,A23,A24,A28,A29,SPPOL_1:def 2; A34: p`1 <= (f/.(i+1))`1 & p`1 <= (f/.(i-'1))`1 by A7,A25,A26,PSCOMP_1:71; (f/.(i+1))`1 <= (f/.(i-'1))`1 or (f/.(i+1))`1 >= (f/.(i-'1))`1; then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A5,A31,A32,A33,A34,GOBOARD7:9; then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A23,A24,XBOOLE_0:def 3; then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A20,A22,TARSKI:def 1; hence contradiction by A14,A15,A18,A30,TOPREAL1:def 8; end; now per cases by A27,SPPOL_1:41; suppose LSeg(f,i-'1) is vertical; then A35: p`1 = (f/.(i-'1))`1 by A17,A23,SPPOL_1:def 3; then A36: (f/.(i-'1))`2 <> p`2 by A20,TOPREAL3:11; A37: f/.(i-'1) in W-most L~f by A7,A25,A35,SPRECT_2:16; then (f/.(i-'1))`2 >= p`2 by PSCOMP_1:88; then A38: (f/.(i-'1))`2 > p`2 by A36,REAL_1:def 5; (f/.(i-'1))`2 <= (W-max L~f)`2 by A37,PSCOMP_1:88; hence thesis by A38,AXIOMS:22; suppose LSeg(f,i) is vertical; then A39: p`1 = (f/.(i+1))`1 by A19,A24,SPPOL_1:def 3; then A40: (f/.(i+1))`2 <> p`2 by A22,TOPREAL3:11; A41: f/.(i+1) in W-most L~f by A7,A26,A39,SPRECT_2:16; then (f/.(i+1))`2 >= p`2 by PSCOMP_1:88; then A42: (f/.(i+1))`2 > p`2 by A40,REAL_1:def 5; (f/.(i+1))`2 <= (W-max L~f)`2 by A41,PSCOMP_1:88; hence thesis by A42,AXIOMS:22; end; hence thesis; end; theorem for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> W-min L~f & f/.len f <> W-min L~f) or (f/.1 <> W-max L~f & f/.len f <> W-max L~f) holds W-min L~f <> W-max L~f proof let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2); assume (f/.1 <> W-min L~f & f/.len f <> W-min L~f) or (f/.1 <> W-max L~f & f/.len f <> W-max L~f); then (W-min L~f)`2 < (W-max L~f)`2 by Th20; hence thesis; end; theorem Th22: for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> E-min L~f & f/.len f <> E-min L~f) or (f/.1 <> E-max L~f & f/.len f <> E-max L~f) holds (E-min L~f)`2 < (E-max L~f)`2 proof let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2); set p = E-min L~f; set i = p..f; assume A1: (f/.1 <> E-min L~f & f/.len f <> E-min L~f) or (f/.1 <> E-max L~f & f/.len f <> E-max L~f); A2: len f >= 2 by SPPOL_1:2; A3: p in rng f by SPRECT_2:49; then A4: i in dom f by FINSEQ_4:30; A5: p = f.i by A3,FINSEQ_4:29 .= f/.i by A4,FINSEQ_4:def 4; A6: 1 <= i & i <= len f by A4,FINSEQ_3:27; A7: p`1 = E-bound L~f by PSCOMP_1:104; per cases by A6,REAL_1:def 5; suppose A8: i = 1; p`1 = (E-max L~f)`1 by PSCOMP_1:105; then A9: p`2 <> (E-max L~f)`2 by A1,A5,A8,TOPREAL3:11; p`2 <= (E-max L~f)`2 by PSCOMP_1:107; hence p`2 < (E-max L~f)`2 by A9,REAL_1:def 5; suppose A10: i = len f; p`1 = (E-max L~f)`1 by PSCOMP_1:105; then A11: p`2 <> (E-max L~f)`2 by A1,A5,A10,TOPREAL3:11; p`2 <= (E-max L~f)`2 by PSCOMP_1:107; hence p`2 < (E-max L~f)`2 by A11,REAL_1:def 5; suppose that A12: 1 < i and A13: i < len f; A14: i-'1+1 = i by A12,AMI_5:4; then A15: i-'1 >= 1 by A12,NAT_1:38; i-'1 <= i by A14,NAT_1:29; then i-'1 <= len f by A13,AXIOMS:22; then A16: i-'1 in dom f by A15,FINSEQ_3:27; A17: p in LSeg(f,i-'1) by A5,A13,A14,A15,TOPREAL1:27; A18: i+1 <= len f by A13,NAT_1:38; then A19: p in LSeg(f,i) by A5,A12,TOPREAL1:27; A20: p <> f/.(i-'1) by A4,A5,A14,A16,GOBOARD7:31; i+1 >= 1 by NAT_1:29; then A21: i+1 in dom f by A18,FINSEQ_3:27; then A22: p <> f/.(i+1) by A4,A5,GOBOARD7:31; A23: f/.(i-'1) in LSeg(f,i-'1) by A13,A14,A15,TOPREAL1:27; A24: f/.(i+1) in LSeg(f,i) by A12,A18,TOPREAL1:27; A25: f/.(i-'1) in L~f by A2,A16,GOBOARD1:16; A26: f/.(i+1) in L~f by A2,A21,GOBOARD1:16; A27: not(LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal) proof assume that A28: LSeg(f,i-'1) is horizontal and A29: LSeg(f,i) is horizontal; A30: i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1; A31: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A12,A18,TOPREAL1:def 5; A32: LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A13,A14,A15,TOPREAL1:def 5; A33: p`2 = (f/.(i+1))`2 & p`2 = (f/.(i-'1))`2 by A17,A19,A23,A24,A28,A29,SPPOL_1:def 2; A34: p`1 >= (f/.(i+1))`1 & p`1 >= (f/.(i-'1))`1 by A7,A25,A26,PSCOMP_1:71; (f/.(i+1))`1 <= (f/.(i-'1))`1 or (f/.(i+1))`1 >= (f/.(i-'1))`1; then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A5,A31,A32,A33,A34,GOBOARD7:9; then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A23,A24,XBOOLE_0:def 3; then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A20,A22,TARSKI:def 1; hence contradiction by A14,A15,A18,A30,TOPREAL1:def 8; end; now per cases by A27,SPPOL_1:41; suppose LSeg(f,i-'1) is vertical; then A35: p`1 = (f/.(i-'1))`1 by A17,A23,SPPOL_1:def 3; then A36: (f/.(i-'1))`2 <> p`2 by A20,TOPREAL3:11; A37: f/.(i-'1) in E-most L~f by A7,A25,A35,SPRECT_2:17; then (f/.(i-'1))`2 >= p`2 by PSCOMP_1:108; then A38: (f/.(i-'1))`2 > p`2 by A36,REAL_1:def 5; (f/.(i-'1))`2 <= (E-max L~f)`2 by A37,PSCOMP_1:108; hence thesis by A38,AXIOMS:22; suppose LSeg(f,i) is vertical; then A39: p`1 = (f/.(i+1))`1 by A19,A24,SPPOL_1:def 3; then A40: (f/.(i+1))`2 <> p`2 by A22,TOPREAL3:11; A41: f/.(i+1) in E-most L~f by A7,A26,A39,SPRECT_2:17; then (f/.(i+1))`2 >= p`2 by PSCOMP_1:108; then A42: (f/.(i+1))`2 > p`2 by A40,REAL_1:def 5; (f/.(i+1))`2 <= (E-max L~f)`2 by A41,PSCOMP_1:108; hence thesis by A42,AXIOMS:22; end; hence thesis; end; theorem for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> E-min L~f & f/.len f <> E-min L~f) or (f/.1 <> E-max L~f & f/.len f <> E-max L~f) holds E-min L~f <> E-max L~f proof let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2); assume (f/.1 <> E-min L~f & f/.len f <> E-min L~f) or (f/.1 <> E-max L~f & f/.len f <> E-max L~f); then (E-min L~f)`2 < (E-max L~f)`2 by Th22; hence thesis; end; theorem Th24: for D be non empty set for f be FinSequence of D for p,q be Element of D st p in rng f & q in rng f & q..f <= p..f holds (f-:p):-q = (f:-q)-:p proof let D be non empty set; let f be FinSequence of D; let p,q be Element of D; A1: f-:p = f|(p..f) by FINSEQ_5:def 1; assume that A2: p in rng f and A3: q in rng f and A4: q..f <= p..f; consider i be Nat such that A5: i+1 = q..f and A6: f:-q = f/^i by A3,FINSEQ_5:52; q in rng (f-:p) by A2,A3,A4,FINSEQ_5:49; then consider j be Nat such that A7: j+1 = q..(f-:p) and A8: (f-:p):-q = (f-:p)/^j by FINSEQ_5:52; A9: (f:-q)-:p = (f:-q)|(p..(f:-q)) by FINSEQ_5:def 1; A10: i < p..f by A4,A5,NAT_1:38; then p..f = i + p..(f/^i) by A2,FINSEQ_6:61; then A11: p..(f/^i) = p..f-i by XCMPLX_1:26 .= p..f-'i by A10,SCMFSA_7:3; q..(f-:p) = q..f by A2,A3,A4,SPRECT_5:3; then i = j by A5,A7,XCMPLX_1:2; hence (f-:p):-q = (f:-q)-:p by A1,A6,A8,A9,A11,JORDAN3:21; end; theorem Th25: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat holds L~(Cage(C,n)-:W-min L~Cage(C,n)) /\ L~(Cage(C,n):-W-min L~Cage(C,n)) = {N-min L~Cage(C,n),W-min L~Cage(C,n)} proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; set US = Cage(C,n)-:W-min L~Cage(C,n); set LS = Cage(C,n):-W-min L~Cage(C,n); set f=Cage(C,n); set pW=W-min L~Cage(C,n); set pN=N-min L~Cage(C,n); set pNa=N-max L~Cage(C,n); set pSa=S-max L~Cage(C,n); set pSi=S-min L~Cage(C,n); set pEa=E-max L~Cage(C,n); set pEi=E-min L~Cage(C,n); A1: N-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:44; A2: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; A3: (W-min L~Cage(C,n))..Cage(C,n) <= (W-min L~Cage(C,n))..Cage(C,n); (f:-pW)/.len(f:-pW) = f/.len f by A2,FINSEQ_5:57 .= f/.1 by FINSEQ_6:def 1 .= pN by JORDAN9:34; then A4: pN in rng (Cage(C,n):-pW) by REVROT_1:3; A5: Cage(C,n)-:pW <> {} by A2,FINSEQ_5:50; (Cage(C,n):-pW)/.1 = pW by FINSEQ_5:56; then A6: W-min L~Cage(C,n) in rng (Cage(C,n):-W-min L~Cage(C,n)) by FINSEQ_6:46; (Cage(C,n)-:pW)/.1 = Cage(C,n)/.1 by A2,FINSEQ_5:47 .= pN by JORDAN9:34; then A7: N-min L~Cage(C,n) in rng (Cage(C,n)-:W-min L~Cage(C,n)) by A5,FINSEQ_6:46; A8: f/.1 = pN by JORDAN9:34; then A9: pNa..f <= pEa..f by SPRECT_2:74; A10: pEa..f < pEi..f by A8,SPRECT_2:75; A11: pEi..f <= pSa..f by A8,SPRECT_2:76; A12: pSa..f < pSi..f by A8,SPRECT_2:77; A13: pSi..f <= pW..f by A8,SPRECT_2:78; pNa..f < pEi..f by A9,A10,AXIOMS:22; then pNa..f < pSa..f by A11,AXIOMS:22; then pNa..f < pSi..f by A12,AXIOMS:22; then pNa..f <= pW..f by A13,AXIOMS:22; then A14: pNa in rng (f-:pW) by A1,A2,FINSEQ_5:49; len(f-:pW) = pW..f by A2,FINSEQ_5:45; then (f-:pW)/.len (f-:pW) = pW by A2,FINSEQ_5:48; then A15: pW in rng (Cage(C,n)-:pW) by A5,REVROT_1:3; W-max L~f in L~f & pN`2 = N-bound L~f by PSCOMP_1:94,SPRECT_1:15; then (W-max L~f)`2 <= pN`2 by PSCOMP_1:71; then A16: pN <> pW by SPRECT_2:61; then A17: Card {pN,pW} = 2 by CARD_2:76; {pN,pW} c= rng LS proof let x be set; assume x in {pN,pW}; hence x in rng LS by A4,A6,TARSKI:def 2; end; then A18: Card {pN,pW} c= Card rng LS by CARD_1:27; Card rng LS c= Card dom LS by YELLOW_6:3; then Card rng LS c= len LS by PRE_CIRC:21; then 2 c= len LS by A17,A18,XBOOLE_1:1; then len LS >= 2 by CARD_1:56; then A19: rng LS c= L~LS by SPPOL_2:18; A20: W-min L~Cage(C,n) in rng LS by FINSEQ_6:66; A21: pN <> pNa by SPRECT_2:56; W-max L~f in L~f & pNa`2 = N-bound L~f by PSCOMP_1:94,SPRECT_1:15; then (W-max L~f)`2 <= pNa`2 by PSCOMP_1:71; then pNa <> pW by SPRECT_2:61; then A22: Card {pN,pNa,pW} = 3 by A16,A21,CARD_2:77; {pN,pNa,pW} c= rng US proof let x be set; assume x in {pN,pNa,pW}; hence x in rng US by A7,A14,A15,ENUMSET1:def 1; end; then A23: Card {pN,pNa,pW} c= Card rng US by CARD_1:27; Card rng US c= Card dom US by YELLOW_6:3; then Card rng US c= len US by PRE_CIRC:21; then A24: 3 c= len US by A22,A23,XBOOLE_1:1; then A25: len US >= 3 by CARD_1:56; then len US >= 2 by AXIOMS:22; then A26: rng US c= L~US by SPPOL_2:18; len US <> 0 by A24,CARD_1:56; then A27: US is non empty by FINSEQ_1:25; A28: W-min L~Cage(C,n) in rng US by A2,A3,FINSEQ_5:49; US/.1 = Cage(C,n)/.1 by A2,FINSEQ_5:47 .= N-min L~Cage(C,n) by JORDAN9:34; then A29: N-min L~Cage(C,n) in rng US by A27,FINSEQ_6:46; LS/.(len LS) = Cage(C,n)/.len Cage(C,n) by A2,FINSEQ_5:57 .= Cage(C,n)/.1 by FINSEQ_6:def 1 .= N-min L~Cage(C,n) by JORDAN9:34; then A30: N-min L~Cage(C,n) in rng LS by REVROT_1:3; thus L~US /\ L~LS c= {N-min L~Cage(C,n),W-min L~Cage(C,n)} proof let x be set; assume A31: x in L~US /\ L~LS; then A32: x in L~US & x in L~LS by XBOOLE_0:def 3; reconsider x1=x as Point of TOP-REAL 2 by A31; consider i1 be Nat such that A33: 1 <= i1 & i1+1 <= len US and A34: x1 in LSeg(US,i1) by A32,SPPOL_2:13; consider i2 be Nat such that A35: 1 <= i2 & i2+1 <= len LS and A36: x1 in LSeg(LS,i2) by A32,SPPOL_2:13; A37: LSeg(US,i1) = LSeg(f,i1) by A33,SPPOL_2:9; set i3=i2-'1; A38: i3+1 = i2 by A35,AMI_5:4; then A39: LSeg(LS,i2) = LSeg(f,i3+pW..f) by A2,SPPOL_2:10; A40: len US = pW..f by A2,FINSEQ_5:45; A41: len LS = len f-pW..f+1 by A2,FINSEQ_5:53; A42: i2-1 >= 1-1 by A35,REAL_1:49; i2 < len f-pW..f+1 by A35,A41,NAT_1:38; then i2-1 < len f-pW..f by REAL_1:84; then i2-1+pW..f < len f by REAL_1:86; then A43: i3+pW..f < len f by A42,BINARITH:def 3; A44: i3 >= 0 by NAT_1:18; A45: pW..f >= 1 by A2,FINSEQ_4:31; i3+1 < len f-pW..f+1 by A35,A38,A41,NAT_1:38; then i3 < len f-pW..f by REAL_1:55; then A46: i3+pW..f < len f by REAL_1:86; A47: i1+1 < pW..f+1 by A33,A40,NAT_1:38; 1+pW..f <= i3+1+pW..f by A35,A38,REAL_1:55; then i1+1 < i3+1+pW..f by A47,AXIOMS:22; then i1+1 < i3+pW..f+1 by XCMPLX_1:1; then A48: i1+1 <= i3+pW..f by NAT_1:38; A49: i3+pW..f+1 <= len f by A46,NAT_1:38; A50: len f > 4 by GOBOARD7:36; A51: i3+pW..f >= 0 & i1 >= 0 by NAT_1:18; A52: pW..f-'1+1 = pW..f by A45,AMI_5:4; assume A53: not x in {N-min L~Cage(C,n),W-min L~Cage(C,n)}; now per cases by A33,A48,REAL_1:def 5; suppose i1+1 < i3+pW..f & i1 > 1; then LSeg(f,i1) misses LSeg(f,i3+pW..f) by A46,GOBOARD5:def 4; then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {} by XBOOLE_0:def 7; hence contradiction by A34,A36,A37,A39,XBOOLE_0:def 3; suppose A54: i1 = 1; i3+pW..f >= 0+3 by A25,A40,A44,REAL_1:55; then A55: i1+1 < i3+pW..f by A54,AXIOMS:22; now per cases by A49,REAL_1:def 5; suppose i3+pW..f+1 < len f; then LSeg(f,i1) misses LSeg(f,i3+pW..f) by A55,GOBOARD5:def 4; then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {} by XBOOLE_0:def 7; hence contradiction by A34,A36,A37,A39,XBOOLE_0:def 3; suppose i3+pW..f+1 = len f; then i3+pW..f = len f-1 by XCMPLX_1:26; then i3+pW..f = len f-'1 by A51,BINARITH:def 3; then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {f/.1} by A50,A54,REVROT_1:30; then x1 in {f/.1} by A34,A36,A37,A39,XBOOLE_0:def 3; then x1 = f/.1 by TARSKI:def 1 .= pN by JORDAN9:34; hence contradiction by A53,TARSKI:def 2; end; hence contradiction; suppose A56: i1+1 = i3+pW..f; 0+pW..f <= i3+pW..f by A44,REAL_1:55; then pW..f = i1+1 by A33,A40,A56,AXIOMS:21; then i1 = pW..f-1 by XCMPLX_1:26; then A57: i1 = pW..f-'1 by A51,BINARITH:def 3; i3+pW..f >= pW..f by NAT_1:29; then pW..f < len f by A43,AXIOMS:22; then pW..f+1 <= len f by NAT_1:38; then pW..f-'1 + (1+1) <= len f by A52,XCMPLX_1:1; then LSeg(f,i1) /\ LSeg(f,i3+(pW..f)) = {f/.(pW..f)} by A33,A52,A56,A57,TOPREAL1:def 8; then x1 in {f/.(pW..f)} by A34,A36,A37,A39,XBOOLE_0:def 3; then x1 = f/.(pW..f) by TARSKI:def 1 .= pW by A2,FINSEQ_5:41; hence contradiction by A53,TARSKI:def 2; end; hence contradiction; end; thus {N-min L~Cage(C,n),W-min L~Cage(C,n)} c= L~US /\ L~LS proof let x be set; assume A58: x in {N-min L~Cage(C,n),W-min L~Cage(C,n)}; per cases by A58,TARSKI:def 2; suppose x = N-min L~Cage(C,n); hence x in L~US /\ L~LS by A19,A26,A29,A30,XBOOLE_0:def 3; suppose x = W-min L~Cage(C,n); hence x in L~US /\ L~LS by A19,A20,A26,A28,XBOOLE_0:def 3; end; end; theorem Th26: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds Lower_Seq(C,n) = Rotate(Cage(C,n),E-max L~Cage(C,n))-:W-min L~Cage(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; set Nmi = N-min L~Cage(C,n); set Nma = N-max L~Cage(C,n); set Wmi = W-min L~Cage(C,n); set Wma = W-max L~Cage(C,n); set Ema = E-max L~Cage(C,n); set Emi = E-min L~Cage(C,n); set Sma = S-max L~Cage(C,n); set Smi = S-min L~Cage(C,n); set RotWmi = Rotate(Cage(C,n),Wmi); set RotEma = Rotate(Cage(C,n),Ema); A1: Cage(C,n)/.1 = Nmi by JORDAN9:34; A2: Nmi in rng Cage(C,n) by SPRECT_2:43; A3: Wmi in rng Cage(C,n) by SPRECT_2:47; A4: Ema in rng Cage(C,n) by SPRECT_2:50; A5: Nmi..Cage(C,n) < Nma..Cage(C,n) by A1,SPRECT_2:72; A6: Nma..Cage(C,n) <= Ema..Cage(C,n) by A1,SPRECT_2:74; then A7: Nmi..Cage(C,n) < Ema..Cage(C,n) by A5,AXIOMS:22; A8: Ema..Cage(C,n) < Emi..Cage(C,n) by A1,SPRECT_2:75; A9: Emi..Cage(C,n) <= Sma..Cage(C,n) by A1,SPRECT_2:76; A10: Sma..Cage(C,n) < Smi..Cage(C,n) by A1,SPRECT_2:77; A11: Smi..Cage(C,n) <= Wmi..Cage(C,n) by A1,SPRECT_2:78; Ema..Cage(C,n) < Sma..Cage(C,n) by A8,A9,AXIOMS:22; then Ema..Cage(C,n) < Smi..Cage(C,n) by A10,AXIOMS:22; then A12: Ema..Cage(C,n) < Wmi..Cage(C,n) by A11,AXIOMS:22; then A13: Ema in rng (Cage(C,n)-:Wmi) by A3,A4,FINSEQ_5:49; A14: Cage(C,n)-:Wmi <> {} by A3,FINSEQ_5:50; (Cage(C,n)-:Wmi)/.1 = Cage(C,n)/.1 by A3,FINSEQ_5:47 .= Nmi by JORDAN9:34; then A15: Nmi in rng (Cage(C,n)-:Wmi) by A14,FINSEQ_6:46; len(Cage(C,n)-:Wmi) = Wmi..Cage(C,n) by A3,FINSEQ_5:45; then (Cage(C,n)-:Wmi)/.len (Cage(C,n)-:Wmi) = Wmi by A3,FINSEQ_5:48; then A16: Wmi in rng (Cage(C,n)-:Wmi) by A14,REVROT_1:3; Wma in L~Cage(C,n) & Nmi`2 = N-bound L~Cage(C,n) by PSCOMP_1:94,SPRECT_1:15; then Wma`2 <= Nmi`2 by PSCOMP_1:71; then Nmi <> Wmi by SPRECT_2:61; then A17: Card {Nmi,Wmi} = 2 by CARD_2:76; {Nmi,Wmi} c= rng (Cage(C,n)-:Wmi) proof let x be set; assume x in {Nmi,Wmi}; hence x in rng (Cage(C,n)-:Wmi) by A15,A16,TARSKI:def 2; end; then A18: Card {Nmi,Wmi} c= Card rng (Cage(C,n)-:Wmi) by CARD_1:27; Card rng (Cage(C,n)-:Wmi) c= Card dom (Cage(C,n)-:Wmi) by YELLOW_6:3; then Card rng (Cage(C,n)-:Wmi) c= len (Cage(C,n)-:Wmi) by PRE_CIRC:21; then 2 c= len (Cage(C,n)-:Wmi) by A17,A18,XBOOLE_1:1; then len (Cage(C,n)-:Wmi) >= 2 by CARD_1:56; then A19: rng (Cage(C,n)-:Wmi) c= L~(Cage(C,n)-:Wmi) by SPPOL_2:18; A20: Nmi..Cage(C,n) < Wmi..Cage(C,n) by A7,A12,AXIOMS:22; then A21: Nmi in rng (Cage(C,n)-:Wmi) by A2,A3,FINSEQ_5:49; A22: Ema..(Cage(C,n)-:Wmi) <> 1 proof assume A23: Ema..(Cage(C,n)-:Wmi) = 1; Nmi..(Cage(C,n)-:Wmi) = Nmi..Cage(C,n) by A2,A3,A20,SPRECT_5:3 .= 1 by A1,FINSEQ_6:47; hence contradiction by A5,A6,A13,A21,A23,FINSEQ_5:10; end; then A24: Ema in rng (Cage(C,n)-:Wmi/^1) by A13,FINSEQ_6:83; A25: Nmi`1 < Nma`1 by SPRECT_2:55; Nma`1 <= (NE-corner L~Cage(C,n))`1 by PSCOMP_1:97; then Nma`1 <= E-bound L~Cage(C,n) by PSCOMP_1:76; then A26: Nmi <> Ema by A25,PSCOMP_1:104; not Ema in rng (Cage(C,n):-Wmi) proof assume A27: Ema in rng (Cage(C,n):-Wmi); (Cage(C,n):-Wmi)/.len(Cage(C,n):-Wmi) = Cage(C,n)/.len Cage(C,n) by A3,FINSEQ_5:57 .= Cage(C,n)/.1 by FINSEQ_6:def 1 .= Nmi by JORDAN9:34; then A28: Nmi in rng (Cage(C,n):-Wmi) by REVROT_1:3; (Cage(C,n):-Wmi)/.1 = Wmi by FINSEQ_5:56; then A29: Wmi in rng (Cage(C,n):-Wmi) by FINSEQ_6:46; Wma in L~Cage(C,n) & Nmi`2 = N-bound L~Cage(C,n) by PSCOMP_1:94,SPRECT_1:15; then Wma`2 <= Nmi`2 by PSCOMP_1:71; then Nmi <> Wmi by SPRECT_2:61; then A30: Card {Nmi,Wmi} = 2 by CARD_2:76; {Nmi,Wmi} c= rng (Cage(C,n):-Wmi) proof let x be set; assume x in {Nmi,Wmi}; hence x in rng (Cage(C,n):-Wmi) by A28,A29,TARSKI:def 2; end; then A31: Card {Nmi,Wmi} c= Card rng (Cage(C,n):-Wmi) by CARD_1:27; Card rng (Cage(C,n):-Wmi) c= Card dom (Cage(C,n):-Wmi) by YELLOW_6:3; then Card rng (Cage(C,n):-Wmi) c= len (Cage(C,n):-Wmi) by PRE_CIRC:21; then 2 c= len (Cage(C,n):-Wmi) by A30,A31,XBOOLE_1:1; then len (Cage(C,n):-Wmi) >= 2 by CARD_1:56; then rng (Cage(C,n):-Wmi) c= L~(Cage(C,n):-Wmi) by SPPOL_2:18; then Ema in L~(Cage(C,n)-:Wmi) /\ L~(Cage(C,n):-Wmi) by A13,A19,A27,XBOOLE_0:def 3; then Ema in {Nmi,Wmi} by Th25; then Ema = Wmi by A26,TARSKI:def 2; hence contradiction by TOPREAL5:25; end; then A32: Ema in rng (Cage(C,n)-:Wmi/^1) \ rng (Cage(C,n):-Wmi) by A24,XBOOLE_0:def 4 ; A33: Wmi in rng (Cage(C,n):-Ema) by A3,A4,A12,FINSEQ_6:67; RotWmi:-Ema = ((Cage(C,n):-Wmi)^((Cage(C,n)-:Wmi)/^1)):-Ema by A3,FINSEQ_6:def 2 .= ((Cage(C,n)-:Wmi)/^1):-Ema by A32,FINSEQ_6:70 .= (Cage(C,n)-:Wmi):-Ema by A13,A22,FINSEQ_6:89 .= (Cage(C,n):-Ema)-:Wmi by A3,A4,A12,Th24 .= ((Cage(C,n):-Ema)^((Cage(C,n)-:Ema)/^1))-:Wmi by A33,FINSEQ_6:71 .= RotEma-:Wmi by A4,FINSEQ_6:def 2; hence Lower_Seq(C,n) = Rotate(Cage(C,n),E-max L~Cage(C,n))-: W-min L~Cage(C,n) by JORDAN1E:def 2; end; theorem Th27: for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (W-min L~Cage(C,n))..Upper_Seq(C,n) = 1 proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by JORDAN1F:5; hence (W-min L~Cage(C,n))..Upper_Seq(C,n) = 1 by FINSEQ_6:47; end; theorem Th28: for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (W-min L~Cage(C,n))..Upper_Seq(C,n) < (W-max L~Cage(C,n))..Upper_Seq(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; set Wmi = W-min L~Cage(C,n); set Wma = W-max L~Cage(C,n); set Nmi = N-min L~Cage(C,n); set Nma = N-max L~Cage(C,n); set Ema = E-max L~Cage(C,n); set Rot = Rotate(Cage(C,n),Wmi); A1: Upper_Seq(C,n) = Rot-:Ema by JORDAN1E:def 1; A2: L~Rot = L~Cage(C,n) by REVROT_1:33; Wmi in rng Cage(C,n) by SPRECT_2:47; then A3: Rot/.1 = Wmi by FINSEQ_6:98; A4: Wmi in rng Rot by A2,SPRECT_2:47; A5: Ema in rng Rot by A2,SPRECT_2:50; A6: Wmi..Rot < Wma..Rot by A2,A3,SPRECT_5:22; A7: Wma..Rot <= Nmi..Rot by A2,A3,SPRECT_5:24; A8: Nmi..Rot < Nma..Rot by A2,A3,SPRECT_5:25; A9: Nma..Rot <= Ema..Rot by A2,A3,SPRECT_5:26; Wma..Rot < Nma..Rot by A7,A8,AXIOMS:22; then A10: Wma..Rot < Ema..Rot by A9,AXIOMS:22; then Wmi..Rot < Ema..Rot by A6,AXIOMS:22; then A11: Wmi..(Rot-:Ema) = Wmi..Rot by A4,A5,SPRECT_5:3; Wma in rng Rot by A2,SPRECT_2:48; hence (W-min L~Cage(C,n))..Upper_Seq(C,n) < (W-max L~Cage(C,n))..Upper_Seq(C,n) by A1,A5,A6,A10,A11,SPRECT_5:3; end; theorem Th29: for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (W-max L~Cage(C,n))..Upper_Seq(C,n) <= (N-min L~Cage(C,n))..Upper_Seq(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; set Wmi = W-min L~Cage(C,n); set Wma = W-max L~Cage(C,n); set Nmi = N-min L~Cage(C,n); set Nma = N-max L~Cage(C,n); set Ema = E-max L~Cage(C,n); set Rot = Rotate(Cage(C,n),Wmi); A1: Upper_Seq(C,n) = Rot-:Ema by JORDAN1E:def 1; A2: L~Rot = L~Cage(C,n) by REVROT_1:33; Wmi in rng Cage(C,n) by SPRECT_2:47; then A3: Rot/.1 = Wmi by FINSEQ_6:98; A4: Wma in rng Rot by A2,SPRECT_2:48; A5: Ema in rng Rot by A2,SPRECT_2:50; A6: Wma..Rot <= Nmi..Rot by A2,A3,SPRECT_5:24; A7: Nmi..Rot < Nma..Rot by A2,A3,SPRECT_5:25; Nma..Rot <= Ema..Rot by A2,A3,SPRECT_5:26; then A8: Nmi..Rot < Ema..Rot by A7,AXIOMS:22; then Wma..Rot < Ema..Rot by A6,AXIOMS:22; then A9: Wma..(Rot-:Ema) = Wma..Rot by A4,A5,SPRECT_5:3; Nmi in rng Rot by A2,SPRECT_2:43; hence (W-max L~Cage(C,n))..Upper_Seq(C,n) <= (N-min L~Cage(C,n))..Upper_Seq(C,n) by A1,A5,A6,A8,A9,SPRECT_5:3; end; theorem Th30: for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (N-min L~Cage(C,n))..Upper_Seq(C,n) < (N-max L~Cage(C,n))..Upper_Seq(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; set Wmi = W-min L~Cage(C,n); set Nmi = N-min L~Cage(C,n); set Nma = N-max L~Cage(C,n); set Ema = E-max L~Cage(C,n); set Rot = Rotate(Cage(C,n),Wmi); A1: Upper_Seq(C,n) = Rot-:Ema by JORDAN1E:def 1; A2: L~Rot = L~Cage(C,n) by REVROT_1:33; Wmi in rng Cage(C,n) by SPRECT_2:47; then A3: Rot/.1 = Wmi by FINSEQ_6:98; A4: Nmi in rng Rot by A2,SPRECT_2:43; A5: Ema in rng Rot by A2,SPRECT_2:50; A6: Nmi..Rot < Nma..Rot by A2,A3,SPRECT_5:25; A7: Nma..Rot <= Ema..Rot by A2,A3,SPRECT_5:26; then Nmi..Rot < Ema..Rot by A6,AXIOMS:22; then A8: Nmi..(Rot-:Ema) = Nmi..Rot by A4,A5,SPRECT_5:3; Nma in rng Rot by A2,SPRECT_2:44; hence (N-min L~Cage(C,n))..Upper_Seq(C,n) < (N-max L~Cage(C,n))..Upper_Seq(C,n) by A1,A5,A6,A7,A8,SPRECT_5:3; end; theorem Th31: for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (N-max L~Cage(C,n))..Upper_Seq(C,n) <= (E-max L~Cage(C,n))..Upper_Seq(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; set Wmi = W-min L~Cage(C,n); set Nma = N-max L~Cage(C,n); set Ema = E-max L~Cage(C,n); set Rot = Rotate(Cage(C,n),Wmi); A1: Upper_Seq(C,n) = Rot-:Ema by JORDAN1E:def 1; A2: L~Rot = L~Cage(C,n) by REVROT_1:33; Wmi in rng Cage(C,n) by SPRECT_2:47; then A3: Rot/.1 = Wmi by FINSEQ_6:98; A4: Nma in rng Rot by A2,SPRECT_2:44; A5: Ema in rng Rot by A2,SPRECT_2:50; A6: Nma..Rot <= Ema..Rot by A2,A3,SPRECT_5:26; then Nma..(Rot-:Ema) = Nma..Rot by A4,A5,SPRECT_5:3; hence thesis by A1,A5,A6,SPRECT_5:3; end; theorem Th32: for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (E-max L~Cage(C,n))..Upper_Seq(C,n) = len Upper_Seq(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; A1: Upper_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n) by JORDAN1E:def 1; A2: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; then A3: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by A2,FINSEQ_6:96; (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)); then E-max L~Cage(C,n) in rng Upper_Seq(C,n) by A1,A3,FINSEQ_5:49; then A4: Upper_Seq(C,n) just_once_values E-max L~Cage(C,n) by FINSEQ_4:10; Upper_Seq(C,n)/.len Upper_Seq(C,n) = E-max L~Cage(C,n) by JORDAN1F:7; hence (E-max L~Cage(C,n))..Upper_Seq(C,n) = len Upper_Seq(C,n) by A4,REVROT_1:1; end; theorem Th33: for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (E-max L~Cage(C,n))..Lower_Seq(C,n) = 1 proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; Lower_Seq(C,n)/.1 = E-max L~Cage(C,n) by JORDAN1F:6; hence (E-max L~Cage(C,n))..Lower_Seq(C,n) = 1 by FINSEQ_6:47; end; theorem Th34: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (E-max L~Cage(C,n))..Lower_Seq(C,n) < (E-min L~Cage(C,n))..Lower_Seq(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; set Ema = E-max L~Cage(C,n); set Emi = E-min L~Cage(C,n); set Sma = S-max L~Cage(C,n); set Smi = S-min L~Cage(C,n); set Wmi = W-min L~Cage(C,n); set Rot = Rotate(Cage(C,n),Ema); A1: Lower_Seq(C,n) = Rot-:Wmi by Th26; A2: L~Rot = L~Cage(C,n) by REVROT_1:33; Ema in rng Cage(C,n) by SPRECT_2:50; then A3: Rot/.1 = Ema by FINSEQ_6:98; A4: Ema in rng Rot by A2,SPRECT_2:50; A5: Wmi in rng Rot by A2,SPRECT_2:47; A6: Ema..Rot < Emi..Rot by A2,A3,SPRECT_5:38; A7: Emi..Rot <= Sma..Rot by A2,A3,SPRECT_5:40; A8: Sma..Rot < Smi..Rot by A2,A3,SPRECT_5:41; A9: Smi..Rot <= Wmi..Rot by A2,A3,SPRECT_5:42; Emi..Rot < Smi..Rot by A7,A8,AXIOMS:22; then A10: Emi..Rot < Wmi..Rot by A9,AXIOMS:22; then Ema..Rot < Wmi..Rot by A6,AXIOMS:22; then A11: Ema..(Rot-:Wmi) = Ema..Rot by A4,A5,SPRECT_5:3; Emi in rng Rot by A2,SPRECT_2:49; hence (E-max L~Cage(C,n))..Lower_Seq(C,n) < (E-min L~Cage(C,n))..Lower_Seq(C,n) by A1,A5,A6,A10,A11,SPRECT_5:3; end; theorem Th35: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (E-min L~Cage(C,n))..Lower_Seq(C,n) <= (S-max L~Cage(C,n))..Lower_Seq(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; set Ema = E-max L~Cage(C,n); set Emi = E-min L~Cage(C,n); set Sma = S-max L~Cage(C,n); set Smi = S-min L~Cage(C,n); set Wmi = W-min L~Cage(C,n); set Rot = Rotate(Cage(C,n),Ema); A1: Lower_Seq(C,n) = Rot-:Wmi by Th26; A2: L~Rot = L~Cage(C,n) by REVROT_1:33; Ema in rng Cage(C,n) by SPRECT_2:50; then A3: Rot/.1 = Ema by FINSEQ_6:98; A4: Emi in rng Rot by A2,SPRECT_2:49; A5: Wmi in rng Rot by A2,SPRECT_2:47; A6: Emi..Rot <= Sma..Rot by A2,A3,SPRECT_5:40; A7: Sma..Rot < Smi..Rot by A2,A3,SPRECT_5:41; Smi..Rot <= Wmi..Rot by A2,A3,SPRECT_5:42; then A8: Sma..Rot < Wmi..Rot by A7,AXIOMS:22; then Emi..Rot < Wmi..Rot by A6,AXIOMS:22; then A9: Emi..(Rot-:Wmi) = Emi..Rot by A4,A5,SPRECT_5:3; Sma in rng Rot by A2,SPRECT_2:46; hence (E-min L~Cage(C,n))..Lower_Seq(C,n) <= (S-max L~Cage(C,n))..Lower_Seq(C,n) by A1,A5,A6,A8,A9,SPRECT_5:3; end; theorem Th36: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (S-max L~Cage(C,n))..Lower_Seq(C,n) < (S-min L~Cage(C,n))..Lower_Seq(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; set Ema = E-max L~Cage(C,n); set Sma = S-max L~Cage(C,n); set Smi = S-min L~Cage(C,n); set Wmi = W-min L~Cage(C,n); set Rot = Rotate(Cage(C,n),Ema); A1: Lower_Seq(C,n) = Rot-:Wmi by Th26; A2: L~Rot = L~Cage(C,n) by REVROT_1:33; Ema in rng Cage(C,n) by SPRECT_2:50; then A3: Rot/.1 = Ema by FINSEQ_6:98; A4: Sma in rng Rot by A2,SPRECT_2:46; A5: Wmi in rng Rot by A2,SPRECT_2:47; A6: Sma..Rot < Smi..Rot by A2,A3,SPRECT_5:41; A7: Smi..Rot <= Wmi..Rot by A2,A3,SPRECT_5:42; then Sma..Rot < Wmi..Rot by A6,AXIOMS:22; then A8: Sma..(Rot-:Wmi) = Sma..Rot by A4,A5,SPRECT_5:3; Smi in rng Rot by A2,SPRECT_2:45; hence thesis by A1,A5,A6,A7,A8,SPRECT_5:3; end; theorem Th37: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (S-min L~Cage(C,n))..Lower_Seq(C,n) <= (W-min L~Cage(C,n))..Lower_Seq(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; set Ema = E-max L~Cage(C,n); set Smi = S-min L~Cage(C,n); set Wmi = W-min L~Cage(C,n); set Rot = Rotate(Cage(C,n),Ema); A1: Lower_Seq(C,n) = Rot-:Wmi by Th26; A2: L~Rot = L~Cage(C,n) by REVROT_1:33; Ema in rng Cage(C,n) by SPRECT_2:50; then A3: Rot/.1 = Ema by FINSEQ_6:98; A4: Smi in rng Rot by A2,SPRECT_2:45; A5: Wmi in rng Rot by A2,SPRECT_2:47; A6: Smi..Rot <= Wmi..Rot by A2,A3,SPRECT_5:42; then Smi..(Rot-:Wmi) = Smi..Rot by A4,A5,SPRECT_5:3; hence thesis by A1,A5,A6,SPRECT_5:3; end; theorem Th38: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (W-min L~Cage(C,n))..Lower_Seq(C,n) = len Lower_Seq(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; A1: Lower_Seq(C,n) = Rotate(Cage(C,n),E-max L~Cage(C,n))-:W-min L~Cage(C,n) by Th26; A2: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; then A3: W-min L~Cage(C,n) in rng Rotate(Cage(C,n),E-max L~Cage(C,n)) by A2,FINSEQ_6:96; (W-min L~Cage(C,n))..Rotate(Cage(C,n),E-max L~Cage(C,n)) <= (W-min L~Cage(C,n))..Rotate(Cage(C,n),E-max L~Cage(C,n)); then W-min L~Cage(C,n) in rng Lower_Seq(C,n) by A1,A3,FINSEQ_5:49; then A4: Lower_Seq(C,n) just_once_values W-min L~Cage(C,n) by FINSEQ_4:10; Lower_Seq(C,n)/.len Lower_Seq(C,n) = W-min L~Cage(C,n) by JORDAN1F:8; hence thesis by A4,REVROT_1:1; end; theorem Th39: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (Upper_Seq(C,n)/.2)`1 = W-bound L~Cage(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; set Ca = Cage(C,n); set US = Upper_Seq(C,n); set Wmin = W-min L~Cage(C,n); set Emax = E-max L~Cage(C,n); set Nmin = N-min L~Cage(C,n); A1: Emax in rng Ca by SPRECT_2:50; A2: Wmin in rng Ca by SPRECT_2:47; then A3: Emax in rng Rotate(Ca,Wmin) by A1,FINSEQ_6:96; (Ca:-Wmin)/.len(Ca:-Wmin) = Ca/.len Ca by A2,FINSEQ_5:57 .= Ca/.1 by FINSEQ_6:def 1 .= Nmin by JORDAN9:34; then A4: Nmin in rng (Ca:-Wmin) by REVROT_1:3; (Ca:-Wmin)/.1 = Wmin by FINSEQ_5:56; then A5: Wmin in rng (Ca:-Wmin) by FINSEQ_6:46; W-max L~Ca in L~Ca & Nmin`2 = N-bound L~Ca by PSCOMP_1:94,SPRECT_1:15; then (W-max L~Ca)`2 <= Nmin`2 by PSCOMP_1:71; then Nmin <> Wmin by SPRECT_2:61; then A6: Card {Nmin,Wmin} = 2 by CARD_2:76; {Nmin,Wmin} c= rng (Ca:-Wmin) proof let x be set; assume x in {Nmin,Wmin}; hence x in rng (Ca:-Wmin) by A4,A5,TARSKI:def 2; end; then A7: Card {Nmin,Wmin} c= Card rng (Ca:-Wmin) by CARD_1:27; Card rng (Ca:-Wmin) c= Card dom (Ca:-Wmin) by YELLOW_6:3; then Card rng (Ca:-Wmin) c= len (Ca:-Wmin) by PRE_CIRC:21; then 2 c= len (Ca:-Wmin) by A6,A7,XBOOLE_1:1; then A8: len (Ca:-Wmin) >= 2 by CARD_1:56; then A9: len(Ca:-Wmin) >= 1 by AXIOMS:22; len US >= 3 by JORDAN1E:19; then len US >= 2 by AXIOMS:22; then 2 in Seg len US by FINSEQ_1:3; then A10: 2 in Seg(Emax..Rotate(Ca,Wmin)) by JORDAN1E:12; A11: 1 <= Wmin..Ca by A2,FINSEQ_4:31; Ca/.1 = Nmin by JORDAN9:34; then Wmin..Ca < len Ca by SPRECT_2:80; then A12: Wmin..Ca+1 <= len Ca by NAT_1:38; A13: US/.2 = (Rotate(Ca,Wmin)-:Emax)/.2 by JORDAN1E:def 1 .= Rotate(Ca,Wmin)/.2 by A3,A10,FINSEQ_5:46 .= Ca/.(2-'1+Wmin..Ca) by A2,A8,REVROT_1:9 .= Ca/.(2-1+Wmin..Ca) by BINARITH:def 3; US/.1 = (Rotate(Ca,Wmin)-:Emax)/.1 by JORDAN1E:def 1 .= Rotate(Ca,Wmin)/.1 by A3,FINSEQ_5:47 .= Ca/.(1-'1+Wmin..Ca) by A2,A9,REVROT_1:9 .= Ca/.(0+Wmin..Ca) by GOBOARD9:1; then Ca/.(Wmin..Ca) = Wmin by JORDAN1F:5; hence thesis by A11,A12,A13,JORDAN1E:26; end; theorem for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (Lower_Seq(C,n)/.2)`1 = E-bound L~Cage(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; set Ca = Cage(C,n); set LS = Lower_Seq(C,n); set Emax = E-max L~Cage(C,n); set Emin = E-min L~Cage(C,n); set Smax = S-max L~Cage(C,n); set Smin = S-min L~Cage(C,n); set Wmin = W-min L~Cage(C,n); set Nmin = N-min L~Cage(C,n); A1: Wmin in rng Ca by SPRECT_2:47; A2: Emax in rng Ca by SPRECT_2:50; then A3: Wmin in rng Rotate(Ca,Emax) by A1,FINSEQ_6:96; (Ca:-Emax)/.len(Ca:-Emax) = Ca/.len Ca by A2,FINSEQ_5:57 .= Ca/.1 by FINSEQ_6:def 1 .= Nmin by JORDAN9:34; then A4: Nmin in rng (Ca:-Emax) by REVROT_1:3; (Ca:-Emax)/.1 = Emax by FINSEQ_5:56; then A5: Emax in rng (Ca:-Emax) by FINSEQ_6:46; N-max L~Ca in L~Ca & Emax`1 = E-bound L~Ca by PSCOMP_1:104,SPRECT_1:13; then (N-max L~Ca)`1 <= Emax`1 by PSCOMP_1:71; then Nmin <> Emax by SPRECT_2:55; then A6: Card {Nmin,Emax} = 2 by CARD_2:76; {Nmin,Emax} c= rng (Ca:-Emax) proof let x be set; assume x in {Nmin,Emax}; hence x in rng (Ca:-Emax) by A4,A5,TARSKI:def 2; end; then A7: Card {Nmin,Emax} c= Card rng (Ca:-Emax) by CARD_1:27; Card rng (Ca:-Emax) c= Card dom (Ca:-Emax) by YELLOW_6:3; then Card rng (Ca:-Emax) c= len (Ca:-Emax) by PRE_CIRC:21; then 2 c= len (Ca:-Emax) by A6,A7,XBOOLE_1:1; then A8: len (Ca:-Emax) >= 2 by CARD_1:56; then A9: len(Ca:-Emax) >= 1 by AXIOMS:22; len LS >= 3 by JORDAN1E:19; then len LS >= 2 by AXIOMS:22; then 2 <= Wmin..LS by Th38; then 2 <= Wmin..(Rotate(Ca,Emax)-:Wmin) by Th26; then 2 <= Wmin..Rotate(Ca,Emax) by A3,FINSEQ_6:77; then A10: 2 in Seg (Wmin..Rotate(Ca,Emax)) by FINSEQ_1:3; A11: 1 <= Emax..Ca by A2,FINSEQ_4:31; A12: Ca/.1 = Nmin by JORDAN9:34; then A13: Emax..Ca < Emin..Ca by SPRECT_2:75; Emin..Ca <= Smax..Ca by A12,SPRECT_2:76; then A14: Emax..Ca < Smax..Ca by A13,AXIOMS:22; Smax..Ca < Smin..Ca by A12,SPRECT_2:77; then A15: Emax..Ca < Smin..Ca by A14,AXIOMS:22; Smin..Ca <= Wmin..Ca by A12,SPRECT_2:78; then A16: Emax..Ca < Wmin..Ca by A15,AXIOMS:22; Wmin..Ca < len Ca by A12,SPRECT_2:80; then Emax..Ca < len Ca by A16,AXIOMS:22; then A17: Emax..Ca+1 <= len Ca by NAT_1:38; A18: LS/.2 = (Rotate(Ca,Emax)-:Wmin)/.2 by Th26 .= Rotate(Ca,Emax)/.2 by A3,A10,FINSEQ_5:46 .= Ca/.(2-'1+Emax..Ca) by A2,A8,REVROT_1:9 .= Ca/.(2-1+Emax..Ca) by BINARITH:def 3; LS/.1 = (Rotate(Ca,Emax)-:Wmin)/.1 by Th26 .= Rotate(Ca,Emax)/.1 by A3,FINSEQ_5:47 .= Ca/.(1-'1+Emax..Ca) by A2,A9,REVROT_1:9 .= Ca/.(0+Emax..Ca) by GOBOARD9:1; then Ca/.(Emax..Ca) = Emax by JORDAN1F:6; hence thesis by A11,A17,A18,JORDAN1E:24; end; theorem Th41: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds W-bound L~Cage(C,n) + E-bound L~Cage(C,n) = W-bound C + E-bound C proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; thus W-bound L~Cage(C,n)+E-bound L~Cage(C,n) = W-bound L~Cage(C,n)+ (E-bound C + (E-bound C - W-bound C)/(2|^n)) by JORDAN1A:85 .= (W-bound C - (E-bound C - W-bound C)/(2|^n))+ (E-bound C + (E-bound C - W-bound C)/(2|^n)) by JORDAN1A:83 .= W-bound C + E-bound C by XCMPLX_1:28; end; theorem for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds S-bound L~Cage(C,n) + N-bound L~Cage(C,n) = S-bound C + N-bound C proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; thus S-bound L~Cage(C,n)+N-bound L~Cage(C,n) = S-bound L~Cage(C,n)+ (N-bound C + (N-bound C - S-bound C)/(2|^n)) by JORDAN10:6 .= (S-bound C - (N-bound C - S-bound C)/(2|^n))+ (N-bound C + (N-bound C - S-bound C)/(2|^n)) by JORDAN1A:84 .= S-bound C + N-bound C by XCMPLX_1:28; end; theorem Th43: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n,i be Nat st 1 <= i & i <= width Gauge(C,n) & n > 0 holds Gauge(C,n)*(Center Gauge(C,n),i)`1 = (W-bound C + E-bound C) / 2 proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let n,i be Nat such that A1: 1 <= i & i <= width Gauge(C,n); A2: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; len Gauge(C,1) >= 4 by JORDAN8:13; then A3: len Gauge(C,1) >= 1 by AXIOMS:22; assume n > 0; hence Gauge(C,n)*(Center Gauge(C,n),i)`1 = Gauge(C,1)*(Center Gauge(C,1),1)`1 by A1,A2,A3,JORDAN1A:57 .= (W-bound C + E-bound C) / 2 by A3,JORDAN1A:59; end; theorem for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n,i be Nat st 1 <= i & i <= len Gauge(C,n) & n > 0 holds Gauge(C,n)*(i,Center Gauge(C,n))`2 = (S-bound C + N-bound C) / 2 proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let n,i be Nat such that A1: 1 <= i & i <= len Gauge(C,n); len Gauge(C,1) >= 4 by JORDAN8:13; then A2: len Gauge(C,1) >= 1 by AXIOMS:22; assume n > 0; hence Gauge(C,n)*(i,Center Gauge(C,n))`2 = Gauge(C,1)*(1,Center Gauge(C,1))`2 by A1,A2,JORDAN1A:58 .= (S-bound C + N-bound C) / 2 by A2,JORDAN1A:60; end; theorem Th45: for f be S-Sequence_in_R2 for k1,k2 be Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & f/.1 in L~mid(f,k1,k2) holds k1 = 1 or k2 = 1 proof let f be S-Sequence_in_R2; let k1,k2 be Nat; assume that A1: 1 <= k1 and A2: k1 <= len f and A3: 1 <= k2 and A4: k2 <= len f and A5: f/.1 in L~mid(f,k1,k2); assume A6: k1 <> 1 & k2 <> 1; consider j be Nat such that A7: 1 <= j and A8: j+1 <= len mid(f,k1,k2) and A9: f/.1 in LSeg(mid(f,k1,k2),j) by A5,SPPOL_2:13; A10: len f >= 2 by TOPREAL1:def 10; per cases by REAL_1:def 5; suppose A11: k1 < k2; then len mid(f,k1,k2) = k2-'k1 + 1 by A1,A2,A3,A4,JORDAN3:27; then j < k2-'k1 + 1 by A8,NAT_1:38; then LSeg(mid(f,k1,k2),j) = LSeg(f,j+k1-'1) by A1,A4,A7,A11,JORDAN4:31; then A12: j+k1-'1 = 1 by A9,A10,JORDAN5B:33; j+k1 >= 1+1 by A1,A7,REAL_1:55; then j+k1-1 >= 1+1-1 by REAL_1:49; then j+k1-1 >= 0 by AXIOMS:22; then j+k1-'1 = j+k1-1 by BINARITH:def 3; then j+(k1-1) = 1 by A12,XCMPLX_1:29; then k1-1 = 1-j by XCMPLX_1:26; then k1-1 <= 0 by A7,REAL_2:106; then k1-1 = 0 by A1,SQUARE_1:12; hence contradiction by A6,XCMPLX_1:15; suppose A13: k1 > k2; then len mid(f,k1,k2) = k1-'k2 + 1 by A1,A2,A3,A4,JORDAN3:27; then A14: j < k1-'k2 + 1 by A8,NAT_1:38; then LSeg(mid(f,k1,k2),j) = LSeg(f,k1-'j) by A2,A3,A7,A13,JORDAN4:32; then A15: k1-'j = 1 by A9,A10,JORDAN5B:33; k1-k2 > 0 by A13,SQUARE_1:11; then k1-'k2 = k1-k2 by BINARITH:def 3; then j-1 < k1-k2 by A14,REAL_1:84; then j-1+k2 < k1 by REAL_1:86; then j-(1-k2) < k1 by XCMPLX_1:37; then j+-(1-k2) < k1 by XCMPLX_0:def 8; then -(1-k2) < k1-j by REAL_1:86; then A16: k2-1 < k1-j by XCMPLX_1:143; then k1-j > 0 by A3,SQUARE_1:12; then k1-j = 1 by A15,BINARITH:def 3; then k2 < 1+1 by A16,REAL_1:84; then k2 <= 1 by NAT_1:38; hence contradiction by A3,A6,AXIOMS:21; suppose k1 = k2; then mid(f,k1,k2) = <*f/.k1*> by A1,A2,JORDAN4:27; hence contradiction by A5,SPPOL_2:12; end; theorem Th46: for f be S-Sequence_in_R2 for k1,k2 be Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & f/.(len f) in L~mid(f,k1,k2) holds k1 = len f or k2 = len f proof let f be S-Sequence_in_R2; let k1,k2 be Nat; assume that A1: 1 <= k1 and A2: k1 <= len f and A3: 1 <= k2 and A4: k2 <= len f and A5: f/.len f in L~mid(f,k1,k2); assume A6: k1 <> len f & k2 <> len f; consider j be Nat such that A7: 1 <= j and A8: j+1 <= len mid(f,k1,k2) and A9: f/.len f in LSeg(mid(f,k1,k2),j) by A5,SPPOL_2:13; per cases by REAL_1:def 5; suppose A10: k1 < k2; then k2-k1 > 0 by SQUARE_1:11; then A11: k2-'k1 = k2-k1 by BINARITH:def 3; A12: j+k1 >= 1+1 by A1,A7,REAL_1:55; then A13: j+k1-1 >= 1+1-1 by REAL_1:49; then A14: j+k1-1 >= 0 by AXIOMS:22; then A15: j+k1-'1 = j+k1-1 by BINARITH:def 3; len mid(f,k1,k2) = k2-'k1 + 1 by A1,A2,A3,A4,A10,JORDAN3:27; then A16: j < k2-'k1 + 1 by A8,NAT_1:38; then j-1 < k2-k1 by A11,REAL_1:84; then j-1+k1 < k2 by REAL_1:86; then j+k1-1 < k2 by XCMPLX_1:29; then A17: j+k1-1 < len f by A4,AXIOMS:22; then A18: j+k1-'1 in dom f by A13,A15,FINSEQ_3:27; A19: j+k1 >= 1 by A12,AXIOMS:22; j+k1-1+1 <= len f by A15,A17,NAT_1:38; then j+k1 <= len f by XCMPLX_1:27; then j+k1 in Seg len f by A19,FINSEQ_1:3; then j+k1-1+1 in Seg len f by XCMPLX_1:27; then A20: j+k1-'1+1 in dom f by A15,FINSEQ_1:def 3; LSeg(mid(f,k1,k2),j) = LSeg(f,j+k1-'1) by A1,A4,A7,A10,A16,JORDAN4:31; then A21: j+k1-'1+1=len f by A9,A18,A20,GOBOARD2:7; j+k1-'1 = j+k1-1 by A14,BINARITH:def 3; then A22: len f = j+k1 by A21,XCMPLX_1:27; j < k2+1-k1 by A11,A16,XCMPLX_1:29; then len f < k2+1 by A22,REAL_1:86; then len f <= k2 by NAT_1:38; hence contradiction by A4,A6,AXIOMS:21; suppose A23: k1 > k2; then len mid(f,k1,k2) = k1-'k2 + 1 by A1,A2,A3,A4,JORDAN3:27; then A24: j < k1-'k2 + 1 by A8,NAT_1:38; k1-k2 > 0 by A23,SQUARE_1:11; then k1-'k2 = k1-k2 by BINARITH:def 3; then j-1 < k1-k2 by A24,REAL_1:84; then j-1+k2 < k1 by REAL_1:86; then j-(1-k2) < k1 by XCMPLX_1:37; then j+-(1-k2) < k1 by XCMPLX_0:def 8; then -(1-k2) < k1-j by REAL_1:86; then A25: k2-1 < k1-j by XCMPLX_1:143; A26: k2-1 >= 0 by A3,SQUARE_1:12; A27: k1-j > 0 by A3,A25,SQUARE_1:12; then A28: k1-'j = k1-j by BINARITH:def 3; then A29: k1-j >= 0+1 by A25,A26,NAT_1:38; k1-j <= k1-1 by A7,REAL_2:106; then k1-j+1 <= k1-1+1 by REAL_1:55; then k1-j+1 <= k1 by XCMPLX_1:27; then k1-j < k1 by A28,NAT_1:38; then A30: k1-j < len f by A2,AXIOMS:22; then A31: k1-'j in dom f by A28,A29,FINSEQ_3:27; A32: k1-j+1 > 0+1 by A25,A26,REAL_1:53; k1-j+1 <= len f by A28,A30,NAT_1:38; then A33: k1-'j+1 in dom f by A28,A32,FINSEQ_3:27; LSeg(mid(f,k1,k2),j) = LSeg(f,k1-'j) by A2,A3,A7,A23,A24,JORDAN4:32; then k1-'j+1=len f by A9,A31,A33,GOBOARD2:7; then A34: k1-j+1=len f by A27,BINARITH:def 3; k1-j <= k1-1 by A7,REAL_2:106; then len f <= k1-1+1 by A34,REAL_1:55; then len f <= k1 by XCMPLX_1:27; hence contradiction by A2,A6,AXIOMS:21; suppose k1 = k2; then mid(f,k1,k2) = <*f/.k1*> by A1,A2,JORDAN4:27; hence contradiction by A5,SPPOL_2:12; end; theorem Th47: for C be compact non vertical non horizontal Subset of TOP-REAL 2 for n be Nat holds rng Upper_Seq(C,n) c= rng Cage(C,n) & rng Lower_Seq(C,n) c= rng 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:47; E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; then A2: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by A1,FINSEQ_6:96; Upper_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n) by JORDAN1E:def 1; then rng Upper_Seq(C,n) c= rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_5:51; hence rng Upper_Seq(C,n) c= rng Cage(C,n) by A1,FINSEQ_6:96; Lower_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n) by JORDAN1E:def 2; then rng Lower_Seq(C,n) c= rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by A2,FINSEQ_5:58; hence rng Lower_Seq(C,n) c= rng Cage(C,n) by A1,FINSEQ_6:96; end; theorem Th48: for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds Upper_Seq(C,n) is_a_h.c._for Cage(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; A1: Upper_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:21; A2: (Upper_Seq(C,n)/.1)`1 = (W-min L~Cage(C,n))`1 by JORDAN1F:5 .= W-bound L~Cage(C,n) by PSCOMP_1:84; (Upper_Seq(C,n)/.len Upper_Seq(C,n))`1 = (E-max L~Cage(C,n))`1 by JORDAN1F:7 .= E-bound L~Cage(C,n) by PSCOMP_1:104; hence Upper_Seq(C,n) is_a_h.c._for Cage(C,n) by A1,A2,SPRECT_2:def 2; end; theorem Th49: for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds Rev Lower_Seq(C,n) is_a_h.c._for Cage(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:22; then A1: Rev Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by SPRECT_3:68; A2: (Rev Lower_Seq(C,n)/.1)`1 = (Lower_Seq(C,n)/.len Lower_Seq(C,n))`1 by FINSEQ_5:68 .= (W-min L~Cage(C,n))`1 by JORDAN1F:8 .= W-bound L~Cage(C,n) by PSCOMP_1:84; (Rev Lower_Seq(C,n)/.len Rev Lower_Seq(C,n))`1 = (Rev Lower_Seq(C,n)/.len Lower_Seq(C,n))`1 by FINSEQ_5:def 3 .= (Lower_Seq(C,n)/.1)`1 by FINSEQ_5:68 .= (E-max L~Cage(C,n))`1 by JORDAN1F:6 .= E-bound L~Cage(C,n) by PSCOMP_1:104; hence Rev Lower_Seq(C,n) is_a_h.c._for Cage(C,n) by A1,A2,SPRECT_2:def 2; end; theorem Th50: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i be Nat st 1 < i & i <= len Gauge(C,n) holds not Gauge(C,n)*(i,1) in rng Upper_Seq(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let i be Nat; assume that A1: 1 < i and A2: i <= len Gauge(C,n) and A3: Gauge(C,n)*(i,1) in rng Upper_Seq(C,n); consider i2 be Nat such that A4: i2 in dom Upper_Seq(C,n) and A5: Upper_Seq(C,n).i2 = Gauge(C,n)*(i,1) by A3,FINSEQ_2:11; set i1 = (N-min L~Cage(C,n))..Upper_Seq(C,n); (W-min L~Cage(C,n))..Upper_Seq(C,n) = 1 by Th27; then A6: 1 < (W-max L~Cage(C,n))..Upper_Seq(C,n) by Th28; (W-max L~Cage(C,n))..Upper_Seq(C,n) <= i1 by Th29; then A7: i1 > 1 by A6,AXIOMS:22; A8: i1 < (N-max L~Cage(C,n))..Upper_Seq(C,n) by Th30; (E-max L~Cage(C,n))..Upper_Seq(C,n) = len Upper_Seq(C,n) by Th32; then (N-max L~Cage(C,n))..Upper_Seq(C,n) <= len Upper_Seq(C,n) by Th31; then A9: i1 < len Upper_Seq(C,n) by A8,AXIOMS:22; A10: 1 <= i2 & i2 <= len Upper_Seq(C,n) by A4,FINSEQ_3:27; A11: i1 in dom Upper_Seq(C,n) by A7,A9,FINSEQ_3:27; set f = Rotate(Cage(C,n),W-min L~Cage(C,n)); A12: Upper_Seq(C,n) = f-:E-max L~Cage(C,n) by JORDAN1E:def 1; A13: N-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43; A14: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; A15: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; then A16: rng f = rng Cage(C,n) by FINSEQ_6:96; A17: f/.1 = W-min L~Cage(C,n) by A15,FINSEQ_6:98; A18: L~Cage(C,n) = L~f by REVROT_1:33; then A19: (N-min L~Cage(C,n))..f < (N-max L~Cage(C,n))..f by A17,SPRECT_5:25; (N-max L~Cage(C,n))..f <= (E-max L~Cage(C,n))..f by A17,A18,SPRECT_5:26; then (N-min L~Cage(C,n))..f < (E-max L~Cage(C,n))..f by A19,AXIOMS:22; then A20: N-min L~Cage(C,n) in rng Upper_Seq(C,n) by A12,A13,A14,A16,FINSEQ_5:49; then A21: Upper_Seq(C,n)/.i1 = N-min L~Cage(C,n) by FINSEQ_5:41; A22: i1 <> i2 proof assume i1 = i2; then Gauge(C,n)*(i,1) = N-min L~Cage(C,n) by A5,A11,A21,FINSEQ_4:def 4; then (Gauge(C,n)*(i,1))`2 = N-bound L~Cage(C,n) by PSCOMP_1:94; then S-bound L~Cage(C,n) = N-bound L~Cage(C,n) by A1,A2,JORDAN1A:93; hence contradiction by SPRECT_1:18; end; then mid(Upper_Seq(C,n),i1,i2) is_S-Seq by A7,A9,A10,JORDAN3:39; then reconsider h1 = mid(Upper_Seq(C,n),i1,i2) as one-to-one special FinSequence of TOP-REAL 2 by TOPREAL1:def 10; set h = Rev h1; 3 <= len Lower_Seq(C,n) by JORDAN1E:19; then A23: 2 <= len Lower_Seq(C,n) by AXIOMS:22; A24: len Lower_Seq(C,n) = len Rev Lower_Seq(C,n) by FINSEQ_5:def 3; A25: len h1 = len h by FINSEQ_5:def 3; then A26: len h <> 1 by A4,A11,A22,SPRECT_2:10; A27: len h >= 1 by A4,A11,A25,SPRECT_2:9; then len h > 1 by A26,REAL_1:def 5; then A28: 1+1 <= len h by NAT_1:38; A29: Rev Lower_Seq(C,n) is_a_h.c._for Cage(C,n) by Th49; A30: h is special by SPPOL_2:42; Upper_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:21; then h1 is_in_the_area_of Cage(C,n) by A4,A11,SPRECT_2:26; then A31: h is_in_the_area_of Cage(C,n) by SPRECT_3:68; len h > 0 by A27,AXIOMS:22; then A32: h1 is non empty by A25,FINSEQ_1:25; A33: Rev Lower_Seq(C,n) is special by SPPOL_2:42; A34: L~Rev Lower_Seq(C,n) = L~Lower_Seq(C,n) by SPPOL_2:22; A35: (h/.1)`2 = (h1/.len h1)`2 by A32,FINSEQ_5:68 .= (Upper_Seq(C,n)/.i2)`2 by A4,A11,SPRECT_2:13 .= (Gauge(C,n)*(i,1))`2 by A4,A5,FINSEQ_4:def 4 .= S-bound L~Cage(C,n) by A1,A2,JORDAN1A:93; (h/.len h)`2 = (h1/.1)`2 by A25,A32,FINSEQ_5:68 .= (Upper_Seq(C,n)/.i1)`2 by A4,A11,SPRECT_2:12 .= (N-min L~Cage(C,n))`2 by A20,FINSEQ_5:41 .= N-bound L~Cage(C,n) by PSCOMP_1:94; then h is_a_v.c._for Cage(C,n) by A31,A35,SPRECT_2:def 3; then L~Rev Lower_Seq(C,n) meets L~h by A23,A24,A28,A29,A30,A33,SPRECT_2:33 ; then consider x be set such that A36: x in L~Lower_Seq(C,n) and A37: x in L~h by A34,XBOOLE_0:3; A38: L~h = L~h1 by SPPOL_2:22; L~mid(Upper_Seq(C,n),i1,i2) c= L~Upper_Seq(C,n) by A7,A9,A10,JORDAN4:47; then x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) by A36,A37,A38,XBOOLE_0:def 3; then A39: x in {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:20; 4 <= len Gauge(C,n) by JORDAN8:13; then A40: 1 <= len Gauge(C,n) by AXIOMS:22; A41: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; per cases by A39,TARSKI:def 2; suppose x = W-min L~Cage(C,n); then x = Upper_Seq(C,n)/.1 by JORDAN1F:5; then i2 = 1 by A7,A9,A10,A37,A38,Th45; then Upper_Seq(C,n)/.1 = Gauge(C,n)*(i,1) by A4,A5,FINSEQ_4:def 4; then W-min(L~Cage(C,n)) = Gauge(C,n)*(i,1) by JORDAN1F:5; then Gauge(C,n)*(i,1)`1 = W-bound(L~Cage(C,n)) by PSCOMP_1:84 .= Gauge(C,n)*(1,1)`1 by A40,JORDAN1A:94; hence contradiction by A1,A2,A40,A41,GOBOARD5:4; suppose x = E-max L~Cage(C,n); then x = Upper_Seq(C,n)/.len Upper_Seq(C,n) by JORDAN1F:7; then i2 = len Upper_Seq(C,n) by A7,A9,A10,A37,A38,Th46; then Upper_Seq(C,n)/.len Upper_Seq(C,n) = Gauge(C,n)*(i,1) by A4,A5,FINSEQ_4:def 4; then A42: E-max(L~Cage(C,n)) = Gauge(C,n)*(i,1) by JORDAN1F:7; A43: (E-min L~Cage(C,n))`2 < (E-max L~Cage(C,n))`2 by SPRECT_2:57; (SE-corner L~Cage(C,n))`2 <= (E-min L~Cage(C,n))`2 by PSCOMP_1:107; then (SE-corner L~Cage(C,n))`2 < (E-max L~Cage(C,n))`2 by A43,AXIOMS:22; then S-bound L~Cage(C,n) < (Gauge(C,n)*(i,1))`2 by A42,PSCOMP_1:79; hence contradiction by A1,A2,JORDAN1A:93; end; theorem Th51: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i be Nat st 1 <= i & i < len Gauge(C,n) holds not Gauge(C,n)*(i,width Gauge(C,n)) in rng Lower_Seq(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let i be Nat; set wi = width Gauge(C,n); assume that A1: 1 <= i and A2: i < len Gauge(C,n) and A3: Gauge(C,n)*(i,wi) in rng Lower_Seq(C,n); consider i2 be Nat such that A4: i2 in dom Lower_Seq(C,n) and A5: Lower_Seq(C,n).i2 = Gauge(C,n)*(i,wi) by A3,FINSEQ_2:11; set i1 = (S-max L~Cage(C,n))..Lower_Seq(C,n); A6: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; (E-max L~Cage(C,n))..Lower_Seq(C,n) = 1 by Th33; then A7: 1 < (E-min L~Cage(C,n))..Lower_Seq(C,n) by Th34; (E-min L~Cage(C,n))..Lower_Seq(C,n) <= i1 by Th35; then A8: i1 > 1 by A7,AXIOMS:22; A9: i1 < (S-min L~Cage(C,n))..Lower_Seq(C,n) by Th36; (W-min L~Cage(C,n))..Lower_Seq(C,n) = len Lower_Seq(C,n) by Th38; then (S-min L~Cage(C,n))..Lower_Seq(C,n) <= len Lower_Seq(C,n) by Th37; then A10: i1 < len Lower_Seq(C,n) by A9,AXIOMS:22; A11: 1 <= i2 & i2 <= len Lower_Seq(C,n) by A4,FINSEQ_3:27; A12: i1 in dom Lower_Seq(C,n) by A8,A10,FINSEQ_3:27; set f = Rotate(Cage(C,n),E-max L~Cage(C,n)); A13: Lower_Seq(C,n) = f-:W-min L~Cage(C,n) by Th26; A14: S-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46; A15: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; A16: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; then A17: rng f = rng Cage(C,n) by FINSEQ_6:96; A18: f/.1 = E-max L~Cage(C,n) by A16,FINSEQ_6:98; A19: L~Cage(C,n) = L~f by REVROT_1:33; then A20: (S-max L~Cage(C,n))..f < (S-min L~Cage(C,n))..f by A18,SPRECT_5:41; (S-min L~Cage(C,n))..f <= (W-min L~Cage(C,n))..f by A18,A19,SPRECT_5:42; then (S-max L~Cage(C,n))..f < (W-min L~Cage(C,n))..f by A20,AXIOMS:22; then A21: S-max L~Cage(C,n) in rng Lower_Seq(C,n) by A13,A14,A15,A17,FINSEQ_5:49; then A22: Lower_Seq(C,n)/.i1 = S-max L~Cage(C,n) by FINSEQ_5:41; A23: i1 <> i2 proof assume i1 = i2; then Gauge(C,n)*(i,wi) = S-max L~Cage(C,n) by A5,A12,A22,FINSEQ_4:def 4; then (Gauge(C,n)*(i,wi))`2 = S-bound L~Cage(C,n) by PSCOMP_1:114; then N-bound L~Cage(C,n) = S-bound L~Cage(C,n) by A1,A2,A6,JORDAN1A:91; hence contradiction by SPRECT_1:18; end; then mid(Lower_Seq(C,n),i1,i2) is_S-Seq by A8,A10,A11,JORDAN3:39; then reconsider h = mid(Lower_Seq(C,n),i1,i2) as one-to-one special FinSequence of TOP-REAL 2 by TOPREAL1:def 10; 3 <= len Upper_Seq(C,n) by JORDAN1E:19; then A24: 2 <= len Upper_Seq(C,n) by AXIOMS:22; A25: len h <> 1 by A4,A12,A23,SPRECT_2:10; len h >= 1 by A4,A12,SPRECT_2:9; then len h > 1 by A25,REAL_1:def 5; then A26: 1+1 <= len h by NAT_1:38; A27: Upper_Seq(C,n) is_a_h.c._for Cage(C,n) by Th48; Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:22; then A28: h is_in_the_area_of Cage(C,n) by A4,A12,SPRECT_2:26; A29: (h/.len h)`2 = (Lower_Seq(C,n)/.i2)`2 by A4,A12,SPRECT_2:13 .= (Gauge(C,n)*(i,wi))`2 by A4,A5,FINSEQ_4:def 4 .= N-bound L~Cage(C,n) by A1,A2,A6,JORDAN1A:91; (h/.1)`2 = (Lower_Seq(C,n)/.i1)`2 by A4,A12,SPRECT_2:12 .= (S-max L~Cage(C,n))`2 by A21,FINSEQ_5:41 .= S-bound L~Cage(C,n) by PSCOMP_1:114; then h is_a_v.c._for Cage(C,n) by A28,A29,SPRECT_2:def 3; then L~Upper_Seq(C,n) meets L~h by A24,A26,A27,SPRECT_2:33; then consider x be set such that A30: x in L~Upper_Seq(C,n) and A31: x in L~h by XBOOLE_0:3; L~mid(Lower_Seq(C,n),i1,i2) c= L~Lower_Seq(C,n) by A8,A10,A11,JORDAN4:47; then x in L~Lower_Seq(C,n) /\ L~Upper_Seq(C,n) by A30,A31,XBOOLE_0:def 3; then A32: x in {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:20; 4 <= len Gauge(C,n) by JORDAN8:13; then A33: 1 <= len Gauge(C,n) by AXIOMS:22; per cases by A32,TARSKI:def 2; suppose x = E-max L~Cage(C,n); then x = Lower_Seq(C,n)/.1 by JORDAN1F:6; then i2 = 1 by A8,A10,A11,A31,Th45; then Lower_Seq(C,n)/.1 = Gauge(C,n)*(i,wi) by A4,A5,FINSEQ_4:def 4; then E-max(L~Cage(C,n)) = Gauge(C,n)*(i,wi) by JORDAN1F:6; then Gauge(C,n)*(i,wi)`1 = E-bound(L~Cage(C,n)) by PSCOMP_1:104 .= Gauge(C,n)*(len Gauge(C,n),wi)`1 by A6,A33,JORDAN1A:92; hence contradiction by A1,A2,A6,A33,GOBOARD5:4; suppose x = W-min L~Cage(C,n); then x = Lower_Seq(C,n)/.len Lower_Seq(C,n) by JORDAN1F:8; then i2 = len Lower_Seq(C,n) by A8,A10,A11,A31,Th46; then Lower_Seq(C,n)/.len Lower_Seq(C,n) = Gauge(C,n)*(i,wi) by A4,A5,FINSEQ_4:def 4; then A34: W-min(L~Cage(C,n)) = Gauge(C,n)*(i,wi) by JORDAN1F:8; A35: (W-max L~Cage(C,n))`2 > (W-min L~Cage(C,n))`2 by SPRECT_2:61; (NW-corner L~Cage(C,n))`2 >= (W-max L~Cage(C,n))`2 by PSCOMP_1:87; then (NW-corner L~Cage(C,n))`2 > (W-min L~Cage(C,n))`2 by A35,AXIOMS:22; then N-bound L~Cage(C,n) > (Gauge(C,n)*(i,wi))`2 by A34,PSCOMP_1:75; hence contradiction by A1,A2,A6,JORDAN1A:91; end; theorem Th52: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i be Nat st 1 < i & i <= len Gauge(C,n) holds not Gauge(C,n)*(i,1) in L~Upper_Seq(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let i be Nat such that A1: 1 < i & i <= len Gauge(C,n) and A2: Gauge(C,n)*(i,1) in L~Upper_Seq(C,n); set Gi1 = Gauge(C,n)*(i,1); consider ii be Nat such that A3: 1 <= ii & ii+1 <= len Upper_Seq(C,n) and A4: Gi1 in LSeg(Upper_Seq(C,n),ii) by A2,SPPOL_2:13; A5: LSeg(Upper_Seq(C,n),ii) = LSeg(Upper_Seq(C,n)/.ii,Upper_Seq(C,n)/.(ii+1)) by A3,TOPREAL1:def 5; Upper_Seq(C,n) is_sequence_on Gauge(C,n) by Th4; then consider i1,j1,i2,j2 being Nat such that A6: [i1,j1] in Indices Gauge(C,n) and A7: Upper_Seq(C,n)/.ii = Gauge(C,n)*(i1,j1) and A8: [i2,j2] in Indices Gauge(C,n) and A9: Upper_Seq(C,n)/.(ii+1) = Gauge(C,n)*(i2,j2) and A10: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A3,JORDAN8:6; A11: 1 <= i1 & i1 <= len Gauge(C,n) & 1 <= j1 & j1 <= width Gauge(C,n) by A6,GOBOARD5:1; A12: 1 <= i2 & i2 <= len Gauge(C,n) & 1 <= j2 & j2 <= width Gauge(C,n) by A8,GOBOARD5:1; A13: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; len Gauge(C,n) >= 4 by JORDAN8:13; then len Gauge(C,n) > 1 by AXIOMS:22; then A14: [i,1] in Indices Gauge(C,n) by A1,A13,GOBOARD7:10; ii+1 >= 1 by NAT_1:29; then A15: ii+1 in dom Upper_Seq(C,n) by A3,FINSEQ_3:27; ii < len Upper_Seq(C,n) by A3,NAT_1:38; then A16: ii in dom Upper_Seq(C,n) by A3,FINSEQ_3:27; A17: not Gi1 in rng Upper_Seq(C,n) by A1,Th50; per cases by A10; suppose A18: i1 = i2 & j1+1 = j2; then Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A11,GOBOARD5:3 .= Gauge(C,n)*(i2,j2)`1 by A12,GOBOARD5:3; then LSeg(Upper_Seq(C,n)/.ii,Upper_Seq(C,n)/.(ii+1)) is vertical by A7,A9,SPPOL_1:37; then Gi1`1 = Gauge(C,n)*(i1,j1)`1 by A4,A5,A7,SPRECT_3:20; then A19: i1 = i by A6,A14,Th7; j1 <= j2 by A18,NAT_1:29; then Gauge(C,n)*(i1,j1)`2 <= Gauge(C,n)*(i2,j2)`2 by A11,A12,A18,SPRECT_3:24; then A20: Gauge(C,n)*(i1,j1)`2 <= Gi1`2 by A4,A5,A7,A9,TOPREAL1:10; Gi1`2 <= Gauge(C,n)*(i1,j1)`2 by A11,A19,SPRECT_3:24; then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A20,AXIOMS:21; then j1 = 1 by A6,A14,Th6; hence contradiction by A7,A16,A17,A19,PARTFUN2:4; suppose A21: i1+1 = i2 & j1 = j2; then Gauge(C,n)*(i1,j1)`2 = Gauge(C,n)*(1,j2)`2 by A11,GOBOARD5:2 .= Gauge(C,n)*(i2,j2)`2 by A12,GOBOARD5:2; then LSeg(Upper_Seq(C,n)/.ii,Upper_Seq(C,n)/.(ii+1)) is horizontal by A7,A9,SPPOL_1:36; then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A4,A5,A7,SPRECT_3:19; then A22: j1 = 1 by A6,A14,Th6; i2 > 1 by A11,A21,NAT_1:38; then not Upper_Seq(C,n)/.(ii+1) in rng Upper_Seq(C,n) by A9,A12,A21,A22,Th50; hence contradiction by A15,PARTFUN2:4; suppose A23: i1 = i2+1 & j1 = j2; then Gauge(C,n)*(i1,j1)`2 = Gauge(C,n)*(1,j2)`2 by A11,GOBOARD5:2 .= Gauge(C,n)*(i2,j2)`2 by A12,GOBOARD5:2; then LSeg(Upper_Seq(C,n)/.ii,Upper_Seq(C,n)/.(ii+1)) is horizontal by A7,A9,SPPOL_1:36; then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A4,A5,A7,SPRECT_3:19; then A24: j1 = 1 by A6,A14,Th6; i1 > 1 by A12,A23,NAT_1:38; then not Upper_Seq(C,n)/.ii in rng Upper_Seq(C,n) by A7,A11,A24,Th50; hence contradiction by A16,PARTFUN2:4; suppose A25: i1 = i2 & j1 = j2+1; then Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A11,GOBOARD5:3 .= Gauge(C,n)*(i2,j2)`1 by A12,GOBOARD5:3; then LSeg(Upper_Seq(C,n)/.ii,Upper_Seq(C,n)/.(ii+1)) is vertical by A7,A9,SPPOL_1:37; then Gi1`1 = Gauge(C,n)*(i1,j1)`1 by A4,A5,A7,SPRECT_3:20; then A26: i1 = i by A6,A14,Th7; j2 <= j1 by A25,NAT_1:29; then Gauge(C,n)*(i2,j2)`2 <= Gauge(C,n)*(i1,j1)`2 by A11,A12,A25,SPRECT_3:24; then A27: Gauge(C,n)*(i2,j2)`2 <= Gi1`2 by A4,A5,A7,A9,TOPREAL1:10; Gi1`2 <= Gauge(C,n)*(i2,j2)`2 by A12,A25,A26,SPRECT_3:24; then Gi1`2 = Gauge(C,n)*(i2,j2)`2 by A27,AXIOMS:21; then j2 = 1 by A8,A14,Th6; hence contradiction by A9,A15,A17,A25,A26,PARTFUN2:4; end; theorem for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i be Nat st 1 <= i & i < len Gauge(C,n) holds not Gauge(C,n)*(i,width Gauge(C,n)) in L~Lower_Seq(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; set wi = width Gauge(C,n); let i be Nat such that A1: 1 <= i & i < len Gauge(C,n) and A2: Gauge(C,n)*(i,wi) in L~Lower_Seq(C,n); set Gi1 = Gauge(C,n)*(i,wi); consider ii be Nat such that A3: 1 <= ii & ii+1 <= len Lower_Seq(C,n) and A4: Gi1 in LSeg(Lower_Seq(C,n),ii) by A2,SPPOL_2:13; A5: LSeg(Lower_Seq(C,n),ii) = LSeg(Lower_Seq(C,n)/.ii,Lower_Seq(C,n)/.(ii+1)) by A3,TOPREAL1:def 5; Lower_Seq(C,n) is_sequence_on Gauge(C,n) by Th5; then consider i1,j1,i2,j2 being Nat such that A6: [i1,j1] in Indices Gauge(C,n) and A7: Lower_Seq(C,n)/.ii = Gauge(C,n)*(i1,j1) and A8: [i2,j2] in Indices Gauge(C,n) and A9: Lower_Seq(C,n)/.(ii+1) = Gauge(C,n)*(i2,j2) and A10: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A3,JORDAN8:6; A11: 1 <= i1 & i1 <= len Gauge(C,n) & 1 <= j1 & j1 <= width Gauge(C,n) by A6,GOBOARD5:1; A12: 1 <= i2 & i2 <= len Gauge(C,n) & 1 <= j2 & j2 <= width Gauge(C,n) by A8,GOBOARD5:1; A13: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; len Gauge(C,n) >= 4 by JORDAN8:13; then len Gauge(C,n) > 1 by AXIOMS:22; then A14: [i,wi] in Indices Gauge(C,n) by A1,A13,GOBOARD7:10; ii+1 >= 1 by NAT_1:29; then A15: ii+1 in dom Lower_Seq(C,n) by A3,FINSEQ_3:27; ii < len Lower_Seq(C,n) by A3,NAT_1:38; then A16: ii in dom Lower_Seq(C,n) by A3,FINSEQ_3:27; A17: not Gi1 in rng Lower_Seq(C,n) by A1,Th51; per cases by A10; suppose A18: i1 = i2 & j2+1 = j1; then Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A11,GOBOARD5:3 .= Gauge(C,n)*(i2,j2)`1 by A12,GOBOARD5:3; then LSeg(Lower_Seq(C,n)/.ii,Lower_Seq(C,n)/.(ii+1)) is vertical by A7,A9,SPPOL_1:37; then Gi1`1 = Gauge(C,n)*(i1,j1)`1 by A4,A5,A7,SPRECT_3:20; then A19: i1 = i by A6,A14,Th7; j1 >= j2 by A18,NAT_1:29; then Gauge(C,n)*(i1,j1)`2 >= Gauge(C,n)*(i2,j2)`2 by A11,A12,A18,SPRECT_3:24; then A20: Gauge(C,n)*(i1,j1)`2 >= Gi1`2 by A4,A5,A7,A9,TOPREAL1:10; Gi1`2 >= Gauge(C,n)*(i1,j1)`2 by A11,A19,SPRECT_3:24; then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A20,AXIOMS:21; then j1 = wi by A6,A14,Th6; hence contradiction by A7,A16,A17,A19,PARTFUN2:4; suppose A21: i2+1 = i1 & j1 = j2; then Gauge(C,n)*(i1,j1)`2 = Gauge(C,n)*(1,j2)`2 by A11,GOBOARD5:2 .= Gauge(C,n)*(i2,j2)`2 by A12,GOBOARD5:2; then LSeg(Lower_Seq(C,n)/.ii,Lower_Seq(C,n)/.(ii+1)) is horizontal by A7,A9,SPPOL_1:36; then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A4,A5,A7,SPRECT_3:19; then A22: j1 = wi by A6,A14,Th6; i2 < len Gauge(C,n) by A11,A21,NAT_1:38; then not Lower_Seq(C,n)/.(ii+1) in rng Lower_Seq(C,n) by A9,A12,A21,A22,Th51; hence contradiction by A15,PARTFUN2:4; suppose A23: i2 = i1+1 & j1 = j2; then Gauge(C,n)*(i1,j1)`2 = Gauge(C,n)*(1,j2)`2 by A11,GOBOARD5:2 .= Gauge(C,n)*(i2,j2)`2 by A12,GOBOARD5:2; then LSeg(Lower_Seq(C,n)/.ii,Lower_Seq(C,n)/.(ii+1)) is horizontal by A7,A9,SPPOL_1:36; then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A4,A5,A7,SPRECT_3:19; then A24: j1 = wi by A6,A14,Th6; i1 < len Gauge(C,n) by A12,A23,NAT_1:38; then not Lower_Seq(C,n)/.ii in rng Lower_Seq(C,n) by A7,A11,A24,Th51; hence contradiction by A16,PARTFUN2:4; suppose A25: i1 = i2 & j2 = j1+1; then Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A11,GOBOARD5:3 .= Gauge(C,n)*(i2,j2)`1 by A12,GOBOARD5:3; then LSeg(Lower_Seq(C,n)/.ii,Lower_Seq(C,n)/.(ii+1)) is vertical by A7,A9,SPPOL_1:37; then Gi1`1 = Gauge(C,n)*(i1,j1)`1 by A4,A5,A7,SPRECT_3:20; then A26: i1 = i by A6,A14,Th7; j2 >= j1 by A25,NAT_1:29; then Gauge(C,n)*(i2,j2)`2 >= Gauge(C,n)*(i1,j1)`2 by A11,A12,A25,SPRECT_3:24; then A27: Gauge(C,n)*(i2,j2)`2 >= Gi1`2 by A4,A5,A7,A9,TOPREAL1:10; Gi1`2 >= Gauge(C,n)*(i2,j2)`2 by A12,A25,A26,SPRECT_3:24; then Gi1`2 = Gauge(C,n)*(i2,j2)`2 by A27,AXIOMS:21; then j2 = wi by A8,A14,Th6; hence contradiction by A9,A15,A17,A25,A26,PARTFUN2:4; end; theorem Th54: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j be Nat st 1 <= i & i <= len Gauge(C,n) & 1 <= j & j <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Cage(C,n) holds LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,j)) meets L~Lower_Seq(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let i,j be Nat; set Gij = Gauge(C,n)*(i,j); assume that A1: 1 <= i & i <= len Gauge(C,n) and A2: 1 <= j & j <= width Gauge(C,n) and A3: Gij in L~Cage(C,n); set NE = NE-corner L~Cage(C,n); set v1 = L_Cut(Upper_Seq(C,n),Gij); set Gv1 = <*Gauge(C,n)*(i,1)*>^v1; set v = Gv1^<*NE*>; set h = mid(Lower_Seq(C,n),2,len Lower_Seq(C,n)); A4: L~Cage(C,n) = L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n) by JORDAN1E:17; A5: Lower_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n)):- E-max L~Cage(C,n) by JORDAN1E:def 2; A6: Upper_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n))-: E-max L~Cage(C,n) by JORDAN1E:def 1; len Lower_Seq(C,n) >= 3 & len Upper_Seq(C,n) >= 3 by JORDAN1E:19; then A7: len Lower_Seq(C,n) >= 2 & len Lower_Seq(C,n) >= 1 & len Upper_Seq(C,n) >= 2 & len Upper_Seq(C,n) >= 1 by AXIOMS:22; A8: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; A9: Gauge(C,n)*(i,1)`2 = S-bound L~Cage(C,n) by A1,JORDAN1A:93; set Wmi = W-min L~Cage(C,n); now per cases by A1,A3,A4,REAL_1:def 5,XBOOLE_0:def 2; suppose A10: Gij in L~Upper_Seq(C,n) & i = 1; set G11 = Gauge(C,n)*(1,1); A11: G11`1 = W-bound L~Cage(C,n) by A1,A10,JORDAN1A:94; A12: Wmi`1 = W-bound L~Cage(C,n) by PSCOMP_1:84; A13: S-bound L~Cage(C,n) = G11`2 by A1,A10,JORDAN1A:93; Wmi in L~Cage(C,n) by SPRECT_1:15; then A14: G11`2 <= Wmi`2 by A13,PSCOMP_1:71; A15: Gij`1 = W-bound L~Cage(C,n) by A2,A8,A10,JORDAN1A:94; then Gij in W-most L~Cage(C,n) by A3,SPRECT_2:16; then Wmi`2 <= Gij`2 by PSCOMP_1:88; then A16: Wmi in LSeg(Gauge(C,n)*(1,1),Gauge(C,n)*(1,j)) by A10,A11,A12,A14,A15,GOBOARD7:8; A17: rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by A7,SPPOL_2:18; Lower_Seq(C,n)/.(len Lower_Seq(C,n)) = Wmi by JORDAN1F:8; then Wmi in rng Lower_Seq(C,n) by REVROT_1:3; hence LSeg(Gauge(C,n)*(i,1),Gij) meets L~Lower_Seq(C,n) by A10,A16,A17,XBOOLE_0:3; suppose A18: Gij in L~Upper_Seq(C,n) & Gij <> Upper_Seq(C,n).len Upper_Seq(C,n) & E-max L~Cage(C,n) <> NE & i > 1; then A19: v1 is non empty by JORDAN1E:7; then len v1 <> 0 by FINSEQ_1:25; then len v1 > 0 by NAT_1:19; then A20: 0+1 <= len v1 by NAT_1:38; then A21: 1 in dom v1 by FINSEQ_3:27; A22: len v1 in dom v1 & len Upper_Seq(C,n) in dom Upper_Seq(C,n) by A7,A20,FINSEQ_3:27; A23: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; then A24: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by A23,FINSEQ_6:96; A25: v1/.(len v1) = v1.(len v1) by A22,FINSEQ_4:def 4 .= Upper_Seq(C,n).len Upper_Seq(C,n) by A18,JORDAN1B:5 .= Upper_Seq(C,n)/.len Upper_Seq(C,n) by A22,FINSEQ_4:def 4 .= (Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n))/. ((E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))) by A6,A24,FINSEQ_5:45 .= E-max L~Cage(C,n) by A24,FINSEQ_5:48; then A26: Gv1/.len Gv1 = E-max L~Cage(C,n) by A19,SPRECT_3:11; A27: v1/.1 = v1.1 by A21,FINSEQ_4:def 4 .= Gij by A18,JORDAN3:58; then A28: (v1^<*NE*>)/.1 = Gij by A20,BOOLMARK:8; A29: 1+len v1 >= 1+1 by A20,REAL_1:55; len v = len Gv1 + 1 by FINSEQ_2:19 .= 1 + len v1 + 1 by FINSEQ_5:8; then A30: 2 < len v by A29,NAT_1:38; S-bound L~Cage(C,n) < N-bound L~Cage(C,n) by SPRECT_1:34; then NE <> Gauge(C,n)*(i,1) by A9,PSCOMP_1:77; then not NE in {Gauge(C,n)*(i,1)} by TARSKI:def 1; then A31: not NE in rng <*Gauge(C,n)*(i,1)*> by FINSEQ_1:56; len Cage(C,n) > 4 by GOBOARD7:36; then len Cage(C,n) >= 2 by AXIOMS:22; then A32: rng Cage(C,n) c= L~Cage(C,n) by SPPOL_2:18; A33: not NE in rng Cage(C,n) proof assume A34: NE in rng Cage(C,n); A35: NE`1 = E-bound L~Cage(C,n) & NE`2 = N-bound L~Cage(C,n) by PSCOMP_1:76,77; then NE`2 >= S-bound L~Cage(C,n) by SPRECT_1:24; then NE in { p where p is Point of TOP-REAL 2 : p`1 = E-bound L~Cage(C,n) & p`2 <= N-bound L~Cage(C,n) & p`2 >= S-bound L~Cage(C,n) } by A35; then NE in LSeg(SE-corner L~Cage(C,n), NE-corner L~Cage(C,n)) by SPRECT_1:25; then NE in LSeg(SE-corner L~Cage(C,n), NE-corner L~Cage(C,n)) /\ L~Cage(C,n) by A32,A34,XBOOLE_0:def 3; then NE in E-most L~Cage(C,n) by PSCOMP_1:def 40; then A36: NE`2 <= (E-max L~Cage(C,n))`2 by PSCOMP_1:108; (E-max L~Cage(C,n))`2 <= NE`2 by PSCOMP_1:107; then A37: (E-max L~Cage(C,n))`2 = NE`2 by A36,AXIOMS:21; (E-max L~Cage(C,n))`1 = NE`1 by PSCOMP_1:105; hence contradiction by A18,A37,TOPREAL3:11; end; now per cases; suppose Gij <> Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1); then v1 = <*Gij*>^mid(Upper_Seq(C,n), Index(Gij,Upper_Seq(C,n))+1,len Upper_Seq(C,n)) by JORDAN3:def 4; then rng v1 = rng <*Gij*> \/ rng mid(Upper_Seq(C,n), Index(Gij,Upper_Seq(C,n))+1,len Upper_Seq(C,n)) by FINSEQ_1:44; then A38: rng v1 = {Gij} \/ rng mid(Upper_Seq(C,n), Index(Gij,Upper_Seq(C,n))+1,len Upper_Seq(C,n)) by FINSEQ_1:55; not NE in L~Cage(C,n) proof assume NE in L~Cage(C,n); then consider i be Nat such that A39: 1 <= i and A40: i+1 <= len Cage(C,n) and A41: NE in LSeg(Cage(C,n)/.i,Cage(C,n)/.(i+1)) by SPPOL_2:14; per cases by A39,A40,TOPREAL1:def 7; suppose A42: (Cage(C,n)/.i)`1 = (Cage(C,n)/.(i+1))`1; then A43: NE`1 = (Cage(C,n)/.i)`1 by A41,GOBOARD7:5; A44: NE`2 = N-bound L~Cage(C,n) by PSCOMP_1:77; A45: i < len Cage(C,n) by A40,NAT_1:38; then A46: (Cage(C,n)/.i)`2 <= NE`2 by A39,A44,JORDAN5D:13; A47: 1 <= i+1 by NAT_1:29; then A48: (Cage(C,n)/.(i+1))`2 <= NE`2 by A40,A44,JORDAN5D:13; A49: i in dom Cage(C,n) & i+1 in dom Cage(C,n) by A39,A40,A45,A47,FINSEQ_3:27; (Cage(C,n)/.i)`2 <= (Cage(C,n)/.(i+1))`2 or (Cage(C,n)/.i)`2 >= (Cage(C,n)/.(i+1))`2; then NE`2 <= (Cage(C,n)/.(i+1))`2 or NE`2 <= (Cage(C,n)/.i)`2 by A41,TOPREAL1:10; then NE`2 = (Cage(C,n)/.(i+1))`2 or NE`2 = (Cage(C,n)/.i)`2 by A46,A48,AXIOMS:21; then NE = (Cage(C,n)/.(i+1)) or NE = (Cage(C,n)/.i) by A42,A43,TOPREAL3:11; hence contradiction by A33,A49,PARTFUN2:4; suppose A50: (Cage(C,n)/.i)`2 = (Cage(C,n)/.(i+1))`2; then A51: NE`2 = (Cage(C,n)/.i)`2 by A41,GOBOARD7:6; A52: NE`1 = E-bound L~Cage(C,n) by PSCOMP_1:76; A53: i < len Cage(C,n) by A40,NAT_1:38; then A54: (Cage(C,n)/.i)`1 <= NE`1 by A39,A52,JORDAN5D:14; A55: 1 <= i+1 by NAT_1:29; then A56: (Cage(C,n)/.(i+1))`1 <= NE`1 by A40,A52,JORDAN5D:14; A57: i in dom Cage(C,n) & i+1 in dom Cage(C,n) by A39,A40,A53,A55,FINSEQ_3:27; (Cage(C,n)/.i)`1 <= (Cage(C,n)/.(i+1))`1 or (Cage(C,n)/.i)`1 >= (Cage(C,n)/.(i+1))`1; then NE`1 <= (Cage(C,n)/.(i+1))`1 or NE`1 <= (Cage(C,n)/.i)`1 by A41,TOPREAL1:9; then NE`1 = (Cage(C,n)/.(i+1))`1 or NE`1 = (Cage(C,n)/.i)`1 by A54,A56,AXIOMS:21; then NE = (Cage(C,n)/.(i+1)) or NE = (Cage(C,n)/.i) by A50,A51,TOPREAL3:11; hence contradiction by A33,A57,PARTFUN2:4; end; then A58: not NE in {Gij} by A3,TARSKI:def 1; A59: rng mid(Upper_Seq(C,n),Index(Gij,Upper_Seq(C,n))+1, len Upper_Seq(C,n)) c= rng Upper_Seq(C,n) by JORDAN3:28; rng Upper_Seq(C,n) c= rng Cage(C,n) by Th47; then rng mid(Upper_Seq(C,n),Index(Gij,Upper_Seq(C,n))+1, len Upper_Seq(C,n)) c= rng Cage(C,n) by A59,XBOOLE_1:1; then not NE in rng mid(Upper_Seq(C,n),Index(Gij,Upper_Seq(C,n))+1, len Upper_Seq(C,n)) by A33; hence not NE in rng v1 by A38,A58,XBOOLE_0:def 2; suppose Gij = Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1); then v1 = mid(Upper_Seq(C,n), Index(Gij,Upper_Seq(C,n))+1,len Upper_Seq(C,n)) by JORDAN3:def 4; then A60: rng v1 c= rng Upper_Seq(C,n) by JORDAN3:28; rng Upper_Seq(C,n) c= rng Cage(C,n) by Th47; then rng v1 c= rng Cage(C,n) by A60,XBOOLE_1:1; hence not NE in rng v1 by A33; end; then not NE in rng <*Gauge(C,n)*(i,1)*> \/ rng v1 by A31,XBOOLE_0:def 2; then not NE in rng Gv1 by FINSEQ_1:44; then rng Gv1 misses {NE} by ZFMISC_1:56; then A61: rng Gv1 misses rng <*NE*> by FINSEQ_1:55; A62: not Gauge(C,n)*(i,1) in L~Upper_Seq(C,n) by A1,A18,Th52; rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by A7,SPPOL_2:18; then A63: not Gauge(C,n)*(i,1) in rng Upper_Seq(C,n) by A1,A18,Th52; not Gauge(C,n)*(i,1) in {Gij} by A18,A62,TARSKI:def 1; then A64: not Gauge(C,n)*(i,1) in rng <*Gij*> by FINSEQ_1:55; set ci = mid(Upper_Seq(C,n),Index(Gij,Upper_Seq(C,n))+1, len Upper_Seq(C,n)); now per cases; suppose A65: Gij <> Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1); rng ci c= rng Upper_Seq(C,n) by JORDAN3:28; then not Gauge(C,n)*(i,1) in rng ci by A63; then not Gauge(C,n)*(i,1) in rng <*Gij*> \/ rng ci by A64,XBOOLE_0:def 2; then not Gauge(C,n)*(i,1) in rng(<*Gij*>^ci) by FINSEQ_1:44; hence not Gauge(C,n)*(i,1) in rng v1 by A65,JORDAN3:def 4; suppose Gij = Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1); then v1 = ci by JORDAN3:def 4; then rng v1 c= rng Upper_Seq(C,n) by JORDAN3:28; hence not Gauge(C,n)*(i,1) in rng v1 by A63; end; then {Gauge(C,n)*(i,1)} misses rng v1 by ZFMISC_1:56; then A66: rng <*Gauge(C,n)*(i,1)*> misses rng v1 by FINSEQ_1:55; A67: <*Gauge(C,n)*(i,1)*> is one-to-one by FINSEQ_3:102; A68: v1 is_S-Seq by A18,JORDAN3:69; then v1 is one-to-one by TOPREAL1:def 10; then A69: Gv1 is one-to-one by A66,A67,FINSEQ_3:98; <*NE*> is one-to-one by FINSEQ_3:102; then A70: v is one-to-one by A61,A69,FINSEQ_3:98; A71: <*Gauge(C,n)*(i,1)*> is special by SPPOL_2:39; A72: v1 is special by A68,TOPREAL1:def 10; (<*Gauge(C,n)*(i,1)*>/.len <*Gauge(C,n)*(i,1)*>)`1 = (<*Gauge(C,n)*(i,1)*>/.1)`1 by FINSEQ_1:56 .= Gauge(C,n)*(i,1)`1 by FINSEQ_4:25 .= (v1/.1)`1 by A1,A2,A27,GOBOARD5:3; then A73: Gv1 is special by A71,A72,GOBOARD2:13; A74: <*NE*> is special by SPPOL_2:39; (Gv1/.len Gv1)`1 = NE`1 by A26,PSCOMP_1:105 .= (<*NE*>/.1)`1 by FINSEQ_4:25; then A75: v is special by A73,A74,GOBOARD2:13; A76: len Lower_Seq(C,n) >= 2+1 by JORDAN1E:19; then A77: len Lower_Seq(C,n) > 2 by NAT_1:38; A78: len Lower_Seq(C,n) > 1 by A76,AXIOMS:22; then h is S-Sequence_in_R2 by A77,JORDAN3:39; then Rev h is S-Sequence_in_R2 by SPPOL_2:47; then A79: 2 <= len Rev h & Rev h is one-to-one & Rev h is special by TOPREAL1:def 10; A80: Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:22; 3 <= len Lower_Seq(C,n) by JORDAN1E:19; then 2 <= len Lower_Seq(C,n) by AXIOMS:22; then A81: 2 in dom Lower_Seq(C,n) by FINSEQ_3:27; A82: len Lower_Seq(C,n) in dom Lower_Seq(C,n) by SCMFSA_7:12; then h is_in_the_area_of Cage(C,n) by A80,A81,SPRECT_2:26; then A83: Rev h is_in_the_area_of Cage(C,n) by SPRECT_3:68; A84: h is non empty by A77,A78,JORDAN1B:3; A85: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; A86: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; then A87: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by A85,FINSEQ_6:96; then 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 A5,FINSEQ_5:57 .= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by FINSEQ_6:def 1 .= W-min L~Cage(C,n) by A85,FINSEQ_6:98; then (Lower_Seq(C,n)/.len Lower_Seq(C,n))`1 = W-bound L~Cage(C,n) by PSCOMP_1:84; then (h/.len h)`1 = W-bound L~Cage(C,n) by A81,A82,SPRECT_2:13; then A88: (Rev h/.1)`1 = W-bound L~Cage(C,n) by A84,FINSEQ_5:68; A89: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:34; then A90: (E-max L~Cage(C,n))..Cage(C,n) < (E-min L~Cage(C,n))..Cage(C,n) by SPRECT_2:75; A91: (E-min L~Cage(C,n))..Cage(C,n) <= (S-max L~Cage(C,n))..Cage(C,n) by A89,SPRECT_2:76; A92: (S-max L~Cage(C,n))..Cage(C,n) < (S-min L~Cage(C,n))..Cage(C,n) by A89,SPRECT_2:77; A93: (S-min L~Cage(C,n))..Cage(C,n) <= (W-min L~Cage(C,n))..Cage(C,n) by A89,SPRECT_2:78; (E-max L~Cage(C,n))..Cage(C,n) < (S-max L~Cage(C,n))..Cage(C,n) by A90,A91,AXIOMS:22; then (E-max L~Cage(C,n))..Cage(C,n) < (S-min L~Cage(C,n))..Cage(C,n) by A92,AXIOMS:22; then A94: (E-max L~Cage(C,n))..Cage(C,n) < (W-min L~Cage(C,n))..Cage(C,n) by A93,AXIOMS:22; then A95: (E-max L~Cage(C,n))..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) by A85,A86,SPRECT_5:10; 0 <= (E-max L~Cage(C,n))..Cage(C,n) by NAT_1:18; then len Cage(C,n)+0 <= len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n) by AXIOMS:24; then len Cage(C,n)-(W-min L~Cage(C,n))..Cage(C,n) <= (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) by A95,REAL_1:49; then len Cage(C,n)-(W-min L~Cage(C,n))..Cage(C,n)+1 <= 1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) by AXIOMS:24; then A96: len(Cage(C,n):-W-min L~Cage(C,n)) <= 1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) by A85,FINSEQ_5:53; 1+(E-max L~Cage(C,n))..Cage(C,n)<=0+(W-min L~Cage(C,n))..Cage(C,n) by A94,NAT_1:38; then 1+(E-max L~Cage(C,n))..Cage(C,n)-(W-min L~Cage(C,n))..Cage(C,n)<=0 by REAL_1:86; then len Cage(C,n)+(1+(E-max L~Cage(C,n))..Cage(C,n)- (W-min L~Cage(C,n))..Cage(C,n)) <= len Cage(C,n)+0 by AXIOMS:24; then len Cage(C,n)+(1+(E-max L~Cage(C,n))..Cage(C,n))- (W-min L~Cage(C,n))..Cage(C,n) <= len Cage(C,n) by XCMPLX_1:29; then 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))- (W-min L~Cage(C,n))..Cage(C,n) <= len Cage(C,n) by XCMPLX_1:1; then A97: 1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) <= len Cage(C,n) by A95,XCMPLX_1:29; A98: 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)- (W-min L~Cage(C,n))..Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)- len Cage(C,n) = 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))- (W-min L~Cage(C,n))..Cage(C,n)+(W-min L~Cage(C,n))..Cage(C,n)- len Cage(C,n) by XCMPLX_1:29 .= 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))+(- (W-min L~Cage(C,n))..Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)- len Cage(C,n) by XCMPLX_0:def 8 .= 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))-len Cage(C,n) by XCMPLX_1: 139 .= 1+len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)-len Cage(C,n) by XCMPLX_1:1 .= 1+len Cage(C,n)-len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n) by XCMPLX_1:29 .= 1+(E-max L~Cage(C,n))..Cage(C,n) by XCMPLX_1:26; then A99: 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)- (W-min L~Cage(C,n))..Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)- len Cage(C,n) >= 0 by NAT_1:18; A100: Lower_Seq(C,n)/.(1+1) = Rotate(Cage(C,n),W-min L~Cage(C,n))/. (1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))) by A5,A81,A87,FINSEQ_5:55 .= Cage(C,n)/.(1+(E-max L~Cage(C,n))..Rotate(Cage(C,n), W-min L~Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)-'len Cage(C,n)) by A85,A96,A97,REVROT_1:17 .= Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)+1) by A95,A98,A99,BINARITH:def 3; A101: (N-max L~Cage(C,n))..Cage(C,n) <= (E-max L~Cage(C,n))..Cage(C,n) by A89,SPRECT_2:74; (N-max L~Cage(C,n))..Cage(C,n) > 1 by A89,SPRECT_2:73; then A102: (E-max L~Cage(C,n))..Cage(C,n) > 1 by A101,AXIOMS:22; (W-min L~Cage(C,n))..Cage(C,n) < len Cage(C,n) by A89,SPRECT_2:80; then (E-max L~Cage(C,n))..Cage(C,n) < len Cage(C,n) by A94,AXIOMS:22; then A103: (E-max L~Cage(C,n))..Cage(C,n)+1 <= len Cage(C,n) by NAT_1:38; Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)) = E-max L~Cage(C,n) by A86,FINSEQ_5:41; then (Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)+1))`1 = E-bound L~Cage(C,n) by A102,A103,JORDAN1E:24; then (h/.1)`1 = E-bound L~Cage(C,n) by A81,A82,A100,SPRECT_2:12; then (Rev h/.len h)`1 = E-bound L~Cage(C,n) by A84,FINSEQ_5:68; then (Rev h/.len Rev h)`1 = E-bound L~Cage(C,n) by FINSEQ_5:def 3; then A104: Rev h is_a_h.c._for Cage(C,n) by A83,A88,SPRECT_2:def 2; now let m be Nat; assume A105: m in dom <*Gauge(C,n)*(i,1)*>; then m in Seg 1 by FINSEQ_1:55; then m = 1 by FINSEQ_1:4,TARSKI:def 1; then <*Gauge(C,n)*(i,1)*>.m = Gauge(C,n)*(i,1) by FINSEQ_1:57; then A106: <*Gauge(C,n)*(i,1)*>/.m = Gauge(C,n)*(i,1) by A105,FINSEQ_4:def 4; width Gauge(C,n) >= 4 by A8,JORDAN8:13; then A107: 1 <= width Gauge(C,n) by AXIOMS:22; then Gauge(C,n)*(1,1)`1 <= Gauge(C,n)*(i,1)`1 by A1,SPRECT_3:25; hence W-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,1)*>/.m)`1 by A8,A106,A107,JORDAN1A:94; (Gauge(C,n)*(i,1))`1 <= Gauge(C,n)*(len Gauge(C,n),1)`1 by A1,A107,SPRECT_3:25; hence (<*Gauge(C,n)*(i,1)*>/.m)`1 <= E-bound L~Cage(C,n) by A8,A106,A107,JORDAN1A:92; thus S-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,1)*>/.m)`2 by A1,A106,JORDAN1A:93; S-bound L~Cage(C,n) = Gauge(C,n)*(i,1)`2 by A1,JORDAN1A:93; hence (<*Gauge(C,n)*(i,1)*>/.m)`2 <= N-bound L~Cage(C,n) by A106,SPRECT_1:24; end; then A108: <*Gauge(C,n)*(i,1)*> is_in_the_area_of Cage(C,n) by SPRECT_2:def 1; A109: Upper_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:21; then <*Gij*> is_in_the_area_of Cage(C,n) by A18,SPRECT_3:63; then v1 is_in_the_area_of Cage(C,n) by A18,A109,SPRECT_3:73; then A110: Gv1 is_in_the_area_of Cage(C,n) by A108,SPRECT_2:28; <*NE*> is_in_the_area_of Cage(C,n) by SPRECT_2:29; then A111: v is_in_the_area_of Cage(C,n) by A110,SPRECT_2:28; v = <*Gauge(C,n)*(i,1)*>^(v1^<*NE*>) by FINSEQ_1:45; then v/.1 = Gauge(C,n)*(i,1) by FINSEQ_5:16; then A112: (v/.1)`2 = S-bound L~Cage(C,n) by A1,JORDAN1A:93; len v = len Gv1 + 1 by FINSEQ_2:19; then v/.(len v) = NE by TOPREAL4:1; then (v/.len v)`2 = N-bound L~Cage(C,n) by PSCOMP_1:77; then v is_a_v.c._for Cage(C,n) by A111,A112,SPRECT_2:def 3; then L~Rev h meets L~v by A30,A70,A75,A79,A104,SPRECT_2:33; then L~h meets L~v by SPPOL_2:22; then consider x be set such that A113: x in L~h and A114: x in L~v by XBOOLE_0:3; A115: L~h c= L~Lower_Seq(C,n) by A7,JORDAN4:47; A116: L~v1 c= L~Upper_Seq(C,n) by A18,JORDAN3:77; L~v = L~(<*Gauge(C,n)*(i,1)*>^(v1^<*NE*>)) by FINSEQ_1:45 .= LSeg(Gauge(C,n)*(i,1),(v1^<*NE*>)/.1) \/ L~(v1^<*NE*>) by SPPOL_2:20 .= LSeg(Gauge(C,n)*(i,1),(v1^<*NE*>)/.1) \/ (L~v1 \/ LSeg(v1/.(len v1),NE)) by A19,SPPOL_2:19; then A117: x in LSeg(Gauge(C,n)*(i,1),(v1^<*NE*>)/.1) or x in L~v1 \/ LSeg(v1/.(len v1),NE) by A114,XBOOLE_0:def 2; Lower_Seq(C,n)/.1 = (Rotate(Cage(C,n),W-min L~Cage(C,n)):- E-max L~Cage(C,n))/.1 by JORDAN1E:def 2 .= E-max L~Cage(C,n) by FINSEQ_5:56; then A118: not E-max L~Cage(C,n) in L~h by A77,JORDAN5B:16; now per cases by A117,XBOOLE_0:def 2; suppose x in LSeg(Gauge(C,n)*(i,1),(v1^<*NE*>)/.1); then x in L~<*Gauge(C,n)*(i,1),Gij*> by A28,SPPOL_2:21; hence L~Lower_Seq(C,n) meets L~<*Gauge(C,n)*(i,1),Gij*> by A113,A115,XBOOLE_0:3; suppose A119: x in L~v1; then x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) by A113,A115,A116,XBOOLE_0:def 3; then x in {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:20; then A120: x = W-min L~Cage(C,n) by A113,A118,TARSKI:def 2; 1 in dom Upper_Seq(C,n) by A7,FINSEQ_3:27; then Upper_Seq(C,n).1 = Upper_Seq(C,n)/.1 by FINSEQ_4:def 4 .= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by A6,A24,FINSEQ_5:47 .= W-min L~Cage(C,n) by A23,FINSEQ_6:98; then x = Gij by A18,A119,A120,JORDAN1E:11; then x in LSeg(Gauge(C,n)*(i,1),Gij) by TOPREAL1:6; then x in L~<*Gauge(C,n)*(i,1),Gij*> by SPPOL_2:21; hence L~Lower_Seq(C,n) meets L~<*Gauge(C,n)*(i,1),Gij*> by A113,A115,XBOOLE_0:3; suppose A121: x in LSeg(v1/.(len v1),NE); x in L~Cage(C,n) by A4,A113,A115,XBOOLE_0:def 2; then x in LSeg(E-max L~Cage(C,n), NE) /\ L~Cage(C,n) by A25,A121,XBOOLE_0:def 3; then x in {E-max L~Cage(C,n)} by PSCOMP_1:112; hence L~Lower_Seq(C,n) meets L~<*Gauge(C,n)*(i,1),Gij*> by A113,A118,TARSKI:def 1; end; then L~<*Gauge(C,n)*(i,1),Gij*> meets L~Lower_Seq(C,n); hence LSeg(Gauge(C,n)*(i,1),Gij) meets L~Lower_Seq(C,n) by SPPOL_2:21; suppose A122: Gij in L~Upper_Seq(C,n) & Gij <> Upper_Seq(C,n).len Upper_Seq(C,n) & E-max L~Cage(C,n) = NE & i > 1; then A123: v1 is non empty by JORDAN1E:7; then len v1 <> 0 by FINSEQ_1:25; then len v1 > 0 by NAT_1:19; then A124: 0+1 <= len v1 by NAT_1:38; then A125: 1 in dom v1 by FINSEQ_3:27; A126: len v1 in dom v1 & len Upper_Seq(C,n) in dom Upper_Seq(C,n) by A7,A124,FINSEQ_3:27; A127: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; then A128: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by A127,FINSEQ_6:96; v1/.(len v1) = v1.(len v1) by A126,FINSEQ_4:def 4 .= Upper_Seq(C,n).len Upper_Seq(C,n) by A122,JORDAN1B:5 .= Upper_Seq(C,n)/.len Upper_Seq(C,n) by A126,FINSEQ_4:def 4 .= (Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n))/. ((E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))) by A6,A128,FINSEQ_5:45 .= E-max L~Cage(C,n) by A128,FINSEQ_5:48; then A129: Gv1/.len Gv1 = E-max L~Cage(C,n) by A123,SPRECT_3:11; A130: v1/.1 = v1.1 by A125,FINSEQ_4:def 4 .= Gij by A122,JORDAN3:58; 1+len v1 >= 1+1 by A124,REAL_1:55; then A131: len Gv1 >= 2 by FINSEQ_5:8; A132: not Gauge(C,n)*(i,1) in L~Upper_Seq(C,n) by A1,A122,Th52; rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by A7,SPPOL_2:18; then A133: not Gauge(C,n)*(i,1) in rng Upper_Seq(C,n) by A1,A122,Th52; not Gauge(C,n)*(i,1) in {Gij} by A122,A132,TARSKI:def 1; then A134: not Gauge(C,n)*(i,1) in rng <*Gij*> by FINSEQ_1:55; set ci = mid(Upper_Seq(C,n),Index(Gij,Upper_Seq(C,n))+1, len Upper_Seq(C,n)); now per cases; suppose A135: Gij <> Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1); rng ci c= rng Upper_Seq(C,n) by JORDAN3:28; then not Gauge(C,n)*(i,1) in rng ci by A133; then not Gauge(C,n)*(i,1) in rng <*Gij*> \/ rng ci by A134,XBOOLE_0:def 2; then not Gauge(C,n)*(i,1) in rng(<*Gij*>^ci) by FINSEQ_1:44; hence not Gauge(C,n)*(i,1) in rng v1 by A135,JORDAN3:def 4; suppose Gij = Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1); then v1 = ci by JORDAN3:def 4; then rng v1 c= rng Upper_Seq(C,n) by JORDAN3:28; hence not Gauge(C,n)*(i,1) in rng v1 by A133; end; then {Gauge(C,n)*(i,1)} misses rng v1 by ZFMISC_1:56; then A136: rng <*Gauge(C,n)*(i,1)*> misses rng v1 by FINSEQ_1:55; A137: <*Gauge(C,n)*(i,1)*> is one-to-one by FINSEQ_3:102; A138: v1 is_S-Seq by A122,JORDAN3:69; then v1 is one-to-one by TOPREAL1:def 10; then A139: Gv1 is one-to-one by A136,A137,FINSEQ_3:98; A140: <*Gauge(C,n)*(i,1)*> is special by SPPOL_2:39; A141: v1 is special by A138,TOPREAL1:def 10; (<*Gauge(C,n)*(i,1)*>/.len <*Gauge(C,n)*(i,1)*>)`1 = (<*Gauge(C,n)*(i,1)*>/.1)`1 by FINSEQ_1:56 .= Gauge(C,n)*(i,1)`1 by FINSEQ_4:25 .= (v1/.1)`1 by A1,A2,A130,GOBOARD5:3; then A142: Gv1 is special by A140,A141,GOBOARD2:13; A143: len Lower_Seq(C,n) >= 2+1 by JORDAN1E:19; then A144: len Lower_Seq(C,n) > 2 by NAT_1:38; A145: len Lower_Seq(C,n) > 1 by A143,AXIOMS:22; then h is S-Sequence_in_R2 by A144,JORDAN3:39; then Rev h is S-Sequence_in_R2 by SPPOL_2:47; then A146: 2 <= len Rev h & Rev h is one-to-one & Rev h is special by TOPREAL1:def 10; A147: Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:22; 3 <= len Lower_Seq(C,n) by JORDAN1E:19; then 2 <= len Lower_Seq(C,n) by AXIOMS:22; then A148: 2 in dom Lower_Seq(C,n) by FINSEQ_3:27; A149: len Lower_Seq(C,n) in dom Lower_Seq(C,n) by SCMFSA_7:12; then h is_in_the_area_of Cage(C,n) by A147,A148,SPRECT_2:26; then A150: Rev h is_in_the_area_of Cage(C,n) by SPRECT_3:68; A151: h is non empty by A144,A145,JORDAN1B:3; A152: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; A153: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; then A154: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by A152,FINSEQ_6:96; then 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 A5,FINSEQ_5:57 .= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by FINSEQ_6:def 1 .= W-min L~Cage(C,n) by A152,FINSEQ_6:98; then (Lower_Seq(C,n)/.len Lower_Seq(C,n))`1 = W-bound L~Cage(C,n) by PSCOMP_1:84; then (h/.len h)`1 = W-bound L~Cage(C,n) by A148,A149,SPRECT_2:13; then A155: (Rev h/.1)`1 = W-bound L~Cage(C,n) by A151,FINSEQ_5:68; A156: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:34; then A157: (E-max L~Cage(C,n))..Cage(C,n) < (E-min L~Cage(C,n))..Cage(C,n ) by SPRECT_2:75; A158: (E-min L~Cage(C,n))..Cage(C,n) <= (S-max L~Cage(C,n))..Cage(C,n) by A156,SPRECT_2:76; A159: (S-max L~Cage(C,n))..Cage(C,n) < (S-min L~Cage(C,n))..Cage(C,n) by A156,SPRECT_2:77; A160: (S-min L~Cage(C,n))..Cage(C,n) <= (W-min L~Cage(C,n))..Cage(C,n) by A156,SPRECT_2:78; (E-max L~Cage(C,n))..Cage(C,n) < (S-max L~Cage(C,n))..Cage(C,n) by A157,A158,AXIOMS: 22; then (E-max L~Cage(C,n))..Cage(C,n) < (S-min L~Cage(C,n))..Cage(C,n) by A159,AXIOMS:22; then A161: (E-max L~Cage(C,n))..Cage(C,n) < (W-min L~Cage(C,n))..Cage(C,n ) by A160,AXIOMS:22; then A162: (E-max L~Cage(C,n))..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) by A152,A153,SPRECT_5:10; 0 <= (E-max L~Cage(C,n))..Cage(C,n) by NAT_1:18; then len Cage(C,n)+0 <= len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n) by AXIOMS:24; then len Cage(C,n)-(W-min L~Cage(C,n))..Cage(C,n) <= (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) by A162,REAL_1:49; then len Cage(C,n)-(W-min L~Cage(C,n))..Cage(C,n)+1 <= 1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) by AXIOMS:24; then A163: len(Cage(C,n):-W-min L~Cage(C,n)) <= 1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) by A152,FINSEQ_5:53; 1+(E-max L~Cage(C,n))..Cage(C,n)<=0+(W-min L~Cage(C,n))..Cage(C,n) by A161,NAT_1:38; then 1+(E-max L~Cage(C,n))..Cage(C,n)-(W-min L~Cage(C,n))..Cage(C,n)<=0 by REAL_1:86; then len Cage(C,n)+(1+(E-max L~Cage(C,n))..Cage(C,n)- (W-min L~Cage(C,n))..Cage(C,n)) <= len Cage(C,n)+0 by AXIOMS:24; then len Cage(C,n)+(1+(E-max L~Cage(C,n))..Cage(C,n))- (W-min L~Cage(C,n))..Cage(C,n) <= len Cage(C,n) by XCMPLX_1:29; then 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))- (W-min L~Cage(C,n))..Cage(C,n) <= len Cage(C,n) by XCMPLX_1:1; then A164: 1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) <= len Cage(C,n) by A162,XCMPLX_1:29; A165: 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)- (W-min L~Cage(C,n))..Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)- len Cage(C,n) = 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))- (W-min L~Cage(C,n))..Cage(C,n)+(W-min L~Cage(C,n))..Cage(C,n)- len Cage(C,n) by XCMPLX_1:29 .= 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))+(- (W-min L~Cage(C,n))..Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)- len Cage(C,n) by XCMPLX_0:def 8 .= 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))-len Cage(C,n) by XCMPLX_1: 139 .= 1+len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)-len Cage(C,n) by XCMPLX_1:1 .= 1+len Cage(C,n)-len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n) by XCMPLX_1:29 .= 1+(E-max L~Cage(C,n))..Cage(C,n) by XCMPLX_1:26; then A166: 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)- (W-min L~Cage(C,n))..Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)- len Cage(C,n) >= 0 by NAT_1:18; A167: Lower_Seq(C,n)/.(1+1) = Rotate(Cage(C,n),W-min L~Cage(C,n))/. (1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))) by A5,A148,A154,FINSEQ_5:55 .= Cage(C,n)/.(1+(E-max L~Cage(C,n))..Rotate(Cage(C,n), W-min L~Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)-'len Cage(C,n)) by A152,A163,A164,REVROT_1:17 .= Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)+1) by A162,A165,A166,BINARITH:def 3; A168: (N-max L~Cage(C,n))..Cage(C,n) <= (E-max L~Cage(C,n))..Cage(C,n) by A156,SPRECT_2:74; (N-max L~Cage(C,n))..Cage(C,n) > 1 by A156,SPRECT_2:73; then A169: (E-max L~Cage(C,n))..Cage(C,n) > 1 by A168,AXIOMS:22; (W-min L~Cage(C,n))..Cage(C,n) < len Cage(C,n) by A156,SPRECT_2:80; then (E-max L~Cage(C,n))..Cage(C,n) < len Cage(C,n) by A161,AXIOMS:22; then A170: (E-max L~Cage(C,n))..Cage(C,n)+1 <= len Cage(C,n) by NAT_1:38; Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)) = E-max L~Cage(C,n) by A153,FINSEQ_5:41; then (Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)+1))`1 = E-bound L~Cage(C,n) by A169,A170,JORDAN1E:24; then (h/.1)`1 = E-bound L~Cage(C,n) by A148,A149,A167,SPRECT_2:12; then (Rev h/.len h)`1 = E-bound L~Cage(C,n) by A151,FINSEQ_5:68; then (Rev h/.len Rev h)`1 = E-bound L~Cage(C,n) by FINSEQ_5:def 3; then A171: Rev h is_a_h.c._for Cage(C,n) by A150,A155,SPRECT_2:def 2; now let m be Nat; assume A172: m in dom <*Gauge(C,n)*(i,1)*>; then m in Seg 1 by FINSEQ_1:55; then m = 1 by FINSEQ_1:4,TARSKI:def 1; then <*Gauge(C,n)*(i,1)*>.m = Gauge(C,n)*(i,1) by FINSEQ_1:57; then A173: <*Gauge(C,n)*(i,1)*>/.m = Gauge(C,n)*(i,1) by A172,FINSEQ_4:def 4; width Gauge(C,n) >= 4 by A8,JORDAN8:13; then A174: 1 <= width Gauge(C,n) by AXIOMS:22; then Gauge(C,n)*(1,1)`1 <= Gauge(C,n)*(i,1)`1 by A1,SPRECT_3:25; hence W-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,1)*>/.m)`1 by A8,A173,A174,JORDAN1A:94; (Gauge(C,n)*(i,1))`1 <= Gauge(C,n)*(len Gauge(C,n),1)`1 by A1,A174,SPRECT_3:25; hence (<*Gauge(C,n)*(i,1)*>/.m)`1 <= E-bound L~Cage(C,n) by A8,A173,A174,JORDAN1A:92; thus S-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,1)*>/.m)`2 by A1,A173,JORDAN1A:93; S-bound L~Cage(C,n) = Gauge(C,n)*(i,1)`2 by A1,JORDAN1A:93; hence (<*Gauge(C,n)*(i,1)*>/.m)`2 <= N-bound L~Cage(C,n) by A173,SPRECT_1:24; end; then A175: <*Gauge(C,n)*(i,1)*> is_in_the_area_of Cage(C,n) by SPRECT_2:def 1; A176: Upper_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:21; then <*Gij*> is_in_the_area_of Cage(C,n) by A122,SPRECT_3:63; then v1 is_in_the_area_of Cage(C,n) by A122,A176,SPRECT_3:73; then A177: Gv1 is_in_the_area_of Cage(C,n) by A175,SPRECT_2:28; Gv1/.1 = Gauge(C,n)*(i,1) by FINSEQ_5:16; then A178: (Gv1/.1)`2 = S-bound L~Cage(C,n) by A1,JORDAN1A:93; (Gv1/.len Gv1)`2 = N-bound L~Cage(C,n) by A122,A129,PSCOMP_1:77; then Gv1 is_a_v.c._for Cage(C,n) by A177,A178,SPRECT_2:def 3; then L~Rev h meets L~Gv1 by A131,A139,A142,A146,A171,SPRECT_2:33; then L~h meets L~Gv1 by SPPOL_2:22; then consider x be set such that A179: x in L~h and A180: x in L~Gv1 by XBOOLE_0:3; A181: L~h c= L~Lower_Seq(C,n) by A7,JORDAN4:47; A182: L~v1 c= L~Upper_Seq(C,n) by A122,JORDAN3:77; A183: L~Gv1 = LSeg(Gauge(C,n)*(i,1),v1/.1) \/ L~v1 by A123,SPPOL_2:20; Lower_Seq(C,n)/.1 = (Rotate(Cage(C,n),W-min L~Cage(C,n)):- E-max L~Cage(C,n))/.1 by JORDAN1E:def 2 .= E-max L~Cage(C,n) by FINSEQ_5:56; then A184: not E-max L~Cage(C,n) in L~h by A144,JORDAN5B:16; now per cases by A180,A183,XBOOLE_0:def 2; suppose x in LSeg(Gauge(C,n)*(i,1),v1/.1); then x in L~<*Gauge(C,n)*(i,1),Gij*> by A130,SPPOL_2:21; hence L~Lower_Seq(C,n) meets L~<*Gauge(C,n)*(i,1),Gij*> by A179,A181,XBOOLE_0:3; suppose A185: x in L~v1; then x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) by A179,A181,A182,XBOOLE_0:def 3; then x in {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:20; then A186: x = W-min L~Cage(C,n) by A179,A184,TARSKI:def 2; 1 in dom Upper_Seq(C,n) by A7,FINSEQ_3:27; then Upper_Seq(C,n).1 = Upper_Seq(C,n)/.1 by FINSEQ_4:def 4 .= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by A6,A128,FINSEQ_5:47 .= W-min L~Cage(C,n) by A127,FINSEQ_6:98; then x = Gij by A122,A185,A186,JORDAN1E:11; then x in LSeg(Gauge(C,n)*(i,1),Gij) by TOPREAL1:6; then x in L~<*Gauge(C,n)*(i,1),Gij*> by SPPOL_2:21; hence L~Lower_Seq(C,n) meets L~<*Gauge(C,n)*(i,1),Gij*> by A179,A181,XBOOLE_0:3; end; then L~<*Gauge(C,n)*(i,1),Gij*> meets L~Lower_Seq(C,n); hence LSeg(Gauge(C,n)*(i,1),Gij) meets L~Lower_Seq(C,n) by SPPOL_2:21; suppose A187: Gij in L~Lower_Seq(C,n); Gij in LSeg(Gauge(C,n)*(i,1),Gij) by TOPREAL1:6; hence LSeg(Gauge(C,n)*(i,1),Gij) meets L~Lower_Seq(C,n) by A187,XBOOLE_0:3; suppose A188: Gij in L~Upper_Seq(C,n) & Gij = Upper_Seq(C,n).len Upper_Seq(C,n); then v1 is non empty by JORDAN1E:7; then len v1 <> 0 by FINSEQ_1:25; then len v1 > 0 by NAT_1:19; then 0+1 <= len v1 by NAT_1:38; then A189: len v1 in dom v1 & len Upper_Seq(C,n) in dom Upper_Seq(C,n) by A7,FINSEQ_3:27; A190: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; then A191: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by A190,FINSEQ_6:96; A192: Upper_Seq(C,n).len Upper_Seq(C,n) = Upper_Seq(C,n)/.len Upper_Seq(C,n) by A189,FINSEQ_4:def 4 .= (Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n))/. ((E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))) by A6,A191,FINSEQ_5:45 .= E-max L~Cage(C,n) by A191,FINSEQ_5:48; A193: rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by A7,SPPOL_2:18; A194: E-max L~Cage(C,n) in rng Lower_Seq(C,n) by A5,FINSEQ_6:66; Gij in LSeg(Gauge(C,n)*(i,1),Gij) by TOPREAL1:6; hence LSeg(Gauge(C,n)*(i,1),Gij) meets L~Lower_Seq(C,n) by A188,A192,A193,A194,XBOOLE_0:3; end; hence thesis; end; theorem Th55: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 holds First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2)) in rng Upper_Seq(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; assume A1: n > 0; set Wmin = W-min L~Cage(C,n); set Emax = E-max L~Cage(C,n); set Wbo = W-bound L~Cage(C,n); set Ebo = E-bound L~Cage(C,n); set sr = (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2; set FiP = First_Point(L~Upper_Seq(C,n),Wmin,Emax,Vertical_Line sr); A2: Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by JORDAN1F:5; A3: Upper_Seq(C,n)/.len Upper_Seq(C,n) = E-max L~Cage(C,n) by JORDAN1F:7; then A4: L~Upper_Seq(C,n) is_an_arc_of Wmin,Emax by A2,TOPREAL1:31; Wbo < Ebo by SPRECT_1:33; then Wbo < sr & sr < Ebo by TOPREAL3:3; then Wmin`1 <= sr & sr <= Emax`1 by PSCOMP_1:84,104; then A5: L~Upper_Seq(C,n) meets Vertical_Line(sr) & L~Upper_Seq(C,n) /\ Vertical_Line(sr) is closed by A4,JORDAN6:64; then FiP in L~Upper_Seq(C,n) /\ Vertical_Line sr by A4,JORDAN5C:def 1; then A6: FiP in L~Upper_Seq(C,n) & FiP in Vertical_Line sr by XBOOLE_0:def 3; then consider t be Nat such that A7: 1 <= t & t+1 <= len Upper_Seq(C,n) and A8: FiP in LSeg(Upper_Seq(C,n),t) by SPPOL_2:13; Vertical_Line sr is closed by JORDAN6:33; then A9: FiP = First_Point (LSeg (Upper_Seq(C,n),t),Upper_Seq(C,n)/.t, Upper_Seq(C,n)/.(t+1),Vertical_Line sr) by A2,A3,A5,A7,A8,JORDAN5C:19; A10: LSeg(Upper_Seq(C,n),t) = LSeg(Upper_Seq(C,n)/.t,Upper_Seq(C,n)/.(t+1)) by A7,TOPREAL1:def 5; A11: FiP`1 = sr by A6,JORDAN6:34; t < len Upper_Seq(C,n) & 1 <= t+1 by A7,NAT_1:38; then A12: t in dom Upper_Seq(C,n) & t+1 in dom Upper_Seq(C,n) by A7,FINSEQ_3:27; A13: 1 <= Center Gauge(C,n) & Center Gauge(C,n) <= len Gauge(C,n) by JORDAN1B:12,14; now per cases by SPPOL_1:41; suppose LSeg(Upper_Seq(C,n),t) is vertical; then (Upper_Seq(C,n)/.t)`1 = sr & (Upper_Seq(C,n)/.(t+1))`1 = sr by A8,A10,A11,SPRECT_3:20; then Upper_Seq(C,n)/.t in {p where p is Point of TOP-REAL 2: p`1 = sr} & Upper_Seq(C,n)/.(t+1) in {p where p is Point of TOP-REAL 2: p`1 = sr}; then Upper_Seq(C,n)/.t in Vertical_Line sr & Upper_Seq(C,n)/.(t+1) in Vertical_Line sr by JORDAN6:def 6; then A14: LSeg(Upper_Seq(C,n),t) c= Vertical_Line sr by A10,JORDAN1A:23; A15: LSeg(Upper_Seq(C,n),t) is closed by SPPOL_1:40; Upper_Seq(C,n)/.t <> Upper_Seq(C,n)/.(t+1) by A12,GOBOARD7:31; then LSeg(Upper_Seq(C,n),t) is_an_arc_of Upper_Seq(C,n)/.t, Upper_Seq(C,n)/.(t+1) by A10,TOPREAL1:15; then First_Point (LSeg(Upper_Seq(C,n),t),Upper_Seq(C,n)/.t, Upper_Seq(C,n)/.(t+1),Vertical_Line sr) = Upper_Seq(C,n)/.t by A14,A15,JORDAN5C:7; hence FiP in rng Upper_Seq(C,n) by A9,A12,PARTFUN2:4; suppose LSeg(Upper_Seq(C,n),t) is horizontal; then A16: (Upper_Seq(C,n)/.t)`2 = (Upper_Seq(C,n)/.(t+1))`2 by A10,SPPOL_1:36; then A17: FiP`2 = (Upper_Seq(C,n)/.t)`2 by A8,A10,GOBOARD7:6; Upper_Seq(C,n) is_sequence_on Gauge(C,n) by Th4; then consider i1,j1,i2,j2 be Nat such that A18: [i1,j1] in Indices Gauge(C,n) and A19: Upper_Seq(C,n)/.t = Gauge(C,n)*(i1,j1) and A20: [i2,j2] in Indices Gauge(C,n) and A21: Upper_Seq(C,n)/.(t+1) = Gauge(C,n)*(i2,j2) and A22: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A7,JORDAN8:6; A23: 1 <= i1 & i1 <= len Gauge(C,n) & 1 <= j1 & j1 <= width Gauge(C,n) by A18,GOBOARD5:1; A24: 1 <= i2 & i2 <= len Gauge(C,n) & 1 <= j2 & j2 <= width Gauge(C,n) by A20,GOBOARD5:1; A25: j1 = j2 by A16,A18,A19,A20,A21,Th6; A26: Gauge(C,n)*(Center Gauge(C,n),j1)`1 = (W-bound C + E-bound C)/2 by A1,A23,Th43 .= FiP`1 by A11,Th41; Gauge(C,n)*(Center Gauge(C,n),j1)`2 = Gauge(C,n)*(1,j1)`2 by A13,A23,GOBOARD5:2 .= FiP`2 by A17,A19,A23,GOBOARD5:2; then A27: FiP = Gauge(C,n)*(Center Gauge(C,n),j1) by A26,TOPREAL3:11; now per cases by A22,A25,NAT_1:38; suppose A28: i1+1 = i2; i1 < i1+1 by NAT_1:38; then Gauge(C,n)*(i1,j1)`1 <= Gauge(C,n)*(i1+1,j1)`1 by A23,A24,A28,SPRECT_3:25; then Gauge(C,n)*(i1,j1)`1 <= FiP`1 & FiP`1 <= Gauge(C,n)*(i1+1,j1)`1 by A8,A10,A19,A21,A25,A28,TOPREAL1:9; then A29: i1 <= Center Gauge(C,n) & Center Gauge(C,n) <= i1+1 by A13,A23,A24,A26,A28,GOBOARD5:4; then i1 = Center Gauge(C,n) or i1 < Center Gauge(C,n) by REAL_1:def 5; then i1 = Center Gauge(C,n) or i1+1 <= Center Gauge(C,n) by NAT_1:38; then i1 = Center Gauge(C,n) or i1+1 = Center Gauge(C,n) by A29,AXIOMS:21; hence FiP in rng Upper_Seq(C,n) by A12,A19,A21,A25,A27,A28,PARTFUN2:4; suppose A30: i1 = i2+1; i2 < i2+1 by NAT_1:38; then Gauge(C,n)*(i2,j1)`1 <= Gauge(C,n)*(i2+1,j1)`1 by A23,A24,A30,SPRECT_3:25; then Gauge(C,n)*(i2,j1)`1 <= FiP`1 & FiP`1 <= Gauge(C,n)*(i2+1,j1)`1 by A8,A10,A19,A21,A25,A30,TOPREAL1:9; then A31: i2 <= Center Gauge(C,n) & Center Gauge(C,n) <= i2+1 by A13,A23,A24,A26,A30,GOBOARD5:4; then i2 = Center Gauge(C,n) or i2 < Center Gauge(C,n) by REAL_1:def 5; then i2 = Center Gauge(C,n) or i2+1 <= Center Gauge(C,n) by NAT_1:38; then i2 = Center Gauge(C,n) or i2+1 = Center Gauge(C,n) by A31,AXIOMS:21; hence FiP in rng Upper_Seq(C,n) by A12,A19,A21,A25,A27,A30,PARTFUN2:4; end; hence FiP in rng Upper_Seq(C,n); end; hence thesis; end; theorem Th56: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 holds Last_Point(L~Lower_Seq(C,n),E-max L~Cage(C,n),W-min L~Cage(C,n), Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2)) in rng Lower_Seq(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; assume A1: n > 0; set Wmin = W-min L~Cage(C,n); set Emax = E-max L~Cage(C,n); set Wbo = W-bound L~Cage(C,n); set Ebo = E-bound L~Cage(C,n); set sr = (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2; set LaP = Last_Point(L~Lower_Seq(C,n),Emax,Wmin,Vertical_Line sr); A2: Lower_Seq(C,n)/.1 = E-max L~Cage(C,n) by JORDAN1F:6; A3: Lower_Seq(C,n)/.len Lower_Seq(C,n) = W-min L~Cage(C,n) by JORDAN1F:8; then A4: L~Lower_Seq(C,n) is_an_arc_of Emax,Wmin by A2,TOPREAL1:31; then A5: L~Lower_Seq(C,n) is_an_arc_of Wmin,Emax by JORDAN5B:14; Wbo <= Ebo by SPRECT_1:23; then Wbo <= sr & sr <= Ebo by JORDAN6:2; then Wmin`1 <= sr & sr <= Emax`1 by PSCOMP_1:84,104; then A6: L~Lower_Seq(C,n) meets Vertical_Line(sr) & L~Lower_Seq(C,n) /\ Vertical_Line(sr) is closed by A5,JORDAN6:64; then LaP in L~Lower_Seq(C,n) /\ Vertical_Line sr by A4,JORDAN5C:def 2; then A7: LaP in L~Lower_Seq(C,n) & LaP in Vertical_Line sr by XBOOLE_0:def 3; then consider t be Nat such that A8: 1 <= t & t+1 <= len Lower_Seq(C,n) and A9: LaP in LSeg(Lower_Seq(C,n),t) by SPPOL_2:13; Vertical_Line sr is closed by JORDAN6:33; then A10: LaP = Last_Point (LSeg (Lower_Seq(C,n),t),Lower_Seq(C,n)/.t, Lower_Seq(C,n)/.(t+1),Vertical_Line sr) by A2,A3,A6,A8,A9,JORDAN5C:20; A11: LSeg(Lower_Seq(C,n),t) = LSeg(Lower_Seq(C,n)/.t,Lower_Seq(C,n)/.(t+1)) by A8,TOPREAL1:def 5; A12: LaP`1 = sr by A7,JORDAN6:34; t < len Lower_Seq(C,n) & 1 <= t+1 by A8,NAT_1:38; then A13: t in dom Lower_Seq(C,n) & t+1 in dom Lower_Seq(C,n) by A8,FINSEQ_3:27; now per cases by SPPOL_1:41; suppose LSeg(Lower_Seq(C,n),t) is vertical; then (Lower_Seq(C,n)/.t)`1 = sr & (Lower_Seq(C,n)/.(t+1))`1 = sr by A9,A11,A12,SPRECT_3:20; then Lower_Seq(C,n)/.t in {p where p is Point of TOP-REAL 2: p`1 = sr} & Lower_Seq(C,n)/.(t+1) in {p where p is Point of TOP-REAL 2: p`1 = sr}; then Lower_Seq(C,n)/.t in Vertical_Line sr & Lower_Seq(C,n)/.(t+1) in Vertical_Line sr by JORDAN6:def 6; then A14: LSeg(Lower_Seq(C,n),t) c= Vertical_Line sr by A11,JORDAN1A:23; A15: LSeg(Lower_Seq(C,n),t) is closed by SPPOL_1:40; Lower_Seq(C,n)/.t <> Lower_Seq(C,n)/.(t+1) by A13,GOBOARD7:31; then LSeg(Lower_Seq(C,n),t) is_an_arc_of Lower_Seq(C,n)/.t, Lower_Seq(C,n)/.(t+1) by A11,TOPREAL1:15; then Last_Point (LSeg(Lower_Seq(C,n),t),Lower_Seq(C,n)/.t, Lower_Seq(C,n)/.(t+1),Vertical_Line sr) = Lower_Seq(C,n)/.(t+1) by A14,A15,JORDAN5C:7; hence LaP in rng Lower_Seq(C,n) by A10,A13,PARTFUN2:4; suppose LSeg(Lower_Seq(C,n),t) is horizontal; then A16: (Lower_Seq(C,n)/.t)`2 = (Lower_Seq(C,n)/.(t+1))`2 by A11,SPPOL_1:36; then A17: LaP`2 = (Lower_Seq(C,n)/.t)`2 by A9,A11,GOBOARD7:6; Lower_Seq(C,n) is_sequence_on Gauge(C,n) by Th5; then consider i1,j1,i2,j2 be Nat such that A18: [i1,j1] in Indices Gauge(C,n) and A19: Lower_Seq(C,n)/.t = Gauge(C,n)*(i1,j1) and A20: [i2,j2] in Indices Gauge(C,n) and A21: Lower_Seq(C,n)/.(t+1) = Gauge(C,n)*(i2,j2) and A22: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A8,JORDAN8:6; A23: 1 <= i1 & i1 <= len Gauge(C,n) & 1 <= j1 & j1 <= width Gauge(C,n) by A18,GOBOARD5:1; A24: 1 <= i2 & i2 <= len Gauge(C,n) & 1 <= j2 & j2 <= width Gauge(C,n) by A20,GOBOARD5:1; A25: j1 = j2 by A16,A18,A19,A20,A21,Th6; A26: 1 <= Center Gauge(C,n) & Center Gauge(C,n) <= len Gauge(C,n) by JORDAN1B:12,14; A27: Gauge(C,n)*(Center Gauge(C,n),j1)`1 = (W-bound C + E-bound C)/2 by A1,A23,Th43 .= LaP`1 by A12,Th41; Gauge(C,n)*(Center Gauge(C,n),j1)`2 = Gauge(C,n)*(1,j1)`2 by A23,A26,GOBOARD5:2 .= LaP`2 by A17,A19,A23,GOBOARD5:2; then A28: LaP = Gauge(C,n)*(Center Gauge(C,n),j1) by A27,TOPREAL3:11; now per cases by A22,A25,NAT_1:38; suppose A29: i1+1 = i2; i1 < i1+1 by NAT_1:38; then Gauge(C,n)*(i1,j1)`1 <= Gauge(C,n)*(i1+1,j1)`1 by A23,A24,A29,SPRECT_3:25; then Gauge(C,n)*(i1,j1)`1 <= LaP`1 & LaP`1 <= Gauge(C,n)*(i1+1,j1)`1 by A9,A11,A19,A21,A25,A29,TOPREAL1:9; then A30: i1 <= Center Gauge(C,n) & Center Gauge(C,n) <= i1+1 by A23,A24,A26,A27,A29,GOBOARD5:4; then i1 = Center Gauge(C,n) or i1 < Center Gauge(C,n) by REAL_1:def 5; then i1 = Center Gauge(C,n) or i1+1 <= Center Gauge(C,n) by NAT_1:38; then i1 = Center Gauge(C,n) or i1+1 = Center Gauge(C,n) by A30,AXIOMS:21; hence LaP in rng Lower_Seq(C,n) by A13,A19,A21,A25,A28,A29,PARTFUN2:4; suppose A31: i1 = i2+1; i2 < i2+1 by NAT_1:38; then Gauge(C,n)*(i2,j1)`1 <= Gauge(C,n)*(i2+1,j1)`1 by A23,A24,A31,SPRECT_3:25; then Gauge(C,n)*(i2,j1)`1 <= LaP`1 & LaP`1 <= Gauge(C,n)*(i2+1,j1)`1 by A9,A11,A19,A21,A25,A31,TOPREAL1:9; then A32: i2 <= Center Gauge(C,n) & Center Gauge(C,n) <= i2+1 by A23,A24,A26,A27,A31,GOBOARD5:4; then i2 = Center Gauge(C,n) or i2 < Center Gauge(C,n) by REAL_1:def 5; then i2 = Center Gauge(C,n) or i2+1 <= Center Gauge(C,n) by NAT_1:38; then i2 = Center Gauge(C,n) or i2+1 = Center Gauge(C,n) by A32,AXIOMS:21; hence LaP in rng Lower_Seq(C,n) by A13,A19,A21,A25,A28,A31,PARTFUN2:4; end; hence LaP in rng Lower_Seq(C,n); end; hence thesis; end; theorem Th57: for f be S-Sequence_in_R2 for p be Point of TOP-REAL 2 st p in rng f holds R_Cut(f,p) = mid(f,1,p..f) proof let f be S-Sequence_in_R2; let p be Point of TOP-REAL 2; assume A1: p in rng f; then consider i be Nat such that A2: i in dom f and A3: f.i = p by FINSEQ_2:11; A4: 0+1 <= i & i <= len f by A2,FINSEQ_3:27; then A5: i-1 >= 0 by REAL_1:84; len f >= 2 by TOPREAL1:def 10; then rng f c= L~f by SPPOL_2:18; then A6: 1 <= Index(p,f) & Index(p,f) < len f by A1,JORDAN3:41; per cases by A4,REAL_1:def 5; suppose A7: 1 < i; then A8: Index(p,f) + 1 = i by A3,A4,JORDAN3:45; 1 <= len f by A4,AXIOMS:22; then 1 in dom f by FINSEQ_3:27; then p <> f.1 by A2,A3,A7,FUNCT_1:def 8; then A9: R_Cut(f,p) = mid(f,1,Index(p,f))^<*p*> by JORDAN3:def 5; A10: len mid(f,1,i) = i-'1+1 by A4,JORDAN4:20 .= i by A4,AMI_5:4; A11: len mid(f,1,Index(p,f)) = Index(p,f)-'1+1 by A6,JORDAN4:20 .= i-'1 by A6,A8,JORDAN4:3; then A12: len (mid(f,1,Index(p,f))^<*p*>) = i-'1+1 by FINSEQ_2:19 .= i by A4,AMI_5:4; now let j be Nat; assume j in Seg i; then A13: 1 <= j & j <= i by FINSEQ_1:3; now per cases by A13,REAL_1:def 5; suppose j < i; then A14: j <= Index(p,f) by A8,NAT_1:38; then j <= i-1 by A8,XCMPLX_1:26; then j <= i-'1 by A5,BINARITH:def 3; then A15: j in dom mid(f,1,Index(p,f)) by A11,A13,FINSEQ_3:27; thus mid(f,1,i).j = f.j by A4,A13,JORDAN3:32 .= mid(f,1,Index(p,f)).j by A6,A13,A14,JORDAN3:32 .= (mid(f,1,Index(p,f))^<*p*>).j by A15,FINSEQ_1:def 7; suppose A16: j = i; A17: i-'1+1 = i by A4,AMI_5:4; thus mid(f,1,i).j = f.j by A4,A13,JORDAN3:32 .= (mid(f,1,Index(p,f))^<*p*>).j by A3,A11,A16,A17,FINSEQ_1:59; end; hence mid(f,1,i).j = (mid(f,1,Index(p,f))^<*p*>).j; end; then mid(f,1,i) = R_Cut(f,p) by A9,A10,A12,FINSEQ_2:10; hence R_Cut(f,p) = mid(f,1,p..f) by A2,A3,FINSEQ_5:12; suppose A18: 1 = i; then A19: R_Cut(f,p) = <*p*> by A3,JORDAN3:def 5; A20: p = f/.1 by A2,A3,A18,FINSEQ_4:def 4; then p..f = 1 by FINSEQ_6:47; hence R_Cut(f,p) = mid(f,1,p..f) by A4,A18,A19,A20,JORDAN4:27; end; theorem Th58: for f be S-Sequence_in_R2 for Q be closed Subset of TOP-REAL 2 st L~f meets Q & not f/.1 in Q & First_Point(L~f,f/.1,f/.len f,Q) in rng f holds L~mid(f,1,First_Point(L~f,f/.1,f/.len f,Q)..f) /\ Q = {First_Point(L~f,f/.1,f/.len f,Q)} proof let f be S-Sequence_in_R2; let Q be closed Subset of TOP-REAL 2; assume that A1: L~f meets Q and A2: not f/.1 in Q and A3: First_Point(L~f,f/.1,f/.len f,Q) in rng f; L~R_Cut(f,First_Point(L~f,f/.1,f/.len f,Q)) /\ Q = {First_Point(L~f,f/.1,f/.len f,Q)} by A1,A2,SPRECT_4:1; hence thesis by A3,Th57; end; theorem Th59: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 for k be Nat st 1 <= k & k < First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2)).. Upper_Seq(C,n) holds (Upper_Seq(C,n)/.k)`1 < (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2 proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; assume A1: n > 0; let k be Nat such that A2: 1 <= k and A3: k < First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2)).. Upper_Seq(C,n); set Wmin = W-min L~Cage(C,n); set Emax = E-max L~Cage(C,n); set Wbo = W-bound L~Cage(C,n); set Ebo = E-bound L~Cage(C,n); set sr = (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2; set US = Upper_Seq(C,n); set FiP = First_Point(L~US,Wmin,Emax,Vertical_Line sr); A4: k > 0 by A2,AXIOMS:22; Wbo < Ebo by SPRECT_1:33; then A5: Wbo < sr & sr < Ebo by TOPREAL3:3; defpred P[Nat] means 1 <= $1 & $1 < FiP..US implies (US/.$1)`1 < sr; for k be non empty Nat holds P[k] proof A6: P[1] proof assume 1 <= 1 & 1 < FiP..US; US/.1 = Wmin by JORDAN1F:5; hence (US/.1)`1 < sr by A5,PSCOMP_1:84; end; A7: for k be non empty Nat st P[k] holds P[k+1] proof let k be non empty Nat; assume A8: 1 <= k & k < FiP..US implies (US/.k)`1 < sr; assume that A9: 1 <= k+1 and A10: k+1 < FiP..US; A11: k >= 1 by RLVECT_1:99; A12: FiP in rng US by A1,Th55; then A13: FiP..Upper_Seq(C,n) in dom Upper_Seq(C,n) by FINSEQ_4:30; then A14: 1 <= FiP..US & FiP..US <= len US by FINSEQ_3:27; then A15: k+1 <= len US by A10,AXIOMS:22; US is_sequence_on Gauge(C,n) by Th4; then consider i1,j1,i2,j2 be Nat such that A16: [i1,j1] in Indices Gauge(C,n) and A17: US/.k = Gauge(C,n)*(i1,j1) and A18: [i2,j2] in Indices Gauge(C,n) and A19: US/.(k+1) = Gauge(C,n)*(i2,j2) and A20: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A11,A15,JORDAN8:6; A21: 1 <= i1 & i1 <= len Gauge(C,n) & 1 <= j1 & j1 <= width Gauge(C,n) by A16,GOBOARD5:1; A22: 1 <= i2 & i2 <= len Gauge(C,n) & 1 <= j2 & j2 <= width Gauge(C,n) by A18,GOBOARD5:1; A23: 1 <= Center Gauge(C,n) & Center Gauge(C,n) <= len Gauge(C,n) by JORDAN1B:12,14; set GC1 = Gauge(C,n)*(Center Gauge(C,n),1); 4 <= len Gauge(C,n) by JORDAN8:13; then 1 <= len Gauge(C,n) by AXIOMS:22; then A24: 1 <= width Gauge(C,n) by JORDAN8:def 1; then A25: GC1`1 = (W-bound C + E-bound C)/2 by A1,Th43 .= sr by Th41; A26: i1+1 >= 1 by NAT_1:29; A27: US/.1 = Wmin by JORDAN1F:5; A28: US/.len US = Emax by JORDAN1F:7; now per cases by A20; suppose i1 = i2 & j1+1 = j2; then (US/.k)`1 = Gauge(C,n)*(i2,1)`1 by A17,A21,GOBOARD5:3 .= (US/.(k+1))`1 by A19,A22,GOBOARD5:3; hence (US/.(k+1))`1 < sr by A8,A10,NAT_1:38,RLVECT_1:99; suppose A29: i1+1 = i2 & j1 = j2; i1 < Center Gauge(C,n) by A8,A10,A17,A21,A23,A24,A25,JORDAN1A:39, NAT_1:38,RLVECT_1:99; then i1+1 <= Center Gauge(C,n) by NAT_1:38; then A30: (US/.(k+1))`1 <= sr by A19,A21,A23,A24,A25,A26,A29,JORDAN1A:39; now assume (US/.(k+1))`1 = sr; then US/.(k+1) in {p where p is Point of TOP-REAL 2 : p`1 = sr}; then A31: US/.(k+1) in Vertical_Line sr by JORDAN6:def 6; A32: k+1 >= 1+1 by A11,REAL_1:55; len mid(US,1,FiP..US) = FiP..US-'1+1 by A14,JORDAN4:20 .= FiP..US by A14,AMI_5:4; then len mid(US,1,FiP..US) >= 2 by A10,A32,AXIOMS:22; then A33: rng mid(US,1,FiP..US) c= L~mid(US,1,FiP..US) by SPPOL_2:18; A34: mid(US,1,FiP..US) = US|(FiP..US) by A14,JORDAN3:25; A35: US|Seg(FiP..US) = US|(FiP..US) by TOPREAL1:def 1; A36: k+1 in dom US by A9,A15,FINSEQ_3:27; k+1 in Seg (FiP..US) by A9,A10,FINSEQ_1:3; then A37: US/.(k+1) in rng mid(US,1,FiP..US) by A34,A35,A36,PARTFUN2:36; A38: Vertical_Line sr is closed by JORDAN6:33; A39: L~US is_an_arc_of Wmin,Emax by A27,A28,TOPREAL1:31; Wmin`1 <= sr & sr <= Emax`1 by A5,PSCOMP_1:84,104; then A40: L~US meets Vertical_Line sr by A39,JORDAN6:64; A41: now assume US/.1 in Vertical_Line sr; then Wmin`1 = sr by A27,JORDAN6:34; hence contradiction by A5,PSCOMP_1:84; end; First_Point(L~US,US/.1,US/.len US,Vertical_Line sr) in rng US by A1,A27,A28,Th55; then L~mid(US,1,FiP..US) /\ Vertical_Line sr = {FiP} by A27,A28,A38,A40,A41,Th58; then US/.(k+1) in {FiP} by A31,A33,A37,XBOOLE_0:def 3; then A42: US/.(k+1) = FiP by TARSKI:def 1; US/.(FiP..US) = FiP by A12,FINSEQ_5:41; hence contradiction by A10,A13,A36,A42,PARTFUN2:17; end; hence (US/.(k+1))`1 < sr by A30,REAL_1:def 5; suppose i1 = i2+1 & j1 = j2; then i2 < i1 by NAT_1:38; then (US/.(k+1))`1 <= (US/.k)`1 by A17,A19,A21,A22,JORDAN1A:39; hence (US/.(k+1))`1 < sr by A8,A10,AXIOMS:22,NAT_1:38,RLVECT_1:99; suppose i1 = i2 & j1 = j2+1; then (US/.k)`1 = Gauge(C,n)*(i2,1)`1 by A17,A21,GOBOARD5:3 .= (US/.(k+1))`1 by A19,A22,GOBOARD5:3; hence (US/.(k+1))`1 < sr by A8,A10,NAT_1:38,RLVECT_1:99; end; hence (US/.(k+1))`1 < sr; end; thus for k being non empty Nat holds P[k] from Ind_from_1(A6,A7); end; hence thesis by A2,A3,A4; end; theorem Th60: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 for k be Nat st 1 <= k & k < First_Point(L~Rev Lower_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2)).. Rev Lower_Seq(C,n) holds (Rev Lower_Seq(C,n)/.k)`1 < (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2 proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; assume A1: n > 0; let k be Nat such that A2: 1 <= k and A3: k < First_Point(L~Rev Lower_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n),Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2)) ..Rev Lower_Seq(C,n); set Wmin = W-min L~Cage(C,n); set Emax = E-max L~Cage(C,n); set Wbo = W-bound L~Cage(C,n); set Ebo = E-bound L~Cage(C,n); set sr = (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2; set LS = Lower_Seq(C,n); set RLS = Rev LS; set FiP = First_Point(L~RLS,Wmin,Emax,Vertical_Line sr); set LaP = Last_Point(L~LS,Emax,Wmin,Vertical_Line sr); A4: L~RLS = L~LS by SPPOL_2:22; A5: rng RLS = rng LS by FINSEQ_5:60; A6: len RLS = len LS by FINSEQ_5:def 3; A7: k > 0 by A2,AXIOMS:22; Wbo < Ebo by SPRECT_1:33; then A8: Wbo < sr & sr < Ebo by TOPREAL3:3; defpred P[Nat] means 1 <= $1 & $1 < FiP..RLS implies (RLS/.$1)`1 < sr; for k be non empty Nat holds P[k] proof A9: P[1] proof assume 1 <= 1 & 1 < FiP..RLS; RLS/.1 = LS/.len LS by FINSEQ_5:68 .= Wmin by JORDAN1F:8; hence (RLS/.1)`1 < sr by A8,PSCOMP_1:84; end; A10: for k be non empty Nat st P[k] holds P[k+1] proof let k be non empty Nat; assume A11: 1 <= k & k < FiP..RLS implies (RLS/.k)`1 < sr; assume that A12: 1 <= k+1 and A13: k+1 < FiP..RLS; A14: k >= 1 by RLVECT_1:99; A15: LS/.1 = Emax by JORDAN1F:6; LS/.len LS = Wmin by JORDAN1F:8; then A16: L~LS is_an_arc_of Emax,Wmin by A15,TOPREAL1:31; then A17: L~LS is_an_arc_of Wmin,Emax by JORDAN5B:14; Wbo <= Ebo by SPRECT_1:23; then Wbo <= sr & sr <= Ebo by JORDAN6:2; then Wmin`1 <= sr & sr <= Emax`1 by PSCOMP_1:84,104; then L~LS meets Vertical_Line(sr) & L~LS /\ Vertical_Line(sr) is closed by A17,JORDAN6:64; then A18: FiP = LaP by A4,A16,JORDAN5C:18; then A19: FiP in rng RLS by A1,A5,Th56; then A20: FiP..RLS in dom RLS by FINSEQ_4:30; then A21: 1 <= FiP..RLS & FiP..RLS <= len RLS by FINSEQ_3:27; then A22: k+1 <= len RLS by A13,AXIOMS:22; LS is_sequence_on Gauge(C,n) by Th5; then RLS is_sequence_on Gauge(C,n) by JORDAN9:7; then consider i1,j1,i2,j2 be Nat such that A23: [i1,j1] in Indices Gauge(C,n) and A24: RLS/.k = Gauge(C,n)*(i1,j1) and A25: [i2,j2] in Indices Gauge(C,n) and A26: RLS/.(k+1) = Gauge(C,n)*(i2,j2) and A27: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A14,A22,JORDAN8:6; A28: 1 <= i1 & i1 <= len Gauge(C,n) & 1 <= j1 & j1 <= width Gauge(C,n) by A23,GOBOARD5:1; A29: 1 <= i2 & i2 <= len Gauge(C,n) & 1 <= j2 & j2 <= width Gauge(C,n) by A25,GOBOARD5:1; A30: 1 <= Center Gauge(C,n) & Center Gauge(C,n) <= len Gauge(C,n) by JORDAN1B:12,14; set GC1 = Gauge(C,n)*(Center Gauge(C,n),1); 4 <= len Gauge(C,n) by JORDAN8:13; then 1 <= len Gauge(C,n) by AXIOMS:22; then A31: 1 <= width Gauge(C,n) by JORDAN8:def 1; then A32: GC1`1 = (W-bound C + E-bound C)/2 by A1,Th43 .= sr by Th41; A33: i1+1 >= 1 by NAT_1:29; A34: RLS/.1 = LS/.len LS by FINSEQ_5:68 .= Wmin by JORDAN1F:8; A35: RLS/.len RLS = LS/.1 by A6,FINSEQ_5:68 .= Emax by JORDAN1F:6; now per cases by A27; suppose i1 = i2 & j1+1 = j2; then (RLS/.k)`1 = Gauge(C,n)*(i2,1)`1 by A24,A28,GOBOARD5:3 .= (RLS/.(k+1))`1 by A26,A29,GOBOARD5:3; hence (RLS/.(k+1))`1 < sr by A11,A13,NAT_1:38,RLVECT_1:99; suppose A36: i1+1 = i2 & j1 = j2; i1 < Center Gauge(C,n) by A11,A13,A24,A28,A30,A31,A32,JORDAN1A:39, NAT_1:38,RLVECT_1:99; then i1+1 <= Center Gauge(C,n) by NAT_1:38; then A37: (RLS/.(k+1))`1 <= sr by A26,A28,A30,A31,A32,A33,A36,JORDAN1A:39; now assume (RLS/.(k+1))`1 = sr; then RLS/.(k+1) in {p where p is Point of TOP-REAL 2 : p`1 = sr}; then A38: RLS/.(k+1) in Vertical_Line sr by JORDAN6:def 6; A39: k+1 >= 1+1 by A14,REAL_1:55; len mid(RLS,1,FiP..RLS) = FiP..RLS-'1+1 by A21,JORDAN4:20 .= FiP..RLS by A21,AMI_5:4; then len mid(RLS,1,FiP..RLS) >= 2 by A13,A39,AXIOMS:22; then A40: rng mid(RLS,1,FiP..RLS) c= L~mid(RLS,1,FiP..RLS) by SPPOL_2:18; A41: mid(RLS,1,FiP..RLS) = RLS|(FiP..RLS) by A21,JORDAN3:25; A42: RLS|Seg(FiP..RLS) = RLS|(FiP..RLS) by TOPREAL1:def 1; A43: k+1 in dom RLS by A12,A22,FINSEQ_3:27; k+1 in Seg (FiP..RLS) by A12,A13,FINSEQ_1:3; then A44: RLS/.(k+1) in rng mid(RLS,1,FiP..RLS) by A41,A42,A43,PARTFUN2:36; A45: Vertical_Line sr is closed by JORDAN6:33; A46: RLS is_S-Seq by SPPOL_2:47; then A47: L~RLS is_an_arc_of Wmin,Emax by A34,A35,TOPREAL1:31; Wmin`1 <= sr & sr <= Emax`1 by A8,PSCOMP_1:84,104; then A48: L~RLS meets Vertical_Line sr by A47,JORDAN6:64; A49: now assume RLS/.1 in Vertical_Line sr; then Wmin`1 = sr by A34,JORDAN6:34; hence contradiction by A8,PSCOMP_1:84; end; First_Point(L~RLS,RLS/.1,RLS/.len RLS,Vertical_Line sr) in rng RLS by A1,A5,A18,A34,A35,Th56; then L~mid(RLS,1,FiP..RLS) /\ Vertical_Line sr = {FiP} by A34,A35,A45,A46,A48,A49,Th58; then RLS/.(k+1) in {FiP} by A38,A40,A44,XBOOLE_0:def 3; then A50: RLS/.(k+1) = FiP by TARSKI:def 1; RLS/.(FiP..RLS) = FiP by A19,FINSEQ_5:41; hence contradiction by A13,A20,A43,A50,PARTFUN2:17; end; hence (RLS/.(k+1))`1 < sr by A37,REAL_1:def 5; suppose i1 = i2+1 & j1 = j2; then i2 < i1 by NAT_1:38; then (RLS/.(k+1))`1 <= (RLS/.k)`1 by A24,A26,A28,A29,JORDAN1A:39; hence (RLS/.(k+1))`1 < sr by A11,A13,AXIOMS:22,NAT_1:38,RLVECT_1:99; suppose i1 = i2 & j1 = j2+1; then (RLS/.k)`1 = Gauge(C,n)*(i2,1)`1 by A24,A28,GOBOARD5:3 .= (RLS/.(k+1))`1 by A26,A29,GOBOARD5:3; hence (RLS/.(k+1))`1 < sr by A11,A13,NAT_1:38,RLVECT_1:99; end; hence (RLS/.(k+1))`1 < sr; end; thus for k being non empty Nat holds P[k] from Ind_from_1(A9,A10); end; hence thesis by A2,A3,A7; end; theorem Th61: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 for q be Point of TOP-REAL 2 holds q in rng mid(Upper_Seq(C,n),2,First_Point(L~Upper_Seq(C,n), W-min L~Cage(C,n),E-max L~Cage(C,n),Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))..Upper_Seq(C,n)) implies q`1 <= (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2 proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; assume A1: n > 0; let q be Point of TOP-REAL 2; set Wmin = W-min L~Cage(C,n); set Emax = E-max L~Cage(C,n); set Wbo = W-bound L~Cage(C,n); set Ebo = E-bound L~Cage(C,n); set sr = (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2; set US = Upper_Seq(C,n); set FiP = First_Point(L~US,Wmin,Emax,Vertical_Line sr); assume q in rng mid(US,2,FiP..US); then consider k be Nat such that A2: k in dom mid(US,2,FiP..US) and A3: q = mid(US,2,FiP..US)/.k by PARTFUN2:4; A4: FiP in rng US by A1,Th55; then A5: FiP..US in dom US by FINSEQ_4:30; then A6: 1 <= FiP..US & FiP..US <= len US by FINSEQ_3:27; A7: US/.1 = Wmin by JORDAN1F:5; then A8: Wmin in rng US by FINSEQ_6:46; US/.len US = Emax by JORDAN1F:7; then A9: L~US is_an_arc_of Wmin,Emax by A7,TOPREAL1:31; Wbo < Ebo by SPRECT_1:33; then A10: Wbo < sr & sr < Ebo by TOPREAL3:3; then Wmin`1 <= sr & sr <= Emax`1 by PSCOMP_1:84,104; then L~US meets Vertical_Line sr & L~US /\ Vertical_Line sr is closed by A9,JORDAN6:64; then FiP in L~US /\ Vertical_Line sr by A9,JORDAN5C:def 1; then FiP in L~US & FiP in Vertical_Line sr by XBOOLE_0:def 3; then A11: FiP`1 = sr by JORDAN6:34; now assume FiP..US = 1; then FiP..US = (US/.1)..US by FINSEQ_6:47 .= Wmin..US by JORDAN1F:5; then FiP = Wmin by A4,A8,FINSEQ_5:10; hence contradiction by A10,A11,PSCOMP_1:84; end; then FiP..US > 1 by A6,REAL_1:def 5; then A12: 1+1+0 <= FiP..US by NAT_1:38; k+2 >= 1+1 by NAT_1:29; then k+2-1 >= 1+1-1 by REAL_1:49; then A13: k+2-1 >= 0 by AXIOMS:22; len US >= 3 by JORDAN1E:19; then len US >= 2 by AXIOMS:22; then 2 in dom US by FINSEQ_3:27; then A14: mid(US,2,FiP..US)/.k = US/.(k+2-'1) by A2,A5,A12,SPRECT_2:7 .= US/.(k+2-1) by A13,BINARITH:def 3 .= US/.(k+(2-1)) by XCMPLX_1:29; A15: 1 <= k+1 by NAT_1:29; A16: k <= len mid(US,2,FiP..US) by A2,FINSEQ_3:27; FiP..US-2 >= 0 by A12,REAL_1:84; then FiP..US-'2 = FiP..US-2 by BINARITH:def 3; then len mid(US,2,FiP..US) = FiP..US-2+1 by A6,A12,JORDAN4:20; then k < FiP..US-2+1+1 by A16,NAT_1:38; then k < FiP..US-2+(1+1) by XCMPLX_1:1; then k < FiP..US by XCMPLX_1:27; then A17: k+1 <= FiP..US by NAT_1:38; per cases by A17,REAL_1:def 5; suppose k+1 < FiP..US; hence q`1 <= sr by A1,A3,A14,A15,Th59; suppose k+1 = FiP..US; hence q`1 <= sr by A3,A4,A11,A14,FINSEQ_5:41; end; theorem Th62: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 holds First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))`2 > Last_Point(L~Lower_Seq(C,n),E-max L~Cage(C,n),W-min L~Cage(C,n), Vertical_Line((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))`2 proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; set sr = (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2; set Wmin = W-min L~Cage(C,n); set Emax = E-max L~Cage(C,n); set Nbo = N-bound L~Cage(C,n); set Ebo = E-bound L~Cage(C,n); set Sbo = S-bound L~Cage(C,n); set Wbo = W-bound L~Cage(C,n); set SW = SW-corner L~Cage(C,n); set FiP = First_Point(L~Upper_Seq(C,n),Wmin,Emax,Vertical_Line sr); set LaP = Last_Point(L~Lower_Seq(C,n),Emax,Wmin,Vertical_Line sr); set g = mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n))^<*|[Ebo,FiP`2]|*>; set h = <*SW*>^((Rev Lower_Seq(C,n))-:LaP)^<*|[sr,Nbo]|*>; assume A1: n > 0; A2: Upper_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:21; len Upper_Seq(C,n) >= 3 by JORDAN1E:19; then A3: len Upper_Seq(C,n) > 2 by AXIOMS:22; then A4: 2 in dom Upper_Seq(C,n) by FINSEQ_3:27; A5: Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by JORDAN1F:5; A6: Upper_Seq(C,n)/.len Upper_Seq(C,n) = E-max L~Cage(C,n) by JORDAN1F:7; then A7: L~Upper_Seq(C,n) is_an_arc_of Wmin,Emax by A5,TOPREAL1:31; Wbo < Ebo by SPRECT_1:33; then A8: Wbo < sr & sr < Ebo by TOPREAL3:3; then Wmin`1 <= sr & sr <= Emax`1 by PSCOMP_1:84,104; then L~Upper_Seq(C,n) meets Vertical_Line(sr) & L~Upper_Seq(C,n) /\ Vertical_Line(sr) is closed by A7,JORDAN6:64; then FiP in L~Upper_Seq(C,n) /\ Vertical_Line sr by A7,JORDAN5C:def 1; then A9: FiP in L~Upper_Seq(C,n) & FiP in Vertical_Line sr by XBOOLE_0:def 3; then FiP in L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n) by XBOOLE_0:def 2; then A10: FiP in L~Cage(C,n) by JORDAN1E:17; A11: FiP`1 = sr by A9,JORDAN6:34; A12: 1 <= Center Gauge(C,n) & Center Gauge(C,n) <= len Gauge(C,n) by JORDAN1B:12,14; A13: FiP in rng Upper_Seq(C,n) by A1,Th55; then A14: FiP..Upper_Seq(C,n) in dom Upper_Seq(C,n) by FINSEQ_4:30; A15: Lower_Seq(C,n)/.1 = E-max L~Cage(C,n) by JORDAN1F:6; Lower_Seq(C,n)/.len Lower_Seq(C,n) = W-min L~Cage(C,n) by JORDAN1F:8; then A16: L~Lower_Seq(C,n) is_an_arc_of Emax,Wmin by A15,TOPREAL1:31; then A17: L~Lower_Seq(C,n) is_an_arc_of Wmin,Emax by JORDAN5B:14; Wbo <= Ebo by SPRECT_1:23; then Wbo <= sr & sr <= Ebo by JORDAN6:2; then Wmin`1 <= sr & sr <= Emax`1 by PSCOMP_1:84,104; then A18: L~Lower_Seq(C,n) meets Vertical_Line(sr) & L~Lower_Seq(C,n) /\ Vertical_Line(sr) is closed by A17,JORDAN6:64; then LaP in L~Lower_Seq(C,n) /\ Vertical_Line sr by A16,JORDAN5C:def 2; then A19: LaP in L~Lower_Seq(C,n) & LaP in Vertical_Line sr by XBOOLE_0:def 3; then LaP in L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n) by XBOOLE_0:def 2; then A20: LaP in L~Cage(C,n) by JORDAN1E:17; A21: LaP`1 = sr by A19,JORDAN6:34; assume A22: FiP`2 <= LaP`2; A23: now assume FiP`2 = LaP`2; then FiP = LaP by A11,A21,TOPREAL3:11; then FiP in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) by A9,A19,XBOOLE_0:def 3 ; then FiP in {Wmin,Emax} by JORDAN1E:20; then FiP = Wmin or FiP = Emax by TARSKI:def 2; hence contradiction by A8,A11,PSCOMP_1:84,104; end; then A24: FiP`2 < LaP`2 by A22,REAL_1:def 5; LaP in rng Lower_Seq(C,n) by A1,Th56; then A25: LaP in rng Rev Lower_Seq(C,n) by FINSEQ_5:60; now assume rng mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) /\ {|[Ebo,FiP`2]|} <> {}; then consider x be set such that A26: x in rng mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) /\ {|[Ebo,FiP`2]|} by XBOOLE_0:def 1; x in rng mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) & x in {|[Ebo,FiP`2]| } by A26,XBOOLE_0:def 3; then |[Ebo,FiP`2]| in rng mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) by TARSKI:def 1; then |[Ebo,FiP`2]|`1 <= sr by A1,Th61; hence contradiction by A8,EUCLID:56; end; then rng mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) misses {|[Ebo,FiP`2]|} by XBOOLE_0:def 7; then A27: rng mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) misses rng <*|[Ebo,FiP`2]|*> by FINSEQ_1:55; A28: 1<=FiP..Upper_Seq(C,n) & FiP..Upper_Seq(C,n)<=len Upper_Seq(C,n) by A14,FINSEQ_3:27; 2 <> FiP..Upper_Seq(C,n) proof assume 2 = FiP..Upper_Seq(C,n); then Upper_Seq(C,n)/.2 = FiP by A13,FINSEQ_5:41; then FiP`1 = Wbo by Th39; then Wbo = sr by A9,JORDAN6:34; then Wbo = Ebo by XCMPLX_1:67; hence contradiction by SPRECT_1:33; end; then mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) is_S-Seq by A3,A28,JORDAN3:39; then A29: mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) is one-to-one special by TOPREAL1:def 10; A30: <*|[Ebo,FiP`2]|*> is one-to-one by FINSEQ_3:102; A31: (mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n))/.len mid(Upper_Seq(C,n),2, FiP..Upper_Seq(C,n)))`2 = (Upper_Seq(C,n)/.(FiP..Upper_Seq(C,n)))`2 by A4,A14,SPRECT_2:13 .= FiP`2 by A13,FINSEQ_5:41 .= |[Ebo,FiP`2]|`2 by EUCLID:56 .= (<*|[Ebo,FiP`2]|*>/.1)`2 by FINSEQ_4:25; <*|[Ebo,FiP`2]|*> is special by SPPOL_2:39; then reconsider g as one-to-one special FinSequence of TOP-REAL 2 by A27,A29,A30,A31,FINSEQ_3:98,GOBOARD2:13; A32: rng ((Rev Lower_Seq(C,n))-:LaP) c= rng (Rev Lower_Seq(C,n)) by FINSEQ_5:51; set GCw = Gauge(C,n)*(Center Gauge(C,n),width Gauge(C,n)); A33: 4 <= len Gauge(C,n) by JORDAN8:13; then 1 <= len Gauge(C,n) by AXIOMS:22; then 1 <= width Gauge(C,n) by JORDAN8:def 1; then A34: GCw`1 = (W-bound C + E-bound C)/2 by A1,Th43 .= sr by Th41; len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; then GCw`2 = Nbo by A12,JORDAN1A:91; then A35: GCw = |[sr,Nbo]| by A34,EUCLID:57; len Gauge(C,n) >= 3 by A33,AXIOMS:22; then Center Gauge(C,n) < len Gauge(C,n) by JORDAN1B:16; then not |[sr,Nbo]| in rng Lower_Seq(C,n) by A12,A35,Th51; then not |[sr,Nbo]| in rng (Rev Lower_Seq(C,n)) by FINSEQ_5:60; then A36: not |[sr,Nbo]| in rng ((Rev Lower_Seq(C,n))-:LaP) by A32; A37: |[sr,Nbo]|`2 = Nbo & SW`2 = Sbo by EUCLID:56,PSCOMP_1:73; then |[sr,Nbo]| <> SW by SPRECT_1:34; then not |[sr,Nbo]| in {SW} by TARSKI:def 1; then not |[sr,Nbo]| in rng <*SW*> by FINSEQ_1:55; then not |[sr,Nbo]| in rng <*SW*> \/ rng ((Rev Lower_Seq(C,n))-:LaP) by A36,XBOOLE_0:def 2; then not |[sr,Nbo]| in rng (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) by FINSEQ_1:44; then rng (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) misses {|[sr,Nbo]|} by ZFMISC_1:56; then rng (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) /\ {|[sr,Nbo]|} = {} by XBOOLE_0:def 7; then rng (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) /\ rng <*|[sr,Nbo]|*> = {} by FINSEQ_1:55; then A38: rng (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) misses rng <*|[sr,Nbo]| *> by XBOOLE_0:def 7; A39: SW`2 <= Wmin`2 by PSCOMP_1:87; A40: rng Lower_Seq(C,n) c= rng Cage(C,n) by Th47; A41: mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) is_in_the_area_of Cage(C,n) by A2,A4,A14,SPRECT_2:26; now let m be Nat; assume m in dom <*|[Ebo,FiP`2]|*>; then m in Seg 1 by FINSEQ_1:55; then m = 1 by FINSEQ_1:4,TARSKI:def 1; then <*|[Ebo,FiP`2]|*>/.m = |[Ebo,FiP`2]| by FINSEQ_4:25; then A42: (<*|[Ebo,FiP`2]|*>/.m)`1 = Ebo & (<*|[Ebo,FiP`2]|*>/.m)`2 = FiP`2 by EUCLID:56; hence W-bound L~Cage(C,n) <= (<*|[Ebo,FiP`2]|*>/.m)`1 & (<*|[Ebo,FiP`2]|*>/.m)`1 <= E-bound L~Cage(C,n) by SPRECT_1:23; thus S-bound L~Cage(C,n) <= (<*|[Ebo,FiP`2]|*>/.m)`2 & (<*|[Ebo,FiP`2]|*>/.m)`2 <= N-bound L~Cage(C,n) by A10,A42,PSCOMP_1:71; end; then <*|[Ebo,FiP`2]|*> is_in_the_area_of Cage(C,n) by SPRECT_2:def 1; then A43: g is_in_the_area_of Cage(C,n) by A41,SPRECT_2:28; A44: 1 <= len mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) by A4,A14,SPRECT_2:9; then 1 in dom mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) by FINSEQ_3:27; then A45: (g/.1)`1 = (mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n))/.1)`1 by GROUP_5:95 .= (Upper_Seq(C,n)/.2)`1 by A4,A14,SPRECT_2:12 .= W-bound L~Cage(C,n) by Th39; (g/.len g)`1 = (<*|[Ebo,FiP`2]|*>/.len <*|[Ebo,FiP`2]|*>)`1 by SPRECT_3: 11 .= (<*|[Ebo,FiP`2]|*>/.1)`1 by FINSEQ_1:56 .= (|[Ebo,FiP`2]|)`1 by FINSEQ_4:25 .= E-bound L~Cage(C,n) by EUCLID:56; then A46: g is_a_h.c._for Cage(C,n) by A43,A45,SPRECT_2:def 2; set RevL = (Rev Lower_Seq(C,n))-:LaP; A47: RevL is non empty by A25,FINSEQ_5:50; A48: len RevL = LaP..Rev Lower_Seq(C,n) by A25,FINSEQ_5:45; now per cases; suppose A49: SW <> Wmin; not SW in rng Lower_Seq(C,n) proof assume SW in rng Lower_Seq(C,n); then A50: SW in rng Cage(C,n) by A40; len Cage(C,n) > 4 by GOBOARD7:36; then len Cage(C,n) >= 2 by AXIOMS:22; then A51: rng Cage(C,n) c= L~Cage(C,n) by SPPOL_2:18; SW`1 = W-bound L~Cage(C,n) by PSCOMP_1:72; then SW in W-most L~Cage(C,n) by A50,A51,SPRECT_2:16; then A52: Wmin`2 <= SW`2 by PSCOMP_1:88; SW`1 = Wmin`1 by PSCOMP_1:85; then SW`2 <> Wmin`2 by A49,TOPREAL3:11; hence contradiction by A39,A52,REAL_1:def 5; end; then not SW in rng (Rev Lower_Seq(C,n)) by FINSEQ_5:60; then not SW in rng ((Rev Lower_Seq(C,n))-:LaP) by A32; then {SW} misses rng ((Rev Lower_Seq(C,n))-:LaP) by ZFMISC_1:56; then {SW} /\ rng ((Rev Lower_Seq(C,n))-:LaP) = {} by XBOOLE_0:def 7; then rng <*SW*> /\ rng ((Rev Lower_Seq(C,n))-:LaP) = {} by FINSEQ_1:55; then A53: rng <*SW*> misses rng ((Rev Lower_Seq(C,n))-:LaP) by XBOOLE_0: def 7; <*SW*> is one-to-one by FINSEQ_3:102; then A54: <*SW*>^((Rev Lower_Seq(C,n))-:LaP) is one-to-one by A53,FINSEQ_3:98; A55: <*|[sr,Nbo]|*> is one-to-one by FINSEQ_3:102; (Rev Lower_Seq(C,n))-:LaP is non empty by A25,FINSEQ_5:50; then A56: ((<*SW*>^((Rev Lower_Seq(C,n))-:LaP))/. len (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)))`1 = (((Rev Lower_Seq(C,n))-:LaP)/.len ((Rev Lower_Seq(C,n))-:LaP))`1 by SPRECT_3:11 .= (((Rev Lower_Seq(C,n))-:LaP)/.(LaP..Rev Lower_Seq(C,n)))`1 by A25,FINSEQ_5:45 .= LaP`1 by A25,FINSEQ_5:48 .= |[sr,Nbo]|`1 by A21,EUCLID:56 .= (<*|[sr,Nbo]|*>/.1)`1 by FINSEQ_4:25; A57: (<*SW*>/.len <*SW*>)`1 = (<*SW*>/.1)`1 by FINSEQ_1:56 .= SW`1 by FINSEQ_4:25 .= W-bound L~Cage(C,n) by PSCOMP_1:72 .= (W-min L~Cage(C,n))`1 by PSCOMP_1:84 .= (Lower_Seq(C,n)/.len Lower_Seq(C,n))`1 by JORDAN1F:8 .= ((Rev Lower_Seq(C,n))/.1)`1 by FINSEQ_5:68 .= (((Rev Lower_Seq(C,n))-:LaP)/.1)`1 by A25,FINSEQ_5:47; reconsider RevLS = Rev Lower_Seq(C,n) as special FinSequence of TOP-REAL 2 by SPPOL_2:42; <*SW*> is special by SPPOL_2:39; then A58: <*SW*>^(RevLS-:LaP) is special by A57,GOBOARD2:13; <*|[sr,Nbo]|*> is special by SPPOL_2:39; then reconsider h as one-to-one special FinSequence of TOP-REAL 2 by A38,A54,A55,A56,A58,FINSEQ_3:98,GOBOARD2:13; now let m be Nat; assume m in dom <*SW*>; then m in Seg 1 by FINSEQ_1:55; then m = 1 by FINSEQ_1:4,TARSKI:def 1; then <*SW*>/.m = SW by FINSEQ_4:25; then A59: (<*SW*>/.m)`1 = Wbo & (<*SW*>/.m)`2 = Sbo by PSCOMP_1:72,73; hence W-bound L~Cage(C,n) <= (<*SW*>/.m)`1 & (<*SW*>/.m)`1 <= E-bound L~Cage(C,n) by SPRECT_1:23; thus S-bound L~Cage(C,n) <= (<*SW*>/.m)`2 & (<*SW*>/.m)`2 <= N-bound L~Cage(C,n) by A59,SPRECT_1:24; end; then A60: <*SW*> is_in_the_area_of Cage(C,n) by SPRECT_2:def 1; Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:22; then Rev Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by SPRECT_3:68; then ((Rev Lower_Seq(C,n))-:LaP) is_in_the_area_of Cage(C,n) by A25,JORDAN1E:5; then A61: <*SW*>^((Rev Lower_Seq(C,n))-:LaP) is_in_the_area_of Cage(C,n) by A60,SPRECT_2:28; now let m be Nat; assume m in dom <*|[sr,Nbo]|*>; then m in Seg 1 by FINSEQ_1:55; then m = 1 by FINSEQ_1:4,TARSKI:def 1; then <*|[sr,Nbo]|*>/.m = |[sr,Nbo]| by FINSEQ_4:25; then A62: (<*|[sr,Nbo]|*>/.m)`1 = sr & (<*|[sr,Nbo]|*>/.m)`2 = Nbo by EUCLID:56; W-bound L~Cage(C,n) <= E-bound L~Cage(C,n) by SPRECT_1:23; hence W-bound L~Cage(C,n) <= (<*|[sr,Nbo]|*>/.m)`1 & (<*|[sr,Nbo]|*>/.m)`1 <= E-bound L~Cage(C,n) by A62,JORDAN6:2; thus S-bound L~Cage(C,n) <= (<*|[sr,Nbo]|*>/.m)`2 & (<*|[sr,Nbo]|*>/.m)`2 <= N-bound L~Cage(C,n) by A62,SPRECT_1:24; end; then <*|[sr,Nbo]|*> is_in_the_area_of Cage(C,n) by SPRECT_2:def 1; then A63: h is_in_the_area_of Cage(C,n) by A61,SPRECT_2:28; len (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) = 1 + len ((Rev Lower_Seq(C,n))-:LaP) by FINSEQ_5:8; then A64: len (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) >= 1 by NAT_1:29; A65: len h = len (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) + 1 by FINSEQ_2:19; then A66: 1+1 <= len h by A64,REAL_1:55; 1 in dom h by FINSEQ_5:6; then h/.1 = h.1 by FINSEQ_4:def 4; then A67: (h/.1)`2 = ((<*SW*>^((Rev Lower_Seq(C,n))-:LaP))/.1)`2 by A64,JORDAN3:17 .= SW`2 by FINSEQ_5:16 .= S-bound L~Cage(C,n) by PSCOMP_1:73; (h/.len h)`2 = |[sr,Nbo]|`2 by A65,TOPREAL4:1 .= N-bound L~Cage(C,n) by EUCLID:56; then A68: h is_a_v.c._for Cage(C,n) by A63,A67,SPRECT_2:def 3; len g = len mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n))+1 by FINSEQ_2:19; then 1+1 <= len g by A44,REAL_1:55; then L~g meets L~h by A46,A66,A68,SPRECT_2:33; then consider x be set such that A69: x in L~g and A70: x in L~h by XBOOLE_0:3; reconsider x as Point of TOP-REAL 2 by A69; set midU = mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)); midU is non empty by A4,A14,SPRECT_2:11; then A71: L~g = L~midU \/ LSeg(midU/.len midU,|[Ebo,FiP`2]|) by SPPOL_2:19; L~h = L~(<*SW*>^(((Rev Lower_Seq(C,n))-:LaP)^<*|[sr,Nbo]|*>)) by FINSEQ_1:45 .= LSeg(SW,(RevL^<*|[sr,Nbo]|*>)/.1) \/ L~(RevL^<*|[sr,Nbo]|*>) by SPPOL_2:20 .= LSeg(SW,(RevL^<*|[sr,Nbo]|*>)/.1) \/ (L~RevL \/ LSeg(RevL/.len RevL,|[sr,Nbo]|)) by A47,SPPOL_2:19; then A72: x in LSeg(SW,(RevL^<*|[sr,Nbo]|*>)/.1) or x in L~RevL \/ LSeg(RevL/.len RevL,|[sr,Nbo]|) by A70,XBOOLE_0:def 2; 1 in dom RevL by A47,FINSEQ_5:6; then A73: (RevL^<*|[sr,Nbo]|*>)/.1 = RevL/.1 by GROUP_5:95 .= (Rev Lower_Seq(C,n))/.1 by A25,FINSEQ_5:47 .= Lower_Seq(C,n)/.len Lower_Seq(C,n) by FINSEQ_5:68 .= Wmin by JORDAN1F:8; A74: L~midU c= L~Upper_Seq(C,n) by A4,A14,SPRECT_3:34; L~Rev Lower_Seq(C,n) = L~RevL \/ L~((Rev Lower_Seq(C,n)):-LaP) by A25,SPPOL_2:25; then L~RevL c= L~Rev Lower_Seq(C,n) by XBOOLE_1:7; then A75: L~RevL c= L~Lower_Seq(C,n) by SPPOL_2:22; A76: midU/.len midU = Upper_Seq(C,n)/.(FiP..Upper_Seq(C,n)) by A4,A14,SPRECT_2:13 .= FiP by A13,FINSEQ_5:41; A77: RevL/.len RevL = RevL/.(LaP..Rev Lower_Seq(C,n)) by A25,FINSEQ_5:45 .= LaP by A25,FINSEQ_5:48; A78: |[Ebo,FiP`2]|`1 = Ebo by EUCLID:56; A79: SW`1 = Wmin`1 by PSCOMP_1:85; then A80: LSeg(SW,Wmin) is vertical by SPPOL_1:37; A81: SW`2 <= Wmin`2 by PSCOMP_1:87; L~Cage(C,n) = L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n) by JORDAN1E:17; then A82: L~Upper_Seq(C,n) c= L~Cage(C,n) by XBOOLE_1:7; LaP`1 = |[sr,Nbo]|`1 by A21,EUCLID:56; then A83: LSeg(LaP,|[sr,Nbo]|) is vertical by SPPOL_1:37; A84: |[Ebo,FiP`2]|`2 = FiP`2 by EUCLID:56; then A85: LSeg(FiP,|[Ebo,FiP`2]|) is horizontal by SPPOL_1:36; A86: LaP`2 <= Nbo by A20,PSCOMP_1:71; A87: Wmin in rng Upper_Seq(C,n) by A5,FINSEQ_6:46; now assume FiP..Upper_Seq(C,n) = 1; then FiP..Upper_Seq(C,n) = (Upper_Seq(C,n)/.1)..Upper_Seq(C,n) by FINSEQ_6:47 .= Wmin..Upper_Seq(C,n) by JORDAN1F:5; then FiP = Wmin by A13,A87,FINSEQ_5:10; hence contradiction by A8,A11,PSCOMP_1:84; end; then FiP..Upper_Seq(C,n) > 1 by A28,REAL_1:def 5; then A88: 1+1+0 <= FiP..Upper_Seq(C,n) by NAT_1:38; then FiP..Upper_Seq(C,n)-2 >= 0 by REAL_1:84; then FiP..Upper_Seq(C,n)-'2 = FiP..Upper_Seq(C,n)-2 by BINARITH:def 3; then A89: len midU = FiP..Upper_Seq(C,n)-2+1 by A28,A88,JORDAN4:20 .= FiP..Upper_Seq(C,n)-(2-1) by XCMPLX_1:37; set FiP2 = First_Point(L~Lower_Seq(C,n),Wmin,Emax,Vertical_Line sr); A90: L~Rev Lower_Seq(C,n) = L~Lower_Seq(C,n) by SPPOL_2:22; A91: FiP2 = LaP by A16,A18,JORDAN5C:18; now per cases by A72,A73,A77,XBOOLE_0:def 2; suppose A92: x in LSeg(SW,Wmin); then A93: x`1 = SW`1 by A80,SPRECT_3:20; then A94: x`1 = Wbo by PSCOMP_1:72; A95: x`2 <= Wmin`2 by A81,A92,TOPREAL1:10; now per cases by A69,A71,A76,XBOOLE_0:def 2; suppose A96: x in L~midU; then x in L~Upper_Seq(C,n) by A74; then x in W-most L~Cage(C,n) by A82,A94,SPRECT_2:16; then x`2 >= Wmin`2 by PSCOMP_1:88; then x`2 = Wmin`2 by A95,AXIOMS:21; then x = Wmin by A79,A93,TOPREAL3:11; then FiP..Upper_Seq(C,n) = 1 by A3,A5,A28,A96,Th45; then Wmin = FiP by A5,A13,FINSEQ_5:41; hence contradiction by A8,A11,PSCOMP_1:84; suppose x in LSeg(FiP,|[Ebo,FiP`2]|); hence contradiction by A8,A11,A78,A94,TOPREAL1:9; end; hence contradiction; suppose A97: x in L~RevL; now per cases by A69,A71,A76,XBOOLE_0:def 2; suppose A98: x in L~midU; then x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) by A74,A75,A97,XBOOLE_0:def 3; then A99: x in {Wmin,Emax} by JORDAN1E:20; now per cases by A99,TARSKI:def 2; suppose x = Wmin; then FiP..Upper_Seq(C,n) = 1 by A3,A5,A28,A98,Th45; then Wmin = FiP by A5,A13,FINSEQ_5:41; hence contradiction by A8,A11,PSCOMP_1:84; suppose x = Emax; then FiP..Upper_Seq(C,n) = len Upper_Seq(C,n) by A3,A6,A28,A98,Th46; then Emax = FiP by A6,A13,FINSEQ_5:41; hence contradiction by A8,A11,PSCOMP_1:104; end; hence contradiction; suppose A100: x in LSeg(FiP,|[Ebo,FiP`2]|); LSeg(FiP,|[Ebo,FiP`2]|) is horizontal by A84,SPPOL_1:36; then A101: x`2 = FiP`2 by A100,SPRECT_3:19; A102: FiP`1 <= x`1 & x`1 <= |[Ebo,FiP`2]|`1 by A8,A11,A78,A100,TOPREAL1:9; consider i be Nat such that A103: 1 <= i & i+1 <= len RevL and A104: x in LSeg(RevL/.i,RevL/.(i+1)) by A97,SPPOL_2:14; A105: i < len RevL by A103,NAT_1:38; then i in Seg (LaP..Rev Lower_Seq(C,n)) by A48,A103,FINSEQ_1:3; then A106: RevL/.i = (Rev Lower_Seq(C,n))/.i by A25,FINSEQ_5:46; A107: i+1 >= 1 by NAT_1:29; then i+1 in Seg (LaP..Rev Lower_Seq(C,n)) by A48,A103,FINSEQ_1:3; then A108: RevL/.(i+1) = (Rev Lower_Seq(C,n))/.(i+1) by A25,FINSEQ_5:46; A109: (Rev Lower_Seq(C,n)/.i)`1 < sr by A1,A48,A90,A91,A103,A105,Th60; now per cases by A103,REAL_1:def 5; suppose i+1 < len RevL; then A110: (Rev Lower_Seq(C,n)/.(i+1))`1 < sr by A1,A48,A90,A91,A107,Th60; (RevL/.i)`1 <= (RevL/.(i+1))`1 or (RevL/.(i+1))`1 <= (RevL/.i)`1; then x`1 <= (RevL/.(i+1))`1 or x`1 <= (RevL/.i)`1 by A104,TOPREAL1:9; hence contradiction by A11,A102,A106,A108,A109,A110,AXIOMS:22; suppose A111: i+1 = len RevL; A112: Rev Lower_Seq(C,n) is special by SPPOL_2:42; i+1 <= len Rev Lower_Seq(C,n) by A25,A48,A111,FINSEQ_4:31; then LSeg(Rev Lower_Seq(C,n)/.i,Rev Lower_Seq(C,n)/.(i+1)) = LSeg(Rev Lower_Seq(C,n),i) by A103,TOPREAL1:def 5; then LSeg(RevL/.i,RevL/.(i+1)) is vertical or LSeg(RevL/.i,RevL/.(i+1)) is horizontal by A106,A108,A112,SPPOL_1: 41; hence contradiction by A21,A23,A77,A101,A104,A106,A109,A111,SPPOL_1 :37,SPRECT_3:19; end; hence contradiction; end; hence contradiction; suppose A113: x in LSeg(LaP,|[sr,Nbo]|); then A114: x`1 = LaP`1 by A83,SPRECT_3:20; A115: LaP`2 <= x`2 by A37,A86,A113,TOPREAL1:10; now per cases by A69,A71,A76,XBOOLE_0:def 2; suppose x in L~midU; then consider i be Nat such that A116: 1 <= i & i+1 <= len midU and A117: x in LSeg(midU/.i,midU/.(i+1)) by SPPOL_2:14; i < len midU by A116,NAT_1:38; then A118: i in dom midU by A116,FINSEQ_3:27; i+2 >= 1+1 by NAT_1:29; then i+2-1 >= 1+1-1 by REAL_1:49; then A119: i+2-1 >= 0 by AXIOMS:22; A120: midU/.i = Upper_Seq(C,n)/.(i+2-'1) by A4,A14,A88,A118,SPRECT_2: 7 .= Upper_Seq(C,n)/.(i+2-1) by A119,BINARITH:def 3 .= Upper_Seq(C,n)/.(i+(2-1)) by XCMPLX_1:29; A121: 1 <= i+1 by NAT_1:29; then A122: i+1 in dom midU by A116,FINSEQ_3:27; i+1+2 >= 1+1 by NAT_1:29; then i+1+2-1 >= 1+1-1 by REAL_1:49; then A123: i+1+2-1 >= 0 by AXIOMS:22; A124: midU/.(i+1) = Upper_Seq(C,n)/.(i+1+2-'1) by A4,A14,A88,A122,SPRECT_2:7 .= Upper_Seq(C,n)/.(i+1+2-1) by A123,BINARITH:def 3 .= Upper_Seq(C,n)/.(i+1+(2-1)) by XCMPLX_1:29; i+1+1 <= FiP..Upper_Seq(C,n)-1+1 by A89,A116,REAL_1:55; then A125: i+1+1 <= FiP..Upper_Seq(C,n) by XCMPLX_1:27; then i+1 < FiP..Upper_Seq(C,n) by NAT_1:38; then A126: (midU/.i)`1 < sr by A1,A120,A121,Th59; A127: 1 <= i+1+1 by NAT_1:29; i+1+1 <= len Upper_Seq(C,n) by A28,A125,AXIOMS:22; then LSeg(midU/.i,midU/.(i+1)) = LSeg(Upper_Seq(C,n),i+1) by A120,A121,A124,TOPREAL1:def 5; then A128: LSeg(midU/.i,midU/.(i+1)) is vertical or LSeg(midU/.i,midU/.(i+1)) is horizontal by SPPOL_1:41; now per cases by A116,REAL_1:def 5; suppose i+1 < len midU; then i+1+1 <= len midU by NAT_1:38; then i+1+1+1 <= FiP..Upper_Seq(C,n)-1+1 by A89,REAL_1:55; then i+1+1+1 <= FiP..Upper_Seq(C,n) by XCMPLX_1:27; then i+1+1 < FiP..Upper_Seq(C,n) by NAT_1:38; then A129: (midU/.(i+1))`1 < sr by A1,A124,A127,Th59; (midU/.i)`1 <= (midU/.(i+1))`1 or (midU/.(i+1))`1 <= (midU/.i)`1; hence contradiction by A21,A114,A117,A126,A129,TOPREAL1:9; suppose A130: i+1 = len midU; then (midU/.i)`2 = (midU/.(i+1))`2 by A11,A76,A126,A128,SPPOL_1:36,37; hence contradiction by A24,A76,A115,A117,A130,GOBOARD7:6; end; hence contradiction; suppose x in LSeg(FiP,|[Ebo,FiP`2]|); hence contradiction by A24,A85,A115,SPRECT_3:19; end; hence contradiction; end; hence contradiction; suppose A131: SW = Wmin; set h = ((Rev Lower_Seq(C,n))-:LaP)^<*|[sr,Nbo]|*>; rng ((Rev Lower_Seq(C,n))-:LaP) misses {|[sr,Nbo]|} by A36,ZFMISC_1:56; then rng ((Rev Lower_Seq(C,n))-:LaP) /\ {|[sr,Nbo]|} = {} by XBOOLE_0:def 7; then rng ((Rev Lower_Seq(C,n))-:LaP) /\ rng <*|[sr,Nbo]|*> = {} by FINSEQ_1:55; then A132: rng ((Rev Lower_Seq(C,n))-:LaP) misses rng <*|[sr,Nbo]|*> by XBOOLE_0:def 7; A133: <*|[sr,Nbo]|*> is one-to-one by FINSEQ_3:102; A134: (((Rev Lower_Seq(C,n))-:LaP)/.len ((Rev Lower_Seq(C,n))-:LaP))`1 = (((Rev Lower_Seq(C,n))-:LaP)/.(LaP..Rev Lower_Seq(C,n)))`1 by A25,FINSEQ_5:45 .= LaP`1 by A25,FINSEQ_5:48 .= |[sr,Nbo]|`1 by A21,EUCLID:56 .= (<*|[sr,Nbo]|*>/.1)`1 by FINSEQ_4:25; reconsider RevLS = Rev Lower_Seq(C,n) as special FinSequence of TOP-REAL 2 by SPPOL_2:42; A135: RevLS-:LaP is special; <*|[sr,Nbo]|*> is special by SPPOL_2:39; then reconsider h as one-to-one special FinSequence of TOP-REAL 2 by A132,A133,A134,A135,FINSEQ_3:98,GOBOARD2:13; Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:22; then Rev Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by SPRECT_3:68; then A136: ((Rev Lower_Seq(C,n))-:LaP) is_in_the_area_of Cage(C,n) by A25,JORDAN1E:5; now let m be Nat; assume m in dom <*|[sr,Nbo]|*>; then m in Seg 1 by FINSEQ_1:55; then m = 1 by FINSEQ_1:4,TARSKI:def 1; then <*|[sr,Nbo]|*>/.m = |[sr,Nbo]| by FINSEQ_4:25; then A137: (<*|[sr,Nbo]|*>/.m)`1 = sr & (<*|[sr,Nbo]|*>/.m)`2 = Nbo by EUCLID:56; W-bound L~Cage(C,n) <= E-bound L~Cage(C,n) by SPRECT_1:23; hence W-bound L~Cage(C,n) <= (<*|[sr,Nbo]|*>/.m)`1 & (<*|[sr,Nbo]|*>/.m)`1 <= E-bound L~Cage(C,n) by A137,JORDAN6:2; thus S-bound L~Cage(C,n) <= (<*|[sr,Nbo]|*>/.m)`2 & (<*|[sr,Nbo]|*>/.m)`2 <= N-bound L~Cage(C,n) by A137,SPRECT_1:24; end; then <*|[sr,Nbo]|*> is_in_the_area_of Cage(C,n) by SPRECT_2:def 1; then A138: h is_in_the_area_of Cage(C,n) by A136,SPRECT_2:28; LaP..(Rev Lower_Seq(C,n)) <> 0 by A47,A48,FINSEQ_1:25; then LaP..(Rev Lower_Seq(C,n)) > 0 by NAT_1:19; then LaP..(Rev Lower_Seq(C,n)) >= 0+1 by NAT_1:38; then A139: len ((Rev Lower_Seq(C,n))-:LaP) >= 1 by A25,FINSEQ_5:45; A140: len h = len ((Rev Lower_Seq(C,n))-:LaP) + 1 by FINSEQ_2:19; then A141: 1+1 <= len h by A139,REAL_1:55; 1 in dom h by FINSEQ_5:6; then h/.1 = h.1 by FINSEQ_4:def 4; then A142: (h/.1)`2 = (((Rev Lower_Seq(C,n))-:LaP)/.1)`2 by A139,JORDAN3:17 .= ((Rev Lower_Seq(C,n))/.1)`2 by A25,FINSEQ_5:47 .= (Lower_Seq(C,n)/.len Lower_Seq(C,n))`2 by FINSEQ_5:68 .= Wmin`2 by JORDAN1F:8 .= S-bound L~Cage(C,n) by A131,PSCOMP_1:73; (h/.len h)`2 = |[sr,Nbo]|`2 by A140,TOPREAL4:1 .= N-bound L~Cage(C,n) by EUCLID:56; then A143: h is_a_v.c._for Cage(C,n) by A138,A142,SPRECT_2:def 3; len g = len mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n))+1 by FINSEQ_2:19; then 1+1 <= len g by A44,REAL_1:55; then L~g meets L~h by A46,A141,A143,SPRECT_2:33; then consider x be set such that A144: x in L~g and A145: x in L~h by XBOOLE_0:3; reconsider x as Point of TOP-REAL 2 by A144; set midU = mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)); midU is non empty by A4,A14,SPRECT_2:11; then A146: L~g = L~midU \/ LSeg(midU/.len midU,|[Ebo,FiP`2]|) by SPPOL_2:19; A147: L~h = L~RevL \/ LSeg(RevL/.len RevL,|[sr,Nbo]|) by A47,SPPOL_2:19; A148: L~midU c= L~Upper_Seq(C,n) by A4,A14,SPRECT_3:34; L~Rev Lower_Seq(C,n) = L~RevL \/ L~((Rev Lower_Seq(C,n)):-LaP) by A25,SPPOL_2:25; then L~RevL c= L~Rev Lower_Seq(C,n) by XBOOLE_1:7; then A149: L~RevL c= L~Lower_Seq(C,n) by SPPOL_2:22; A150: midU/.len midU = Upper_Seq(C,n)/.(FiP..Upper_Seq(C,n)) by A4,A14,SPRECT_2:13 .= FiP by A13,FINSEQ_5:41; A151: RevL/.len RevL = RevL/.(LaP..Rev Lower_Seq(C,n)) by A25,FINSEQ_5:45 .= LaP by A25,FINSEQ_5:48; A152: |[Ebo,FiP`2]|`1 = Ebo by EUCLID:56; LaP`1 = |[sr,Nbo]|`1 by A21,EUCLID:56; then A153: LSeg(LaP,|[sr,Nbo]|) is vertical by SPPOL_1:37; A154: |[Ebo,FiP`2]|`2 = FiP`2 by EUCLID:56; then A155: LSeg(FiP,|[Ebo,FiP`2]|) is horizontal by SPPOL_1:36; A156: LaP`2 <= Nbo by A20,PSCOMP_1:71; A157: Wmin in rng Upper_Seq(C,n) by A5,FINSEQ_6:46; now assume FiP..Upper_Seq(C,n) = 1; then FiP..Upper_Seq(C,n) = (Upper_Seq(C,n)/.1)..Upper_Seq(C,n) by FINSEQ_6:47 .= Wmin..Upper_Seq(C,n) by JORDAN1F:5; then FiP = Wmin by A13,A157,FINSEQ_5:10; hence contradiction by A8,A11,PSCOMP_1:84; end; then FiP..Upper_Seq(C,n) > 1 by A28,REAL_1:def 5; then A158: 1+1+0 <= FiP..Upper_Seq(C,n) by NAT_1:38; then FiP..Upper_Seq(C,n)-2 >= 0 by REAL_1:84; then FiP..Upper_Seq(C,n)-'2 = FiP..Upper_Seq(C,n)-2 by BINARITH:def 3; then A159: len midU = FiP..Upper_Seq(C,n)-2+1 by A28,A158,JORDAN4:20 .= FiP..Upper_Seq(C,n)-(2-1) by XCMPLX_1:37; set FiP2 = First_Point(L~Lower_Seq(C,n),Wmin,Emax,Vertical_Line sr); A160: L~Rev Lower_Seq(C,n) = L~Lower_Seq(C,n) by SPPOL_2:22; A161: FiP2 = LaP by A16,A18,JORDAN5C:18; now per cases by A145,A147,A151,XBOOLE_0:def 2; suppose A162: x in L~RevL; now per cases by A144,A146,A150,XBOOLE_0:def 2; suppose A163: x in L~midU; then x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) by A148,A149,A162,XBOOLE_0:def 3; then A164: x in {Wmin,Emax} by JORDAN1E:20; now per cases by A164,TARSKI:def 2; suppose x = Wmin; then FiP..Upper_Seq(C,n) = 1 by A3,A5,A28,A163,Th45; then Wmin = FiP by A5,A13,FINSEQ_5:41; hence contradiction by A8,A11,PSCOMP_1:84; suppose x = Emax; then FiP..Upper_Seq(C,n) = len Upper_Seq(C,n) by A3,A6,A28,A163,Th46; then Emax = FiP by A6,A13,FINSEQ_5:41; hence contradiction by A8,A11,PSCOMP_1:104; end; hence contradiction; suppose A165: x in LSeg(FiP,|[Ebo,FiP`2]|); LSeg(FiP,|[Ebo,FiP`2]|) is horizontal by A154,SPPOL_1:36; then A166: x`2 = FiP`2 by A165,SPRECT_3:19; A167: FiP`1 <= x`1 & x`1 <= |[Ebo,FiP`2]|`1 by A8,A11,A152,A165,TOPREAL1:9; consider i be Nat such that A168: 1 <= i & i+1 <= len RevL and A169: x in LSeg(RevL/.i,RevL/.(i+1)) by A162,SPPOL_2:14; A170: i < len RevL by A168,NAT_1:38; then i in Seg (LaP..Rev Lower_Seq(C,n)) by A48,A168,FINSEQ_1:3; then A171: RevL/.i = (Rev Lower_Seq(C,n))/.i by A25,FINSEQ_5:46; A172: i+1 >= 1 by NAT_1:29; then i+1 in Seg (LaP..Rev Lower_Seq(C,n)) by A48,A168,FINSEQ_1:3; then A173: RevL/.(i+1) = (Rev Lower_Seq(C,n))/.(i+1) by A25,FINSEQ_5:46; A174: (Rev Lower_Seq(C,n)/.i)`1 < sr by A1,A48,A160,A161,A168,A170,Th60; now per cases by A168,REAL_1:def 5; suppose i+1 < len RevL; then A175: (Rev Lower_Seq(C,n)/.(i+1))`1 < sr by A1,A48,A160,A161,A172,Th60; (RevL/.i)`1 <= (RevL/.(i+1))`1 or (RevL/.(i+1))`1 <= (RevL/.i)`1; then x`1 <= (RevL/.(i+1))`1 or x`1 <= (RevL/.i)`1 by A169,TOPREAL1:9; hence contradiction by A11,A167,A171,A173,A174,A175,AXIOMS:22; suppose A176: i+1 = len RevL; A177: Rev Lower_Seq(C,n) is special by SPPOL_2:42; i+1 <= len Rev Lower_Seq(C,n) by A25,A48,A176,FINSEQ_4:31; then LSeg(Rev Lower_Seq(C,n)/.i,Rev Lower_Seq(C,n)/.(i+1)) = LSeg(Rev Lower_Seq(C,n),i) by A168,TOPREAL1:def 5; then LSeg(RevL/.i,RevL/.(i+1)) is vertical or LSeg(RevL/.i,RevL/.(i+1)) is horizontal by A171,A173,A177,SPPOL_1: 41; hence contradiction by A21,A23,A151,A166,A169,A171,A174,A176, SPPOL_1:37,SPRECT_3:19; end; hence contradiction; end; hence contradiction; suppose A178: x in LSeg(LaP,|[sr,Nbo]|); then A179: x`1 = LaP`1 by A153,SPRECT_3:20; A180: LaP`2 <= x`2 by A37,A156,A178,TOPREAL1:10; now per cases by A144,A146,A150,XBOOLE_0:def 2; suppose x in L~midU; then consider i be Nat such that A181: 1 <= i & i+1 <= len midU and A182: x in LSeg(midU/.i,midU/.(i+1)) by SPPOL_2:14; i < len midU by A181,NAT_1:38; then A183: i in dom midU by A181,FINSEQ_3:27; i+2 >= 1+1 by NAT_1:29; then i+2-1 >= 1+1-1 by REAL_1:49; then A184: i+2-1 >= 0 by AXIOMS:22; A185: midU/.i = Upper_Seq(C,n)/.(i+2-'1) by A4,A14,A158,A183,SPRECT_2 :7 .= Upper_Seq(C,n)/.(i+2-1) by A184,BINARITH:def 3 .= Upper_Seq(C,n)/.(i+(2-1)) by XCMPLX_1:29; A186: 1 <= i+1 by NAT_1:29; then A187: i+1 in dom midU by A181,FINSEQ_3:27; i+1+2 >= 1+1 by NAT_1:29; then i+1+2-1 >= 1+1-1 by REAL_1:49; then A188: i+1+2-1 >= 0 by AXIOMS:22; A189: midU/.(i+1) = Upper_Seq(C,n)/.(i+1+2-'1) by A4,A14,A158,A187,SPRECT_2:7 .= Upper_Seq(C,n)/.(i+1+2-1) by A188,BINARITH:def 3 .= Upper_Seq(C,n)/.(i+1+(2-1)) by XCMPLX_1:29; i+1+1 <= FiP..Upper_Seq(C,n)-1+1 by A159,A181,REAL_1:55; then A190: i+1+1 <= FiP..Upper_Seq(C,n) by XCMPLX_1:27; then i+1 < FiP..Upper_Seq(C,n) by NAT_1:38; then A191: (midU/.i)`1 < sr by A1,A185,A186,Th59; A192: 1 <= i+1+1 by NAT_1:29; i+1+1 <= len Upper_Seq(C,n) by A28,A190,AXIOMS:22; then LSeg(midU/.i,midU/.(i+1)) = LSeg(Upper_Seq(C,n),i+1) by A185,A186,A189,TOPREAL1:def 5; then A193: LSeg(midU/.i,midU/.(i+1)) is vertical or LSeg(midU/.i,midU/.(i+1)) is horizontal by SPPOL_1:41; now per cases by A181,REAL_1:def 5; suppose i+1 < len midU; then i+1+1 <= len midU by NAT_1:38; then i+1+1+1 <= FiP..Upper_Seq(C,n)-1+1 by A159,REAL_1:55; then i+1+1+1 <= FiP..Upper_Seq(C,n) by XCMPLX_1:27; then i+1+1 < FiP..Upper_Seq(C,n) by NAT_1:38; then A194: (midU/.(i+1))`1 < sr by A1,A189,A192,Th59; (midU/.i)`1 <= (midU/.(i+1))`1 or (midU/.(i+1))`1 <= (midU/.i)`1; hence contradiction by A21,A179,A182,A191,A194,TOPREAL1:9; suppose A195: i+1 = len midU; then (midU/.i)`2 = (midU/.(i+1))`2 by A11,A150,A191,A193,SPPOL_1:36,37; hence contradiction by A24,A150,A180,A182,A195,GOBOARD7:6; end; hence contradiction; suppose x in LSeg(FiP,|[Ebo,FiP`2]|); hence contradiction by A24,A155,A180,SPRECT_3:19; end; hence contradiction; end; hence contradiction; end; hence contradiction; end; theorem Th63: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 holds L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; assume A1: n > 0; A2: Upper_Seq(C,n)=Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n) by JORDAN1E:def 1; 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; A4: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; then A5: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by A4,FINSEQ_6:96; then Upper_Seq(C,n)/.1 = Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by A2,FINSEQ_5:47; then A6: Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by A4,FINSEQ_6:98; A7: Upper_Seq(C,n)/.len 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))..Rotate(Cage(C,n),W-min L~Cage(C,n))) by A2,A5,FINSEQ_5:45 .= E-max L~Cage(C,n) by A5,FINSEQ_5:48; A8: Lower_Seq(C,n)/.1 = (Rotate(Cage(C,n),W-min L~Cage(C,n)):- E-max L~Cage(C,n))/.1 by JORDAN1E:def 2 .= E-max L~Cage(C,n) by FINSEQ_5:56; A9: 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 A3,A5,FINSEQ_5:57 .= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by FINSEQ_6:def 1 .= W-min L~Cage(C,n) by A4,FINSEQ_6:98; A10: L~Upper_Seq(C,n) is_an_arc_of W-min L~Cage(C,n),E-max L~Cage(C,n) by A6,A7,TOPREAL1:31; A11: L~Lower_Seq(C,n) is_an_arc_of E-max L~Cage(C,n),W-min L~Cage(C,n) by A8,A9,TOPREAL1:31; A12: L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) = {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:20; A13: L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n) = L~Cage(C,n) by JORDAN1E:17; First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))`2 > Last_Point(L~Lower_Seq(C,n),E-max L~Cage(C,n),W-min L~Cage(C,n), Vertical_Line((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))`2 by A1,Th62; hence thesis by A10,A11,A12,A13,JORDAN6:def 8; end; theorem Th64: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 holds L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; assume A1: n > 0; A2: Lower_Seq(C,n)=Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n) by JORDAN1E:def 2; A3: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; then A4: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by A3,FINSEQ_6:96; A5: Lower_Seq(C,n)/.1 = (Rotate(Cage(C,n),W-min L~Cage(C,n)):- E-max L~Cage(C,n))/.1 by JORDAN1E:def 2 .= E-max L~Cage(C,n) by FINSEQ_5:56; A6: 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 A2,A4,FINSEQ_5:57 .= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by FINSEQ_6:def 1 .= W-min L~Cage(C,n) by A3,FINSEQ_6:98; A7: L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) by A1,Th63; A8: L~Lower_Seq(C,n) is_an_arc_of E-max L~Cage(C,n),W-min L~Cage(C,n) by A5,A6,TOPREAL1:31; A9: L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) = {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:20; A10: L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n) = L~Cage(C,n) by JORDAN1E:17; First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))`2 > Last_Point(L~Lower_Seq(C,n),E-max L~Cage(C,n),W-min L~Cage(C,n), Vertical_Line((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))`2 by A1,Th62; hence thesis by A7,A8,A9,A10,JORDAN6:def 9; end; theorem for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 for i,j be Nat st 1 <= i & i <= len Gauge(C,n) & 1 <= j & j <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Cage(C,n) holds LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,j)) meets Lower_Arc L~Cage(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; assume A1: n > 0; let i,j be Nat; assume A2: 1 <= i & i <= len Gauge(C,n) & 1 <= j & j <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Cage(C,n); L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) by A1,Th64; hence thesis by A2,Th54; end;