Copyright (c) 2002 Association of Mizar Users
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;