Copyright (c) 2000 Association of Mizar Users
environ vocabulary COMPTS_1, SPPOL_1, EUCLID, RELAT_2, GOBOARD1, PRE_TOPC, TOPREAL2, RELAT_1, TOPREAL1, TOPS_2, SUBSET_1, BOOLE, MCART_1, CONNSP_3, CONNSP_1, SETFAM_1, TARSKI, FINSEQ_1, JORDAN3, ARYTM_1, FINSEQ_5, FUNCT_1, GROUP_2, PSCOMP_1, ORDINAL2, FUNCT_5, REALSET1, FINSEQ_4, SPRECT_2, FINSEQ_6, JORDAN1A, NAT_1, INT_1, JORDAN8, GROUP_1, ARYTM_3, GOBOARD5, TREES_1, JORDAN2C, JORDAN9, JORDAN6, COMPLEX1, SQUARE_1, ABSVALUE, ARYTM; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1, INT_1, NAT_1, ABSVALUE, SQUARE_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_4, FINSEQ_5, MATRIX_1, REALSET1, FINSEQ_6, STRUCT_0, PRE_TOPC, TOPS_2, JGRAPH_1, TOPREAL2, CARD_4, BINARITH, CONNSP_1, CONNSP_3, COMPTS_1, EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD5, SPPOL_1, JORDAN3, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A; constructors JORDAN8, REALSET1, JORDAN6, REAL_1, CARD_4, PSCOMP_1, BINARITH, JORDAN2C, CONNSP_1, JORDAN9, JORDAN1A, WSIERP_1, SQUARE_1, ABSVALUE, FINSEQ_4, JORDAN1, JORDAN3, RFINSEQ, TOPS_2, TOPREAL2, JORDAN5C, CONNSP_3, TOPREAL4, SPRECT_1, FINSEQ_5, GOBOARD1, TOPRNS_1, INT_1; clusters XREAL_0, TOPREAL6, JORDAN8, INT_1, RELSET_1, STRUCT_0, EUCLID, SPRECT_3, FINSEQ_1, FINSEQ_5, JORDAN1A, PRE_TOPC, JORDAN3, MEMBERED; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; definitions TARSKI, XBOOLE_0; theorems AXIOMS, BINARITH, EUCLID, GOBRD11, JORDAN8, NEWTON, PSCOMP_1, JORDAN1A, NAT_1, SCMFSA9A, GROUP_4, TOPREAL6, REAL_1, GOBOARD5, SQUARE_1, NAT_2, FINSEQ_1, FINSEQ_2, JORDAN4, JORDAN6, SPRECT_2, FINSEQ_4, FINSEQ_5, FINSEQ_6, GOBOARD7, GOBOARD9, SPPOL_1, SPPOL_2, TOPREAL4, REVROT_1, TOPREAL1, SPRECT_3, BOOLMARK, JORDAN5B, AMI_5, JORDAN3, RLVECT_1, JORDAN2C, SUBSET_1, CQC_THE1, JGRAPH_1, ABSVALUE, GOBOARD1, RELAT_1, PRE_TOPC, TOPREAL5, XREAL_0, TOPREAL2, TOPS_2, CONNSP_3, ORDERS_1, ZFMISC_1, TARSKI, CONNSP_1, SCMFSA_7, FINSEQ_3, XBOOLE_0, XBOOLE_1, INT_1, XCMPLX_0, XCMPLX_1; begin reserve E for compact non vertical non horizontal Subset of TOP-REAL 2, C for compact connected non vertical non horizontal Subset of TOP-REAL 2, G for Go-board, i, j, m, n for Nat, p for Point of TOP-REAL 2; definition cluster -> non vertical non horizontal Simple_closed_curve; coherence proof let S be Simple_closed_curve; consider f being map of (TOP-REAL 2)|R^2-unit_square, (TOP-REAL 2)|S such that A1: f is_homeomorphism by TOPREAL2:def 1; dom f = [#]((TOP-REAL 2)|R^2-unit_square) by A1,TOPS_2:def 5 .= R^2-unit_square by PRE_TOPC:def 10; then rng f <> {} by RELAT_1:65; then [#]((TOP-REAL 2)|S) <> {} by A1,TOPS_2:def 5; then A2: S is non empty by PRE_TOPC:def 10; then consider p1 be set such that A3: p1 in S by XBOOLE_0:def 1; reconsider p1 as Point of TOP-REAL 2 by A3; ex p2 be Point of TOP-REAL 2 st p2 in S & p2`1 <> p1`1 by A2,TOPREAL5:21; hence S is non vertical by A3,SPPOL_1:def 3; ex p2 be Point of TOP-REAL 2 st p2 in S & p2`2 <> p1`2 by A2,TOPREAL5:20; hence S is non horizontal by A3,SPPOL_1:def 2; end; end; definition let T be non empty TopSpace; cluster non empty a_union_of_components of T; existence proof [#]T = the carrier of T by PRE_TOPC:12; then reconsider A = [#]T as a_union_of_components of T by CONNSP_3:20; A is non empty; hence thesis; end; end; theorem for T being non empty TopSpace for A being non empty a_union_of_components of T st A is connected holds A is_a_component_of T proof let T be non empty TopSpace; let A be non empty a_union_of_components of T; consider F being Subset-Family of T such that A1: (for B being Subset of T st B in F holds B is_a_component_of T) & A = union F by CONNSP_3:def 2; consider X being set such that A2: X <> {} & X in F by A1,ORDERS_1:91; reconsider X as Subset of T by A2; assume A3: A is connected; F={X} proof thus F c= {X} proof let x be set; assume A4: x in F; then reconsider Y=x as Subset of T; A5: Y is_a_component_of T & X is_a_component_of T by A1,A2,A4; A6: X c= A by A1,A2,ZFMISC_1:92; Y c= A by A1,A4,ZFMISC_1:92; then Y = A by A3,A5,CONNSP_1:def 5 .= X by A3,A5,A6,CONNSP_1:def 5; hence x in {X} by TARSKI:def 1; end; let x be set; assume x in {X}; hence x in F by A2,TARSKI:def 1; end; then A = X by A1,ZFMISC_1:31; hence A is_a_component_of T by A1,A2; end; Lm1: for D being non empty set, f being FinSequence of D for i,j st 1 <= i & i <= j & j <= len f holds mid(f,i,j) is non empty proof let D be non empty set, f be FinSequence of D, i,j; assume 1 <= i & i <= j & j <= len f; then len mid(f,i,j) = j-'i+1 by JORDAN4:20; then len mid(f,i,j) <> 0 by NAT_1:29; hence mid(f,i,j) is non empty by FINSEQ_1:25; end; theorem Th2: for f being FinSequence holds f is empty iff Rev f is empty proof let f be FinSequence; hereby assume f is empty; then reconsider g=f as empty FinSequence; Rev g is empty; hence Rev f is empty; end; assume Rev f is empty; then reconsider g=Rev f as empty FinSequence; Rev g is empty; hence f is empty by FINSEQ_6:29; end; theorem for D being non empty set, f being FinSequence of D for i,j st 1 <= i & i <= len f & 1 <= j & j <= len f holds mid(f,i,j) is non empty proof let D be non empty set, f be FinSequence of D; let i,j such that A1: 1 <= i and A2: i <= len f and A3: 1 <= j and A4: j <= len f; per cases; suppose i <= j; hence mid(f,i,j) is non empty by A1,A4,Lm1; suppose j <= i; then A5: mid(f,j,i) is non empty by A2,A3,Lm1; mid(f,i,j) = Rev mid(f,j,i) by JORDAN4:30; hence mid(f,i,j) is non empty by A5,Th2; end; theorem Th4: for f be non empty FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st 1 <= len f & p in L~f holds R_Cut(f,p).1 = f.1 proof let f be non empty FinSequence of TOP-REAL 2; let p be Point of TOP-REAL 2; assume that A1: 1 <= len f and A2: p in L~f; A3: 1 in dom f by FINSEQ_5:6; A4: 1 <= Index(p,f) by A2,JORDAN3:41; now per cases; suppose A5: p<>f.1; A6: Index(p,f) < len f by A2,JORDAN3:41; then Index(p,f) in dom f by A4,FINSEQ_3:27; then A7: len mid(f,1,Index(p,f)) >= 1 by A3,SPRECT_2:9; R_Cut(f,p) = mid(f,1,Index(p,f))^<*p*> by A5,JORDAN3:def 5; hence R_Cut(f,p).1 = mid(f,1,Index(p,f)).1 by A7,JORDAN3:17 .= f.1 by A1,A4,A6,JORDAN3:27; suppose A8: p = f.1; then R_Cut(f,p) = <*p*> by JORDAN3:def 5; hence R_Cut(f,p).1 = f.1 by A8,FINSEQ_1:57; end; hence R_Cut(f,p).1 = f.1; end; theorem for f be non empty FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st f is_S-Seq & p in L~f holds L_Cut(f,p).(len L_Cut(f,p)) = f.(len f) proof let f be non empty FinSequence of TOP-REAL 2; let p be Point of TOP-REAL 2 such that A1: f is_S-Seq and A2: p in L~f; A3: Rev f is_S-Seq by A1,SPPOL_2:47; A4: p in L~Rev f by A2,SPPOL_2:22; then A5: L_Cut(Rev Rev f,p) = Rev R_Cut(Rev f,p) by A3,JORDAN3:57; 2 <= len Rev f by A3,TOPREAL1:def 10; then A6: 1 <= len Rev f by AXIOMS:22; Rev Rev f = f by FINSEQ_6:29; hence L_Cut(f,p).(len L_Cut(f,p)) = Rev R_Cut(Rev f,p).(len R_Cut(Rev f,p)) by A5,FINSEQ_5:def 3 .= R_Cut(Rev f,p).1 by FINSEQ_5:65 .= Rev f.1 by A4,A6,Th4 .= f.(len f) by FINSEQ_5:65; end; theorem for P be Simple_closed_curve holds W-max(P) <> E-max(P) proof let P be Simple_closed_curve; now assume A1: W-max(P) = E-max(P); A2:|[W-bound P, sup (proj2||W-most P)]|=W-max(P) by PSCOMP_1:def 43; |[E-bound P, sup (proj2||E-most P)]|=E-max(P) by PSCOMP_1:def 46; then W-bound P= E-bound P by A1,A2,SPPOL_2:1; hence contradiction by TOPREAL5:23; end; hence W-max(P) <> E-max(P); end; theorem for D be non empty set for f be FinSequence of D st 1 <= i & i < len f holds mid(f,i,len f-'1)^<*f/.(len f)*> = mid(f,i,len f) proof let D be non empty set; let f be FinSequence of D; assume A1: 1 <= i & i < len f; then A2: i+1 <= len f by NAT_1:38; then i+1-1 <= len f-1 by REAL_1:49; then A3: 0+i <= len f-1 by XCMPLX_1:26; then len f-1 >= 1 by A1,AXIOMS:22; then A4: len f-1 >= 0 by AXIOMS:22; then A5: i <= len f-'1 by A3,BINARITH:def 3; len f <= len f+1 by NAT_1:29; then len f-1 <= len f+1-1 by REAL_1:49; then len f-1 <= len f by XCMPLX_1:26; then A6: len f-'1 <= len f by A4,BINARITH:def 3; len f-i >= 1 by A2,REAL_1:84; then A7: len f-i >= 0 by AXIOMS:22; len f-1-i >= 0 by A3,REAL_1:84; then A8: len f-'1-i >= 0 by A4,BINARITH:def 3; A9: len (mid(f,i,len f-'1)^<*f/.(len f)*>) = len mid(f,i,len f-'1) + 1 by FINSEQ_2:19; A10: len mid(f,i,len f-'1) + 1 = len f-'1-'i+1+1 by A1,A5,A6,JORDAN4:20 .= len f-'1-i+1+1 by A8,BINARITH:def 3 .= len f-1-i+1+1 by A4,BINARITH:def 3 .= len f-i-1+1+1 by XCMPLX_1:21 .= len f-i+-1+1+1 by XCMPLX_0:def 8 .= len f-i+1 by XCMPLX_1:139 .= len f-'i+1 by A7,BINARITH:def 3 .= len mid(f,i,len f) by A1,JORDAN4:20; now let j; assume A11: 1 <= j & j <= len mid(f,i,len f); 1 < len f by A1,AXIOMS:22; then i in Seg len f & len f in Seg len f by A1,FINSEQ_1:3; then A12: i in dom f & len f in dom f by FINSEQ_1:def 3; per cases by A11,REAL_1:def 5; suppose j < len mid(f,i,len f); then A13: j <= len mid(f,i,len f-'1) by A10,NAT_1:38; then j in Seg len mid(f,i,len f-'1) by A11,FINSEQ_1:3; then A14: j in dom mid(f,i,len f-'1) by FINSEQ_1:def 3; j in Seg len mid(f,i,len f) by A11,FINSEQ_1:3; then A15: j in dom mid(f,i,len f) by FINSEQ_1:def 3; 1 <= len f-'1 by A1,A5,AXIOMS:22; then len f-'1 in Seg len f by A6,FINSEQ_1:3; then A16: len f-'1 in dom f by FINSEQ_1:def 3; thus (mid(f,i,len f-'1)^<*f/.(len f)*>)/.j = mid(f,i,len f-'1)/.j by A11,A13,BOOLMARK:8 .= f/.(j+i-'1) by A5,A12,A14,A16,SPRECT_2:7 .= mid(f,i,len f)/.j by A1,A12,A15,SPRECT_2:7; suppose A17: j = len mid(f,i,len f); hence (mid(f,i,len f-'1)^<*f/.(len f)*>)/.j = f/.(len f) by A10,TOPREAL4:1 .= mid(f,i,len f)/.j by A12,A17,SPRECT_2:13; end; hence mid(f,i,len f-'1)^<*f/.(len f)*> = mid(f,i,len f) by A9,A10,FINSEQ_5:14; end; theorem for p,q be Point of TOP-REAL 2 st p <> q & LSeg(p,q) is vertical holds <*p,q*> is_S-Seq proof let p,q be Point of TOP-REAL 2; assume that A1: p <> q and A2: LSeg(p,q) is vertical; p`1 = q`1 by A2,SPPOL_1:37; hence <*p,q*> is_S-Seq by A1,SPPOL_2:46; end; theorem for p,q be Point of TOP-REAL 2 st p <> q & LSeg(p,q) is horizontal holds <*p,q*> is_S-Seq proof let p,q be Point of TOP-REAL 2; assume that A1: p <> q and A2: LSeg(p,q) is horizontal; p`2 = q`2 by A2,SPPOL_1:36; hence <*p,q*> is_S-Seq by A1,SPPOL_2:46; end; theorem Th10: for p,q be FinSequence of TOP-REAL 2 for v be Point of TOP-REAL 2 st p is_in_the_area_of q holds Rotate(p,v) is_in_the_area_of q proof let p,q be FinSequence of TOP-REAL 2; let v be Point of TOP-REAL 2; assume A1: p is_in_the_area_of q; per cases; suppose A2: v in rng p; now let n; assume n in dom Rotate(p,v); then n in dom p by REVROT_1:15; then n in Seg len p by FINSEQ_1:def 3; then A3: 0+1 <= n & n <= len p by FINSEQ_1:3; then A4: n-1 >= 0 by REAL_1:84; per cases; suppose A5: n <= len(p:-v); then A6: Rotate(p,v)/.n = p/.(n-'1+v..p) by A2,A3,REVROT_1:9; n <= len p-v..p+1 by A2,A5,FINSEQ_5:53; then n-1 <= len p-v..p by REAL_1:86; then n-1+v..p <= len p by REAL_1:84; then A7: n-'1+v..p <= len p by A4,BINARITH:def 3; A8: n-'1 >= 0 by NAT_1:18; 1 <= v..p by A2,FINSEQ_4:31; then 0+1 <= n-'1+v..p by A8,REAL_1:55; then n-'1+v..p in Seg len p by A7,FINSEQ_1:3; then A9: n-'1+v..p in dom p by FINSEQ_1:def 3; hence W-bound L~q <= (Rotate(p,v)/.n)`1 by A1,A6,SPRECT_2:def 1; thus (Rotate(p,v)/.n)`1 <= E-bound L~q by A1,A6,A9,SPRECT_2:def 1; thus S-bound L~q <= (Rotate(p,v)/.n)`2 by A1,A6,A9,SPRECT_2:def 1; thus (Rotate(p,v)/.n)`2 <= N-bound L~q by A1,A6,A9,SPRECT_2:def 1; suppose A10: n > len(p:-v); then A11: Rotate(p,v)/.n = p/.(n+v..p-'len p) by A2,A3,REVROT_1:12; n > len p-v..p+1 by A2,A10,FINSEQ_5:53; then n > 1+len p-v..p by XCMPLX_1:29; then n+v..p > 1+len p by REAL_1:84; then A12: n+v..p-len p > 1 by REAL_1:86; then A13: n+v..p-len p >= 0 by AXIOMS:22; v..p <= len p by A2,FINSEQ_4:31; then n+v..p <= len p+len p by A3,REAL_1:55; then n+v..p-len p <= len p by REAL_1:86; then A14: n+v..p-'len p <= len p by A13,BINARITH:def 3; 1 <= n+v..p-'len p by A12,A13,BINARITH:def 3; then n+v..p-'len p in Seg len p by A14,FINSEQ_1:3; then A15: n+v..p-'len p in dom p by FINSEQ_1:def 3; hence W-bound L~q <= (Rotate(p,v)/.n)`1 by A1,A11,SPRECT_2:def 1; thus (Rotate(p,v)/.n)`1 <= E-bound L~q by A1,A11,A15,SPRECT_2:def 1; thus S-bound L~q <= (Rotate(p,v)/.n)`2 by A1,A11,A15,SPRECT_2:def 1; thus (Rotate(p,v)/.n)`2 <= N-bound L~q by A1,A11,A15,SPRECT_2:def 1; end; hence Rotate(p,v) is_in_the_area_of q by SPRECT_2:def 1; suppose not v in rng p; hence Rotate(p,v) is_in_the_area_of q by A1,FINSEQ_6:def 2; end; theorem for p be non trivial FinSequence of TOP-REAL 2 for v be Point of TOP-REAL 2 holds Rotate(p,v) is_in_the_area_of p proof let p be non trivial FinSequence of TOP-REAL 2; let v be Point of TOP-REAL 2; p is_in_the_area_of p by SPRECT_2:25; hence Rotate(p,v) is_in_the_area_of p by Th10; end; theorem Th12: for f be FinSequence holds Center f >= 1 proof let f be FinSequence; len f div 2 >= 0 by NAT_1:19; then len f div 2 + 1 >= 0+1 by AXIOMS:24; hence thesis by JORDAN1A:def 1; end; theorem for f be FinSequence st len f >= 1 holds Center f <= len f proof let f be FinSequence; assume len f >= 1; then len f >= 0+1; then len f > 0 by NAT_1:38; then 0 + len f < len f + len f by REAL_1:53; then len f < 2*len f by XCMPLX_1:11; then len f+1 <= 2*len f by NAT_1:38; then (len f+1+1) div 2 <= len f by NAT_2:27; then (len f+(1+1)) div 2 <= len f by XCMPLX_1:1; then len f div 2+1 <= len f by NAT_2:16; hence thesis by JORDAN1A:def 1; end; theorem Th14: Center G <= len G proof A1: Center G = len G div 2 + 1 by JORDAN1A:def 1; 1 <= len G by GOBRD11:34; then 0 < len G by AXIOMS:22; then len G div (2 qua Integer) < len G by SCMFSA9A:4; then len G div 2 < len G by SCMFSA9A:5; hence thesis by A1,NAT_1:38; end; theorem Th15: for f be FinSequence st len f >= 2 holds Center f > 1 proof let f be FinSequence; assume len f >= 2; then len f div 2 >= 1 by NAT_2:15; then len f div 2 + 1 > 1 by NAT_1:38; hence thesis by JORDAN1A:def 1; end; theorem Th16: for f be FinSequence st len f >= 3 holds Center f < len f proof let f be FinSequence; assume len f >= 3; then len f+(2+1) <= len f+len f by AXIOMS:24; then len f+2+1 <= len f+len f by XCMPLX_1:1; then len f+2+1 <= 2*len f by XCMPLX_1:11; then (len f+2+1+1) div 2 <= len f by NAT_2:27; then (len f+2+(1+1)) div 2 <= len f by XCMPLX_1:1; then (len f+2) div 2+1 <= len f by NAT_2:16; then (len f+2) div 2 < len f by NAT_1:38; then len f div 2 + 1 < len f by NAT_2:16; hence thesis by JORDAN1A:def 1; end; Lm2: now let E be non empty Subset of TOP-REAL 2; thus len Gauge(E,0)-'1 = 2|^0 + 3 -' 1 by JORDAN8:def 1 .= 1+3-'1 by NEWTON:9 .= 3 by BINARITH:39; end; theorem Center Gauge(E,n) = 2|^(n-'1) + 2 proof set G = Gauge(E,n); per cases by NAT_1:19; suppose A1: n = 0; A2: 0-1 < 0; A3: 4 = 2 * 2 + 0; Center G = len G div 2 + 1 by JORDAN1A:def 1; hence Center G = (2|^0 + 3) div 2 + 1 by A1,JORDAN8:def 1 .= (1+3) div 2 + 1 by NEWTON:9 .= 1 + 1 + 1 by A3,NAT_1:def 1 .= 2|^0 + 1 + 1 by NEWTON:9 .= 2|^(0-'1) + 1 + 1 by A2,BINARITH:def 3 .= 2|^(0-'1) + (1 + 1) by XCMPLX_1:1 .= 2|^(n-'1) + 2 by A1; suppose A4: n > 0; then A5: 2|^n mod 2 = 0 by JORDAN1A:3; 3 = 2 * 1 + 1; then A6: 3 div 2 = 1 by NAT_1:def 1; A7: len G div 2 + 1 = (2|^n + 3) div 2 + 1 by JORDAN8:def 1 .= (2|^n div 2) + (3 div 2) + 1 by A5,GROUP_4:106 .= (2|^n div 2) + (1 + 1) by A6,XCMPLX_1:1; A8: 0+1 <= n by A4,NAT_1:38; 2|^n div 2 = 2|^n / 2 by A4,JORDAN1A:5 .= 2|^n / 2|^1 by NEWTON:10 .= 2|^(n-'1) by A8,TOPREAL6:15; hence thesis by A7,JORDAN1A:def 1; end; theorem Th18: E c= cell(Gauge(E,0),2,2) proof set G = Gauge(E,0); let x be set; assume A1: x in E; then reconsider x as Point of TOP-REAL 2; A2: x = |[x`1,x`2]| by EUCLID:57; A3: len G = width G by JORDAN8:def 1; A4: len G-'1 = 3 by Lm2; A5: 4 <= len G by JORDAN8:13; then 1 < len G by AXIOMS:22; then G*(2+1,1)`1 = E-bound E & G*(1,2)`2 = S-bound E & G*(1,2+1)`2 = N-bound E & G*(2,1)`1 = W-bound E by A4,JORDAN8:14,15,16,17; then A6: G*(2,1)`1 <= x`1 & x`1 <= G*(2+1,1)`1 & G*(1,2)`2 <= x`2 & x`2 <= G*(1,2+1)`2 by A1,PSCOMP_1:71; 2 < len G by A5,AXIOMS:22; then cell(G,2,2) = { |[p,q]| where p, q is Real: G*(2,1)`1 <= p & p <= G*(2+1,1)`1 & G*(1,2)`2 <= q & q <= G*(1,2+1)`2 } by A3,GOBRD11:32; hence thesis by A2,A6; end; theorem Th19: not cell(Gauge(E,0),2,2) c= BDD E proof assume A1: cell(Gauge(E,0),2,2) c= BDD E; E c= cell(Gauge(E,0),2,2) by Th18; then A2: E c= BDD E by A1,XBOOLE_1:1; consider e being Element of E; A3: e in E; BDD E misses E by JORDAN1A:15; hence thesis by A2,A3,XBOOLE_0:3; end; theorem Gauge(C,1)*(Center Gauge(C,1),1) = |[(W-bound C + E-bound C)/2,S-bound L~Cage(C,1)]| proof set G = Gauge(C,1); 1 <= len G by GOBRD11:34; then A1: G*(Center G,1)`1 = (W-bound C + E-bound C) / 2 by JORDAN1A:59; 1 <= Center G & Center G <= len G by Th12,Th14; then G*(Center G,1)`2 = S-bound L~Cage(C,1) by JORDAN1A:93; hence thesis by A1,EUCLID:57; end; theorem Gauge(C,1)*(Center Gauge(C,1),len Gauge(C,1)) = |[(W-bound C + E-bound C)/2,N-bound L~Cage(C,1)]| proof set G = Gauge(C,1); 1 <= len G by GOBRD11:34; then A1: G*(Center G,len G)`1 = (W-bound C + E-bound C) / 2 by JORDAN1A:59; 1 <= Center G & Center G <= len G by Th12,Th14; then G*(Center G,len G)`2 = N-bound L~Cage(C,1) by JORDAN1A:91; hence thesis by A1,EUCLID:57; end; Lm3: i <= m & m <= i+1 implies i = m or i = m -' 1 proof assume that A1: i <= m and A2: m <= i+1 and A3: i <> m; i < m by A1,A3,REAL_1:def 5; then i+1 <= m by NAT_1:38; then m = i+1 by A2,AXIOMS:21; hence i = m -' 1 by BINARITH:39; end; theorem Th22: 1 <= j & j < width G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell(G,len G,j) & p`1 = G*(m,n)`1 implies len G = m proof assume that A1: 1 <= j & j < width G and A2: 1 <= m & m <= len G and A3: 1 <= n & n <= width G and A4: p in cell(G,len G,j) and A5: p`1 = G*(m,n)`1; A6: 1 <= width G by A1,AXIOMS:22; A7: G*(m,1)`1 = G*(m,n)`1 by A2,A3,GOBOARD5:3; cell(G,len G,j) = { |[r,s]| where r, s is Real: G*(len G,1)`1 <= r & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } by A1,GOBRD11:29; then consider r, s being Real such that A8: p = |[r,s]| and A9: G*(len G,1)`1 <= r and G*(1,j)`2 <= s & s <= G*(1,j+1)`2 by A4; p`1 = r by A8,EUCLID:56; then len G <= m by A2,A5,A6,A7,A9,GOBOARD5:4; hence thesis by A2,AXIOMS:21; end; theorem 1 <= i & i <= len G & 1 <= j & j < width G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell(G,i,j) & p`1 = G*(m,n)`1 implies i = m or i = m -' 1 proof assume that A1: 1 <= i & i <= len G and A2: 1 <= j & j < width G and A3: 1 <= m & m <= len G and A4: 1 <= n & n <= width G and A5: p in cell(G,i,j) and A6: p`1 = G*(m,n)`1; A7: 1 <= width G by A2,AXIOMS:22; A8: G*(m,1)`1 = G*(m,n)`1 by A3,A4,GOBOARD5:3; per cases by A1,REAL_1:def 5; suppose i = len G; hence thesis by A2,A3,A4,A5,A6,Th22; suppose i < len G; then cell(G,i,j) = { |[r,s]| where r, s is Real: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } by A1,A2,GOBRD11:32; then consider r, s being Real such that A9: p = |[r,s]| and A10: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 and G*(1,j)`2 <= s & s <= G*(1,j+1)`2 by A5; A11: p`1 = r by A9,EUCLID:56; i <= m & m <= i+1 proof assume A12: not thesis; per cases by A12; suppose i > m; hence contradiction by A1,A3,A6,A7,A8,A10,A11,GOBOARD5:4; suppose A13: m > i+1; 1 <= i+1 by NAT_1:29; hence contradiction by A3,A6,A7,A8,A10,A11,A13,GOBOARD5:4; end; hence thesis by Lm3; end; theorem Th24: 1 <= i & i < len G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell(G,i,width G) & p`2 = G*(m,n)`2 implies width G = n proof assume that A1: 1 <= i & i < len G and A2: 1 <= m & m <= len G and A3: 1 <= n & n <= width G and A4: p in cell(G,i,width G) and A5: p`2 = G*(m,n)`2; A6: 1 <= len G by A1,AXIOMS:22; A7: G*(1,n)`2 = G*(m,n)`2 by A2,A3,GOBOARD5:2; cell(G,i,width G) = { |[r,s]| where r, s is Real: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,width G)`2 <= s } by A1,GOBRD11:31; then consider r, s being Real such that A8: p = |[r,s]| and G*(i,1)`1 <= r and A9: r <= G*(i+1,1)`1 & G*(1,width G)`2 <= s by A4; p`2 = s by A8,EUCLID:56; then width G <= n by A3,A5,A6,A7,A9,GOBOARD5:5; hence thesis by A3,AXIOMS:21; end; theorem 1 <= i & i < len G & 1 <= j & j <= width G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell(G,i,j) & p`2 = G*(m,n)`2 implies j = n or j = n -' 1 proof assume that A1: 1 <= i & i < len G and A2: 1 <= j & j <= width G and A3: 1 <= m & m <= len G and A4: 1 <= n & n <= width G and A5: p in cell(G,i,j) and A6: p`2 = G*(m,n)`2; A7: 1 <= len G by A1,AXIOMS:22; A8: G*(1,n)`2 = G*(m,n)`2 by A3,A4,GOBOARD5:2; per cases by A2,REAL_1:def 5; suppose j = width G; hence thesis by A1,A3,A4,A5,A6,Th24; suppose j < width G; then cell(G,i,j) = { |[r,s]| where r, s is Real: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } by A1,A2,GOBRD11:32; then consider r, s being Real such that A9: p = |[r,s]| and G*(i,1)`1 <= r & r <= G*(i+1,1)`1 and A10: G*(1,j)`2 <= s & s <= G*(1,j+1)`2 by A5; A11: p`2 = s by A9,EUCLID:56; j <= n & n <= j+1 proof assume A12: not thesis; per cases by A12; suppose j > n; hence contradiction by A2,A4,A6,A7,A8,A10,A11,GOBOARD5:5; suppose A13: n > j+1; 1 <= j+1 by NAT_1:29; hence contradiction by A4,A6,A7,A8,A10,A11,A13,GOBOARD5:5; end; hence thesis by Lm3; end; theorem Th26: for C be Simple_closed_curve for r be real number st W-bound C <= r & r <= E-bound C holds LSeg(|[r,S-bound C]|,|[r,N-bound C]|) meets Upper_Arc C proof let C be Simple_closed_curve; let r be real number; A1: (W-min C)`1 = W-bound C by PSCOMP_1:84; A2: (E-max C)`1 = E-bound C by PSCOMP_1:104; A3: r is Real by XREAL_0:def 1; assume A4: W-bound C <= r & r <= E-bound C; Upper_Arc C is_an_arc_of W-min(C),E-max(C) by JORDAN6:def 8; then Upper_Arc C meets Vertical_Line(r) by A1,A2,A3,A4,JORDAN6:64; then consider x be set such that A5: x in Upper_Arc C /\ Vertical_Line(r) by XBOOLE_0:4; A6: x in Upper_Arc C & x in Vertical_Line(r) by A5,XBOOLE_0:def 3; reconsider fs = x as Point of TOP-REAL 2 by A5; Upper_Arc C c= C by JORDAN1A:16; then A7: S-bound C <= fs`2 & fs`2 <= N-bound C by A6,PSCOMP_1:71; A8: |[r,S-bound C]|`1 = r by EUCLID:56 .= fs`1 by A6,JORDAN6:34; A9: |[r,N-bound C]|`1 = r by EUCLID:56 .= fs`1 by A6,JORDAN6:34; |[r,S-bound C]|`2 = S-bound C & |[r,N-bound C]|`2 = N-bound C by EUCLID: 56 ; then x in LSeg(|[r,S-bound C]|,|[r,N-bound C]|) by A7,A8,A9,GOBOARD7:8; hence LSeg(|[r,S-bound C]|,|[r,N-bound C]|) meets Upper_Arc C by A6,XBOOLE_0:3; end; theorem Th27: for C be Simple_closed_curve for r be real number st W-bound C <= r & r <= E-bound C holds LSeg(|[r,S-bound C]|,|[r,N-bound C]|) meets Lower_Arc C proof let C be Simple_closed_curve; let r be real number; A1: (W-min C)`1 = W-bound C by PSCOMP_1:84; A2: (E-max C)`1 = E-bound C by PSCOMP_1:104; A3: r is Real by XREAL_0:def 1; assume A4: W-bound C <= r & r <= E-bound C; Lower_Arc C is_an_arc_of E-max(C),W-min(C) by JORDAN6:def 9; then Lower_Arc C is_an_arc_of W-min(C),E-max(C) by JORDAN5B:14; then Lower_Arc C meets Vertical_Line(r) by A1,A2,A3,A4,JORDAN6:64; then consider x be set such that A5: x in Lower_Arc C /\ Vertical_Line(r) by XBOOLE_0:4; A6: x in Lower_Arc C & x in Vertical_Line(r) by A5,XBOOLE_0:def 3; reconsider fs = x as Point of TOP-REAL 2 by A5; Lower_Arc C c= C by JORDAN1A:16; then A7: S-bound C <= fs`2 & fs`2 <= N-bound C by A6,PSCOMP_1:71; A8: |[r,S-bound C]|`1 = r by EUCLID:56 .= fs`1 by A6,JORDAN6:34; A9: |[r,N-bound C]|`1 = r by EUCLID:56 .= fs`1 by A6,JORDAN6:34; |[r,S-bound C]|`2 = S-bound C & |[r,N-bound C]|`2 = N-bound C by EUCLID: 56 ; then x in LSeg(|[r,S-bound C]|,|[r,N-bound C]|) by A7,A8,A9,GOBOARD7:8; hence LSeg(|[r,S-bound C]|,|[r,N-bound C]|) meets Lower_Arc C by A6,XBOOLE_0:3; end; theorem Th28: for C be Simple_closed_curve for i be Nat st 1 < i & i < len Gauge(C,n) holds LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) meets Upper_Arc C proof let C be Simple_closed_curve; let i be Nat; assume A1: 1 < i & i < len Gauge(C,n); A2: Gauge(C,n)*(i,2) = |[(Gauge(C,n)*(i,2))`1,(Gauge(C,n)*(i,2))`2]| by EUCLID:57 .= |[(Gauge(C,n)*(i,2))`1,S-bound C]| by A1,JORDAN8:16; A3: Gauge(C,n)*(i,len Gauge(C,n)-'1) = |[(Gauge(C,n)*(i,len Gauge(C,n)-'1))`1, (Gauge(C,n)*(i,len Gauge(C,n)-'1))`2]| by EUCLID:57 .= |[(Gauge(C,n)*(i,len Gauge(C,n)-'1))`1,N-bound C]| by A1,JORDAN8:17; set r = (Gauge(C,n)*(i,2))`1; A4: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; A5: 4 <= len Gauge(C,n) by JORDAN8:13; then len Gauge(C,n) >= 0+1 by AXIOMS:22; then A6: len Gauge(C,n)-1 >= 0 by REAL_1:84; A7: 1+1 <= len Gauge(C,n) by A5,AXIOMS:22; then 1 <= len Gauge(C,n)-1 by REAL_1:84; then A8: 1 <= len Gauge(C,n)-'1 by A6,BINARITH:def 3; A9: len Gauge(C,n)-'1 <= len Gauge(C,n) by GOBOARD9:2; A10: r = (Gauge(C,n)*(i,1))`1 by A1,A4,A7,GOBOARD5:3 .= (Gauge(C,n)*(i,len Gauge(C,n)-'1))`1 by A1,A4,A8,A9,GOBOARD5:3; 1+1 <= i by A1,NAT_1:38; then (Gauge(C,n)*(2,2))`1 <= r by A1,A4,A7,SPRECT_3:25; then A11: W-bound C <= r by A7,JORDAN8:14; i+1 <= len Gauge(C,n) by A1,NAT_1:38; then i <= len Gauge(C,n)-1 by REAL_1:84; then i <= len Gauge(C,n)-'1 by A6,BINARITH:def 3; then r <= Gauge(C,n)*(len Gauge(C,n)-'1,len Gauge(C,n)-'1)`1 by A1,A4,A8,A9,A10,SPRECT_3:25; then r <= E-bound C by A8,A9,JORDAN8:15; then A12: LSeg(Gauge(C,n)*(i,2),Gauge(C,n)*(i,len Gauge(C,n)-'1)) meets Upper_Arc C by A2,A3,A10,A11,Th26; A13: Gauge(C,n)*(i,2) in LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) by A1,A4,A7,JORDAN1A:37; Gauge(C,n)*(i,len Gauge(C,n)-'1) in LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) by A1,A4,A8,A9,JORDAN1A:37; then LSeg(Gauge(C,n)*(i,2),Gauge(C,n)*(i,len Gauge(C,n)-'1)) c= LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) by A13,TOPREAL1:12; hence LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) meets Upper_Arc C by A12,XBOOLE_1:63; end; theorem Th29: for C be Simple_closed_curve for i be Nat st 1 < i & i < len Gauge(C,n) holds LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) meets Lower_Arc C proof let C be Simple_closed_curve; let i be Nat; assume A1: 1 < i & i < len Gauge(C,n); A2: Gauge(C,n)*(i,2) = |[(Gauge(C,n)*(i,2))`1,(Gauge(C,n)*(i,2))`2]| by EUCLID:57 .= |[(Gauge(C,n)*(i,2))`1,S-bound C]| by A1,JORDAN8:16; A3: Gauge(C,n)*(i,len Gauge(C,n)-'1) = |[(Gauge(C,n)*(i,len Gauge(C,n)-'1))`1, (Gauge(C,n)*(i,len Gauge(C,n)-'1))`2]| by EUCLID:57 .= |[(Gauge(C,n)*(i,len Gauge(C,n)-'1))`1,N-bound C]| by A1,JORDAN8:17; set r = (Gauge(C,n)*(i,2))`1; A4: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; A5: 4 <= len Gauge(C,n) by JORDAN8:13; then len Gauge(C,n) >= 0+1 by AXIOMS:22; then A6: len Gauge(C,n)-1 >= 0 by REAL_1:84; A7: 1+1 <= len Gauge(C,n) by A5,AXIOMS:22; then 1 <= len Gauge(C,n)-1 by REAL_1:84; then A8: 1 <= len Gauge(C,n)-'1 by A6,BINARITH:def 3; A9: len Gauge(C,n)-'1 <= len Gauge(C,n) by GOBOARD9:2; A10: r = (Gauge(C,n)*(i,1))`1 by A1,A4,A7,GOBOARD5:3 .= (Gauge(C,n)*(i,len Gauge(C,n)-'1))`1 by A1,A4,A8,A9,GOBOARD5:3; 1+1 <= i by A1,NAT_1:38; then (Gauge(C,n)*(2,2))`1 <= r by A1,A4,A7,SPRECT_3:25; then A11: W-bound C <= r by A7,JORDAN8:14; i+1 <= len Gauge(C,n) by A1,NAT_1:38; then i <= len Gauge(C,n)-1 by REAL_1:84; then i <= len Gauge(C,n)-'1 by A6,BINARITH:def 3; then r <= Gauge(C,n)*(len Gauge(C,n)-'1,len Gauge(C,n)-'1)`1 by A1,A4,A8,A9,A10,SPRECT_3:25; then r <= E-bound C by A8,A9,JORDAN8:15; then A12: LSeg(Gauge(C,n)*(i,2),Gauge(C,n)*(i,len Gauge(C,n)-'1)) meets Lower_Arc C by A2,A3,A10,A11,Th27; A13: Gauge(C,n)*(i,2) in LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) by A1,A4,A7,JORDAN1A:37; Gauge(C,n)*(i,len Gauge(C,n)-'1) in LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) by A1,A4,A8,A9,JORDAN1A:37; then LSeg(Gauge(C,n)*(i,2),Gauge(C,n)*(i,len Gauge(C,n)-'1)) c= LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) by A13,TOPREAL1:12; hence LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) meets Lower_Arc C by A12,XBOOLE_1:63; end; theorem for C be Simple_closed_curve holds LSeg(Gauge(C,n)*(Center Gauge(C,n),1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))) meets Upper_Arc C proof let C be Simple_closed_curve; A1: 4 <= len Gauge(C,n) by JORDAN8:13; then len Gauge(C,n) >= 2 by AXIOMS:22; then A2: 1 < Center Gauge(C,n) by Th15; len Gauge(C,n) >= 3 by A1,AXIOMS:22; then Center Gauge(C,n) < len Gauge(C,n) by Th16; hence LSeg(Gauge(C,n)*(Center Gauge(C,n),1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))) meets Upper_Arc C by A2,Th28; end; theorem for C be Simple_closed_curve holds LSeg(Gauge(C,n)*(Center Gauge(C,n),1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))) meets Lower_Arc C proof let C be Simple_closed_curve; A1: 4 <= len Gauge(C,n) by JORDAN8:13; then len Gauge(C,n) >= 2 by AXIOMS:22; then A2: 1 < Center Gauge(C,n) by Th15; len Gauge(C,n) >= 3 by A1,AXIOMS:22; then Center Gauge(C,n) < len Gauge(C,n) by Th16; hence LSeg(Gauge(C,n)*(Center Gauge(C,n),1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))) meets Lower_Arc C by A2,Th29; end; theorem Th32: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i be Nat st 1 <= i & i <= len Gauge(C,n) holds LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) meets Upper_Arc L~Cage(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let i be Nat; assume A1: 1 <= i & i <= len Gauge(C,n); A2: Gauge(C,n)*(i,1) = |[(Gauge(C,n)*(i,1))`1,(Gauge(C,n)*(i,1))`2]| by EUCLID:57 .= |[(Gauge(C,n)*(i,1))`1,S-bound L~Cage(C,n)]| by A1,JORDAN1A:93; A3: Gauge(C,n)*(i,len Gauge(C,n)) = |[(Gauge(C,n)*(i,len Gauge(C,n)))`1, (Gauge(C,n)*(i,len Gauge(C,n)))`2]| by EUCLID:57 .= |[(Gauge(C,n)*(i,len Gauge(C,n)))`1, N-bound L~Cage(C,n)]| by A1,JORDAN1A:91; set r = (Gauge(C,n)*(i,1))`1; A4: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; 4 <= len Gauge(C,n) by JORDAN8:13; then A5: 1 <= len Gauge(C,n) by AXIOMS:22; then A6: r = (Gauge(C,n)*(i,len Gauge(C,n)))`1 by A1,A4,GOBOARD5:3; (Gauge(C,n)*(1,1))`1 <= r by A1,A4,A5,SPRECT_3:25; then A7: W-bound L~Cage(C,n) <= r by A5,JORDAN1A:94; r <= Gauge(C,n)*(len Gauge(C,n),1)`1 by A1,A4,A5,SPRECT_3:25; then r <= E-bound L~Cage(C,n) by A5,JORDAN1A:92; hence LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) meets Upper_Arc L~Cage(C,n) by A2,A3,A6,A7,Th26; end; theorem Th33: for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i be Nat st 1 <= i & i <= len Gauge(C,n) holds LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) meets Lower_Arc L~Cage(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let i be Nat; assume A1: 1 <= i & i <= len Gauge(C,n); A2: Gauge(C,n)*(i,1) = |[(Gauge(C,n)*(i,1))`1,(Gauge(C,n)*(i,1))`2]| by EUCLID:57 .= |[(Gauge(C,n)*(i,1))`1,S-bound L~Cage(C,n)]| by A1,JORDAN1A:93; A3: Gauge(C,n)*(i,len Gauge(C,n)) = |[(Gauge(C,n)*(i,len Gauge(C,n)))`1, (Gauge(C,n)*(i,len Gauge(C,n)))`2]| by EUCLID:57 .= |[(Gauge(C,n)*(i,len Gauge(C,n)))`1, N-bound L~Cage(C,n)]| by A1,JORDAN1A:91; set r = (Gauge(C,n)*(i,1))`1; A4: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; 4 <= len Gauge(C,n) by JORDAN8:13; then A5: 1 <= len Gauge(C,n) by AXIOMS:22; then A6: r = (Gauge(C,n)*(i,len Gauge(C,n)))`1 by A1,A4,GOBOARD5:3; (Gauge(C,n)*(1,1))`1 <= r by A1,A4,A5,SPRECT_3:25; then A7: W-bound L~Cage(C,n) <= r by A5,JORDAN1A:94; r <= Gauge(C,n)*(len Gauge(C,n),1)`1 by A1,A4,A5,SPRECT_3:25; then r <= E-bound L~Cage(C,n) by A5,JORDAN1A:92; hence LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) meets Lower_Arc L~Cage(C,n) by A2,A3,A6,A7,Th27; end; theorem for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds LSeg(Gauge(C,n)*(Center Gauge(C,n),1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))) meets Upper_Arc L~Cage(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; A1: 4 <= len Gauge(C,n) by JORDAN8:13; then len Gauge(C,n) >= 2 by AXIOMS:22; then A2: 1 < Center Gauge(C,n) by Th15; len Gauge(C,n) >= 3 by A1,AXIOMS:22; then Center Gauge(C,n) < len Gauge(C,n) by Th16; hence LSeg(Gauge(C,n)*(Center Gauge(C,n),1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))) meets Upper_Arc L~Cage(C,n) by A2,Th32; end; theorem for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds LSeg(Gauge(C,n)*(Center Gauge(C,n),1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))) meets Lower_Arc L~Cage(C,n) proof let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; A1: 4 <= len Gauge(C,n) by JORDAN8:13; then len Gauge(C,n) >= 2 by AXIOMS:22; then A2: 1 < Center Gauge(C,n) by Th15; len Gauge(C,n) >= 3 by A1,AXIOMS:22; then Center Gauge(C,n) < len Gauge(C,n) by Th16; hence LSeg(Gauge(C,n)*(Center Gauge(C,n),1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))) meets Lower_Arc L~Cage(C,n) by A2,Th33; end; theorem Th36: j <= width G implies cell(G,0,j) is not Bounded proof assume A1: j <= width G; per cases by A1,AXIOMS:21,RLVECT_1:99; suppose j = 0; then A2: cell(G,0,j) = { |[r,s]| where r, s is Real : r <= G*(1,1)`1 & s <= G*(1,1)`2 } by GOBRD11:24; not ex r being Real st for q being Point of TOP-REAL 2 st q in cell(G,0,j) holds |.q.| < r proof let r be Real; take q = |[min(-r,G*(1,1)`1),min(-r,G*(1,1)`2)]|; min(-r,G*(1,1)`1) <= G*(1,1)`1 & min(-r,G*(1,1)`2) <= G*(1,1)`2 by SQUARE_1:35; hence q in cell(G,0,j) by A2; A3: abs(q`1)<=|.q.| by JGRAPH_1:50; per cases; suppose A4: r <= 0; abs(q`1) >= 0 by ABSVALUE:5; hence thesis by A4,JGRAPH_1:50; suppose r > 0; then --r > 0; then A5: -r < 0 by REAL_1:66; q`1 = min(-r,G*(1,1)`1) by EUCLID:56; then q`1 <= -r by SQUARE_1:35; then abs(-r) <= abs(q`1) by A5,TOPREAL6:8; then --r <= abs(q`1) by A5,ABSVALUE:def 1; hence thesis by A3,AXIOMS:22; end; hence cell(G,0,j) is not Bounded by JORDAN2C:40; suppose A6: j >= 1 & j < width G; then A7: cell(G,0,j) = { |[r,s]| where r is Element of REAL, s is Element of REAL: r <= G*(1,1)`1 & G*(1,j)`2 <= s & s <= G* (1,j+1)`2 } by GOBRD11:26; not ex r being Real st for q being Point of TOP-REAL 2 st q in cell(G,0,j) holds |.q.| < r proof let r be Real; take q = |[min(-r,G*(1,1)`1),G*(1,j)`2]|; len G <> 0 by GOBOARD1:def 5; then A8: 1 <= len G by RLVECT_1:99; j < j+1 & j+1 <= width G by A6,NAT_1:38; then A9: G*(1,j)`2 <= G*(1,j+1)`2 by A6,A8,GOBOARD5:5; min(-r,G*(1,1)`1) <= G*(1,1)`1 by SQUARE_1:35; hence q in cell(G,0,j) by A7,A9; A10: abs(q`1)<=|.q.| by JGRAPH_1:50; per cases; suppose A11: r <= 0; abs(q`1) >= 0 by ABSVALUE:5; hence thesis by A11,JGRAPH_1:50; suppose r > 0; then --r > 0; then A12: -r < 0 by REAL_1:66; q`1 = min(-r,G*(1,1)`1) by EUCLID:56; then q`1 <= -r by SQUARE_1:35; then abs(-r) <= abs(q`1) by A12,TOPREAL6:8; then --r <= abs(q`1) by A12,ABSVALUE:def 1; hence thesis by A10,AXIOMS:22; end; hence cell(G,0,j) is not Bounded by JORDAN2C:40; suppose j = width G; then A13: cell(G,0,j) = { |[r,s]| where r is Element of REAL, s is Element of REAL : r <= G*(1,1)`1 & G*(1,width G)`2 <= s } by GOBRD11:25; not ex r being Real st for q being Point of TOP-REAL 2 st q in cell(G,0,j) holds |.q.| < r proof let r be Real; take q = |[G*(1,1)`1,max(r,G*(1,width G)`2)]|; G*(1, width G)`2 <= max(r,G*(1,width G)`2) by SQUARE_1:46; hence q in cell(G,0,j) by A13; A14: abs(q`2)<=|.q.| by JGRAPH_1:50; per cases; suppose A15: r <= 0; abs(q`2) >= 0 by ABSVALUE:5; hence thesis by A15,JGRAPH_1:50; suppose A16: r > 0; A17: q`2 = max(r,G*(1,width G)`2) by EUCLID:56; then A18: r <= q`2 by SQUARE_1:46; q`2 > 0 by A16,A17,SQUARE_1:46; then r <= abs(q`2) by A18,ABSVALUE:def 1; hence thesis by A14,AXIOMS:22; end; hence cell(G,0,j) is not Bounded by JORDAN2C:40; end; theorem Th37: i <= width G implies cell(G,len G,i) is not Bounded proof assume A1: i <= width G; per cases by A1,AXIOMS:21,RLVECT_1:99; suppose A2: i = 0; A3: cell(G,len G,0) = { |[r,s]| where r is Element of REAL, s is Element of REAL : G*(len G,1)`1 <= r & s <= G*(1,1)`2 } by GOBRD11:27; not ex r being Real st for q being Point of TOP-REAL 2 st q in cell(G,len G,0) holds |.q.| < r proof let r be Real; take q = |[G*(len G,1)`1,min(-r,G*(1,1)`2)]|; min(-r,G*(1,1)`2) <= G*(1,1)`2 by SQUARE_1:35; hence q in cell(G,len G,0) by A3; A4: abs(q`2)<=|.q.| by JGRAPH_1:50; per cases; suppose A5: r <= 0; abs(q`2) >= 0 by ABSVALUE:5; hence thesis by A5,JGRAPH_1:50; suppose r > 0; then --r > 0; then A6: -r < 0 by REAL_1:66; q`2 = min(-r,G*(1,1)`2) by EUCLID:56; then q`2 <= -r by SQUARE_1:35; then abs(-r) <= abs(q`2) by A6,TOPREAL6:8; then --r <= abs(q`2) by A6,ABSVALUE:def 1; hence thesis by A4,AXIOMS:22; end; hence cell(G,len G,i) is not Bounded by A2,JORDAN2C:40; suppose A7: i >= 1 & i < width G; then A8: cell(G,len G,i) = { |[r,s]| where r is Element of REAL, s is Element of REAL: G*(len G,1)`1 <= r & G*(1,i)`2 <=s & s <= G*(1,i+1)`2 } by GOBRD11:29; not ex r being Real st for q being Point of TOP-REAL 2 st q in cell(G,len G,i) holds |.q.| < r proof let r be Real; take q = |[max(r,G*(len G,1)`1),G*(1,i)`2]|; len G <> 0 by GOBOARD1:def 5; then A9: 1 <= len G by RLVECT_1:99; i < i+1 & i+1 <= width G by A7,NAT_1:38; then A10: G*(1,i)`2 <= G*(1,i+1)`2 by A7,A9,GOBOARD5:5; max(r,G*(len G,1)`1) >= G*(len G,1)`1 by SQUARE_1:46; hence q in cell(G,len G,i) by A8,A10; A11: abs(q`1)<=|.q.| by JGRAPH_1:50; per cases; suppose A12: r <= 0; abs(q`1) >= 0 by ABSVALUE:5; hence thesis by A12,JGRAPH_1:50; suppose A13: r > 0; q`1 = max(r,G*(len G,1)`1) by EUCLID:56; then q`1 >= r by SQUARE_1:46; then abs(r) <= abs(q`1) by A13,TOPREAL6:7; then r <= abs(q`1) by A13,ABSVALUE:def 1; hence thesis by A11,AXIOMS:22; end; hence cell(G,len G,i) is not Bounded by JORDAN2C:40; suppose A14: i = width G; A15: cell(G,len G,width G) = { |[r,s]| where r, s is Real : G*(len G,1)`1 <= r & G*(1,width G)`2 <= s } by GOBRD11:28; not ex r being Real st for q being Point of TOP-REAL 2 st q in cell(G,len G,i) holds |.q.| < r proof let r be Real; take q = |[G*(len G,1)`1,max(r,G*(1,width G)`2)]|; G*(1,width G)`2 <= max(r,G*(1,width G)`2) by SQUARE_1:46; hence q in cell(G,len G,i) by A14,A15; A16: abs(q`2)<=|.q.| by JGRAPH_1:50; per cases; suppose A17: r <= 0; abs(q`2) >= 0 by ABSVALUE:5; hence thesis by A17,JGRAPH_1:50; suppose A18: r > 0; A19: q`2 = max(r,G*(1,width G)`2) by EUCLID:56; then A20: r <= q`2 by SQUARE_1:46; q`2 > 0 by A18,A19,SQUARE_1:46; then r <= abs(q`2) by A20,ABSVALUE:def 1; hence thesis by A16,AXIOMS:22; end; hence cell(G,len G,i) is not Bounded by JORDAN2C:40; end; theorem Th38: j <= width Gauge(C,n) implies cell(Gauge(C,n),0,j) c= UBD C proof A1: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; assume A2: j <= width Gauge(C,n); then cell(Gauge(C,n),0,j) misses C by A1,JORDAN8:21; then A3: cell(Gauge(C,n),0,j) c= C` by SUBSET_1:43; A4: 0 <= width Gauge(C,n) by NAT_1:18; then A5: cell(Gauge(C,n),0,j) is connected by A1,A2,JORDAN1A:46; C is Bounded by JORDAN2C:73; then A6: C` is non empty by JORDAN2C:74; cell(Gauge(C,n),0,j) is non empty by A1,A2,A4,JORDAN1A:45; then consider W being Subset of TOP-REAL 2 such that A7: W is_a_component_of C` and A8: cell(Gauge(C,n),0,j) c= W by A3,A5,A6,GOBOARD9:5; cell(Gauge(C,n),0,j) is not Bounded by A2,Th36; then W is not Bounded by A8,JORDAN2C:16; then W is_outside_component_of C by A7,JORDAN2C:def 4; then W c= UBD C by JORDAN2C:27; hence cell(Gauge(C,n),0,j) c= UBD C by A8,XBOOLE_1:1; end; theorem Th39: j <= len Gauge(E,n) implies cell(Gauge(E,n),len Gauge(E,n),j) c= UBD E proof A1: width Gauge(E,n) = len Gauge(E,n) by JORDAN8:def 1; assume A2: j <= len Gauge(E,n); then cell(Gauge(E,n),len Gauge(E,n),j) misses E by JORDAN8:19; then A3: cell(Gauge(E,n),len Gauge(E,n),j) c= E` by SUBSET_1:43; A4: cell(Gauge(E,n),len Gauge(E,n),j) is connected by A1,A2,JORDAN1A:46; E is Bounded by JORDAN2C:73; then A5: E` is non empty by JORDAN2C:74; cell(Gauge(E,n),len Gauge(E,n),j) is non empty by A1,A2,JORDAN1A:45; then consider W being Subset of TOP-REAL 2 such that A6: W is_a_component_of E` and A7: cell(Gauge(E,n),len Gauge(E,n),j) c= W by A3,A4,A5,GOBOARD9:5; cell(Gauge(E,n),len Gauge(E,n),j) is not Bounded by A1,A2,Th37; then W is not Bounded by A7,JORDAN2C:16; then W is_outside_component_of E by A6,JORDAN2C:def 4; then W c= UBD E by JORDAN2C:27; hence cell(Gauge(E,n),len Gauge(E,n),j) c= UBD E by A7,XBOOLE_1:1; end; Lm4: j <= width Gauge(C,n) & cell(Gauge(C,n),i,j) c= BDD C implies i <> 0 proof assume that A1: j <= width Gauge(C,n) and A2: cell(Gauge(C,n),i,j) c= BDD C and A3: i = 0; 0 <= len Gauge(C,n) by NAT_1:18; then A4: cell(Gauge(C,n),0,j) is non empty by A1,JORDAN1A:45; cell(Gauge(C,n),0,j) c= UBD C by A1,Th38; then UBD C meets BDD C by A2,A3,A4,XBOOLE_1:68; hence contradiction by JORDAN2C:28; end; Lm5: i <= len Gauge(C,n) & cell(Gauge(C,n),i,j) c= BDD C implies j <> 0 proof assume that A1: i <= len Gauge(C,n) and A2: cell(Gauge(C,n),i,j) c= BDD C and A3: j = 0; 0 <= width Gauge(C,n) by NAT_1:18; then A4: cell(Gauge(C,n),i,0) is non empty by A1,JORDAN1A:45; cell(Gauge(C,n),i,0) c= UBD C by A1,JORDAN1A:70; then UBD C meets BDD C by A2,A3,A4,XBOOLE_1:68; hence contradiction by JORDAN2C:28; end; Lm6: j <= width Gauge(C,n) & cell(Gauge(C,n),i,j) c= BDD C implies i <> len Gauge(C,n) proof assume that A1: j <= width Gauge(C,n) and A2: cell(Gauge(C,n),i,j) c= BDD C; A3: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; assume A4: i = len Gauge(C,n); A5: cell(Gauge(C,n),len Gauge(C,n),j) is non empty by A1,JORDAN1A:45; cell(Gauge(C,n),len Gauge(C,n),j) c= UBD C by A1,A3,Th39; then UBD C meets BDD C by A2,A4,A5,XBOOLE_1:68; hence contradiction by JORDAN2C:28; end; Lm7: i <= len Gauge(C,n) & cell(Gauge(C,n),i,j) c= BDD C implies j <> width Gauge(C,n) proof assume that A1: i <= len Gauge(C,n) and A2: cell(Gauge(C,n),i,j) c= BDD C; assume A3: j = width Gauge(C,n); A4: cell(Gauge(C,n),i,width Gauge(C,n)) is non empty by A1,JORDAN1A:45; cell(Gauge(C,n),i,width Gauge(C,n)) c= UBD C by A1,JORDAN1A:71; then UBD C meets BDD C by A2,A3,A4,XBOOLE_1:68; hence contradiction by JORDAN2C:28; end; theorem Th40: i <= len Gauge(C,n) & j <= width Gauge(C,n) & cell(Gauge(C,n),i,j) c= BDD C implies j > 1 proof assume that A1: i <= len Gauge(C,n) and A2: j <= width Gauge(C,n) and A3: cell(Gauge(C,n),i,j) c= BDD C and A4: j <= 1; per cases by A4,CQC_THE1:2; suppose j = 0; hence contradiction by A1,A3,Lm5; suppose A5: j = 1; width Gauge(C,n) <> 0 by GOBOARD1:def 5; then A6: 0+1 <= width Gauge(C,n) by RLVECT_1:99; then A7: cell(Gauge(C,n),i,1) is non empty by A1,JORDAN1A:45; A8: cell(Gauge(C,n),i,0) c= UBD C by A1,JORDAN1A:70; A9: C is Bounded by JORDAN2C:73; i <> len Gauge(C,n) by A2,A3,Lm6; then A10: i < len Gauge(C,n) by A1,AXIOMS:21; A11: 0 < width Gauge(C,n) by A6,NAT_1:38; i <> 0 by A2,A3,Lm4; then 1 <= i by RLVECT_1:99; then cell(Gauge(C,n),i,0) /\ cell(Gauge(C,n),i,0+1) = LSeg(Gauge(C,n)*(i,0+1),Gauge(C,n)*(i+1,0+1)) by A10,A11,GOBOARD5:27; then A12: cell(Gauge(C,n),i,0) meets cell(Gauge(C,n),i,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 A9,JORDAN2C:76; then A13: UBD C is_a_component_of C` by JORDAN2C:def 4; A14: cell(Gauge(C,n),i,1) is connected by A1,A6,JORDAN1A:46; BDD C c= C` by JORDAN2C:29; then cell(Gauge(C,n),i,1) c= C` by A3,A5,XBOOLE_1:1; then cell(Gauge(C,n),i,1) c= UBD C by A8,A12,A13,A14,GOBOARD9:6; then UBD C meets BDD C by A3,A5,A7,XBOOLE_1:68; hence contradiction by JORDAN2C:28; end; theorem Th41: i <= len Gauge(C,n) & j <= width Gauge(C,n) & cell(Gauge(C,n),i,j) c= BDD C implies i > 1 proof assume that A1: i <= len Gauge(C,n) and A2: j <= width Gauge(C,n) and A3: cell(Gauge(C,n),i,j) c= BDD C and A4: i <= 1; per cases by A4,CQC_THE1:2; suppose i = 0; hence contradiction by A2,A3,Lm4; suppose A5: i = 1; len Gauge(C,n) <> 0 by GOBOARD1:def 5; then A6: 0+1 <= len Gauge(C,n) by RLVECT_1:99; then A7: cell(Gauge(C,n),1,j) is non empty by A2,JORDAN1A:45; A8: cell(Gauge(C,n),0,j) c= UBD C by A2,Th38; A9: C is Bounded by JORDAN2C:73; j <> width Gauge(C,n) by A1,A3,Lm7; then A10: j < width Gauge(C,n) by A2,AXIOMS:21; A11: 0 < len Gauge(C,n) by A6,NAT_1:38; j <> 0 by A1,A3,Lm5; then 1 <= j by RLVECT_1:99; then cell(Gauge(C,n),0,j) /\ cell(Gauge(C,n),0+1,j) = LSeg(Gauge(C,n)*(0+1,j),Gauge(C,n)*(0+1,j+1)) by A10,A11,GOBOARD5:26; then A12: cell(Gauge(C,n),0,j) meets cell(Gauge(C,n),0+1,j) by XBOOLE_0: def 7; ex B being Subset of TOP-REAL 2 st B is_outside_component_of C & B=UBD C by A9,JORDAN2C:76; then A13: UBD C is_a_component_of C` by JORDAN2C:def 4; A14: cell(Gauge(C,n),1,j) is connected by A2,A6,JORDAN1A:46; BDD C c= C` by JORDAN2C:29; then cell(Gauge(C,n),1,j) c= C` by A3,A5,XBOOLE_1:1; then cell(Gauge(C,n),1,j) c= UBD C by A8,A12,A13,A14,GOBOARD9:6; then UBD C meets BDD C by A3,A5,A7,XBOOLE_1:68; hence contradiction by JORDAN2C:28; end; theorem Th42: i <= len Gauge(C,n) & j <= width Gauge(C,n) & cell(Gauge(C,n),i,j) c= BDD C implies j+1 < width Gauge(C,n) proof assume that A1: i <= len Gauge(C,n) and A2: j <= width Gauge(C,n) and A3: cell(Gauge(C,n),i,j) c= BDD C; assume j + 1 >= width Gauge(C,n); then A4: j + 1 > width Gauge(C,n) or j + 1 = width Gauge(C,n) by AXIOMS:21; A5: j < width Gauge(C,n) or j = width Gauge(C,n) by A2,AXIOMS:21; per cases by A4,A5,NAT_1:38; suppose j = width Gauge(C,n); hence contradiction by A1,A3,Lm7; suppose j + 1 = width Gauge(C,n); then A6: cell(Gauge(C,n),i,width Gauge(C,n)-'1) c= BDD C by A3,BINARITH:39; width Gauge(C,n)-'1 <= width Gauge(C,n) by JORDAN3:7; then A7: cell(Gauge(C,n),i,width Gauge(C,n)-'1) is non empty by A1,JORDAN1A:45; A8: cell(Gauge(C,n),i,width Gauge(C,n)) c= UBD C by A1,JORDAN1A:71; A9: C is Bounded by JORDAN2C:73; width Gauge(C,n) <> 0 by GOBOARD1:def 5; then A10: 0+1 <= width Gauge(C,n) by RLVECT_1:99; i <> len Gauge(C,n) by A2,A3,Lm6; then A11: i < len Gauge(C,n) by A1,AXIOMS:21; width Gauge(C,n)-1 < width Gauge(C,n) by INT_1:26; then A12: width Gauge(C,n)-'1 < width Gauge(C,n) by A10,SCMFSA_7:3; A13: width Gauge(C,n)-'1+1 = width Gauge(C,n) by A10,AMI_5:4; i <> 0 by A2,A3,Lm4; then 1 <= i by RLVECT_1:99; then cell(Gauge(C,n),i,width Gauge(C,n)) /\ cell(Gauge(C,n),i,width Gauge(C,n)-'1) = LSeg(Gauge(C,n)*(i,width Gauge(C,n)), Gauge(C,n)*(i+1,width Gauge(C,n))) by A11,A12,A13,GOBOARD5:27; then A14: cell(Gauge(C,n),i,width Gauge(C,n)) meets cell(Gauge(C,n),i,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 A9,JORDAN2C:76; then A15: UBD C is_a_component_of C` by JORDAN2C:def 4; A16: cell(Gauge(C,n),i,width Gauge(C,n)-'1) is connected by A1,A12,JORDAN1A:46; BDD C c= C` by JORDAN2C:29; then cell(Gauge(C,n),i,width Gauge(C,n)-'1) c= C` by A6,XBOOLE_1:1; then cell(Gauge(C,n),i,width Gauge(C,n)-'1) c= UBD C by A8,A14,A15,A16,GOBOARD9:6; then UBD C meets BDD C by A6,A7,XBOOLE_1:68; hence contradiction by JORDAN2C:28; end; theorem Th43: i <= len Gauge(C,n) & j <= width Gauge(C,n) & cell(Gauge(C,n),i,j) c= BDD C implies i+1 < len Gauge(C,n) proof assume that A1: i <= len Gauge(C,n) and A2: j <= width Gauge(C,n) and A3: cell(Gauge(C,n),i,j) c= BDD C; assume i + 1 >= len Gauge(C,n); then A4: i + 1 > len Gauge(C,n) or i + 1 = len Gauge(C,n) by AXIOMS:21; A5: i < len Gauge(C,n) or i = len Gauge(C,n) by A1,AXIOMS:21; per cases by A4,A5,NAT_1:38; suppose i = len Gauge(C,n); hence contradiction by A2,A3,Lm6; suppose i + 1 = len Gauge(C,n); then A6: cell(Gauge(C,n),len Gauge(C,n)-'1,j) c= BDD C by A3,BINARITH:39; len Gauge(C,n)-'1 <= len Gauge(C,n) by JORDAN3:7; then A7: cell(Gauge(C,n),len Gauge(C,n)-'1,j) is non empty by A2,JORDAN1A:45; len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; then A8: cell(Gauge(C,n),len Gauge(C,n),j) c= UBD C by A2,Th39; A9: C is Bounded by JORDAN2C:73; len Gauge(C,n) <> 0 by GOBOARD1:def 5; then A10: 0+1 <= len Gauge(C,n) by RLVECT_1:99; j <> width Gauge(C,n) by A1,A3,Lm7; then A11: j < width Gauge(C,n) by A2,AXIOMS:21; len Gauge(C,n)-1 < len Gauge(C,n) by INT_1:26; then A12: len Gauge(C,n)-'1 < len Gauge(C,n) by A10,SCMFSA_7:3; A13: len Gauge(C,n)-'1+1 = len Gauge(C,n) by A10,AMI_5:4; j <> 0 by A1,A3,Lm5; then 1 <= j by RLVECT_1:99; then cell(Gauge(C,n),len Gauge(C,n),j) /\ cell(Gauge(C,n),len Gauge(C,n)-'1,j) = LSeg(Gauge(C,n)*(len Gauge(C,n),j), Gauge(C,n)*(len Gauge(C,n),j+1)) by A11,A12,A13,GOBOARD5:26; then A14: cell(Gauge(C,n),len Gauge(C,n),j) meets cell(Gauge(C,n),len Gauge(C,n)-'1,j) by XBOOLE_0:def 7; ex B being Subset of TOP-REAL 2 st B is_outside_component_of C & B=UBD C by A9,JORDAN2C:76; then A15: UBD C is_a_component_of C` by JORDAN2C:def 4; A16: cell(Gauge(C,n),len Gauge(C,n)-'1,j) is connected by A2,A12,JORDAN1A:46; BDD C c= C` by JORDAN2C:29; then cell(Gauge(C,n),len Gauge(C,n)-'1,j) c= C` by A6,XBOOLE_1:1; then cell(Gauge(C,n),len Gauge(C,n)-'1,j) c= UBD C by A8,A14,A15,A16,GOBOARD9:6; then UBD C meets BDD C by A6,A7,XBOOLE_1:68; hence contradiction by JORDAN2C:28; end; theorem (ex i,j st i <= len Gauge(C,n) & j <= width Gauge(C,n) & cell(Gauge(C,n),i,j) c= BDD C) implies n >= 1 proof given i,j such that A1: i <= len Gauge(C,n) and A2: j <= width Gauge(C,n) and A3: cell(Gauge(C,n),i,j) c= BDD C; A4: width Gauge(C,n) = 2|^n + 3 by JORDAN1A:49; A5: len Gauge(C,n) = 2|^n + 3 by JORDAN8:def 1; A6: j + 1 < width Gauge(C,n) by A1,A2,A3,Th42; A7: i + 1 < len Gauge(C,n) by A1,A2,A3,Th43; A8: 2|^0 = 1 by NEWTON:9; assume A9: n < 1; then A10: width Gauge(C,n) = 1 + 3 by A4,A8,RLVECT_1:99; A11: len Gauge(C,n) = 1 + 3 by A5,A8,A9,RLVECT_1:99; per cases by A1,A2,A10,A11,CQC_THE1:5; suppose j= 0 or j=1; hence thesis by A1,A2,A3,Th40; suppose i= 0 or i=1; hence thesis by A1,A2,A3,Th41; suppose j=2 & i=2; then cell(Gauge(C,0),2,2) c= BDD C by A3,A9,RLVECT_1:99; hence contradiction by Th19; suppose j=3 or j=4 or i=3 or i=4; hence thesis by A6,A7,A10,A11; end;