### The Mizar article:

### Upper and Lower Sequence on the Cage, Upper and Lower Arcs

**by****Robert Milewski**

- Received April 5, 2002
Copyright (c) 2002 Association of Mizar Users

- MML identifier: JORDAN1J
- [ MML identifier index ]

environ vocabulary JORDAN8, PSCOMP_1, BOOLE, JORDAN1A, JORDAN9, GOBOARD1, GOBOARD5, JORDAN6, SPRECT_2, JORDAN3, FINSEQ_5, JORDAN2C, SPPOL_2, GROUP_2, RFINSEQ, REALSET1, JORDAN1E, SQUARE_1, FINSEQ_4, TOPREAL2, CONNSP_1, COMPTS_1, TOPREAL1, SPPOL_1, FINSEQ_1, TREES_1, EUCLID, RELAT_1, MCART_1, MATRIX_1, GOBOARD9, PRE_TOPC, RELAT_2, SEQM_3, SUBSET_1, FUNCT_1, ARYTM_1, FINSEQ_6, CARD_1, GOBOARD2, GROUP_1, GRAPH_2; notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, SQUARE_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_1, FINSEQ_6, REALSET1, GRAPH_2, STRUCT_0, PRE_TOPC, TOPREAL2, CARD_1, CARD_4, BINARITH, CONNSP_1, COMPTS_1, EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13, SPPOL_1, SPPOL_2, JORDAN3, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A, JORDAN1E; constructors JORDAN8, REALSET1, GOBOARD9, JORDAN6, REAL_1, CARD_4, PSCOMP_1, BINARITH, JORDAN2C, CONNSP_1, JORDAN9, JORDAN1A, SQUARE_1, FINSEQ_4, GOBRD13, JORDAN1, JORDAN3, RFINSEQ, MATRIX_2, TOPREAL2, JORDAN5C, PARTFUN1, GRAPH_2, SPRECT_1, GOBOARD2, INT_1, TOPS_1, FINSOP_1, JORDAN1E, MEMBERED; clusters SPRECT_1, TOPREAL6, JORDAN8, REVROT_1, INT_1, RELSET_1, SUBSET_1, PRE_TOPC, SPRECT_3, GOBOARD2, FINSEQ_1, FINSEQ_5, SPPOL_2, JORDAN1A, JORDAN1B, JORDAN1E, JORDAN1G, GOBRD11, FUNCT_7, XBOOLE_0, XREAL_0, MEMBERED, ZFMISC_1, NUMBERS, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; definitions TARSKI, GOBOARD5, XBOOLE_0; theorems AXIOMS, BINARITH, JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, REAL_1, GOBOARD5, SQUARE_1, 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, JORDAN5B, AMI_5, JORDAN3, GOBRD13, INT_1, JORDAN9, RLVECT_1, JORDAN2C, SUBSET_1, CONNSP_1, ZFMISC_1, JGRAPH_1, GOBOARD1, SPRECT_1, TARSKI, TOPREAL3, FINSEQ_3, RELAT_1, COMPTS_1, FUNCT_1, TOPREAL5, JORDAN10, GRAPH_2, GOBOARD2, CARD_1, CARD_2, YELLOW_6, PRE_CIRC, ENUMSET1, GROUP_5, SPRECT_4, JORDAN1B, SPRECT_5, SCMFSA_7, JORDAN1E, PARTFUN2, JORDAN1F, JORDAN1, TDLAT_1, JORDAN1G, JORDAN1C, GOBOARD3, JORDAN1H, TOPREAL8, GOBRD14, JORDAN1D, JORDAN1I, AMISTD_1, ALGSEQ_1, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes NAT_1; begin reserve n for Nat; theorem Th1: for G be Go-board for i1,i2,j1,j2 be Nat st 1 <= j1 & j1 <= width G & 1 <= j2 & j2 <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds G*(i1,j1)`1 < G*(i2,j2)`1 proof let G be Go-board; let i1,i2,j1,j2 be Nat; assume that A1: 1 <= j1 and A2: j1 <= width G and A3: 1 <= j2 and A4: j2 <= width G and A5: 1 <= i1 and A6: i1 < i2 and A7: i2 <= len G; A8: 1 <= i2 by A5,A6,AXIOMS:22; then G*(i2,j1)`1 = G*(i2,1)`1 by A1,A2,A7,GOBOARD5:3 .= G*(i2,j2)`1 by A3,A4,A7,A8,GOBOARD5:3; hence G*(i1,j1)`1 < G*(i2,j2)`1 by A1,A2,A5,A6,A7,GOBOARD5:4; end; theorem Th2: for G be Go-board for i1,i2,j1,j2 be Nat st 1 <= i1 & i1 <= len G & 1 <= i2 & i2 <= len G & 1 <= j1 & j1 < j2 & j2 <= width G holds G*(i1,j1)`2 < G*(i2,j2)`2 proof let G be Go-board; let i1,i2,j1,j2 be Nat; assume that A1: 1 <= i1 and A2: i1 <= len G and A3: 1 <= i2 and A4: i2 <= len G and A5: 1 <= j1 and A6: j1 < j2 and A7: j2 <= width G; A8: 1 <= j2 by A5,A6,AXIOMS:22; then G*(i1,j2)`2 = G*(1,j2)`2 by A1,A2,A7,GOBOARD5:2 .= G*(i2,j2)`2 by A3,A4,A7,A8,GOBOARD5:2; hence G*(i1,j1)`2 < G*(i2,j2)`2 by A1,A2,A5,A6,A7,GOBOARD5:5; end; definition let f be non empty FinSequence; let g be FinSequence; cluster f^'g -> non empty; coherence proof f^'g = f^(2,len g)-cut g by GRAPH_2:def 2; hence thesis; end; end; theorem Th3: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat holds L~(Cage(C,n)-:E-max L~Cage(C,n)) /\ L~(Cage(C,n):-E-max L~Cage(C,n)) = {N-min L~Cage(C,n),E-max 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)-:E-max L~Cage(C,n); set LS = Cage(C,n):-E-max L~Cage(C,n); set f=Cage(C,n); set pW=E-max L~Cage(C,n); set pN=N-min L~Cage(C,n); A1: pW in rng Cage(C,n) by SPRECT_2:50; A2: pW..Cage(C,n) <= pW..Cage(C,n); (f:-pW)/.len(f:-pW) = f/.len f by A1,FINSEQ_5:57 .= f/.1 by FINSEQ_6:def 1 .= pN by JORDAN9:34; then A3: pN in rng (Cage(C,n):-pW) by REVROT_1:3; A4: Cage(C,n)-:pW <> {} by A1,FINSEQ_5:50; (Cage(C,n):-pW)/.1 = pW by FINSEQ_5:56; then A5: E-max L~Cage(C,n) in rng (Cage(C,n):-E-max L~Cage(C,n)) by FINSEQ_6:46; (Cage(C,n)-:pW)/.1 = Cage(C,n)/.1 by A1,FINSEQ_5:47 .= pN by JORDAN9:34; then A6: N-min L~Cage(C,n) in rng (Cage(C,n)-:E-max L~Cage(C,n)) by A4,FINSEQ_6:46; len(f-:pW) = pW..f by A1,FINSEQ_5:45; then (f-:pW)/.len (f-:pW) = pW by A1,FINSEQ_5:48; then A7: pW in rng (Cage(C,n)-:pW) by A4,REVROT_1:3; N-max L~f in L~f & pW`1 = E-bound L~f by PSCOMP_1:104,SPRECT_1:13; then (N-max L~f)`1 <= pW`1 by PSCOMP_1:71; then A8: pN <> pW by SPRECT_2:55; then A9: 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 A3,A5,TARSKI:def 2; end; then A10: 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 A9,A10,XBOOLE_1:1; then len LS >= 2 by CARD_1:56; then A11: rng LS c= L~LS by SPPOL_2:18; A12: E-max L~Cage(C,n) in rng LS by FINSEQ_6:66; A13: Card {pN,pW} = 2 by A8,CARD_2:76; {pN,pW} c= rng US proof let x be set; assume x in {pN,pW}; hence x in rng US by A6,A7,TARSKI:def 2; end; then A14: Card {pN,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 A15: 2 c= len US by A13,A14,XBOOLE_1:1; then A16: len US >= 2 by CARD_1:56; then A17: rng US c= L~US by SPPOL_2:18; len US <> 0 by A15,CARD_1:56; then A18: US is non empty by FINSEQ_1:25; A19: E-max L~Cage(C,n) in rng US by A1,A2,FINSEQ_5:49; US/.1 = Cage(C,n)/.1 by A1,FINSEQ_5:47 .= N-min L~Cage(C,n) by JORDAN9:34; then A20: N-min L~Cage(C,n) in rng US by A18,FINSEQ_6:46; LS/.(len LS) = Cage(C,n)/.len Cage(C,n) by A1,FINSEQ_5:57 .= Cage(C,n)/.1 by FINSEQ_6:def 1 .= N-min L~Cage(C,n) by JORDAN9:34; then A21: 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),E-max L~Cage(C,n)} proof let x be set; assume A22: x in L~US /\ L~LS; then A23: x in L~US & x in L~LS by XBOOLE_0:def 3; reconsider x1=x as Point of TOP-REAL 2 by A22; consider i1 be Nat such that A24: 1 <= i1 & i1+1 <= len US and A25: x1 in LSeg(US,i1) by A23,SPPOL_2:13; consider i2 be Nat such that A26: 1 <= i2 & i2+1 <= len LS and A27: x1 in LSeg(LS,i2) by A23,SPPOL_2:13; A28: LSeg(US,i1) = LSeg(f,i1) by A24,SPPOL_2:9; set i3=i2-'1; A29: i3+1 = i2 by A26,AMI_5:4; then A30: LSeg(LS,i2) = LSeg(f,i3+pW..f) by A1,SPPOL_2:10; A31: len US = pW..f by A1,FINSEQ_5:45; A32: len LS = len f-pW..f+1 by A1,FINSEQ_5:53; A33: i2-1 >= 1-1 by A26,REAL_1:49; i2 < len f-pW..f+1 by A26,A32,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 A34: i3+pW..f < len f by A33,BINARITH:def 3; A35: i3 >= 0 by NAT_1:18; A36: pW..f >= 1 by A1,FINSEQ_4:31; i3+1 < len f-pW..f+1 by A26,A29,A32,NAT_1:38; then i3 < len f-pW..f by REAL_1:55; then A37: i3+pW..f < len f by REAL_1:86; A38: i1+1 < pW..f+1 by A24,A31,NAT_1:38; 1+pW..f <= i3+1+pW..f by A26,A29,REAL_1:55; then i1+1 < i3+1+pW..f by A38,AXIOMS:22; then i1+1 < i3+pW..f+1 by XCMPLX_1:1; then A39: i1+1 <= i3+pW..f by NAT_1:38; A40: i3+pW..f+1 <= len f by A37,NAT_1:38; A41: len f > 4 by GOBOARD7:36; A42: i3+pW..f >= 0 & i1 >= 0 by NAT_1:18; A43: pW..f-'1+1 = pW..f by A36,AMI_5:4; assume A44: not x in {N-min L~Cage(C,n),E-max L~Cage(C,n)}; now per cases by A24,A39,REAL_1:def 5; suppose i1+1 < i3+pW..f & i1 > 1; then LSeg(f,i1) misses LSeg(f,i3+pW..f) by A37,GOBOARD5:def 4; then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {} by XBOOLE_0:def 7; hence contradiction by A25,A27,A28,A30,XBOOLE_0:def 3; suppose A45: i1 = 1; A46: i3+pW..f >= 0+2 by A16,A31,A35,REAL_1:55; now per cases by A46,REAL_1:def 5; suppose i3+pW..f > 2; then A47: i1+1 < i3+pW..f by A45; now per cases by A40,REAL_1:def 5; suppose i3+pW..f+1 < len f; then LSeg(f,i1) misses LSeg(f,i3+pW..f) by A47,GOBOARD5:def 4; then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {} by XBOOLE_0:def 7; hence contradiction by A25,A27,A28,A30,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 A42,BINARITH:def 3; then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {f/.1} by A41,A45,REVROT_1:30 ; then x1 in {f/.1} by A25,A27,A28,A30,XBOOLE_0:def 3; then x1 = f/.1 by TARSKI:def 1 .= pN by JORDAN9:34; hence contradiction by A44,TARSKI:def 2; end; hence contradiction; suppose A48: i3+pW..f = 2; then A49: x1 in LSeg(f,1) /\ LSeg(f,1+1) by A25,A27,A28,A30,A45,XBOOLE_0:def 3; 1 + 2 <= len f by A41,AXIOMS:22; then x1 in {f/.(1+1)} by A49,TOPREAL1:def 8; then A50: x1 = f/.(1+1) by TARSKI:def 1; A51: 0+1 in dom LS by FINSEQ_5:6; 0+pW..f >= i3+pW..f by A15,A31,A48,CARD_1:56; then i3 <= 0 by REAL_1:53; then i3 = 0 by NAT_1:18; then LS/.1 = x1 by A1,A48,A50,A51,FINSEQ_5:55; then x1 = pW by FINSEQ_5:56; hence contradiction by A44,TARSKI:def 2; end; hence contradiction; suppose A52: i1+1 = i3+pW..f; 0+pW..f <= i3+pW..f by A35,REAL_1:55; then pW..f = i1+1 by A24,A31,A52,AXIOMS:21; then i1 = pW..f-1 by XCMPLX_1:26; then A53: i1 = pW..f-'1 by A42,BINARITH:def 3; i3+pW..f >= pW..f by NAT_1:29; then pW..f < len f by A34,AXIOMS:22; then pW..f+1 <= len f by NAT_1:38; then pW..f-'1 + (1+1) <= len f by A43,XCMPLX_1:1; then LSeg(f,i1) /\ LSeg(f,i3+(pW..f)) = {f/.(pW..f)} by A24,A43,A52,A53,TOPREAL1:def 8; then x1 in {f/.(pW..f)} by A25,A27,A28,A30,XBOOLE_0:def 3; then x1 = f/.(pW..f) by TARSKI:def 1 .= pW by A1,FINSEQ_5:41; hence contradiction by A44,TARSKI:def 2; end; hence contradiction; end; thus {N-min L~Cage(C,n),E-max L~Cage(C,n)} c= L~US /\ L~LS proof let x be set; assume A54: x in {N-min L~Cage(C,n),E-max L~Cage(C,n)}; per cases by A54,TARSKI:def 2; suppose x = N-min L~Cage(C,n); hence x in L~US /\ L~LS by A11,A17,A20,A21,XBOOLE_0:def 3; suppose x = E-max L~Cage(C,n); hence x in L~US /\ L~LS by A11,A12,A17,A19,XBOOLE_0:def 3; end; end; theorem Th4: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds Upper_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 A17: Nmi <> Wmi by SPRECT_2:61; then A18: 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 A19: 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 A18,A19,XBOOLE_1:1; then len (Cage(C,n)-:Wmi) >= 2 by CARD_1:56; then A20: rng (Cage(C,n)-:Wmi) c= L~(Cage(C,n)-:Wmi) by SPPOL_2:18; A21: Nmi..Cage(C,n) < Wmi..Cage(C,n) by A7,A12,AXIOMS:22; then A22: Nmi in rng (Cage(C,n)-:Wmi) by A2,A3,FINSEQ_5:49; A23: Ema..(Cage(C,n)-:Wmi) <> 1 proof assume A24: Ema..(Cage(C,n)-:Wmi) = 1; Nmi..(Cage(C,n)-:Wmi) = Nmi..Cage(C,n) by A2,A3,A21,SPRECT_5:3 .= 1 by A1,FINSEQ_6:47; hence contradiction by A5,A6,A13,A22,A24,FINSEQ_5:10; end; then A25: Ema in rng (Cage(C,n)-:Wmi/^1) by A13,FINSEQ_6:83; A26: 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 A27: Nmi <> Ema by A26,PSCOMP_1:104; not Ema in rng (Cage(C,n):-Wmi) proof assume A28: 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 A29: Nmi in rng (Cage(C,n):-Wmi) by REVROT_1:3; (Cage(C,n):-Wmi)/.1 = Wmi by FINSEQ_5:56; then A30: 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 A31: 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 A29,A30,TARSKI:def 2; end; then A32: 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 A31,A32,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,A20,A28,XBOOLE_0:def 3; then Ema in {Nmi,Wmi} by JORDAN1G:25; then Ema = Wmi by A27,TARSKI:def 2; hence contradiction by TOPREAL5:25; end; then A33: Ema in rng (Cage(C,n)-:Wmi/^1) \ rng (Cage(C,n):-Wmi) by A25,XBOOLE_0:def 4 ; A34: Wmi in rng (Cage(C,n):-Ema) by A3,A4,A12,FINSEQ_6:67; A35: Card {Nmi,Ema} = 2 by A27,CARD_2:76; (Cage(C,n):-Ema)/.len(Cage(C,n):-Ema) = Cage(C,n)/.len Cage(C,n) by A4,FINSEQ_5:57 .= Cage(C,n)/.1 by FINSEQ_6:def 1 .= Nmi by JORDAN9:34; then A36: Nmi in rng (Cage(C,n):-Ema) by REVROT_1:3; (Cage(C,n):-Ema)/.1 = Ema by FINSEQ_5:56; then A37: Ema in rng (Cage(C,n):-Ema) by FINSEQ_6:46; {Nmi,Ema} c= rng (Cage(C,n):-Ema) proof let x be set; assume x in {Nmi,Ema}; hence x in rng (Cage(C,n):-Ema) by A36,A37,TARSKI:def 2; end; then A38: Card {Nmi,Ema} c= Card rng (Cage(C,n):-Ema) by CARD_1:27; Card rng (Cage(C,n):-Ema) c= Card dom (Cage(C,n):-Ema) by YELLOW_6:3; then Card rng (Cage(C,n):-Ema) c= len (Cage(C,n):-Ema) by PRE_CIRC:21; then 2 c= len (Cage(C,n):-Ema) by A35,A38,XBOOLE_1:1; then len (Cage(C,n):-Ema) >= 2 by CARD_1:56; then A39: rng (Cage(C,n):-Ema) c= L~(Cage(C,n):-Ema) by SPPOL_2:18; not Wmi in rng (Cage(C,n)-:Ema) proof assume A40: Wmi in rng (Cage(C,n)-:Ema); then A41: Cage(C,n)-:Ema is non empty by FINSEQ_1:27; (Cage(C,n)-:Ema)/.1 = Cage(C,n)/.1 by A4,FINSEQ_5:47 .= Nmi by JORDAN9:34; then A42: Nmi in rng (Cage(C,n)-:Ema) by A41,FINSEQ_6:46; (Cage(C,n)-:Ema)/.len (Cage(C,n)-:Ema) = (Cage(C,n)-:Ema)/.(Ema..Cage(C,n)) by A4,FINSEQ_5:45 .= Ema by A4,FINSEQ_5:48; then A43: Ema in rng (Cage(C,n)-:Ema) by A41,REVROT_1:3; {Nmi,Ema} c= rng (Cage(C,n)-:Ema) proof let x be set; assume x in {Nmi,Ema}; hence x in rng (Cage(C,n)-:Ema) by A42,A43,TARSKI:def 2; end; then A44: Card {Nmi,Ema} c= Card rng (Cage(C,n)-:Ema) by CARD_1:27; Card rng (Cage(C,n)-:Ema) c= Card dom (Cage(C,n)-:Ema) by YELLOW_6:3; then Card rng (Cage(C,n)-:Ema) c= len (Cage(C,n)-:Ema) by PRE_CIRC:21; then 2 c= len (Cage(C,n)-:Ema) by A35,A44,XBOOLE_1:1; then len (Cage(C,n)-:Ema) >= 2 by CARD_1:56; then rng (Cage(C,n)-:Ema) c= L~(Cage(C,n)-:Ema) by SPPOL_2:18; then Wmi in L~(Cage(C,n)-:Ema) /\ L~(Cage(C,n):-Ema) by A34,A39,A40,XBOOLE_0:def 3 ; then Wmi in {Nmi,Ema} by Th3; then Wmi = Ema by A17,TARSKI:def 2; hence contradiction by TOPREAL5:25; end; then A45: Wmi in rng Cage(C,n) \ rng(Cage(C,n)-:Ema) by A3,XBOOLE_0:def 4; RotWmi-:Ema = ((Cage(C,n):-Wmi)^((Cage(C,n)-:Wmi)/^1))-:Ema by A3,FINSEQ_6:def 2 .= (Cage(C,n):-Wmi)^(((Cage(C,n)-:Wmi)/^1)-:Ema) by A33,FINSEQ_6:72 .= (Cage(C,n):-Wmi)^(((Cage(C,n)-:Wmi)-:Ema)/^1) by A13,A23,FINSEQ_6:65 .= ((Cage(C,n):-Ema):-Wmi)^(((Cage(C,n)-:Wmi)-:Ema)/^1) by A4,A45,FINSEQ_6:76 .= ((Cage(C,n):-Ema):-Wmi)^((Cage(C,n)-:Ema)/^1) by A3,A13,FINSEQ_6:80 .= ((Cage(C,n):-Ema)^((Cage(C,n)-:Ema)/^1)):-Wmi by A34,FINSEQ_6:69 .= RotEma:-Wmi by A4,FINSEQ_6:def 2; hence Upper_Seq(C,n) = Rotate(Cage(C,n),E-max L~Cage(C,n)):- W-min L~Cage(C,n) by JORDAN1E:def 1; end; theorem for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds W-min L~Cage(C,n) in rng Upper_Seq(C,n) & W-min L~Cage(C,n) in L~Upper_Seq(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; set p = W-min L~Cage(C,n); A1: Upper_Seq(C,n) = Rotate(Cage(C,n),p)-:E-max L~Cage(C,n) by JORDAN1E:def 1; A2: p 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 E-max L~Cage(C,n) in rng Rotate(Cage(C,n),p) by A2,FINSEQ_6:96; then Upper_Seq(C,n)/.1 = Rotate(Cage(C,n),p)/.1 by A1,FINSEQ_5:47; then Upper_Seq(C,n)/.1 = p by A2,FINSEQ_6:98; hence A3: p in rng Upper_Seq(C,n) by FINSEQ_6:46; len Upper_Seq(C,n) >= 2 by TOPREAL1:def 10; then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18; hence p in L~Upper_Seq(C,n) by A3; end; theorem for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds W-max L~Cage(C,n) in rng Upper_Seq(C,n) & W-max L~Cage(C,n) in L~Upper_Seq(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; set x = W-max L~Cage(C,n); set p = W-min L~Cage(C,n); set f = Rotate(Cage(C,n),E-max L~Cage(C,n)); E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; then A1: rng f = rng Cage(C,n) by FINSEQ_6:96; A2: x in rng Cage(C,n) by SPRECT_2:48; A3: p in rng Cage(C,n) by SPRECT_2:47; A4: Lower_Seq(C,n) = f-:W-min L~Cage(C,n) by JORDAN1G:26; A5: 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 W-min L~Cage(C,n) in rng f by A5,FINSEQ_6:96; then A6: Lower_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:47; A7: Lower_Seq(C,n)/.1 = E-max L~Cage(C,n) by JORDAN1F:6; A8: L~Cage(C,n) = L~f by REVROT_1:33; then (W-min L~f)..f < (W-max L~f)..f by A6,A7,SPRECT_5:43; then x in rng(f:-p) by A1,A2,A3,A8,FINSEQ_6:67; hence A9: x in rng Upper_Seq(C,n) by Th4; len Upper_Seq(C,n) >= 2 by TOPREAL1:def 10; then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18; hence x in L~Upper_Seq(C,n) by A9; end; theorem Th7: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds N-min L~Cage(C,n) in rng Upper_Seq(C,n) & N-min L~Cage(C,n) in L~Upper_Seq(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; set x = N-min L~Cage(C,n); set p = W-min L~Cage(C,n); set f = Rotate(Cage(C,n),E-max L~Cage(C,n)); E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; then A1: rng f = rng Cage(C,n) by FINSEQ_6:96; A2: x in rng Cage(C,n) by SPRECT_2:43; A3: p in rng Cage(C,n) by SPRECT_2:47; A4: Lower_Seq(C,n) = f-:W-min L~Cage(C,n) by JORDAN1G:26; A5: 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 W-min L~Cage(C,n) in rng f by A5,FINSEQ_6:96; then A6: Lower_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:47; A7: Lower_Seq(C,n)/.1 = E-max L~Cage(C,n) by JORDAN1F:6; A8: L~Cage(C,n) = L~f by REVROT_1:33; then A9: (W-min L~f)..f < (W-max L~f)..f by A6,A7,SPRECT_5:43; (W-max L~f)..f <= (N-min L~f)..f by A6,A7,A8,SPRECT_5:44; then p..f < x..f by A8,A9,AXIOMS:22; then x in rng(f:-p) by A1,A2,A3,FINSEQ_6:67; hence A10: x in rng Upper_Seq(C,n) by Th4; len Upper_Seq(C,n) >= 2 by TOPREAL1:def 10; then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18; hence x in L~Upper_Seq(C,n) by A10; end; theorem for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds N-max L~Cage(C,n) in rng Upper_Seq(C,n) & N-max L~Cage(C,n) in L~Upper_Seq(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; set x = N-max L~Cage(C,n); set p = W-min L~Cage(C,n); set f = Rotate(Cage(C,n),E-max L~Cage(C,n)); E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; then A1: rng f = rng Cage(C,n) by FINSEQ_6:96; A2: x in rng Cage(C,n) by SPRECT_2:44; A3: p in rng Cage(C,n) by SPRECT_2:47; A4: Lower_Seq(C,n) = f-:W-min L~Cage(C,n) by JORDAN1G:26; A5: 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 W-min L~Cage(C,n) in rng f by A5,FINSEQ_6:96; then A6: Lower_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:47; A7: Lower_Seq(C,n)/.1 = E-max L~Cage(C,n) by JORDAN1F:6; A8: L~Cage(C,n) = L~f by REVROT_1:33; then A9: (W-min L~f)..f < (W-max L~f)..f by A6,A7,SPRECT_5:43; A10: (W-max L~f)..f <= (N-min L~f)..f by A6,A7,A8,SPRECT_5:44; per cases; suppose N-max L~f <> E-max L~f; then (N-min L~f)..f < (N-max L~f)..f by A6,A7,A8,SPRECT_5:45; then (W-max L~f)..f < (N-max L~f)..f by A10,AXIOMS:22; then p..f < x..f by A8,A9,AXIOMS:22; then x in rng(f:-p) by A1,A2,A3,FINSEQ_6:67; hence A11: x in rng Upper_Seq(C,n) by Th4; len Upper_Seq(C,n) >= 2 by TOPREAL1:def 10; then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18; hence x in L~Upper_Seq(C,n) by A11; suppose A12: N-max L~f = E-max L~f; A13: Upper_Seq(C,n) = Rotate(Cage(C,n),p)-:E-max L~Cage(C,n) by JORDAN1E:def 1; A14: 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 A15: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by A14,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)); hence A16: x in rng Upper_Seq(C,n) by A8,A12,A13,A15,FINSEQ_5:49; len Upper_Seq(C,n) >= 2 by TOPREAL1:def 10; then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18; hence x in L~Upper_Seq(C,n) by A16; end; theorem for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds E-max L~Cage(C,n) in rng Upper_Seq(C,n) & E-max L~Cage(C,n) in L~Upper_Seq(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; set x = E-max L~Cage(C,n); set p = W-min L~Cage(C,n); A1: Upper_Seq(C,n) = Rotate(Cage(C,n),p)-: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)); hence A4: x in rng Upper_Seq(C,n) by A1,A3,FINSEQ_5:49; len Upper_Seq(C,n) >= 2 by TOPREAL1:def 10; then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18; hence x in L~Upper_Seq(C,n) by A4; end; theorem for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds E-max L~Cage(C,n) in rng Lower_Seq(C,n) & E-max L~Cage(C,n) in L~Lower_Seq(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; set p = E-max L~Cage(C,n); Lower_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n)):-p by JORDAN1E:def 2 ; hence A1: p in rng Lower_Seq(C,n) by FINSEQ_6:66; len Lower_Seq(C,n) >= 2 by TOPREAL1:def 10; then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18; hence p in L~Lower_Seq(C,n) by A1; end; theorem for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds E-min L~Cage(C,n) in rng Lower_Seq(C,n) & E-min L~Cage(C,n) in L~Lower_Seq(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; set x = E-min L~Cage(C,n); set p = E-max L~Cage(C,n); set f = Rotate(Cage(C,n),W-min L~Cage(C,n)); W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; then A1: rng f = rng Cage(C,n) by FINSEQ_6:96; A2: x in rng Cage(C,n) by SPRECT_2:49; A3: p in rng Cage(C,n) by SPRECT_2:50; A4: Upper_Seq(C,n) = f-:E-max L~Cage(C,n) by JORDAN1E:def 1; A5: 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 E-max L~Cage(C,n) in rng f by A5,FINSEQ_6:96; then A6: Upper_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:47; A7: Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by JORDAN1F:5; A8: L~Cage(C,n) = L~f by REVROT_1:33; then (E-max L~f)..f < (E-min L~f)..f by A6,A7,SPRECT_5:27; then x in rng(f:-p) by A1,A2,A3,A8,FINSEQ_6:67; hence A9: x in rng Lower_Seq(C,n) by JORDAN1E:def 2; len Lower_Seq(C,n) >= 2 by TOPREAL1:def 10; then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18; hence x in L~Lower_Seq(C,n) by A9; end; theorem Th12: for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds S-max L~Cage(C,n) in rng Lower_Seq(C,n) & S-max L~Cage(C,n) in L~Lower_Seq(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; set x = S-max L~Cage(C,n); set p = E-max L~Cage(C,n); set f = Rotate(Cage(C,n),W-min L~Cage(C,n)); W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; then A1: rng f = rng Cage(C,n) by FINSEQ_6:96; A2: x in rng Cage(C,n) by SPRECT_2:46; A3: p in rng Cage(C,n) by SPRECT_2:50; A4: Upper_Seq(C,n) = f-:E-max L~Cage(C,n) by JORDAN1E:def 1; A5: 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 E-max L~Cage(C,n) in rng f by A5,FINSEQ_6:96; then A6: Upper_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:47; A7: Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by JORDAN1F:5; A8: L~Cage(C,n) = L~f by REVROT_1:33; then A9: (E-max L~f)..f < (E-min L~f)..f by A6,A7,SPRECT_5:27; (E-min L~f)..f <= (S-max L~f)..f by A6,A7,A8,SPRECT_5:28; then p..f < x..f by A8,A9,AXIOMS:22; then x in rng(f:-p) by A1,A2,A3,FINSEQ_6:67; hence A10: x in rng Lower_Seq(C,n) by JORDAN1E:def 2; len Lower_Seq(C,n) >= 2 by TOPREAL1:def 10; then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18; hence x in L~Lower_Seq(C,n) by A10; end; theorem for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds S-min L~Cage(C,n) in rng Lower_Seq(C,n) & S-min L~Cage(C,n) in L~Lower_Seq(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; set x = S-min L~Cage(C,n); set p = E-max L~Cage(C,n); set f = Rotate(Cage(C,n),W-min L~Cage(C,n)); W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; then A1: rng f = rng Cage(C,n) by FINSEQ_6:96; A2: x in rng Cage(C,n) by SPRECT_2:45; A3: p in rng Cage(C,n) by SPRECT_2:50; A4: Upper_Seq(C,n) = f-:E-max L~Cage(C,n) by JORDAN1E:def 1; A5: 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 E-max L~Cage(C,n) in rng f by A5,FINSEQ_6:96; then A6: Upper_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:47; A7: Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by JORDAN1F:5; A8: L~Cage(C,n) = L~f by REVROT_1:33; then A9: (E-max L~f)..f < (E-min L~f)..f by A6,A7,SPRECT_5:27; A10: (E-min L~f)..f <= (S-max L~f)..f by A6,A7,A8,SPRECT_5:28; per cases; suppose S-min L~f <> W-min L~f; then (S-max L~f)..f < (S-min L~f)..f by A6,A7,A8,SPRECT_5:29; then (E-min L~f)..f < (S-min L~f)..f by A10,AXIOMS:22; then p..f < x..f by A8,A9,AXIOMS:22; then x in rng(f:-p) by A1,A2,A3,FINSEQ_6:67; hence A11: x in rng Lower_Seq(C,n) by JORDAN1E:def 2; len Lower_Seq(C,n) >= 2 by TOPREAL1:def 10; then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18; hence x in L~Lower_Seq(C,n) by A11; suppose A12: S-min L~f = W-min L~f; Lower_Seq(C,n)/.(len Lower_Seq(C,n)) = W-min L~Cage(C,n) by JORDAN1F:8; hence A13: x in rng Lower_Seq(C,n) by A8,A12,REVROT_1:3; len Lower_Seq(C,n) >= 2 by TOPREAL1:def 10; then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18; hence x in L~Lower_Seq(C,n) by A13; end; theorem for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds W-min L~Cage(C,n) in rng Lower_Seq(C,n) & W-min L~Cage(C,n) in L~Lower_Seq(C,n) proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; set p = W-min L~Cage(C,n); Lower_Seq(C,n)/.(len Lower_Seq(C,n)) = p by JORDAN1F:8; hence A1: p in rng Lower_Seq(C,n) by REVROT_1:3; len Lower_Seq(C,n) >= 2 by TOPREAL1:def 10; then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18; hence p in L~Lower_Seq(C,n) by A1; end; theorem for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & N-min Y in X holds N-min X = N-min Y proof let X,Y be non empty compact Subset of TOP-REAL 2; assume that A1: X c= Y and A2: N-min Y in X; A3: N-bound X <= N-bound Y by A1,JORDAN1E:1; A4: (N-min X)`2 = N-bound X & (N-min Y)`2 = N-bound Y by PSCOMP_1:94; N-bound X >= (N-min Y)`2 by A2,PSCOMP_1:71; then A5: N-bound X = N-bound Y by A3,A4,AXIOMS:21; then N-min Y in N-most X by A2,A4,SPRECT_2:14; then A6: (N-min X)`1 <= (N-min Y)`1 by PSCOMP_1:98; N-min X in X by SPRECT_1:13; then N-min X in N-most Y by A1,A4,A5,SPRECT_2:14; then (N-min X)`1 >= (N-min Y)`1 by PSCOMP_1:98; then (N-min X)`1 = (N-min Y)`1 by A6,AXIOMS:21; hence N-min X = N-min Y by A4,A5,TOPREAL3:11; end; theorem for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & N-max Y in X holds N-max X = N-max Y proof let X,Y be non empty compact Subset of TOP-REAL 2; assume that A1: X c= Y and A2: N-max Y in X; A3: N-bound X <= N-bound Y by A1,JORDAN1E:1; A4: (N-max X)`2 = N-bound X & (N-max Y)`2 = N-bound Y by PSCOMP_1:94; N-bound X >= (N-max Y)`2 by A2,PSCOMP_1:71; then A5: N-bound X = N-bound Y by A3,A4,AXIOMS:21; then N-max Y in N-most X by A2,A4,SPRECT_2:14; then A6: (N-max X)`1 >= (N-max Y)`1 by PSCOMP_1:98; N-max X in X by SPRECT_1:13; then N-max X in N-most Y by A1,A4,A5,SPRECT_2:14; then (N-max X)`1 <= (N-max Y)`1 by PSCOMP_1:98; then (N-max X)`1 = (N-max Y)`1 by A6,AXIOMS:21; hence N-max X = N-max Y by A4,A5,TOPREAL3:11; end; theorem for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & E-min Y in X holds E-min X = E-min Y proof let X,Y be non empty compact Subset of TOP-REAL 2; assume that A1: X c= Y and A2: E-min Y in X; A3: E-bound X <= E-bound Y by A1,JORDAN1E:2; A4: (E-min X)`1 = E-bound X & (E-min Y)`1 = E-bound Y by PSCOMP_1:104; E-bound X >= (E-min Y)`1 by A2,PSCOMP_1:71; then A5: E-bound X = E-bound Y by A3,A4,AXIOMS:21; then E-min Y in E-most X by A2,A4,SPRECT_2:17; then A6: (E-min X)`2 <= (E-min Y)`2 by PSCOMP_1:108; E-min X in X by SPRECT_1:16; then E-min X in E-most Y by A1,A4,A5,SPRECT_2:17; then (E-min X)`2 >= (E-min Y)`2 by PSCOMP_1:108; then (E-min X)`2 = (E-min Y)`2 by A6,AXIOMS:21; hence E-min X = E-min Y by A4,A5,TOPREAL3:11; end; theorem for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & E-max Y in X holds E-max X = E-max Y proof let X,Y be non empty compact Subset of TOP-REAL 2; assume that A1: X c= Y and A2: E-max Y in X; A3: E-bound X <= E-bound Y by A1,JORDAN1E:2; A4: (E-max X)`1 = E-bound X & (E-max Y)`1 = E-bound Y by PSCOMP_1:104; E-bound X >= (E-max Y)`1 by A2,PSCOMP_1:71; then A5: E-bound X = E-bound Y by A3,A4,AXIOMS:21; then E-max Y in E-most X by A2,A4,SPRECT_2:17; then A6: (E-max X)`2 >= (E-max Y)`2 by PSCOMP_1:108; E-max X in X by SPRECT_1:16; then E-max X in E-most Y by A1,A4,A5,SPRECT_2:17; then (E-max X)`2 <= (E-max Y)`2 by PSCOMP_1:108; then (E-max X)`2 = (E-max Y)`2 by A6,AXIOMS:21; hence E-max X = E-max Y by A4,A5,TOPREAL3:11; end; theorem for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & S-min Y in X holds S-min X = S-min Y proof let X,Y be non empty compact Subset of TOP-REAL 2; assume that A1: X c= Y and A2: S-min Y in X; A3: S-bound X >= S-bound Y by A1,JORDAN1E:3; A4: (S-min X)`2 = S-bound X & (S-min Y)`2 = S-bound Y by PSCOMP_1:114; S-bound X <= (S-min Y)`2 by A2,PSCOMP_1:71; then A5: S-bound X = S-bound Y by A3,A4,AXIOMS:21; then S-min Y in S-most X by A2,A4,SPRECT_2:15; then A6: (S-min X)`1 <= (S-min Y)`1 by PSCOMP_1:118; S-min X in X by SPRECT_1:14; then S-min X in S-most Y by A1,A4,A5,SPRECT_2:15; then (S-min X)`1 >= (S-min Y)`1 by PSCOMP_1:118; then (S-min X)`1 = (S-min Y)`1 by A6,AXIOMS:21; hence S-min X = S-min Y by A4,A5,TOPREAL3:11; end; theorem for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & S-max Y in X holds S-max X = S-max Y proof let X,Y be non empty compact Subset of TOP-REAL 2; assume that A1: X c= Y and A2: S-max Y in X; A3: S-bound X >= S-bound Y by A1,JORDAN1E:3; A4: (S-max X)`2 = S-bound X & (S-max Y)`2 = S-bound Y by PSCOMP_1:114; S-bound X <= (S-max Y)`2 by A2,PSCOMP_1:71; then A5: S-bound X = S-bound Y by A3,A4,AXIOMS:21; then S-max Y in S-most X by A2,A4,SPRECT_2:15; then A6: (S-max X)`1 >= (S-max Y)`1 by PSCOMP_1:118; S-max X in X by SPRECT_1:14; then S-max X in S-most Y by A1,A4,A5,SPRECT_2:15; then (S-max X)`1 <= (S-max Y)`1 by PSCOMP_1:118; then (S-max X)`1 = (S-max Y)`1 by A6,AXIOMS:21; hence S-max X = S-max Y by A4,A5,TOPREAL3:11; end; theorem Th21: for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & W-min Y in X holds W-min X = W-min Y proof let X,Y be non empty compact Subset of TOP-REAL 2; assume that A1: X c= Y and A2: W-min Y in X; A3: W-bound X >= W-bound Y by A1,JORDAN1E:4; A4: (W-min X)`1 = W-bound X & (W-min Y)`1 = W-bound Y by PSCOMP_1:84; W-bound X <= (W-min Y)`1 by A2,PSCOMP_1:71; then A5: W-bound X = W-bound Y by A3,A4,AXIOMS:21; then W-min Y in W-most X by A2,A4,SPRECT_2:16; then A6: (W-min X)`2 <= (W-min Y)`2 by PSCOMP_1:88; W-min X in X by SPRECT_1:15; then W-min X in W-most Y by A1,A4,A5,SPRECT_2:16; then (W-min X)`2 >= (W-min Y)`2 by PSCOMP_1:88; then (W-min X)`2 = (W-min Y)`2 by A6,AXIOMS:21; hence W-min X = W-min Y by A4,A5,TOPREAL3:11; end; theorem for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & W-max Y in X holds W-max X = W-max Y proof let X,Y be non empty compact Subset of TOP-REAL 2; assume that A1: X c= Y and A2: W-max Y in X; A3: W-bound X >= W-bound Y by A1,JORDAN1E:4; A4: (W-max X)`1 = W-bound X & (W-max Y)`1 = W-bound Y by PSCOMP_1:84; W-bound X <= (W-max Y)`1 by A2,PSCOMP_1:71; then A5: W-bound X = W-bound Y by A3,A4,AXIOMS:21; then W-max Y in W-most X by A2,A4,SPRECT_2:16; then A6: (W-max X)`2 >= (W-max Y)`2 by PSCOMP_1:88; W-max X in X by SPRECT_1:15; then W-max X in W-most Y by A1,A4,A5,SPRECT_2:16; then (W-max X)`2 <= (W-max Y)`2 by PSCOMP_1:88; then (W-max X)`2 = (W-max Y)`2 by A6,AXIOMS:21; hence W-max X = W-max Y by A4,A5,TOPREAL3:11; end; theorem Th23: for X,Y be non empty compact Subset of TOP-REAL 2 st N-bound X < N-bound Y holds N-bound (X\/Y) = N-bound Y proof let X,Y be non empty compact Subset of TOP-REAL 2; assume N-bound X < N-bound Y; then max(N-bound X,N-bound Y) = N-bound Y by SQUARE_1:def 2; hence N-bound (X\/Y) = N-bound Y by SPRECT_1:56; end; theorem Th24: for X,Y be non empty compact Subset of TOP-REAL 2 st E-bound X < E-bound Y holds E-bound (X\/Y) = E-bound Y proof let X,Y be non empty compact Subset of TOP-REAL 2; assume E-bound X < E-bound Y; then max(E-bound X,E-bound Y) = E-bound Y by SQUARE_1:def 2; hence E-bound (X\/Y) = E-bound Y by SPRECT_1:57; end; theorem Th25: for X,Y be non empty compact Subset of TOP-REAL 2 st S-bound X < S-bound Y holds S-bound (X\/Y) = S-bound X proof let X,Y be non empty compact Subset of TOP-REAL 2; assume S-bound X < S-bound Y; then min(S-bound X,S-bound Y) = S-bound X by SQUARE_1:def 1; hence S-bound (X\/Y) = S-bound X by SPRECT_1:55; end; theorem Th26: for X,Y be non empty compact Subset of TOP-REAL 2 st W-bound X < W-bound Y holds W-bound (X\/Y) = W-bound X proof let X,Y be non empty compact Subset of TOP-REAL 2; assume W-bound X < W-bound Y; then min(W-bound X,W-bound Y) = W-bound X by SQUARE_1:def 1; hence W-bound (X\/Y) = W-bound X by SPRECT_1:54; end; theorem for X,Y be non empty compact Subset of TOP-REAL 2 st N-bound X < N-bound Y holds N-min (X\/Y) = N-min Y proof let X,Y be non empty compact Subset of TOP-REAL 2; A1: X\/Y is compact by COMPTS_1:19; assume A2: N-bound X < N-bound Y; then A3: N-bound (X\/Y) = N-bound Y by Th23; A4: (N-min(X\/Y))`2 = N-bound (X\/Y) & (N-min Y)`2 = N-bound Y by PSCOMP_1:94; A5: Y c= X\/Y by XBOOLE_1:7; N-min Y in Y by SPRECT_1:13; then N-min Y in N-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:14; then A6: (N-min(X\/Y))`1 <= (N-min Y)`1 by A1,PSCOMP_1:98; A7: N-min(X\/Y) in X\/Y by A1,SPRECT_1:13; per cases by A7,XBOOLE_0:def 2; suppose N-min(X\/Y) in Y; then N-min(X\/Y) in N-most Y by A3,A4,SPRECT_2:14; then (N-min(X\/Y))`1 >= (N-min Y)`1 by PSCOMP_1:98; then (N-min(X\/Y))`1 = (N-min Y)`1 by A6,AXIOMS:21; hence N-min (X\/Y) = N-min Y by A3,A4,TOPREAL3:11; suppose N-min(X\/Y) in X; hence N-min (X\/Y) = N-min Y by A2,A3,A4,PSCOMP_1:71; end; theorem for X,Y be non empty compact Subset of TOP-REAL 2 st N-bound X < N-bound Y holds N-max (X\/Y) = N-max Y proof let X,Y be non empty compact Subset of TOP-REAL 2; A1: X\/Y is compact by COMPTS_1:19; assume A2: N-bound X < N-bound Y; then A3: N-bound (X\/Y) = N-bound Y by Th23; A4: (N-max(X\/Y))`2 = N-bound (X\/Y) & (N-max Y)`2 = N-bound Y by PSCOMP_1:94; A5: Y c= X\/Y by XBOOLE_1:7; N-max Y in Y by SPRECT_1:13; then N-max Y in N-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:14; then A6: (N-max(X\/Y))`1 >= (N-max Y)`1 by A1,PSCOMP_1:98; A7: N-max(X\/Y) in X\/Y by A1,SPRECT_1:13; per cases by A7,XBOOLE_0:def 2; suppose N-max(X\/Y) in Y; then N-max(X\/Y) in N-most Y by A3,A4,SPRECT_2:14; then (N-max(X\/Y))`1 <= (N-max Y)`1 by PSCOMP_1:98; then (N-max(X\/Y))`1 = (N-max Y)`1 by A6,AXIOMS:21; hence N-max (X\/Y) = N-max Y by A3,A4,TOPREAL3:11; suppose N-max(X\/Y) in X; hence N-max (X\/Y) = N-max Y by A2,A3,A4,PSCOMP_1:71; end; theorem for X,Y be non empty compact Subset of TOP-REAL 2 st E-bound X < E-bound Y holds E-min (X\/Y) = E-min Y proof let X,Y be non empty compact Subset of TOP-REAL 2; A1: X\/Y is compact by COMPTS_1:19; assume A2: E-bound X < E-bound Y; then A3: E-bound (X\/Y) = E-bound Y by Th24; A4: (E-min(X\/Y))`1 = E-bound (X\/Y) & (E-min Y)`1 = E-bound Y by PSCOMP_1:104; A5: Y c= X\/Y by XBOOLE_1:7; E-min Y in Y by SPRECT_1:16; then E-min Y in E-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:17; then A6: (E-min(X\/Y))`2 <= (E-min Y)`2 by A1,PSCOMP_1:108; A7: E-min(X\/Y) in X\/Y by A1,SPRECT_1:16; per cases by A7,XBOOLE_0:def 2; suppose E-min(X\/Y) in Y; then E-min(X\/Y) in E-most Y by A3,A4,SPRECT_2:17; then (E-min(X\/Y))`2 >= (E-min Y)`2 by PSCOMP_1:108; then (E-min(X\/Y))`2 = (E-min Y)`2 by A6,AXIOMS:21; hence E-min (X\/Y) = E-min Y by A3,A4,TOPREAL3:11; suppose E-min(X\/Y) in X; hence E-min (X\/Y) = E-min Y by A2,A3,A4,PSCOMP_1:71; end; theorem for X,Y be non empty compact Subset of TOP-REAL 2 st E-bound X < E-bound Y holds E-max (X\/Y) = E-max Y proof let X,Y be non empty compact Subset of TOP-REAL 2; A1: X\/Y is compact by COMPTS_1:19; assume A2: E-bound X < E-bound Y; then A3: E-bound (X\/Y) = E-bound Y by Th24; A4: (E-max(X\/Y))`1 = E-bound (X\/Y) & (E-max Y)`1 = E-bound Y by PSCOMP_1:104; A5: Y c= X\/Y by XBOOLE_1:7; E-max Y in Y by SPRECT_1:16; then E-max Y in E-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:17; then A6: (E-max(X\/Y))`2 >= (E-max Y)`2 by A1,PSCOMP_1:108; A7: E-max(X\/Y) in X\/Y by A1,SPRECT_1:16; per cases by A7,XBOOLE_0:def 2; suppose E-max(X\/Y) in Y; then E-max(X\/Y) in E-most Y by A3,A4,SPRECT_2:17; then (E-max(X\/Y))`2 <= (E-max Y)`2 by PSCOMP_1:108; then (E-max(X\/Y))`2 = (E-max Y)`2 by A6,AXIOMS:21; hence E-max (X\/Y) = E-max Y by A3,A4,TOPREAL3:11; suppose E-max(X\/Y) in X; hence E-max (X\/Y) = E-max Y by A2,A3,A4,PSCOMP_1:71; end; theorem for X,Y be non empty compact Subset of TOP-REAL 2 st S-bound X < S-bound Y holds S-min (X\/Y) = S-min X proof let X,Y be non empty compact Subset of TOP-REAL 2; A1: X\/Y is compact by COMPTS_1:19; assume A2: S-bound X < S-bound Y; then A3: S-bound (X\/Y) = S-bound X by Th25; A4: (S-min(X\/Y))`2 = S-bound (X\/Y) & (S-min X)`2 = S-bound X by PSCOMP_1:114; A5: X c= X\/Y by XBOOLE_1:7; S-min X in X by SPRECT_1:14; then S-min X in S-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:15; then A6: (S-min(X\/Y))`1 <= (S-min X)`1 by A1,PSCOMP_1:118; A7: S-min(X\/Y) in X\/Y by A1,SPRECT_1:14; per cases by A7,XBOOLE_0:def 2; suppose S-min(X\/Y) in X; then S-min(X\/Y) in S-most X by A3,A4,SPRECT_2:15; then (S-min(X\/Y))`1 >= (S-min X)`1 by PSCOMP_1:118; then (S-min(X\/Y))`1 = (S-min X)`1 by A6,AXIOMS:21; hence S-min (X\/Y) = S-min X by A3,A4,TOPREAL3:11; suppose S-min(X\/Y) in Y; hence S-min (X\/Y) = S-min X by A2,A3,A4,PSCOMP_1:71; end; theorem for X,Y be non empty compact Subset of TOP-REAL 2 st S-bound X < S-bound Y holds S-max (X\/Y) = S-max X proof let X,Y be non empty compact Subset of TOP-REAL 2; A1: X\/Y is compact by COMPTS_1:19; assume A2: S-bound X < S-bound Y; then A3: S-bound (X\/Y) = S-bound X by Th25; A4: (S-max(X\/Y))`2 = S-bound (X\/Y) & (S-max X)`2 = S-bound X by PSCOMP_1:114; A5: X c= X\/Y by XBOOLE_1:7; S-max X in X by SPRECT_1:14; then S-max X in S-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:15; then A6: (S-max(X\/Y))`1 >= (S-max X)`1 by A1,PSCOMP_1:118; A7: S-max(X\/Y) in X\/Y by A1,SPRECT_1:14; per cases by A7,XBOOLE_0:def 2; suppose S-max(X\/Y) in X; then S-max(X\/Y) in S-most X by A3,A4,SPRECT_2:15; then (S-max(X\/Y))`1 <= (S-max X)`1 by PSCOMP_1:118; then (S-max(X\/Y))`1 = (S-max X)`1 by A6,AXIOMS:21; hence S-max (X\/Y) = S-max X by A3,A4,TOPREAL3:11; suppose S-max(X\/Y) in Y; hence S-max (X\/Y) = S-max X by A2,A3,A4,PSCOMP_1:71; end; theorem Th33: for X,Y be non empty compact Subset of TOP-REAL 2 st W-bound X < W-bound Y holds W-min (X\/Y) = W-min X proof let X,Y be non empty compact Subset of TOP-REAL 2; A1: X\/Y is compact by COMPTS_1:19; assume A2: W-bound X < W-bound Y; then A3: W-bound (X\/Y) = W-bound X by Th26; A4: (W-min(X\/Y))`1 = W-bound (X\/Y) & (W-min X)`1 = W-bound X by PSCOMP_1:84; A5: X c= X\/Y by XBOOLE_1:7; W-min X in X by SPRECT_1:15; then W-min X in W-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:16; then A6: (W-min(X\/Y))`2 <= (W-min X)`2 by A1,PSCOMP_1:88; A7: W-min(X\/Y) in X\/Y by A1,SPRECT_1:15; per cases by A7,XBOOLE_0:def 2; suppose W-min(X\/Y) in X; then W-min(X\/Y) in W-most X by A3,A4,SPRECT_2:16; then (W-min(X\/Y))`2 >= (W-min X)`2 by PSCOMP_1:88; then (W-min(X\/Y))`2 = (W-min X)`2 by A6,AXIOMS:21; hence W-min (X\/Y) = W-min X by A3,A4,TOPREAL3:11; suppose W-min(X\/Y) in Y; hence W-min (X\/Y) = W-min X by A2,A3,A4,PSCOMP_1:71; end; theorem for X,Y be non empty compact Subset of TOP-REAL 2 st W-bound X < W-bound Y holds W-max (X\/Y) = W-max X proof let X,Y be non empty compact Subset of TOP-REAL 2; A1: X\/Y is compact by COMPTS_1:19; assume A2: W-bound X < W-bound Y; then A3: W-bound (X\/Y) = W-bound X by Th26; A4: (W-max(X\/Y))`1 = W-bound (X\/Y) & (W-max X)`1 = W-bound X by PSCOMP_1:84; A5: X c= X\/Y by XBOOLE_1:7; W-max X in X by SPRECT_1:15; then W-max X in W-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:16; then A6: (W-max(X\/Y))`2 >= (W-max X)`2 by A1,PSCOMP_1:88; A7: W-max(X\/Y) in X\/Y by A1,SPRECT_1:15; per cases by A7,XBOOLE_0:def 2; suppose W-max(X\/Y) in X; then W-max(X\/Y) in W-most X by A3,A4,SPRECT_2:16; then (W-max(X\/Y))`2 <= (W-max X)`2 by PSCOMP_1:88; then (W-max(X\/Y))`2 = (W-max X)`2 by A6,AXIOMS:21; hence W-max (X\/Y) = W-max X by A3,A4,TOPREAL3:11; suppose W-max(X\/Y) in Y; hence W-max (X\/Y) = W-max X by A2,A3,A4,PSCOMP_1:71; end; theorem Th35: for f be non empty FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st f is_S-Seq & p in L~f holds L_Cut(f,p)/.len L_Cut(f,p) = f/.len f proof let f be non empty FinSequence of TOP-REAL 2; let p be Point of TOP-REAL 2; assume that A1: f is_S-Seq and A2: p in L~f; A3: len f in dom f by SCMFSA_7:12; L_Cut(f,p) <> {} by A2,JORDAN1E:7; then len L_Cut(f,p) in dom L_Cut(f,p) by SCMFSA_7:12; hence L_Cut(f,p)/.len L_Cut(f,p) = L_Cut(f,p).len L_Cut(f,p) by FINSEQ_4:def 4 .= f.len f by A1,A2,JORDAN1B:5 .= f/.len f by A3,FINSEQ_4:def 4; end; theorem Th36: for f be non constant standard special_circular_sequence for p,q be Point of TOP-REAL 2 for g be connected Subset of TOP-REAL 2 st p in RightComp f & q in LeftComp f & p in g & q in g holds g meets L~f proof let f be non constant standard special_circular_sequence; let p,q be Point of TOP-REAL 2; let g be connected Subset of TOP-REAL 2; assume that A1: p in RightComp f & q in LeftComp f and A2: p in g & q in g; assume g misses L~f; then g c= (L~f)` by TDLAT_1:2; then g c= (L~f)`; then g c= the carrier of (TOP-REAL 2)|(L~f)` by JORDAN1:1; then reconsider A = g as Subset of (TOP-REAL 2)|(L~f)`; A3: A is connected by CONNSP_1:24; RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2; then consider R being Subset of (TOP-REAL 2)|(L~f)` such that A4: R = RightComp f and A5: R is_a_component_of (TOP-REAL 2)|(L~f)` by CONNSP_1:def 6; LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1; then consider L being Subset of (TOP-REAL 2)|(L~f)` such that A6: L = LeftComp f and A7: L is_a_component_of (TOP-REAL 2)|(L~f)` by CONNSP_1:def 6; R /\ A <> {} & L /\ A <> {} by A1,A2,A4,A6,XBOOLE_0:def 3; then R meets A & L meets A by XBOOLE_0:def 7; then RightComp f = LeftComp f by A3,A4,A5,A6,A7,JORDAN2C:100; hence contradiction by SPRECT_4:7; end; definition cluster non constant standard s.c.c. (being_S-Seq FinSequence of TOP-REAL 2); existence proof consider C be Simple_closed_curve; consider n be Nat; A1: len Upper_Seq(C,n) >= 2 by TOPREAL1:def 10; A2: Upper_Seq(C,n) is_sequence_on Gauge(C,n) by JORDAN1G:4; take Upper_Seq(C,n); thus thesis by A1,A2,JGRAPH_1:16,JORDAN8:8; end; end; theorem Th37: for f be S-Sequence_in_R2 for p be Point of TOP-REAL 2 st p in rng f holds L_Cut(f,p) = mid(f,p..f,len f) proof let f be S-Sequence_in_R2; let p be Point of TOP-REAL 2; assume p in rng f; then consider i be Nat such that A1: i in dom f and A2: f.i = p by FINSEQ_2:11; A3: 0+1 <= i & i <= len f by A1,FINSEQ_3:27; len f >= 2 by TOPREAL1:def 10; then A4: len f >= 1 by AXIOMS:22; per cases by A3,REAL_1:def 5; suppose i > 1; then A5: Index(p,f) + 1 = i by A2,A3,JORDAN3:45; then L_Cut(f,p) = mid(f,Index(p,f)+1,len f) by A2,JORDAN3:def 4; hence L_Cut(f,p) = mid(f,p..f,len f) by A1,A2,A5,FINSEQ_5:12; suppose A6: i = 1; thus L_Cut(f,p) = L_Cut(f,f/.i) by A1,A2,FINSEQ_4:def 4 .= f by A6,JORDAN5B:30 .= mid(f,1,len f) by A4,JORDAN3:29 .= mid(f,p..f,len f) by A1,A2,A6,FINSEQ_5:12; end; theorem Th38: for M be Go-board for f be S-Sequence_in_R2 st f is_sequence_on M for p be Point of TOP-REAL 2 st p in rng f holds R_Cut(f,p) is_sequence_on M proof let M be Go-board; let f be S-Sequence_in_R2; assume A1: f is_sequence_on M; let p be Point of TOP-REAL 2; assume p in rng f; then R_Cut(f,p) = mid(f,1,p..f) by JORDAN1G:57; hence R_Cut(f,p) is_sequence_on M by A1,JORDAN1H:33; end; theorem Th39: for M be Go-board for f be S-Sequence_in_R2 st f is_sequence_on M for p be Point of TOP-REAL 2 st p in rng f holds L_Cut(f,p) is_sequence_on M proof let M be Go-board; let f be S-Sequence_in_R2; assume A1: f is_sequence_on M; let p be Point of TOP-REAL 2; assume p in rng f; then L_Cut(f,p) = mid(f,p..f,len f) by Th37; hence L_Cut(f,p) is_sequence_on M by A1,JORDAN1H:33; end; theorem Th40: for G be Go-board for f be FinSequence of TOP-REAL 2 st f is_sequence_on G for i,j be Nat st 1 <= i & i <= len G & 1 <= j & j <= width G holds G*(i,j) in L~f implies G*(i,j) in rng f proof let G be Go-board; let f be FinSequence of TOP-REAL 2; assume A1: f is_sequence_on G; let i,j be Nat; assume A2: 1 <= i & i <= len G & 1 <= j & j <= width G; assume G*(i,j) in L~f; then consider k be Nat such that A3: 1 <= k and A4: k+1 <= len f and A5: G*(i,j) in LSeg(f/.k,f/.(k+1)) by SPPOL_2:14; consider i1,j1,i2,j2 be Nat such that A6: [i1,j1] in Indices G and A7: f/.k = G*(i1,j1) and A8: [i2,j2] in Indices G and A9: f/.(k+1) = G*(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 A1,A3,A4,JORDAN8:6; A11: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A6,GOBOARD5:1; A12: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A8,GOBOARD5:1; k+1 >= 1 & k < len f by A4,NAT_1:29,38; then A13: k in dom f & k+1 in dom f by A3,A4,FINSEQ_3:27; per cases by A10; suppose A14: i1 = i2 & j1+1 = j2; j1 <= j1+1 by NAT_1:29; then G*(i1,j1)`1 <= G*(i1,j1+1)`1 & G*(i1,j1)`2 <= G*(i1,j1+1)`2 by A11,A12,A14,JORDAN1A:39,40; then G*(i1,j1)`1 <= G*(i,j)`1 & G*(i,j)`1 <= G*(i1,j1+1)`1 & G*(i1,j1)`2 <= G*(i,j)`2 & G*(i,j)`2 <= G*(i1,j1+1)`2 by A5,A7,A9,A14,TOPREAL1:9,10; then i1 <= i & i <= i1 & j1 <= j & j <= j1+1 by A2,A11,A12,A14,Th1,Th2; then i = i1 & (j = j1 or j = j1+1) by AXIOMS:21,NAT_1:27; hence G*(i,j) in rng f by A7,A9,A13,A14,PARTFUN2:4; suppose A15: i1+1 = i2 & j1 = j2; i1 <= i1+1 by NAT_1:29; then G*(i1,j1)`1 <= G*(i1+1,j1)`1 & G*(i1,j1)`2 <= G*(i1+1,j1)`2 by A11,A12,A15,JORDAN1A:39,40; then G*(i1,j1)`1 <= G*(i,j)`1 & G*(i,j)`1 <= G*(i1+1,j1)`1 & G*(i1,j1)`2 <= G*(i,j)`2 & G*(i,j)`2 <= G*(i1+1,j1)`2 by A5,A7,A9,A15,TOPREAL1:9,10; then j1 <= j & j <= j1 & i1 <= i & i <= i1+1 by A2,A11,A12,A15,Th1,Th2; then j = j1 & (i = i1 or i = i1+1) by AXIOMS:21,NAT_1:27; hence G*(i,j) in rng f by A7,A9,A13,A15,PARTFUN2:4; suppose A16: i1 = i2+1 & j1 = j2; i2 <= i2+1 by NAT_1:29; then G*(i2,j1)`1 <= G*(i2+1,j1)`1 & G*(i2,j1)`2 <= G*(i2+1,j1)`2 by A11,A12,A16,JORDAN1A:39,40; then G*(i2,j1)`1 <= G*(i,j)`1 & G*(i,j)`1 <= G*(i2+1,j1)`1 & G*(i2,j1)`2 <= G*(i,j)`2 & G*(i,j)`2 <= G*(i2+1,j1)`2 by A5,A7,A9,A16,TOPREAL1:9,10; then j1 <= j & j <= j1 & i2 <= i & i <= i2+1 by A2,A11,A12,A16,Th1,Th2; then j = j1 & (i = i2 or i = i2+1) by AXIOMS:21,NAT_1:27; hence G*(i,j) in rng f by A7,A9,A13,A16,PARTFUN2:4; suppose A17: i1 = i2 & j1 = j2+1; j2 <= j2+1 by NAT_1:29; then G*(i1,j2)`1 <= G*(i1,j2+1)`1 & G*(i1,j2)`2 <= G*(i1,j2+1)`2 by A11,A12,A17,JORDAN1A:39,40; then G*(i1,j2)`1 <= G*(i,j)`1 & G*(i,j)`1 <= G*(i1,j2+1)`1 & G*(i1,j2)`2 <= G*(i,j)`2 & G*(i,j)`2 <= G*(i1,j2+1)`2 by A5,A7,A9,A17,TOPREAL1:9,10; then i1 <= i & i <= i1 & j2 <= j & j <= j2+1 by A2,A11,A12,A17,Th1,Th2; then i = i1 & (j = j2 or j = j2+1) by AXIOMS:21,NAT_1:27; hence G*(i,j) in rng f by A7,A9,A13,A17,PARTFUN2:4; end; theorem for f be S-Sequence_in_R2 for g be FinSequence of TOP-REAL 2 holds g is unfolded s.n.c. one-to-one & L~f /\ L~g = {f/.1} & f/.1 = g/.len g & (for i be Nat st 1<=i & i+2 <= len f holds LSeg(f,i) /\ LSeg(f/.len f,g/.1) = {}) & (for i be Nat st 2<=i & i+1 <= len g holds LSeg(g,i) /\ LSeg(f/.len f,g/.1) = {}) implies f^g is s.c.c. proof let f be S-Sequence_in_R2; let g be FinSequence of TOP-REAL 2; assume that A1: g is unfolded s.n.c. one-to-one and A2: L~f /\ L~g = {f/.1} and A3: f/.1 = g/.len g and A4: for i be Nat st 1<=i & i+2<=len f holds LSeg(f,i) /\ LSeg(f/.len f,g/.1) = {} and A5: for i be Nat st 2<=i & i+1 <= len g holds LSeg(g,i) /\ LSeg(f/.len f,g/.1) = {}; A6: now let i be Nat; assume 1 <= i & i+2 <= len f; then LSeg(f,i) /\ LSeg(f/.len f,g/.1) = {} by A4; hence LSeg(f,i) misses LSeg(f/.len f,g/.1) by XBOOLE_0:def 7; end; A7: now let i be Nat; assume 2 <= i & i+1 <= len g; then LSeg(g,i) /\ LSeg(f/.len f,g/.1) = {} by A5; hence LSeg(g,i) misses LSeg(f/.len f,g/.1) by XBOOLE_0:def 7; end; let i,j be Nat such that A8: i+1 < j and A9: i > 1 & j < len (f^g) or j+1 < len (f^g); A10: j+1 <= len (f^g) by A9,NAT_1:38; per cases; suppose i = 0; then LSeg(f^g,i) = {} by TOPREAL1:def 5; then LSeg(f^g,i) /\ LSeg(f^g,j) = {}; hence thesis by XBOOLE_0:def 7; suppose A11: i <> 0; A12: len(f^g) = len f + len g by FINSEQ_1:35; A13: 1 <= i by A11,RLVECT_1:99; i <= i+1 by NAT_1:29; then A14: i < j by A8,AXIOMS:22; now per cases; suppose A15: j+1 <= len f; j <= j+1 by NAT_1:29; then i < j+1 by A14,AXIOMS:22; then i < len f by A15,AXIOMS:22; then i+1 <= len f by NAT_1:38; then A16: LSeg(f^g,i) = LSeg(f,i) by SPPOL_2:6; LSeg(f^g,j) = LSeg(f,j) by A15,SPPOL_2:6; hence thesis by A8,A16,TOPREAL1:def 9; suppose j+1 > len f; then A17: len f <= j by NAT_1:38; then reconsider j' = j - len f as Nat by INT_1:18; A18: len f + j' = j by XCMPLX_1:27; j+1-len f <= len g by A10,A12,REAL_1:86; then A19: j'+1 <= len g by XCMPLX_1:29; now per cases; suppose A20: i <= len f; now per cases; suppose A21: i = len f; then len f +1+1 <= j by A8,NAT_1:38; then len f +(1+1) <= j by XCMPLX_1:1; then A22: 1+1 <= j' by REAL_1:84; then A23: 1 <= j' by AXIOMS:22; then A24: LSeg(f^g,j) = LSeg(g,j') by A18,SPPOL_2:7; g is non empty by A19,A23,GOBOARD2:3,RELAT_1:60; then LSeg(f^g,i) = LSeg(f/.len f,g/.1) by A21,SPPOL_2:8; hence thesis by A7,A19,A22,A24; suppose i <> len f; then i < len f by A20,REAL_1:def 5; then i+1 <= len f by NAT_1:38; then A25: LSeg(f^g,i) = LSeg(f,i) by SPPOL_2:6; now per cases; suppose A26: j = len f; then i+1+1 <= len f by A8,NAT_1:38; then A27: i+(1+1) <= len f by XCMPLX_1:1; 1 <= len g by A10,A12,A26,REAL_1:53; then g is non empty by FINSEQ_3:27,RELAT_1:60; then LSeg(f^g,j) = LSeg(f/.len f,g/.1) by A26,SPPOL_2:8; hence thesis by A6,A13,A25,A27; suppose j <> len f; then len f < j by A17,REAL_1:def 5; then len f+1 <= j by NAT_1:38; then A28: 1 <= j' by REAL_1:84; then A29: LSeg(f^g,len f+j') = LSeg(g,j') by SPPOL_2:7; then A30: LSeg(f^g,j) c= L~g by A18,TOPREAL3:26; LSeg(f^g,i) c= L~f by A25,TOPREAL3:26; then A31: LSeg(f^g,i) /\ LSeg(f^g,j) c= {f/.1} by A2,A30,XBOOLE_1: 27; A32: len f >= 2 by TOPREAL1:def 10; now per cases by A31,ZFMISC_1:39; suppose LSeg(f^g,i) /\ LSeg(f^g,j) = {}; hence thesis by XBOOLE_0:def 7; suppose LSeg(f^g,i) /\ LSeg(f^g,j) = {f/.1}; then f/.1 in LSeg(f^g,i) /\ LSeg(f^g,j) by TARSKI:def 1; then A33: f/.1 in LSeg(f^g,i) & f/.1 in LSeg(f^g,j) by XBOOLE_0:def 3; j'+1 >= 1 & j' < len g by A19,NAT_1:29,38; then j' in dom g & j'+1 in dom g by A19,A28,FINSEQ_3:27; then j'+1=len g by A1,A3,A18,A29,A33,GOBOARD2:7; hence thesis by A9,A12,A18,A25,A32,A33,JORDAN5B:33,XCMPLX_1:1; end; hence thesis; end; hence thesis; end; hence thesis; suppose A34: i > len f; then reconsider i' = i - len f as Nat by INT_1:18; A35: len f + i' = i by XCMPLX_1:27; len f + 1 <= i by A34,NAT_1:38; then 1 <= i' by REAL_1:84; then A36: LSeg(f^g,len f+i') = LSeg(g,i') by SPPOL_2:7; i+1-len f < j' by A8,REAL_1:54; then A37: i'+1 < j' by XCMPLX_1:29; j <> len f by A8,A34,NAT_1:38; then len f < j by A17,REAL_1:def 5; then len f+1 <= j by NAT_1:38; then 1 <= j' by REAL_1:84; then LSeg(f^g,len f+j') = LSeg(g,j') by SPPOL_2:7; hence thesis by A1,A18,A35,A36,A37,TOPREAL1:def 9; end; hence thesis; end; hence thesis; end; theorem for C be compact non vertical non horizontal non empty Subset of TOP-REAL 2 ex i be Nat st 1 <= i & i+1 <= len Gauge(C,n) & W-min C in cell(Gauge(C,n),1,i) & W-min C <> Gauge(C,n)*(2,i) proof let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2; set G = Gauge(C,n); A1: len G = width G by JORDAN8:def 1; defpred P[Nat] means 1 <= $1 & $1 < len G & G*(2,$1)`2 < (W-min C)`2; A2: for k be Nat st P[k] holds k <= len G; A3: len G = 2|^n+3 & len G = width G by JORDAN8:def 1; A4: len G >= 4 by JORDAN8:13; then A5: 1 < len G by AXIOMS:22; (SW-corner C)`2 <= (W-min C)`2 by PSCOMP_1:87; then A6: S-bound C <= (W-min C)`2 by PSCOMP_1:73; A7: 2 <= len G by A4,AXIOMS:22; then G*(2,2)`2 = S-bound C by JORDAN8:16; then G*(2,1)`2 < S-bound C by A3,A7,GOBOARD5:5; then G*(2,1)`2 < (W-min C)`2 by A6,AXIOMS:22; then A8: ex k be Nat st P[k] by A5; ex i being Nat st P[i] & for n st P[n] holds n <= i from Max(A2,A8); then consider i being Nat such that A9: 1 <= i & i < len G and A10: G*(2,i)`2 < (W-min C)`2 and A11: for n st P[n] holds n <= i; take i; thus 1 <= i & i+1 <= len G by A9,NAT_1:38; A12: LSeg(G*(1+1,i),G*(1+1,i+1)) c= cell(G,1,i) by A1,A5,A9,GOBOARD5:19; A13: i+1 <= len G by A9,NAT_1:38; A14: 1 <= i+1 by NAT_1:37; (W-min C)`1 = W-bound C by PSCOMP_1:84; then A15: G*(2,i)`1 = (W-min C)`1 & (W-min C)`1 = G*(2,i+1)`1 by A9,A13,A14,JORDAN8:14; now assume i+1 = len G; then len G-'1 = i by BINARITH:39; then A16: G*(2,i)`2 = N-bound C by A7,JORDAN8:17; (NW-corner C)`2 >= (W-min C)`2 by PSCOMP_1:87; hence contradiction by A10,A16,PSCOMP_1:75; end; then i+1 < len G & i < i+1 by A13,NAT_1:38,REAL_1:def 5; then (W-min C)`2 <= G*(2,i+1)`2 by A11,A14; then W-min C in LSeg(G*(2,i),G*(2,i+1)) by A10,A15,GOBOARD7:8; hence W-min C in cell(G,1,i) by A12; thus W-min C <> G*(2,i) by A10; end; theorem Th43: for f be S-Sequence_in_R2 for p be Point of TOP-REAL 2 st p in L~f & f.len f in L~R_Cut(f,p) holds f.len f = p proof let f be S-Sequence_in_R2; let p be Point of TOP-REAL 2; assume that A1: p in L~f and A2: f.len f in L~R_Cut(f,p); A3: L~f = L~(Rev f) by SPPOL_2:22; A4: (Rev f).1 = f.len f by FINSEQ_5:65; A5: Rev f is_S-Seq by SPPOL_2:47; L_Cut(Rev f,p) = Rev R_Cut(f,p) by A1,JORDAN3:57; then (Rev f).1 in L~L_Cut(Rev f,p) by A2,A4,SPPOL_2:22; hence f.len f = p by A1,A3,A4,A5,JORDAN1E:11; end; theorem Th44: for f be non empty FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 holds R_Cut (f,p) <> {} proof let f be non empty FinSequence of TOP-REAL 2; let p be Point of TOP-REAL 2; per cases; suppose p<>f.1; then R_Cut (f,p) = mid(f,1,Index(p,f))^<*p*> by JORDAN3:def 5; hence thesis; suppose p=f.1; then R_Cut (f,p) = <*p*> by JORDAN3:def 5; hence thesis; end; theorem Th45: for f be S-Sequence_in_R2 for p be Point of TOP-REAL 2 st p in L~f holds R_Cut(f,p)/.(len R_Cut(f,p)) = p proof let f be S-Sequence_in_R2; let p be Point of TOP-REAL 2; assume A1: p in L~f; R_Cut(f,p) is non empty by Th44; then len R_Cut(f,p) in dom R_Cut(f,p) by FINSEQ_5:6; hence R_Cut(f,p)/.len R_Cut(f,p) = R_Cut(f,p).len R_Cut(f,p) by FINSEQ_4:def 4 .= p by A1,JORDAN3:59; end; theorem Th46: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for p be Point of TOP-REAL 2 holds p in L~Upper_Seq(C,n) & p`1 = E-bound L~Cage(C,n) implies p = E-max L~Cage(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let p be Point of TOP-REAL 2; set Ca = Cage(C,n); set US = Upper_Seq(C,n); set LS = Lower_Seq(C,n); set Wmin = W-min L~Ca; set Smax = S-max L~Ca; set Smin = S-min L~Ca; set Emin = E-min L~Ca; set Emax = E-max L~Ca; set Wbo = W-bound 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 NE = NE-corner L~Ca; assume that A1: p in L~Upper_Seq(C,n) and A2: p`1 = E-bound L~Cage(C,n) and A3: p <> E-max L~Cage(C,n); A4: 1 in dom US & 1 in dom LS by FINSEQ_5:6; US/.1 = Wmin by JORDAN1F:5; then A5: US.1 = Wmin by A4,FINSEQ_4:def 4; LS/.1 = Emax by JORDAN1F:6; then A6: LS.1 = Emax by A4,FINSEQ_4:def 4; Wbo <> Ebo by SPRECT_1:33; then p <> US.1 by A2,A5,PSCOMP_1:84; then reconsider g = R_Cut(US,p) as being_S-Seq FinSequence of TOP-REAL 2 by A1,JORDAN3:70; A7: US is_in_the_area_of Ca by JORDAN1E:21; then <*p*> is_in_the_area_of Ca by A1,SPRECT_3:63; then A8: g is_in_the_area_of Ca by A1,A7,SPRECT_3:69; A9: (g/.1)`1 = (US/.1)`1 by A1,SPRECT_3:39 .= Wmin`1 by JORDAN1F:5 .= Wbo by PSCOMP_1:84; len g in dom g by FINSEQ_5:6; then g/.len g = g.len g by FINSEQ_4:def 4 .= p by A1,JORDAN3:59; then A10: g is_a_h.c._for Ca by A2,A8,A9,SPRECT_2:def 2; len Cage(C,n) > 4 by GOBOARD7:36; then len Cage(C,n) >= 2 by AXIOMS:22; then A11: rng Cage(C,n) c= L~Cage(C,n) by SPPOL_2:18; now per cases; suppose A12: Emax <> NE; set h = Rev R_Cut(LS,Smax)^<*NE*>; A13: not NE in rng Cage(C,n) proof assume A14: NE in rng Cage(C,n); A15: 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 { p1 where p1 is Point of TOP-REAL 2 : p1`1 = E-bound L~Cage(C,n) & p1`2 <= N-bound L~Cage(C,n) & p1`2 >= S-bound L~Cage(C,n) } by A15; 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 A11,A14,XBOOLE_0:def 3; then NE in E-most L~Cage(C,n) by PSCOMP_1:def 40; then A16: 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 A17: (E-max L~Cage(C,n))`2 = NE`2 by A16,AXIOMS:21; (E-max L~Cage(C,n))`1 = NE`1 by PSCOMP_1:105; hence contradiction by A12,A17,TOPREAL3:11; end; Smax in rng LS by Th12; then R_Cut(LS,Smax) = mid(LS,1,Smax..LS) by JORDAN1G:57; then A18: rng R_Cut(LS,Smax) c= rng LS by JORDAN3:28; rng LS c= rng Ca by JORDAN1G:47; then rng R_Cut(LS,Smax) c= rng Ca by A18,XBOOLE_1:1; then not NE in rng R_Cut(LS,Smax) by A13; then rng R_Cut(LS,Smax) misses {NE} by ZFMISC_1:56; then rng R_Cut(LS,Smax) misses rng <*NE*> by FINSEQ_1:55; then A19: rng Rev R_Cut(LS,Smax) misses rng <*NE*> by FINSEQ_5:60; A20: Smax in L~LS by Th12; A21: Emin`2 < Emax`2 by SPRECT_2:57; Emin in L~Ca by SPRECT_1:16; then Sbo <= Emin`2 by PSCOMP_1:71; then A22: Smax <> LS.1 by A6,A21,PSCOMP_1:114; then reconsider RCutLS = R_Cut(LS,Smax) as being_S-Seq FinSequence of TOP-REAL 2 by A20,JORDAN3:70; A23: <*NE*> is one-to-one by FINSEQ_3:102; A24: Rev RCutLS is special by SPPOL_2:42; A25: <*NE*> is special by SPPOL_2:39; A26: Rev RCutLS/.len Rev RCutLS = Rev RCutLS/.len RCutLS by FINSEQ_5:def 3 .= RCutLS/.1 by FINSEQ_5:68 .= LS/.1 by A20,SPRECT_3:39 .= Emax by JORDAN1F:6; then (Rev RCutLS/.len Rev RCutLS)`1 = E-bound L~Ca by PSCOMP_1:104 .= NE`1 by PSCOMP_1:76 .= (<*NE*>/.1)`1 by FINSEQ_4:25; then A27: h is one-to-one special by A19,A23,A24,A25,FINSEQ_3:98,GOBOARD2 :13; A28: 2 <= len g by TOPREAL1:def 10; A29: len h = len Rev R_Cut(LS,Smax) + 1 by FINSEQ_2:19 .= len R_Cut(LS,Smax) + 1 by FINSEQ_5:def 3 .= Index(Smax,LS)+1+1 by A20,A22,JORDAN3:60; Index(Smax,LS) >= 0 by NAT_1:18; then Index(Smax,LS)+1 >= 0+1 by REAL_1:55; then A30: len h >= 1+1 by A29,REAL_1:55; A31: LS is_in_the_area_of Ca by JORDAN1E:22; then <*Smax*> is_in_the_area_of Ca by A20,SPRECT_3:63; then R_Cut(LS,Smax) is_in_the_area_of Ca by A20,A31,SPRECT_3:69; then A32: Rev R_Cut(LS,Smax) is_in_the_area_of Ca by SPRECT_3:68; <*NE*> is_in_the_area_of Ca by SPRECT_2:29; then A33: h is_in_the_area_of Ca by A32,SPRECT_2:28; 1 in dom Rev RCutLS by FINSEQ_5:6; then h/.1 = Rev RCutLS/.1 by GROUP_5:95 .= R_Cut(LS,Smax)/.len R_Cut(LS,Smax) by FINSEQ_5:68 .= Smax by A20,Th45; then A34: (h/.1)`2 = Sbo by PSCOMP_1:114; (h/.len h)`2 = (h/.(len Rev R_Cut(LS,Smax)+1))`2 by FINSEQ_2:19 .= NE`2 by TOPREAL4:1 .= Nbo by PSCOMP_1:77; then h is_a_v.c._for Ca by A33,A34,SPRECT_2:def 3; then L~g meets L~h by A10,A27,A28,A30,SPRECT_2:33; then consider x be set such that A35: x in L~g and A36: x in L~h by XBOOLE_0:3; reconsider x as Point of TOP-REAL 2 by A35; A37: L~g c= L~US by A1,JORDAN3:76; then A38: x in L~US by A35; A39: L~h = L~Rev RCutLS \/ LSeg(Rev RCutLS/.len Rev RCutLS,NE) by SPPOL_2:19; A40: L~RCutLS c= L~LS by A20,JORDAN3:76; A41: len US in dom US & len LS in dom LS by FINSEQ_5:6; now per cases by A36,A39,XBOOLE_0:def 2; suppose x in L~Rev RCutLS; then A42: x in L~RCutLS by SPPOL_2:22; then x in L~US /\ L~LS by A35,A37,A40,XBOOLE_0:def 3; then A43: x in {Wmin,Emax} by JORDAN1E:20; now per cases by A43,TARSKI:def 2; suppose x = Wmin; then LS/.len LS in L~R_Cut(LS,Smax) by A42,JORDAN1F:8; then LS.len LS in L~R_Cut(LS,Smax) by A41,FINSEQ_4:def 4; then LS.len LS = Smax by A20,Th43; then LS/.len LS = Smax by A41,FINSEQ_4:def 4; then A44: Wmin = Smax by JORDAN1F:8; A45: Smin`1 < Smax`1 by SPRECT_2:59; Smin in L~Ca by SPRECT_1:14; then Wbo <= Smin`1 by PSCOMP_1:71; hence contradiction by A44,A45,PSCOMP_1:84; suppose x = Emax; then US/.len US in L~R_Cut(US,p) by A35,JORDAN1F:7; then US.len US in L~R_Cut(US,p) by A41,FINSEQ_4:def 4; then US.len US = p by A1,Th43; then US/.len US = p by A41,FINSEQ_4:def 4; hence contradiction by A3,JORDAN1F:7; end; hence contradiction; suppose A46: x in LSeg(Rev RCutLS/.len Rev RCutLS,NE); A47: Emax`1 = Ebo by PSCOMP_1:104; NE`1 = Ebo by PSCOMP_1:76; then A48: x`1 = Ebo by A26,A46,A47,GOBOARD7:5; Emax`2 <= NE`2 by PSCOMP_1:107; then A49: Emax`2 <= x`2 by A26,A46,TOPREAL1:10; L~Ca = L~US \/ L~LS by JORDAN1E:17; then L~US c= L~Ca by XBOOLE_1:7; then x in E-most L~Ca by A38,A48,SPRECT_2:17; then x`2 <= Emax`2 by PSCOMP_1:108; then x`2 = Emax`2 by A49,AXIOMS:21; then x = Emax by A47,A48,TOPREAL3:11; then US/.len US in L~R_Cut(US,p) by A35,JORDAN1F:7; then US.len US in L~R_Cut(US,p) by A41,FINSEQ_4:def 4; then US.len US = p by A1,Th43; then US/.len US = p by A41,FINSEQ_4:def 4; hence contradiction by A3,JORDAN1F:7; end; hence contradiction; suppose A50: Emax = NE; set h = Rev R_Cut(LS,Smax); A51: Smax in L~LS by Th12; A52: Emin`2 < Emax`2 by SPRECT_2:57; Emin in L~Ca by SPRECT_1:16; then Sbo <= Emin`2 by PSCOMP_1:71; then Smax <> LS.1 by A6,A52,PSCOMP_1:114; then reconsider RCutLS = R_Cut(LS,Smax) as being_S-Seq FinSequence of TOP-REAL 2 by A51,JORDAN3:70; A53: Rev RCutLS is special by SPPOL_2:42; A54: Rev RCutLS/.len Rev RCutLS = Rev RCutLS/.len RCutLS by FINSEQ_5:def 3 .= RCutLS/.1 by FINSEQ_5:68 .= LS/.1 by A51,SPRECT_3:39 .= Emax by JORDAN1F:6; A55: 2 <= len g by TOPREAL1:def 10; len RCutLS >= 2 by TOPREAL1:def 10; then A56: len h >= 2 by FINSEQ_5:def 3; A57: LS is_in_the_area_of Ca by JORDAN1E:22; then <*Smax*> is_in_the_area_of Ca by A51,SPRECT_3:63; then R_Cut(LS,Smax) is_in_the_area_of Ca by A51,A57,SPRECT_3:69; then A58: h is_in_the_area_of Ca by SPRECT_3:68; 1 in dom Rev RCutLS by FINSEQ_5:6; then h/.1 = R_Cut(LS,Smax)/.len R_Cut(LS,Smax) by FINSEQ_5:68 .= Smax by A51,Th45; then A59: (h/.1)`2 = Sbo by PSCOMP_1:114; (h/.len h)`2 = Nbo by A50,A54,PSCOMP_1:77; then h is_a_v.c._for Ca by A58,A59,SPRECT_2:def 3; then L~g meets L~h by A10,A53,A55,A56,SPRECT_2:33; then consider x be set such that A60: x in L~g and A61: x in L~h by XBOOLE_0:3; reconsider x as Point of TOP-REAL 2 by A60; A62: L~g c= L~US by A1,JORDAN3:76; A63: L~RCutLS c= L~LS by A51,JORDAN3:76; A64: len US in dom US & len LS in dom LS by FINSEQ_5:6; A65: x in L~RCutLS by A61,SPPOL_2:22; then x in L~US /\ L~LS by A60,A62,A63,XBOOLE_0:def 3; then A66: x in {Wmin,Emax} by JORDAN1E:20; now per cases by A66,TARSKI:def 2; suppose x = Wmin; then LS/.len LS in L~R_Cut(LS,Smax) by A65,JORDAN1F:8; then LS.len LS in L~R_Cut(LS,Smax) by A64,FINSEQ_4:def 4; then LS.len LS = Smax by A51,Th43; then LS/.len LS = Smax by A64,FINSEQ_4:def 4; then A67: Wmin = Smax by JORDAN1F:8; A68: Smin`1 < Smax`1 by SPRECT_2:59; Smin in L~Ca by SPRECT_1:14; then Wbo <= Smin`1 by PSCOMP_1:71; hence contradiction by A67,A68,PSCOMP_1:84; suppose x = Emax; then US/.len US in L~R_Cut(US,p) by A60,JORDAN1F:7; then US.len US in L~R_Cut(US,p) by A64,FINSEQ_4:def 4; then US.len US = p by A1,Th43; then US/.len US = p by A64,FINSEQ_4:def 4; hence contradiction by A3,JORDAN1F:7; end; hence contradiction; end; hence contradiction; end; theorem for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for p be Point of TOP-REAL 2 holds p in L~Lower_Seq(C,n) & p`1 = W-bound L~Cage(C,n) implies p = W-min L~Cage(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let p be Point of TOP-REAL 2; set Ca = Cage(C,n); set LS = Lower_Seq(C,n); set US = Upper_Seq(C,n); set Emax = E-max L~Ca; set Nmin = N-min L~Ca; set Nmax = N-max L~Ca; set Wmax = W-max L~Ca; set Wmin = W-min L~Ca; 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 Nbo = N-bound L~Cage(C,n); set SW = SW-corner L~Ca; assume that A1: p in L~Lower_Seq(C,n) and A2: p`1 = W-bound L~Cage(C,n) and A3: p <> W-min L~Cage(C,n); A4: 1 in dom LS & 1 in dom US by FINSEQ_5:6; LS/.1 = Emax by JORDAN1F:6; then A5: LS.1 = Emax by A4,FINSEQ_4:def 4; US/.1 = Wmin by JORDAN1F:5; then A6: US.1 = Wmin by A4,FINSEQ_4:def 4; Ebo <> Wbo by SPRECT_1:33; then p <> LS.1 by A2,A5,PSCOMP_1:104; then reconsider g1 = R_Cut(LS,p) as being_S-Seq FinSequence of TOP-REAL 2 by A1,JORDAN3:70; reconsider g = Rev g1 as being_S-Seq FinSequence of TOP-REAL 2 by SPPOL_2:47; A7: L~g = L~g1 by SPPOL_2:22; A8: LS is_in_the_area_of Ca by JORDAN1E:22; then <*p*> is_in_the_area_of Ca by A1,SPRECT_3:63; then g1 is_in_the_area_of Ca by A1,A8,SPRECT_3:69; then A9: g is_in_the_area_of Ca by SPRECT_3:68; A10: g/.1 = g1/.len g1 by FINSEQ_5:68; A11: g/.len g = g/.len g1 by FINSEQ_5:def 3 .= g1/.1 by FINSEQ_5:68; A12: (g1/.1)`1 = (LS/.1)`1 by A1,SPRECT_3:39 .= Emax`1 by JORDAN1F:6 .= Ebo by PSCOMP_1:104; len g1 in dom g1 by FINSEQ_5:6; then g1/.len g1 = g1.len g1 by FINSEQ_4:def 4 .= p by A1,JORDAN3:59; then A13: g is_a_h.c._for Ca by A2,A9,A10,A11,A12,SPRECT_2:def 2; len Cage(C,n) > 4 by GOBOARD7:36; then len Cage(C,n) >= 2 by AXIOMS:22; then A14: rng Cage(C,n) c= L~Cage(C,n) by SPPOL_2:18; now per cases; suppose A15: Wmin <> SW; set h1 = Rev R_Cut(US,Nmin)^<*SW*>; A16: not SW in rng Cage(C,n) proof assume A17: SW in rng Cage(C,n); A18: SW`1 = W-bound L~Cage(C,n) & SW`2 = S-bound L~Cage(C,n) by PSCOMP_1:72,73; then SW`2 <= N-bound L~Cage(C,n) by SPRECT_1:24; then SW in { p1 where p1 is Point of TOP-REAL 2 : p1`1 = W-bound L~Cage(C,n) & p1`2 <= N-bound L~Cage(C,n) & p1`2 >= S-bound L~Cage(C,n) } by A18; then SW in LSeg(SW-corner L~Cage(C,n), NW-corner L~Cage(C,n)) by SPRECT_1:28; then SW in LSeg(SW-corner L~Cage(C,n), NW-corner L~Cage(C,n)) /\ L~Cage(C,n) by A14,A17,XBOOLE_0:def 3; then SW in W-most L~Cage(C,n) by PSCOMP_1:def 38; then A19: SW`2 >= (W-min L~Cage(C,n))`2 by PSCOMP_1:88; (W-min L~Cage(C,n))`2 >= SW`2 by PSCOMP_1:87; then A20: (W-min L~Cage(C,n))`2 = SW`2 by A19,AXIOMS:21; (W-min L~Cage(C,n))`1 = SW`1 by PSCOMP_1:85; hence contradiction by A15,A20,TOPREAL3:11; end; Nmin in rng US by Th7; then R_Cut(US,Nmin) = mid(US,1,Nmin..US) by JORDAN1G:57; then A21: rng R_Cut(US,Nmin) c= rng US by JORDAN3:28; rng US c= rng Ca by JORDAN1G:47; then rng R_Cut(US,Nmin) c= rng Ca by A21,XBOOLE_1:1; then not SW in rng R_Cut(US,Nmin) by A16; then rng R_Cut(US,Nmin) misses {SW} by ZFMISC_1:56; then rng R_Cut(US,Nmin) misses rng <*SW*> by FINSEQ_1:55; then A22: rng Rev R_Cut(US,Nmin) misses rng <*SW*> by FINSEQ_5:60; A23: Nmin in L~US by Th7; A24: Wmax`2 > Wmin`2 by SPRECT_2:61; Wmax in L~Ca by SPRECT_1:15; then Nbo >= Wmax`2 by PSCOMP_1:71; then A25: Nmin <> US.1 by A6,A24,PSCOMP_1:94; then reconsider RCutUS = R_Cut(US,Nmin) as being_S-Seq FinSequence of TOP-REAL 2 by A23,JORDAN3:70; A26: <*SW*> is one-to-one by FINSEQ_3:102; A27: Rev RCutUS is special by SPPOL_2:42; A28: <*SW*> is special by SPPOL_2:39; A29: Rev RCutUS/.len Rev RCutUS = Rev RCutUS/.len RCutUS by FINSEQ_5:def 3 .= RCutUS/.1 by FINSEQ_5:68 .= US/.1 by A23,SPRECT_3:39 .= Wmin by JORDAN1F:5; then (Rev RCutUS/.len Rev RCutUS)`1 = W-bound L~Ca by PSCOMP_1:84 .= SW`1 by PSCOMP_1:72 .= (<*SW*>/.1)`1 by FINSEQ_4:25; then reconsider h1 as one-to-one special FinSequence of TOP-REAL 2 by A22,A26,A27,A28,FINSEQ_3: 98,GOBOARD2:13; set h = Rev h1; A30: h is special by SPPOL_2:42; A31: 2 <= len g by TOPREAL1:def 10; A32: len h1 = len Rev R_Cut(US,Nmin) + 1 by FINSEQ_2:19 .= len R_Cut(US,Nmin) + 1 by FINSEQ_5:def 3 .= Index(Nmin,US)+1+1 by A23,A25,JORDAN3:60; Index(Nmin,US) >= 0 by NAT_1:18; then Index(Nmin,US)+1 >= 0+1 by REAL_1:55; then len h1 >= 1+1 by A32,REAL_1:55; then A33: len h >= 2 by FINSEQ_5:def 3; A34: US is_in_the_area_of Ca by JORDAN1E:21; then <*Nmin*> is_in_the_area_of Ca by A23,SPRECT_3:63; then R_Cut(US,Nmin) is_in_the_area_of Ca by A23,A34,SPRECT_3:69; then A35: Rev R_Cut(US,Nmin) is_in_the_area_of Ca by SPRECT_3:68; <*SW*> is_in_the_area_of Ca by SPRECT_2:32; then h1 is_in_the_area_of Ca by A35,SPRECT_2:28; then A36: h is_in_the_area_of Ca by SPRECT_3:68; 1 in dom Rev RCutUS by FINSEQ_5:6; then h1/.1 = Rev RCutUS/.1 by GROUP_5:95 .= R_Cut(US,Nmin)/.len R_Cut(US,Nmin) by FINSEQ_5:68 .= Nmin by A23,Th45; then A37: (h1/.1)`2 = Nbo by PSCOMP_1:94; A38: h/.len h = h/.len h1 by FINSEQ_5:def 3 .= h1/.1 by FINSEQ_5:68; A39: h/.1 = h1/.len h1 by FINSEQ_5:68; (h1/.len h1)`2 = (h1/.(len Rev R_Cut(US,Nmin)+1))`2 by FINSEQ_2:19 .= SW`2 by TOPREAL4:1 .= Sbo by PSCOMP_1:73; then h is_a_v.c._for Ca by A36,A37,A38,A39,SPRECT_2:def 3; then L~g meets L~h by A13,A30,A31,A33,SPRECT_2:33; then consider x be set such that A40: x in L~g and A41: x in L~h by XBOOLE_0:3; reconsider x as Point of TOP-REAL 2 by A40; A42: L~g c= L~LS by A1,A7,JORDAN3:76; then A43: x in L~LS by A40; L~h = L~h1 by SPPOL_2:22; then A44: L~h = L~Rev RCutUS \/ LSeg(Rev RCutUS/.len Rev RCutUS,SW) by SPPOL_2:19; A45: L~RCutUS c= L~US by A23,JORDAN3:76; A46: len LS in dom LS & len US in dom US by FINSEQ_5:6; now per cases by A41,A44,XBOOLE_0:def 2; suppose x in L~Rev RCutUS; then A47: x in L~RCutUS by SPPOL_2:22; then x in L~LS /\ L~US by A40,A42,A45,XBOOLE_0:def 3; then A48: x in {Emax,Wmin} by JORDAN1E:20; now per cases by A48,TARSKI:def 2; suppose x = Emax; then US/.len US in L~R_Cut(US,Nmin) by A47,JORDAN1F:7; then US.len US in L~R_Cut(US,Nmin) by A46,FINSEQ_4:def 4; then US.len US = Nmin by A23,Th43; then US/.len US = Nmin by A46,FINSEQ_4:def 4; then A49: Emax = Nmin by JORDAN1F:7; A50: Nmax`1 > Nmin`1 by SPRECT_2:55; Nmax in L~Ca by SPRECT_1:13; then Ebo >= Nmax`1 by PSCOMP_1:71; hence contradiction by A49,A50,PSCOMP_1:104; suppose x = Wmin; then LS/.len LS in L~R_Cut(LS,p) by A7,A40,JORDAN1F:8; then LS.len LS in L~R_Cut(LS,p) by A46,FINSEQ_4:def 4; then LS.len LS = p by A1,Th43; then LS/.len LS = p by A46,FINSEQ_4:def 4; hence contradiction by A3,JORDAN1F:8; end; hence contradiction; suppose A51: x in LSeg(Rev RCutUS/.len Rev RCutUS,SW); A52: Wmin`1 = Wbo by PSCOMP_1:84; SW`1 = Wbo by PSCOMP_1:72; then A53: x`1 = Wbo by A29,A51,A52,GOBOARD7:5; Wmin`2 >= SW`2 by PSCOMP_1:87; then A54: Wmin`2 >= x`2 by A29,A51,TOPREAL1:10; L~Ca = L~LS \/ L~US by JORDAN1E:17; then L~LS c= L~Ca by XBOOLE_1:7; then x in W-most L~Ca by A43,A53,SPRECT_2:16; then x`2 >= Wmin`2 by PSCOMP_1:88; then x`2 = Wmin`2 by A54,AXIOMS:21; then x = Wmin by A52,A53,TOPREAL3:11; then LS/.len LS in L~R_Cut(LS,p) by A7,A40,JORDAN1F:8; then LS.len LS in L~R_Cut(LS,p) by A46,FINSEQ_4:def 4; then LS.len LS = p by A1,Th43; then LS/.len LS = p by A46,FINSEQ_4:def 4; hence contradiction by A3,JORDAN1F:8; end; hence contradiction; suppose A55: Wmin = SW; set h = R_Cut(US,Nmin); A56: Nmin in L~US by Th7; A57: Wmax`2 > Wmin`2 by SPRECT_2:61; Wmax in L~Ca by SPRECT_1:15; then Nbo >= Wmax`2 by PSCOMP_1:71; then Nmin <> US.1 by A6,A57,PSCOMP_1:94; then reconsider RCutUS = R_Cut(US,Nmin) as being_S-Seq FinSequence of TOP-REAL 2 by A56,JORDAN3:70; A58: RCutUS/.1 = US/.1 by A56,SPRECT_3:39 .= Wmin by JORDAN1F:5; A59: 2 <= len g by TOPREAL1:def 10; A60: len RCutUS >= 2 by TOPREAL1:def 10; A61: US is_in_the_area_of Ca by JORDAN1E:21; then <*Nmin*> is_in_the_area_of Ca by A56,SPRECT_3:63; then A62: R_Cut(US,Nmin) is_in_the_area_of Ca by A56,A61,SPRECT_3:69; R_Cut(US,Nmin)/.len R_Cut(US,Nmin) = Nmin by A56,Th45; then A63: (h/.len h)`2 = Nbo by PSCOMP_1:94; (h/.1)`2 = Sbo by A55,A58,PSCOMP_1:73; then h is_a_v.c._for Ca by A62,A63,SPRECT_2:def 3; then L~g meets L~h by A13,A59,A60,SPRECT_2:33; then consider x be set such that A64: x in L~g and A65: x in L~h by XBOOLE_0:3; reconsider x as Point of TOP-REAL 2 by A64; A66: L~g c= L~LS by A1,A7,JORDAN3:76; A67: L~RCutUS c= L~US by A56,JORDAN3:76; A68: len LS in dom LS & len US in dom US by FINSEQ_5:6; x in L~LS /\ L~US by A64,A65,A66,A67,XBOOLE_0:def 3; then A69: x in {Emax,Wmin} by JORDAN1E:20; now per cases by A69,TARSKI:def 2; suppose x = Emax; then US/.len US in L~R_Cut(US,Nmin) by A65,JORDAN1F:7; then US.len US in L~R_Cut(US,Nmin) by A68,FINSEQ_4:def 4; then US.len US = Nmin by A56,Th43; then US/.len US = Nmin by A68,FINSEQ_4:def 4; then A70: Emax = Nmin by JORDAN1F:7; A71: Nmax`1 > Nmin`1 by SPRECT_2:55; Nmax in L~Ca by SPRECT_1:13; then Ebo >= Nmax`1 by PSCOMP_1:71; hence contradiction by A70,A71,PSCOMP_1:104; suppose x = Wmin; then LS/.len LS in L~R_Cut(LS,p) by A7,A64,JORDAN1F:8; then LS.len LS in L~R_Cut(LS,p) by A68,FINSEQ_4:def 4; then LS.len LS = p by A1,Th43; then LS/.len LS = p by A68,FINSEQ_4:def 4; hence contradiction by A3,JORDAN1F:8; end; hence contradiction; end; hence contradiction; end; theorem for G be Go-board for f,g be FinSequence of TOP-REAL 2 for k be Nat holds 1 <= k & k < len f & f^g is_sequence_on G implies left_cell(f^g,k,G) = left_cell(f,k,G) & right_cell(f^g,k,G) = right_cell(f,k,G) proof let G be Go-board; let f,g be FinSequence of TOP-REAL 2; let k be Nat; assume that A1: 1 <= k and A2: k < len f and A3: f^g is_sequence_on G; A4: (f^g)|len f = f by FINSEQ_5:26; A5: k+1 <= len f by A2,NAT_1:38; len f <= len f + len g by NAT_1:29; then len f <= len (f^g) by FINSEQ_1:35; then k+1 <= len (f^g) by A5,AXIOMS:22; hence thesis by A1,A3,A4,A5,GOBRD13:32; end; theorem Th49: for D be set for f,g be FinSequence of D for i be Nat st i <= len f holds (f^'g)|i = f|i proof let D be set; let f,g be FinSequence of D; let i be Nat; assume A1: i <= len f; then A2: len(f|i) = i by TOPREAL1:3; per cases; suppose A3: g <> {}; then len g <> 0 by FINSEQ_1:25; then len g > 0 by NAT_1:19; then len g >= 0+1 by NAT_1:38; then i+1 <= len f+len g by A1,REAL_1:55; then i+1 <= len(f^'g)+1 by A3,GRAPH_2:13; then i <= len(f^'g) by REAL_1:53; then A4: len((f^'g)|i) = i by TOPREAL1:3; now let j be Nat; assume A5: j in Seg i; then j <= i by FINSEQ_1:3; then A6: 1 <= j & j <= len f by A1,A5,AXIOMS:22,FINSEQ_1:3; thus ((f^'g)|i).j = ((f^'g)|(Seg i)).j by TOPREAL1:def 1 .= (f^'g).j by A5,FUNCT_1:72 .= f.j by A6,GRAPH_2:14 .= (f|(Seg i)).j by A5,FUNCT_1:72 .= (f|i).j by TOPREAL1:def 1; end; hence (f^'g)|i = f|i by A2,A4,FINSEQ_2:10; suppose g = {}; hence thesis by AMISTD_1:7; end; theorem Th50: for D be set for f,g be FinSequence of D holds (f^'g)|(len f) = f proof let D be set; let f,g be FinSequence of D; f|len f = f|(Seg len f) by TOPREAL1:def 1; hence f = f|len f by FINSEQ_2:23 .= (f^'g)|(len f) by Th49; end; theorem Th51: for G be Go-board for f,g be FinSequence of TOP-REAL 2 for k be Nat holds 1 <= k & k < len f & f^'g is_sequence_on G implies left_cell(f^'g,k,G) = left_cell(f,k,G) & right_cell(f^'g,k,G) = right_cell(f,k,G) proof let G be Go-board; let f,g be FinSequence of TOP-REAL 2; let k be Nat; assume that A1: 1 <= k and A2: k < len f and A3: f^'g is_sequence_on G; A4: (f^'g)|len f = f by Th50; A5: k+1 <= len f by A2,NAT_1:38; len f <= len (f^'g) by TOPREAL8:7; then k+1 <= len (f^'g) by A5,AXIOMS:22; hence thesis by A1,A3,A4,A5,GOBRD13:32; end; theorem Th52: for G be Go-board for f be S-Sequence_in_R2 for p be Point of TOP-REAL 2 for k be Nat st 1 <= k & k < p..f & f is_sequence_on G & p in rng f holds left_cell(R_Cut(f,p),k,G) = left_cell(f,k,G) & right_cell(R_Cut(f,p),k,G) = right_cell(f,k,G) proof let G be Go-board; let f be S-Sequence_in_R2; let p be Point of TOP-REAL 2; let k be Nat; assume that A1: 1 <= k and A2: k < p..f and A3: f is_sequence_on G and A4: p in rng f; p..f >= 1 by A1,A2,AXIOMS:22; then A5: f|(p..f) = mid(f,1,p..f) by JORDAN3:25 .= R_Cut(f,p) by A4,JORDAN1G:57; A6: k+1 <= p..f by A2,NAT_1:38; p..f <= len f by A4,FINSEQ_4:31; then k+1 <= len f by A6,AXIOMS:22; hence thesis by A1,A3,A5,A6,GOBRD13:32; end; theorem Th53: for G be Go-board for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 for k be Nat st 1 <= k & k < p..f & f is_sequence_on G holds left_cell(f-:p,k,G) = left_cell(f,k,G) & right_cell(f-:p,k,G) = right_cell(f,k,G) proof let G be Go-board; let f be FinSequence of TOP-REAL 2; let p be Point of TOP-REAL 2; let k be Nat; assume that A1: 1 <= k and A2: k < p..f and A3: f is_sequence_on G; A4: f|(p..f) = f-:p by FINSEQ_5:def 1; A5: k+1 <= p..f by A2,NAT_1:38; per cases by TOPREAL8:4; suppose p in rng f; then p..f <= len f by FINSEQ_4:31; then k+1 <= len f by A5,AXIOMS:22; hence thesis by A1,A3,A4,A5,GOBRD13:32; suppose p..f = 0; hence thesis by A2,NAT_1:18; end; theorem Th54: for f,g be FinSequence of TOP-REAL 2 st f is unfolded s.n.c. one-to-one & g is unfolded s.n.c. one-to-one & f/.len f = g/.1 & L~f /\ L~g = {g/.1} holds f^'g is s.n.c. proof let f,g be FinSequence of TOP-REAL 2; assume that A1: f is unfolded s.n.c. one-to-one and A2: g is unfolded s.n.c. one-to-one and A3: f/.len f = g/.1 and A4: L~f /\ L~g = {g/.1}; now let i,j be Nat; assume A5: i+1 < j; now per cases; suppose A6: j < len f; then A7: LSeg(f^'g,j) = LSeg(f,j) by TOPREAL8:28; i+1 < len f by A5,A6,AXIOMS:22; then i < len f by NAT_1:38; then LSeg(f^'g,i) = LSeg(f,i) by TOPREAL8:28; hence LSeg(f^'g,i) misses LSeg(f^'g,j) by A1,A5,A7,TOPREAL1:def 9; suppose j >= len f; then consider k be Nat such that A8: j = len f + k by NAT_1:28; A9: now assume f is empty; then len f = 0 by FINSEQ_1:25; then L~f = {} by TOPREAL1:28; hence contradiction by A4; end; A10: now assume g is trivial; then len g < 2 by SPPOL_1:2; then len g = 0 or len g = 1 by ALGSEQ_1:4; then L~g = {} by TOPREAL1:28; hence contradiction by A4; end; now per cases; suppose A11: i >= 1 & j+1 <= len(f^'g); then j+1 < len(f^'g)+1 by NAT_1:38; then len f+k+1 < len f + len g by A8,A10,GRAPH_2:13; then len f+(k+1) < len f + len g by XCMPLX_1:1; then A12: k+1 < len g by REAL_1:55; then A13: LSeg(f^'g,len f+k) = LSeg(g,k+1) by A3,A9,A10,TOPREAL8:31; then A14: LSeg(f^'g,j) c= L~g by A8,TOPREAL3:26; now per cases; suppose A15: i < len f; then A16: LSeg(f^'g,i) = LSeg(f,i) by TOPREAL8:28; then LSeg(f^'g,i) c= L~f by TOPREAL3:26; then A17: LSeg(f^'g,i) /\ LSeg(f^'g,j) c= {g/.1} by A4,A14,XBOOLE_1: 27; assume LSeg(f^'g,i) meets LSeg(f^'g,j); then consider x be set such that A18: x in LSeg(f^'g,i) and A19: x in LSeg(f^'g,j) by XBOOLE_0:3; x in LSeg(f^'g,i) /\ LSeg(f^'g,j) by A18,A19,XBOOLE_0:def 3; then A20: x = g/.1 by A17,TARSKI:def 1; A21: i in dom f by A11,A15,FINSEQ_3:27; i+1 > 1 & i+1 <= len f by A11,A15,NAT_1:38; then i+1 in dom f by FINSEQ_3:27; then len f+0 < len f+k by A1,A3,A5,A8,A16,A18,A20,A21,GOBOARD2:7; then k > 0 by REAL_1:55; then A22: k+1 > 0+1 by REAL_1:53; len g >= 2 by A10,SPPOL_1:2; hence contradiction by A2,A8,A13,A19,A20,A22,JORDAN5B:33; suppose i >= len f; then consider l be Nat such that A23: i = len f + l by NAT_1:28; len f+(l+1) < len f+k by A5,A8,A23,XCMPLX_1:1; then l+1 < k by REAL_1:55; then A24: l+1+1 < k+1 by REAL_1:53; then l+1+1 < len g by A12,AXIOMS:22; then l+1 < len g by NAT_1:38; then LSeg(f^'g,len f+l) = LSeg(g,l+1) by A3,A9,A10,TOPREAL8:31; hence LSeg(f^'g,i) misses LSeg(f^'g,j) by A2,A8,A13,A23,A24,TOPREAL1:def 9; end; hence LSeg(f^'g,i) misses LSeg(f^'g,j); suppose j+1 > len(f^'g); then LSeg(f^'g,j) = {} by TOPREAL1:def 5; hence LSeg(f^'g,i) misses LSeg(f^'g,j) by XBOOLE_1:65; suppose i < 1; then LSeg(f^'g,i) = {} by TOPREAL1:def 5; hence LSeg(f^'g,i) misses LSeg(f^'g,j) by XBOOLE_1:65; end; hence LSeg(f^'g,i) misses LSeg(f^'g,j); end; hence LSeg(f^'g,i) misses LSeg(f^'g,j); end; hence f^'g is s.n.c. by TOPREAL1:def 9; end; theorem Th55: for f,g be FinSequence of TOP-REAL 2 st f is one-to-one & g is one-to-one & rng f /\ rng g c= {g/.1} holds f^'g is one-to-one proof let f,g be FinSequence of TOP-REAL 2; assume that A1: f is one-to-one and A2: g is one-to-one and A3: rng f /\ rng g c= {g/.1}; per cases; suppose A4: rng g <> {}; now let i,j be Nat; assume that A5: i in dom (f^'g) and A6: j in dom (f^'g) and A7: (f^'g)/.i = (f^'g)/.j; A8: 1 <= i & i <= len (f^'g) by A5,FINSEQ_3:27; A9: 1 <= j & j <= len (f^'g) by A6,FINSEQ_3:27; g <> {} by A4,FINSEQ_1:27; then len (f^'g)+1 = len f + len g by GRAPH_2:13; then A10: i < len f + len g & j < len f + len g by A8,A9,NAT_1:38; A11: len f = len f + 0; A12: 1 in dom g by A4,FINSEQ_3:34; now per cases; suppose A13: i <= len f & j <= len f; then A14: (f^'g)/.i = f/.i & (f^'g)/.j = f/.j by A8,A9,AMISTD_1:9; i in dom f & j in dom f by A8,A9,A13,FINSEQ_3:27; hence i = j by A1,A7,A14,PARTFUN2:17; suppose A15: i > len f & j > len f; then consider k be Nat such that A16: i = len f + k by NAT_1:28; consider l be Nat such that A17: j = len f + l by A15,NAT_1:28; A18: k < len g & l < len g by A10,A16,A17,REAL_1:55; k > 0 by A11,A15,A16,REAL_1:55; then A19: k >= 0+1 by NAT_1:38; then A20: (f^'g)/.i = g/.(k+1) by A16,A18,AMISTD_1:10; l > 0 by A11,A15,A17,REAL_1:55; then A21: l >= 0+1 by NAT_1:38; then A22: (f^'g)/.j = g/.(l+1) by A17,A18,AMISTD_1:10; A23: k+1 <= len g & l+1 <= len g by A18,NAT_1:38; k+1 > 1 & l+1 > 1 by A19,A21,NAT_1:38; then k+1 in dom g & l+1 in dom g by A23,FINSEQ_3:27; then k+1 = l+1 by A2,A7,A20,A22,PARTFUN2:17; hence i = j by A16,A17,XCMPLX_1:2; suppose A24: i <= len f & j > len f; then A25: (f^'g)/.i = f/.i by A8,AMISTD_1:9; i in dom f by A8,A24,FINSEQ_3:27; then A26: (f^'g)/.i in rng f by A25,PARTFUN2:4; consider l be Nat such that A27: j = len f + l by A24,NAT_1:28; A28: l < len g by A10,A27,REAL_1:55; l > 0 by A11,A24,A27,REAL_1:55; then A29: l >= 0+1 by NAT_1:38; then A30: (f^'g)/.j = g/.(l+1) by A27,A28,AMISTD_1:10; A31: l+1 <= len g by A28,NAT_1:38; A32: l+1 > 1 by A29,NAT_1:38; then A33: l+1 in dom g by A31,FINSEQ_3:27; then (f^'g)/.j in rng g by A30,PARTFUN2:4; then (f^'g)/.j in rng f /\ rng g by A7,A26,XBOOLE_0:def 3; then g/.(l+1) = g/.1 by A3,A30,TARSKI:def 1; hence i = j by A2,A12,A32,A33,PARTFUN2:17; suppose A34: j <= len f & i > len f; then A35: (f^'g)/.j = f/.j by A9,AMISTD_1:9; j in dom f by A9,A34,FINSEQ_3:27; then A36: (f^'g)/.j in rng f by A35,PARTFUN2:4; consider l be Nat such that A37: i = len f + l by A34,NAT_1:28; A38: l < len g by A10,A37,REAL_1:55; l > 0 by A11,A34,A37,REAL_1:55; then A39: l >= 0+1 by NAT_1:38; then A40: (f^'g)/.i = g/.(l+1) by A37,A38,AMISTD_1:10; A41: l+1 <= len g by A38,NAT_1:38; A42: l+1 > 1 by A39,NAT_1:38; then A43: l+1 in dom g by A41,FINSEQ_3:27; then (f^'g)/.i in rng g by A40,PARTFUN2:4; then (f^'g)/.i in rng f /\ rng g by A7,A36,XBOOLE_0:def 3; then g/.(l+1) = g/.1 by A3,A40,TARSKI:def 1; hence i = j by A2,A12,A42,A43,PARTFUN2:17; end; hence i = j; end; hence f^'g is one-to-one by PARTFUN2:16; suppose rng g = {}; then g = {} by FINSEQ_1:27; hence f^'g is one-to-one by A1,AMISTD_1:7; end; theorem Th56: for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st f is_S-Seq & p in rng f & p <> f.1 holds Index(p,f)+1 = p..f proof let f be FinSequence of TOP-REAL 2; let p be Point of TOP-REAL 2; assume that A1: f is_S-Seq and A2: p in rng f and A3: p <> f.1; A4: 1 <= p..f & p..f <= len f by A2,FINSEQ_4:31; p..f <> 1 by A2,A3,FINSEQ_4:29; then A5: 1 < p..f by A4,REAL_1:def 5; f.(p..f) = p by A2,FINSEQ_4:29; hence Index(p,f)+1 = p..f by A1,A4,A5,JORDAN3:45; end; theorem Th57: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= j & k <= width Gauge(C,n) & Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) & Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) holds j <> k proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let i,j,k be Nat; assume that A1: 1 < i & i < len Gauge(C,n) and A2: 1 <= j & k <= width Gauge(C,n) and A3: Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) and A4: Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) and A5: j = k; A6: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) by A3,A4,A5,XBOOLE_0:def 3; then A7: Gauge(C,n)*(i,k) in {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:20; A8: [i,j] in Indices Gauge(C,n) by A1,A2,A5,GOBOARD7:10; len Gauge(C,n) >= 4 by JORDAN8:13; then A9: len Gauge(C,n) >= 1 by AXIOMS:22; then A10: [len Gauge(C,n),j] in Indices Gauge(C,n) by A2,A5,GOBOARD7:10; A11: [1,j] in Indices Gauge(C,n) by A2,A5,A9,GOBOARD7:10; per cases by A7,TARSKI:def 2; suppose A12: Gauge(C,n)*(i,k) = W-min L~Cage(C,n); Gauge(C,n)*(1,j)`1 = W-bound L~Cage(C,n) by A2,A5,A6,JORDAN1A:94; then (W-min L~Cage(C,n))`1 <> W-bound L~Cage(C,n) by A1,A5,A8,A11,A12,JORDAN1G:7; hence contradiction by PSCOMP_1:84; suppose A13: Gauge(C,n)*(i,k) = E-max L~Cage(C,n); Gauge(C,n)*(len Gauge(C,n),j)`1 = E-bound L~Cage(C,n) by A2,A5,A6,JORDAN1A:92; then (E-max L~Cage(C,n))`1 <> E-bound L~Cage(C,n) by A1,A5,A8,A10,A13,JORDAN1G:7; hence contradiction by PSCOMP_1:104; end; theorem Th58: for C be Simple_closed_curve for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i,k)} & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(i,j)} holds LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C proof let C be Simple_closed_curve; let i,j,k be Nat; set Ga = Gauge(C,n); set US = Upper_Seq(C,n); set LS = Lower_Seq(C,n); set LA = Lower_Arc C; 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 Gij = Ga*(i,j); set Gik = Ga*(i,k); assume that A1: 1 < i & i < len Ga and A2: 1 <= j & j <= k & k <= width Ga and A3: LSeg(Gij,Gik) /\ L~US = {Gik} and A4: LSeg(Gij,Gik) /\ L~LS = {Gij} and A5: LSeg(Gij,Gik) misses LA; Gij in {Gij} by TARSKI:def 1; then A6: Gij in L~LS by A4,XBOOLE_0:def 3; Gik in {Gik} by TARSKI:def 1; then A7: Gik in L~US by A3,XBOOLE_0:def 3; then A8: j <> k by A1,A2,A6,Th57; A9: 1 <= j & j <= width Ga by A2,AXIOMS:22; A10: 1 <= k & k <= width Ga by A2,AXIOMS:22; A11: [i,j] in Indices Ga by A1,A9,GOBOARD7:10; A12: [i,k] in Indices Ga by A1,A10,GOBOARD7:10; A13: US is_sequence_on Ga by JORDAN1G:4; A14: LS is_sequence_on Ga by JORDAN1G:5; set go = R_Cut(US,Gik); set do = L_Cut(LS,Gij); A15: len Ga = width Ga by JORDAN8:def 1; A16: len US >= 3 by JORDAN1E:19; then len US >= 1 by AXIOMS:22; then 1 in dom US by FINSEQ_3:27; then A17: US.1 = US/.1 by FINSEQ_4:def 4 .= Wmin by JORDAN1F:5; A18: Wmin`1 = Wbo by PSCOMP_1:84 .= Ga*(1,k)`1 by A10,A15,JORDAN1A:94; len Ga >= 4 by JORDAN8:13; then A19: len Ga >= 1 by AXIOMS:22; then A20: [1,k] in Indices Ga by A10,GOBOARD7:10; then A21: Gik <> US.1 by A1,A12,A17,A18,JORDAN1G:7; then reconsider go as being_S-Seq FinSequence of TOP-REAL 2 by A7,JORDAN3:70; A22: len LS >= 1+2 by JORDAN1E:19; then len LS >= 1 by AXIOMS:22; then A23: 1 in dom LS & len LS in dom LS by FINSEQ_3:27; then A24: LS.len LS = LS/.len LS by FINSEQ_4:def 4 .= Wmin by JORDAN1F:8; A25: Wmin`1 = Wbo by PSCOMP_1:84 .= Ga*(1,k)`1 by A10,A15,JORDAN1A:94; A26: [i,j] in Indices Ga by A1,A9,GOBOARD7:10; then A27: Gij <> LS.len LS by A1,A20,A24,A25,JORDAN1G:7; then reconsider do as being_S-Seq FinSequence of TOP-REAL 2 by A6,JORDAN3:69; A28: [len Ga,k] in Indices Ga by A10,A19,GOBOARD7:10; A29: LS.1 = LS/.1 by A23,FINSEQ_4:def 4 .= Emax by JORDAN1F:6; Emax`1 = Ebo by PSCOMP_1:104 .= Ga*(len Ga,k)`1 by A10,A15,JORDAN1A:92; then A30: Gij <> LS.1 by A1,A26,A28,A29,JORDAN1G:7; A31: len go >= 1+1 by TOPREAL1:def 10; A32: Gik in rng US by A1,A7,A10,A13,Th40; then A33: go is_sequence_on Ga by A13,Th38; A34: len do >= 1+1 by TOPREAL1:def 10; A35: Gij in rng LS by A1,A6,A9,A14,Th40; then A36: do is_sequence_on Ga by A14,Th39; reconsider go as non constant s.c.c. (being_S-Seq FinSequence of TOP-REAL 2) by A31,A33,JGRAPH_1:16, JORDAN8:8; reconsider do as non constant s.c.c. (being_S-Seq FinSequence of TOP-REAL 2) by A34,A36,JGRAPH_1:16, JORDAN8:8; A37: len go > 1 by A31,NAT_1:38; then A38: len go in dom go by FINSEQ_3:27; then A39: go/.len go = go.len go by FINSEQ_4:def 4 .= Gik by A7,JORDAN3:59; len do >= 1 by A34,AXIOMS:22; then 1 in dom do by FINSEQ_3:27; then A40: do/.1 = do.1 by FINSEQ_4:def 4 .= Gij by A6,JORDAN3:58; reconsider m = len go - 1 as Nat by A38,FINSEQ_3:28; A41: m+1 = len go by XCMPLX_1:27; then A42: len go-'1 = m by BINARITH:39; A43: LSeg(go,m) c= L~go by TOPREAL3:26; A44: L~go c= L~US by A7,JORDAN3:76; then LSeg(go,m) c= L~US by A43,XBOOLE_1:1; then A45: LSeg(go,m) /\ LSeg(Gik,Gij) c= {Gik} by A3,XBOOLE_1:26; m >= 1 by A31,REAL_1:84; then A46: LSeg(go,m) = LSeg(go/.m,Gik) by A39,A41,TOPREAL1:def 5; {Gik} c= LSeg(go,m) /\ LSeg(Gik,Gij) proof let x be set; assume x in {Gik}; then A47: x = Gik by TARSKI:def 1; A48: Gik in LSeg(go,m) by A46,TOPREAL1:6; Gik in LSeg(Gik,Gij) by TOPREAL1:6; hence x in LSeg(go,m) /\ LSeg(Gik,Gij) by A47,A48,XBOOLE_0:def 3; end; then A49: LSeg(go,m) /\ LSeg(Gik,Gij) = {Gik} by A45,XBOOLE_0:def 10; A50: LSeg(do,1) c= L~do by TOPREAL3:26; A51: L~do c= L~LS by A6,JORDAN3:77; then LSeg(do,1) c= L~LS by A50,XBOOLE_1:1; then A52: LSeg(do,1) /\ LSeg(Gik,Gij) c= {Gij} by A4,XBOOLE_1:26; A53: LSeg(do,1) = LSeg(Gij,do/.(1+1)) by A34,A40,TOPREAL1:def 5; {Gij} c= LSeg(do,1) /\ LSeg(Gik,Gij) proof let x be set; assume x in {Gij}; then A54: x = Gij by TARSKI:def 1; A55: Gij in LSeg(do,1) by A53,TOPREAL1:6; Gij in LSeg(Gik,Gij) by TOPREAL1:6; hence x in LSeg(do,1) /\ LSeg(Gik,Gij) by A54,A55,XBOOLE_0:def 3; end; then A56: LSeg(Gik,Gij) /\ LSeg(do,1) = {Gij} by A52,XBOOLE_0:def 10; A57: go/.1 = US/.1 by A7,SPRECT_3:39 .= Wmin by JORDAN1F:5; then A58: go/.1 = LS/.len LS by JORDAN1F:8 .= do/.len do by A6,Th35; A59: rng go c= L~go & rng do c= L~do by A31,A34,SPPOL_2:18; A60: {go/.1} c= L~go /\ L~do proof let x be set; assume x in {go/.1}; then x = go/.1 by TARSKI:def 1; then x in rng go & x in rng do by A58,FINSEQ_6:46,REVROT_1:3; hence x in L~go /\ L~do by A59,XBOOLE_0:def 3; end; A61: LS.1 = LS/.1 by A23,FINSEQ_4:def 4 .= Emax by JORDAN1F:6; A62: [len Ga,j] in Indices Ga by A9,A19,GOBOARD7:10; L~go /\ L~do c= {go/.1} proof let x be set; assume x in L~go /\ L~do; then A63: x in L~go & x in L~do by XBOOLE_0:def 3; then x in L~US /\ L~LS by A44,A51,XBOOLE_0:def 3; then x in {Wmin,Emax} by JORDAN1E:20; then A64: x = Wmin or x = Emax by TARSKI:def 2; now assume x = Emax; then A65: Emax = Gij by A6,A61,A63,JORDAN1E:11; Ga*(len Ga,j)`1 = Ebo by A9,A15,JORDAN1A:92; then Emax`1 <> Ebo by A1,A11,A62,A65,JORDAN1G:7; hence contradiction by PSCOMP_1:104; end; hence x in {go/.1} by A57,A64,TARSKI:def 1; end; then A66: L~go /\ L~do = {go/.1} by A60,XBOOLE_0:def 10; set W2 = go/.2; A67: 2 in dom go by A31,FINSEQ_3:27; A68: Gik..US >= 1 by A32,FINSEQ_4:31; A69: now assume Gik`1 = Wbo; then Ga*(1,k)`1 = Ga*(i,k)`1 by A10,A15,JORDAN1A:94; hence contradiction by A1,A12,A20,JORDAN1G:7; end; go = mid(US,1,Gik..US) by A32,JORDAN1G:57 .= US|(Gik..US) by A68,JORDAN3:25; then A70: W2 = US/.2 by A67,TOPREAL1:1; set pion = <*Gik,Gij*>; A71: now let n be Nat; assume n in dom pion; then n in Seg 2 by FINSEQ_3:29; then n = 1 or n = 2 by FINSEQ_1:4,TARSKI:def 2; then pion/.n = Gik or pion/.n = Gij by FINSEQ_4:26; hence ex i,j be Nat st [i,j] in Indices Ga & pion/.n = Ga*(i,j) by A11,A12; end; A72: Gik <> Gij by A8,A11,A12,GOBOARD1:21; A73: Gik`1 = Ga*(i,1)`1 by A1,A10,GOBOARD5:3 .= Gij`1 by A1,A9,GOBOARD5:3; then LSeg(Gik,Gij) is vertical by SPPOL_1:37; then pion is_S-Seq by A72,JORDAN1B:8; then consider pion1 be FinSequence of TOP-REAL 2 such that A74: pion1 is_sequence_on Ga and A75: pion1 is_S-Seq and A76: L~pion = L~pion1 and A77: pion/.1 = pion1/.1 and A78: pion/.len pion = pion1/.len pion1 and A79: len pion <= len pion1 by A71,GOBOARD3:2; reconsider pion1 as being_S-Seq FinSequence of TOP-REAL 2 by A75; set godo = go^'pion1^'do; len Cage(C,n) > 4 by GOBOARD7:36; then A80: 1+1 <= len Cage(C,n) by AXIOMS:22; then A81: 1+1 <= len Rotate(Cage(C,n),Wmin) by REVROT_1:14; len (go^'pion1) >= len go by TOPREAL8:7; then A82: len (go^'pion1) >= 1+1 by A31,AXIOMS:22; then A83: len (go^'pion1) > 1+0 by NAT_1:38; len godo >= len (go^'pion1) by TOPREAL8:7; then A84: 1+1 <= len godo by A82,AXIOMS:22; A85: US is_sequence_on Ga by JORDAN1G:4; A86: go/.len go = pion1/.1 by A39,A77,FINSEQ_4:26; then A87: go^'pion1 is_sequence_on Ga by A33,A74,TOPREAL8:12; A88: (go^'pion1)/.len (go^'pion1) = pion/.len pion by A78,AMISTD_1:6 .= pion/.2 by FINSEQ_1:61 .= do/.1 by A40,FINSEQ_4:26; then A89: godo is_sequence_on Ga by A36,A87,TOPREAL8:12; LSeg(pion1,1) c= L~<*Gik,Gij*> by A76,TOPREAL3:26; then LSeg(pion1,1) c= LSeg(Gik,Gij) by SPPOL_2:21; then A90: LSeg(go,len go-'1) /\ LSeg(pion1,1) c= {Gik} by A42,A49,XBOOLE_1: 27; A91: len pion1 >= 1+1 by A79,FINSEQ_1:61; {Gik} c= LSeg(go,m) /\ LSeg(pion1,1) proof let x be set; assume x in {Gik}; then A92: x = Gik by TARSKI:def 1; A93: Gik in LSeg(go,m) by A46,TOPREAL1:6; Gik in LSeg(pion1,1) by A39,A86,A91,TOPREAL1:27; hence x in LSeg(go,m) /\ LSeg(pion1,1) by A92,A93,XBOOLE_0:def 3; end; then LSeg(go,len go-'1) /\ LSeg(pion1,1) = { go/.len go } by A39,A42,A90,XBOOLE_0:def 10 ; then A94: go^'pion1 is unfolded by A86,TOPREAL8:34; len pion1 >= 2+0 by A79,FINSEQ_1:61; then A95: len pion1-2 >= 0 by REAL_1:84; A96: len (go^'pion1)-1 >= 0 by A83,REAL_1:84; len (go^'pion1)+1-1 = len go+len pion1-1 by GRAPH_2:13; then len (go^'pion1)-1 = len go+len pion1-1-1 by XCMPLX_1:26 .= len go + len pion1-(1+1) by XCMPLX_1:36 .= len go + (len pion1-2) by XCMPLX_1:29 .= len go + (len pion1-'2) by A95,BINARITH:def 3; then A97: len (go^'pion1)-'1 = len go + (len pion1-'2) by A96,BINARITH:def 3; A98: len pion1-1 >= 1 by A91,REAL_1:84; then A99: len pion1-1 >= 0 by AXIOMS:22; then A100: len pion1-'1 = len pion1-1 by BINARITH:def 3; A101: len pion1-'2+1 = len pion1-2+1 by A95,BINARITH:def 3 .= len pion1-(2-1) by XCMPLX_1:37 .= len pion1-'1 by A99,BINARITH:def 3; len pion1-1+1 <= len pion1 by XCMPLX_1:27; then A102: len pion1-'1 < len pion1 by A100,NAT_1:38; LSeg(pion1,len pion1-'1) c= L~<*Gik,Gij*> by A76,TOPREAL3:26; then LSeg(pion1,len pion1-'1) c= LSeg(Gik,Gij) by SPPOL_2:21; then A103: LSeg(pion1,len pion1-'1) /\ LSeg(do,1) c= {Gij} by A56,XBOOLE_1: 27; {Gij} c= LSeg(pion1,len pion1-'1) /\ LSeg(do,1) proof let x be set; assume x in {Gij}; then A104: x = Gij by TARSKI:def 1; A105: Gij in LSeg(do,1) by A53,TOPREAL1:6; A106: len pion1-'1+1 = len pion1 by A100,XCMPLX_1:27; then pion1/.(len pion1-'1+1) = pion/.2 by A78,FINSEQ_1:61 .= Gij by FINSEQ_4:26; then Gij in LSeg(pion1,len pion1-'1) by A98,A100,A106,TOPREAL1:27; hence x in LSeg(pion1,len pion1-'1) /\ LSeg(do,1) by A104,A105,XBOOLE_0: def 3; end; then LSeg(pion1,len pion1-'1) /\ LSeg(do,1) = {Gij} by A103,XBOOLE_0:def 10 ; then A107: LSeg(go^'pion1,len go+(len pion1-'2)) /\ LSeg(do,1) = {(go^'pion1)/.len (go^'pion1)} by A40,A86,A88,A101,A102,TOPREAL8:31; A108: (go^'pion1) is non trivial by A82,SPPOL_1:2; A109: rng pion1 c= L~pion1 by A91,SPPOL_2:18; A110: {pion1/.1} c= L~go /\ L~pion1 proof let x be set; assume x in {pion1/.1}; then x = pion1/.1 by TARSKI:def 1; then x in rng go & x in rng pion1 by A86,FINSEQ_6:46,REVROT_1:3; hence x in L~go /\ L~pion1 by A59,A109,XBOOLE_0:def 3; end; L~go /\ L~pion1 c= {pion1/.1} proof let x be set; assume x in L~go /\ L~pion1; then x in L~go & x in L~pion1 by XBOOLE_0:def 3; then x in L~pion1 /\ L~US by A44,XBOOLE_0:def 3; hence x in {pion1/.1} by A3,A39,A76,A86,SPPOL_2:21; end; then A111: L~go /\ L~pion1 = {pion1/.1} by A110,XBOOLE_0:def 10; then A112: (go^'pion1) is s.n.c. by A86,Th54; rng go /\ rng pion1 c= {pion1/.1} by A59,A109,A111,XBOOLE_1:27; then A113: go^'pion1 is one-to-one by Th55; A114: pion/.len pion = pion/.2 by FINSEQ_1:61 .= do/.1 by A40,FINSEQ_4:26; A115: {pion1/.len pion1} c= L~do /\ L~pion1 proof let x be set; assume x in {pion1/.len pion1}; then x = pion1/.len pion1 by TARSKI:def 1; then x in rng do & x in rng pion1 by A78,A114,FINSEQ_6:46,REVROT_1:3; hence x in L~do /\ L~pion1 by A59,A109,XBOOLE_0:def 3; end; L~do /\ L~pion1 c= {pion1/.len pion1} proof let x be set; assume x in L~do /\ L~pion1; then x in L~do & x in L~pion1 by XBOOLE_0:def 3; then x in L~pion1 /\ L~LS by A51,XBOOLE_0:def 3; hence x in {pion1/.len pion1} by A4,A40,A76,A78,A114,SPPOL_2:21; end; then A116: L~do /\ L~pion1 = {pion1/.len pion1} by A115,XBOOLE_0:def 10; A117: L~(go^'pion1) /\ L~do = (L~go \/ L~pion1) /\ L~do by A86,TOPREAL8:35 .= {go/.1} \/ {do/.1} by A66,A78,A114,A116,XBOOLE_1:23 .= {(go^'pion1)/.1} \/ {do/.1} by AMISTD_1:5 .= {(go^'pion1)/.1,do/.1} by ENUMSET1:41; do/.len do = (go^'pion1)/.1 by A58,AMISTD_1:5; then reconsider godo as non constant standard special_circular_sequence by A84,A88,A89,A94,A97,A107,A108, A112,A113,A117,JORDAN8:7,8,TOPREAL8:11,33,34; A118: LA is_an_arc_of E-max C,W-min C by JORDAN6:def 9; then A119: LA is connected by JORDAN6:11; A120: W-min C in LA & E-max C in LA by A118,TOPREAL1:4; set ff = Rotate(Cage(C,n),Wmin); Wmin in rng Cage(C,n) by SPRECT_2:47; then A121: ff/.1 = Wmin by FINSEQ_6:98; A122: L~ff = L~Cage(C,n) by REVROT_1:33; then A123: (W-max L~ff)..ff > 1 by A121,SPRECT_5:23; (W-max L~ff)..ff <= (N-min L~ff)..ff by A121,A122,SPRECT_5:24; then A124: (N-min L~ff)..ff > 1 by A123,AXIOMS:22; (N-min L~ff)..ff < (N-max L~ff)..ff by A121,A122,SPRECT_5:25; then A125: (N-max L~ff)..ff > 1 by A124,AXIOMS:22; (N-max L~ff)..ff <= (E-max L~ff)..ff by A121,A122,SPRECT_5:26; then A126: Emax..ff > 1 by A122,A125,AXIOMS:22; A127: now assume A128: Gik..US <= 1; Gik..US >= 1 by A32,FINSEQ_4:31; then Gik..US = 1 by A128,AXIOMS:21; then Gik = US/.1 by A32,FINSEQ_5:41; hence contradiction by A17,A21,JORDAN1F:5; end; A129: Cage(C,n) is_sequence_on Ga by JORDAN9:def 1; then A130: ff is_sequence_on Ga by REVROT_1:34; A131: right_cell(godo,1,Ga)\L~godo c= RightComp godo by A84,A89,JORDAN9:29; A132: L~godo = L~(go^'pion1) \/ L~do by A88,TOPREAL8:35 .= L~go \/ L~pion1 \/ L~do by A86,TOPREAL8:35; L~Cage(C,n) = L~US \/ L~LS by JORDAN1E:17; then A133: L~US c= L~Cage(C,n) & L~LS c= L~Cage(C,n) by XBOOLE_1:7; then A134: L~go c= L~Cage(C,n) & L~do c= L~Cage(C,n) by A44,A51,XBOOLE_1:1; A135: W-min C in C by SPRECT_1:15; A136: L~pion = LSeg(Gik,Gij) by SPPOL_2:21; A137: now assume W-min C in L~godo; then A138: W-min C in L~go \/ L~pion1 or W-min C in L~do by A132,XBOOLE_0: def 2; per cases by A138,XBOOLE_0:def 2; suppose W-min C in L~go; then C meets L~Cage(C,n) by A134,A135,XBOOLE_0:3; hence contradiction by JORDAN10:5; suppose W-min C in L~pion1; hence contradiction by A5,A76,A120,A136,XBOOLE_0:3; suppose W-min C in L~do; then C meets L~Cage(C,n) by A134,A135,XBOOLE_0:3; hence contradiction by JORDAN10:5; end; right_cell(Rotate(Cage(C,n),Wmin),1) = right_cell(ff,1,GoB ff) by A81,JORDAN1H:29 .= right_cell(ff,1,GoB Cage(C,n)) by REVROT_1:28 .= right_cell(ff,1,Ga) by JORDAN1H:52 .= right_cell(ff-:Emax,1,Ga) by A126,A130,Th53 .= right_cell(US,1,Ga) by JORDAN1E:def 1 .= right_cell(R_Cut(US,Gik),1,Ga) by A32,A85,A127,Th52 .= right_cell(go^'pion1,1,Ga) by A37,A87,Th51 .= right_cell(godo,1,Ga) by A83,A89,Th51; then W-min C in right_cell(godo,1,Ga) by JORDAN1I:8; then A139: W-min C in right_cell(godo,1,Ga)\L~godo by A137,XBOOLE_0:def 4; A140: godo/.1 = (go^'pion1)/.1 by AMISTD_1:5 .= Wmin by A57,AMISTD_1:5; A141: len US >= 2 by A16,AXIOMS:22; A142: godo/.2 = (go^'pion1)/.2 by A82,AMISTD_1:9 .= US/.2 by A31,A70,AMISTD_1:9 .= (US^'LS)/.2 by A141,AMISTD_1:9 .= Rotate(Cage(C,n),Wmin)/.2 by JORDAN1E:15; A143: L~go \/ L~do is compact by COMPTS_1:19; A144: L~go \/ L~do c= L~Cage(C,n) by A134,XBOOLE_1:8; Wmin in rng go by A57,FINSEQ_6:46; then Wmin in L~go \/ L~do by A59,XBOOLE_0:def 2; then A145: W-min (L~go \/ L~do) = Wmin by A143,A144,Th21; A146: (W-min (L~go \/ L~do))`1 = W-bound (L~go \/ L~do) & Wmin`1 = Wbo by PSCOMP_1:84; W-bound LSeg(Gik,Gij) = Gik`1 by A73,SPRECT_1:62; then A147: W-bound L~pion1 = Gik`1 by A76,SPPOL_2:21; Gik`1 >= Wbo by A7,A133,PSCOMP_1:71; then Gik`1 > Wbo by A69,REAL_1:def 5; then W-min (L~go\/L~do\/L~pion1) = W-min (L~go \/ L~do) by A143,A145,A146,A147,Th33; then A148: W-min L~godo = Wmin by A132,A145,XBOOLE_1:4; A149: rng godo c= L~godo by A84,SPPOL_2:18; 2 in dom godo by A84,FINSEQ_3:27; then A150: godo/.2 in rng godo by PARTFUN2:4; godo/.2 in W-most L~Cage(C,n) by A142,JORDAN1I:27; then (godo/.2)`1 = (W-min L~godo)`1 by A148,PSCOMP_1:88 .= W-bound L~godo by PSCOMP_1:84; then godo/.2 in W-most L~godo by A149,A150,SPRECT_2:16; then Rotate(godo,W-min L~godo)/.2 in W-most L~godo by A140,A148,FINSEQ_6:95 ; then reconsider godo as clockwise_oriented non constant standard special_circular_sequence by JORDAN1I:27; len US in dom US by FINSEQ_5:6; then A151: US.len US = US/.len US by FINSEQ_4:def 4 .= Emax by JORDAN1F:7; A152: E-max C in E-most C by PSCOMP_1:111; A153: east_halfline E-max C misses L~go proof assume east_halfline E-max C meets L~go; then consider p be set such that A154: p in east_halfline E-max C and A155: p in L~go by XBOOLE_0:3; reconsider p as Point of TOP-REAL 2 by A154; p in L~US by A44,A155; then p in east_halfline E-max C /\ L~Cage(C,n) by A133,A154,XBOOLE_0:def 3 ; then A156: p`1 = Ebo by A152,JORDAN1A:104; then A157: p = Emax by A44,A155,Th46; then Emax = Gik by A7,A151,A155,Th43; then Gik`1 = Ga*(len Ga,k)`1 by A10,A15,A156,A157,JORDAN1A:92; hence contradiction by A1,A12,A28,JORDAN1G:7; end; now assume east_halfline E-max C meets L~godo; then A158: east_halfline E-max C meets (L~go \/ L~pion1) or east_halfline E-max C meets L~do by A132,XBOOLE_1:70; per cases by A158,XBOOLE_1:70; suppose east_halfline E-max C meets L~go; hence contradiction by A153; suppose east_halfline E-max C meets L~pion1; then consider p be set such that A159: p in east_halfline E-max C and A160: p in L~pion1 by XBOOLE_0:3; reconsider p as Point of TOP-REAL 2 by A159; A161: p`1 = Gik`1 by A73,A76,A136,A160,GOBOARD7:5; i+1 <= len Ga by A1,NAT_1:38; then i+1-1 <= len Ga-1 by REAL_1:49; then A162: i <= len Ga-1 by XCMPLX_1:26; then len Ga-1 > 0 by A1,AXIOMS:22; then A163: i <= len Ga-'1 by A162,BINARITH:def 3; len Ga-'1 <= len Ga by GOBOARD9:2; then p`1 <= Ga*(len Ga-'1,1)`1 by A1,A10,A15,A19,A161,A163,JORDAN1A:39; then p`1 <= E-bound C by A19,JORDAN8:15; then A164: p`1 <= (E-max C)`1 by PSCOMP_1:104; p`1 >= (E-max C)`1 by A159,JORDAN1A:def 3; then A165: p`1 = (E-max C)`1 by A164,AXIOMS:21; p`2 = (E-max C)`2 by A159,JORDAN1A:def 3; then p = E-max C by A165,TOPREAL3:11; hence contradiction by A5,A76,A120,A136,A160,XBOOLE_0:3; suppose east_halfline E-max C meets L~do; then consider p be set such that A166: p in east_halfline E-max C and A167: p in L~do by XBOOLE_0:3; reconsider p as Point of TOP-REAL 2 by A166; p in L~LS by A51,A167; then p in east_halfline E-max C /\ L~Cage(C,n) by A133,A166,XBOOLE_0:def 3; then A168: p`1 = Ebo by A152,JORDAN1A:104; A169: (E-max C)`2 = p`2 by A166,JORDAN1A:def 3; set RC = Rotate(Cage(C,n),Emax); A170: E-max C in right_cell(RC,1) by JORDAN1I:9; A171: 1+1 <= len LS by A22,AXIOMS:22; LS = RC-:Wmin by JORDAN1G:26; then A172: LSeg(LS,1) = LSeg(RC,1) by A171,SPPOL_2:9; A173: L~RC = L~Cage(C,n) by REVROT_1:33; A174: len RC = len Cage(C,n) by REVROT_1:14; A175: GoB RC = GoB Cage(C,n) by REVROT_1:28 .= Ga by JORDAN1H:52; A176: Emax in rng Cage(C,n) by SPRECT_2:50; A177: RC is_sequence_on Ga by A129,REVROT_1:34; A178: RC/.1 = E-max L~RC by A173,A176,FINSEQ_6:98; then consider ii,jj be Nat such that A179: [ii,jj+1] in Indices Ga and A180: [ii,jj] in Indices Ga and A181: RC/.1 = Ga*(ii,jj+1) and A182: RC/.(1+1) = Ga*(ii,jj) by A80,A174,A177,JORDAN1I:25; consider jj2 be Nat such that A183: 1 <= jj2 & jj2 <= width Ga and A184: Emax = Ga*(len Ga,jj2) by JORDAN1D:29; A185: len Ga >= 4 by JORDAN8:13; then len Ga >= 1 by AXIOMS:22; then [len Ga,jj2] in Indices Ga by A183,GOBOARD7:10; then A186: ii = len Ga by A173,A178,A179,A181,A184,GOBOARD1:21; A187: 1 <= ii & ii <= len Ga & 1 <= jj+1 & jj+1 <= width Ga by A179,GOBOARD5:1; A188: 1 <= ii & ii <= len Ga & 1 <= jj & jj <= width Ga by A180,GOBOARD5:1; A189: ii+1 <> ii by NAT_1:38; jj+1 > jj by NAT_1:38; then jj+1+1 <> jj by NAT_1:38; then A190: right_cell(RC,1) = cell(Ga,ii-'1,jj) by A80,A174,A175,A179,A180,A181,A182,A189,GOBOARD5: def 6; A191: ii-'1+1 = ii by A187,AMI_5:4; A192: ii-1 >= 4-1 by A185,A186,REAL_1:49; then A193: ii-1 >= 1 by AXIOMS:22; ii-1 >= 0 by A192,AXIOMS:22; then A194: 1 <= ii-'1 by A193,BINARITH:def 3; then A195: Ga*(ii-'1,jj)`1 <= (E-max C)`1 & (E-max C)`1 <= Ga*(ii-'1+1, jj)`1 & Ga*(ii-'1,jj)`2 <= (E-max C)`2 & (E-max C)`2 <= Ga*(ii-'1,jj+1)`2 by A170,A187,A188,A190,A191,JORDAN9:19; A196: ii-'1 < len Ga by A187,A191,NAT_1:38; then A197: Ga*(ii-'1,jj)`2 = Ga*(1,jj)`2 by A188,A194,GOBOARD5:2 .= Ga*(ii,jj)`2 by A188,GOBOARD5:2; A198: Ga*(ii-'1,jj+1)`2 = Ga*(1,jj+1)`2 by A187,A194,A196,GOBOARD5:2 .= Ga*(ii,jj+1)`2 by A187,GOBOARD5:2; Ga*(len Ga,jj)`1 = Ebo & Ebo = Ga*(len Ga,jj+1)`1 by A15,A187,A188,JORDAN1A:92; then p in LSeg(RC/.1,RC/.(1+1)) by A168,A169,A181,A182,A186,A195,A197,A198, GOBOARD7:8; then A199: p in LSeg(LS,1) by A80,A172,A174,TOPREAL1:def 5; A200: p in LSeg(do,Index(p,do)) by A167,JORDAN3:42; A201: do = mid(LS,Gij..LS,len LS) by A35,Th37; A202: 1<=Gij..LS & Gij..LS<=len LS by A35,FINSEQ_4:31; Gij..LS <> len LS by A27,A35,FINSEQ_4:29; then A203: Gij..LS < len LS by A202,REAL_1:def 5; A204: 1<=Index(p,do) & Index(p,do) < len do by A167,JORDAN3:41; A205: Index(Gij,LS)+1 = Gij..LS by A30,A35,Th56; consider t be Nat such that A206: t in dom LS and A207: LS.t = Gij by A35,FINSEQ_2:11; A208: 1 <= t & t <= len LS by A206,FINSEQ_3:27; then 1 < t by A30,A207,REAL_1:def 5; then Index(Gij,LS)+1 = t by A207,A208,JORDAN3:45; then A209: len L_Cut(LS,Gij) = len LS-Index(Gij,LS) by A6,A27,A207,JORDAN3:61; set tt = Index(p,do)+(Gij..LS)-'1; A210: 1<=Index(Gij,LS) & 0+Index(Gij,LS) < len LS by A6,JORDAN3:41; then A211: len LS-Index(Gij,LS) > 0 by REAL_1:86; then Index(p,do) < len LS-'Index(Gij,LS) by A204,A209,BINARITH:def 3; then Index(p,do)+1 <= len LS-'Index(Gij,LS) by NAT_1:38; then Index(p,do) <= len LS-'Index(Gij,LS)-1 by REAL_1:84; then Index(p,do) <= len LS-Index(Gij,LS)-1 by A211,BINARITH:def 3; then A212: Index(p,do) <= len LS-Gij..LS by A205,XCMPLX_1:36; then len LS-Gij..LS >= 1 by A204,AXIOMS:22; then len LS-Gij..LS >= 0 by AXIOMS:22; then Index(p,do) <= len LS-'Gij..LS by A212,BINARITH:def 3; then Index(p,do) < len LS-'(Gij..LS)+1 by NAT_1:38; then A213: LSeg(mid(LS,Gij..LS,len LS),Index(p,do)) = LSeg(LS,Index(p,do)+(Gij..LS)-'1) by A202,A203,A204,JORDAN4:31; A214: 1+1 <= Gij..LS by A205,A210,REAL_1:55; then Index(p,do)+Gij..LS >= 1+1+1 by A204,REAL_1:55; then A215: Index(p,do)+Gij..LS-1 >= 1+1+1-1 by REAL_1:49; then A216: Index(p,do)+Gij..LS-1 >= 0 by AXIOMS:22; then A217: tt >= 1+1 by A215,BINARITH:def 3; A218: 2 in dom LS by A171,FINSEQ_3:27; now per cases by A217,REAL_1:def 5; suppose tt > 1+1; then LSeg(LS,1) misses LSeg(LS,tt) by TOPREAL1:def 9; hence contradiction by A199,A200,A201,A213,XBOOLE_0:3; suppose A219: tt = 1+1; then LSeg(LS,1) /\ LSeg(LS,tt) = {LS/.2} by A22,TOPREAL1:def 8; then p in {LS/.2} by A199,A200,A201,A213,XBOOLE_0:def 3; then A220: p = LS/.2 by TARSKI:def 1; then A221: p..LS = 2 by A218,FINSEQ_5:44; 1+1 = Index(p,do)+(Gij..LS)-1 by A216,A219,BINARITH:def 3; then 1+1+1 = Index(p,do)+(Gij..LS) by XCMPLX_1:27; then A222: Gij..LS = 2 by A204,A214,JORDAN1E:10; p in rng LS by A218,A220,PARTFUN2:4; then p = Gij by A35,A221,A222,FINSEQ_5:10; then Gij`1 = Ebo by A220,JORDAN1G:40; then Gij`1 = Ga*(len Ga,j)`1 by A9,A15,JORDAN1A:92; hence contradiction by A1,A11,A62,JORDAN1G:7; end; hence contradiction; end; then east_halfline E-max C c= (L~godo)` by SUBSET_1:43; then consider W be Subset of TOP-REAL 2 such that A223: W is_a_component_of (L~godo)` and A224: east_halfline E-max C c= W by GOBOARD9:5; east_halfline E-max C is not Bounded by JORDAN1C:9; then W is not Bounded by A224,JORDAN2C:16; then W is_outside_component_of L~godo by A223,JORDAN2C:def 4; then W c= UBD L~godo by JORDAN2C:27; then A225: east_halfline E-max C c= UBD L~godo by A224,XBOOLE_1:1; E-max C in east_halfline E-max C by JORDAN1C:7; then E-max C in UBD L~godo by A225; then E-max C in LeftComp godo by GOBRD14:46; then LA meets L~godo by A119,A120,A131,A139,Th36; then A226: LA meets (L~go \/ L~pion1) or LA meets L~do by A132,XBOOLE_1:70; A227: LA c= C by JORDAN1A:16; per cases by A226,XBOOLE_1:70; suppose LA meets L~go; then LA meets L~Cage(C,n) by A134,XBOOLE_1:63; then C meets L~Cage(C,n) by A227,XBOOLE_1:63; hence contradiction by JORDAN10:5; suppose LA meets L~pion1; hence contradiction by A5,A76,A136; suppose LA meets L~do; then LA meets L~Cage(C,n) by A134,XBOOLE_1:63; then C meets L~Cage(C,n) by A227,XBOOLE_1:63; hence contradiction by JORDAN10:5; end; theorem Th59: for C be Simple_closed_curve for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i,k)} & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(i,j)} holds LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C proof let C be Simple_closed_curve; let i,j,k be Nat; set Ga = Gauge(C,n); set US = Upper_Seq(C,n); set LS = Lower_Seq(C,n); set UA = Upper_Arc C; 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 Gij = Ga*(i,j); set Gik = Ga*(i,k); assume that A1: 1 < i & i < len Ga and A2: 1 <= j & j <= k & k <= width Ga and A3: LSeg(Gij,Gik) /\ L~US = {Gik} and A4: LSeg(Gij,Gik) /\ L~LS = {Gij} and A5: LSeg(Gij,Gik) misses UA; Gij in {Gij} by TARSKI:def 1; then A6: Gij in L~LS by A4,XBOOLE_0:def 3; Gik in {Gik} by TARSKI:def 1; then A7: Gik in L~US by A3,XBOOLE_0:def 3; then A8: j <> k by A1,A2,A6,Th57; A9: 1 <= j & j <= width Ga by A2,AXIOMS:22; A10: 1 <= k & k <= width Ga by A2,AXIOMS:22; A11: [i,j] in Indices Ga by A1,A9,GOBOARD7:10; A12: [i,k] in Indices Ga by A1,A10,GOBOARD7:10; A13: US is_sequence_on Ga by JORDAN1G:4; A14: LS is_sequence_on Ga by JORDAN1G:5; set go = R_Cut(US,Gik); set do = L_Cut(LS,Gij); A15: len Ga = width Ga by JORDAN8:def 1; A16: len US >= 3 by JORDAN1E:19; then len US >= 1 by AXIOMS:22; then 1 in dom US by FINSEQ_3:27; then A17: US.1 = US/.1 by FINSEQ_4:def 4 .= Wmin by JORDAN1F:5; A18: Wmin`1 = Wbo by PSCOMP_1:84 .= Ga*(1,k)`1 by A10,A15,JORDAN1A:94; len Ga >= 4 by JORDAN8:13; then A19: len Ga >= 1 by AXIOMS:22; then A20: [1,k] in Indices Ga by A10,GOBOARD7:10; then A21: Gik <> US.1 by A1,A12,A17,A18,JORDAN1G:7; then reconsider go as being_S-Seq FinSequence of TOP-REAL 2 by A7,JORDAN3:70; A22: len LS >= 1+2 by JORDAN1E:19; then len LS >= 1 by AXIOMS:22; then A23: 1 in dom LS & len LS in dom LS by FINSEQ_3:27; then A24: LS.len LS = LS/.len LS by FINSEQ_4:def 4 .= Wmin by JORDAN1F:8; A25: Wmin`1 = Wbo by PSCOMP_1:84 .= Ga*(1,k)`1 by A10,A15,JORDAN1A:94; A26: [i,j] in Indices Ga by A1,A9,GOBOARD7:10; then A27: Gij <> LS.len LS by A1,A20,A24,A25,JORDAN1G:7; then reconsider do as being_S-Seq FinSequence of TOP-REAL 2 by A6,JORDAN3:69; A28: [len Ga,k] in Indices Ga by A10,A19,GOBOARD7:10; A29: LS.1 = LS/.1 by A23,FINSEQ_4:def 4 .= Emax by JORDAN1F:6; Emax`1 = Ebo by PSCOMP_1:104 .= Ga*(len Ga,k)`1 by A10,A15,JORDAN1A:92; then A30: Gij <> LS.1 by A1,A26,A28,A29,JORDAN1G:7; A31: len go >= 1+1 by TOPREAL1:def 10; A32: Gik in rng US by A1,A7,A10,A13,Th40; then A33: go is_sequence_on Ga by A13,Th38; A34: len do >= 1+1 by TOPREAL1:def 10; A35: Gij in rng LS by A1,A6,A9,A14,Th40; then A36: do is_sequence_on Ga by A14,Th39; reconsider go as non constant s.c.c. (being_S-Seq FinSequence of TOP-REAL 2) by A31,A33,JGRAPH_1:16, JORDAN8:8; reconsider do as non constant s.c.c. (being_S-Seq FinSequence of TOP-REAL 2) by A34,A36,JGRAPH_1:16, JORDAN8:8; A37: len go > 1 by A31,NAT_1:38; then A38: len go in dom go by FINSEQ_3:27; then A39: go/.len go = go.len go by FINSEQ_4:def 4 .= Gik by A7,JORDAN3:59; len do >= 1 by A34,AXIOMS:22; then 1 in dom do by FINSEQ_3:27; then A40: do/.1 = do.1 by FINSEQ_4:def 4 .= Gij by A6,JORDAN3:58; reconsider m = len go - 1 as Nat by A38,FINSEQ_3:28; A41: m+1 = len go by XCMPLX_1:27; then A42: len go-'1 = m by BINARITH:39; A43: LSeg(go,m) c= L~go by TOPREAL3:26; A44: L~go c= L~US by A7,JORDAN3:76; then LSeg(go,m) c= L~US by A43,XBOOLE_1:1; then A45: LSeg(go,m) /\ LSeg(Gik,Gij) c= {Gik} by A3,XBOOLE_1:26; m >= 1 by A31,REAL_1:84; then A46: LSeg(go,m) = LSeg(go/.m,Gik) by A39,A41,TOPREAL1:def 5; {Gik} c= LSeg(go,m) /\ LSeg(Gik,Gij) proof let x be set; assume x in {Gik}; then A47: x = Gik by TARSKI:def 1; A48: Gik in LSeg(go,m) by A46,TOPREAL1:6; Gik in LSeg(Gik,Gij) by TOPREAL1:6; hence x in LSeg(go,m) /\ LSeg(Gik,Gij) by A47,A48,XBOOLE_0:def 3; end; then A49: LSeg(go,m) /\ LSeg(Gik,Gij) = {Gik} by A45,XBOOLE_0:def 10; A50: LSeg(do,1) c= L~do by TOPREAL3:26; A51: L~do c= L~LS by A6,JORDAN3:77; then LSeg(do,1) c= L~LS by A50,XBOOLE_1:1; then A52: LSeg(do,1) /\ LSeg(Gik,Gij) c= {Gij} by A4,XBOOLE_1:26; A53: LSeg(do,1) = LSeg(Gij,do/.(1+1)) by A34,A40,TOPREAL1:def 5; {Gij} c= LSeg(do,1) /\ LSeg(Gik,Gij) proof let x be set; assume x in {Gij}; then A54: x = Gij by TARSKI:def 1; A55: Gij in LSeg(do,1) by A53,TOPREAL1:6; Gij in LSeg(Gik,Gij) by TOPREAL1:6; hence x in LSeg(do,1) /\ LSeg(Gik,Gij) by A54,A55,XBOOLE_0:def 3; end; then A56: LSeg(Gik,Gij) /\ LSeg(do,1) = {Gij} by A52,XBOOLE_0:def 10; A57: go/.1 = US/.1 by A7,SPRECT_3:39 .= Wmin by JORDAN1F:5; then A58: go/.1 = LS/.len LS by JORDAN1F:8 .= do/.len do by A6,Th35; A59: rng go c= L~go & rng do c= L~do by A31,A34,SPPOL_2:18; A60: {go/.1} c= L~go /\ L~do proof let x be set; assume x in {go/.1}; then x = go/.1 by TARSKI:def 1; then x in rng go & x in rng do by A58,FINSEQ_6:46,REVROT_1:3; hence x in L~go /\ L~do by A59,XBOOLE_0:def 3; end; A61: LS.1 = LS/.1 by A23,FINSEQ_4:def 4 .= Emax by JORDAN1F:6; A62: [len Ga,j] in Indices Ga by A9,A19,GOBOARD7:10; L~go /\ L~do c= {go/.1} proof let x be set; assume x in L~go /\ L~do; then A63: x in L~go & x in L~do by XBOOLE_0:def 3; then x in L~US /\ L~LS by A44,A51,XBOOLE_0:def 3; then x in {Wmin,Emax} by JORDAN1E:20; then A64: x = Wmin or x = Emax by TARSKI:def 2; now assume x = Emax; then A65: Emax = Gij by A6,A61,A63,JORDAN1E:11; Ga*(len Ga,j)`1 = Ebo by A9,A15,JORDAN1A:92; then Emax`1 <> Ebo by A1,A11,A62,A65,JORDAN1G:7; hence contradiction by PSCOMP_1:104; end; hence x in {go/.1} by A57,A64,TARSKI:def 1; end; then A66: L~go /\ L~do = {go/.1} by A60,XBOOLE_0:def 10; set W2 = go/.2; A67: 2 in dom go by A31,FINSEQ_3:27; A68: Gik..US >= 1 by A32,FINSEQ_4:31; A69: now assume Gik`1 = Wbo; then Ga*(1,k)`1 = Ga*(i,k)`1 by A10,A15,JORDAN1A:94; hence contradiction by A1,A12,A20,JORDAN1G:7; end; go = mid(US,1,Gik..US) by A32,JORDAN1G:57 .= US|(Gik..US) by A68,JORDAN3:25; then A70: W2 = US/.2 by A67,TOPREAL1:1; set pion = <*Gik,Gij*>; A71: now let n be Nat; assume n in dom pion; then n in Seg 2 by FINSEQ_3:29; then n = 1 or n = 2 by FINSEQ_1:4,TARSKI:def 2; then pion/.n = Gik or pion/.n = Gij by FINSEQ_4:26; hence ex i,j be Nat st [i,j] in Indices Ga & pion/.n = Ga*(i,j) by A11,A12; end; A72: Gik <> Gij by A8,A11,A12,GOBOARD1:21; A73: Gik`1 = Ga*(i,1)`1 by A1,A10,GOBOARD5:3 .= Gij`1 by A1,A9,GOBOARD5:3; then LSeg(Gik,Gij) is vertical by SPPOL_1:37; then pion is_S-Seq by A72,JORDAN1B:8; then consider pion1 be FinSequence of TOP-REAL 2 such that A74: pion1 is_sequence_on Ga and A75: pion1 is_S-Seq and A76: L~pion = L~pion1 and A77: pion/.1 = pion1/.1 and A78: pion/.len pion = pion1/.len pion1 and A79: len pion <= len pion1 by A71,GOBOARD3:2; reconsider pion1 as being_S-Seq FinSequence of TOP-REAL 2 by A75; set godo = go^'pion1^'do; len Cage(C,n) > 4 by GOBOARD7:36; then A80: 1+1 <= len Cage(C,n) by AXIOMS:22; then A81: 1+1 <= len Rotate(Cage(C,n),Wmin) by REVROT_1:14; len (go^'pion1) >= len go by TOPREAL8:7; then A82: len (go^'pion1) >= 1+1 by A31,AXIOMS:22; then A83: len (go^'pion1) > 1+0 by NAT_1:38; len godo >= len (go^'pion1) by TOPREAL8:7; then A84: 1+1 <= len godo by A82,AXIOMS:22; A85: US is_sequence_on Ga by JORDAN1G:4; A86: go/.len go = pion1/.1 by A39,A77,FINSEQ_4:26; then A87: go^'pion1 is_sequence_on Ga by A33,A74,TOPREAL8:12; A88: (go^'pion1)/.len (go^'pion1) = pion/.len pion by A78,AMISTD_1:6 .= pion/.2 by FINSEQ_1:61 .= do/.1 by A40,FINSEQ_4:26; then A89: godo is_sequence_on Ga by A36,A87,TOPREAL8:12; LSeg(pion1,1) c= L~<*Gik,Gij*> by A76,TOPREAL3:26; then LSeg(pion1,1) c= LSeg(Gik,Gij) by SPPOL_2:21; then A90: LSeg(go,len go-'1) /\ LSeg(pion1,1) c= {Gik} by A42,A49,XBOOLE_1: 27; A91: len pion1 >= 1+1 by A79,FINSEQ_1:61; {Gik} c= LSeg(go,m) /\ LSeg(pion1,1) proof let x be set; assume x in {Gik}; then A92: x = Gik by TARSKI:def 1; A93: Gik in LSeg(go,m) by A46,TOPREAL1:6; Gik in LSeg(pion1,1) by A39,A86,A91,TOPREAL1:27; hence x in LSeg(go,m) /\ LSeg(pion1,1) by A92,A93,XBOOLE_0:def 3; end; then LSeg(go,len go-'1) /\ LSeg(pion1,1) = { go/.len go } by A39,A42,A90,XBOOLE_0:def 10; then A94: go^'pion1 is unfolded by A86,TOPREAL8:34; len pion1 >= 2+0 by A79,FINSEQ_1:61; then A95: len pion1-2 >= 0 by REAL_1:84; A96: len (go^'pion1)-1 >= 0 by A83,REAL_1:84; len (go^'pion1)+1-1 = len go+len pion1-1 by GRAPH_2:13; then len (go^'pion1)-1 = len go+len pion1-1-1 by XCMPLX_1:26 .= len go + len pion1-(1+1) by XCMPLX_1:36 .= len go + (len pion1-2) by XCMPLX_1:29 .= len go + (len pion1-'2) by A95,BINARITH:def 3; then A97: len (go^'pion1)-'1 = len go + (len pion1-'2) by A96,BINARITH:def 3; A98: len pion1-1 >= 1 by A91,REAL_1:84; then A99: len pion1-1 >= 0 by AXIOMS:22; then A100: len pion1-'1 = len pion1-1 by BINARITH:def 3; A101: len pion1-'2+1 = len pion1-2+1 by A95,BINARITH:def 3 .= len pion1-(2-1) by XCMPLX_1:37 .= len pion1-'1 by A99,BINARITH:def 3; len pion1-1+1 <= len pion1 by XCMPLX_1:27; then A102: len pion1-'1 < len pion1 by A100,NAT_1:38; LSeg(pion1,len pion1-'1) c= L~<*Gik,Gij*> by A76,TOPREAL3:26; then LSeg(pion1,len pion1-'1) c= LSeg(Gik,Gij) by SPPOL_2:21; then A103: LSeg(pion1,len pion1-'1) /\ LSeg(do,1) c= {Gij} by A56,XBOOLE_1: 27; {Gij} c= LSeg(pion1,len pion1-'1) /\ LSeg(do,1) proof let x be set; assume x in {Gij}; then A104: x = Gij by TARSKI:def 1; A105: Gij in LSeg(do,1) by A53,TOPREAL1:6; A106: len pion1-'1+1 = len pion1 by A100,XCMPLX_1:27; then pion1/.(len pion1-'1+1) = pion/.2 by A78,FINSEQ_1:61 .= Gij by FINSEQ_4:26; then Gij in LSeg(pion1,len pion1-'1) by A98,A100,A106,TOPREAL1:27; hence x in LSeg(pion1,len pion1-'1) /\ LSeg(do,1) by A104,A105,XBOOLE_0: def 3; end; then LSeg(pion1,len pion1-'1) /\ LSeg(do,1) = {Gij} by A103,XBOOLE_0:def 10 ; then A107: LSeg(go^'pion1,len go+(len pion1-'2)) /\ LSeg(do,1) = {(go^'pion1)/.len (go^'pion1)} by A40,A86,A88,A101,A102,TOPREAL8:31; A108: (go^'pion1) is non trivial by A82,SPPOL_1:2; A109: rng pion1 c= L~pion1 by A91,SPPOL_2:18; A110: {pion1/.1} c= L~go /\ L~pion1 proof let x be set; assume x in {pion1/.1}; then x = pion1/.1 by TARSKI:def 1; then x in rng go & x in rng pion1 by A86,FINSEQ_6:46,REVROT_1:3; hence x in L~go /\ L~pion1 by A59,A109,XBOOLE_0:def 3; end; L~go /\ L~pion1 c= {pion1/.1} proof let x be set; assume x in L~go /\ L~pion1; then x in L~go & x in L~pion1 by XBOOLE_0:def 3; then x in L~pion1 /\ L~US by A44,XBOOLE_0:def 3; hence x in {pion1/.1} by A3,A39,A76,A86,SPPOL_2:21; end; then A111: L~go /\ L~pion1 = {pion1/.1} by A110,XBOOLE_0:def 10; then A112: (go^'pion1) is s.n.c. by A86,Th54; rng go /\ rng pion1 c= {pion1/.1} by A59,A109,A111,XBOOLE_1:27; then A113: go^'pion1 is one-to-one by Th55; A114: pion/.len pion = pion/.2 by FINSEQ_1:61 .= do/.1 by A40,FINSEQ_4:26; A115: {pion1/.len pion1} c= L~do /\ L~pion1 proof let x be set; assume x in {pion1/.len pion1}; then x = pion1/.len pion1 by TARSKI:def 1; then x in rng do & x in rng pion1 by A78,A114,FINSEQ_6:46,REVROT_1:3; hence x in L~do /\ L~pion1 by A59,A109,XBOOLE_0:def 3; end; L~do /\ L~pion1 c= {pion1/.len pion1} proof let x be set; assume x in L~do /\ L~pion1; then x in L~do & x in L~pion1 by XBOOLE_0:def 3; then x in L~pion1 /\ L~LS by A51,XBOOLE_0:def 3; hence x in {pion1/.len pion1} by A4,A40,A76,A78,A114,SPPOL_2:21; end; then A116: L~do /\ L~pion1 = {pion1/.len pion1} by A115,XBOOLE_0:def 10; A117: L~(go^'pion1) /\ L~do = (L~go \/ L~pion1) /\ L~do by A86,TOPREAL8:35 .= {go/.1} \/ {do/.1} by A66,A78,A114,A116,XBOOLE_1:23 .= {(go^'pion1)/.1} \/ {do/.1} by AMISTD_1:5 .= {(go^'pion1)/.1,do/.1} by ENUMSET1:41; do/.len do = (go^'pion1)/.1 by A58,AMISTD_1:5; then reconsider godo as non constant standard special_circular_sequence by A84,A88,A89,A94,A97,A107,A108, A112,A113,A117,JORDAN8:7,8,TOPREAL8:11,33,34; A118: UA is_an_arc_of W-min C,E-max C by JORDAN6:def 8; then A119: UA is connected by JORDAN6:11; A120: W-min C in UA & E-max C in UA by A118,TOPREAL1:4; set ff = Rotate(Cage(C,n),Wmin); Wmin in rng Cage(C,n) by SPRECT_2:47; then A121: ff/.1 = Wmin by FINSEQ_6:98; A122: L~ff = L~Cage(C,n) by REVROT_1:33; then A123: (W-max L~ff)..ff > 1 by A121,SPRECT_5:23; (W-max L~ff)..ff <= (N-min L~ff)..ff by A121,A122,SPRECT_5:24; then A124: (N-min L~ff)..ff > 1 by A123,AXIOMS:22; (N-min L~ff)..ff < (N-max L~ff)..ff by A121,A122,SPRECT_5:25; then A125: (N-max L~ff)..ff > 1 by A124,AXIOMS:22; (N-max L~ff)..ff <= (E-max L~ff)..ff by A121,A122,SPRECT_5:26; then A126: Emax..ff > 1 by A122,A125,AXIOMS:22; A127: now assume A128: Gik..US <= 1; Gik..US >= 1 by A32,FINSEQ_4:31; then Gik..US = 1 by A128,AXIOMS:21; then Gik = US/.1 by A32,FINSEQ_5:41; hence contradiction by A17,A21,JORDAN1F:5; end; A129: Cage(C,n) is_sequence_on Ga by JORDAN9:def 1; then A130: ff is_sequence_on Ga by REVROT_1:34; A131: right_cell(godo,1,Ga)\L~godo c= RightComp godo by A84,A89,JORDAN9:29; A132: L~godo = L~(go^'pion1) \/ L~do by A88,TOPREAL8:35 .= L~go \/ L~pion1 \/ L~do by A86,TOPREAL8:35; L~Cage(C,n) = L~US \/ L~LS by JORDAN1E:17; then A133: L~US c= L~Cage(C,n) & L~LS c= L~Cage(C,n) by XBOOLE_1:7; then A134: L~go c= L~Cage(C,n) & L~do c= L~Cage(C,n) by A44,A51,XBOOLE_1:1; A135: W-min C in C by SPRECT_1:15; A136: L~pion = LSeg(Gik,Gij) by SPPOL_2:21; A137: now assume W-min C in L~godo; then A138: W-min C in L~go \/ L~pion1 or W-min C in L~do by A132,XBOOLE_0: def 2; per cases by A138,XBOOLE_0:def 2; suppose W-min C in L~go; then C meets L~Cage(C,n) by A134,A135,XBOOLE_0:3; hence contradiction by JORDAN10:5; suppose W-min C in L~pion1; hence contradiction by A5,A76,A120,A136,XBOOLE_0:3; suppose W-min C in L~do; then C meets L~Cage(C,n) by A134,A135,XBOOLE_0:3; hence contradiction by JORDAN10:5; end; right_cell(Rotate(Cage(C,n),Wmin),1) = right_cell(ff,1,GoB ff) by A81,JORDAN1H:29 .= right_cell(ff,1,GoB Cage(C,n)) by REVROT_1:28 .= right_cell(ff,1,Ga) by JORDAN1H:52 .= right_cell(ff-:Emax,1,Ga) by A126,A130,Th53 .= right_cell(US,1,Ga) by JORDAN1E:def 1 .= right_cell(R_Cut(US,Gik),1,Ga) by A32,A85,A127,Th52 .= right_cell(go^'pion1,1,Ga) by A37,A87,Th51 .= right_cell(godo,1,Ga) by A83,A89,Th51; then W-min C in right_cell(godo,1,Ga) by JORDAN1I:8; then A139: W-min C in right_cell(godo,1,Ga)\L~godo by A137,XBOOLE_0:def 4; A140: godo/.1 = (go^'pion1)/.1 by AMISTD_1:5 .= Wmin by A57,AMISTD_1:5; A141: len US >= 2 by A16,AXIOMS:22; A142: godo/.2 = (go^'pion1)/.2 by A82,AMISTD_1:9 .= US/.2 by A31,A70,AMISTD_1:9 .= (US^'LS)/.2 by A141,AMISTD_1:9 .= Rotate(Cage(C,n),Wmin)/.2 by JORDAN1E:15; A143: L~go \/ L~do is compact by COMPTS_1:19; A144: L~go \/ L~do c= L~Cage(C,n) by A134,XBOOLE_1:8; Wmin in rng go by A57,FINSEQ_6:46; then Wmin in L~go \/ L~do by A59,XBOOLE_0:def 2; then A145: W-min (L~go \/ L~do) = Wmin by A143,A144,Th21; A146: (W-min (L~go \/ L~do))`1 = W-bound (L~go \/ L~do) & Wmin`1 = Wbo by PSCOMP_1:84; W-bound LSeg(Gik,Gij) = Gik`1 by A73,SPRECT_1:62; then A147: W-bound L~pion1 = Gik`1 by A76,SPPOL_2:21; Gik`1 >= Wbo by A7,A133,PSCOMP_1:71; then Gik`1 > Wbo by A69,REAL_1:def 5; then W-min (L~go\/L~do\/L~pion1) = W-min (L~go \/ L~do) by A143,A145,A146,A147,Th33; then A148: W-min L~godo = Wmin by A132,A145,XBOOLE_1:4; A149: rng godo c= L~godo by A84,SPPOL_2:18; 2 in dom godo by A84,FINSEQ_3:27; then A150: godo/.2 in rng godo by PARTFUN2:4; godo/.2 in W-most L~Cage(C,n) by A142,JORDAN1I:27; then (godo/.2)`1 = (W-min L~godo)`1 by A148,PSCOMP_1:88 .= W-bound L~godo by PSCOMP_1:84; then godo/.2 in W-most L~godo by A149,A150,SPRECT_2:16; then Rotate(godo,W-min L~godo)/.2 in W-most L~godo by A140,A148,FINSEQ_6:95 ; then reconsider godo as clockwise_oriented non constant standard special_circular_sequence by JORDAN1I:27; len US in dom US by FINSEQ_5:6; then A151: US.len US = US/.len US by FINSEQ_4:def 4 .= Emax by JORDAN1F:7; A152: E-max C in E-most C by PSCOMP_1:111; A153: east_halfline E-max C misses L~go proof assume east_halfline E-max C meets L~go; then consider p be set such that A154: p in east_halfline E-max C and A155: p in L~go by XBOOLE_0:3; reconsider p as Point of TOP-REAL 2 by A154; p in L~US by A44,A155; then p in east_halfline E-max C /\ L~Cage(C,n) by A133,A154,XBOOLE_0:def 3 ; then A156: p`1 = Ebo by A152,JORDAN1A:104; then A157: p = Emax by A44,A155,Th46; then Emax = Gik by A7,A151,A155,Th43; then Gik`1 = Ga*(len Ga,k)`1 by A10,A15,A156,A157,JORDAN1A:92; hence contradiction by A1,A12,A28,JORDAN1G:7; end; now assume east_halfline E-max C meets L~godo; then A158: east_halfline E-max C meets (L~go \/ L~pion1) or east_halfline E-max C meets L~do by A132,XBOOLE_1:70; per cases by A158,XBOOLE_1:70; suppose east_halfline E-max C meets L~go; hence contradiction by A153; suppose east_halfline E-max C meets L~pion1; then consider p be set such that A159: p in east_halfline E-max C and A160: p in L~pion1 by XBOOLE_0:3; reconsider p as Point of TOP-REAL 2 by A159; A161: p`1 = Gik`1 by A73,A76,A136,A160,GOBOARD7:5; i+1 <= len Ga by A1,NAT_1:38; then i+1-1 <= len Ga-1 by REAL_1:49; then A162: i <= len Ga-1 by XCMPLX_1:26; then len Ga-1 > 0 by A1,AXIOMS:22; then A163: i <= len Ga-'1 by A162,BINARITH:def 3; len Ga-'1 <= len Ga by GOBOARD9:2; then p`1 <= Ga*(len Ga-'1,1)`1 by A1,A10,A15,A19,A161,A163,JORDAN1A:39; then p`1 <= E-bound C by A19,JORDAN8:15; then A164: p`1 <= (E-max C)`1 by PSCOMP_1:104; p`1 >= (E-max C)`1 by A159,JORDAN1A:def 3; then A165: p`1 = (E-max C)`1 by A164,AXIOMS:21; p`2 = (E-max C)`2 by A159,JORDAN1A:def 3; then p = E-max C by A165,TOPREAL3:11; hence contradiction by A5,A76,A120,A136,A160,XBOOLE_0:3; suppose east_halfline E-max C meets L~do; then consider p be set such that A166: p in east_halfline E-max C and A167: p in L~do by XBOOLE_0:3; reconsider p as Point of TOP-REAL 2 by A166; p in L~LS by A51,A167; then p in east_halfline E-max C /\ L~Cage(C,n) by A133,A166,XBOOLE_0:def 3; then A168: p`1 = Ebo by A152,JORDAN1A:104; A169: (E-max C)`2 = p`2 by A166,JORDAN1A:def 3; set RC = Rotate(Cage(C,n),Emax); A170: E-max C in right_cell(RC,1) by JORDAN1I:9; A171: 1+1 <= len LS by A22,AXIOMS:22; LS = RC-:Wmin by JORDAN1G:26; then A172: LSeg(LS,1) = LSeg(RC,1) by A171,SPPOL_2:9; A173: L~RC = L~Cage(C,n) by REVROT_1:33; A174: len RC = len Cage(C,n) by REVROT_1:14; A175: GoB RC = GoB Cage(C,n) by REVROT_1:28 .= Ga by JORDAN1H:52; A176: Emax in rng Cage(C,n) by SPRECT_2:50; A177: RC is_sequence_on Ga by A129,REVROT_1:34; A178: RC/.1 = E-max L~RC by A173,A176,FINSEQ_6:98; then consider ii,jj be Nat such that A179: [ii,jj+1] in Indices Ga and A180: [ii,jj] in Indices Ga and A181: RC/.1 = Ga*(ii,jj+1) and A182: RC/.(1+1) = Ga*(ii,jj) by A80,A174,A177,JORDAN1I:25; consider jj2 be Nat such that A183: 1 <= jj2 & jj2 <= width Ga and A184: Emax = Ga*(len Ga,jj2) by JORDAN1D:29; A185: len Ga >= 4 by JORDAN8:13; then len Ga >= 1 by AXIOMS:22; then [len Ga,jj2] in Indices Ga by A183,GOBOARD7:10; then A186: ii = len Ga by A173,A178,A179,A181,A184,GOBOARD1:21; A187: 1 <= ii & ii <= len Ga & 1 <= jj+1 & jj+1 <= width Ga by A179,GOBOARD5:1; A188: 1 <= ii & ii <= len Ga & 1 <= jj & jj <= width Ga by A180,GOBOARD5:1; A189: ii+1 <> ii by NAT_1:38; jj+1 > jj by NAT_1:38; then jj+1+1 <> jj by NAT_1:38; then A190: right_cell(RC,1) = cell(Ga,ii-'1,jj) by A80,A174,A175,A179,A180,A181,A182,A189,GOBOARD5: def 6; A191: ii-'1+1 = ii by A187,AMI_5:4; A192: ii-1 >= 4-1 by A185,A186,REAL_1:49; then A193: ii-1 >= 1 by AXIOMS:22; ii-1 >= 0 by A192,AXIOMS:22; then A194: 1 <= ii-'1 by A193,BINARITH:def 3; then A195: Ga*(ii-'1,jj)`1 <= (E-max C)`1 & (E-max C)`1 <= Ga*(ii-'1+1, jj)`1 & Ga*(ii-'1,jj)`2 <= (E-max C)`2 & (E-max C)`2 <= Ga*(ii-'1,jj+1)`2 by A170,A187,A188,A190,A191,JORDAN9:19; A196: ii-'1 < len Ga by A187,A191,NAT_1:38; then A197: Ga*(ii-'1,jj)`2 = Ga*(1,jj)`2 by A188,A194,GOBOARD5:2 .= Ga*(ii,jj)`2 by A188,GOBOARD5:2; A198: Ga*(ii-'1,jj+1)`2 = Ga*(1,jj+1)`2 by A187,A194,A196,GOBOARD5:2 .= Ga*(ii,jj+1)`2 by A187,GOBOARD5:2; Ga*(len Ga,jj)`1 = Ebo & Ebo = Ga*(len Ga,jj+1)`1 by A15,A187,A188,JORDAN1A:92; then p in LSeg(RC/.1,RC/.(1+1)) by A168,A169,A181,A182,A186,A195,A197,A198, GOBOARD7:8; then A199: p in LSeg(LS,1) by A80,A172,A174,TOPREAL1:def 5; A200: p in LSeg(do,Index(p,do)) by A167,JORDAN3:42; A201: do = mid(LS,Gij..LS,len LS) by A35,Th37; A202: 1<=Gij..LS & Gij..LS<=len LS by A35,FINSEQ_4:31; Gij..LS <> len LS by A27,A35,FINSEQ_4:29; then A203: Gij..LS < len LS by A202,REAL_1:def 5; A204: 1<=Index(p,do) & Index(p,do) < len do by A167,JORDAN3:41; A205: Index(Gij,LS)+1 = Gij..LS by A30,A35,Th56; consider t be Nat such that A206: t in dom LS and A207: LS.t = Gij by A35,FINSEQ_2:11; A208: 1 <= t & t <= len LS by A206,FINSEQ_3:27; then 1 < t by A30,A207,REAL_1:def 5; then Index(Gij,LS)+1 = t by A207,A208,JORDAN3:45; then A209: len L_Cut(LS,Gij) = len LS-Index(Gij,LS) by A6,A27,A207,JORDAN3:61; set tt = Index(p,do)+(Gij..LS)-'1; A210: 1<=Index(Gij,LS) & 0+Index(Gij,LS) < len LS by A6,JORDAN3:41; then A211: len LS-Index(Gij,LS) > 0 by REAL_1:86; then Index(p,do) < len LS-'Index(Gij,LS) by A204,A209,BINARITH:def 3; then Index(p,do)+1 <= len LS-'Index(Gij,LS) by NAT_1:38; then Index(p,do) <= len LS-'Index(Gij,LS)-1 by REAL_1:84; then Index(p,do) <= len LS-Index(Gij,LS)-1 by A211,BINARITH:def 3; then A212: Index(p,do) <= len LS-Gij..LS by A205,XCMPLX_1:36; then len LS-Gij..LS >= 1 by A204,AXIOMS:22; then len LS-Gij..LS >= 0 by AXIOMS:22; then Index(p,do) <= len LS-'Gij..LS by A212,BINARITH:def 3; then Index(p,do) < len LS-'(Gij..LS)+1 by NAT_1:38; then A213: LSeg(mid(LS,Gij..LS,len LS),Index(p,do)) = LSeg(LS,Index(p,do)+(Gij..LS)-'1) by A202,A203,A204,JORDAN4:31; A214: 1+1 <= Gij..LS by A205,A210,REAL_1:55; then Index(p,do)+Gij..LS >= 1+1+1 by A204,REAL_1:55; then A215: Index(p,do)+Gij..LS-1 >= 1+1+1-1 by REAL_1:49; then A216: Index(p,do)+Gij..LS-1 >= 0 by AXIOMS:22; then A217: tt >= 1+1 by A215,BINARITH:def 3; A218: 2 in dom LS by A171,FINSEQ_3:27; now per cases by A217,REAL_1:def 5; suppose tt > 1+1; then LSeg(LS,1) misses LSeg(LS,tt) by TOPREAL1:def 9; hence contradiction by A199,A200,A201,A213,XBOOLE_0:3; suppose A219: tt = 1+1; then LSeg(LS,1) /\ LSeg(LS,tt) = {LS/.2} by A22,TOPREAL1:def 8; then p in {LS/.2} by A199,A200,A201,A213,XBOOLE_0:def 3; then A220: p = LS/.2 by TARSKI:def 1; then A221: p..LS = 2 by A218,FINSEQ_5:44; 1+1 = Index(p,do)+(Gij..LS)-1 by A216,A219,BINARITH:def 3; then 1+1+1 = Index(p,do)+(Gij..LS) by XCMPLX_1:27; then A222: Gij..LS = 2 by A204,A214,JORDAN1E:10; p in rng LS by A218,A220,PARTFUN2:4; then p = Gij by A35,A221,A222,FINSEQ_5:10; then Gij`1 = Ebo by A220,JORDAN1G:40; then Gij`1 = Ga*(len Ga,j)`1 by A9,A15,JORDAN1A:92; hence contradiction by A1,A11,A62,JORDAN1G:7; end; hence contradiction; end; then east_halfline E-max C c= (L~godo)` by SUBSET_1:43; then consider W be Subset of TOP-REAL 2 such that A223: W is_a_component_of (L~godo)` and A224: east_halfline E-max C c= W by GOBOARD9:5; east_halfline E-max C is not Bounded by JORDAN1C:9; then W is not Bounded by A224,JORDAN2C:16; then W is_outside_component_of L~godo by A223,JORDAN2C:def 4; then W c= UBD L~godo by JORDAN2C:27; then A225: east_halfline E-max C c= UBD L~godo by A224,XBOOLE_1:1; E-max C in east_halfline E-max C by JORDAN1C:7; then E-max C in UBD L~godo by A225; then E-max C in LeftComp godo by GOBRD14:46; then UA meets L~godo by A119,A120,A131,A139,Th36; then A226: UA meets (L~go \/ L~pion1) or UA meets L~do by A132,XBOOLE_1:70; A227: UA c= C by JORDAN1A:16; per cases by A226,XBOOLE_1:70; suppose UA meets L~go; then UA meets L~Cage(C,n) by A134,XBOOLE_1:63; then C meets L~Cage(C,n) by A227,XBOOLE_1:63; hence contradiction by JORDAN10:5; suppose UA meets L~pion1; hence contradiction by A5,A76,A136; suppose UA meets L~do; then UA meets L~Cage(C,n) by A134,XBOOLE_1:63; then C meets L~Cage(C,n) by A227,XBOOLE_1:63; hence contradiction by JORDAN10:5; end; theorem Th60: for C be Simple_closed_curve for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) = {Gauge(C,n)*(i,k)} & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) = {Gauge(C,n)*(i,j)} holds LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C proof let C be Simple_closed_curve; let i,j,k be Nat; assume that A1: 1 < i & i < len Gauge(C,n) and A2: 1 <= j & j <= k & k <= width Gauge(C,n) and A3: n > 0 and A4: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) = {Gauge(C,n)*(i,k)} and A5: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) = {Gauge(C,n)*(i,j)}; A6: L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) by A3,JORDAN1G:63; L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) by A3,JORDAN1G:64; hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C by A1,A2,A4,A5,A6,Th58; end; theorem Th61: for C be Simple_closed_curve for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) = {Gauge(C,n)*(i,k)} & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) = {Gauge(C,n)*(i,j)} holds LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C proof let C be Simple_closed_curve; let i,j,k be Nat; assume that A1: 1 < i & i < len Gauge(C,n) and A2: 1 <= j & j <= k & k <= width Gauge(C,n) and A3: n > 0 and A4: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) = {Gauge(C,n)*(i,k)} and A5: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) = {Gauge(C,n)*(i,j)}; A6: L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) by A3,JORDAN1G:63; L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) by A3,JORDAN1G:64; hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C by A1,A2,A4,A5,A6,Th59; end; theorem for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for j be Nat holds Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Upper_Arc L~Cage(C,n+1) & 1 <= j & j <= width Gauge(C,n+1) implies LSeg(Gauge(C,1)*(Center Gauge(C,1),1),Gauge(C,n+1)*(Center Gauge(C,n+1),j)) meets Lower_Arc L~Cage(C,n+1) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let j be Nat; assume that A1: Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Upper_Arc L~Cage(C,n+1) and A2: 1 <= j & j <= width Gauge(C,n+1); set in1 = Center Gauge(C,n+1); A3: n+1 >= 0+1 by NAT_1:29; then A4: n+1 > 0 by NAT_1:38; A5: 1 <= in1 by JORDAN1B:12; A6: in1 <= len Gauge(C,n+1) by JORDAN1B:14; A7: LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),1), Gauge(C,n+1)*(Center Gauge(C,n+1),j)) c= LSeg(Gauge(C,1)*(Center Gauge(C,1),1), Gauge(C,n+1)*(Center Gauge(C,n+1),j)) by A2,A3,JORDAN1A:66; Upper_Arc L~Cage(C,n+1) c= L~Cage(C,n+1) by JORDAN1A:16; then LSeg(Gauge(C,n+1)*(in1,1),Gauge(C,n+1)*(in1,j)) meets Lower_Arc L~Cage(C,n+1) by A1,A2,A4,A5,A6,JORDAN1G:65; hence thesis by A7,XBOOLE_1:63; end; theorem for C be Simple_closed_curve for j,k be Nat holds 1 <= j & j <= k & k <= width Gauge(C,n+1) & LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Upper_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*(Center Gauge(C,n+1),k)} & LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Lower_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*(Center Gauge(C,n+1),j)} implies LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Lower_Arc C proof let C be Simple_closed_curve; let j,k be Nat; assume that A1: 1 <= j & j <= k & k <= width Gauge(C,n+1) and A2: LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Upper_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*(Center Gauge(C,n+1),k)} and A3: LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Lower_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*(Center Gauge(C,n+1),j)}; n+1 >= 0+1 by NAT_1:29; then A4: n+1 > 0 by NAT_1:38; A5: len Gauge(C,n+1) >= 4 by JORDAN8:13; then A6: len Gauge(C,n+1) >= 3 by AXIOMS:22; len Gauge(C,n+1) >= 2 by A5,AXIOMS:22; then A7: 1 < Center Gauge(C,n+1) by JORDAN1B:15; Center Gauge(C,n+1) < len Gauge(C,n+1) by A6,JORDAN1B:16; hence LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Lower_Arc C by A1,A2,A3,A4,A7,Th60; end; theorem for C be Simple_closed_curve for j,k be Nat holds 1 <= j & j <= k & k <= width Gauge(C,n+1) & LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Upper_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*(Center Gauge(C,n+1),k)} & LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Lower_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*(Center Gauge(C,n+1),j)} implies LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Upper_Arc C proof let C be Simple_closed_curve; let j,k be Nat; assume that A1: 1 <= j & j <= k & k <= width Gauge(C,n+1) and A2: LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Upper_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*(Center Gauge(C,n+1),k)} and A3: LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Lower_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*(Center Gauge(C,n+1),j)}; n+1 >= 0+1 by NAT_1:29; then A4: n+1 > 0 by NAT_1:38; A5: len Gauge(C,n+1) >= 4 by JORDAN8:13; then A6: len Gauge(C,n+1) >= 3 by AXIOMS:22; len Gauge(C,n+1) >= 2 by A5,AXIOMS:22; then A7: 1 < Center Gauge(C,n+1) by JORDAN1B:15; Center Gauge(C,n+1) < len Gauge(C,n+1) by A6,JORDAN1B:16; hence LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Upper_Arc C by A1,A2,A3,A4,A7,Th61; end;

Back to top