### The Mizar article:

### More on External Approximation of a Continuum

**by****Andrzej Trybulec**

- Received October 7, 2001
Copyright (c) 2001 Association of Mizar Users

- MML identifier: JORDAN1H
- [ MML identifier index ]

environ vocabulary COMPTS_1, SPPOL_1, EUCLID, FINSEQ_1, GOBOARD1, PRE_TOPC, BOOLE, ARYTM_3, RELAT_1, RELAT_2, TRIANG_1, ZF_REFLE, AMI_1, PRALG_1, FUNCT_1, FUNCT_6, ORDINAL2, TOPREAL1, JORDAN1, PCOMPS_1, METRIC_1, SQUARE_1, ARYTM_1, FINSEQ_2, COMPLEX1, ABSVALUE, ORDERS_1, ORDERS_2, FINSET_1, FINSEQ_4, GOBOARD2, CARD_1, FUNCT_5, MCART_1, GOBRD13, TARSKI, PROB_1, MATRIX_1, TREES_1, INCSP_1, GOBOARD5, SEQM_3, CONNSP_1, SUBSET_1, GOBOARD9, TOPS_1, JORDAN3, RFINSEQ, FINSEQ_5, JORDAN8, INT_1, GROUP_1, PSCOMP_1, JORDAN2C, FINSEQ_6, SPRECT_2, JORDAN9, JORDAN1A, JORDAN1H, ARYTM, PARTFUN1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSEQ_6, RVSUM_1, GOBOARD5, STRUCT_0, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, NAT_1, INT_1, BINARITH, ABSVALUE, RELAT_1, RELAT_2, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, CARD_1, CARD_4, FINSET_1, FINSEQ_1, FUNCT_6, PROB_1, PRALG_1, FINSEQ_2, FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_1, METRIC_1, ORDERS_1, ORDERS_2, TRIANG_1, PRE_TOPC, TOPS_1, COMPTS_1, CONNSP_1, PCOMPS_1, EUCLID, JORDAN1, SPRECT_2, TOPREAL1, GOBOARD1, GOBOARD2, JORDAN3, JORDAN2C, SPPOL_1, PSCOMP_1, GOBOARD9, JORDAN8, GOBRD13, JORDAN9, JORDAN1A; constructors REAL_1, CARD_4, RFINSEQ, BINARITH, TOPS_1, CONNSP_1, PSCOMP_1, GOBOARD9, JORDAN8, GOBRD13, GROUP_1, JORDAN9, GOBOARD2, TRIANG_1, ORDERS_2, AMI_1, JORDAN1, PRALG_1, MATRLIN, JORDAN3, JORDAN2C, SQUARE_1, WSIERP_1, JORDAN1A, TOPREAL4, SPRECT_1, PROB_1; clusters PSCOMP_1, RELSET_1, FINSEQ_1, FINSEQ_5, REVROT_1, XREAL_0, GOBOARD9, JORDAN8, GOBRD13, EUCLID, FINSET_1, POLYNOM1, WAYBEL_2, GOBOARD1, PRELAMB, TRIANG_1, PUA2MSS1, MSAFREE1, FUNCT_7, PRALG_1, GENEALG1, GOBOARD2, SPRECT_3, TOPREAL6, INT_1, BORSUK_2, SPRECT_4, SPRECT_1, MEMBERED, RELAT_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions GOBOARD1, TARSKI, RELSET_1, RELAT_2, ORDERS_2, FUNCT_1, JORDAN1, RELAT_1, XBOOLE_0; theorems JORDAN9, GOBOARD5, TOPREAL1, GOBOARD7, AXIOMS, GOBOARD1, SPRECT_2, GOBOARD2, FINSEQ_4, TRIANG_1, ORDERS_2, CARD_2, PRE_CIRC, CARD_1, FINSEQ_3, FUNCT_2, GOBRD13, PSCOMP_1, FINSEQ_1, FUNCT_1, MATRIX_1, RELAT_1, RLVECT_1, EUCLID, NAT_1, SUBSET_1, GOBRD11, JORDAN1D, ZFMISC_1, RELSET_1, FUNCT_7, TARSKI, UNIALG_1, PROB_1, EXTENS_1, FUNCT_6, JORDAN3, JORDAN4, JORDAN8, TOPREAL3, GOBRD14, GOBOARD9, SPRECT_4, GOBRD12, SPPOL_2, REAL_1, PRE_TOPC, AMI_5, TOPS_1, SPRECT_3, JORDAN1A, TSEP_1, INT_1, REAL_2, HEINE, NEWTON, JORDAN5B, JORDAN2C, JORDAN1, TOPMETR, SUB_METR, SQUARE_1, RVSUM_1, ABSVALUE, METRIC_1, JORDAN1B, CQC_THE1, BINARITH, SCMFSA_7, POLYNOM4, SPRECT_1, FINSEQ_2, JORDAN10, SPPOL_1, CONNSP_1, REVROT_1, PCOMPS_2, XBOOLE_0, XBOOLE_1, XREAL_0, PARTIT_2, XCMPLX_0, XCMPLX_1, PARTFUN1, RELAT_2; schemes FINSEQ_1, FINSEQ_2, NAT_1; begin :: Preliminaries reserve m,k,j,j1,i,i1,i2,n for Nat, r,s for Real, C for compact non vertical non horizontal Subset of TOP-REAL 2, G for Go-board, p for Point of TOP-REAL 2; definition cluster with_non-empty_element set; existence proof consider X being with_non-empty_element set; take X; thus thesis; end; end; definition let D be non empty with_non-empty_element set; cluster non empty non-empty FinSequence of D*; existence proof consider X being non empty set such that A1: X in D by TRIANG_1:def 1; A2: rng<*<*X*>*> = {<*X*>} by FINSEQ_1:56; <*X*> in D* by A1,FUNCT_7:20; then rng<*<*X*>*> c= D* by A2,ZFMISC_1:37; then reconsider F = <*<*X*>*> as FinSequence of D* by FINSEQ_1:def 4; take F; thus F is non empty; assume {} in rng F; hence thesis by A2,TARSKI:def 1; end; end; definition let D be non empty with_non-empty_elements set; cluster non empty non-empty FinSequence of D*; existence proof consider X being Element of D; A1: rng<*<*X*>*> = {<*X*>} by FINSEQ_1:56; <*X*> in D* by FUNCT_7:20; then rng<*<*X*>*> c= D* by A1,ZFMISC_1:37; then reconsider F = <*<*X*>*> as FinSequence of D* by FINSEQ_1:def 4; take F; thus F is non empty; assume {} in rng F; hence thesis by A1,TARSKI:def 1; end; end; definition let F be non-empty Function-yielding Function; cluster rngs F -> non-empty; coherence proof now let n be set; assume n in dom rngs F; then A1: n in dom F by EXTENS_1:4; then A2: (rngs F).n = rng(F.n) by FUNCT_6:31; F.n is non empty by A1,UNIALG_1:def 6; hence (rngs F).n is non empty by A2,RELAT_1:64; end; hence thesis by UNIALG_1:def 6; end; end; definition cluster increasing -> one-to-one FinSequence of REAL; coherence proof let f be FinSequence of REAL such that A1: f is increasing; let x1,x2 be set; assume A2: x1 in dom f & x2 in dom f; then reconsider n1=x1, n2=x2 as Nat; assume A3: f.x1 = f.x2; assume A4: not thesis; per cases by A4,AXIOMS:21; suppose n1 < n2; hence contradiction by A1,A2,A3,GOBOARD1:def 1; suppose n1 > n2; hence contradiction by A1,A2,A3,GOBOARD1:def 1; end; end; canceled 3; theorem Th4: for p,q being Point of TOP-REAL 2 holds LSeg(p,q) \ {p,q} is convex proof let p,q,w1,w2 be Point of TOP-REAL 2; set P = LSeg(p,q) \ {p,q}; assume A1: w1 in P & w2 in P; then w1 in LSeg(p,q) & w2 in LSeg(p,q) by XBOOLE_0:def 4; then A2: LSeg(w1,w2) c= LSeg(p,q) by TOPREAL1:12; not w1 in {p,q} & not w2 in {p,q} by A1,XBOOLE_0:def 4; then w1 <> p & w2 <> p & w1 <> q & w2 <> q by TARSKI:def 2; then not p in LSeg(w1,w2) & not q in LSeg(w1,w2) by A2,SPPOL_1:24; then LSeg(w1,w2) misses {p,q} by ZFMISC_1:57; hence LSeg(w1,w2) c= P by A2,XBOOLE_1:86; end; theorem for p,q being Point of TOP-REAL 2 holds LSeg(p,q) \ {p,q} is connected proof let p,q be Point of TOP-REAL 2; LSeg(p,q) \ {p,q} is convex by Th4; hence thesis by JORDAN1:9; end; theorem Th6: for p,q being Point of TOP-REAL 2 st p <> q holds p in Cl(LSeg(p,q) \ {p,q}) proof let p,q be Point of TOP-REAL 2 such that A1: p <> q; for G being Subset of TOP-REAL 2 st G is open holds p in G implies (LSeg(p,q) \ {p,q}) meets G proof let G be Subset of TOP-REAL 2 such that A2: G is open and A3: p in G; reconsider P = G as Subset of TopSpaceMetr Euclid 2 by EUCLID:def 8; reconsider x = p, y = q as Point of Euclid 2 by TOPREAL3:13; TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8; then consider r being real number such that A4: r>0 and A5: Ball(x,r) c= P by A2,A3,TOPMETR:22; reconsider r as Real by XREAL_0:def 1; set t = min(r/2,dist(x,y)/2), s = t/dist(x,y); A6: r/2 > 0 by A4,REAL_2:127; A7: 0 < dist(x,y) by A1,SUB_METR:2; then 0 < dist(x,y)/2 by REAL_2:127; then A8: 0 < t by A6,SPPOL_1:13; then A9: 0 < s by A7,REAL_2:127; A10: t <= dist(x,y)/2 by SQUARE_1:35; dist(x,y)/2 < dist(x,y)/1 by A7,REAL_2:200; then t < dist(x,y) by A10,AXIOMS:22; then A11: s < 1 by A8,REAL_2:142; set pp = (1-s)*p+s*q; reconsider z = pp as Point of Euclid 2 by TOPREAL3:13; A12: pp in LSeg(p,q) by A9,A11,SPPOL_1:22; A13: (1-s)*p+s*p = (1-s+s)*p by EUCLID:37 .= 1 * p by XCMPLX_1:27 .= p by EUCLID:33; A14: now assume pp = p; then s*p = pp - (1-s)*p by A13,EUCLID:52 .= s*q by EUCLID:52; hence contradiction by A1,A9,EUCLID:38; end; A15: (1-s)*q+s*q = (1-s+s)*q by EUCLID:37 .= 1 *q by XCMPLX_1:27 .= q by EUCLID:33; A16: 1-s <> 0 by A11,XCMPLX_1:15; now assume pp = q; then (1-s)*q = pp - s*q by A15,EUCLID:52 .= (1-s)*p by EUCLID:52; hence contradiction by A1,A16,EUCLID:38; end; then not pp in {p,q} by A14,TARSKI:def 2; then A17: pp in LSeg(p,q) \ {p,q} by A12,XBOOLE_0:def 4; reconsider x' = x, y' = y, z' = z as Element of REAL 2 by EUCLID:25; reconsider a = x', b = y' as Element of 2-tuples_on REAL by EUCLID:def 1; reconsider u = a-b, v = s*b, w = (1-s)*a as Element of REAL 2 by EUCLID:def 1; A18: (1-s)*p = (1-s)*x' by EUCLID:def 11; s*q = s*y' by EUCLID:def 11; then A19: (1-s)*p+s*q = w+v by A18,EUCLID:def 10; dist(x,z) = |.x'-z'.| by SPPOL_1:20 .= |.a-(1-s)*a-s*b.| by A19,RVSUM_1:60 .= |.1 *a-(1-s)*a-s*b.| by RVSUM_1:74 .= |.1 *a +-(1-s)*a-s*b.| by RVSUM_1:52 .= |.1 *a +(-1)*((1-s)*a)-s*b.| by RVSUM_1:76 .= |.1 *a +(-1)*(1-s)*a-s*b.| by RVSUM_1:71 .= |.1 *a + (-(1-s))*a-s*b.| by XCMPLX_1:180 .= |.(1+ (-(1-s)))*a-s*b.| by RVSUM_1:72 .= |.(1-(1-s))*a-s*b.| by XCMPLX_0:def 8 .= |.s*a-s*b.| by XCMPLX_1:18 .= |.s*a+ -s*b.| by RVSUM_1:52 .= |.s*a+ (-1)*(s*b).| by RVSUM_1:76 .= |.s*a+ (-1)*s*b.| by RVSUM_1:71 .= |.s*a+ s*((-1)*b).| by RVSUM_1:71 .= |.s*(a+ (-1)*b).| by RVSUM_1:73 .= |.s*(a+ -b).| by RVSUM_1:76 .= |.s*(a-b).| by RVSUM_1:52 .= abs(s)*|.u.| by EUCLID:14 .= s*|.a-b.| by A9,ABSVALUE:def 1 .= s*dist(x,y) by SPPOL_1:20 .= t by A7,XCMPLX_1:88; then A20: dist(x,z) <= r/2 by SQUARE_1:35; r/2 < r/1 by A4,REAL_2:200; then dist(x,z) < r by A20,AXIOMS:22; then z in Ball(x,r) by METRIC_1:12; hence (LSeg(p,q) \ {p,q}) meets G by A5,A17,XBOOLE_0:3; end; hence p in Cl(LSeg(p,q) \ {p,q}) by TOPS_1:39; end; theorem Th7: for p,q being Point of TOP-REAL 2 st p <> q holds Cl(LSeg(p,q) \ {p,q}) = LSeg(p,q) proof let p,q be Point of TOP-REAL 2 such that A1: p <> q; LSeg(p,q) \ {p,q} c= LSeg(p,q) by XBOOLE_1:36; then Cl(LSeg(p,q) \ {p,q}) c= Cl LSeg(p,q) by PRE_TOPC:49; hence Cl(LSeg(p,q) \ {p,q}) c= LSeg(p,q) by PRE_TOPC:52; let e be set; assume A2: e in LSeg(p,q); p in LSeg(p,q) & q in LSeg(p,q) by TOPREAL1:6; then {p,q} c= LSeg(p,q) by ZFMISC_1:38; then LSeg(p,q) = LSeg(p,q) \ {p,q} \/ {p,q} by XBOOLE_1:45; then A3: e in LSeg(p,q) \ {p,q} or e in {p,q} by A2,XBOOLE_0:def 2; per cases by A3,TARSKI:def 2; suppose A4: e in LSeg(p,q) \ {p,q}; LSeg(p,q) \ {p,q} c= Cl(LSeg(p,q) \ {p,q}) by PRE_TOPC:48; hence e in Cl(LSeg(p,q) \ {p,q}) by A4; suppose e = p or e = q; hence thesis by A1,Th6; end; theorem for S being Subset of TOP-REAL 2, p,q be Point of TOP-REAL 2 st p <> q & LSeg(p,q) \ {p,q} c= S holds LSeg(p,q) c= Cl S proof let S be Subset of TOP-REAL 2, p,q be Point of TOP-REAL 2 such that A1: p <> q; assume LSeg(p,q) \ {p,q} c= S; then Cl(LSeg(p,q) \ {p,q}) c= Cl S by PRE_TOPC:49; hence thesis by A1,Th7; end; begin :: Transforming Finite Sets to Finite Sequences definition func RealOrd -> Relation of REAL equals :Def1: {[r,s] : r <= s }; coherence proof set R = {[r,s] : r <= s }; let x be set; assume x in R; then ex r,s st x = [r,s] & r <= s; hence x in [:REAL,REAL:] by ZFMISC_1:106; end; end; theorem Th9: [r,s] in RealOrd implies r <= s proof hereby assume [r,s] in RealOrd; then consider r1,s1 being Real such that A1: [r,s] = [r1,s1] and A2: r1 <= s1 by Def1; r = r1 & s = s1 by A1,ZFMISC_1:33; hence r <= s by A2; end; end; Lm1: RealOrd is_reflexive_in REAL proof let x be set such that A1: x in REAL; reconsider x as Element of REAL by A1; x <= x; hence thesis by Def1; end; Lm2: RealOrd is_antisymmetric_in REAL proof let x,y be set such that A1: x in REAL & y in REAL and A2: [x,y] in RealOrd & [y,x] in RealOrd; reconsider x,y as Element of REAL by A1; x <= y & y <= x by A2,Th9; hence thesis by AXIOMS:21; end; Lm3: RealOrd is_transitive_in REAL proof let x,y,z be set such that A1: x in REAL & y in REAL & z in REAL and A2: [x,y] in RealOrd & [y,z] in RealOrd; reconsider x,y,z as Element of REAL by A1; x <= y & y <= z by A2,Th9; then x <= z by AXIOMS:22; hence thesis by Def1; end; Lm4: RealOrd is_connected_in REAL proof let x,y be set; assume x in REAL & y in REAL; then reconsider x,y as Element of REAL; x <= y or y <= x; hence thesis by Def1; end; theorem Th10: field RealOrd = REAL proof field RealOrd c= REAL \/ REAL by RELSET_1:19; hence field RealOrd c= REAL; thus REAL c= field RealOrd by Lm1,PARTIT_2:8; end; definition cluster RealOrd -> total reflexive antisymmetric transitive being_linear-order; coherence proof A1: REAL c= dom RealOrd proof let x be set such that A2: x in REAL; reconsider x as Element of REAL by A2; [x,x] in RealOrd by Def1; hence thesis by RELAT_1:def 4; end; dom RealOrd = REAL by A1,XBOOLE_0:def 10; hence RealOrd is total by PARTFUN1:def 4; RealOrd is_reflexive_in REAL by Lm1; hence RealOrd is reflexive by Th10,RELAT_2:def 9; RealOrd is_antisymmetric_in REAL by Lm2; hence RealOrd is antisymmetric by Th10,RELAT_2:def 12; RealOrd is_transitive_in REAL by Lm3; hence RealOrd is transitive by Th10,RELAT_2:def 16; thus RealOrd is_reflexive_in field RealOrd by Lm1,Th10; thus RealOrd is_transitive_in field RealOrd by Lm3,Th10; thus RealOrd is_antisymmetric_in field RealOrd by Lm2,Th10; thus RealOrd is_connected_in field RealOrd by Lm4,Th10; end; end; theorem Th11: RealOrd linearly_orders REAL proof thus RealOrd is_reflexive_in REAL by Lm1; thus RealOrd is_transitive_in REAL by Lm3; thus RealOrd is_antisymmetric_in REAL by Lm2; thus RealOrd is_connected_in REAL by Lm4; end; theorem Th12: for A being finite Subset of REAL holds SgmX(RealOrd,A) is increasing proof let A be finite Subset of REAL; set IT = SgmX(RealOrd,A); let n,m be Nat such that A1: n in dom IT and A2: m in dom IT and A3: n<m; A4: RealOrd linearly_orders A by Th11,ORDERS_2:36; then IT is one-to-one by TRIANG_1:8; then A5: IT.n <> IT.m by A1,A2,A3,FUNCT_1:def 8; IT/.n = IT.n & IT/.m = IT.m by A1,A2,FINSEQ_4:def 4; then [IT.n,IT.m] in RealOrd by A1,A2,A3,A4,TRIANG_1:def 2; then IT.n <= IT.m by Th9; hence IT.n < IT.m by A5,AXIOMS:21; end; theorem Th13: for f being FinSequence of REAL, A being finite Subset of REAL st A = rng f holds SgmX(RealOrd,A) = Incr f proof let f be FinSequence of REAL, A be finite Subset of REAL such that A1: A = rng f; A2: RealOrd linearly_orders A by Th11,ORDERS_2:36; then A3: rng SgmX(RealOrd,A) = rng f by A1,TRIANG_1:def 2; reconsider F = SgmX(RealOrd,A) as increasing FinSequence of REAL by Th12; len F = card rng f by A1,A2,TRIANG_1:9; hence thesis by A3,GOBOARD2:def 2; end; definition let A be finite Subset of REAL; cluster SgmX(RealOrd,A) -> increasing; coherence by Th12; end; canceled; theorem Th15: for X being non empty set, A being finite Subset of X, R be being_linear-order Order of X holds len SgmX(R,A) = card A proof let X being non empty set, A being finite Subset of X, R be being_linear-order Order of X; A1: field R = X by ORDERS_2:2; R linearly_orders field R by ORDERS_2:35; then R linearly_orders A by A1,ORDERS_2:36; hence thesis by TRIANG_1:9; end; begin :: On the construction of go boards theorem Th16: for f being FinSequence of TOP-REAL 2 holds X_axis f = proj1*f proof let f be FinSequence of TOP-REAL 2; reconsider pf = proj1*f as FinSequence of REAL by FINSEQ_2:36; A1: len pf = len f by FINSEQ_2:37; A2: len X_axis f = len f by GOBOARD1:def 3; then A3: dom X_axis f = dom f by FINSEQ_3:31; A4: dom X_axis f = dom pf by A1,A2,FINSEQ_3:31; for k being Nat st k in dom X_axis f holds (X_axis f).k = pf.k proof let k be Nat such that A5: k in dom X_axis f; A6: f/.k = f.k by A3,A5,FINSEQ_4:def 4; thus (X_axis f).k = (f/.k)`1 by A5,GOBOARD1:def 3 .= proj1.(f.k) by A6,PSCOMP_1:def 28 .= pf.k by A3,A5,FUNCT_1:23; end; hence X_axis f = proj1*f by A4,FINSEQ_1:17; end; theorem Th17: for f being FinSequence of TOP-REAL 2 holds Y_axis f = proj2*f proof let f be FinSequence of TOP-REAL 2; reconsider pf = proj2*f as FinSequence of REAL by FINSEQ_2:36; A1: len pf = len f by FINSEQ_2:37; A2: len Y_axis f = len f by GOBOARD1:def 4; then A3: dom Y_axis f = dom f by FINSEQ_3:31; A4: dom Y_axis f = dom pf by A1,A2,FINSEQ_3:31; for k being Nat st k in dom Y_axis f holds (Y_axis f).k = pf.k proof let k be Nat such that A5: k in dom Y_axis f; A6: f/.k = f.k by A3,A5,FINSEQ_4:def 4; thus (Y_axis f).k = (f/.k)`2 by A5,GOBOARD1:def 4 .= proj2.(f.k) by A6,PSCOMP_1:def 29 .= pf.k by A3,A5,FUNCT_1:23; end; hence Y_axis f = proj2*f by A4,FINSEQ_1:17; end; definition let D be non empty set; let M be FinSequence of D*; redefine func Values M -> Subset of D; coherence proof set A = {rng f where f is Element of D*: f in rng M}; for X being set st X in A holds X c= D proof let X be set; assume X in A; then ex f being Element of D* st X = rng f & f in rng M; hence thesis by FINSEQ_1:def 4; end; then union A c= D by ZFMISC_1:94; hence Values M is Subset of D by GOBRD13:3; end; end; definition let D be non empty with_non-empty_elements set; let M be non empty non-empty FinSequence of D*; cluster Values M -> non empty; coherence proof dom rngs M = dom M by EXTENS_1:4; then reconsider X = rng rngs M as non empty with_non-empty_elements set by RELAT_1:65; Values M = Union rngs M by GOBRD13:def 1 .= union X by PROB_1:def 3; hence thesis; end; end; theorem Th18: for D being non empty set, M being (Matrix of D), i st i in Seg width M holds rng Col(M,i) c= Values M proof let D be non empty set; let M be (Matrix of D), k such that A1: k in Seg width M; A2: Values M = { M*(i,j): [i,j] in Indices M } by GOBRD13:7; let e be set; assume e in rng Col(M,k); then consider u being set such that A3: u in dom Col(M,k) and A4: e = Col(M,k).u by FUNCT_1:def 5; reconsider u as Nat by A3; A5: len Col(M,k) = len M by MATRIX_1:def 9; then dom Col(M,k) = dom M by FINSEQ_3:31; then A6: Col(M,k).u = M*(u,k) by A3,MATRIX_1:def 9; A7: 1 <= u & u <= len M by A3,A5,FINSEQ_3:27; 1 <= k & k <= width M by A1,FINSEQ_1:3; then [u,k] in Indices M by A7,GOBOARD7:10; hence e in Values M by A2,A4,A6; end; theorem Th19: for D being non empty set, M being (Matrix of D), i st i in dom M holds rng Line(M,i) c= Values M proof let D be non empty set; let M be (Matrix of D), k such that A1: k in dom M; A2: Values M = { M*(i,j): [i,j] in Indices M } by GOBRD13:7; let e be set; assume e in rng Line(M,k); then consider u being set such that A3: u in dom Line(M,k) and A4: e = Line(M,k).u by FUNCT_1:def 5; reconsider u as Nat by A3; A5: len Line(M,k) = width M by MATRIX_1:def 8; then dom Line(M,k) = Seg width M by FINSEQ_1:def 3; then A6: Line(M,k).u = M*(k,u) by A3,MATRIX_1:def 8; A7: 1 <= k & k <= len M by A1,FINSEQ_3:27; 1 <= u & u <= width M by A3,A5,FINSEQ_3:27; then [k,u] in Indices M by A7,GOBOARD7:10; hence e in Values M by A2,A4,A6; end; theorem Th20: for G being X_increasing-in-column non empty-yielding Matrix of TOP-REAL 2 holds len G <= card(proj1.:Values G) proof let G be X_increasing-in-column non empty-yielding Matrix of TOP-REAL 2; 0 <> width G by GOBOARD1:def 5; then 1 <= width G by RLVECT_1:99; then A1: 1 in Seg width G by FINSEQ_1:3; then reconsider L = X_axis(Col(G,1)) as increasing FinSequence of REAL by GOBOARD1:def 9; A2: rng L = rng(proj1*Col(G,1)) by Th16 .= proj1.:rng Col(G,1) by RELAT_1:160; A3: card rng L= len L by FINSEQ_4:77 .= len Col(G,1) by GOBOARD1:def 3 .= len G by MATRIX_1:def 9; rng Col(G,1) c= Values G by A1,Th18; then proj1.:rng Col(G,1) c= proj1.:Values G by RELAT_1:156; hence len G <= card(proj1.:Values G) by A2,A3,CARD_1:80; end; theorem Th21: for G being X_equal-in-line Matrix of TOP-REAL 2 holds card(proj1.:Values G) <= len G proof let G be X_equal-in-line Matrix of TOP-REAL 2; deffunc F(Nat)=proj1.(G*($1,1)); consider f being FinSequence such that A1: len f = len G and A2: for k st k in Seg len G holds f.k = F(k) from SeqLambda; A3: dom f = dom G by A1,FINSEQ_3:31; proj1.:Values G c= rng f proof let y be set; assume y in proj1.:Values G; then consider x being set such that A4: x in the carrier of TOP-REAL 2 and A5: x in Values G and A6: y = proj1.x by FUNCT_2:115; Values G = { G*(i,j): [i,j] in Indices G } by GOBRD13:7; then consider i,j such that A7: x = G*(i,j) and A8: [i,j] in Indices G by A5; A9: 1 <= i & i <= len G by A8,GOBOARD5:1; then A10: i in dom G by FINSEQ_3:27; then A11: i in Seg len G by FINSEQ_1:def 3; reconsider x as Point of TOP-REAL 2 by A4; A12: 1 <= j & j <= width G by A8,GOBOARD5:1; y = x`1 by A6,PSCOMP_1:def 28 .= G*(i,1)`1 by A7,A9,A12,GOBOARD5:3 .= proj1.(G*(i,1)) by PSCOMP_1:def 28 .= f.i by A2,A11; hence thesis by A3,A10,FUNCT_1:12; end; then Card(proj1.:Values G) c= Card dom G by A3,CARD_1:28; then card(proj1.:Values G) <= card dom G by CARD_2:57; hence card(proj1.:Values G) <= len G by PRE_CIRC:21; end; theorem Th22: for G being X_equal-in-line X_increasing-in-column non empty-yielding Matrix of TOP-REAL 2 holds len G = card(proj1.:Values G) proof let G be X_equal-in-line X_increasing-in-column non empty-yielding Matrix of TOP-REAL 2; A1: len G <= card(proj1.:Values G) by Th20; card(proj1.:Values G) <= len G by Th21; hence len G = card(proj1.:Values G) by A1,AXIOMS:21; end; theorem Th23: for G being Y_increasing-in-line non empty-yielding Matrix of TOP-REAL 2 holds width G <= card(proj2.:Values G) proof let G be Y_increasing-in-line non empty-yielding Matrix of TOP-REAL 2; 0 <> len G by GOBOARD1:def 5; then 1 <= len G by RLVECT_1:99; then A1: 1 in dom G by FINSEQ_3:27; then reconsider L = Y_axis(Line(G,1)) as increasing FinSequence of REAL by GOBOARD1:def 8; A2: rng L = rng(proj2*Line(G,1)) by Th17 .= proj2.:rng Line(G,1) by RELAT_1:160; A3: card rng L= len L by FINSEQ_4:77 .= len Line(G,1) by GOBOARD1:def 4 .= width G by MATRIX_1:def 8; rng Line(G,1) c= Values G by A1,Th19; then proj2.:rng Line(G,1) c= proj2.:Values G by RELAT_1:156; hence width G <= card(proj2.:Values G) by A2,A3,CARD_1:80; end; theorem Th24: for G being Y_equal-in-column non empty-yielding Matrix of TOP-REAL 2 holds card(proj2.:Values G) <= width G proof let G be Y_equal-in-column non empty-yielding Matrix of TOP-REAL 2; deffunc F(Nat)=proj2.(G*(1,$1)); consider f being FinSequence such that A1: len f = width G and A2: for k st k in Seg width G holds f.k = F(k) from SeqLambda; A3: dom f = Seg width G by A1,FINSEQ_1:def 3; proj2.:Values G c= rng f proof let y be set; assume y in proj2.:Values G; then consider x being set such that A4: x in the carrier of TOP-REAL 2 and A5: x in Values G and A6: y = proj2.x by FUNCT_2:115; Values G = { G*(i,j): [i,j] in Indices G } by GOBRD13:7; then consider i,j such that A7: x = G*(i,j) and A8: [i,j] in Indices G by A5; A9: 1 <= j & j <= width G by A8,GOBOARD5:1; then A10: j in Seg width G by FINSEQ_1:3; reconsider x as Point of TOP-REAL 2 by A4; A11: 1 <= i & i <= len G by A8,GOBOARD5:1; y = x`2 by A6,PSCOMP_1:def 29 .= G*(1,j)`2 by A7,A9,A11,GOBOARD5:2 .= proj2.(G*(1,j)) by PSCOMP_1:def 29 .= f.j by A2,A10; hence thesis by A3,A10,FUNCT_1:12; end; then Card(proj2.:Values G) c= Card Seg width G by A3,CARD_1:28; then card(proj2.:Values G) <= card Seg width G by CARD_2:57; hence card(proj2.:Values G) <= width G by FINSEQ_1:78; end; theorem Th25: for G being Y_equal-in-column Y_increasing-in-line non empty-yielding Matrix of TOP-REAL 2 holds width G = card(proj2.:Values G) proof let G be Y_equal-in-column Y_increasing-in-line non empty-yielding Matrix of TOP-REAL 2; A1: width G <= card(proj2.:Values G) by Th23; card(proj2.:Values G) <= width G by Th24; hence width G = card(proj2.:Values G) by A1,AXIOMS:21; end; begin :: On go boards theorem for G be Go-board for f be FinSequence of TOP-REAL 2 st f is_sequence_on G for k be Nat st 1 <= k & k+1 <= len f holds LSeg(f,k) c= left_cell(f,k,G) proof let G be Go-board; let f be FinSequence of TOP-REAL 2; assume A1: f is_sequence_on G; let k be Nat; assume that A2: 1 <= k and A3: k+1 <= len f; A4: k in dom f & k+1 in dom f by A2,A3,GOBOARD2:3; then consider i1,j1 be Nat such that A5: [i1,j1] in Indices G and A6: f/.k = G*(i1,j1) by A1,GOBOARD1:def 11; consider i2,j2 be Nat such that A7: [i2,j2] in Indices G and A8: f/.(k+1) = G*(i2,j2) by A1,A4,GOBOARD1:def 11; A9: j1+1+1 = j1+(1+1) by XCMPLX_1:1; A10: i1+1+1 = i1+(1+1) by XCMPLX_1:1; A11: 1 <= i1 & i1 <= len G by A5,GOBOARD5:1; A12: 1 <= j1 & j1 <= width G by A5,GOBOARD5:1; A13: 1 <= i2 & i2 <= len G by A7,GOBOARD5:1; A14: 1 <= j2 & j2 <= width G by A7,GOBOARD5:1; left_cell(f,k,G) = left_cell(f,k,G); then A15: i1 = i2 & j1+1 = j2 & left_cell(f,k,G) = cell(G,i1-'1,j1) or i1+1 = i2 & j1 = j2 & left_cell(f,k,G) = cell(G,i1,j1) or i1 = i2+1 & j1 = j2 & left_cell(f,k,G) = cell(G,i2,j2-'1) or i1 = i2 & j1 = j2+1 & left_cell(f,k,G) = cell(G,i1,j2) by A1,A2,A3,A5,A6,A7,A8,GOBRD13:def 3; abs(i1-i2)+abs(j1-j2) = 1 by A1,A4,A5,A6,A7,A8,GOBOARD1:def 11; then A16: abs(i1-i2)=1 & j1=j2 or abs(j1-j2)=1 & i1=i2 by GOBOARD1:2; per cases by A16,GOBOARD1:1; suppose A17: i1 = i2 & j1+1 = j2; A18: i1 -' 1 + 1 = i1 by A11,AMI_5:4; then A19: i1-'1 < len G by A11,NAT_1:38; j1 < width G by A14,A17,NAT_1:38; then LSeg(f/.k,f/.(k+1)) c= cell(G,i1-'1,j1) by A6,A8,A12,A17,A18,A19,GOBOARD5:19; hence LSeg(f,k) c= left_cell(f,k,G) by A2,A3,A9,A15,A17,REAL_1:69,TOPREAL1: def 5; suppose A20: i1+1 = i2 & j1 = j2; then i1 < len G by A13,NAT_1:38; then LSeg(f/.k,f/.(k+1)) c= cell(G,i1,j1) by A6,A8,A11,A12,A20,GOBOARD5:23; hence LSeg(f,k) c= left_cell(f,k,G) by A2,A3,A10,A15,A20,REAL_1:69,TOPREAL1: def 5; suppose A21: i1 = i2+1 & j1 = j2; A22: j2 -' 1 + 1 = j2 by A14,AMI_5:4; then A23: j2 -' 1 < width G by A14,NAT_1:38; i2 < len G by A11,A21,NAT_1:38; then LSeg(f/.k,f/.(k+1)) c= cell(G,i2,j2-'1) by A6,A8,A13,A21,A22,A23,GOBOARD5:22; hence LSeg(f,k) c= left_cell(f,k,G) by A2,A3,A10,A15,A21,REAL_1:69,TOPREAL1 :def 5; suppose A24: i1 = i2 & j1 = j2+1; then j2 < width G by A12,NAT_1:38; then LSeg(f/.k,f/.(k+1)) c= left_cell(f,k,G) by A6,A8,A9,A11,A14,A15,A24, GOBOARD5:20,REAL_1:69; hence LSeg(f,k) c= left_cell(f,k,G) by A2,A3,TOPREAL1:def 5; end; theorem for f being standard special_circular_sequence st 1 <= k & k+1 <= len f holds left_cell(f,k,GoB f) = left_cell(f,k) proof let f be standard special_circular_sequence such that A1: 1 <= k and A2: k+1 <= len f; set G = GoB f; A3: f is_sequence_on GoB f by GOBOARD5:def 5; for i1,j1,i2,j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds i1 = i2 & j1+1 = j2 & left_cell(f,k) = cell(GoB f,i1-'1,j1) or i1+1 = i2 & j1 = j2 & left_cell(f,k) = cell(GoB f,i1,j1) or i1 = i2+1 & j1 = j2 & left_cell(f,k) = cell(GoB f,i2,j2-'1) or i1 = i2 & j1 = j2+1 & left_cell(f,k) = cell(GoB f,i1,j2) proof let i1,j1,i2,j2 be Nat such that A4: [i1,j1] in Indices G and A5: [i2,j2] in Indices G and A6: f/.k = G*(i1,j1) and A7: f/.(k+1) = G*(i2,j2); left_cell(f,k) = left_cell(f,k); then A8: i1 = i2 & j1+1 = j2 & left_cell(f,k) = cell(GoB f,i1-'1,j1) or i1+1 = i2 & j1 = j2 & left_cell(f,k) = cell(GoB f,i1,j1) or i1 = i2+1 & j1 = j2 & left_cell(f,k) = cell(GoB f,i2,j2-'1) or i1 = i2 & j1 = j2+1 & left_cell(f,k) = cell(GoB f,i1,j2) by A1,A2,A4,A5,A6,A7,GOBOARD5:def 7; A9: j1+1+1 = j1+(1+1) by XCMPLX_1:1; A10: i1+1+1 = i1+(1+1) by XCMPLX_1:1; k < len f by A2,NAT_1:38; then A11: k in dom f by A1,FINSEQ_3:27; 1 <= k+1 by NAT_1:29; then k+1 in dom f by A2,FINSEQ_3:27; then abs(i1-i2)+abs(j1-j2) = 1 by A3,A4,A5,A6,A7,A11,GOBOARD1:def 11; then A12: abs(i1-i2)=1 & j1=j2 or abs(j1-j2)=1 & i1=i2 by GOBOARD1:2; per cases by A12,GOBOARD1:1; case i1 = i2 & j1+1 = j2; hence left_cell(f,k) = cell(G,i1-'1,j1) by A8,A9,REAL_1:69; case i1+1 = i2 & j1 = j2; hence left_cell(f,k) = cell(G,i1,j1) by A8,A10,REAL_1:69; case i1 = i2+1 & j1 = j2; hence left_cell(f,k) = cell(G,i2,j2-'1) by A8,A10,REAL_1:69; case i1 = i2 & j1 = j2+1; hence left_cell(f,k) = cell(G,i1,j2) by A8,A9,REAL_1:69; end; hence left_cell(f,k,GoB f) = left_cell(f,k) by A1,A2,A3,GOBRD13:def 3; end; theorem Th28: for G be Go-board for f be FinSequence of TOP-REAL 2 st f is_sequence_on G for k be Nat st 1 <= k & k+1 <= len f holds LSeg(f,k) c= right_cell(f,k,G) proof let G be Go-board; let f be FinSequence of TOP-REAL 2; assume A1: f is_sequence_on G; let k be Nat; assume that A2: 1 <= k and A3: k+1 <= len f; A4: k in dom f & k+1 in dom f by A2,A3,GOBOARD2:3; then consider i1,j1 be Nat such that A5: [i1,j1] in Indices G and A6: f/.k = G*(i1,j1) by A1,GOBOARD1:def 11; consider i2,j2 be Nat such that A7: [i2,j2] in Indices G and A8: f/.(k+1) = G*(i2,j2) by A1,A4,GOBOARD1:def 11; A9: j1+1+1 = j1+(1+1) by XCMPLX_1:1; A10: i1+1+1 = i1+(1+1) by XCMPLX_1:1; A11: 1 <= i1 & i1 <= len G by A5,GOBOARD5:1; A12: 1 <= j1 & j1 <= width G by A5,GOBOARD5:1; A13: 1 <= i2 & i2 <= len G by A7,GOBOARD5:1; A14: 1 <= j2 & j2 <= width G by A7,GOBOARD5:1; right_cell(f,k,G) = right_cell(f,k,G); then A15: i1 = i2 & j1+1 = j2 & right_cell(f,k,G) = cell(G,i1,j1) or i1+1 = i2 & j1 = j2 & right_cell(f,k,G) = cell(G,i1,j1-'1) or i1 = i2+1 & j1 = j2 & right_cell(f,k,G) = cell(G,i2,j2) or i1 = i2 & j1 = j2+1 & right_cell(f,k,G) = cell(G,i1-'1,j2) by A1,A2,A3,A5,A6,A7,A8,GOBRD13:def 2; abs(i1-i2)+abs(j1-j2) = 1 by A1,A4,A5,A6,A7,A8,GOBOARD1:def 11; then A16: abs(i1-i2)=1 & j1=j2 or abs(j1-j2)=1 & i1=i2 by GOBOARD1:2; per cases by A16,GOBOARD1:1; suppose A17: i1 = i2 & j1+1 = j2; then j1 < width G by A14,NAT_1:38; then LSeg(f/.k,f/.(k+1)) c= cell(G,i1,j1) by A6,A8,A11,A12,A17,GOBOARD5:20; hence LSeg(f,k) c= right_cell(f,k,G) by A2,A3,A9,A15,A17,REAL_1:69,TOPREAL1 :def 5; suppose A18: i1+1 = i2 & j1 = j2; A19: j1 -' 1 + 1 = j1 by A12,AMI_5:4; then A20: j1-'1 < width G by A12,NAT_1:38; i1 < len G by A13,A18,NAT_1:38; then LSeg(f/.k,f/.(k+1)) c= cell(G,i1,j1-'1) by A6,A8,A11,A18,A19,A20,GOBOARD5:22; hence LSeg(f,k) c= right_cell(f,k,G) by A2,A3,A10,A15,A18,REAL_1:69, TOPREAL1:def 5; suppose A21: i1 = i2+1 & j1 = j2; then i2 < len G by A11,NAT_1:38; then LSeg(f/.k,f/.(k+1)) c= cell(G,i2,j2) by A6,A8,A13,A14,A21,GOBOARD5:23; hence LSeg(f,k) c= right_cell(f,k,G) by A2,A3,A10,A15,A21,REAL_1:69, TOPREAL1:def 5; suppose A22: i1 = i2 & j1 = j2+1; A23: i1 -' 1 + 1 = i1 by A11,AMI_5:4; then A24: i1-'1 < len G by A11,NAT_1:38; j2 < width G by A12,A22,NAT_1:38; then LSeg(f/.k,f/.(k+1)) c= right_cell(f,k,G) by A6,A8,A9,A14,A15,A22,A23,A24,GOBOARD5:19, REAL_1:69; hence LSeg(f,k) c= right_cell(f,k,G) by A2,A3,TOPREAL1:def 5; end; theorem Th29: for f being standard special_circular_sequence st 1 <= k & k+1 <= len f holds right_cell(f,k,GoB f) = right_cell(f,k) proof let f be standard special_circular_sequence such that A1: 1 <= k and A2: k+1 <= len f; set G = GoB f; A3: f is_sequence_on GoB f by GOBOARD5:def 5; for i1,j1,i2,j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds i1 = i2 & j1+1 = j2 & right_cell(f,k) = cell(G,i1,j1) or i1+1 = i2 & j1 = j2 & right_cell(f,k) = cell(G,i1,j1-'1) or i1 = i2+1 & j1 = j2 & right_cell(f,k) = cell(G,i2,j2) or i1 = i2 & j1 = j2+1 & right_cell(f,k) = cell(G,i1-'1,j2) proof let i1,j1,i2,j2 be Nat such that A4: [i1,j1] in Indices G and A5: [i2,j2] in Indices G and A6: f/.k = G*(i1,j1) and A7: f/.(k+1) = G*(i2,j2); set IT = right_cell(f,k); right_cell(f,k) = right_cell(f,k); then A8: i1 = i2 & j1+1 = j2 & IT = cell(GoB f,i1,j1) or i1+1 = i2 & j1 = j2 & IT = cell(GoB f,i1,j1-'1) or i1 = i2+1 & j1 = j2 & IT = cell(GoB f,i2,j2) or i1 = i2 & j1 = j2+1 & IT = cell(GoB f,i1-'1,j2) by A1,A2,A4,A5,A6,A7,GOBOARD5:def 6; A9: j1+1+1 = j1+(1+1) by XCMPLX_1:1; A10: i1+1+1 = i1+(1+1) by XCMPLX_1:1; k < len f by A2,NAT_1:38; then A11: k in dom f by A1,FINSEQ_3:27; 1 <= k+1 by NAT_1:29; then k+1 in dom f by A2,FINSEQ_3:27; then abs(i1-i2)+abs(j1-j2) = 1 by A3,A4,A5,A6,A7,A11,GOBOARD1:def 11; then A12: abs(i1-i2)=1 & j1=j2 or abs(j1-j2)=1 & i1=i2 by GOBOARD1:2; per cases by A12,GOBOARD1:1; case i1 = i2 & j1+1 = j2; hence right_cell(f,k) = cell(G,i1,j1) by A8,A9,REAL_1:69; case i1+1 = i2 & j1 = j2; hence right_cell(f,k) = cell(G,i1,j1-'1) by A8,A10,REAL_1:69; case i1 = i2+1 & j1 = j2; hence right_cell(f,k) = cell(G,i2,j2) by A8,A10,REAL_1:69; case i1 = i2 & j1 = j2+1; hence right_cell(f,k) = cell(G,i1-'1,j2) by A8,A9,REAL_1:69; end; hence right_cell(f,k,GoB f) = right_cell(f,k) by A1,A2,A3,GOBRD13:def 2; end; theorem for P being Subset of TOP-REAL 2, f being non constant standard special_circular_sequence st P is_a_component_of (L~f)` holds P = RightComp f or P = LeftComp f proof let P be Subset of TOP-REAL 2, f be non constant standard special_circular_sequence; assume P is_a_component_of (L~f)`; then ex B1 being Subset of (TOP-REAL 2)|(L~f)` st B1 = P & B1 is_a_component_of (TOP-REAL 2)|(L~f)` by CONNSP_1:def 6; hence P = RightComp f or P = LeftComp f by GOBRD14:22; end; theorem for f being non constant standard special_circular_sequence st f is_sequence_on G for k st 1 <= k & k+1 <= len f holds Int right_cell(f,k,G) c= RightComp f & Int left_cell(f,k,G) c= LeftComp f proof let f be non constant standard special_circular_sequence such that A1: f is_sequence_on G; let k such that A2: 1 <= k & k+1 <= len f; A3: Int right_cell(f,k,G) c= right_cell(f,k,G) by TOPS_1:44; Int right_cell(f,k,G) misses L~f by A1,A2,JORDAN9:17; then A4: Int right_cell(f,k,G) c= right_cell(f,k,G)\L~f by A3,XBOOLE_1:86; right_cell(f,k,G)\L~f c= RightComp f by A1,A2,JORDAN9:29; hence Int right_cell(f,k,G) c= RightComp f by A4,XBOOLE_1:1; A5: Int left_cell(f,k,G) c= left_cell(f,k,G) by TOPS_1:44; Int left_cell(f,k,G) misses L~f by A1,A2,JORDAN9:17; then A6: Int left_cell(f,k,G) c= left_cell(f,k,G)\L~f by A5,XBOOLE_1:86; left_cell(f,k,G)\L~f c= LeftComp f by A1,A2,JORDAN9:29; hence Int left_cell(f,k,G) c= LeftComp f by A6,XBOOLE_1:1; end; theorem Th32: for i1,j1,i2,j2 being Nat, G being Go-board st [i1,j1] in Indices G & [i2,j2] in Indices G & G*(i1,j1) = G*(i2,j2) holds i1 = i2 & j1 = j2 proof let i1,j1,i2,j2 be Nat, G be Go-board such that A1: [i1,j1] in Indices G and A2: [i2,j2] in Indices G and A3: G*(i1,j1) = G*(i2,j2); A4: 1 <= i1 & i1 <= len G by A1,GOBOARD5:1; A5: 1 <= j1 & j1 <= width G by A1,GOBOARD5:1; A6: 1 <= i2 & i2 <= len G by A2,GOBOARD5:1; A7: 1 <= j2 & j2 <= width G by A2,GOBOARD5:1; then A8: G*(i1,j2)`1 = G*(i1,1)`1 by A4,GOBOARD5:3 .= G*(i1,j1)`1 by A4,A5,GOBOARD5:3; A9: G*(i1,j2)`2 = G*(1,j2)`2 by A4,A7,GOBOARD5:2 .= G*(i1,j1)`2 by A3,A6,A7,GOBOARD5:2; assume A10: not thesis; per cases by A10,AXIOMS:21; suppose i1 < i2; hence contradiction by A3,A4,A6,A7,A8,GOBOARD5:4; suppose i1 > i2; hence contradiction by A3,A4,A6,A7,A8,GOBOARD5:4; suppose j1 < j2; hence contradiction by A4,A5,A7,A9,GOBOARD5:5; suppose j1 > j2; hence contradiction by A4,A5,A7,A9,GOBOARD5:5; end; theorem Th33: for f being FinSequence of TOP-REAL 2, M being Go-board holds f is_sequence_on M implies mid(f,i1,i2) is_sequence_on M proof let f be FinSequence of TOP-REAL 2, M be Go-board; assume that A1: f is_sequence_on M; per cases; suppose i1<=i2; then A2: mid(f,i1,i2) = (f/^(i1-'1))|(i2-'i1+1) by JORDAN3:def 1; f/^(i1-'1) is_sequence_on M by A1,JORDAN8:5; hence mid(f,i1,i2) is_sequence_on M by A2,GOBOARD1:38; suppose i1 > i2; then A3: mid(f,i1,i2) = Rev ((f/^(i2-'1))|(i1-'i2+1)) by JORDAN3:def 1; f/^(i2-'1) is_sequence_on M by A1,JORDAN8:5; then (f/^(i2-'1))|(i1-'i2+1) is_sequence_on M by GOBOARD1:38; hence mid(f,i1,i2) is_sequence_on M by A3,JORDAN9:7; end; definition cluster -> non empty non-empty Go-board; coherence proof let G be Go-board; A1: len G <> 0 by GOBOARD1:def 5; thus G is non empty by CARD_1:47,GOBOARD1:def 5; assume G is not non-empty; then consider n being set such that A2: n in dom G and A3: G.n is empty by UNIALG_1:def 6; len G > 0 by A1,NAT_1:19; then consider s0 being FinSequence such that A4: s0 in rng G and A5: len s0 = width G by MATRIX_1:def 4; consider n0 being Nat such that A6: for x being set st x in rng G ex s being FinSequence st s=x & len s = n0 by MATRIX_1:def 1; G.n in rng G by A2,FUNCT_1:12; then consider s1 being FinSequence such that A7: s1 = G.n and A8: len s1 = n0 by A6; ex s being FinSequence st s=s0 & len s = n0 by A4,A6; hence contradiction by A3,A5,A7,A8,CARD_1:47,GOBOARD1:def 5; end; end; theorem Th34: for G being Go-board st 1 <= i & i <= len G holds SgmX(RealOrd, proj1.:Values G).i = G*(i,1)`1 proof let G be Go-board such that A1: 1 <= i & i <= len G; deffunc F(Nat)=G*($1,1)`1; consider f being FinSequence of REAL such that A2: len f = len G and A3: for i st i in Seg len G holds f.i = F(i) from SeqLambdaD; 0 <> width G by GOBOARD1:def 5; then A4: 1 <= width G by RLVECT_1:99; reconsider A = proj1.:Values G as finite Subset of REAL; A5: rng f = A proof A6: Values G = { G*(m,n): [m,n] in Indices G } by GOBRD13:7; thus rng f c= A proof let x be set; assume A7: x in rng f; rng f c= REAL by FINSEQ_1:def 4; then reconsider x as Element of REAL by A7; consider y being set such that A8: y in dom f and A9: x = f.y by A7,FUNCT_1:def 5; reconsider y as Nat by A8; 1 <= y & y <= len G by A2,A8,FINSEQ_3:27; then [y,1] in Indices G by A4,GOBOARD7:10; then A10: G*(y,1) in Values G by A6; y in Seg len G by A2,A8,FINSEQ_1:def 3; then x = G*(y,1)`1 by A3,A9 .= proj1.(G*(y,1)) by PSCOMP_1:def 28; hence thesis by A10,FUNCT_2:43; end; let x be set; assume A11: x in A; then reconsider x as Element of REAL; consider p being Element of TOP-REAL 2 such that A12: p in Values G and A13: x = proj1.p by A11,FUNCT_2:116; consider m,n such that A14: p = G*(m,n) and A15: [m,n] in Indices G by A6,A12; A16: 1 <= n & n <= width G by A15,GOBOARD5:1; A17: 1 <= m & m <= len G by A15,GOBOARD5:1; then A18: m in Seg len G by FINSEQ_1:3; A19: m in dom f by A2,A17,FINSEQ_3:27; x = p`1 by A13,PSCOMP_1:def 28 .= G*(m,1)`1 by A14,A16,A17,GOBOARD5:3 .= f.m by A3,A18; hence thesis by A19,FUNCT_1:def 5; end; for n,m be Nat st n in dom f & m in dom f & n < m holds f/.n <> f/.m & [f/.n, f/.m] in RealOrd proof let n,m be Nat such that A20: n in dom f and A21: m in dom f and A22: n < m; dom f = Seg len G by A2,FINSEQ_1:def 3; then A23: f.n = G*(n,1)`1 & f.m = G*(m,1)`1 by A3,A20,A21; A24: 1 <= n & m <= len G by A2,A20,A21,FINSEQ_3:27; then A25: f.n < f.m by A4,A22,A23,GOBOARD5:4; A26: f/.n = f.n & f/.m = f.m by A20,A21,FINSEQ_4:def 4; hence f/.n <> f/.m by A4,A22,A23,A24,GOBOARD5:4; thus [f/.n, f/.m] in RealOrd by A25,A26,Def1; end; then A27: f = SgmX(RealOrd, proj1.:Values G) by A5,TRIANG_1:4; i in dom G by A1,FINSEQ_3:27; then i in Seg len G by FINSEQ_1:def 3; hence SgmX(RealOrd, proj1.:Values G).i = G*(i,1)`1 by A3,A27; end; theorem Th35: for G being Go-board st 1 <= j & j <= width G holds SgmX(RealOrd, proj2.:Values G).j = G*(1,j)`2 proof let G be Go-board such that A1: 1 <= j & j <= width G; deffunc F(Nat)=G*(1,$1)`2; consider f being FinSequence of REAL such that A2: len f = width G and A3: for i st i in Seg width G holds f.i = F(i) from SeqLambdaD; 0 <> len G by GOBOARD1:def 5; then A4: 1 <= len G by RLVECT_1:99; reconsider A = proj2.:Values G as finite Subset of REAL; A5: rng f = A proof A6: Values G = { G*(m,n): [m,n] in Indices G } by GOBRD13:7; thus rng f c= A proof let x be set; assume A7: x in rng f; rng f c= REAL by FINSEQ_1:def 4; then reconsider x as Element of REAL by A7; consider y being set such that A8: y in dom f and A9: x = f.y by A7,FUNCT_1:def 5; reconsider y as Nat by A8; 1 <= y & y <= width G by A2,A8,FINSEQ_3:27; then [1,y] in Indices G by A4,GOBOARD7:10; then A10: G*(1,y) in Values G by A6; y in Seg width G by A2,A8,FINSEQ_1:def 3; then x = G*(1,y)`2 by A3,A9 .= proj2.(G*(1,y)) by PSCOMP_1:def 29; hence thesis by A10,FUNCT_2:43; end; let x be set; assume A11: x in A; then reconsider x as Element of REAL; consider p being Element of TOP-REAL 2 such that A12: p in Values G and A13: x = proj2.p by A11,FUNCT_2:116; consider m,n such that A14: p = G*(m,n) and A15: [m,n] in Indices G by A6,A12; A16: 1 <= m & m <= len G by A15,GOBOARD5:1; A17: 1 <= n & n <= width G by A15,GOBOARD5:1; then A18: n in Seg width G by FINSEQ_1:3; A19: n in dom f by A2,A17,FINSEQ_3:27; x = p`2 by A13,PSCOMP_1:def 29 .= G*(1,n)`2 by A14,A16,A17,GOBOARD5:2 .= f.n by A3,A18; hence thesis by A19,FUNCT_1:def 5; end; for n,m be Nat st n in dom f & m in dom f & n < m holds f/.n <> f/.m & [f/.n, f/.m] in RealOrd proof let n,m be Nat such that A20: n in dom f and A21: m in dom f and A22: n < m; dom f = Seg width G by A2,FINSEQ_1:def 3; then A23: f.n = G*(1,n)`2 & f.m = G*(1,m)`2 by A3,A20,A21; A24: 1 <= n & m <= width G by A2,A20,A21,FINSEQ_3:27; then A25: f.n < f.m by A4,A22,A23,GOBOARD5:5; A26: f/.n = f.n & f/.m = f.m by A20,A21,FINSEQ_4:def 4; hence f/.n <> f/.m by A4,A22,A23,A24,GOBOARD5:5; thus [f/.n, f/.m] in RealOrd by A25,A26,Def1; end; then A27: f = SgmX(RealOrd, proj2.:Values G) by A5,TRIANG_1:4; j in Seg width G by A1,FINSEQ_1:3; hence SgmX(RealOrd, proj2.:Values G).j = G*(1,j)`2 by A3,A27; end; theorem Th36: for f being non empty FinSequence of TOP-REAL 2, G being Go-board st f is_sequence_on G & (ex i st [1,i] in Indices G & G*(1,i) in rng f) & (ex i st [len G,i] in Indices G & G*(len G,i) in rng f) holds proj1.:rng f = proj1.:Values G proof let f be non empty FinSequence of TOP-REAL 2, G be Go-board such that A1: f is_sequence_on G; given i1 being Nat such that A2: [1,i1] in Indices G and A3: G*(1,i1) in rng f; given i2 being Nat such that A4: [len G,i2] in Indices G and A5: G*(len G,i2) in rng f; rng f c= Values G by A1,GOBRD13:9; hence proj1.:rng f c= proj1.:Values G by RELAT_1:156; A6: Values G = { G*(i,j): [i,j] in Indices G } by GOBRD13:7; consider k1 being set such that A7: k1 in dom f and A8: G*(1,i1) = f.k1 by A3,FUNCT_1:def 5; reconsider k1 as Nat by A7; A9: 1 <= k1 & k1 <= len f by A7,FINSEQ_3:27; consider k2 being set such that A10: k2 in dom f and A11: G*(len G,i2) = f.k2 by A5,FUNCT_1:def 5; reconsider k2 as Nat by A10; A12: 1 <= k2 & k2 <= len f by A10,FINSEQ_3:27; set g = mid(f,k1,k2); A13: g is_sequence_on G by A1,Th33; A14: now per cases; suppose k1 <= k2; then A15: len g = k2-'k1+1 by A9,A12,JORDAN4:20; k2-'k1 >= 0 by NAT_1:18; hence len g >= 0+1 by A15,AXIOMS:24; suppose k1 > k2; then A16: len g=k1-'k2+1 by A9,A12,JORDAN4:21; k1-'k2 >= 0 by NAT_1:18; hence len g >= 0+1 by A16,AXIOMS:24; end; A17: proj1.:Values G c= proj1.:rng g proof assume not thesis; then consider x being Element of REAL such that A18: x in proj1.:Values G and A19: not x in proj1.:rng g by SUBSET_1:7; consider p being Element of TOP-REAL 2 such that A20: p in Values G and A21: x = proj1.p by A18,FUNCT_2:116; consider i0,j0 being Nat such that A22: p = G*(i0,j0) and A23: [i0,j0] in Indices G by A6,A20; A24: 1 <= i0 & i0 <= len G by A23,GOBOARD5:1; A25: 1 <= j0 & j0 <= width G by A23,GOBOARD5:1; defpred P[Nat] means 1 <= $1 & $1 <= len g implies for i,j st [i,j] in Indices G & G*(i,j) = g.$1 holds i < i0; A26: P[0]; A27: for n st P[n] holds P[n+1] proof let n such that A28: 1 <= n & n <= len g implies for i,j st [i,j] in Indices G & G*(i,j) = g.n holds i < i0 and A29: 1 <= n+1 & n+1 <= len g; let i,j such that A30: [i,j] in Indices G and A31: G*(i,j) = g.(n+1); A32: now assume A33: i = i0; A34: n+1 in dom g by A29,FINSEQ_3:27; then A35: G*(i,j) = g/.(n+1) by A31,FINSEQ_4:def 4; A36: 1 <= j & j <= width G by A30,GOBOARD5:1; A37: x = p`1 by A21,PSCOMP_1:def 28 .= G*(i0,1)`1 by A22,A24,A25,GOBOARD5:3 .= G*(i,j)`1 by A24,A33,A36,GOBOARD5:3 .= proj1.(g/.(n+1)) by A35,PSCOMP_1:def 28; A38: dom proj1 = the carrier of TOP-REAL 2 by FUNCT_2:def 1; g/.(n+1) in rng g by A31,A34,A35,FUNCT_1:12; hence contradiction by A19,A37,A38,FUNCT_1:def 12; end; per cases; suppose n = 0; then G*(i,j) = G*(1,i1) by A8,A9,A12,A31,JORDAN3:27; then i = 1 by A2,A30,Th32; hence thesis by A24,A32,AXIOMS:21; suppose A39: n <> 0; then A40: 1 <= n by RLVECT_1:99; A41: n <= n + 1 by NAT_1:29; then n <= len g by A29,AXIOMS:22; then A42: n in dom g by A40,FINSEQ_3:27; then consider i1,j1 being Nat such that A43: [i1,j1] in Indices G and A44: g/.n = G*(i1,j1) by A13,GOBOARD1:def 11; A45: n+1 in dom g by A29,FINSEQ_3:27; then g/.(n+1) = G*(i,j) by A31,FINSEQ_4:def 4; then abs(i1-i)+abs(j1-j) = 1 by A13,A30,A42,A43,A44,A45,GOBOARD1:def 11; then A46: abs(i1-i)=1 & j1=j or abs(j1-j)=1 & i1=i by GOBOARD1:2; now g.n = g/.n by A42,FINSEQ_4:def 4; then A47: i1 < i0 by A28,A29,A39,A41,A43,A44,AXIOMS:22,RLVECT_1:99; per cases by A46,GOBOARD1:1; suppose i1 = i or i < i1; hence i < i0 by A47,AXIOMS:22; suppose i = i1 + 1; then i <= i0 by A47,NAT_1:38; hence thesis by A32,AXIOMS:21; end; hence i < i0; end; A48: for n holds P[n] from Ind(A26,A27); G*(len G,i2) = g.len g by A9,A11,A12,JORDAN4:23; then len G < i0 by A4,A14,A48; hence contradiction by A23,GOBOARD5:1; end; rng g c= rng f by JORDAN3:28; then proj1.:rng g c= proj1.:rng f by RELAT_1:156; hence thesis by A17,XBOOLE_1:1; end; theorem Th37: for f being non empty FinSequence of TOP-REAL 2, G being Go-board st f is_sequence_on G & (ex i st [i,1] in Indices G & G*(i,1) in rng f) & (ex i st [i,width G] in Indices G & G*(i,width G) in rng f) holds proj2.:rng f = proj2.:Values G proof let f be non empty FinSequence of TOP-REAL 2, G be Go-board such that A1: f is_sequence_on G; given i1 being Nat such that A2: [i1,1] in Indices G and A3: G*(i1,1) in rng f; given i2 being Nat such that A4: [i2,width G] in Indices G and A5: G*(i2,width G) in rng f; rng f c= Values G by A1,GOBRD13:9; hence proj2.:rng f c= proj2.:Values G by RELAT_1:156; A6: Values G = { G*(i,j): [i,j] in Indices G } by GOBRD13:7; consider k1 being set such that A7: k1 in dom f and A8: G*(i1,1) = f.k1 by A3,FUNCT_1:def 5; reconsider k1 as Nat by A7; A9: 1 <= k1 & k1 <= len f by A7,FINSEQ_3:27; consider k2 being set such that A10: k2 in dom f and A11: G*(i2, width G) = f.k2 by A5,FUNCT_1:def 5; reconsider k2 as Nat by A10; A12: 1 <= k2 & k2 <= len f by A10,FINSEQ_3:27; set g = mid(f,k1,k2); A13: g is_sequence_on G by A1,Th33; A14: now per cases; suppose k1 <= k2; then A15: len g = k2-'k1+1 by A9,A12,JORDAN4:20; k2-'k1 >= 0 by NAT_1:18; hence len g >= 0+1 by A15,AXIOMS:24; suppose k1 > k2; then A16: len g=k1-'k2+1 by A9,A12,JORDAN4:21; k1-'k2 >= 0 by NAT_1:18; hence len g >= 0+1 by A16,AXIOMS:24; end; A17: proj2.:Values G c= proj2.:rng g proof assume not thesis; then consider x being Element of REAL such that A18: x in proj2.:Values G and A19: not x in proj2.:rng g by SUBSET_1:7; consider p being Element of TOP-REAL 2 such that A20: p in Values G and A21: x = proj2.p by A18,FUNCT_2:116; consider i0,j0 being Nat such that A22: p = G*(i0,j0) and A23: [i0,j0] in Indices G by A6,A20; A24: 1 <= i0 & i0 <= len G by A23,GOBOARD5:1; A25: 1 <= j0 & j0 <= width G by A23,GOBOARD5:1; defpred P[Nat] means 1 <= $1 & $1 <= len g implies for i,j st [i,j] in Indices G & G*(i,j) = g.$1 holds j < j0; A26: P[0]; A27: for n st P[n] holds P[n+1] proof let n such that A28: 1 <= n & n <= len g implies for i,j st [i,j] in Indices G & G*(i,j) = g.n holds j < j0 and A29: 1 <= n+1 & n+1 <= len g; let i,j such that A30: [i,j] in Indices G and A31: G*(i,j) = g.(n+1); A32: now assume A33: j = j0; A34: n+1 in dom g by A29,FINSEQ_3:27; then A35: G*(i,j) = g/.(n+1) by A31,FINSEQ_4:def 4; A36: 1 <= i & i <= len G by A30,GOBOARD5:1; A37: x = p`2 by A21,PSCOMP_1:def 29 .= G*(1,j0)`2 by A22,A24,A25,GOBOARD5:2 .= G*(i,j)`2 by A25,A33,A36,GOBOARD5:2 .= proj2.(g/.(n+1)) by A35,PSCOMP_1:def 29; A38: dom proj2 = the carrier of TOP-REAL 2 by FUNCT_2:def 1; g/.(n+1) in rng g by A31,A34,A35,FUNCT_1:12; hence contradiction by A19,A37,A38,FUNCT_1:def 12; end; per cases; suppose n = 0; then G*(i,j) = G*(i1,1) by A8,A9,A12,A31,JORDAN3:27; then j = 1 by A2,A30,Th32; hence thesis by A25,A32,AXIOMS:21; suppose A39: n <> 0; then A40: 1 <= n by RLVECT_1:99; A41: n <= n + 1 by NAT_1:29; then n <= len g by A29,AXIOMS:22; then A42: n in dom g by A40,FINSEQ_3:27; then consider i1,j1 being Nat such that A43: [i1,j1] in Indices G and A44: g/.n = G*(i1,j1) by A13,GOBOARD1:def 11; A45: n+1 in dom g by A29,FINSEQ_3:27; then g/.(n+1) = G*(i,j) by A31,FINSEQ_4:def 4; then abs(i1-i)+abs(j1-j) = 1 by A13,A30,A42,A43,A44,A45,GOBOARD1:def 11; then A46: abs(i1-i)=1 & j1=j or abs(j1-j)=1 & i1=i by GOBOARD1:2; now g.n = g/.n by A42,FINSEQ_4:def 4; then A47: j1 < j0 by A28,A29,A39,A41,A43,A44,AXIOMS:22,RLVECT_1:99; per cases by A46,GOBOARD1:1; suppose j1 = j or j < j1; hence j < j0 by A47,AXIOMS:22; suppose j = j1 + 1; then j <= j0 by A47,NAT_1:38; hence thesis by A32,AXIOMS:21; end; hence j < j0; end; A48: for n holds P[n] from Ind(A26,A27); G*(i2,width G) = g.len g by A9,A11,A12,JORDAN4:23; then width G < j0 by A4,A14,A48; hence contradiction by A23,GOBOARD5:1; end; rng g c= rng f by JORDAN3:28; then proj2.:rng g c= proj2.:rng f by RELAT_1:156; hence thesis by A17,XBOOLE_1:1; end; definition let G be Go-board; cluster Values G -> non empty; coherence proof dom G is non empty; then reconsider f = rngs G as non empty non-empty Function by EXTENS_1:4,RELAT_1:60; Union f is non empty; hence thesis by GOBRD13:def 1; end; end; theorem Th38: for G being Go-board holds G = GoB(SgmX(RealOrd, proj1.:Values G), SgmX(RealOrd,proj2.:Values G)) proof let G be Go-board; set v1 = SgmX(RealOrd, proj1.:Values G), v2 = SgmX(RealOrd,proj2.:Values G); A1: len G = card(proj1.:Values G) by Th22 .= len v1 by Th15; A2: width G = card(proj2.:Values G) by Th25 .= len v2 by Th15; for n,m st [n,m] in Indices G holds G*(n,m) = |[v1.n,v2.m]| proof let n,m; assume A3: [n,m] in Indices G; then A4: 1 <= n & n <= len G by GOBOARD5:1; then A5: v1.n = G*(n,1)`1 by Th34; A6: 1 <= m & m <= width G by A3,GOBOARD5:1; then v2.m = G*(1,m)`2 by Th35; then A7: v2.m = G*(n,m)`2 by A4,A6,GOBOARD5:2; v1.n = G*(n,m)`1 by A4,A5,A6,GOBOARD5:3; hence G*(n,m) = |[v1.n,v2.m]| by A7,EUCLID:57; end; hence G = GoB(SgmX(RealOrd, proj1.:Values G), SgmX(RealOrd,proj2.:Values G)) by A1,A2,GOBOARD2:def 1; end; theorem Th39: for f being non empty FinSequence of TOP-REAL 2, G being Go-board st proj1.:rng f = proj1.:Values G & proj2.:rng f = proj2.:Values G holds G = GoB f proof let f be non empty FinSequence of TOP-REAL 2, G being Go-board; assume A1: proj1.:rng f = proj1.:Values G & proj2.:rng f = proj2.:Values G; X_axis f = proj1*f by Th16; then rng X_axis f = proj1.:rng f by RELAT_1:160; then A2: Incr X_axis f = SgmX(RealOrd, proj1.:rng f) by Th13; Y_axis f = proj2*f by Th17; then rng Y_axis f = proj2.:rng f by RELAT_1:160; then Incr Y_axis f = SgmX(RealOrd, proj2.:rng f) by Th13; hence G = GoB(Incr X_axis f, Incr Y_axis f) by A1,A2,Th38 .= GoB f by GOBOARD2:def 3; end; theorem Th40: for f being non empty FinSequence of TOP-REAL 2, G being Go-board st f is_sequence_on G & (ex i st [1,i] in Indices G & G*(1,i) in rng f) & (ex i st [i,1] in Indices G & G*(i,1) in rng f) & (ex i st [len G,i] in Indices G & G*(len G,i) in rng f) & (ex i st [i,width G] in Indices G & G*(i,width G) in rng f) holds G = GoB f proof let f be non empty FinSequence of TOP-REAL 2, G being Go-board such that A1: f is_sequence_on G; given i1 being Nat such that A2: [1,i1] in Indices G and A3: G*(1,i1) in rng f; given i2 being Nat such that A4: [i2,1] in Indices G and A5: G*(i2,1) in rng f; given i3 being Nat such that A6: [len G,i3] in Indices G and A7: G*(len G,i3) in rng f; given i4 being Nat such that A8: [i4,width G] in Indices G and A9: G*(i4,width G) in rng f; A10: proj1.:rng f = proj1.:Values G by A1,A2,A3,A6,A7,Th36; proj2.:rng f = proj2.:Values G by A1,A4,A5,A8,A9,Th37; hence thesis by A10,Th39; end; begin :: More about gauges theorem Th41: m <= n & 1 <= i & i+1 <= len Gauge(C,n) implies [\ (i-2)/2|^(n-'m)+2 /] is Nat proof assume that A1: m <= n and A2: 1 <= i & i+1 <= len Gauge(C,n); set i1 = [\ (i-2)/2|^(n-'m)+2 /]; (i-2)/2|^(n-'m)+2-1 = (i-2)/2|^(n-'m)+(2-1) by XCMPLX_1:29; then A3: (i-2)/2|^(n-'m)+1 < i1 by INT_1:def 4; m + 0 <= n by A1; then n -' m >= 0 by SPRECT_3:8; then A4: n -' m + 1 >= 0 + 1 by AXIOMS:24; A5: n-'m +1 <= 2|^(n-'m) by HEINE:7; then A6: 0 +1 <= 2|^(n-'m) by A4,AXIOMS:22; A7: 0 < 2|^(n-'m) by A4,A5,AXIOMS:22; 1-2 <= i-2 by A2,REAL_1:49; then A8: (-1)/2|^(n-'m) <= (i-2)/2|^(n-'m) by A7,REAL_1:73; (-1)/1 <= (-1)/2|^(n-'m) by A6,REAL_2:203; then -1 <= (i-2)/2|^(n-'m) by A8,AXIOMS:22; then -1 + 1 <= (i-2)/2|^(n-'m) + 1 by AXIOMS:24; then i1 >= 0 by A3,AXIOMS:22; hence i1 is Nat by INT_1:16; end; theorem Th42: m <= n & 1 <= i & i+1 <= len Gauge(C,n) implies 1 <= [\ (i-2)/2|^(n-'m)+2 /] & [\ (i-2)/2|^(n-'m)+2 /]+1 <= len Gauge(C,m) proof assume that A1: m <= n and A2: 1 <= i & i+1 <= len Gauge(C,n); set i1 = [\ (i-2)/2|^(n-'m)+2 /]; (i-2)/2|^(n-'m)+2-1 = (i-2)/2|^(n-'m)+(2-1) by XCMPLX_1:29; then A3: (i-2)/2|^(n-'m)+1 < i1 by INT_1:def 4; m + 0 <= n by A1; then n -' m >= 0 by SPRECT_3:8; then A4: n -' m + 1 >= 0 + 1 by AXIOMS:24; A5: n-'m +1 <= 2|^(n-'m) by HEINE:7; then A6: 0 +1 <= 2|^(n-'m) by A4,AXIOMS:22; A7: 0 < 2|^(n-'m) by A4,A5,AXIOMS:22; 1-2 <= i-2 by A2,REAL_1:49; then A8: (-1)/2|^(n-'m) <= (i-2)/2|^(n-'m) by A7,REAL_1:73; (-1)/1 <= (-1)/2|^(n-'m) by A6,REAL_2:203; then -1 <= (i-2)/2|^(n-'m) by A8,AXIOMS:22; then -1 + 1 <= (i-2)/2|^(n-'m) + 1 by AXIOMS:24; then i1 >= 1+0 by A3,INT_1:20; hence 1 <= i1; i1 <= (i-2)/2|^(n-'m)+2 by INT_1:def 4; then i1+1 <= (i-2)/2|^(n-'m)+2+1 by AXIOMS:24; then A9: i1+1 <= (i-2)/2|^(n-'m)+(2+1) by XCMPLX_1:1; i+1 <= 2|^n+ (2+1) by A2,JORDAN8:def 1; then i+1 <= 2|^n+ 2+1 by XCMPLX_1:1; then i <= 2|^n+ 2 by REAL_1:53; then i-2 <= 2|^n by REAL_1:86; then (i-2) <= 2|^(m+(n-'m)) by A1,AMI_5:4; then (i-2)*1 <= 2|^m*2|^(n-'m) by NEWTON:13; then (i-2)/2|^(n-'m) <= 2|^m/1 by A7,REAL_2:187; then (i-2)/2|^(n-'m) + 3 <= 2|^m + 3 by AXIOMS:24; then (i-2)/2|^(n-'m) + 3 <= len Gauge(C,m) by JORDAN8:def 1; hence i1+1 <= len Gauge(C,m) by A9,AXIOMS:22; end; theorem Th43: m <= n & 1 <= i & i+1 <= len Gauge(C,n) & 1 <= j & j+1 <= width Gauge(C,n) implies ex i1,j1 st i1 = [\ (i-2)/2|^(n-'m)+2 /] & j1 = [\ (j-2)/2|^(n-'m)+2 /] & cell(Gauge(C,n),i,j) c= cell(Gauge(C,m),i1,j1) proof assume that A1: m <= n and A2: 1 <= i & i+1 <= len Gauge(C,n) and A3: 1 <= j & j+1 <= width Gauge(C,n); A4: len Gauge(C,m) = width Gauge(C,m) & len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; then reconsider i1 = [\ (i-2)/2|^(n-'m)+2 /], j1 = [\ (j-2)/2|^(n-'m)+2 /] as Nat by A1,A2,A3,Th41; take i1,j1; thus i1 = [\ (i-2)/2|^(n-'m)+2 /]; thus j1 = [\ (j-2)/2|^(n-'m)+2 /]; (i-2)/2|^(n-'m)+2-1 = (i-2)/2|^(n-'m)+(2-1) by XCMPLX_1:29; then A5: (i-2)/2|^(n-'m)+1 < i1 by INT_1:def 4; m + 0 <= n by A1; then A6: n -' m >= 0 by SPRECT_3:8; then A7: n -' m + 1 >= 0 + 1 by AXIOMS:24; A8: n-'m +1 <= 2|^(n-'m) by HEINE:7; then A9: 0 +1 <= 2|^(n-'m) by A7,AXIOMS:22; A10: 0 < 2|^(n-'m) by A7,A8,AXIOMS:22; 1-2 <= i-2 by A2,REAL_1:49; then A11: (-1)/2|^(n-'m) <= (i-2)/2|^(n-'m) by A10,REAL_1:73; A12: (-1)/1 <= (-1)/2|^(n-'m) by A9,REAL_2:203; then -1 <= (i-2)/2|^(n-'m) by A11,AXIOMS:22; then -1 + 1 <= (i-2)/2|^(n-'m) + 1 by AXIOMS:24; then A13: i1 >= 1+0 by A5,INT_1:20; (j-2)/2|^(n-'m)+2-1 = (j-2)/2|^(n-'m)+(2-1) by XCMPLX_1:29; then A14: (j-2)/2|^(n-'m)+1 < j1 by INT_1:def 4; 1-2 <= j-2 by A3,REAL_1:49; then (-1)/2|^(n-'m) <= (j-2)/2|^(n-'m) by A10,REAL_1:73; then -1 <= (j-2)/2|^(n-'m) by A12,AXIOMS:22; then -1 + 1 <= (j-2)/2|^(n-'m) + 1 by AXIOMS:24; then A15: j1 >= 1+0 by A14,INT_1:20; A16:i1 <= (i-2)/2|^(n-'m)+2 by INT_1:def 4; A17: i1+1 <= len Gauge(C,m) by A1,A2,Th42; A18: j1 <= (j-2)/2|^(n-'m)+2 by INT_1:def 4; A19: j1+1 <= width Gauge(C,m) by A1,A3,A4,Th42; let e be set; set Gm = Gauge(C,m), Gn = Gauge(C,n); assume A20: e in cell(Gauge(C,n),i,j); then reconsider p = e as Point of TOP-REAL 2; A21: 2|^m >m by HEINE:8; A22: m >= 0 by NAT_1:18; i <= len Gn & j <= width Gn by A2,A3,NAT_1:38; then [i,j] in Indices Gn by A2,A3,GOBOARD7:10; then A23: Gn*(i,j) =|[(W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*(i-2), (S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*(j-2)]| by JORDAN8:def 1; then A24: Gn*(i,j)`1 =(W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*((i-2) /1) by EUCLID:56 .= (W-bound C)+((E-bound C)-(W-bound C))/1 *((i-2)/(2|^n)) by XCMPLX_1: 86; A25: Gn*(i,j)`2 =(S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*((j-2)/1) by A23,EUCLID:56 .= (S-bound C)+(((N-bound C)-(S-bound C))/1)*((j-2)/(2|^n)) by XCMPLX_1:86 ; i1 <= len Gauge(C,m) & j1 <= width Gauge(C,m) by A17,A19,NAT_1:38; then [i1,j1] in Indices Gm by A13,A15,GOBOARD7:10; then A26: Gm*(i1,j1) =|[(W-bound C)+(((E-bound C)-(W-bound C))/(2|^m))*(i1- 2), (S-bound C)+(((N-bound C)-(S-bound C))/(2|^m))*(j1-2)]| by JORDAN8:def 1; then A27: Gm*(i1,j1)`1 =(W-bound C)+(((E-bound C)-(W-bound C))/(2|^m))*((i1 -2)/1) by EUCLID:56 .= (W-bound C)+(((E-bound C)-(W-bound C))/1)*((i1-2)/(2|^m)) by XCMPLX_1: 86; A28: Gm*(i1,j1)`2 =(S-bound C)+(((N-bound C)-(S-bound C))/(2|^m))*((j1-2)/1) by A26,EUCLID:56 .= (S-bound C)+(((N-bound C)-(S-bound C))/1)*((j1-2)/(2|^m)) by XCMPLX_1: 86; (E-bound C) >= (W-bound C)+0 by SPRECT_1:23; then A29: (E-bound C)-(W-bound C) >= 0 by REAL_1:84; (N-bound C) >= (S-bound C)+0 by SPRECT_1:24; then A30: (N-bound C)-(S-bound C) >= 0 by REAL_1:84; A31: Gn*(i,j)`1 <= p`1 by A2,A3,A20,JORDAN9:19; i1-2 <= (i-2)/2|^(n-'m) by A16,REAL_1:86; then (i1-2)/2|^m <= (i-2)/2|^(n-'m)/2|^m by A21,A22,REAL_1:73; then (i1-2)/2|^m <= (i-2)/(2|^(n-'m)*2|^m) by XCMPLX_1:79; then (i1-2)/2|^m <= (i-2)/2|^(n-'m+m) by NEWTON:13; then (i1-2)/2|^m <= (i-2)/2|^n by A1,AMI_5:4; then (((E-bound C)-(W-bound C)))*((i1-2)/(2|^m)) <= (((E-bound C)-(W-bound C)))*((i-2)/(2|^n)) by A29,AXIOMS:25; then Gm*(i1,j1)`1 <= Gn*(i,j)`1 by A24,A27,AXIOMS:24; then A32: Gm*(i1,j1)`1 <= p`1 by A31,AXIOMS:22; 1 <= i1+1 & j1 <= width Gauge(C,m) by A19,NAT_1:29,38; then [i1+1,j1] in Indices Gm by A15,A17,GOBOARD7:10; then Gm*(i1+1,j1) =|[(W-bound C)+(((E-bound C)-(W-bound C))/(2|^m))*(i1+1-2), (S-bound C)+(((N-bound C)-(S-bound C))/(2|^m))*(j1-2)]| by JORDAN8:def 1; then A33: Gm*(i1+1,j1)`1 =(W-bound C)+(((E-bound C)-(W-bound C))/(2|^m))*((i1+1-2)/1) by EUCLID:56 .= (W-bound C)+(((E-bound C)-(W-bound C))/1)*((i1+1-2)/(2|^m)) by XCMPLX_1:86; 1 <= i+1 & j <= width Gn by A3,NAT_1:29,38; then [i+1,j] in Indices Gn by A2,A3,GOBOARD7:10; then Gn*(i+1,j) =|[(W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*(i+1-2), (S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*(j-2)]| by JORDAN8:def 1; then A34: Gn*(i+1,j)`1 =(W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*((i+1-2)/1) by EUCLID:56 .= (W-bound C)+(((E-bound C)-(W-bound C))/1)*((i+1-2)/(2|^n)) by XCMPLX_1:86; A35: p`1 <= Gn*(i+1,j)`1 by A2,A3,A20,JORDAN9:19; A36: 2|^(n-'m) >n-'m by HEINE:8; (i-2)/2|^(n-'m)+2-1 < i1 by INT_1:def 4; then (i-2)/2|^(n-'m)+2 < i1+1 by REAL_1:84; then (i-2)/2|^(n-'m) < i1+1-2 by REAL_1:86; then (i-2) < (i1+1-2)*2|^(n-'m) by A6,A36,REAL_2:177; then (i-2) + 1 <= (i1+1-2)*2|^(n-'m) by INT_1:20; then i+1-2 <= (i1+1-2)*2|^(n-'m) by XCMPLX_1:29; then (i+1-2)/2|^(n-'m) <= i1+1-2 by A6,A36,REAL_2:177; then (i+1-2)/2|^(n-'m)/2|^m <= (i1+1-2)/2|^m by A21,A22,REAL_1:73; then (i+1-2)/(2|^(n-'m)*2|^m) <= (i1+1-2)/2|^m by XCMPLX_1:79; then (i+1-2)/2|^(n-'m+m) <= (i1+1-2)/2|^m by NEWTON:13; then (i+1-2)/2|^n <= (i1+1-2)/2|^m by A1,AMI_5:4; then (((E-bound C)-(W-bound C)))*((i+1-2)/(2|^n)) <= (((E-bound C)-(W-bound C)))*((i1+1-2)/(2|^m)) by A29,AXIOMS:25; then Gn*(i+1,j)`1 <= Gm*(i1+1,j1)`1 by A33,A34,AXIOMS:24; then A37: p`1 <= Gm*(i1+1,j1)`1 by A35,AXIOMS:22; A38: Gn*(i,j)`2 <= p`2 by A2,A3,A20,JORDAN9:19; j1-2 <= (j-2)/2|^(n-'m) by A18,REAL_1:86; then (j1-2)/2|^m <= (j-2)/2|^(n-'m)/2|^m by A21,A22,REAL_1:73; then (j1-2)/2|^m <= (j-2)/(2|^(n-'m)*2|^m) by XCMPLX_1:79; then (j1-2)/2|^m <= (j-2)/2|^(n-'m+m) by NEWTON:13; then (j1-2)/2|^m <= (j-2)/2|^n by A1,AMI_5:4; then (((N-bound C)-(S-bound C)))*((j1-2)/(2|^m)) <= (((N-bound C)-(S-bound C)))*((j-2)/(2|^n)) by A30,AXIOMS:25; then Gm*(i1,j1)`2 <= Gn*(i,j)`2 by A25,A28,AXIOMS:24; then A39: Gm*(i1,j1)`2 <= p`2 by A38,AXIOMS:22; 1 <= j1+1 & i1 <= len Gauge(C,m) by A17,NAT_1:29,38; then [i1,j1+1] in Indices Gm by A13,A19,GOBOARD7:10; then Gm*(i1,j1+1) =|[(W-bound C)+(((E-bound C)-(W-bound C))/(2|^m))*(i1-2), (S-bound C)+(((N-bound C)-(S-bound C))/(2|^m))*(j1+1-2)]| by JORDAN8:def 1; then A40: Gm*(i1,j1+1)`2 =(S-bound C)+(((N-bound C)-(S-bound C))/(2|^m))*((j1+1-2)/1) by EUCLID:56 .= (S-bound C)+(((N-bound C)-(S-bound C))/1)*((j1+1-2)/(2|^m)) by XCMPLX_1:86; 1 <= j+1 & i <= len Gn by A2,NAT_1:29,38; then [i,j+1] in Indices Gn by A2,A3,GOBOARD7:10; then Gn*(i,j+1) =|[(W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*(i-2), (S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*(j+1-2)]| by JORDAN8:def 1; then A41: Gn*(i,j+1)`2 =(S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*((j+1-2)/1) by EUCLID:56 .= (S-bound C)+(((N-bound C)-(S-bound C))/1)*((j+1-2)/(2|^n)) by XCMPLX_1:86; A42: p`2 <= Gn*(i,j+1)`2 by A2,A3,A20,JORDAN9:19; (j-2)/2|^(n-'m)+2-1 < j1 by INT_1:def 4; then (j-2)/2|^(n-'m)+2 < j1+1 by REAL_1:84; then (j-2)/2|^(n-'m) < j1+1-2 by REAL_1:86; then (j-2) < (j1+1-2)*2|^(n-'m) by A6,A36,REAL_2:177; then (j-2) + 1 <= (j1+1-2)*2|^(n-'m) by INT_1:20; then j+1-2 <= (j1+1-2)*2|^(n-'m) by XCMPLX_1:29; then (j+1-2)/2|^(n-'m) <= j1+1-2 by A6,A36,REAL_2:177; then (j+1-2)/2|^(n-'m)/2|^m <= (j1+1-2)/2|^m by A21,A22,REAL_1:73; then (j+1-2)/(2|^(n-'m)*2|^m) <= (j1+1-2)/2|^m by XCMPLX_1:79; then (j+1-2)/2|^(n-'m+m) <= (j1+1-2)/2|^m by NEWTON:13; then (j+1-2)/2|^n <= (j1+1-2)/2|^m by A1,AMI_5:4; then (((N-bound C)-(S-bound C)))*((j+1-2)/(2|^n)) <= (((N-bound C)-(S-bound C)))*((j1+1-2)/(2|^m)) by A30,AXIOMS:25; then Gn*(i,j+1)`2 <= Gm*(i1,j1+1)`2 by A40,A41,AXIOMS:24; then p`2 <= Gm*(i1,j1+1)`2 by A42,AXIOMS:22; hence e in cell(Gauge(C,m),i1,j1) by A13,A15,A17,A19,A32,A37,A39,JORDAN9:19; end; theorem Th44: m <= n & 1 <= i & i+1 <= len Gauge(C,n) & 1 <= j & j+1 <= width Gauge(C,n) implies ex i1,j1 st 1 <= i1 & i1+1 <= len Gauge(C,m) & 1 <= j1 & j1+1 <= width Gauge(C,m) & cell(Gauge(C,n),i,j) c= cell(Gauge(C,m),i1,j1) proof assume that A1: m <= n and A2: 1 <= i & i+1 <= len Gauge(C,n) and A3: 1 <= j & j+1 <= width Gauge(C,n); consider i1,j1 such that A4: i1 = [\ (i-2)/2|^(n-'m)+2 /] and A5: j1 = [\ (j-2)/2|^(n-'m)+2 /] and A6: cell(Gauge(C,n),i,j) c= cell(Gauge(C,m),i1,j1) by A1,A2,A3,Th43; take i1,j1; thus 1 <= i1 & i1+1 <= len Gauge(C,m) by A1,A2,A4,Th42; len Gauge(C,m) = width Gauge(C,m) & len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; hence 1 <= j1 & j1+1 <= width Gauge(C,m) by A1,A3,A5,Th42; thus thesis by A6; end; canceled 2; theorem for P being Subset of TOP-REAL2 st P is Bounded holds UBD P is not Bounded proof let P be Subset of TOP-REAL2; assume P is Bounded; then ex B being Subset of TOP-REAL 2 st B is_outside_component_of P & B=UBD P by JORDAN2C:76; hence UBD P is not Bounded by JORDAN2C:def 4; end; theorem Th48: for f being non constant standard special_circular_sequence st Rotate(f,p) is clockwise_oriented holds f is clockwise_oriented proof let f be non constant standard special_circular_sequence; assume Rotate(f,p) is clockwise_oriented; then reconsider g = Rotate(f,p) as clockwise_oriented non constant standard special_circular_sequence; 1 < i & i < len f implies f/.i <> f/.1 by GOBOARD7:38; then f = Rotate(g,f/.1) by REVROT_1:16; hence thesis; end; theorem for f being non constant standard special_circular_sequence st LeftComp f = UBD L~f holds f is clockwise_oriented proof let f be non constant standard special_circular_sequence such that A1: LeftComp f = UBD L~f; set g = Rotate(f,N-min L~f); A2: L~f = L~g by REVROT_1:33; assume not thesis; then g is not clockwise_oriented by Th48; then A3: Rev g is clockwise_oriented by REVROT_1:38; UBD L~f = UBD L~Rev g by A2,SPPOL_2:22 .= LeftComp Rev g by A3,GOBRD14:46 .= RightComp g by GOBOARD9:26 .= RightComp f by REVROT_1:37; hence contradiction by A1,SPRECT_4:7; end; begin :: More about cages theorem Th50: for f being non constant standard special_circular_sequence holds (Cl LeftComp(f))` = RightComp f proof let f be non constant standard special_circular_sequence; A1:Cl LeftComp f = (LeftComp f) \/ L~f by GOBRD14:32; A2: Cl LeftComp f \/ RightComp f = L~f \/ LeftComp f \/ RightComp f by GOBRD14:32 .= L~f \/ RightComp f \/ LeftComp f by XBOOLE_1:4 .= the carrier of TOP-REAL 2 by GOBRD14:25; (Cl LeftComp(f))` misses Cl LeftComp(f) by SUBSET_1:44; hence (Cl LeftComp(f))` c= RightComp(f) by A2,XBOOLE_1:73; A3:L~f misses RightComp(f) by SPRECT_3:42; RightComp f misses LeftComp f by GOBRD14:24; then Cl LeftComp(f) misses RightComp(f) by A1,A3,XBOOLE_1:70; hence RightComp(f) c= (Cl LeftComp(f))` by SUBSET_1:43; end; theorem for f being non constant standard special_circular_sequence holds (Cl RightComp(f))` = LeftComp f proof let f be non constant standard special_circular_sequence; A1:Cl RightComp f = (RightComp f) \/ L~f by GOBRD14:31; A2: Cl RightComp f \/ LeftComp f = L~f \/ RightComp f \/ LeftComp f by GOBRD14:31 .= the carrier of TOP-REAL 2 by GOBRD14:25; (Cl RightComp(f))` misses Cl RightComp(f) by SUBSET_1:44; hence (Cl RightComp(f))` c= LeftComp(f) by A2,XBOOLE_1:73; A3:L~f misses LeftComp(f) by SPRECT_3:43; LeftComp f misses RightComp f by GOBRD14:24; then Cl RightComp(f) misses LeftComp(f) by A1,A3,XBOOLE_1:70; hence LeftComp(f) c= (Cl RightComp(f))` by SUBSET_1:43; end; theorem Th52: C is connected implies GoB Cage(C,n) = Gauge(C,n) proof assume A1: C is connected; A2: 1 <= len Gauge(C,n) & 1 <= width Gauge(C,n) by GOBRD11:34; consider iw being Nat such that A3: 1 <= iw & iw <= width Gauge(C,n) and A4: W-min L~Cage(C,n) = Gauge(C,n)*(1,iw) by A1,JORDAN1D:34; A5: [1,iw] in Indices Gauge(C,n) by A2,A3,GOBOARD7:10; A6: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47; consider iS being Nat such that A7: 1 <= iS & iS <= len Gauge(C,n) and A8: Gauge(C,n)*(iS,1) = S-max L~Cage(C,n) by A1,JORDAN1D:32; A9: [iS,1] in Indices Gauge(C,n) by A2,A7,GOBOARD7:10; A10: S-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46; consider ie being Nat such that A11: 1 <= ie & ie <= width Gauge(C,n) and A12: Gauge(C,n)*(len Gauge(C,n),ie) = E-max L~Cage(C,n) by A1,JORDAN1D:29; A13: [len Gauge(C,n),ie] in Indices Gauge(C,n) by A2,A11,GOBOARD7:10; A14: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50; consider IN being Nat such that A15: 1 <= IN & IN <= len Gauge(C,n) and A16: Gauge(C,n)*(IN,width Gauge(C,n)) = N-min L~Cage(C,n) by A1,JORDAN1D:25; A17: [IN,width Gauge(C,n)] in Indices Gauge(C,n) by A2,A15,GOBOARD7:10; A18: N-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43; Cage(C,n) is_sequence_on Gauge(C,n) by A1,JORDAN9:def 1; hence thesis by A4,A5,A6,A8,A9,A10,A12,A13,A14,A16,A17,A18,Th40; end; theorem C is connected implies N-min C in right_cell(Cage(C,n),1) proof assume A1: C is connected; then consider i such that A2: 1 <= i & i+1 <= len Gauge(C,n) and A3: Cage(C,n)/.1 = Gauge(C,n)*(i,width Gauge(C,n)) and A4: Cage(C,n)/.2 = Gauge(C,n)*(i+1,width Gauge(C,n)) and A5: N-min C in cell(Gauge(C,n),i,width Gauge(C,n)-'1) and N-min C <> Gauge(C,n)*(i,width Gauge(C,n)-'1) by JORDAN9:def 1; len Cage(C,n) > 4 by GOBOARD7:36; then A6: 1+1 <= len Cage(C,n) by AXIOMS:22; for i1,j1,i2,j2 being Nat st [i1,j1] in Indices GoB Cage(C,n) & [i2,j2] in Indices GoB Cage(C,n) & Cage(C,n)/.1 = (GoB Cage(C,n))*(i1,j1) & Cage(C,n)/.(1+1) = (GoB Cage(C,n))*(i2,j2) holds i1 = i2 & j1+1 = j2 & cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i1,j1) or i1+1 = i2 & j1 = j2 & cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i1,j1-'1) or i1 = i2+1 & j1 = j2 & cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i2,j2) or i1 = i2 & j1 = j2+1 & cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i1-'1,j2) proof let i1,j1,i2,j2 be Nat such that A7: [i1,j1] in Indices GoB Cage(C,n) and A8: [i2,j2] in Indices GoB Cage(C,n) and A9: Cage(C,n)/.1 = (GoB Cage(C,n))*(i1,j1) and A10: Cage(C,n)/.(1+1) = (GoB Cage(C,n))*(i2,j2); A11: GoB Cage(C,n) = Gauge(C,n) by A1,Th52; 0 <> width Gauge(C,n) by GOBOARD1:def 5; then A12: 1 <= width Gauge(C,n) by RLVECT_1:99; i < len Gauge(C,n) by A2,NAT_1:38; then A13: [i,width Gauge(C,n)] in Indices Gauge(C,n) by A2,A12,GOBOARD7:10; then A14: i1 = i & j1 = width Gauge(C,n) by A3,A7,A9,A11,GOBOARD1:21; 1 <= i+1 by NAT_1:29; then [i+1,width Gauge(C,n)] in Indices Gauge(C,n) by A2,A12,GOBOARD7:10; then A15: i2 = i+1 & j2 = width Gauge(C,n) by A4,A8,A10,A11,GOBOARD1:21; per cases by A3,A7,A9,A11,A13,A15,GOBOARD1:21; case i1 = i2 & j1+1 = j2; hence cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i1,j1) by A14,A15,NAT_1:38; case i1+1 = i2 & j1 = j2; thus cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i1,j1-'1) by A1,A14,Th52; case i1 = i2+1 & j1 = j2; then i2 < i1 by NAT_1:38; hence cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i2,j2) by A14,A15,NAT_1:38; case i1 = i2 & j1 = j2+1; hence cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i1-'1,j2) by A14,A15,NAT_1:38; end; hence thesis by A5,A6,GOBOARD5:def 6; end; theorem Th54: C is connected & i <= j implies L~Cage(C,j) c= Cl RightComp(Cage(C,i)) proof assume that A1: C is connected and A2: i <= j and A3: not L~Cage(C,j) c= Cl RightComp(Cage(C,i)); A4: Cage(C,j) is_sequence_on Gauge(C,j) by A1,JORDAN9:def 1; consider p being Point of TOP-REAL 2 such that A5: p in L~Cage(C,j) and A6: not p in Cl RightComp(Cage(C,i)) by A3,SUBSET_1:7; reconsider D = (L~Cage(C,i))` as Subset of TOP-REAL 2; consider i1 such that A7: 1 <= i1 and A8: i1+1 <= len Cage(C,j) and A9: p in LSeg(Cage(C,j),i1) by A5,SPPOL_2:13; A10: i1 < len Cage(C,j) by A8,NAT_1:38; A11: GoB Cage(C,i) = Gauge(C,i) by A1,Th52; A12: GoB Cage(C,j) = Gauge(C,j) by A1,Th52; then A13: right_cell(Cage(C,j),i1,Gauge(C,j)) = right_cell(Cage(C,j),i1) by A7,A8,Th29; A14: now assume A15: not right_cell(Cage(C,j),i1) c= Cl LeftComp Cage(C,i); ex i2,j2 being Nat st 1 <= i2 & i2+1 <= len Gauge(C,i) & 1 <= j2 & j2+1 <= width Gauge(C,i) & right_cell(Cage(C,j),i1) c= cell(Gauge(C,i),i2,j2) proof set f = Cage(C,j); A16: i1 in dom f by A7,A10,FINSEQ_3:27; then consider i4,j4 being Nat such that A17: [i4,j4] in Indices Gauge(C,j) and A18: f/.i1 = (Gauge(C,j))*(i4,j4) by A4,GOBOARD1:def 11; A19: 1 <= i4 & i4 <= len Gauge(C,j) by A17,GOBOARD5:1; A20: 1 <= j4 & j4 <= width Gauge(C,j) by A17,GOBOARD5:1; 1 <= i1+1 by NAT_1:29; then A21: i1+1 in dom f by A8,FINSEQ_3:27; then consider i5,j5 being Nat such that A22: [i5,j5] in Indices Gauge(C,j) and A23: f/.(i1+1) = (Gauge(C,j))*(i5,j5) by A4,GOBOARD1:def 11; A24: 1 <= i5 & i5 <= len Gauge(C,j) by A22,GOBOARD5:1; A25: 1 <= j5 & j5 <= width Gauge(C,j) by A22,GOBOARD5:1; right_cell(f,i1) = right_cell(f,i1); then A26: i4 = i5 & j4+1 = j5 & right_cell(f,i1) = cell(GoB f,i4,j4) or i4+1 = i5 & j4 = j5 & right_cell(f,i1) = cell(GoB f,i4,j4-'1) or i4 = i5+1 & j4 = j5 & right_cell(f,i1) = cell(GoB f,i5,j5) or i4 = i5 & j4 = j5+1 & right_cell(f,i1) = cell(GoB f,i4-'1,j5) by A7,A8,A12,A17,A18,A22,A23,GOBOARD5:def 6; A27: j4+1+1 = j4+(1+1) by XCMPLX_1:1; A28: i4+1+1 = i4+(1+1) by XCMPLX_1:1; abs(i4-i5)+abs(j4-j5) = 1 by A4,A16,A17,A18,A21,A22,A23,GOBOARD1:def 11; then A29: abs(i4-i5)=1 & j4=j5 or abs(j4-j5)=1 & i4=i5 by GOBOARD1:2; per cases by A29,GOBOARD1:1; suppose A30: i4 = i5 & j4+1 = j5; then i4 < len Gauge(C,j) by A1,A7,A8,A17,A18,A22,A23,JORDAN10:1; then i4+1 <= len Gauge(C,j) by NAT_1:38; hence thesis by A2,A12,A19,A20,A25,A26,A27,A30,Th44,REAL_1:69; suppose A31: i4+1 = i5 & j4 = j5; A32: j4-'1+1 = j4 by A20,AMI_5:4; 1 < j4 by A1,A7,A8,A17,A18,A22,A23,A31,JORDAN10:3; then 1+1 <= j4 by NAT_1:38; then 1 <= j4-'1 by JORDAN5B:2; hence thesis by A2,A12,A19,A20,A24,A26,A28,A31,A32,Th44,REAL_1:69; suppose A33: i4 = i5+1 & j4 = j5; then j5 < width Gauge(C,j) by A1,A7,A8,A17,A18,A22,A23,JORDAN10:4; then j5+1 <= width Gauge(C,j) by NAT_1:38; hence thesis by A2,A12,A19,A24,A25,A26,A28,A33,Th44,REAL_1:69; suppose A34: i4 = i5 & j4 = j5+1; A35: i4-'1+1 = i4 by A19,AMI_5:4; 1 < i4 by A1,A7,A8,A17,A18,A22,A23,A34,JORDAN10:2; then 1+1 <= i4 by NAT_1:38; then 1 <= i4-'1 by JORDAN5B:2; hence thesis by A2,A12,A19,A20,A25,A26,A27,A34,A35,Th44,REAL_1:69; end; then consider i2,j2 being Nat such that A36: 1 <= i2 & i2+1 <= len Gauge(C,i) and A37: 1 <= j2 & j2+1 <= width Gauge(C,i) and A38: right_cell(Cage(C,j),i1) c= cell(Gauge(C,i),i2,j2); A39: i2< len Gauge(C,i) by A36,NAT_1:38; A40: j2 < width Gauge(C,i) by A37,NAT_1:38; A41: not cell(Gauge(C,i),i2,j2) c= Cl LeftComp Cage(C,i) by A15,A38,XBOOLE_1:1 ; Cl LeftComp Cage(C,i) \/ RightComp Cage(C,i) = L~Cage(C,i) \/ LeftComp Cage(C,i) \/ RightComp Cage(C,i) by GOBRD14:32 .= L~Cage(C,i) \/ RightComp Cage(C,i) \/ LeftComp Cage(C,i) by XBOOLE_1:4 .= the carrier of TOP-REAL 2 by GOBRD14:25; then A42: cell(Gauge(C,i),i2,j2) meets RightComp Cage(C,i) by A41,XBOOLE_1 :73; cell(Gauge(C,i),i2,j2) = Cl Int cell(Gauge(C,i),i2,j2) by A39,A40,GOBRD11:35; then A43: Int cell(Gauge(C,i),i2,j2) meets RightComp Cage(C,i) by A42,TSEP_1:40; A44: Int cell(Gauge(C,i),i2,j2) c= (L~Cage(C,i))` by A11,A39,A40,GOBRD12:2; A45: RightComp Cage(C,i) is_a_component_of (L~Cage(C,i))` by GOBOARD9:def 2; Int cell(Gauge(C,i),i2,j2) is connected by A39,A40,GOBOARD9:21; then A46: Int cell(Gauge(C,i),i2,j2) c= RightComp Cage(C,i) by A43,A44,A45,JORDAN1A:8; Int right_cell(Cage(C,j),i1) c= Int cell(Gauge(C,i),i2,j2) by A38,TOPS_1:48; then Int right_cell(Cage(C,j),i1) c= RightComp Cage(C,i) by A46,XBOOLE_1:1 ; then Cl Int right_cell(Cage(C,j),i1) c= Cl RightComp Cage(C,i) by PRE_TOPC:49; then A47: right_cell(Cage(C,j),i1) c= Cl RightComp Cage(C,i) by A4,A7,A8,A13,JORDAN9:13; A48: LSeg(Cage(C,j),i1) c= right_cell(Cage(C,j),i1,Gauge(C,j)) by A4,A7,A8,Th28; right_cell(Cage(C,j),i1,Gauge(C,j)) c= right_cell(Cage(C,j),i1) by A4,A7,A8,GOBRD13:34; then LSeg(Cage(C,j),i1) c= right_cell(Cage(C,j),i1) by A48,XBOOLE_1:1; then LSeg(Cage(C,j),i1) c= Cl RightComp Cage(C,i) by A47,XBOOLE_1:1; hence contradiction by A6,A9; end; A49: C c= RightComp Cage(C,i) by A1,JORDAN10:11; right_cell(Cage(C,j),i1,Gauge(C,j)) meets C by A1,A7,A8,JORDAN9:33; then A50: C meets Cl LeftComp Cage(C,i) by A13,A14,XBOOLE_1:63; A51: Cl LeftComp Cage(C,i) = LeftComp Cage(C,i) \/ L~Cage(C,i) by GOBRD14:32; C misses L~Cage(C,i) by A1,JORDAN10:5; then A52: C meets LeftComp Cage(C,i) by A50,A51,XBOOLE_1:70; A53: LeftComp Cage(C,i) is_a_component_of D by GOBOARD9:def 1; D = LeftComp Cage(C,i) \/ RightComp Cage(C,i) by GOBRD12:11; then RightComp Cage(C,i) c= D by XBOOLE_1:7; then A54: C c= D by A49,XBOOLE_1:1; A55: RightComp Cage(C,i) is_a_component_of D by GOBOARD9:def 2; C meets C; then C meets RightComp Cage(C,i) by A49,XBOOLE_1:63; then LeftComp Cage(C,i) = RightComp Cage(C,i) by A1,A52,A53,A54,A55,JORDAN9:3 ; hence contradiction by SPRECT_4:7; end; theorem Th55: C is connected & i <= j implies LeftComp(Cage(C,i)) c= LeftComp(Cage(C,j)) proof assume that A1: C is connected and A2: i <= j; set p = |[E-bound L~Cage(C,i) + 1,0]|; p`1 = E-bound L~Cage(C,i) + 1 by EUCLID:56; then A3: p`1 > E-bound (L~Cage(C,i)) by REAL_1:69; Cage(C,i)/.1 = N-min L~Cage(C,i) by A1,JORDAN9:34; then A4: p in LeftComp Cage(C,i) by A3,JORDAN2C:119; i < j or i = j by A2,AXIOMS:21; then E-bound (L~Cage(C,i)) > E-bound (L~Cage(C,j)) or E-bound (L~Cage(C,i)) = E-bound (L~Cage(C,j)) by A1,JORDAN1A:88; then A5: p`1 > E-bound (L~Cage(C,j)) by A3,AXIOMS:22; Cage(C,j)/.1 = N-min L~Cage(C,j) by A1,JORDAN9:34; then p in LeftComp Cage(C,j) by A5,JORDAN2C:119; then A6:LeftComp(Cage(C,i)) meets LeftComp(Cage(C,j)) by A4,XBOOLE_0:3; A7: LeftComp(Cage(C,j)) is_a_component_of (L~Cage(C,j))` by GOBOARD9:def 1; A8: L~Cage(C,j) c= Cl RightComp(Cage(C,i)) by A1,A2,Th54; A9:Cl RightComp Cage(C,i) = (RightComp Cage(C,i)) \/ L~Cage(C,i) by GOBRD14:31; A10:L~Cage(C,i) misses LeftComp(Cage(C,i)) by SPRECT_3:43; LeftComp Cage(C,i) misses RightComp Cage(C,i) by GOBRD14:24; then Cl RightComp(Cage(C,i)) misses LeftComp(Cage(C,i)) by A9,A10,XBOOLE_1:70 ; then L~Cage(C,j) misses LeftComp(Cage(C,i)) by A8,XBOOLE_1:63; then LeftComp(Cage(C,i)) c= (L~Cage(C,j))` by SUBSET_1:43; hence LeftComp(Cage(C,i)) c= LeftComp(Cage(C,j)) by A6,A7,JORDAN1A:8; end; theorem C is connected & i <= j implies RightComp(Cage(C,j)) c= RightComp(Cage(C,i)) proof assume that A1: C is connected and A2: i <= j; LeftComp(Cage(C,i)) c= LeftComp(Cage(C,j)) by A1,A2,Th55; then A3: Cl LeftComp(Cage(C,i)) c= Cl LeftComp(Cage(C,j)) by PRE_TOPC:49; (Cl LeftComp(Cage(C,i)))` = RightComp(Cage(C,i)) & (Cl LeftComp(Cage(C,j)))` = RightComp(Cage(C,j)) by Th50; hence RightComp(Cage(C,j)) c= RightComp(Cage(C,i)) by A3,SUBSET_1:31; end; begin :: Preparing the Internal Approximation definition let C,n; func X-SpanStart(C,n) -> Nat equals :Def2: 2|^(n-'1) + 2; correctness; end; theorem X-SpanStart(C,n) = Center Gauge(C,n) proof thus X-SpanStart(C,n) = 2|^(n-'1) + 2 by Def2 .= Center Gauge(C,n) by JORDAN1B:17; end; theorem Th58: 2 < X-SpanStart(C,n) & X-SpanStart(C,n) < len Gauge(C,n) proof 2|^(n-'1) > 0 by HEINE:5; then 2|^(n-'1) + 2 > 0+2 by REAL_1:53; hence 2 < X-SpanStart(C,n) by Def2; A1: len Gauge(C,n) = 2|^n + 3 by JORDAN8:def 1; A2: X-SpanStart(C,n) = 2|^(n-'1) + 2 by Def2; n-'1 <= n by JORDAN3:7; then 2|^(n-'1) <= 2|^n by PCOMPS_2:4; hence X-SpanStart(C,n) < len Gauge(C,n) by A1,A2,REAL_1:67; end; theorem Th59: 1 <= X-SpanStart(C,n)-'1 & X-SpanStart(C,n)-'1 < len Gauge(C,n) proof 2 < X-SpanStart(C,n) by Th58; then A1: 1 < X-SpanStart(C,n) by AXIOMS:22; then X-SpanStart(C,n)-'1+1 = X-SpanStart(C,n) by AMI_5:4; hence 1 <= X-SpanStart(C,n)-'1 by A1,NAT_1:38; A2: X-SpanStart(C,n) < len Gauge(C,n) by Th58; X-SpanStart(C,n)-'1 <= X-SpanStart(C,n) by JORDAN3:7; hence X-SpanStart(C,n)-'1 < len Gauge(C,n) by A2,AXIOMS:22; end; definition let C,n; pred n is_sufficiently_large_for C means :Def3: ex j st j < width Gauge(C,n) & cell(Gauge(C,n),X-SpanStart(C,n)-'1,j) c= BDD C; end; theorem n is_sufficiently_large_for C implies n >= 1 proof assume n is_sufficiently_large_for C; then consider j such that A1: j < width Gauge(C,n) and A2: cell(Gauge(C,n),X-SpanStart(C,n)-'1,j) c= BDD C by Def3; A3: width Gauge(C,n) = 2|^n + 3 by JORDAN1A:49; A4: j > 1 proof A5: X-SpanStart(C,n)-'1 <= len Gauge(C,n) by Th59; assume A6: j <= 1; per cases by A6,CQC_THE1:2; suppose A7: j = 0; 0 <= width Gauge(C,n) by NAT_1:18; then A8: cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) is non empty by A5,JORDAN1A: 45; cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= UBD C by A5,JORDAN1A:70; then UBD C meets BDD C by A2,A7,A8,XBOOLE_1:68; hence contradiction by JORDAN2C:28; suppose A9: j = 1; width Gauge(C,n) <> 0 by GOBOARD1:def 5; then A10: 0+1 <= width Gauge(C,n) by RLVECT_1:99; then A11: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) is non empty by A5,JORDAN1A :45; A12: cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= UBD C by A5,JORDAN1A:70; set i1 = X-SpanStart(C,n); A13: C is Bounded by JORDAN2C:73; A14: i1 < len Gauge(C,n) by Th58; i1-'1 <= i1 by JORDAN3:7; then A15: i1-'1 < len Gauge(C,n) by A14,AXIOMS:22; A16: 0 < width Gauge(C,n) by A10,NAT_1:38; 1 <= i1-'1 by Th59; then cell(Gauge(C,n),i1-'1,0) /\ cell(Gauge(C,n),i1-'1,0+1) = LSeg(Gauge(C,n)*(i1-'1,0+1),Gauge(C,n)*(i1-'1+1,0+1)) by A15,A16,GOBOARD5:27; then A17: cell(Gauge(C,n),i1-'1,0) meets cell(Gauge(C,n),i1-'1,0+1) by XBOOLE_0:def 7; ex B being Subset of TOP-REAL 2 st B is_outside_component_of C & B=UBD C by A13,JORDAN2C:76; then A18: UBD C is_a_component_of C` by JORDAN2C:def 4; A19: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) is connected by A10,A15,JORDAN1A: 46; BDD C c= C` by JORDAN2C:29; then cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= C` by A2,A9,XBOOLE_1:1; then cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= UBD C by A12,A17,A18,A19, GOBOARD9:6; then UBD C meets BDD C by A2,A9,A11,XBOOLE_1:68; hence contradiction by JORDAN2C:28; end; A20: j + 1 < width Gauge(C,n) proof A21: X-SpanStart(C,n)-'1 <= len Gauge(C,n) by Th59; assume j + 1 >= width Gauge(C,n); then A22: j + 1 > width Gauge(C,n) or j + 1 = width Gauge(C,n) by AXIOMS:21; per cases by A1,A22,NAT_1:38; suppose A23: j = width Gauge(C,n); A24: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)) is non empty by A21,JORDAN1A:45; cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)) c= UBD C by A21, JORDAN1A:71; then UBD C meets BDD C by A2,A23,A24,XBOOLE_1:68; hence contradiction by JORDAN2C:28; suppose j + 1 = width Gauge(C,n); then A25: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) c= BDD C by A2,BINARITH:39; width Gauge(C,n)-'1 <= width Gauge(C,n) by JORDAN3:7; then A26: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) is non empty by A21,JORDAN1A:45; A27: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)) c= UBD C by A21, JORDAN1A:71 ; set i1 = X-SpanStart(C,n); A28: C is Bounded by JORDAN2C:73; A29: i1 < len Gauge(C,n) by Th58; width Gauge(C,n) <> 0 by GOBOARD1:def 5; then A30: 0+1 <= width Gauge(C,n) by RLVECT_1:99; i1-'1 <= i1 by JORDAN3:7; then A31: i1-'1 < len Gauge(C,n) by A29,AXIOMS:22; width Gauge(C,n)-1 < width Gauge(C,n) by INT_1:26; then A32: width Gauge(C,n)-'1 < width Gauge(C,n) by A30,SCMFSA_7:3; A33: width Gauge(C,n)-'1+1 = width Gauge(C,n) by A30,AMI_5:4; 1 <= i1-'1 by Th59; then cell(Gauge(C,n),i1-'1,width Gauge(C,n)) /\ cell(Gauge(C,n),i1-'1,width Gauge(C,n)-'1) = LSeg(Gauge(C,n)*(i1-'1,width Gauge(C,n)), Gauge(C,n)*(i1-'1+1,width Gauge(C,n))) by A31,A32,A33,GOBOARD5:27; then A34: cell(Gauge(C,n),i1-'1,width Gauge(C,n)) meets cell(Gauge(C,n),i1-'1,width Gauge(C,n)-'1) by XBOOLE_0:def 7; ex B being Subset of TOP-REAL 2 st B is_outside_component_of C & B=UBD C by A28,JORDAN2C:76; then A35: UBD C is_a_component_of C` by JORDAN2C:def 4; A36: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) is connected by A31,A32,JORDAN1A:46; BDD C c= C` by JORDAN2C:29; then cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) c= C` by A25,XBOOLE_1:1; then cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) c= UBD C by A27,A34,A35,A36,GOBOARD9:6; then UBD C meets BDD C by A25,A26,XBOOLE_1:68; hence contradiction by JORDAN2C:28; end; A37: 2|^0 = 1 by NEWTON:9; assume n < 1; then A38: n = 0 by RLVECT_1:99; per cases by A1,A3,A37,A38,CQC_THE1:5; suppose j= 0 or j=1; hence thesis by A4; suppose A39: j=2; A40: X-SpanStart(C,0) = 2|^(0-'1) + 2 by Def2 .= 1 + 2 by A37,POLYNOM4:1; then X-SpanStart(C,0)-'1 = X-SpanStart(C,0)-1 by JORDAN3:1 .= 2 by A40; hence contradiction by A2,A38,A39,JORDAN1B:19; suppose j=3 or j=4; hence thesis by A3,A20,A37,A38; end; theorem for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j1 being Nat st left_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j1) & [i1,j1+1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1,j1+1) holds [i1-'1,j1+1] in Indices Gauge(C,n) proof let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2; let n; set G = Gauge(C,n); A1: len G = width G by JORDAN8:def 1; let f be FinSequence of TOP-REAL 2 such that A2: f is_sequence_on G and A3: len f > 1; let i1,j1 being Nat such that A4: left_cell(f,(len f)-'1,G) meets C and A5: [i1,j1] in Indices G & f/.((len f) -'1) = G*(i1,j1) and A6: [i1,j1+1] in Indices G & f/.len f = G*(i1,j1+1); A7: 1 <= (len f)-'1 by A3,JORDAN3:12; A8: (len f) -'1 +1 = len f by A3,AMI_5:4; A9: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A5,GOBOARD5:1; A10: 1 <= i1 & i1 <= len G & 1 <= j1+1 & j1+1 <= width G by A6,GOBOARD5:1; i1-'1 <= i1 by GOBOARD9:2; then A11: i1-'1 <= len G by A9,AXIOMS:22; now assume i1-'1 < 1; then i1-'1 = 0 by RLVECT_1:98; then i1 <= 1 by JORDAN4:1; then i1 = 1 by A10,AXIOMS:21; then cell(G,1-'1,j1) meets C by A2,A4,A5,A6,A7,A8,GOBRD13:22; then cell(G,0,j1) meets C by GOBOARD9:1; hence contradiction by A1,A9,JORDAN8:21; end; hence [i1-'1,j1+1] in Indices G by A10,A11,GOBOARD7:10; end; theorem for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j1 being Nat st left_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j1) & [i1+1,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1+1,j1) holds [i1+1,j1+1] in Indices Gauge(C,n) proof let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2; let n; set G = Gauge(C,n); let f be FinSequence of TOP-REAL 2 such that A1: f is_sequence_on G and A2: len f > 1; A3: len G = width G by JORDAN8:def 1; let i1,j1 being Nat such that A4: left_cell(f,(len f)-'1,G) meets C and A5: [i1,j1] in Indices G & f/.((len f) -'1) = G*(i1,j1) and A6: [i1+1,j1] in Indices G & f/.len f = G*(i1+1,j1); A7: 1 <= (len f)-'1 by A2,JORDAN3:12; A8: (len f) -'1 +1 = len f by A2,AMI_5:4; A9: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A5,GOBOARD5:1; A10: 1 <= i1+1 & i1+1 <= len G & 1 <= j1 & j1 <= width G by A6,GOBOARD5:1; A11: 1 <= j1+1 by NAT_1:29; now assume j1+1 > len G; then j1+1 <= (len G)+1 & (len G)+1 <= j1+1 by A3,A10,AXIOMS:24,NAT_1:38; then j1+1 = (len G)+1 by AXIOMS:21; then j1 = len G by XCMPLX_1:2; then cell(G,i1,len G) meets C by A1,A4,A5,A6,A7,A8,GOBRD13:24; hence contradiction by A9,JORDAN8:18; end; hence [i1+1,j1+1] in Indices G by A3,A10,A11,GOBOARD7:10; end; theorem for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for j1,i2 being Nat st left_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i2+1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i2+1,j1) & [i2,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i2,j1) holds [i2,j1-'1] in Indices Gauge(C,n) proof let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2; let n; set G = Gauge(C,n); let f be FinSequence of TOP-REAL 2 such that A1: f is_sequence_on G and A2: len f > 1; let j1,i2 being Nat such that A3: left_cell(f,(len f)-'1,G) meets C and A4: [i2+1,j1] in Indices G & f/.((len f) -'1) = G*(i2+1,j1) and A5: [i2,j1] in Indices G & f/.len f = G*(i2,j1); A6: 1 <= (len f)-'1 by A2,JORDAN3:12; A7: (len f) -'1 +1 = len f by A2,AMI_5:4; A8: 1 <= i2 & i2 <= len G & 1 <= j1 & j1 <= width G by A5,GOBOARD5:1; j1-'1 <= j1 by GOBOARD9:2; then A9: j1-'1 <= width G by A8,AXIOMS:22; now assume j1-'1 < 1; then j1-'1 = 0 by RLVECT_1:98; then j1 <= 1 by JORDAN4:1; then j1 = 1 by A8,AXIOMS:21; then cell(G,i2,1-'1) meets C by A1,A3,A4,A5,A6,A7,GOBRD13:26; then cell(G,i2,0) meets C by GOBOARD9:1; hence contradiction by A8,JORDAN8:20; end; hence [i2,j1-'1] in Indices G by A8,A9,GOBOARD7:10; end; theorem for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j2 being Nat st left_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i1,j2+1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j2+1) & [i1,j2] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1,j2) holds [i1+1,j2] in Indices Gauge(C,n) proof let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2; let n; set G = Gauge(C,n); A1: len G = width G by JORDAN8:def 1; let f be FinSequence of TOP-REAL 2 such that A2: f is_sequence_on G and A3: len f > 1; let i1,j2 being Nat such that A4: left_cell(f,(len f)-'1,G) meets C and A5: [i1,j2+1] in Indices G & f/.((len f) -'1) = G*(i1,j2+1) and A6: [i1,j2] in Indices G & f/.len f = G*(i1,j2); A7: 1 <= (len f)-'1 by A3,JORDAN3:12; A8: (len f) -'1 +1 = len f by A3,AMI_5:4; A9: 1 <= i1 & i1 <= len G & 1 <= j2 & j2 <= width G by A6,GOBOARD5:1; A10: 1 <= i1+1 by NAT_1:29; now assume i1+1 > len G; then i1+1 <= (len G)+1 & (len G)+1 <= i1+1 by A9,AXIOMS:24,NAT_1:38; then i1+1 = (len G)+1 by AXIOMS:21; then i1 = len G by XCMPLX_1:2; then cell(G,len G,j2) meets C by A2,A4,A5,A6,A7,A8,GOBRD13:28; hence contradiction by A1,A9,JORDAN8:19; end; hence [i1+1,j2] in Indices G by A9,A10,GOBOARD7:10; end; theorem for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j1 being Nat st front_left_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j1) & [i1,j1+1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1,j1+1) holds [i1,j1+2] in Indices Gauge(C,n) proof let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2; let n; set G = Gauge(C,n); A1: len G = width G by JORDAN8:def 1; let f be FinSequence of TOP-REAL 2 such that A2: f is_sequence_on G and A3: len f > 1; let i1,j1 being Nat such that A4: front_left_cell(f,(len f)-'1,G) meets C and A5: [i1,j1] in Indices G & f/.((len f) -'1) = G*(i1,j1) and A6: [i1,j1+1] in Indices G & f/.len f = G*(i1,j1+1); A7: 1 <= (len f)-'1 by A3,JORDAN3:12; A8: (len f) -'1 +1 = len f by A3,AMI_5:4; A9: 1 <= i1 & i1 <= len G & 1 <= j1+1 & j1+1 <= width G by A6,GOBOARD5:1; A10: 1 <= i1+1 & 1 <= j1+1+1 by NAT_1:37; i1-'1 <= i1 by GOBOARD9:2; then A11: i1-'1 <= len G by A9,AXIOMS:22; A12: j1+1+1 = j1+(1+1) by XCMPLX_1:1; now assume j1+1+1 > len G; then j1+1+1 <= (len G)+1 & (len G)+1 <= j1+1+1 by A1,A9,AXIOMS:24,NAT_1:38; then j1+1+1 = (len G)+1 by AXIOMS:21; then j1+1 = len G by XCMPLX_1:2; then cell(G,i1-'1,len G) meets C by A2,A4,A5,A6,A7,A8,GOBRD13:35; hence contradiction by A11,JORDAN8:18; end; hence [i1,j1+2] in Indices G by A1,A9,A10,A12,GOBOARD7:10; end; theorem for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j1 being Nat st front_left_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j1) & [i1+1,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1+1,j1) holds [i1+2,j1] in Indices Gauge(C,n) proof let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2; let n; set G = Gauge(C,n); A1: len G = width G by JORDAN8:def 1; let f be FinSequence of TOP-REAL 2 such that A2: f is_sequence_on G and A3: len f > 1; let i1,j1 being Nat such that A4: front_left_cell(f,(len f)-'1,G) meets C and A5: [i1,j1] in Indices G & f/.((len f) -'1) = G*(i1,j1) and A6: [i1+1,j1] in Indices G & f/.len f = G*(i1+1,j1); A7: 1 <= (len f)-'1 by A3,JORDAN3:12; A8: (len f) -'1 +1 = len f by A3,AMI_5:4; A9: 1 <= i1+1 & i1+1 <= len G & 1 <= j1 & j1 <= width G by A6,GOBOARD5:1; A10: 1 <= i1+1+1 & 1 <= j1+1 by NAT_1:37; A11: i1+1+1 = i1 +(1+1) by XCMPLX_1:1; now assume i1+1+1 > len G; then i1+1+1 <= (len G)+1 & (len G)+1 <= i1+1+1 by A9,AXIOMS:24,NAT_1:38; then i1+1+1 = (len G)+1 by AXIOMS:21; then i1+1 = len G by XCMPLX_1:2; then cell(G,len G,j1) meets C by A2,A4,A5,A6,A7,A8,GOBRD13:37; hence contradiction by A1,A9,JORDAN8:19; end; hence [i1+2,j1] in Indices G by A9,A10,A11,GOBOARD7:10; end; theorem for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for j1,i2 being Nat st front_left_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i2+1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i2+1,j1) & [i2,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i2,j1) holds [i2-'1,j1] in Indices Gauge(C,n) proof let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2; let n; set G = Gauge(C,n); A1: len G = width G by JORDAN8:def 1; let f be FinSequence of TOP-REAL 2 such that A2: f is_sequence_on G and A3: len f > 1; let j1,i2 being Nat such that A4: front_left_cell(f,(len f)-'1,G) meets C and A5: [i2+1,j1] in Indices G & f/.((len f) -'1) = G*(i2+1,j1) and A6: [i2,j1] in Indices G & f/.len f = G*(i2,j1); A7: 1 <= (len f)-'1 by A3,JORDAN3:12; A8: (len f) -'1 +1 = len f by A3,AMI_5:4; A9: 1 <= i2 & i2 <= len G & 1 <= j1 & j1 <= width G by A6,GOBOARD5:1; then A10: i2-'1 <= len G & j1-'1 <= width G by JORDAN3:7; now assume i2-'1 < 1; then i2-'1 = 0 by RLVECT_1:98; then i2 <= 1 by JORDAN4:1; then i2 = 1 by A9,AXIOMS:21; then cell(G,1-'1,j1-'1) meets C by A2,A4,A5,A6,A7,A8,GOBRD13:39; then cell(G,0,j1-'1) meets C by GOBOARD9:1; hence contradiction by A1,A10,JORDAN8:21; end; hence [i2-'1,j1] in Indices G by A9,A10,GOBOARD7:10; end; theorem for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j2 being Nat st front_left_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i1,j2+1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j2+1) & [i1,j2] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1,j2) holds [i1,j2-'1] in Indices Gauge(C,n) proof let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2; let n; set G = Gauge(C,n); let f be FinSequence of TOP-REAL 2 such that A1: f is_sequence_on G and A2: len f > 1; let i1,j2 being Nat such that A3: front_left_cell(f,(len f)-'1,G) meets C and A4: [i1,j2+1] in Indices G & f/.((len f) -'1) = G*(i1,j2+1) and A5: [i1,j2] in Indices G & f/.len f = G*(i1,j2); A6: 1 <= (len f)-'1 by A2,JORDAN3:12; A7: (len f) -'1 +1 = len f by A2,AMI_5:4; A8: 1 <= i1 & i1 <= len G & 1 <= j2+1 & j2+1 <= width G by A4,GOBOARD5:1; A9: 1 <= i1 & i1 <= len G & 1 <= j2 & j2 <= width G by A5,GOBOARD5:1; then A10: i1-'1 <= len G & j2-'1 <= width G by JORDAN3:7; now assume j2-'1 < 1; then j2-'1 = 0 by RLVECT_1:98; then j2 <= 1 by JORDAN4:1; then j2 = 1 by A9,AXIOMS:21; then cell(G,i1,1-'1) meets C by A1,A3,A4,A5,A6,A7,GOBRD13:41; then cell(G,i1,0) meets C by GOBOARD9:1; hence contradiction by A8,JORDAN8:20; end; hence [i1,j2-'1] in Indices G by A9,A10,GOBOARD7:10; end; theorem for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j1 being Nat st front_right_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j1) & [i1,j1+1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1,j1+1) holds [i1+1,j1+1] in Indices Gauge(C,n) proof let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2; let n; set G = Gauge(C,n); A1: len G = width G by JORDAN8:def 1; let f be FinSequence of TOP-REAL 2 such that A2: f is_sequence_on G and A3: len f > 1; let i1,j1 being Nat such that A4: front_right_cell(f,(len f)-'1,G) meets C and A5: [i1,j1] in Indices G & f/.((len f) -'1) = G*(i1,j1) and A6: [i1,j1+1] in Indices G & f/.len f = G*(i1,j1+1); A7: 1 <= (len f)-'1 by A3,JORDAN3:12; A8: (len f) -'1 +1 = len f by A3,AMI_5:4; A9: 1 <= i1 & i1 <= len G & 1 <= j1+1 & j1+1 <= width G by A6,GOBOARD5:1; A10: 1 <= i1+1 by NAT_1:29; now assume i1+1 > len G; then i1+1 <= (len G)+1 & (len G)+1 <= i1+1 by A9,AXIOMS:24,NAT_1:38; then i1+1 = (len G)+1 by AXIOMS:21; then i1 = len G by XCMPLX_1:2; then cell(G,len G,j1+1) meets C by A2,A4,A5,A6,A7,A8,GOBRD13:36; hence contradiction by A1,A9,JORDAN8:19; end; hence [i1+1,j1+1] in Indices G by A9,A10,GOBOARD7:10; end; theorem for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j1 being Nat st front_right_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j1) & [i1+1,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1+1,j1) holds [i1+1,j1-'1] in Indices Gauge(C,n) proof let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2; let n; set G = Gauge(C,n); let f be FinSequence of TOP-REAL 2 such that A1: f is_sequence_on G and A2: len f > 1; let i1,j1 being Nat such that A3: front_right_cell(f,(len f)-'1,G) meets C and A4: [i1,j1] in Indices G & f/.((len f) -'1) = G*(i1,j1) and A5: [i1+1,j1] in Indices G & f/.len f = G*(i1+1,j1); A6: 1 <= (len f)-'1 by A2,JORDAN3:12; A7: (len f) -'1 +1 = len f by A2,AMI_5:4; A8: 1 <= i1+1 & i1+1 <= len G & 1 <= j1 & j1 <= width G by A5,GOBOARD5:1; j1-'1 <= j1 by GOBOARD9:2; then A9: j1-'1 <= width G by A8,AXIOMS:22; now assume j1-'1 < 1; then j1-'1 = 0 by RLVECT_1:98; then j1 <= 1 by JORDAN4:1; then j1 = 1 by A8,AXIOMS:21; then cell(G,i1+1,1-'1) meets C by A1,A3,A4,A5,A6,A7,GOBRD13:38; then cell(G,i1+1,0) meets C by GOBOARD9:1; hence contradiction by A8,JORDAN8:20; end; hence [i1+1,j1-'1] in Indices G by A8,A9,GOBOARD7:10; end; theorem for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for j1,i2 being Nat st front_right_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i2+1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i2+1,j1) & [i2,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i2,j1) holds [i2,j1+1] in Indices Gauge(C,n) proof let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2; let n; set G = Gauge(C,n); let f be FinSequence of TOP-REAL 2 such that A1: f is_sequence_on G and A2: len f > 1; let j1,i2 being Nat such that A3: front_right_cell(f,(len f)-'1,G) meets C and A4: [i2+1,j1] in Indices G & f/.((len f) -'1) = G*(i2+1,j1) and A5: [i2,j1] in Indices G & f/.len f = G*(i2,j1); A6: 1 <= (len f)-'1 by A2,JORDAN3:12; A7: (len f) -'1 +1 = len f by A2,AMI_5:4; A8: 1 <= i2 & i2 <= len G & 1 <= j1 & j1 <= width G by A5,GOBOARD5:1; then A9: i2-'1 <= len G & j1-'1 <= width G by JORDAN3:7; A10: 1 <= j1+1 by NAT_1:29; A11: len G = width G by JORDAN8:def 1; now assume j1+1 > len G; then j1+1 <= (len G)+1 & (len G)+1 <= j1+1 by A8,A11,AXIOMS:24,NAT_1:38; then j1+1 = (len G)+1 by AXIOMS:21; then j1 = len G by XCMPLX_1:2; then cell(G,i2-'1,len G) meets C by A1,A3,A4,A5,A6,A7,GOBRD13:40; hence contradiction by A9,JORDAN8:18; end; hence [i2,j1+1] in Indices G by A8,A10,A11,GOBOARD7:10; end; theorem for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j2 being Nat st front_right_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i1,j2+1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j2+1) & [i1,j2] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1,j2) holds [i1-'1,j2] in Indices Gauge(C,n) proof let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2; let n; set G = Gauge(C,n); A1: len G = width G by JORDAN8:def 1; let f be FinSequence of TOP-REAL 2 such that A2: f is_sequence_on G and A3: len f > 1; let i1,j2 being Nat such that A4: front_right_cell(f,(len f)-'1,G) meets C and A5: [i1,j2+1] in Indices G & f/.((len f) -'1) = G*(i1,j2+1) and A6: [i1,j2] in Indices G & f/.len f = G*(i1,j2); A7: 1 <= (len f)-'1 by A3,JORDAN3:12; A8: (len f) -'1 +1 = len f by A3,AMI_5:4; A9: 1 <= i1 & i1 <= len G & 1 <= j2 & j2 <= width G by A6,GOBOARD5:1; then A10: i1-'1 <= len G & j2-'1 <= width G by JORDAN3:7; now assume i1-'1 < 1; then i1-'1 = 0 by RLVECT_1:98; then i1 <= 1 by JORDAN4:1; then i1 = 1 by A9,AXIOMS:21; then cell(G,1-'1,j2-'1) meets C by A2,A4,A5,A6,A7,A8,GOBRD13:42; then cell(G,0,j2-'1) meets C by GOBOARD9:1; hence contradiction by A1,A10,JORDAN8:21; end; hence [i1-'1,j2] in Indices G by A9,A10,GOBOARD7:10; end;

Back to top