### The Mizar article:

### Preparing the Internal Approximations of Simple Closed Curves

**by****Andrzej Trybulec**

- Received May 21, 2002
Copyright (c) 2002 Association of Mizar Users

- MML identifier: JORDAN11
- [ MML identifier index ]

environ vocabulary JORDAN1A, JORDAN11, JORDAN8, EUCLID, GROUP_1, FINSEQ_1, ARYTM_1, SEQ_1, BOOLE, GOBOARD5, SETFAM_1, SQUARE_1, FUNCT_1, PSCOMP_1, RCOMP_1, RELAT_2, JORDAN2C, JORDAN6, JORDAN9, PRE_TOPC, RELAT_1, TARSKI, ORDINAL2, CONNSP_1, COMPTS_1, MCART_1, TOPREAL1, TOPREAL2, GOBOARD9, ARYTM_3, SUBSET_1, LATTICES, NAT_1, INT_1, JORDAN10, SEQ_2, FUNCT_5, TREES_1, MATRIX_1, JORDAN1H, JORDAN1E, ARYTM; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1, INT_1, NAT_1, BINARITH, CARD_4, CQC_SIM1, RELAT_1, FUNCT_2, FINSEQ_1, MATRIX_1, SEQ_1, SEQ_4, RCOMP_1, STRUCT_0, PRE_TOPC, CONNSP_1, COMPTS_1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD5, GOBOARD9, PSCOMP_1, JORDAN2C, JORDAN6, JCT_MISC, JORDAN8, JORDAN9, JORDAN10, JORDAN1A, JORDAN1E, JORDAN1H; constructors TOPREAL2, JORDAN8, JORDAN2C, BINARITH, REALSET1, GOBOARD9, JORDAN1, RCOMP_1, PSCOMP_1, CONNSP_1, CQC_SIM1, REAL_1, CARD_4, TOPS_1, JORDAN6, JORDAN9, JORDAN5C, JORDAN1A, JORDAN10, WSIERP_1, JCT_MISC, JORDAN1H, JORDAN1E, PARTFUN1, INT_1; clusters SPRECT_3, BORSUK_2, TOPREAL6, XREAL_0, SUBSET_1, PSCOMP_1, REVROT_1, JORDAN8, INT_1, JORDAN1A, JORDAN1B, JORDAN10, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; definitions TARSKI, XBOOLE_0, JORDAN1H; theorems AXIOMS, CQC_SIM1, JORDAN8, REAL_1, AMI_5, NEWTON, JORDAN3, NAT_1, GOBOARD7, RLVECT_1, GOBOARD5, INT_1, SPRECT_3, XBOOLE_0, XBOOLE_1, JORDAN2C, SUBSET_1, GOBOARD9, ZFMISC_1, CQC_THE1, EUCLID, GOBOARD1, BINARITH, JORDAN6, PSCOMP_1, SPRECT_1, TARSKI, TOPREAL3, SETFAM_1, RCOMP_1, RELAT_1, FUNCT_2, TOPREAL1, PRE_TOPC, COMPTS_1, JORDAN1A, ENUMSET1, SEQ_4, FUNCT_1, XREAL_0, SCMFSA9A, JCT_MISC, JORDAN10, GOBRD14, JORDAN1B, JORDAN1C, SCMFSA_7, PCOMPS_2, JORDAN1F, JORDAN1G, JORDAN1H, JORDAN1I, JORDAN1J, PREPOWER, XCMPLX_1; schemes DOMAIN_1, FUNCT_2; begin reserve i,j,k,n for Nat, C for being_simple_closed_curve Subset of TOP-REAL 2; Lm1: i > 0 & 1 <= j & j <= width Gauge(C,i) & k <= j & 1 <= k & k <= width Gauge(C,i) & LSeg(Gauge(C,i)*(Center Gauge(C,i),j),Gauge(C,i)*(Center Gauge(C,i),k)) /\ Upper_Arc L~Cage(C,i) = {Gauge(C,i)*(Center Gauge(C,i),j)} & LSeg(Gauge(C,i)*(Center Gauge(C,i),j),Gauge(C,i)*(Center Gauge(C,i),k)) /\ Lower_Arc L~Cage(C,i) = {Gauge(C,i)*(Center Gauge(C,i),k)} implies LSeg(Gauge(C,i)*(Center Gauge(C,i),j),Gauge(C,i)*(Center Gauge(C,i),k)) c= Cl RightComp Cage(C,i) proof assume that A1: i > 0 and A2: 1 <= j and A3: j <= width Gauge(C,i) and A4: k <= j and A5: 1 <= k and A6: k <= width Gauge(C,i) and A7: LSeg(Gauge(C,i)*(Center Gauge(C,i),j),Gauge(C,i)*(Center Gauge(C,i),k)) /\ Upper_Arc L~Cage(C,i) = {Gauge(C,i)*(Center Gauge(C,i),j)} and A8: LSeg(Gauge(C,i)*(Center Gauge(C,i),j),Gauge(C,i)*(Center Gauge(C,i),k)) /\ Lower_Arc L~Cage(C,i) = {Gauge(C,i)*(Center Gauge(C,i),k)}; set p = Gauge(C,i)*(Center Gauge(C,i),j), q = Gauge(C,i)*(Center Gauge(C,i),k), S = RightComp Cage(C,i); X-SpanStart(C,i) = Center Gauge(C,i) by JORDAN1H:57; then 2 <= Center Gauge(C,i) & Center Gauge(C,i) < len Gauge(C,i) by JORDAN1H:58; then A9: 1 < Center Gauge(C,i) & Center Gauge(C,i) < len Gauge(C,i) by AXIOMS:22; q in {q} by TARSKI:def 1; then q in Lower_Arc L~Cage(C,i) by A8,XBOOLE_0:def 3; then A10: q in L~Lower_Seq(C,i) by A1,JORDAN1G:64; p in {p} by TARSKI:def 1; then p in Upper_Arc L~Cage(C,i) by A7,XBOOLE_0:def 3; then p in L~Upper_Seq(C,i) by A1,JORDAN1G:63; then A11: j <> k by A2,A6,A9,A10,JORDAN1J:57; A12: [Center Gauge(C,i),j] in Indices Gauge(C,i) by A2,A3,A9,GOBOARD7:10; [Center Gauge(C,i),k] in Indices Gauge(C,i) by A5,A6,A9,GOBOARD7:10; then A13: p <> q by A11,A12,JORDAN1H:32; set A = LSeg(p,q) \ {p,q}; A14: A is connected by JORDAN1H:5; A15: S is_a_component_of (L~Cage(C,i))` by GOBOARD9:def 2; LSeg(p,q) /\ L~Cage(C,i) = LSeg(p,q) /\ (Upper_Arc L~Cage(C,i) \/ Lower_Arc L~Cage(C,i)) by JORDAN6:65 .= LSeg(p,q) /\ Upper_Arc L~Cage(C,i) \/ LSeg(p,q) /\ Lower_Arc L~Cage(C,i) by XBOOLE_1:23 .= {p,q} by A7,A8,ENUMSET1:41; then A misses L~Cage(C,i) by XBOOLE_1:90; then A16: A c= (L~Cage(C,i))` by SUBSET_1:43; A17: LSeg(q,p) meets Upper_Arc C by A1,A3,A4,A5,A7,A8,A9,JORDAN1J:61; Upper_Arc C c= C by JORDAN1A:16; then A18: LSeg(q,p) meets C by A17,XBOOLE_1:63; A19: {p} c= Upper_Arc L~Cage(C,i) by A7,XBOOLE_1:17; {q} c= Lower_Arc L~Cage(C,i) by A8,XBOOLE_1:17; then {p} \/ {q} c= Upper_Arc L~Cage(C,i) \/ Lower_Arc L~Cage(C,i) by A19,XBOOLE_1:13; then {p} \/ {q} c= L~Cage(C,i) by JORDAN6:65; then A20: {p,q} c= L~Cage(C,i) by ENUMSET1:41; L~Cage(C,i) misses C by JORDAN10:5; then {p,q} misses C by A20,XBOOLE_1:63; then A21: A meets C by A18,XBOOLE_1:84; C c= S by JORDAN10:11; then A meets S by A21,XBOOLE_1:63; then A c= S by A14,A15,A16,JORDAN1A:8; hence LSeg(p,q) c= Cl S by A13,JORDAN1H:8; end; Lm2: ex n st n is_sufficiently_large_for C proof set s = (W-bound C + E-bound C)/2, e = Gauge(C,1)*(X-SpanStart(C,1),len Gauge(C,1)), f = Gauge(C,1)*(X-SpanStart(C,1),1); A1: X-SpanStart(C,1) = Center Gauge(C,1) by JORDAN1H:57; then X-SpanStart(C,1) = (len Gauge(C,1)) div 2 + 1 by JORDAN1A:def 1; then A2: 1 <= X-SpanStart(C,1) by NAT_1:29; A3: len Gauge(C,1) >= 4 by JORDAN8:13; then A4: 1 < len Gauge(C,1) by AXIOMS:22; then A5: f`1 = s by A1,JORDAN1A:59; then A6: f in Vertical_Line s by JORDAN1A:17; A7: e`1 = s by A1,A4,JORDAN1A:59; then e in Vertical_Line s by JORDAN1A:17; then A8: LSeg(e,f) c= Vertical_Line s by A6,JORDAN1A:23; A9: len Gauge(C,1) = width Gauge(C,1) by JORDAN8:def 1; 0 < len Gauge(C,1) by A3,AXIOMS:22; then len Gauge(C,1) qua Integer div 2 < len Gauge(C,1) by SCMFSA9A:4; then (len Gauge(C,1)) div 2 < len Gauge(C,1) by SCMFSA9A:5; then (len Gauge(C,1)) div 2 + 1 <= len Gauge(C,1) by NAT_1:38; then X-SpanStart(C,1) <= len Gauge(C,1) by A1,JORDAN1A:def 1; then A10: f`2 < e`2 by A2,A4,A9,GOBOARD5:5; A11: proj2.f = f`2 & proj2.e = e`2 by PSCOMP_1:def 29; A12: W-bound C < E-bound C by SPRECT_1:33; deffunc F(Nat)=inf(proj2.:(LSeg(f,e) /\ Upper_Arc L~Cage(C,$1+1))); consider Es being Real_Sequence such that A13: for i being Nat holds Es.i = F(i) from LambdaD; deffunc G(Nat)=|[s,Es.$1]|; consider E being Function of NAT, the carrier of TOP-REAL 2 such that A14: for i being Nat holds E.i = G(i) from LambdaD; deffunc H(Nat)=sup(proj2.:(LSeg(f,E.$1) /\ Lower_Arc L~Cage(C,$1+1))); consider Fs being Real_Sequence such that A15: for i being Nat holds Fs.i = H(i) from LambdaD; deffunc I(Nat)=|[s,Fs.$1]|; consider F being Function of NAT, the carrier of TOP-REAL 2 such that A16: for i being Nat holds F.i = I(i) from LambdaD; set e1 = proj2.e, f1 = proj2.f; A17: for i holds E.i in Upper_Arc L~Cage(C,i+1) proof let i; set p = E.i; A18: X-SpanStart(C,i+1) = Center Gauge(C,i+1) by JORDAN1H:57; then A19: LSeg(Gauge(C,i+1)*(X-SpanStart(C,i+1),1), Gauge(C,i+1)*(X-SpanStart(C,i+1),len Gauge(C,i+1))) meets Upper_Arc L~Cage(C,i+1) by JORDAN1B:34; i+1 >= 1 by NAT_1:29; then LSeg(Gauge(C,i+1)*(X-SpanStart(C,i+1),1), Gauge(C,i+1)*(X-SpanStart(C,i+1),len Gauge(C,i+1))) c= LSeg(f,e) by A1,A18,JORDAN1A:65; then A20: LSeg(f,e) meets Upper_Arc L~Cage(C,i+1) by A19,XBOOLE_1:63; E.i = |[s,Es.i]| by A14; then A21: p`1 = s & p`2 = Es.i by EUCLID:56; reconsider DD = LSeg(f,e) /\ Upper_Arc L~Cage(C,i+1) as compact Subset of TOP-REAL 2 by PSCOMP_1:64; reconsider D = proj2.:DD as compact Subset of REAL by JORDAN1A:28; DD c= the carrier of TOP-REAL 2; then DD c= dom proj2 by FUNCT_2:def 1; then A22: dom proj2 /\ DD = DD by XBOOLE_1:28; DD <> {} by A20,XBOOLE_0:def 7; then dom proj2 meets DD by A22,XBOOLE_0:def 7; then A23: D <> {} by RELAT_1:151; Es.i = inf D by A13; then Es.i in D by A23,RCOMP_1:32; then consider dd being Point of TOP-REAL 2 such that A24: dd in DD and A25: Es.i = proj2.dd by FUNCT_2:116; A26: dd in Upper_Arc L~Cage(C,i+1) by A24,XBOOLE_0:def 3; dd in LSeg(e,f) by A24,XBOOLE_0:def 3; then A27: dd`1 = p`1 by A8,A21,JORDAN6:34; dd`2 = p`2 by A21,A25,PSCOMP_1:def 29; hence E.i in Upper_Arc L~Cage(C,i+1) by A26,A27,TOPREAL3:11; end; A28: for i holds F.i in Lower_Arc L~Cage(C,i+1) proof let i; set p = F.i; A29: X-SpanStart(C,i+1) = Center Gauge(C,i+1) by JORDAN1H:57; A30: E.i = |[s,Es.i]| by A14; then A31: (E.i)`1 = s by EUCLID:56; (E.i)`2 = Es.i by A30,EUCLID:56 .= inf(proj2.:(LSeg(f,e) /\ Upper_Arc L~Cage(C,i+1))) by A13; then consider j such that A32: 1 <= j and A33: j <= width Gauge(C,i+1) and A34: E.i = Gauge(C,i+1)*(X-SpanStart(C,i+1),j) by A1,A9,A29,A31,JORDAN1F:13; E.i in Upper_Arc L~Cage(C,i+1) by A17; then A35: LSeg(f,E.i) meets Lower_Arc L~Cage(C,i+1) by A1,A29,A32,A33,A34,JORDAN1J:62; F.i = |[s,Fs.i]| by A16; then A36: p`1 = s & p`2 = Fs.i by EUCLID:56; reconsider DD = LSeg(f,E.i) /\ Lower_Arc L~Cage(C,i+1) as compact Subset of TOP-REAL 2 by PSCOMP_1:64; reconsider D = proj2.:DD as compact Subset of REAL by JORDAN1A:28; DD c= the carrier of TOP-REAL 2; then DD c= dom proj2 by FUNCT_2:def 1; then A37: dom proj2 /\ DD = DD by XBOOLE_1:28; DD <> {} by A35,XBOOLE_0:def 7; then dom proj2 meets DD by A37,XBOOLE_0:def 7; then A38: D <> {} by RELAT_1:151; Fs.i = sup D by A15; then Fs.i in D by A38,RCOMP_1:32; then consider dd being Point of TOP-REAL 2 such that A39: dd in DD and A40: Fs.i = proj2.dd by FUNCT_2:116; A41: dd in Lower_Arc L~Cage(C,i+1) by A39,XBOOLE_0:def 3; A42: dd in LSeg(E.i,f) by A39,XBOOLE_0:def 3; E.i in Vertical_Line s by A31,JORDAN1A:17; then LSeg(E.i,f) c= Vertical_Line s by A6,JORDAN1A:23; then A43: dd`1 = p`1 by A36,A42,JORDAN6:34; dd`2 = p`2 by A36,A40,PSCOMP_1:def 29; hence F.i in Lower_Arc L~Cage(C,i+1) by A41,A43,TOPREAL3:11; end; A44: proj2.:LSeg(f,e) = [.f1,e1.] by A10,A11,SPRECT_1:61; deffunc F(Nat)=proj2.:LSeg(E.$1,F.$1); consider S being Function of NAT, bool REAL such that A45: for i being Nat holds S.i = F(i) from LambdaD; set AA = LSeg(e,f) /\ Upper_Arc C, BB = LSeg(e,f) /\ Lower_Arc C; AA is compact & BB is compact by COMPTS_1:20; then reconsider A = proj2.:AA, B = proj2.:BB as compact Subset of REAL by JORDAN1A:28; A46: A misses B proof assume A meets B; then consider z being set such that A47: z in A and A48: z in B by XBOOLE_0:3; reconsider z as Real by A47; consider p being Point of TOP-REAL 2 such that A49: p in AA and A50: z = proj2.p by A47,FUNCT_2:116; consider q being Point of TOP-REAL 2 such that A51: q in BB and A52: z = proj2.q by A48,FUNCT_2:116; A53: q in LSeg(e,f) by A51,XBOOLE_0:def 3; A54: p in LSeg(e,f) by A49,XBOOLE_0:def 3; then A55: p`1 = s by A8,JORDAN6:34 .= q`1 by A8,A53,JORDAN6:34; p`2 = proj2.q by A50,A52,PSCOMP_1:def 29 .= q`2 by PSCOMP_1:def 29; then A56: p = q by A55,TOPREAL3:11; A57: p in Upper_Arc C by A49,XBOOLE_0:def 3; q in Lower_Arc C by A51,XBOOLE_0:def 3; then p in Upper_Arc C /\ Lower_Arc C by A56,A57,XBOOLE_0:def 3; then A58: p in {W-min C,E-max C } by JORDAN6:65; per cases by A58,TARSKI:def 2; suppose p = W-min C; then A59: (W-min C)`1 = s by A8,A54,JORDAN6:34; (W-min C)`1 = W-bound C by PSCOMP_1:84; hence contradiction by A12,A59,XCMPLX_1:67; suppose p = E-max C; then A60: (E-max C)`1 = s by A8,A54,JORDAN6:34; (E-max C)`1 = E-bound C by PSCOMP_1:104; hence contradiction by A12,A60,XCMPLX_1:67; end; AA c= LSeg(e,f) by XBOOLE_1:17; then A61: A c= [.f1,e1.] by A44,RELAT_1:156; BB c= LSeg(e,f) by XBOOLE_1:17; then A62: B c= [.f1,e1.] by A44,RELAT_1:156; for i being Nat holds S.i qua Subset of REAL is connected & S.i meets A & S.i meets B proof let i be Nat; A63: S.i = proj2.:LSeg(E.i,F.i) by A45; hence S.i is connected by JCT_MISC:15; reconsider DD = LSeg(e,f) /\ Upper_Arc L~Cage(C,i+1) as compact Subset of TOP-REAL 2 by PSCOMP_1:64; reconsider D = proj2.:DD as compact Subset of REAL by JORDAN1A:28; A64: E.i = |[s,Es.i]| by A14; then A65: (E.i)`1 = s by EUCLID:56; A66: X-SpanStart(C,i+1) = Center Gauge(C,i+1) by JORDAN1H:57; A67: F.i = |[s,Fs.i]| by A16; then A68: (F.i)`1 = s by EUCLID:56; A69: LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),1), Gauge(C,i+1)*(Center Gauge(C,i+1),len Gauge(C,i+1))) meets Upper_Arc L~Cage(C,i+1) by JORDAN1B:34; 1 <= i+1 by NAT_1:29; then LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),1), Gauge(C,i+1)*(Center Gauge(C,i+1),len Gauge(C,i+1))) c= LSeg(Gauge(C,1)*(Center Gauge(C,1),1), Gauge(C,1)*(Center Gauge(C,1),len Gauge(C,1))) by JORDAN1A:65; then A70: LSeg(f,e) meets Upper_Arc L~Cage(C,i+1) by A1,A69,XBOOLE_1:63; DD c= the carrier of TOP-REAL 2; then DD c= dom proj2 by FUNCT_2:def 1; then A71: dom proj2 /\ DD = DD by XBOOLE_1:28; DD <> {} by A70,XBOOLE_0:def 7; then dom proj2 meets DD by A71,XBOOLE_0:def 7; then A72: D <> {} by RELAT_1:151; Es.i = inf D by A13; then Es.i in D by A72,RCOMP_1:32; then consider dd being Point of TOP-REAL 2 such that A73: dd in DD and A74: Es.i = proj2.dd by FUNCT_2:116; A75: dd in LSeg(f,e) by A73,XBOOLE_0:def 3; then A76: dd`1 = (E.i)`1 by A8,A65,JORDAN6:34; A77: (E.i)`2 = Es.i by A64,EUCLID:56 .= dd`2 by A74,PSCOMP_1:def 29; then A78: E.i in LSeg(e,f) by A75,A76,TOPREAL3:11; f in LSeg(e,f) by TOPREAL1:6; then A79: LSeg(f,E.i) c= LSeg(e,f) by A78,TOPREAL1:12; reconsider DD = LSeg(f,E.i) /\ Lower_Arc L~Cage(C,i+1) as compact Subset of TOP-REAL 2 by PSCOMP_1:64; reconsider D = proj2.:DD as compact Subset of REAL by JORDAN1A:28; (E.i)`2 = Es.i by A64,EUCLID:56 .= inf(proj2.:(LSeg(f,e) /\ Upper_Arc L~Cage(C,i+1))) by A13; then consider j such that A80: 1 <= j and A81: j <= width Gauge(C,i+1) and A82: E.i = Gauge(C,i+1)*(X-SpanStart(C,i+1),j) by A1,A9,A65,A66,JORDAN1F:13; A83: E.i in Upper_Arc L~Cage(C,i+1) by A17; then A84: LSeg(f,E.i) meets Lower_Arc L~Cage(C,i+1) by A1,A66,A80,A81,A82,JORDAN1J:62; DD c= the carrier of TOP-REAL 2; then DD c= dom proj2 by FUNCT_2:def 1; then A85: dom proj2 /\ DD = DD by XBOOLE_1:28; DD <> {} by A84,XBOOLE_0:def 7; then dom proj2 meets DD by A85,XBOOLE_0:def 7; then A86: D <> {} by RELAT_1:151; Fs.i = sup D by A15; then Fs.i in D by A86,RCOMP_1:32; then consider dd being Point of TOP-REAL 2 such that A87: dd in DD and A88: Fs.i = proj2.dd by FUNCT_2:116; A89: dd in LSeg(E.i,f) by A87,XBOOLE_0:def 3; E.i in Vertical_Line s by A65,JORDAN1A:17; then LSeg(E.i,f) c= Vertical_Line s by A6,JORDAN1A:23; then A90: dd`1 = (F.i)`1 by A68,A89,JORDAN6:34; (F.i)`2 = Fs.i by A67,EUCLID:56 .= dd`2 by A88,PSCOMP_1:def 29; then A91: F.i in LSeg(E.i,f) by A89,A90,TOPREAL3:11; then A92: LSeg(E.i,F.i) c= LSeg(e,f) by A78,A79,TOPREAL1:12; E.i in LSeg(E.i,f) by TOPREAL1:6; then A93: LSeg(E.i,F.i) c= LSeg(E.i,f) by A91,TOPREAL1:12; (E.i)`2 = Es.i by A64,EUCLID:56 .= inf(proj2.:(LSeg(f,e) /\ Upper_Arc L~Cage(C,i+1))) by A13; then consider j such that A94: 1 <= j and A95: j <= width Gauge(C,i+1) and A96: E.i = Gauge(C,i+1)*(X-SpanStart(C,i+1),j) by A1,A9,A65,A66,JORDAN1F:13; i+1 >= 0+1 by NAT_1:29; then A97: i+1 > 0 by NAT_1:38; A98: (F.i)`2 =Fs.i by A67,EUCLID:56 .= sup(proj2.:(LSeg(f,E.i) /\ Lower_Arc L~Cage(C,i+1)))by A15; then consider k such that A99: 1 <= k and A100: k <= width Gauge(C,i+1) and A101: F.i = Gauge(C,i+1)*(Center Gauge(C,i+1),k) by A1,A66,A68,A83,A94,A95,A96,A97,JORDAN1I:30; A102: F.i in Lower_Arc L~Cage(C,i+1) by A28; A103: 1 <= Center Gauge(C,i+1) by JORDAN1B:12; A104: Center Gauge(C,i+1) <= len Gauge(C,i+1) by JORDAN1B:14; for p being real number st p in D holds p <= (E.i)`2 proof let p be real number; assume p in D; then consider x being set such that x in dom proj2 and A105: x in DD and A106: p = proj2.x by FUNCT_1:def 12; reconsider x as Point of TOP-REAL 2 by A105; A107: f`2 <= (E.i)`2 by A10,A75,A77,TOPREAL1:10; x in LSeg(f,E.i) by A105,XBOOLE_0:def 3; then x`2 <= (E.i)`2 by A107,TOPREAL1:10; hence p <= (E.i)`2 by A106,PSCOMP_1:def 29; end; then A108: sup D <= (E.i)`2 by A86,PSCOMP_1:10; then A109: k <= j by A66,A94,A96,A98,A100,A101,A103,A104,GOBOARD5:5; A110: for x be set holds x in LSeg(E.i,F.i) /\ Upper_Arc L~Cage(C,i+1) implies x = E.i proof reconsider DD = LSeg(f,e) /\ Upper_Arc L~Cage(C,i+1) as compact Subset of TOP-REAL 2 by PSCOMP_1:64; reconsider D = proj2.:DD as compact Subset of REAL by JORDAN1A:28; let x be set; assume A111: x in LSeg(E.i,F.i) /\ Upper_Arc L~Cage(C,i+1); then reconsider p = x as Point of TOP-REAL 2; A112: p in LSeg(E.i,F.i) by A111,XBOOLE_0:def 3; then A113: p`1 = (E.i)`1 by A65,A68,GOBOARD7:5; A114: p`2 <= (E.i)`2 by A98,A108,A112,TOPREAL1:10; E.i = |[s,Es.i]| by A14; then A115: (E.i)`2 = Es.i by EUCLID:56 .= inf D by A13; D is bounded by RCOMP_1:28; then A116: D is bounded_below by SEQ_4:def 3; p in Upper_Arc L~Cage(C,i+1) by A111,XBOOLE_0:def 3; then p in DD by A92,A112,XBOOLE_0:def 3; then proj2.p in D by FUNCT_2:43; then p`2 in D by PSCOMP_1:def 29; then (E.i)`2 <= p`2 by A115,A116,SEQ_4:def 5; then p`2 = (E.i)`2 by A114,AXIOMS:21; hence x = E.i by A113,TOPREAL3:11; end; A117: for x be set holds x in LSeg(E.i,F.i) /\ Lower_Arc L~Cage(C,i+1) implies x = F.i proof reconsider EE = LSeg(f,E.i) /\ Lower_Arc L~Cage(C,i+1) as compact Subset of TOP-REAL 2 by PSCOMP_1:64; reconsider E0 = proj2.:EE as compact Subset of REAL by JORDAN1A:28; let x be set; assume A118: x in LSeg(E.i,F.i) /\ Lower_Arc L~Cage(C,i+1); then reconsider p = x as Point of TOP-REAL 2; A119: p in LSeg(E.i,F.i) by A118,XBOOLE_0:def 3; then A120: p`1 = (F.i)`1 by A65,A68,GOBOARD7:5; A121: p`2 >= (F.i)`2 by A98,A108,A119,TOPREAL1:10; F.i = |[s,Fs.i]| by A16; then A122: (F.i)`2 = Fs.i by EUCLID:56 .= sup E0 by A15; E0 is bounded by RCOMP_1:28; then A123: E0 is bounded_above by SEQ_4:def 3; p in Lower_Arc L~Cage(C,i+1) by A118,XBOOLE_0:def 3; then p in EE by A93,A119,XBOOLE_0:def 3; then proj2.p in E0 by FUNCT_2:43; then p`2 in E0 by PSCOMP_1:def 29; then (F.i)`2 >= p`2 by A122,A123,SEQ_4:def 4; then p`2 = (F.i)`2 by A121,AXIOMS:21; hence x = F.i by A120,TOPREAL3:11; end; A124: Gauge(C,i+1)*(Center Gauge(C,i+1),j) in LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),k), Gauge(C,i+1)*(Center Gauge(C,i+1),j)) & Gauge(C,i+1)*(Center Gauge(C,i+1),k) in LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),k), Gauge(C,i+1)*(Center Gauge(C,i+1),j)) by TOPREAL1:6; A125: LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),k), Gauge(C,i+1)*(Center Gauge(C,i+1),j)) /\ Upper_Arc L~Cage(C,i+1) = {Gauge(C,i+1)*(Center Gauge(C,i+1),j)} proof thus LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),k), Gauge(C,i+1)*(Center Gauge(C,i+1),j)) /\ Upper_Arc L~Cage(C,i+1) c= {Gauge(C,i+1)*(Center Gauge(C,i+1),j)} proof let x be set; assume x in LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),k), Gauge(C,i+1)*(Center Gauge(C,i+1),j)) /\ Upper_Arc L~Cage(C,i+1); then x = Gauge(C,i+1)*(Center Gauge(C,i+1),j) by A66,A96,A101,A110; hence x in {Gauge(C,i+1)*(Center Gauge(C,i+1),j)} by TARSKI:def 1; end; let x be set; assume x in {Gauge(C,i+1)*(Center Gauge(C,i+1),j)}; then x = Gauge(C,i+1)*(Center Gauge(C,i+1),j) by TARSKI:def 1; hence x in LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),k), Gauge(C,i+1)*(Center Gauge(C,i+1),j)) /\ Upper_Arc L~Cage(C,i+1) by A66,A83,A96,A124,XBOOLE_0:def 3; end; A126: LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),k), Gauge(C,i+1)*(Center Gauge(C,i+1),j)) /\ Lower_Arc L~Cage(C,i+1) = {Gauge(C,i+1)*(Center Gauge(C,i+1),k)} proof thus LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),k), Gauge(C,i+1)*(Center Gauge(C,i+1),j)) /\ Lower_Arc L~Cage(C,i+1) c= {Gauge(C,i+1)*(Center Gauge(C,i+1),k)} proof let x be set; assume x in LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),k), Gauge(C,i+1)*(Center Gauge(C,i+1),j)) /\ Lower_Arc L~Cage(C,i+1); then x = Gauge(C,i+1)*(Center Gauge(C,i+1),k) by A66,A96,A101,A117; hence x in {Gauge(C,i+1)*(Center Gauge(C,i+1),k)} by TARSKI:def 1; end; let x be set; assume x in {Gauge(C,i+1)*(Center Gauge(C,i+1),k)}; then x = Gauge(C,i+1)*(Center Gauge(C,i+1),k) by TARSKI:def 1; hence thesis by A101,A102,A124,XBOOLE_0:def 3; end; then LSeg(F.i,E.i) meets Upper_Arc C by A66,A95,A96,A99,A101,A109,A125,JORDAN1J:64; then LSeg(E.i,F.i) meets AA by A92,XBOOLE_1:77; hence S.i meets A by A63,JORDAN1A:24; LSeg(E.i,F.i) meets Lower_Arc C by A66,A95,A96,A99,A101,A109,A125,A126,JORDAN1J:63; then LSeg(E.i,F.i) meets BB by A92,XBOOLE_1:77; hence S.i meets B by A63,JORDAN1A:24; end; then consider r being real number such that A127: r in [.f1,e1.] and A128: not r in A \/ B and A129: for i being Nat ex k being Nat st i <= k & r in S.k by A46,A61,A62,JCT_MISC:21; reconsider r as Real by XREAL_0:def 1; set p = |[s,r]|; A130: p in LSeg(e,f) by A5,A7,A127,JORDAN1A:21; A131: p`1 = s by EUCLID:56; A132: now assume p in C; then p in Lower_Arc C \/ Upper_Arc C by JORDAN6:65; then p in (Lower_Arc C \/ Upper_Arc C) /\ LSeg(e,f) by A130,XBOOLE_0:def 3; then p in AA \/ BB by XBOOLE_1:23; then proj2.p in proj2.:(AA \/ BB) by FUNCT_2:43; then r in proj2.:(AA \/ BB) by JORDAN1A:20; hence contradiction by A128,RELAT_1:153; end; A133: meet BDD-Family C = C \/ BDD C by JORDAN10:21; for Y being set st Y in BDD-Family C holds p in Y proof let Y be set; A134: BDD-Family C = { Cl BDD L~Cage(C,k1) where k1 is Nat : not contradiction } by JORDAN10:def 2; assume Y in BDD-Family C; then consider k1 being Nat such that A135: Y = Cl BDD L~Cage(C,k1) by A134; consider k0 being Nat such that A136: k1 <= k0 and A137: r in S.k0 by A129; A138: E.k0 = |[s,Es.k0]| by A14; then A139: (E.k0)`1 = s by EUCLID:56; A140: F.k0 = |[s,Fs.k0]| by A16; then A141: (F.k0)`1 = s by EUCLID:56; A142: proj2.(E.k0) = (E.k0)`2 & proj2.(F.k0) = (F.k0)`2 by PSCOMP_1:def 29; reconsider DD = LSeg(f,E.k0) /\ Lower_Arc L~Cage(C,k0+1) as compact Subset of TOP-REAL 2 by PSCOMP_1:64; reconsider D = proj2.:DD as compact Subset of REAL by JORDAN1A:28; A143: X-SpanStart(C,k0+1) = Center Gauge(C,k0+1) by JORDAN1H:57; (E.k0)`2 = Es.k0 by A138,EUCLID:56 .= inf(proj2.:(LSeg(f,e) /\ Upper_Arc L~Cage(C,k0+1))) by A13; then consider j such that A144: 1 <= j and A145: j <= width Gauge(C,k0+1) and A146: E.k0 = Gauge(C,k0+1)*(X-SpanStart(C,k0+1),j) by A1,A9,A139,A143,JORDAN1F:13; E.k0 in Upper_Arc L~Cage(C,k0+1) by A17; then A147: LSeg(f,E.k0) meets Lower_Arc L~Cage(C,k0+1) by A1,A143,A144,A145,A146,JORDAN1J:62; DD c= the carrier of TOP-REAL 2; then DD c= dom proj2 by FUNCT_2:def 1; then A148: dom proj2 /\ DD = DD by XBOOLE_1:28; DD <> {} by A147,XBOOLE_0:def 7; then dom proj2 meets DD by A148,XBOOLE_0:def 7; then A149: D <> {} by RELAT_1:151; Fs.k0 = sup D by A15; then Fs.k0 in D by A149,RCOMP_1:32; then consider dd being Point of TOP-REAL 2 such that A150: dd in DD and A151: Fs.k0 = proj2.dd by FUNCT_2:116; A152: dd in LSeg(E.k0,f) by A150,XBOOLE_0:def 3; E.k0 in Vertical_Line s by A139,JORDAN1A:17; then LSeg(E.k0,f) c= Vertical_Line s by A6,JORDAN1A:23; then A153: dd`1 = (F.k0)`1 by A141,A152,JORDAN6:34; A154: (F.k0)`2 = Fs.k0 by A140,EUCLID:56 .= dd`2 by A151,PSCOMP_1:def 29; then A155: F.k0 in LSeg(E.k0,f) by A152,A153,TOPREAL3:11; reconsider DD = LSeg(f,e) /\ Upper_Arc L~Cage(C,k0+1) as compact Subset of TOP-REAL 2 by PSCOMP_1:64; reconsider D = proj2.:DD as compact Subset of REAL by JORDAN1A:28; A156: LSeg(Gauge(C,k0+1)*(Center Gauge(C,k0+1),1), Gauge(C,k0+1)*(Center Gauge(C,k0+1),len Gauge(C,k0+1))) meets Upper_Arc L~Cage(C,k0+1) by JORDAN1B:34; 1+0 <= k0+1 by NAT_1:29; then LSeg(Gauge(C,k0+1)*(Center Gauge(C,k0+1),1), Gauge(C,k0+1)*(Center Gauge(C,k0+1),len Gauge(C,k0+1))) c= LSeg(Gauge(C,1)*(Center Gauge(C,1),1), Gauge(C,1)*(Center Gauge(C,1),len Gauge(C,1))) by JORDAN1A:65; then A157: LSeg(f,e) meets Upper_Arc L~Cage(C,k0+1) by A1,A156,XBOOLE_1: 63; DD c= the carrier of TOP-REAL 2; then DD c= dom proj2 by FUNCT_2:def 1; then A158: dom proj2 /\ DD = DD by XBOOLE_1:28; DD <> {} by A157,XBOOLE_0:def 7; then dom proj2 meets DD by A158,XBOOLE_0:def 7; then A159: D <> {} by RELAT_1:151; Es.k0 = inf D by A13; then Es.k0 in D by A159,RCOMP_1:32; then consider dd being Point of TOP-REAL 2 such that A160: dd in DD and A161: Es.k0 = proj2.dd by FUNCT_2:116; A162: dd in LSeg(f,e) by A160,XBOOLE_0:def 3; then A163: dd`1 = (E.k0)`1 by A8,A139,JORDAN6:34; A164: (E.k0)`2 = Es.k0 by A138,EUCLID:56 .= dd`2 by A161,PSCOMP_1:def 29; then A165: E.k0 in LSeg(f,e) by A162,A163,TOPREAL3:11; A166: f`2 <= (E.k0)`2 by A10,A162,A164,TOPREAL1:10; then A167: (F.k0)`2 <= (E.k0)`2 by A152,A154,TOPREAL1:10; r in proj2.:LSeg(E.k0,F.k0) by A45,A137; then r in [.proj2.(F.k0),proj2.(E.k0).] by A142,A167,SPRECT_1:61; then A168: p in LSeg(E.k0,F.k0) by A139,A141,JORDAN1A:21; (E.k0)`2 = Es.k0 by A138,EUCLID:56 .= inf(proj2.:(LSeg(f,e) /\ Upper_Arc L~Cage(C,k0+1))) by A13; then consider j such that A169: 1 <= j and A170: j <= width Gauge(C,k0+1) and A171: E.k0 = Gauge(C,k0+1)*(X-SpanStart(C,k0+1),j) by A1,A9,A139,A143,JORDAN1F:13; A172: E.k0 in Upper_Arc L~Cage(C,k0+1) by A17; A173: F.k0 in Lower_Arc L~Cage(C,k0+1) by A28; k0+1 >= 0+1 by NAT_1:29; then A174: k0+1 > 0 by NAT_1:38; A175: (F.k0)`2 =Fs.k0 by A140,EUCLID:56 .= sup(proj2.:(LSeg(f,E.k0) /\ Lower_Arc L~Cage(C,k0+1)))by A15; then consider k such that A176: 1 <= k and A177: k <= width Gauge(C,k0+1) and A178: F.k0 = Gauge(C,k0+1)*(X-SpanStart(C,k0+1),k) by A1,A141,A143,A169,A170,A171,A172,A174,JORDAN1I:30; reconsider CC = LSeg(f,E.k0) /\ Lower_Arc L~Cage(C,k0+1) as compact Subset of TOP-REAL 2 by PSCOMP_1:64; reconsider W = proj2.:CC as compact Subset of REAL by JORDAN1A:28; CC c= the carrier of TOP-REAL 2; then CC c= dom proj2 by FUNCT_2:def 1; then A179: dom proj2 /\ CC = CC by XBOOLE_1:28; CC <> {} by A147,XBOOLE_0:def 7; then dom proj2 meets CC by A179,XBOOLE_0:def 7; then A180: W <> {} by RELAT_1:151; A181: 1 <= Center Gauge(C,k0+1) by JORDAN1B:12; A182: Center Gauge(C,k0+1) <= len Gauge(C,k0+1) by JORDAN1B:14; for p being real number st p in W holds p <= (E.k0)`2 proof let p be real number; assume p in W; then consider x being set such that x in dom proj2 and A183: x in CC and A184: p = proj2.x by FUNCT_1:def 12; reconsider x as Point of TOP-REAL 2 by A183; x in LSeg(f,E.k0) by A183,XBOOLE_0:def 3; then x`2 <= (E.k0)`2 by A166,TOPREAL1:10; hence p <= (E.k0)`2 by A184,PSCOMP_1:def 29; end; then sup W <= (E.k0)`2 by A180,PSCOMP_1:10; then A185: k <= j by A143,A169,A171,A175,A177,A178,A181,A182,GOBOARD5:5; A186: E.k0 in LSeg(f,E.k0) by TOPREAL1:6; then A187: LSeg(E.k0,F.k0) c= LSeg(f,E.k0) by A155,TOPREAL1:12; f in LSeg(f,e) by TOPREAL1:6; then LSeg(f,E.k0) c= LSeg(e,f) by A165,TOPREAL1:12; then A188: LSeg(E.k0,F.k0) c= LSeg(e,f) by A155,A186,TOPREAL1:12; for x being set holds x in LSeg(E.k0,F.k0) /\ Upper_Arc L~Cage(C,k0+1) iff x = E.k0 proof let x be set; thus x in LSeg(E.k0,F.k0) /\ Upper_Arc L~Cage(C,k0+1) implies x = E.k0 proof assume A189: x in LSeg(E.k0,F.k0) /\ Upper_Arc L~Cage(C,k0+1); then reconsider p = x as Point of TOP-REAL 2; A190: p in LSeg(E.k0,F.k0) by A189,XBOOLE_0:def 3; then A191: p`1 = (E.k0)`1 by A139,A141,GOBOARD7:5; A192: p`2 <= (E.k0)`2 by A167,A190,TOPREAL1:10; E.k0 = |[s,Es.k0]| by A14; then A193: (E.k0)`2 = Es.k0 by EUCLID:56 .= inf D by A13; D is bounded by RCOMP_1:28; then A194: D is bounded_below by SEQ_4:def 3; p in Upper_Arc L~Cage(C,k0+1) by A189,XBOOLE_0:def 3; then p in DD by A188,A190,XBOOLE_0:def 3; then proj2.p in D by FUNCT_2:43; then p`2 in D by PSCOMP_1:def 29; then (E.k0)`2 <= p`2 by A193,A194,SEQ_4:def 5; then p`2 = (E.k0)`2 by A192,AXIOMS:21; hence x = E.k0 by A191,TOPREAL3:11; end; assume A195: x = E.k0; then x in LSeg(E.k0,F.k0) by TOPREAL1:6; hence x in LSeg(E.k0,F.k0) /\ Upper_Arc L~Cage(C,k0+1) by A172,A195,XBOOLE_0:def 3; end; then A196: LSeg(E.k0,F.k0) /\ Upper_Arc L~Cage(C,k0+1) = {E.k0} by TARSKI: def 1; reconsider EE = LSeg(f,E.k0) /\ Lower_Arc L~Cage(C,k0+1) as compact Subset of TOP-REAL 2 by PSCOMP_1:64; reconsider E0 = proj2.:EE as compact Subset of REAL by JORDAN1A:28; for x being set holds x in LSeg(E.k0,F.k0) /\ Lower_Arc L~Cage(C,k0+1) iff x = F.k0 proof let x be set; thus x in LSeg(E.k0,F.k0) /\ Lower_Arc L~Cage(C,k0+1) implies x = F.k0 proof assume A197: x in LSeg(E.k0,F.k0) /\ Lower_Arc L~Cage(C,k0+1); then reconsider p = x as Point of TOP-REAL 2; A198: p in LSeg(E.k0,F.k0) by A197,XBOOLE_0:def 3; then A199: p`1 = (F.k0)`1 by A139,A141,GOBOARD7:5; A200: p`2 >= (F.k0)`2 by A167,A198,TOPREAL1:10; F.k0 = |[s,Fs.k0]| by A16; then A201: (F.k0)`2 = Fs.k0 by EUCLID:56 .= sup E0 by A15; E0 is bounded by RCOMP_1:28; then A202: E0 is bounded_above by SEQ_4:def 3; p in Lower_Arc L~Cage(C,k0+1) by A197,XBOOLE_0:def 3; then p in EE by A187,A198,XBOOLE_0:def 3; then proj2.p in E0 by FUNCT_2:43; then p`2 in E0 by PSCOMP_1:def 29; then (F.k0)`2 >= p`2 by A201,A202,SEQ_4:def 4; then p`2 = (F.k0)`2 by A200,AXIOMS:21; hence x = F.k0 by A199,TOPREAL3:11; end; assume A203: x = F.k0; then x in LSeg(E.k0,F.k0) by TOPREAL1:6; hence x in LSeg(E.k0,F.k0) /\ Lower_Arc L~Cage(C,k0+1) by A173,A203,XBOOLE_0:def 3; end; then LSeg(E.k0,F.k0) /\ Lower_Arc L~Cage(C,k0+1) = {F.k0} by TARSKI:def 1 ; then LSeg(E.k0,F.k0) c= Cl RightComp Cage(C,k0+1) by A143,A169,A170,A171,A174,A176,A177,A178,A185,A196,Lm1; then A204: p in Cl RightComp Cage(C,k0+1) by A168; k0 <= k0+1 by NAT_1:29; then A205: RightComp Cage(C,k0+1) c= RightComp Cage(C,k0) by JORDAN1H:56; RightComp Cage(C,k0) c= RightComp Cage(C,k1) by A136,JORDAN1H:56; then RightComp Cage(C,k0+1) c= RightComp Cage(C,k1) by A205,XBOOLE_1:1; then Cl RightComp Cage(C,k0+1) c= Cl RightComp Cage(C,k1) by PRE_TOPC:49; then p in Cl RightComp Cage(C,k1) by A204; hence p in Y by A135,GOBRD14:47; end; then p in meet BDD-Family C by SETFAM_1:def 1; then p in BDD C by A132,A133,XBOOLE_0:def 2; then consider n,i,j such that A206: 1 < i and A207: i < len Gauge(C,n) and A208: 1 < j and A209: j < width Gauge(C,n) and A210: p`1 <> (Gauge(C,n)*(i,j))`1 and A211: p in cell(Gauge(C,n),i,j) and A212: cell(Gauge(C,n),i,j) c= BDD C by JORDAN1C:35; take n,j; thus j < width Gauge(C,n) by A209; n >= 0+1 by A207,A209,A212,JORDAN1B:44; then A213: n > 0 by NAT_1:38; A214: X-SpanStart(C,n) = Center Gauge(C,n) by JORDAN1H:57; 2 <= X-SpanStart(C,n) by JORDAN1H:58; then A215: 1 <= X-SpanStart(C,n) & X-SpanStart(C,n) <= len Gauge(C,n) by AXIOMS:22,JORDAN1H:58; 4 <= len Gauge (C,1) by JORDAN8:13; then A216: 1 <= len Gauge (C,1) by AXIOMS:22; len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; then (Gauge(C,n)*(X-SpanStart(C,n),j))`1 = s by A1,A5,A208,A209,A213,A214,A216,JORDAN1A:57; hence cell(Gauge(C,n),X-SpanStart(C,n)-'1,j) c= BDD C by A131,A206,A207,A208,A209,A210,A211,A212,A215,JORDAN1B:23; end; definition let C; func ApproxIndex C -> Nat means :Def1: it is_sufficiently_large_for C & for j st j is_sufficiently_large_for C holds j >= it; existence proof defpred P[Nat] means $1 is_sufficiently_large_for C; set X = {i : P[i]}; consider i such that A1: i is_sufficiently_large_for C by Lm2; A2: i in X by A1; X is Subset of NAT from SubsetD; then reconsider X as non empty Subset of NAT by A2; take min X; min X in X by CQC_SIM1:def 8; then ex i st i = min X & i is_sufficiently_large_for C; hence min X is_sufficiently_large_for C; let j; assume j is_sufficiently_large_for C; then j in X; hence j >= min X by CQC_SIM1:def 8; end; uniqueness proof let it1,it2 be Nat such that A3: it1 is_sufficiently_large_for C and A4: for j st j is_sufficiently_large_for C holds j >= it1 and A5: it2 is_sufficiently_large_for C and A6: for j st j is_sufficiently_large_for C holds j >= it2; it1 <= it2 & it2 <= it1 by A3,A4,A5,A6; hence it1 = it2 by AXIOMS:21; end; end; theorem Th1: ApproxIndex C >= 1 proof ApproxIndex C is_sufficiently_large_for C by Def1; hence thesis by JORDAN1H:60; end; definition let C; func Y-InitStart C -> Nat means :Def2: it < width Gauge(C,ApproxIndex C) & cell(Gauge(C,ApproxIndex C),X-SpanStart(C,ApproxIndex C)-'1,it) c= BDD C & for j st j < width Gauge(C,ApproxIndex C) & cell(Gauge(C,ApproxIndex C),X-SpanStart(C,ApproxIndex C)-'1,j) c= BDD C holds j >= it; existence proof set n = ApproxIndex C; defpred P[Nat] means $1 < width Gauge(C,n) & cell(Gauge(C,n),X-SpanStart(C,n)-'1,$1) c= BDD C; n is_sufficiently_large_for C by Def1; then consider j such that A1: P[j] by JORDAN1H:def 3; set X = { i: P[i] }; A2: j in X by A1; X is Subset of NAT from SubsetD; then reconsider X as non empty Subset of NAT by A2; take min X; min X in X by CQC_SIM1:def 8; then ex i st i = min X & P[i]; hence P[min X]; let i; assume P[i]; then i in X; hence thesis by CQC_SIM1:def 8; end; uniqueness proof let it1,it2 be Nat; assume it1 < width Gauge(C,ApproxIndex C) & cell(Gauge(C,ApproxIndex C),X-SpanStart(C,ApproxIndex C)-'1,it1) c= BDD C & (for j st j < width Gauge(C,ApproxIndex C) & cell(Gauge(C,ApproxIndex C),X-SpanStart(C,ApproxIndex C)-'1,j) c= BDD C holds j >= it1) & it2 < width Gauge(C,ApproxIndex C) & cell(Gauge(C,ApproxIndex C),X-SpanStart(C,ApproxIndex C)-'1,it2) c= BDD C & for j st j < width Gauge(C,ApproxIndex C) & cell(Gauge(C,ApproxIndex C),X-SpanStart(C,ApproxIndex C)-'1,j) c= BDD C holds j >= it2; then it1 <= it2 & it2 <= it1; hence thesis by AXIOMS:21; end; end; theorem Th2: Y-InitStart C > 1 proof set m = ApproxIndex C; A1: X-SpanStart(C,m)-'1 <= len Gauge(C,m) by JORDAN1H:59; assume A2: Y-InitStart C <= 1; per cases by A2,CQC_THE1:2; suppose Y-InitStart C = 0; then A3: cell(Gauge(C,m),X-SpanStart(C,m)-'1,0) c= BDD C by Def2; 0 <= width Gauge(C,m) by NAT_1:18; then A4: cell(Gauge(C,m),X-SpanStart(C,m)-'1,0) is non empty by A1,JORDAN1A: 45; cell(Gauge(C,m),X-SpanStart(C,m)-'1,0) c= UBD C by A1,JORDAN1A:70; then UBD C meets BDD C by A3,A4,XBOOLE_1:68; hence contradiction by JORDAN2C:28; suppose Y-InitStart C = 1; then A5: cell(Gauge(C,m),X-SpanStart(C,m)-'1,1) c= BDD C by Def2; width Gauge(C,m) <> 0 by GOBOARD1:def 5; then A6: 0+1 <= width Gauge(C,m) by RLVECT_1:99; then A7: cell(Gauge(C,m),X-SpanStart(C,m)-'1,1) is non empty by A1,JORDAN1A: 45; A8: cell(Gauge(C,m),X-SpanStart(C,m)-'1,0) c= UBD C by A1,JORDAN1A:70; set i1 = X-SpanStart(C,m); A9: C is Bounded by JORDAN2C:73; A10: i1 < len Gauge(C,m) by JORDAN1H:58; i1-'1 <= i1 by JORDAN3:7; then A11: i1-'1 < len Gauge(C,m) by A10,AXIOMS:22; A12: 0 < width Gauge(C,m) by A6,NAT_1:38; 1 <= i1-'1 by JORDAN1H:59; then cell(Gauge(C,m),i1-'1,0) /\ cell(Gauge(C,m),i1-'1,0+1) = LSeg(Gauge(C,m)*(i1-'1,0+1),Gauge(C,m)*(i1-'1+1,0+1)) by A11,A12,GOBOARD5:27; then A13: cell(Gauge(C,m),i1-'1,0) meets cell(Gauge(C,m),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 A9,JORDAN2C:76; then A14: UBD C is_a_component_of C` by JORDAN2C:def 4; A15: cell(Gauge(C,m),X-SpanStart(C,m)-'1,1) is connected by A6,A11,JORDAN1A:46 ; BDD C c= C` by JORDAN2C:29; then cell(Gauge(C,m),X-SpanStart(C,m)-'1,1) c= C` by A5,XBOOLE_1:1; then cell(Gauge(C,m),X-SpanStart(C,m)-'1,1) c= UBD C by A8,A13,A14,A15, GOBOARD9:6; then UBD C meets BDD C by A5,A7,XBOOLE_1:68; hence contradiction by JORDAN2C:28; end; theorem Th3: Y-InitStart C + 1 < width Gauge(C,ApproxIndex C) proof set m = ApproxIndex C; A1: X-SpanStart(C,m)-'1 <= len Gauge(C,m) by JORDAN1H:59; assume Y-InitStart C + 1 >= width Gauge(C,m); then A2: Y-InitStart C + 1 > width Gauge(C,m) or Y-InitStart C + 1 = width Gauge(C,m) by AXIOMS:21; A3: Y-InitStart C < width Gauge(C,m) or Y-InitStart C = width Gauge(C,m) by Def2; per cases by A2,A3,NAT_1:38; suppose Y-InitStart C = width Gauge(C,m); hence contradiction by Def2; suppose Y-InitStart C + 1 = width Gauge(C,m); then Y-InitStart C = width Gauge(C,m)-'1 by BINARITH:39; then A4: cell(Gauge(C,m),X-SpanStart(C,m)-'1,width Gauge(C,m)-'1) c= BDD C by Def2; width Gauge(C,m)-'1 <= width Gauge(C,m) by JORDAN3:7; then A5: cell(Gauge(C,m),X-SpanStart(C,m)-'1,width Gauge(C,m)-'1) is non empty by A1,JORDAN1A:45; A6: cell(Gauge(C,m),X-SpanStart(C,m)-'1,width Gauge(C,m)) c= UBD C by A1, JORDAN1A:71; set i1 = X-SpanStart(C,m); A7: C is Bounded by JORDAN2C:73; A8: i1 < len Gauge(C,m) by JORDAN1H:58; width Gauge(C,m) <> 0 by GOBOARD1:def 5; then A9: 0+1 <= width Gauge(C,m) by RLVECT_1:99; i1-'1 <= i1 by JORDAN3:7; then A10: i1-'1 < len Gauge(C,m) by A8,AXIOMS:22; width Gauge(C,m)-1 < width Gauge(C,m) by INT_1:26; then A11: width Gauge(C,m)-'1 < width Gauge(C,m) by A9,SCMFSA_7:3; A12: width Gauge(C,m)-'1+1 = width Gauge(C,m) by A9,AMI_5:4; 1 <= i1-'1 by JORDAN1H:59; then cell(Gauge(C,m),i1-'1,width Gauge(C,m)) /\ cell(Gauge(C,m),i1-'1,width Gauge(C,m)-'1) = LSeg(Gauge(C,m)*(i1-'1,width Gauge(C,m)), Gauge(C,m)*(i1-'1+1,width Gauge(C,m))) by A10,A11,A12,GOBOARD5:27; then A13: cell(Gauge(C,m),i1-'1,width Gauge(C,m)) meets cell(Gauge(C,m),i1-'1,width Gauge(C,m)-'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 A7,JORDAN2C:76; then A14: UBD C is_a_component_of C` by JORDAN2C:def 4; A15: cell(Gauge(C,m),X-SpanStart(C,m)-'1,width Gauge(C,m)-'1) is connected by A10,A11,JORDAN1A:46; BDD C c= C` by JORDAN2C:29; then cell(Gauge(C,m),X-SpanStart(C,m)-'1,width Gauge(C,m)-'1) c= C` by A4,XBOOLE_1:1; then cell(Gauge(C,m),X-SpanStart(C,m)-'1,width Gauge(C,m)-'1) c= UBD C by A6,A13,A14,A15,GOBOARD9:6; then UBD C meets BDD C by A4,A5,XBOOLE_1:68; hence contradiction by JORDAN2C:28; end; definition let C,n such that A1: n is_sufficiently_large_for C; A2: n >= ApproxIndex C by A1,Def1; set i1 = X-SpanStart(C,n); func Y-SpanStart(C,n) -> Nat means :Def3: it <= width Gauge(C,n) & (for k st it <= k & k <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2 holds cell(Gauge(C,n),X-SpanStart(C,n)-'1,k) c= BDD C) & for j st j <= width Gauge(C,n) & for k st j <= k & k <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2 holds cell(Gauge(C,n),X-SpanStart(C,n)-'1,k) c= BDD C holds j >= it; existence proof set m = ApproxIndex C; defpred P[Nat] means $1 <= width Gauge(C,n) & for k st $1 <= k & k <= 2|^(n-'m)*(Y-InitStart C-'2)+2 holds cell(Gauge(C,n),i1-'1,k) c= BDD C; set X = { i: P[i]}; A3: 1 < Y-InitStart C by Th2; A4: Y-InitStart C+1 < width Gauge(C,m) by Th3; set j0 = 2|^(n-'m)*(Y-InitStart C-'2)+2; Y-InitStart C + 1 < 2|^m + (2+1) by A4,JORDAN1A:49; then Y-InitStart C + 1 < 2|^m + 2 + 1 by XCMPLX_1:1; then A5: Y-InitStart C < 2|^m + 2 by AXIOMS:24; 1+1 <= Y-InitStart C by A3,NAT_1:38; then A6: Y-InitStart C-'2 < 2|^m by A5,SPRECT_3:7; 2|^(n-'m) >= 1 by PREPOWER:19; then 2|^(n-'m) >= 0 by AXIOMS:22; then 2|^(n-'m)*(Y-InitStart C-'2) <= 2|^(n-'m)*(2|^m) by A6,AXIOMS:25; then 2|^(n-'m)*(Y-InitStart C-'2) <= 2|^((n-'m)+m) by NEWTON:13; then A7: 2|^(n-'m)*(Y-InitStart C-'2) <= 2|^n by A2,AMI_5:4; 2|^n <= 2|^n + 1 by NAT_1:29; then 2|^(n-'m)*(Y-InitStart C-'2) <= 2|^n + 1 by A7,AXIOMS:22; then j0 <= 2|^n + 1+2 by AXIOMS:24; then j0 <= 2|^n + (1+2) by XCMPLX_1:1; then j0 <= len Gauge(C,n) by JORDAN8:def 1; then A8: j0 <= width Gauge(C,n) by JORDAN8:def 1; now let j; assume j0 <= j & j <= 2|^(n-'m)*(Y-InitStart C-'2)+2; then A9: j = j0 by AXIOMS:21; A10: X-SpanStart(C,m) = 2|^(m-'1) + 2 by JORDAN1H:def 2; 1 <= 2|^(m-'1) by PREPOWER:19; then A11: 2+1 <= X-SpanStart(C,m) by A10,AXIOMS:24; A12: len Gauge(C,m) = 2|^m + (2 + 1) by JORDAN8:def 1 .= 2|^m + 2 + 1 by XCMPLX_1:1; m-'1 <= m by GOBOARD9:2; then 2|^(m-'1) <= 2|^m by PCOMPS_2:4; then 2|^(m-'1) + 2 <= 2|^m + 2 by AXIOMS:24; then A13: X-SpanStart(C,m) < len Gauge(C,m) by A10,A12,NAT_1:38; A14: m >= 1 by Th1; then A15: n >= 1 by A2,AXIOMS:22; (n-'m)+(m-'1) = (n-'m)+(m-1) by A14,SCMFSA_7:3 .= (n-'m)+ m-1 by XCMPLX_1:29 .= n-1 by A2,AMI_5:4 .= n-'1 by A15,SCMFSA_7:3; then 2|^(n-'1) = 2|^(n-'m)*(2|^(m-'1)) by NEWTON:13 .= 2|^(n-'m)*(X-SpanStart(C,m)-2) by A10,XCMPLX_1:26; then A16: i1 = 2|^(n-'m)*(X-SpanStart(C,m)-2)+2 by JORDAN1H:def 2; Y-InitStart C >= 1+1 by A3,NAT_1:38; then j = 2|^(n-'m)*(Y-InitStart C-2)+2 by A9,SCMFSA_7:3; then A17: cell(Gauge(C,n),i1-'1,j) c= cell(Gauge(C,m),X-SpanStart(C,m)-'1,Y-InitStart C) by A2,A3,A4,A11,A13,A16,JORDAN1A:69; cell(Gauge(C,m),X-SpanStart(C,m)-'1,Y-InitStart C) c= BDD C by Def2; hence cell(Gauge(C,n),i1-'1,j) c= BDD C by A17,XBOOLE_1:1; end; then A18: j0 in X by A8; X is Subset of NAT from SubsetD; then reconsider X as non empty Subset of NAT by A18; take min X; min X in X by CQC_SIM1:def 8; then ex j st j = min X & P[j]; hence P[min X]; let j; assume P[j]; then j in X; hence thesis by CQC_SIM1:def 8; end; uniqueness proof defpred definiens[Nat] means $1 <= width Gauge(C,n) & (for i st $1 <= i & i <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2 holds cell(Gauge(C,n),X-SpanStart(C,n)-'1,i) c= BDD C) & for j st j <= width Gauge(C,n) & for i st j <= i & i <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2 holds cell(Gauge(C,n),X-SpanStart(C,n)-'1,i) c= BDD C holds j >= $1; let it1,it2 be Nat; assume definiens[it1] & definiens[it2]; then it1 <= it2 & it2 <= it1; hence thesis by AXIOMS:21; end; end; theorem Th4: n is_sufficiently_large_for C implies X-SpanStart(C,n) = 2|^(n-'ApproxIndex C)*(X-SpanStart(C,ApproxIndex C)-2)+2 proof set i1 = X-SpanStart(C,n), m = ApproxIndex C; A1: X-SpanStart(C,m) = 2|^(m-'1) + 2 by JORDAN1H:def 2; assume n is_sufficiently_large_for C; then A2: n >=ApproxIndex C by Def1; A3: m >= 1 by Th1; then A4: n >= 1 by A2,AXIOMS:22; (n-'m)+(m-'1) = (n-'m)+(m-1) by A3,SCMFSA_7:3 .= (n-'m)+ m-1 by XCMPLX_1:29 .= n-1 by A2,AMI_5:4 .= n-'1 by A4,SCMFSA_7:3; then 2|^(n-'1) = 2|^(n-'m)*(2|^(m-'1)) by NEWTON:13 .= 2|^(n-'m)*(X-SpanStart(C,m)-2) by A1,XCMPLX_1:26; hence i1 = 2|^(n-'m)*(X-SpanStart(C,m)-2)+2 by JORDAN1H:def 2; end; theorem Th5: n is_sufficiently_large_for C implies Y-SpanStart(C,n) <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2 proof set m = ApproxIndex C; A1: X-SpanStart(C,m) > 2 by JORDAN1H:58; assume A2: n is_sufficiently_large_for C; then A3: n >=ApproxIndex C by Def1; set i1 = X-SpanStart(C,n); set j0 = 2|^(n-'m)*(Y-InitStart C-'2)+2; A4: Y-InitStart C+1 < width Gauge(C,m) by Th3; A5: 1 < Y-InitStart C by Th2; then 1+1 <= Y-InitStart C by NAT_1:38; then A6: Y-InitStart C-'2 = Y-InitStart C-2 by SCMFSA_7:3; Y-InitStart C < Y-InitStart C +1 by REAL_1:69; then Y-InitStart C < width Gauge(C,m) by A4,AXIOMS:22; then A7: j0 <= width Gauge(C,n) by A3,A5,A6,JORDAN1A:53; now let j; assume j0 <= j & j <= 2|^(n-'m)*(Y-InitStart C-'2)+2; then A8: j = j0 by AXIOMS:21; A9: cell(Gauge(C,m),X-SpanStart(C,m)-'1,Y-InitStart C) c= BDD C by Def2; A10: 2+1 <= X-SpanStart(C,m) by A1,NAT_1:38; A11: len Gauge(C,m) = 2|^m + 3 by JORDAN8:def 1; A12: X-SpanStart(C,m) = 2|^(m-'1) + 2 by JORDAN1H:def 2; m-'1 <= m by JORDAN3:7; then 2|^(m-'1) <= 2|^m by PCOMPS_2:4; then A13: X-SpanStart(C,m) < len Gauge(C,m) by A11,A12,REAL_1:67; i1 = 2|^(n-'m)*(X-SpanStart(C,m)-2)+2 by A2,Th4; then cell(Gauge(C,n),i1-'1,j) c= cell(Gauge(C,m),X-SpanStart(C,m)-'1,Y-InitStart C) by A3,A4,A5,A6,A8,A10,A13,JORDAN1A:69; hence cell(Gauge(C,n),i1-'1,j) c= BDD C by A9,XBOOLE_1:1; end; hence Y-SpanStart(C,n) <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2 by A2,A7,Def3; end; theorem Th6: n is_sufficiently_large_for C implies cell(Gauge(C,n),X-SpanStart(C,n)-'1,Y-SpanStart(C,n)) c= BDD C proof assume A1: n is_sufficiently_large_for C; then Y-SpanStart(C,n) <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2 by Th5; hence thesis by A1,Def3; end; theorem Th7: n is_sufficiently_large_for C implies 1 < Y-SpanStart(C,n) & Y-SpanStart(C,n) <= width Gauge(C,n) proof assume A1: n is_sufficiently_large_for C; thus 1 < Y-SpanStart(C,n) proof A2: X-SpanStart(C,n)-'1 <= len Gauge(C,n) by JORDAN1H:59; assume A3: Y-SpanStart(C,n) <= 1; per cases by A3,CQC_THE1:2; suppose Y-SpanStart(C,n) = 0; then A4: cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= BDD C by A1,Th6; 0 <= width Gauge(C,n) by NAT_1:18; then A5: cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) is non empty by A2,JORDAN1A :45; cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= UBD C by A2,JORDAN1A:70; then UBD C meets BDD C by A4,A5,XBOOLE_1:68; hence contradiction by JORDAN2C:28; suppose Y-SpanStart(C,n) = 1; then A6: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= BDD C by A1,Th6; width Gauge(C,n) <> 0 by GOBOARD1:def 5; then A7: 0+1 <= width Gauge(C,n) by RLVECT_1:99; then A8: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) is non empty by A2,JORDAN1A :45; A9: cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= UBD C by A2,JORDAN1A:70; set i1 = X-SpanStart(C,n); A10: C is Bounded by JORDAN2C:73; A11: i1 < len Gauge(C,n) by JORDAN1H:58; i1-'1 <= i1 by JORDAN3:7; then A12: i1-'1 < len Gauge(C,n) by A11,AXIOMS:22; A13: 0 < width Gauge(C,n) by A7,NAT_1:38; 1 <= i1-'1 by JORDAN1H:59; 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 A12,A13,GOBOARD5:27; then A14: 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 A10,JORDAN2C:76; then A15: UBD C is_a_component_of C` by JORDAN2C:def 4; A16: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) is connected by A7,A12,JORDAN1A:46 ; BDD C c= C` by JORDAN2C:29; then cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= C` by A6,XBOOLE_1:1; then cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= UBD C by A9,A14,A15,A16, GOBOARD9:6; then UBD C meets BDD C by A6,A8,XBOOLE_1:68; hence contradiction by JORDAN2C:28; end; thus Y-SpanStart(C,n) <= width Gauge(C,n) by A1,Def3; end; theorem n is_sufficiently_large_for C implies [X-SpanStart(C,n),Y-SpanStart(C,n)] in Indices Gauge(C,n) proof assume A1: n is_sufficiently_large_for C; 1+1 < X-SpanStart(C,n) by JORDAN1H:58; then A2: 1 < X-SpanStart(C,n) & X-SpanStart(C,n) < len Gauge(C,n) by JORDAN1H: 58,NAT_1:38; 1 < Y-SpanStart(C,n) & Y-SpanStart(C,n) <= width Gauge(C,n) by A1,Th7; hence thesis by A2,GOBOARD7:10; end; theorem n is_sufficiently_large_for C implies [X-SpanStart(C,n)-'1,Y-SpanStart(C,n)] in Indices Gauge(C,n) proof assume A1: n is_sufficiently_large_for C; A2: 1 <= X-SpanStart(C,n)-'1 & X-SpanStart(C,n)-'1 < len Gauge(C,n) by JORDAN1H :59; 1 < Y-SpanStart(C,n) & Y-SpanStart(C,n) <= width Gauge(C,n) by A1,Th7; hence thesis by A2,GOBOARD7:10; end; theorem n is_sufficiently_large_for C implies cell(Gauge(C,n),X-SpanStart(C,n)-'1,Y-SpanStart(C,n)-'1) meets C proof assume A1: n is_sufficiently_large_for C; set i1 = X-SpanStart(C,n); A2: Y-SpanStart(C,n) <= width Gauge(C,n) by A1,Def3; assume A3: cell(Gauge(C,n),X-SpanStart(C,n)-'1,Y-SpanStart(C,n)-'1) misses C; A4: Y-SpanStart(C,n)-'1 <= width Gauge(C,n) by A2,JORDAN3:7; A5: 1 < Y-SpanStart(C,n) by A1,Th7; for k st Y-SpanStart(C,n)-'1 <= k & k <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2 holds cell(Gauge(C,n),i1-'1,k) c= BDD C proof let k such that A6: Y-SpanStart(C,n)-'1 <= k and A7: k <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2; per cases by A6,AXIOMS:21; suppose A8: Y-SpanStart(C,n)-'1 = k; then A9: cell(Gauge(C,n),i1-'1,k) c= C` by A3,SUBSET_1:43; A10: i1 < len Gauge(C,n) by JORDAN1H:58; i1-'1 <= i1 by JORDAN3:7; then A11: i1-'1 < len Gauge(C,n) by A10,AXIOMS:22; A12: 1 < Y-SpanStart(C,n) & Y-SpanStart(C,n) <= width Gauge(C,n) by A1,Th7; then A13: k+1 = Y-SpanStart(C,n) by A8,AMI_5:4; k < k+1 by REAL_1:69; then A14: k < width Gauge(C,n) by A12,A13,AXIOMS:22; 1+1 < X-SpanStart(C,n) by JORDAN1H:58; then 1 <= i1-1 by REAL_1:84; then 1 <= i1-'1 by JORDAN3:1; then cell(Gauge(C,n),i1-'1,k) /\ cell(Gauge(C,n),i1-'1,k+1) = LSeg(Gauge(C,n)*(i1-'1,k+1),Gauge(C,n)*(i1-'1+1,k+1)) by A11,A14,GOBOARD5:27; then A15: cell(Gauge(C,n),i1-'1,k) meets cell(Gauge(C,n),i1-'1,k+1) by XBOOLE_0:def 7; cell(Gauge(C,n),i1-'1,k+1) c= BDD C by A1,A13,Th6; then A16: cell(Gauge(C,n),i1-'1,k) meets BDD C by A15,XBOOLE_1:63; set W = {B where B is Subset of TOP-REAL 2: B is_inside_component_of C}; A17: BDD C = union W by JORDAN2C:def 5; then consider e being set such that A18: e in W and A19: cell(Gauge(C,n),i1-'1,k) meets e by A16,ZFMISC_1:98; consider B being Subset of TOP-REAL 2 such that A20: e = B and A21: B is_inside_component_of C by A18; A22: cell(Gauge(C,n),i1-'1,k) is connected by A11,A14,JORDAN1A:46; B is_a_component_of C` by A21,JORDAN2C:def 3; then A23: cell(Gauge(C,n),i1-'1,k) c= B by A9,A19,A20,A22,GOBOARD9:6; B c= BDD C by A17,A18,A20,ZFMISC_1:92; hence cell(Gauge(C,n),i1-'1,k) c= BDD C by A23,XBOOLE_1:1; suppose Y-SpanStart(C,n)-'1 < k; then Y-SpanStart(C,n) < k+1 by SPRECT_3:8; then Y-SpanStart(C,n) <= k by NAT_1:38; hence cell(Gauge(C,n),i1-'1,k) c= BDD C by A1,A7,Def3; end; then A24: Y-SpanStart(C,n)-'1 >=Y-SpanStart(C,n) by A1,A4,Def3; Y-SpanStart(C,n)-1 < Y-SpanStart(C,n) by INT_1:26; hence contradiction by A5,A24,SCMFSA_7:3; end; theorem n is_sufficiently_large_for C implies cell(Gauge(C,n),X-SpanStart(C,n)-'1,Y-SpanStart(C,n)) misses C proof assume n is_sufficiently_large_for C; then A1: cell(Gauge(C,n),X-SpanStart(C,n)-'1,Y-SpanStart(C,n)) c= BDD C by Th6; BDD C misses C by JORDAN1A:15; hence thesis by A1,XBOOLE_1:63; end;

Back to top