Copyright (c) 2003 Association of Mizar Users
environ
vocabulary JORDAN19, JORDAN8, PSCOMP_1, BOOLE, JORDAN1A, JORDAN9, GOBOARD1,
GOBOARD5, JORDAN6, SPRECT_2, JORDAN3, FINSEQ_5, JORDAN2C, GROUP_2, NAT_1,
SPPOL_2, REALSET1, JORDAN1E, SQUARE_1, FINSEQ_4, TOPREAL2, CONNSP_1,
COMPTS_1, TOPREAL1, SPPOL_1, FINSEQ_1, TREES_1, EUCLID, RELAT_1, MCART_1,
MATRIX_1, GOBOARD9, PRE_TOPC, RELAT_2, SEQM_3, SUBSET_1, FUNCT_1,
ARYTM_1, FINSEQ_6, GOBOARD2, GROUP_1, GRAPH_2, METRIC_1, ARYTM, ORDINAL2,
ARYTM_3, INT_1, FUNCT_5, ABSVALUE, CONNSP_2, COMPLEX1, POWER, TOPS_1,
KURATO_2, PROB_1;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0,
REAL_1, INT_1, NAT_1, SQUARE_1, FUNCT_1, FUNCT_2, LIMFUNC1, ABSVALUE,
FINSEQ_1, FINSEQ_4, FINSEQ_5, MATRIX_1, FINSEQ_6, POWER, TOPRNS_1,
METRIC_1, CONNSP_2, GRAPH_2, STRUCT_0, REALSET1, PRE_TOPC, TOPS_1,
TOPREAL2, CARD_4, BINARITH, PROB_1, CONNSP_1, COMPTS_1, EUCLID, PSCOMP_1,
SPRECT_2, SPPOL_2, KURATO_2, GOBOARD1, GOBRD14, TOPREAL1, GOBOARD2,
GOBOARD5, GOBOARD9, GOBRD13, SPPOL_1, JORDAN3, JORDAN6, JORDAN8, JORDAN9,
JORDAN2C, JORDAN1A, JORDAN1E;
constructors JORDAN8, REALSET1, GOBOARD9, JORDAN6, REAL_1, CARD_4, PSCOMP_1,
BINARITH, JORDAN2C, CONNSP_1, JORDAN9, JORDAN1A, FINSEQ_4, JORDAN1,
JORDAN3, TOPREAL2, JORDAN5C, GRAPH_2, SPRECT_1, GOBOARD2, TOPS_1,
FINSOP_1, JORDAN1E, WSIERP_1, JORDAN1H, ABSVALUE, CONNSP_2, LIMFUNC1,
TOPRNS_1, SERIES_1, GOBRD14, DOMAIN_1, KURATO_2, INT_1;
clusters SPRECT_1, TOPREAL6, JORDAN8, REVROT_1, INT_1, RELSET_1, REAL_1,
SUBSET_1, SPRECT_3, GOBOARD2, FINSEQ_5, SPPOL_2, JORDAN1A, JORDAN1B,
JORDAN1G, GOBRD11, FUNCT_7, XBOOLE_0, EUCLID, PSCOMP_1, JORDAN1J,
METRIC_1, XREAL_0, ORDINAL2;
requirements NUMERALS, ARITHM, BOOLE, SUBSET, REAL;
definitions TARSKI, XBOOLE_0;
theorems NAT_1, FINSEQ_1, GOBOARD1, FINSEQ_4, EUCLID, FINSEQ_3, AXIOMS,
REAL_1, REAL_2, HEINE, TOPREAL4, SPPOL_2, TARSKI, JORDAN3, SQUARE_1,
PSCOMP_1, FINSEQ_5, FINSEQ_6, GOBOARD7, TOPREAL1, BINARITH, AMI_5,
JORDAN5B, GOBOARD5, SPRECT_2, SPPOL_1, ABSVALUE, GOBOARD9, FINSEQ_2,
UNIFORM1, SUBSET_1, GOBRD11, JORDAN4, GOBOARD2, SPRECT_3, GOBOARD6,
TOPREAL3, JORDAN8, PARTFUN2, SCMFSA_7, SPRECT_1, XBOOLE_0, XBOOLE_1,
ZFMISC_1, GOBRD14, JORDAN2C, TOPREAL5, CONNSP_2, PRE_TOPC, JORDAN6,
JORDAN9, JORDAN1H, JORDAN1A, JORDAN1C, JORDAN1E, JORDAN10, JGRAPH_1,
REVROT_1, COMPTS_1, ENUMSET1, JORDAN1B, PCOMPS_2, JORDAN1F, JORDAN1G,
JORDAN1I, JORDAN1J, GOBOARD3, TOPREAL8, AMISTD_1, GRAPH_2, SPRECT_5,
JORDAN1D, YELLOW_6, METRIC_1, POWER, PRE_FF, NAT_2, JORDAN15, PCOMPS_1,
SEQ_2, JGRAPH_3, TOPRNS_1, BOOLMARK, JORDAN5D, XCMPLX_1, XREAL_0,
KURATO_2;
schemes FUNCT_2, COMPLSP1;
begin
reserve n for Nat;
definition
let C be Simple_closed_curve;
func Upper_Appr C -> SetSequence of the carrier of TOP-REAL 2 means :Def1:
for i be Nat holds it.i = Upper_Arc L~Cage (C,i);
existence
proof
deffunc O(Nat) = Upper_Arc L~Cage (C,$1);
thus ex S be SetSequence of the carrier of TOP-REAL 2 st
for i being Nat holds S.i = O(i) from LambdaD;
end;
uniqueness
proof
deffunc O(Nat) = Upper_Arc L~Cage (C,$1);
thus for S1,S2 be SetSequence of the carrier of TOP-REAL 2 st
(for i being Nat holds S1.i = O(i)) &
(for i being Nat holds S2.i = O(i)) holds S1 = S2 from FuncDefUniq;
end;
func Lower_Appr C -> SetSequence of the carrier of TOP-REAL 2 means :Def2:
for i being Nat holds it.i = Lower_Arc L~Cage (C,i);
existence
proof
deffunc O(Nat) = Lower_Arc L~Cage (C,$1);
thus ex S be SetSequence of the carrier of TOP-REAL 2 st
for i being Nat holds S.i = O(i) from LambdaD;
end;
uniqueness
proof
deffunc O(Nat) = Lower_Arc L~Cage (C,$1);
thus for S1,S2 be SetSequence of the carrier of TOP-REAL 2 st
(for i being Nat holds S1.i = O(i)) &
(for i being Nat holds S2.i = O(i)) holds S1 = S2 from FuncDefUniq;
end;
end;
definition
let C be Simple_closed_curve;
func North_Arc C -> Subset of TOP-REAL 2 equals :Def3:
Lim_inf Upper_Appr C;
coherence;
func South_Arc C -> Subset of TOP-REAL 2 equals :Def4:
Lim_inf Lower_Appr C;
coherence;
end;
Lm1:
now
let G be Go-board;
let j be Nat;
assume A1: 1 <= j & j <= width G;
0 <= len G div 2 by NAT_1:18;
then 0 + 1 <= len G div 2 + 1 by AXIOMS:24;
then A2: 0 + 1 <= Center G by JORDAN1A:def 1;
Center G <= len G by JORDAN1B:14;
hence [Center G,j] in Indices G by A1,A2,GOBOARD7:10;
end;
Lm2:
now
let D be non empty Subset of TOP-REAL 2;
let n,i be Nat;
set a = N-bound D, s = S-bound D, w = W-bound D, e = E-bound D;
set G = Gauge(D,n);
assume [i,width G] in Indices G;
hence G*(i,width G)`2
= |[w+(e-w)/(2|^n)*(i - 2), s+(a-s)/(2|^n)*(width G - 2)]|`2
by JORDAN8:def 1
.= s+(a-s)/(2|^n)*(width G - 2) by EUCLID:56;
end;
theorem Th1:
for n,m be Nat holds n <= m & n <> 0 implies (n+1)/n >= (m+1)/m
proof
let n,m be Nat;
assume that
A1: n <= m and
A2: n <> 0;
A3: n > 0 by A2,NAT_1:19;
then A4: m > 0 by A1;
A5: 1/n >= 1/m by A1,A3,REAL_2:152;
A6: (n+1)/n = n/n + 1/n by XCMPLX_1:63
.= 1 + 1/n by A3,XCMPLX_1:60;
(m+1)/m = m/m + 1/m by XCMPLX_1:63
.= 1 + 1/m by A4,XCMPLX_1:60;
hence (n+1)/n >= (m+1)/m by A5,A6,REAL_1:55;
end;
theorem Th2:
for E be compact non vertical non horizontal Subset of TOP-REAL 2
for m,j be Nat st 1 <= m & m <= n & 1 <= j & j <= width Gauge(E,n) holds
LSeg(Gauge(E,n)*(Center Gauge(E,n),width Gauge(E,n)),
Gauge(E,n)*(Center Gauge(E,n),j)) c=
LSeg(Gauge(E,m)*(Center Gauge(E,m),width Gauge(E,m)),
Gauge(E,n)*(Center Gauge(E,n),j))
proof
let E be compact non vertical non horizontal Subset of TOP-REAL 2;
let m,j be Nat;
set a = N-bound E, s = S-bound E, w = W-bound E, e = E-bound E,
G = Gauge(E,n), M = Gauge(E,m), sn = Center G, sm = Center M;
assume that
A1: 1 <= m and
A2: m <= n and
A3: 1 <= j and
A4: j <= width G;
A5: width M = len M by JORDAN8:def 1
.= 2|^m+3 by JORDAN8:def 1;
A6: width G = len G by JORDAN8:def 1
.= 2|^n+3 by JORDAN8:def 1;
A7: 2|^m <= 2|^n by A2,PCOMPS_2:4;
now
let t be Nat;
assume that
A8: width G >= t and
A9: t >= j;
A10: len M = width M by JORDAN8:def 1;
A11: len G = width G by JORDAN8:def 1;
0+1 <= m by A1;
then A12: m > 0 by NAT_1:38;
then A13: n > 0 by A2;
s < a by SPRECT_1:34;
then A14: 0 < a - s by SQUARE_1:11;
A15: t >= 1 by A3,A9,AXIOMS:22;
A16: 0 < 2|^m by HEINE:5;
A17: 0 < 2|^n by HEINE:5;
A18: 1 <= len M by GOBRD11:34;
then A19: M*(sm,width M)`1 = G*(sn,t)`1 & G*(sn,t)`1 = G*(sn,j)`1
by A3,A4,A8,A10,A11,A12,A13,A15,JORDAN1A:
57;
[sn,t] in Indices G by A8,A15,Lm1;
then A20: G*(sn,t)`2 = |[w+(e-w)/(2|^n)*(sn - 2),s+(a-s)/(2|^n)*(t-2)]|`2
by JORDAN8:def 1
.= s+(a-s)/(2|^n)*(t-2) by EUCLID:56;
[sm,width M] in Indices M by A10,A18,Lm1;
then A21: M*(sm,width M)`2 = s+(a-s)/(2|^m)*(width M-2) by Lm2;
A22: (2|^m+1)/(2|^m) >= (2|^n+1)/(2|^n) by A7,A16,Th1;
A23: width M-2 = 2|^m+(3-2) by A5,XCMPLX_1:29;
t-2 <= 2|^n+3-2 by A6,A8,REAL_1:49;
then t-2 <= 2|^n+(3-2) by XCMPLX_1:29;
then (t-2)/(2|^n) <= (2|^n+1)/(2|^n) by A17,REAL_1:73;
then (t-2)/(2|^n) <= (width M-2)/(2|^m) by A22,A23,AXIOMS:22;
then (a-s)*((t-2)/(2|^n)) <= (a-s)*((width M-2)/(2|^m)) by A14,AXIOMS:25;
then (a-s)/(2|^n)*(t-2) <= (a-s)*((width M-2)/(2|^m)) by XCMPLX_1:76;
then (a-s)/(2|^m)*(width M-2) >= (a-s)/(2|^n)*(t-2) by XCMPLX_1:76;
then s+(a-s)/(2|^m)*(width M-2) >= s+(a-s)/(2|^n)*(t-2) by AXIOMS:24;
then A24: M*(sm,width M)`2 >= G*(sn,t)`2 by A20,A21;
1 <= sn & sn <= len G by JORDAN1B:12,14;
then G*(sn,t)`2 >= G*(sn,j)`2 by A3,A8,A9,SPRECT_3:24;
hence G*(sn,t) in LSeg(M*(sm,width M),G*(sn,j)) by A19,A24,GOBOARD7:8;
end;
then G*(sn,width G) in LSeg(M*(sm,width M),G*(sn,j)) &
G*(sn,j) in LSeg(M*(sm,width M),G*(sn,j)) by A4;
hence thesis by TOPREAL1:12;
end;
theorem Th3:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j be Nat st 1 <= i & i <= len Gauge(C,n) &
1 <= j & j <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Cage(C,n) holds
LSeg(Gauge(C,n)*(i,width Gauge(C,n)),Gauge(C,n)*(i,j)) meets
L~Upper_Seq(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i,j be Nat;
set Gij = Gauge(C,n)*(i,j);
assume that
A1: 1 <= i & i <= len Gauge(C,n) and
A2: 1 <= j & j <= width Gauge(C,n) and
A3: Gij in L~Cage(C,n);
set NE = SW-corner L~Cage(C,n);
set v1 = L_Cut(Lower_Seq(C,n),Gij);
set wG = width Gauge(C,n);
set lG = len Gauge(C,n);
set Gv1 = <*Gauge(C,n)*(i,wG)*>^v1;
set v = Gv1^<*NE*>;
set h = mid(Upper_Seq(C,n),2,len Upper_Seq(C,n));
A4: L~Cage(C,n) = L~Lower_Seq(C,n) \/ L~Upper_Seq(C,n) by JORDAN1E:17;
len Upper_Seq(C,n) >= 3 & len Lower_Seq(C,n) >= 3 by JORDAN1E:19;
then A5: len Upper_Seq(C,n) >= 2 & len Upper_Seq(C,n) >= 1 &
len Lower_Seq(C,n) >= 2 & len Lower_Seq(C,n) >= 1 by AXIOMS:22;
A6: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
then width Gauge(C,n) >= 4 by JORDAN8:13;
then A7: 1 <= width Gauge(C,n) by AXIOMS:22;
A8: Gauge(C,n)*(i,wG)`2 = N-bound L~Cage(C,n) by A1,A6,JORDAN1A:91;
set Ema = E-max L~Cage(C,n);
now per cases by A1,A3,A4,REAL_1:def 5,XBOOLE_0:def 2;
suppose A9: Gij in L~Lower_Seq(C,n) & i = lG;
set G11 = Gauge(C,n)*(lG,wG);
A10: G11`1 = E-bound L~Cage(C,n) by A1,A6,A9,JORDAN1A:92;
A11: Ema`1 = E-bound L~Cage(C,n) by PSCOMP_1:104;
A12: N-bound L~Cage(C,n) = G11`2 by A1,A6,A9,JORDAN1A:91;
Ema in L~Cage(C,n) by SPRECT_1:16;
then A13: G11`2 >= Ema`2 by A12,PSCOMP_1:71;
A14: Gij`1 = E-bound L~Cage(C,n) by A2,A6,A9,JORDAN1A:92;
then Gij in E-most L~Cage(C,n) by A3,SPRECT_2:17;
then Ema`2 >= Gij`2 by PSCOMP_1:108;
then A15: Ema in LSeg(Gauge(C,n)*(lG,wG),Gauge(C,n)*(lG,j))
by A9,A10,A11,A13,A14,GOBOARD7:8;
A16: rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by A5,SPPOL_2:18;
Upper_Seq(C,n)/.(len Upper_Seq(C,n)) = Ema by JORDAN1F:7;
then Ema in rng Upper_Seq(C,n) by REVROT_1:3;
hence LSeg(Gauge(C,n)*(i,wG),Gij) meets L~Upper_Seq(C,n)
by A9,A15,A16,XBOOLE_0:3;
suppose A17: Gij in L~Lower_Seq(C,n) &
Gij <> Lower_Seq(C,n).len Lower_Seq(C,n)
& W-min L~Cage(C,n) <> NE & i < lG;
then A18: v1 is non empty by JORDAN1E:7;
then len v1 <> 0 by FINSEQ_1:25;
then len v1 > 0 by NAT_1:19;
then A19: 0+1 <= len v1 by NAT_1:38;
then A20: 1 in dom v1 by FINSEQ_3:27;
A21: len v1 in dom v1 & len Lower_Seq(C,n) in dom Lower_Seq(C,n)
by A5,A19,FINSEQ_3:27;
A22: v1/.(len v1) = v1.(len v1) by A21,FINSEQ_4:def 4
.= Lower_Seq(C,n).len Lower_Seq(C,n) by A17,JORDAN1B:5
.= Lower_Seq(C,n)/.len Lower_Seq(C,n) by A21,FINSEQ_4:def 4
.= W-min L~Cage(C,n) by JORDAN1F:8;
then A23: Gv1/.len Gv1 = W-min L~Cage(C,n) by A18,SPRECT_3:11;
A24: v1/.1 = v1.1 by A20,FINSEQ_4:def 4
.= Gij by A17,JORDAN3:58;
then A25: (v1^<*NE*>)/.1 = Gij by A19,BOOLMARK:8;
A26: 1+len v1 >= 1+1 by A19,REAL_1:55;
len v = len Gv1 + 1 by FINSEQ_2:19
.= 1 + len v1 + 1 by FINSEQ_5:8;
then 2 < len v by A26,NAT_1:38;
then A27: 2 < len Rev v by FINSEQ_5:def 3;
S-bound L~Cage(C,n) < N-bound L~Cage(C,n) by SPRECT_1:34;
then NE <> Gauge(C,n)*(i,wG) by A8,PSCOMP_1:73;
then not NE in {Gauge(C,n)*(i,wG)} by TARSKI:def 1;
then A28: not NE in rng <*Gauge(C,n)*(i,wG)*> by FINSEQ_1:56;
len Cage(C,n) > 4 by GOBOARD7:36;
then len Cage(C,n) >= 2 by AXIOMS:22;
then A29: rng Cage(C,n) c= L~Cage(C,n) by SPPOL_2:18;
A30: not NE in rng Cage(C,n)
proof
assume A31: NE in rng Cage(C,n);
A32: NE`1 = W-bound L~Cage(C,n) & NE`2 = S-bound L~Cage(C,n)
by PSCOMP_1:72,73;
then NE`2 <= N-bound L~Cage(C,n) by SPRECT_1:24;
then NE in { p where p is Point of TOP-REAL 2 :
p`1 = W-bound L~Cage(C,n) & p`2 <= N-bound L~Cage(C,n) &
p`2 >= S-bound L~Cage(C,n) } by A32;
then NE in LSeg(SW-corner L~Cage(C,n), NW-corner L~Cage(C,n))
by SPRECT_1:28;
then NE in LSeg(SW-corner L~Cage(C,n), NW-corner L~Cage(C,n)) /\
L~Cage(C,n) by A29,A31,XBOOLE_0:def 3;
then NE in W-most L~Cage(C,n) by PSCOMP_1:def 38;
then A33: NE`2 >= (W-min L~Cage(C,n))`2 by PSCOMP_1:88;
(W-min L~Cage(C,n))`2 >= NE`2 by PSCOMP_1:87;
then A34: (W-min L~Cage(C,n))`2 = NE`2 by A33,AXIOMS:21;
(W-min L~Cage(C,n))`1 = NE`1 by PSCOMP_1:85;
hence contradiction by A17,A34,TOPREAL3:11;
end;
now per cases;
suppose Gij <> Lower_Seq(C,n).(Index(Gij,Lower_Seq(C,n))+1);
then v1 = <*Gij*>^mid(Lower_Seq(C,n),
Index(Gij,Lower_Seq(C,n))+1,len Lower_Seq(C,n)) by JORDAN3:def 4;
then rng v1 = rng <*Gij*> \/ rng mid(Lower_Seq(C,n),
Index(Gij,Lower_Seq(C,n))+1,len Lower_Seq(C,n)) by FINSEQ_1:44;
then A35: rng v1 = {Gij} \/ rng mid(Lower_Seq(C,n),
Index(Gij,Lower_Seq(C,n))+1,len Lower_Seq(C,n)) by FINSEQ_1:55;
not NE in L~Cage(C,n)
proof
assume NE in L~Cage(C,n);
then consider i be Nat such that
A36: 1 <= i and
A37: i+1 <= len Cage(C,n) and
A38: NE in LSeg(Cage(C,n)/.i,Cage(C,n)/.(i+1)) by SPPOL_2:14;
per cases by A36,A37,TOPREAL1:def 7;
suppose A39: (Cage(C,n)/.i)`1 = (Cage(C,n)/.(i+1))`1;
then A40: NE`1 = (Cage(C,n)/.i)`1 by A38,GOBOARD7:5;
A41: NE`2 = S-bound L~Cage(C,n) by PSCOMP_1:73;
A42: i < len Cage(C,n) by A37,NAT_1:38;
then A43: (Cage(C,n)/.i)`2 >= NE`2 by A36,A41,JORDAN5D:13;
A44: 1 <= i+1 by NAT_1:29;
then A45: (Cage(C,n)/.(i+1))`2 >= NE`2 by A37,A41,JORDAN5D:13;
A46: i in dom Cage(C,n) & i+1 in dom Cage(C,n)
by A36,A37,A42,A44,FINSEQ_3:27;
(Cage(C,n)/.i)`2 <= (Cage(C,n)/.(i+1))`2 or
(Cage(C,n)/.i)`2 >= (Cage(C,n)/.(i+1))`2;
then NE`2 >= (Cage(C,n)/.(i+1))`2 or NE`2 >= (Cage(C,n)/.i)`2
by A38,TOPREAL1:10;
then NE`2 = (Cage(C,n)/.(i+1))`2 or NE`2 = (Cage(C,n)/.i)`2
by A43,A45,AXIOMS:21;
then NE = (Cage(C,n)/.(i+1)) or NE = (Cage(C,n)/.i)
by A39,A40,TOPREAL3:11;
hence contradiction by A30,A46,PARTFUN2:4;
suppose A47: (Cage(C,n)/.i)`2 = (Cage(C,n)/.(i+1))`2;
then A48: NE`2 = (Cage(C,n)/.i)`2 by A38,GOBOARD7:6;
A49: NE`1 = W-bound L~Cage(C,n) by PSCOMP_1:72;
A50: i < len Cage(C,n) by A37,NAT_1:38;
then A51: (Cage(C,n)/.i)`1 >= NE`1 by A36,A49,JORDAN5D:14;
A52: 1 <= i+1 by NAT_1:29;
then A53: (Cage(C,n)/.(i+1))`1 >= NE`1 by A37,A49,JORDAN5D:14;
A54: i in dom Cage(C,n) & i+1 in dom Cage(C,n)
by A36,A37,A50,A52,FINSEQ_3:27;
(Cage(C,n)/.i)`1 <= (Cage(C,n)/.(i+1))`1 or
(Cage(C,n)/.i)`1 >= (Cage(C,n)/.(i+1))`1;
then NE`1 >= (Cage(C,n)/.(i+1))`1 or NE`1 >= (Cage(C,n)/.i)`1
by A38,TOPREAL1:9;
then NE`1 = (Cage(C,n)/.(i+1))`1 or NE`1 = (Cage(C,n)/.i)`1
by A51,A53,AXIOMS:21;
then NE = (Cage(C,n)/.(i+1)) or NE = (Cage(C,n)/.i)
by A47,A48,TOPREAL3:11;
hence contradiction by A30,A54,PARTFUN2:4;
end;
then A55: not NE in {Gij} by A3,TARSKI:def 1;
A56: rng mid(Lower_Seq(C,n),Index(Gij,Lower_Seq(C,n))+1,
len Lower_Seq(C,n)) c= rng Lower_Seq(C,n) by JORDAN3:28;
rng Lower_Seq(C,n) c= rng Cage(C,n) by JORDAN1G:47;
then rng mid(Lower_Seq(C,n),Index(Gij,Lower_Seq(C,n))+1,
len Lower_Seq(C,n)) c= rng Cage(C,n) by A56,XBOOLE_1:1;
then not NE in rng mid(Lower_Seq(C,n),Index(Gij,Lower_Seq(C,n))+1,
len Lower_Seq(C,n)) by A30;
hence not NE in rng v1 by A35,A55,XBOOLE_0:def 2;
suppose Gij = Lower_Seq(C,n).(Index(Gij,Lower_Seq(C,n))+1);
then v1 = mid(Lower_Seq(C,n),
Index(Gij,Lower_Seq(C,n))+1,len Lower_Seq(C,n)) by JORDAN3:def 4;
then A57: rng v1 c= rng Lower_Seq(C,n) by JORDAN3:28;
rng Lower_Seq(C,n) c= rng Cage(C,n) by JORDAN1G:47;
then rng v1 c= rng Cage(C,n) by A57,XBOOLE_1:1;
hence not NE in rng v1 by A30;
end;
then not NE in rng <*Gauge(C,n)*(i,wG)*> \/ rng v1 by A28,XBOOLE_0:def 2;
then not NE in rng Gv1 by FINSEQ_1:44;
then rng Gv1 misses {NE} by ZFMISC_1:56;
then A58: rng Gv1 misses rng <*NE*> by FINSEQ_1:55;
A59: not Gauge(C,n)*(i,wG) in L~Lower_Seq(C,n) by A1,A17,JORDAN1G:53;
rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by A5,SPPOL_2:18;
then A60: not Gauge(C,n)*(i,wG) in rng Lower_Seq(C,n)
by A1,A17,JORDAN1G:53;
not Gauge(C,n)*(i,wG) in {Gij} by A17,A59,TARSKI:def 1;
then A61: not Gauge(C,n)*(i,wG) in rng <*Gij*> by FINSEQ_1:55;
set ci = mid(Lower_Seq(C,n),Index(Gij,Lower_Seq(C,n))+1,
len Lower_Seq(C,n));
now per cases;
suppose A62: Gij <> Lower_Seq(C,n).(Index(Gij,Lower_Seq(C,n))+1);
rng ci c= rng Lower_Seq(C,n) by JORDAN3:28;
then not Gauge(C,n)*(i,wG) in rng ci by A60;
then not Gauge(C,n)*(i,wG) in rng <*Gij*> \/ rng ci
by A61,XBOOLE_0:def 2;
then not Gauge(C,n)*(i,wG) in rng(<*Gij*>^ci) by FINSEQ_1:44;
hence not Gauge(C,n)*(i,wG) in rng v1 by A62,JORDAN3:def 4;
suppose Gij = Lower_Seq(C,n).(Index(Gij,Lower_Seq(C,n))+1);
then v1 = ci by JORDAN3:def 4;
then rng v1 c= rng Lower_Seq(C,n) by JORDAN3:28;
hence not Gauge(C,n)*(i,wG) in rng v1 by A60;
end;
then {Gauge(C,n)*(i,wG)} misses rng v1 by ZFMISC_1:56;
then A63: rng <*Gauge(C,n)*(i,wG)*> misses rng v1 by FINSEQ_1:55;
A64: <*Gauge(C,n)*(i,wG)*> is one-to-one by FINSEQ_3:102;
A65: v1 is_S-Seq by A17,JORDAN3:69;
then v1 is one-to-one by TOPREAL1:def 10;
then A66: Gv1 is one-to-one by A63,A64,FINSEQ_3:98;
<*NE*> is one-to-one by FINSEQ_3:102;
then A67: v is one-to-one by A58,A66,FINSEQ_3:98;
for v be one-to-one FinSequence holds Rev v is one-to-one;
then A68: Rev v is one-to-one by A67;
A69: <*Gauge(C,n)*(i,wG)*> is special by SPPOL_2:39;
A70: v1 is special by A65,TOPREAL1:def 10;
(<*Gauge(C,n)*(i,wG)*>/.len <*Gauge(C,n)*(i,wG)*>)`1 =
(<*Gauge(C,n)*(i,wG)*>/.1)`1 by FINSEQ_1:56
.= Gauge(C,n)*(i,wG)`1 by FINSEQ_4:25
.= Gauge(C,n)*(i,1)`1 by A1,A7,GOBOARD5:3
.= (v1/.1)`1 by A1,A2,A24,GOBOARD5:3;
then A71: Gv1 is special by A69,A70,GOBOARD2:13;
A72: <*NE*> is special by SPPOL_2:39;
(Gv1/.len Gv1)`1 = NE`1 by A23,PSCOMP_1:85
.= (<*NE*>/.1)`1 by FINSEQ_4:25;
then v is special by A71,A72,GOBOARD2:13;
then A73: Rev v is special by SPPOL_2:42;
A74: len Upper_Seq(C,n) >= 2+1 by JORDAN1E:19;
then A75: len Upper_Seq(C,n) > 2 by NAT_1:38;
len Upper_Seq(C,n) > 1 by A74,AXIOMS:22;
then h is S-Sequence_in_R2 by A75,JORDAN3:39;
then A76: 2 <= len h & h is one-to-one & h is special
by TOPREAL1:def 10;
A77: Upper_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:21;
3 <= len Upper_Seq(C,n) by JORDAN1E:19;
then 2 <= len Upper_Seq(C,n) by AXIOMS:22;
then A78: 2 in dom Upper_Seq(C,n) by FINSEQ_3:27;
A79: len Upper_Seq(C,n) in dom Upper_Seq(C,n) by SCMFSA_7:12;
then A80: h is_in_the_area_of Cage(C,n) by A77,A78,SPRECT_2:26;
Upper_Seq(C,n)/.(len Upper_Seq(C,n)) = E-max L~Cage(C,n) by JORDAN1F:7;
then (Upper_Seq(C,n)/.len Upper_Seq(C,n))`1 = E-bound L~Cage(C,n)
by PSCOMP_1:104;
then A81: (h/.len h)`1 = E-bound L~Cage(C,n) by A78,A79,SPRECT_2:13;
(Upper_Seq(C,n)/.(1+1))`1 = W-bound L~Cage(C,n) by JORDAN1G:39;
then (h/.1)`1 = W-bound L~Cage(C,n) by A78,A79,SPRECT_2:12;
then A82: h is_a_h.c._for Cage(C,n) by A80,A81,SPRECT_2:def 2;
now let m be Nat;
assume A83: m in dom <*Gauge(C,n)*(i,wG)*>;
then m in Seg 1 by FINSEQ_1:55;
then m = 1 by FINSEQ_1:4,TARSKI:def 1;
then <*Gauge(C,n)*(i,wG)*>.m = Gauge(C,n)*(i,wG) by FINSEQ_1:57;
then A84: <*Gauge(C,n)*(i,wG)*>/.m = Gauge(C,n)*(i,wG)
by A83,FINSEQ_4:def 4;
Gauge(C,n)*(1,wG)`1 <= Gauge(C,n)*(i,wG)`1 by A1,A7,SPRECT_3:25;
hence W-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,wG)*>/.m)`1
by A6,A7,A84,JORDAN1A:94;
(Gauge(C,n)*(i,wG))`1 <= Gauge(C,n)*(len Gauge(C,n),wG)`1
by A1,A7,SPRECT_3:25;
hence (<*Gauge(C,n)*(i,wG)*>/.m)`1 <= E-bound L~Cage(C,n)
by A6,A7,A84,JORDAN1A:92;
(<*Gauge(C,n)*(i,wG)*>/.m)`2 = N-bound L~Cage(C,n)
by A1,A6,A84,JORDAN1A:91;
hence S-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,wG)*>/.m)`2
by SPRECT_1:24;
thus (<*Gauge(C,n)*(i,wG)*>/.m)`2 <= N-bound L~Cage(C,n)
by A1,A6,A84,JORDAN1A:91;
end;
then A85: <*Gauge(C,n)*(i,wG)*> is_in_the_area_of Cage(C,n)
by SPRECT_2:def 1;
A86: Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:22;
<*Gij*> is_in_the_area_of Cage(C,n) by A17,A86,SPRECT_3:63;
then v1 is_in_the_area_of Cage(C,n) by A17,A86,SPRECT_3:73;
then A87: Gv1 is_in_the_area_of Cage(C,n) by A85,SPRECT_2:28;
<*NE*> is_in_the_area_of Cage(C,n) by SPRECT_2:32;
then v is_in_the_area_of Cage(C,n) by A87,SPRECT_2:28;
then A88: Rev v is_in_the_area_of Cage(C,n) by SPRECT_3:68;
v = <*Gauge(C,n)*(i,wG)*>^(v1^<*NE*>) by FINSEQ_1:45;
then v/.1 = Gauge(C,n)*(i,wG) by FINSEQ_5:16;
then (v/.1)`2 = N-bound L~Cage(C,n) by A1,A6,JORDAN1A:91;
then (Rev v/.(len v))`2 = N-bound L~Cage(C,n) by FINSEQ_5:68;
then A89: (Rev v/.(len Rev v))`2 = N-bound L~Cage(C,n)
by FINSEQ_5:def 3;
len v = len Gv1 + 1 by FINSEQ_2:19;
then v/.(len v) = NE by TOPREAL4:1;
then (v/.len v)`2 = S-bound L~Cage(C,n) by PSCOMP_1:73;
then (Rev v/.1)`2 = S-bound L~Cage(C,n) by FINSEQ_5:68;
then Rev v is_a_v.c._for Cage(C,n) by A88,A89,SPRECT_2:def 3;
then L~h meets L~Rev v by A27,A68,A73,A76,A82,SPRECT_2:33;
then L~h meets L~v by SPPOL_2:22;
then consider x be set such that
A90: x in L~h and
A91: x in L~v by XBOOLE_0:3;
A92: L~h c= L~Upper_Seq(C,n) by A5,JORDAN4:47;
A93: L~v1 c= L~Lower_Seq(C,n) by A17,JORDAN3:77;
L~v = L~(<*Gauge(C,n)*(i,wG)*>^(v1^<*NE*>)) by FINSEQ_1:45
.= LSeg(Gauge(C,n)*(i,wG),(v1^<*NE*>)/.1) \/ L~(v1^<*NE*>)
by SPPOL_2:20
.= LSeg(Gauge(C,n)*(i,wG),(v1^<*NE*>)/.1) \/
(L~v1 \/ LSeg(v1/.(len v1),NE)) by A18,SPPOL_2:19;
then A94: x in LSeg(Gauge(C,n)*(i,wG),(v1^<*NE*>)/.1) or
x in L~v1 \/ LSeg(v1/.(len v1),NE) by A91,XBOOLE_0:def 2;
Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by JORDAN1F:5;
then A95: not W-min L~Cage(C,n) in L~h by A75,JORDAN5B:16;
now per cases by A94,XBOOLE_0:def 2;
suppose x in LSeg(Gauge(C,n)*(i,wG),(v1^<*NE*>)/.1);
then x in L~<*Gauge(C,n)*(i,wG),Gij*> by A25,SPPOL_2:21;
hence L~Upper_Seq(C,n) meets L~<*Gauge(C,n)*(i,wG),Gij*>
by A90,A92,XBOOLE_0:3;
suppose A96: x in L~v1;
then x in L~Lower_Seq(C,n) /\ L~Upper_Seq(C,n)
by A90,A92,A93,XBOOLE_0:def 3;
then x in {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:20;
then A97: x = E-max L~Cage(C,n) by A90,A95,TARSKI:def 2;
1 in dom Lower_Seq(C,n) by A5,FINSEQ_3:27;
then Lower_Seq(C,n).1 = Lower_Seq(C,n)/.1 by FINSEQ_4:def 4
.= E-max L~Cage(C,n) by JORDAN1F:6;
then x = Gij by A17,A96,A97,JORDAN1E:11;
then x in LSeg(Gauge(C,n)*(i,wG),Gij) by TOPREAL1:6;
then x in L~<*Gauge(C,n)*(i,wG),Gij*> by SPPOL_2:21;
hence L~Upper_Seq(C,n) meets L~<*Gauge(C,n)*(i,wG),Gij*>
by A90,A92,XBOOLE_0:3;
suppose A98: x in LSeg(v1/.(len v1),NE);
x in L~Cage(C,n) by A4,A90,A92,XBOOLE_0:def 2;
then x in LSeg(W-min L~Cage(C,n), NE) /\ L~Cage(C,n)
by A22,A98,XBOOLE_0:def 3;
then x in {W-min L~Cage(C,n)} by PSCOMP_1:92;
hence L~Upper_Seq(C,n) meets L~<*Gauge(C,n)*(i,wG),Gij*>
by A90,A95,TARSKI:def 1;
end;
then L~<*Gauge(C,n)*(i,wG),Gij*> meets L~Upper_Seq(C,n);
hence LSeg(Gauge(C,n)*(i,width Gauge(C,n)),Gij) meets L~Upper_Seq(C,n)
by SPPOL_2:21;
suppose A99: Gij in L~Lower_Seq(C,n) &
Gij <> Lower_Seq(C,n).len Lower_Seq(C,n)
& W-min L~Cage(C,n) = NE & i < lG;
then A100: v1 is non empty by JORDAN1E:7;
then len v1 <> 0 by FINSEQ_1:25;
then len v1 > 0 by NAT_1:19;
then A101: 0+1 <= len v1 by NAT_1:38;
then A102: 1 in dom v1 by FINSEQ_3:27;
set v = Gv1;
A103: len v1 in dom v1 & len Lower_Seq(C,n) in dom Lower_Seq(C,n)
by A5,A101,FINSEQ_3:27;
v1/.(len v1) = v1.(len v1) by A103,FINSEQ_4:def 4
.= Lower_Seq(C,n).len Lower_Seq(C,n) by A99,JORDAN1B:5
.= Lower_Seq(C,n)/.len Lower_Seq(C,n) by A103,FINSEQ_4:def 4
.= W-min L~Cage(C,n) by JORDAN1F:8;
then A104: Gv1/.len Gv1 = W-min L~Cage(C,n) by A100,SPRECT_3:11;
A105: v1/.1 = v1.1 by A102,FINSEQ_4:def 4
.= Gij by A99,JORDAN3:58;
1+len v1 >= 1+1 by A101,REAL_1:55;
then 2 <= len v by FINSEQ_5:8;
then A106: 2 <= len Rev v by FINSEQ_5:def 3;
A107: not Gauge(C,n)*(i,wG) in L~Lower_Seq(C,n) by A1,A99,JORDAN1G:53;
rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by A5,SPPOL_2:18;
then A108: not Gauge(C,n)*(i,wG) in rng Lower_Seq(C,n)
by A1,A99,JORDAN1G:53;
not Gauge(C,n)*(i,wG) in {Gij} by A99,A107,TARSKI:def 1;
then A109: not Gauge(C,n)*(i,wG) in rng <*Gij*> by FINSEQ_1:55;
set ci = mid(Lower_Seq(C,n),Index(Gij,Lower_Seq(C,n))+1,
len Lower_Seq(C,n));
now per cases;
suppose A110: Gij <> Lower_Seq(C,n).(Index(Gij,Lower_Seq(C,n))+1);
rng ci c= rng Lower_Seq(C,n) by JORDAN3:28;
then not Gauge(C,n)*(i,wG) in rng ci by A108;
then not Gauge(C,n)*(i,wG) in rng <*Gij*> \/ rng ci
by A109,XBOOLE_0:def 2;
then not Gauge(C,n)*(i,wG) in rng(<*Gij*>^ci) by FINSEQ_1:44;
hence not Gauge(C,n)*(i,wG) in rng v1 by A110,JORDAN3:def 4;
suppose Gij = Lower_Seq(C,n).(Index(Gij,Lower_Seq(C,n))+1);
then v1 = ci by JORDAN3:def 4;
then rng v1 c= rng Lower_Seq(C,n) by JORDAN3:28;
hence not Gauge(C,n)*(i,wG) in rng v1 by A108;
end;
then {Gauge(C,n)*(i,wG)} misses rng v1 by ZFMISC_1:56;
then A111: rng <*Gauge(C,n)*(i,wG)*> misses rng v1 by FINSEQ_1:55;
A112: <*Gauge(C,n)*(i,wG)*> is one-to-one by FINSEQ_3:102;
A113: v1 is_S-Seq by A99,JORDAN3:69;
then v1 is one-to-one by TOPREAL1:def 10;
then A114: Gv1 is one-to-one by A111,A112,FINSEQ_3:98;
for v be one-to-one FinSequence holds Rev v is one-to-one;
then A115: Rev v is one-to-one by A114;
A116: <*Gauge(C,n)*(i,wG)*> is special by SPPOL_2:39;
A117: v1 is special by A113,TOPREAL1:def 10;
(<*Gauge(C,n)*(i,wG)*>/.len <*Gauge(C,n)*(i,wG)*>)`1 =
(<*Gauge(C,n)*(i,wG)*>/.1)`1 by FINSEQ_1:56
.= Gauge(C,n)*(i,wG)`1 by FINSEQ_4:25
.= Gauge(C,n)*(i,1)`1 by A1,A7,GOBOARD5:3
.= (v1/.1)`1 by A1,A2,A105,GOBOARD5:3;
then Gv1 is special by A116,A117,GOBOARD2:13;
then A118: Rev v is special by SPPOL_2:42;
A119: len Upper_Seq(C,n) >= 2+1 by JORDAN1E:19;
then A120: len Upper_Seq(C,n) > 2 by NAT_1:38;
len Upper_Seq(C,n) > 1 by A119,AXIOMS:22;
then h is S-Sequence_in_R2 by A120,JORDAN3:39;
then A121: 2 <= len h & h is one-to-one & h is special
by TOPREAL1:def 10;
A122: Upper_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:21;
3 <= len Upper_Seq(C,n) by JORDAN1E:19;
then 2 <= len Upper_Seq(C,n) by AXIOMS:22;
then A123: 2 in dom Upper_Seq(C,n) by FINSEQ_3:27;
A124: len Upper_Seq(C,n) in dom Upper_Seq(C,n) by SCMFSA_7:12;
then A125: h is_in_the_area_of Cage(C,n) by A122,A123,SPRECT_2:26;
Upper_Seq(C,n)/.(len Upper_Seq(C,n)) = E-max L~Cage(C,n) by JORDAN1F:7;
then (Upper_Seq(C,n)/.len Upper_Seq(C,n))`1 = E-bound L~Cage(C,n)
by PSCOMP_1:104;
then A126: (h/.len h)`1 = E-bound L~Cage(C,n) by A123,A124,SPRECT_2:13;
(Upper_Seq(C,n)/.(1+1))`1 = W-bound L~Cage(C,n) by JORDAN1G:39;
then (h/.1)`1 = W-bound L~Cage(C,n) by A123,A124,SPRECT_2:12;
then A127: h is_a_h.c._for Cage(C,n) by A125,A126,SPRECT_2:def 2;
now let m be Nat;
assume A128: m in dom <*Gauge(C,n)*(i,wG)*>;
then m in Seg 1 by FINSEQ_1:55;
then m = 1 by FINSEQ_1:4,TARSKI:def 1;
then <*Gauge(C,n)*(i,wG)*>.m = Gauge(C,n)*(i,wG) by FINSEQ_1:57;
then A129: <*Gauge(C,n)*(i,wG)*>/.m = Gauge(C,n)*(i,wG)
by A128,FINSEQ_4:def 4;
Gauge(C,n)*(1,wG)`1 <= Gauge(C,n)*(i,wG)`1 by A1,A7,SPRECT_3:25;
hence W-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,wG)*>/.m)`1
by A6,A7,A129,JORDAN1A:94;
(Gauge(C,n)*(i,wG))`1 <= Gauge(C,n)*(len Gauge(C,n),wG)`1
by A1,A7,SPRECT_3:25;
hence (<*Gauge(C,n)*(i,wG)*>/.m)`1 <= E-bound L~Cage(C,n)
by A6,A7,A129,JORDAN1A:92;
(<*Gauge(C,n)*(i,wG)*>/.m)`2 = N-bound L~Cage(C,n)
by A1,A6,A129,JORDAN1A:91;
hence S-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,wG)*>/.m)`2
by SPRECT_1:24;
thus (<*Gauge(C,n)*(i,wG)*>/.m)`2 <= N-bound L~Cage(C,n)
by A1,A6,A129,JORDAN1A:91;
end;
then A130: <*Gauge(C,n)*(i,wG)*> is_in_the_area_of Cage(C,n)
by SPRECT_2:def 1;
A131: Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:22;
<*Gij*> is_in_the_area_of Cage(C,n) by A99,A131,SPRECT_3:63;
then v1 is_in_the_area_of Cage(C,n) by A99,A131,SPRECT_3:73;
then Gv1 is_in_the_area_of Cage(C,n) by A130,SPRECT_2:28;
then A132: Rev v is_in_the_area_of Cage(C,n) by SPRECT_3:68;
v/.1 = Gauge(C,n)*(i,wG) by FINSEQ_5:16;
then (v/.1)`2 = N-bound L~Cage(C,n) by A1,A6,JORDAN1A:91;
then (Rev v/.(len v))`2 = N-bound L~Cage(C,n) by FINSEQ_5:68;
then A133: (Rev v/.(len Rev v))`2 = N-bound L~Cage(C,n)
by FINSEQ_5:def 3;
(v/.len v)`2 = S-bound L~Cage(C,n) by A99,A104,PSCOMP_1:73;
then (Rev v/.1)`2 = S-bound L~Cage(C,n) by FINSEQ_5:68;
then Rev v is_a_v.c._for Cage(C,n) by A132,A133,SPRECT_2:def 3;
then L~h meets L~Rev v by A106,A115,A118,A121,A127,SPRECT_2:33;
then L~h meets L~v by SPPOL_2:22;
then consider x be set such that
A134: x in L~h and
A135: x in L~v by XBOOLE_0:3;
A136: L~h c= L~Upper_Seq(C,n) by A5,JORDAN4:47;
A137: L~v1 c= L~Lower_Seq(C,n) by A99,JORDAN3:77;
L~v = LSeg(Gauge(C,n)*(i,wG),v1/.1) \/ L~v1 by A100,SPPOL_2:20;
then A138: x in LSeg(Gauge(C,n)*(i,wG),v1/.1) or x in L~v1
by A135,XBOOLE_0:def 2;
Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by JORDAN1F:5;
then A139: not W-min L~Cage(C,n) in L~h by A120,JORDAN5B:16;
now per cases by A138;
suppose x in LSeg(Gauge(C,n)*(i,wG),v1/.1);
then x in L~<*Gauge(C,n)*(i,wG),Gij*> by A105,SPPOL_2:21;
hence L~Upper_Seq(C,n) meets L~<*Gauge(C,n)*(i,wG),Gij*>
by A134,A136,XBOOLE_0:3;
suppose A140: x in L~v1;
then x in L~Lower_Seq(C,n) /\ L~Upper_Seq(C,n)
by A134,A136,A137,XBOOLE_0:def 3;
then x in {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:20;
then A141: x = E-max L~Cage(C,n) by A134,A139,TARSKI:def 2;
1 in dom Lower_Seq(C,n) by A5,FINSEQ_3:27;
then Lower_Seq(C,n).1 = Lower_Seq(C,n)/.1 by FINSEQ_4:def 4
.= E-max L~Cage(C,n) by JORDAN1F:6;
then x = Gij by A99,A140,A141,JORDAN1E:11;
then x in LSeg(Gauge(C,n)*(i,wG),Gij) by TOPREAL1:6;
then x in L~<*Gauge(C,n)*(i,wG),Gij*> by SPPOL_2:21;
hence L~Upper_Seq(C,n) meets L~<*Gauge(C,n)*(i,wG),Gij*>
by A134,A136,XBOOLE_0:3;
end;
then L~<*Gauge(C,n)*(i,wG),Gij*> meets L~Upper_Seq(C,n);
hence LSeg(Gauge(C,n)*(i,width Gauge(C,n)),Gij) meets L~Upper_Seq(C,n)
by SPPOL_2:21;
suppose A142: Gij in L~Upper_Seq(C,n);
Gij in LSeg(Gauge(C,n)*(i,wG),Gij) by TOPREAL1:6;
hence LSeg(Gauge(C,n)*(i,width Gauge(C,n)),Gij) meets L~Upper_Seq(C,n)
by A142,XBOOLE_0:3;
suppose A143: Gij in L~Lower_Seq(C,n) &
Gij = Lower_Seq(C,n).len Lower_Seq(C,n);
len Lower_Seq(C,n) in dom Lower_Seq(C,n) by A5,FINSEQ_3:27;
then A144: Lower_Seq(C,n).len Lower_Seq(C,n) =
Lower_Seq(C,n)/.len Lower_Seq(C,n) by FINSEQ_4:def 4
.= W-min L~Cage(C,n) by JORDAN1F:8;
A145: rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by A5,SPPOL_2:18;
A146: W-min L~Cage(C,n) in rng Upper_Seq(C,n) by JORDAN1J:5;
Gij in LSeg(Gauge(C,n)*(i,wG),Gij) by TOPREAL1:6;
hence LSeg(Gauge(C,n)*(i,wG),Gij) meets L~Upper_Seq(C,n)
by A143,A144,A145,A146,XBOOLE_0:3;
end;
hence thesis;
end;
theorem Th4:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for n be Nat st n > 0
for i,j be Nat st 1 <= i & i <= len Gauge(C,n) &
1 <= j & j <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Cage(C,n) holds
LSeg(Gauge(C,n)*(i,width Gauge(C,n)),Gauge(C,n)*(i,j)) meets
Upper_Arc L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let n be Nat;
assume A1: n > 0;
let i,j be Nat;
assume A2: 1 <= i & i <= len Gauge(C,n) & 1 <= j & j <= width Gauge(C,n) &
Gauge(C,n)*(i,j) in L~Cage(C,n);
L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) by A1,JORDAN1G:63;
hence thesis by A2,Th3;
end;
theorem
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for j be Nat holds
Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Lower_Arc L~Cage(C,n+1) &
1 <= j & j <= width Gauge(C,n+1) implies
LSeg(Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1)),
Gauge(C,n+1)*(Center Gauge(C,n+1),j)) meets Upper_Arc L~Cage(C,n+1)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let j be Nat;
assume that
A1: Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Lower_Arc L~Cage(C,n+1) and
A2: 1 <= j & j <= width Gauge(C,n+1);
set in1 = Center Gauge(C,n+1);
A3: n+1 >= 0+1 by NAT_1:29;
then A4: n+1 > 0 by NAT_1:38;
A5: 1 <= in1 by JORDAN1B:12;
A6: in1 <= len Gauge(C,n+1) by JORDAN1B:14;
A7: LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),width Gauge(C,n+1)),
Gauge(C,n+1)*(Center Gauge(C,n+1),j)) c=
LSeg(Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1)),
Gauge(C,n+1)*(Center Gauge(C,n+1),j)) by A2,A3,Th2;
Lower_Arc L~Cage(C,n+1) c= L~Cage(C,n+1) by JORDAN1A:16;
then LSeg(Gauge(C,n+1)*(in1,width Gauge(C,n+1)),Gauge(C,n+1)*(in1,j))
meets Upper_Arc L~Cage(C,n+1) by A1,A2,A4,A5,A6,Th4;
hence thesis by A7,XBOOLE_1:63;
end;
theorem Th6:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for f be FinSequence of TOP-REAL 2
for k be Nat st 1 <= k & k+1 <= len f & f is_sequence_on Gauge(C,n) holds
dist(f/.k,f/.(k+1)) = (N-bound C - S-bound C)/2|^n or
dist(f/.k,f/.(k+1)) = (E-bound C - W-bound C)/2|^n
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let f be FinSequence of TOP-REAL 2;
let k be Nat;
assume A1: 1 <= k & k+1 <= len f;
assume f is_sequence_on Gauge(C,n);
then consider i1,j1,i2,j2 be Nat such that
A2: [i1,j1] in Indices Gauge(C,n) and
A3: f/.k = Gauge(C,n)*(i1,j1) and
A4: [i2,j2] in Indices Gauge(C,n) and
A5: f/.(k+1) = Gauge(C,n)*(i2,j2) and
A6: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,JORDAN8:6;
per cases by A6;
suppose i1 = i2 & j1+1 = j2;
hence thesis by A2,A3,A4,A5,GOBRD14:19;
suppose i1+1 = i2 & j1 = j2;
hence thesis by A2,A3,A4,A5,GOBRD14:20;
suppose i1 = i2+1 & j1 = j2;
hence thesis by A2,A3,A4,A5,GOBRD14:20;
suppose i1 = i2 & j1 = j2+1;
hence thesis by A2,A3,A4,A5,GOBRD14:19;
end;
theorem
for M be symmetric triangle MetrStruct
for r be real number
for p,q,x be Element of M st
p in Ball(x,r) & q in Ball(x,r) holds
dist(p,q) < 2*r
proof
let M be symmetric triangle MetrStruct;
let r be real number;
let p,q,x be Element of M;
assume that
A1: p in Ball(x,r) and
A2: q in Ball(x,r);
A3: dist(p,x) < r by A1,METRIC_1:12;
A4: dist(x,q) < r by A2,METRIC_1:12;
A5: dist(p,q) <= dist(p,x) + dist(x,q) by METRIC_1:4;
dist(p,x) + dist(x,q) < r+r by A3,A4,REAL_1:67;
then dist(p,q) < r+r by A5,AXIOMS:22;
hence dist(p,q) < 2*r by XCMPLX_1:11;
end;
theorem Th8:
for A be Subset of TOP-REAL n
for p be Point of TOP-REAL n
for p' be Point of Euclid n st p = p'
for s be real number st s > 0 holds
p in Cl A iff
for r be real number st 0 < r & r < s holds Ball (p',r) meets A
proof
let A be Subset of TOP-REAL n;
let p be Point of TOP-REAL n;
let p' be Point of Euclid n;
assume A1: p = p';
let s be real number;
assume A2: s > 0;
hereby assume
A3: p in Cl A;
let r be real number;
assume A4: 0 < r & r < s;
the carrier of TOP-REAL n = the carrier of Euclid n by TOPREAL3:13;
then reconsider B = Ball (p',r) as Subset of TOP-REAL n;
B is a_neighborhood of p by A1,A4,KURATO_2:35;
hence Ball (p', r) meets A by A3,YELLOW_6:6;
end;
assume A5: for r be real number st 0 < r & r < s holds
Ball (p',r) meets A;
for G be a_neighborhood of p holds G meets A
proof
let G be a_neighborhood of p;
p in Int G by CONNSP_2:def 1;
then consider r' be real number such that
A6: r' > 0 & Ball (p',r') c= G by A1,GOBOARD6:8;
set r = min(r',s/2);
reconsider rr = r, rr' = r' as Real by XREAL_0:def 1;
A7: s/2 < s by A2,SEQ_2:4;
s/2 > 0 by A2,SEQ_2:3;
then A8: r > 0 by A6,SQUARE_1:38;
r <= r' by SQUARE_1:35;
then Ball (p',rr) c= Ball (p',rr') by PCOMPS_1:1;
then A9: Ball (p',r) c= G by A6,XBOOLE_1:1;
r <= s/2 by SQUARE_1:35;
then r < s by A7,AXIOMS:22;
then Ball (p',r) meets A by A5,A8;
hence thesis by A9,XBOOLE_1:63;
end;
hence thesis by YELLOW_6:6;
end;
theorem
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
N-bound C < N-bound L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
A1: 2|^n > 0 by HEINE:5;
N-bound C > S-bound C + 0 by SPRECT_1:34;
then N-bound C - S-bound C > 0 by REAL_1:86;
then (N-bound C - S-bound C)/(2|^n) > 0 by A1,REAL_2:127;
then A2: (N-bound C - S-bound C)/(2|^n) > N-bound C - N-bound C
by XCMPLX_1:14;
N-bound L~Cage(C,n) = N-bound C + (N-bound C - S-bound C)/(2|^n)
by JORDAN10:6;
hence N-bound C < N-bound L~Cage(C,n) by A2,REAL_1:84;
end;
theorem Th10:
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
E-bound C < E-bound L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
A1: 2|^n > 0 by HEINE:5;
E-bound C > W-bound C + 0 by SPRECT_1:33;
then E-bound C - W-bound C > 0 by REAL_1:86;
then (E-bound C - W-bound C)/(2|^n) > 0 by A1,REAL_2:127;
then A2: (E-bound C - W-bound C)/(2|^n) > E-bound C - E-bound C
by XCMPLX_1:14;
E-bound L~Cage(C,n) = E-bound C + (E-bound C - W-bound C)/(2|^n)
by JORDAN1A:85;
hence E-bound C < E-bound L~Cage(C,n) by A2,REAL_1:84;
end;
theorem
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
S-bound L~Cage(C,n) < S-bound C
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
A1: 2|^n > 0 by HEINE:5;
N-bound C > S-bound C + 0 by SPRECT_1:34;
then N-bound C - S-bound C > 0 by REAL_1:86;
then (N-bound C - S-bound C)/(2|^n) > 0 by A1,REAL_2:127;
then A2: (N-bound C - S-bound C)/(2|^n) > S-bound C - S-bound C
by XCMPLX_1:14;
S-bound L~Cage(C,n) = S-bound C - (N-bound C - S-bound C)/(2|^n)
by JORDAN1A:84;
hence S-bound L~Cage(C,n) < S-bound C by A2,REAL_2:165;
end;
theorem Th12:
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
W-bound L~Cage(C,n) < W-bound C
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
A1: 2|^n > 0 by HEINE:5;
E-bound C > W-bound C + 0 by SPRECT_1:33;
then E-bound C - W-bound C > 0 by REAL_1:86;
then (E-bound C - W-bound C)/(2|^n) > 0 by A1,REAL_2:127;
then A2: (E-bound C - W-bound C)/(2|^n) > W-bound C - W-bound C
by XCMPLX_1:14;
W-bound L~Cage(C,n) = W-bound C - (E-bound C - W-bound C)/(2|^n)
by JORDAN1A:83;
hence W-bound L~Cage(C,n) < W-bound C by A2,REAL_2:165;
end;
theorem Th13:
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= k & k <= j & j <= width Gauge(C,n) &
LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,k)} &
LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,j)} holds
LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) meets Upper_Arc C
proof
let C be Simple_closed_curve;
let i,j,k be Nat;
set Ga = Gauge(C,n);
set US = Upper_Seq(C,n);
set LS = Lower_Seq(C,n);
set UA = Upper_Arc C;
set Wmin = W-min L~Cage(C,n);
set Emax = E-max L~Cage(C,n);
set Wbo = W-bound L~Cage(C,n);
set Ebo = E-bound L~Cage(C,n);
set Gik = Ga*(i,k);
set Gij = Ga*(i,j);
assume that
A1: 1 < i & i < len Ga and
A2: 1 <= k & k <= j & j <= width Ga and
A3: LSeg(Gik,Gij) /\ L~US = {Gik} and
A4: LSeg(Gik,Gij) /\ L~LS = {Gij} and
A5: LSeg(Gik,Gij) misses UA;
Gij in {Gij} by TARSKI:def 1;
then A6: Gij in L~LS by A4,XBOOLE_0:def 3;
Gik in {Gik} by TARSKI:def 1;
then A7: Gik in L~US by A3,XBOOLE_0:def 3;
A8: j <> k by A1,A2,A6,A7,JORDAN1J:57;
A9: 1 <= j & j <= width Ga by A2,AXIOMS:22;
A10: 1 <= k & k <= width Ga by A2,AXIOMS:22;
A11: [i,j] in Indices Ga by A1,A9,GOBOARD7:10;
A12: [i,k] in Indices Ga by A1,A10,GOBOARD7:10;
A13: LS is_sequence_on Ga by JORDAN1G:5;
A14: US is_sequence_on Ga by JORDAN1G:4;
set do = L_Cut(LS,Gij);
set go = R_Cut(US,Gik);
A15: len Ga = width Ga by JORDAN8:def 1;
A16: len US >= 3 by JORDAN1E:19;
then len US >= 1 by AXIOMS:22;
then 1 in dom US by FINSEQ_3:27;
then A17: US.1 = US/.1 by FINSEQ_4:def 4
.= Wmin by JORDAN1F:5;
A18: Wmin`1 = Wbo by PSCOMP_1:84
.= Ga*(1,k)`1 by A10,A15,JORDAN1A:94;
len Ga >= 4 by JORDAN8:13;
then A19: len Ga >= 1 by AXIOMS:22;
then A20: [1,k] in Indices Ga by A10,GOBOARD7:10;
then A21: Gik <> US.1 by A1,A12,A17,A18,JORDAN1G:7;
then reconsider go as being_S-Seq FinSequence of TOP-REAL 2
by A7,JORDAN3:70;
A22: len LS >= 1+2 by JORDAN1E:19;
then len LS >= 1 by AXIOMS:22;
then A23: 1 in dom LS & len LS in dom LS by FINSEQ_3:27;
then A24: LS.len LS = LS/.len LS by FINSEQ_4:def 4
.= Wmin by JORDAN1F:8;
A25: Wmin`1 = Wbo by PSCOMP_1:84
.= Ga*(1,k)`1 by A10,A15,JORDAN1A:94;
A26: [i,j] in Indices Ga by A1,A9,GOBOARD7:10;
then A27: Gij <> LS.len LS by A1,A20,A24,A25,JORDAN1G:7;
then reconsider do as being_S-Seq FinSequence of TOP-REAL 2
by A6,JORDAN3:69;
A28: [len Ga,k] in Indices Ga by A10,A19,GOBOARD7:10;
A29: LS.1 = LS/.1 by A23,FINSEQ_4:def 4
.= Emax by JORDAN1F:6;
Emax`1 = Ebo by PSCOMP_1:104
.= Ga*(len Ga,k)`1 by A10,A15,JORDAN1A:92;
then A30: Gij <> LS.1 by A1,A26,A28,A29,JORDAN1G:7;
A31: len go >= 1+1 by TOPREAL1:def 10;
A32: Gik in rng US by A1,A7,A10,A14,JORDAN1J:40;
then A33: go is_sequence_on Ga by A14,JORDAN1J:38;
A34: go is s.c.c. by JGRAPH_1:16;
A35: len do >= 1+1 by TOPREAL1:def 10;
A36: Gij in rng LS by A1,A6,A9,A13,JORDAN1J:40;
then A37: do is_sequence_on Ga by A13,JORDAN1J:39;
A38: do is s.c.c. by JGRAPH_1:16;
reconsider go as non constant s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2) by A31,A33,A34,JORDAN8:8;
reconsider do as non constant s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2) by A35,A37,A38,JORDAN8:8;
A39: len go > 1 by A31,NAT_1:38;
then A40: len go in dom go by FINSEQ_3:27;
then A41: go/.len go = go.len go by FINSEQ_4:def 4
.= Gik by A7,JORDAN3:59;
len do >= 1 by A35,AXIOMS:22;
then 1 in dom do by FINSEQ_3:27;
then A42: do/.1 = do.1 by FINSEQ_4:def 4
.= Gij by A6,JORDAN3:58;
reconsider m = len go - 1 as Nat by A40,FINSEQ_3:28;
A43: m+1 = len go by XCMPLX_1:27;
then A44: len go-'1 = m by BINARITH:39;
A45: LSeg(go,m) c= L~go by TOPREAL3:26;
A46: L~go c= L~US by A7,JORDAN3:76;
then LSeg(go,m) c= L~US by A45,XBOOLE_1:1;
then A47: LSeg(go,m) /\ LSeg(Gik,Gij) c= {Gik} by A3,XBOOLE_1:26;
m >= 1 by A31,REAL_1:84;
then A48: LSeg(go,m) = LSeg(go/.m,Gik) by A41,A43,TOPREAL1:def 5;
{Gik} c= LSeg(go,m) /\ LSeg(Gik,Gij)
proof
let x be set;
assume x in {Gik};
then A49: x = Gik by TARSKI:def 1;
A50: Gik in LSeg(go,m) by A48,TOPREAL1:6;
Gik in LSeg(Gik,Gij) by TOPREAL1:6;
hence x in LSeg(go,m) /\ LSeg(Gik,Gij) by A49,A50,XBOOLE_0:def 3;
end;
then A51: LSeg(go,m) /\ LSeg(Gik,Gij) = {Gik} by A47,XBOOLE_0:def 10;
A52: LSeg(do,1) c= L~do by TOPREAL3:26;
A53: L~do c= L~LS by A6,JORDAN3:77;
then LSeg(do,1) c= L~LS by A52,XBOOLE_1:1;
then A54: LSeg(do,1) /\ LSeg(Gik,Gij) c= {Gij} by A4,XBOOLE_1:26;
A55: LSeg(do,1) = LSeg(Gij,do/.(1+1)) by A35,A42,TOPREAL1:def 5;
{Gij} c= LSeg(do,1) /\ LSeg(Gik,Gij)
proof
let x be set;
assume x in {Gij};
then A56: x = Gij by TARSKI:def 1;
A57: Gij in LSeg(do,1) by A55,TOPREAL1:6;
Gij in LSeg(Gik,Gij) by TOPREAL1:6;
hence x in LSeg(do,1) /\ LSeg(Gik,Gij) by A56,A57,XBOOLE_0:def 3;
end;
then A58: LSeg(Gik,Gij) /\ LSeg(do,1) = {Gij} by A54,XBOOLE_0:def 10;
A59: go/.1 = US/.1 by A7,SPRECT_3:39
.= Wmin by JORDAN1F:5;
then A60: go/.1 = LS/.len LS by JORDAN1F:8
.= do/.len do by A6,JORDAN1J:35;
A61: rng go c= L~go & rng do c= L~do by A31,A35,SPPOL_2:18;
A62: {go/.1} c= L~go /\ L~do
proof
let x be set;
assume x in {go/.1};
then x = go/.1 by TARSKI:def 1;
then x in rng go & x in rng do by A60,FINSEQ_6:46,REVROT_1:3;
hence x in L~go /\ L~do by A61,XBOOLE_0:def 3;
end;
A63: LS.1 = LS/.1 by A23,FINSEQ_4:def 4
.= Emax by JORDAN1F:6;
A64: [len Ga,j] in Indices Ga by A9,A19,GOBOARD7:10;
L~go /\ L~do c= {go/.1}
proof
let x be set;
assume x in L~go /\ L~do;
then A65: x in L~go & x in L~do by XBOOLE_0:def 3;
then x in L~US /\ L~LS by A46,A53,XBOOLE_0:def 3;
then x in {Wmin,Emax} by JORDAN1E:20;
then A66: x = Wmin or x = Emax by TARSKI:def 2;
now assume x = Emax;
then A67: Emax = Gij by A6,A63,A65,JORDAN1E:11;
Ga*(len Ga,j)`1 = Ebo by A9,A15,JORDAN1A:92;
then Emax`1 <> Ebo by A1,A11,A64,A67,JORDAN1G:7;
hence contradiction by PSCOMP_1:104;
end;
hence x in {go/.1} by A59,A66,TARSKI:def 1;
end;
then A68: L~go /\ L~do = {go/.1} by A62,XBOOLE_0:def 10;
set W2 = go/.2;
A69: 2 in dom go by A31,FINSEQ_3:27;
A70: Gik..US >= 1 by A32,FINSEQ_4:31;
A71: now assume Gik`1 = Wbo;
then Ga*(1,k)`1 = Ga*(i,k)`1 by A10,A15,JORDAN1A:94;
hence contradiction by A1,A12,A20,JORDAN1G:7;
end;
go = mid(US,1,Gik..US) by A32,JORDAN1G:57
.= US|(Gik..US) by A70,JORDAN3:25;
then A72: W2 = US/.2 by A69,TOPREAL1:1;
A73: Wmin in rng go by A59,FINSEQ_6:46;
set pion = <*Gik,Gij*>;
A74: now let n be Nat;
assume n in dom pion;
then n in Seg 2 by FINSEQ_3:29;
then n = 1 or n = 2 by FINSEQ_1:4,TARSKI:def 2;
then pion/.n = Gik or pion/.n = Gij by FINSEQ_4:26;
hence ex i,j be Nat st [i,j] in Indices Ga & pion/.n = Ga*(i,j)
by A11,A12;
end;
A75: Gik <> Gij by A8,A11,A12,GOBOARD1:21;
A76: Gik`1 = Ga*(i,1)`1 by A1,A10,GOBOARD5:3
.= Gij`1 by A1,A9,GOBOARD5:3;
then LSeg(Gik,Gij) is vertical by SPPOL_1:37;
then pion is_S-Seq by A75,JORDAN1B:8;
then consider pion1 be FinSequence of TOP-REAL 2 such that
A77: pion1 is_sequence_on Ga and
A78: pion1 is_S-Seq and
A79: L~pion = L~pion1 and
A80: pion/.1 = pion1/.1 and
A81: pion/.len pion = pion1/.len pion1 and
A82: len pion <= len pion1 by A74,GOBOARD3:2;
reconsider pion1 as being_S-Seq FinSequence of TOP-REAL 2 by A78;
set godo = go^'pion1^'do;
len Cage(C,n) > 4 by GOBOARD7:36;
then A83: 1+1 <= len Cage(C,n) by AXIOMS:22;
then A84: 1+1 <= len Rotate(Cage(C,n),Wmin) by REVROT_1:14;
len (go^'pion1) >= len go by TOPREAL8:7;
then A85: len (go^'pion1) >= 1+1 by A31,AXIOMS:22;
then A86: len (go^'pion1) > 1+0 by NAT_1:38;
len godo >= len (go^'pion1) by TOPREAL8:7;
then A87: 1+1 <= len godo by A85,AXIOMS:22;
A88: US is_sequence_on Ga by JORDAN1G:4;
A89: go/.len go = pion1/.1 by A41,A80,FINSEQ_4:26;
then A90: go^'pion1 is_sequence_on Ga by A33,A77,TOPREAL8:12;
A91: (go^'pion1)/.len (go^'pion1) = pion/.len pion by A81,AMISTD_1:6
.= pion/.2 by FINSEQ_1:61
.= do/.1 by A42,FINSEQ_4:26;
then A92: godo is_sequence_on Ga by A37,A90,TOPREAL8:12;
then A93: godo is standard special by JORDAN8:7;
A94: godo is non constant by A87,A92,JORDAN8:8;
LSeg(pion1,1) c= L~<*Gik,Gij*> by A79,TOPREAL3:26;
then LSeg(pion1,1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then A95: LSeg(go,len go-'1) /\ LSeg(pion1,1) c= {Gik}
by A44,A51,XBOOLE_1:27;
A96: len pion1 >= 1+1 by A82,FINSEQ_1:61;
{Gik} c= LSeg(go,m) /\ LSeg(pion1,1)
proof
let x be set;
assume x in {Gik};
then A97: x = Gik by TARSKI:def 1;
A98: Gik in LSeg(go,m) by A48,TOPREAL1:6;
Gik in LSeg(pion1,1) by A41,A89,A96,TOPREAL1:27;
hence x in LSeg(go,m) /\ LSeg(pion1,1) by A97,A98,XBOOLE_0:def 3;
end;
then LSeg(go,len go-'1) /\ LSeg(pion1,1) = { go/.len go }
by A41,A44,A95,XBOOLE_0:def 10;
then A99: go^'pion1 is unfolded by A89,TOPREAL8:34;
len pion1 >= 2+0 by A82,FINSEQ_1:61;
then A100: len pion1-2 >= 0 by REAL_1:84;
A101: len (go^'pion1)-1 >= 0 by A86,REAL_1:84;
len (go^'pion1)+1-1 = len go+len pion1-1 by GRAPH_2:13;
then len (go^'pion1)-1 = len go+len pion1-1-1 by XCMPLX_1:26
.= len go + len pion1-(1+1) by XCMPLX_1:36
.= len go + (len pion1-2) by XCMPLX_1:29
.= len go + (len pion1-'2) by A100,BINARITH:def 3;
then A102: len (go^'pion1)-'1 = len go + (len pion1-'2)
by A101,BINARITH:def 3;
A103: len pion1-1 >= 1 by A96,REAL_1:84;
then len pion1-1 >= 0 by AXIOMS:22;
then A104: len pion1-'1 = len pion1-1 by BINARITH:def 3;
A105: len pion1-'2+1 = len pion1-2+1 by A100,BINARITH:def 3
.= len pion1-(2-1) by XCMPLX_1:37
.= len pion1-'1 by A104;
len pion1-1+1 <= len pion1 by XCMPLX_1:27;
then A106: len pion1-'1 < len pion1 by A104,NAT_1:38;
LSeg(pion1,len pion1-'1) c= L~<*Gik,Gij*> by A79,TOPREAL3:26;
then LSeg(pion1,len pion1-'1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then A107: LSeg(pion1,len pion1-'1) /\ LSeg(do,1) c= {Gij}
by A58,XBOOLE_1:27;
{Gij} c= LSeg(pion1,len pion1-'1) /\ LSeg(do,1)
proof
let x be set;
assume x in {Gij};
then A108: x = Gij by TARSKI:def 1;
A109: Gij in LSeg(do,1) by A55,TOPREAL1:6;
A110: len pion1-'1+1 = len pion1 by A104,XCMPLX_1:27;
then pion1/.(len pion1-'1+1) = pion/.2 by A81,FINSEQ_1:61
.= Gij by FINSEQ_4:26;
then Gij in LSeg(pion1,len pion1-'1) by A103,A104,A110,TOPREAL1:27;
hence x in LSeg(pion1,len pion1-'1) /\ LSeg(do,1)
by A108,A109,XBOOLE_0:def 3;
end;
then LSeg(pion1,len pion1-'1) /\ LSeg(do,1) = {Gij}
by A107,XBOOLE_0:def 10;
then LSeg(go^'pion1,len go+(len pion1-'2)) /\ LSeg(do,1) =
{(go^'pion1)/.len (go^'pion1)} by A42,A89,A91,A105,A106,TOPREAL8:31;
then A111: godo is unfolded by A91,A99,A102,TOPREAL8:34;
A112: (go^'pion1) is non trivial by A85,SPPOL_1:2;
A113: rng pion1 c= L~pion1 by A96,SPPOL_2:18;
A114: {pion1/.1} c= L~go /\ L~pion1
proof
let x be set;
assume x in {pion1/.1};
then x = pion1/.1 by TARSKI:def 1;
then x in rng go & x in rng pion1 by A89,FINSEQ_6:46,REVROT_1:3;
hence x in L~go /\ L~pion1 by A61,A113,XBOOLE_0:def 3;
end;
L~go /\ L~pion1 c= {pion1/.1}
proof
let x be set;
assume x in L~go /\ L~pion1;
then x in L~go & x in L~pion1 by XBOOLE_0:def 3;
then x in L~pion1 /\ L~US by A46,XBOOLE_0:def 3;
hence x in {pion1/.1} by A3,A41,A79,A89,SPPOL_2:21;
end;
then A115: L~go /\ L~pion1 = {pion1/.1} by A114,XBOOLE_0:def 10;
then A116: (go^'pion1) is s.n.c. by A89,JORDAN1J:54;
rng go /\ rng pion1 c= {pion1/.1} by A61,A113,A115,XBOOLE_1:27;
then A117: go^'pion1 is one-to-one by JORDAN1J:55;
A118: pion/.len pion = pion/.2 by FINSEQ_1:61
.= do/.1 by A42,FINSEQ_4:26;
A119: {pion1/.len pion1} c= L~do /\ L~pion1
proof
let x be set;
assume x in {pion1/.len pion1};
then x = pion1/.len pion1 by TARSKI:def 1;
then x in rng do & x in rng pion1 by A81,A118,FINSEQ_6:46,REVROT_1:3;
hence x in L~do /\ L~pion1 by A61,A113,XBOOLE_0:def 3;
end;
L~do /\ L~pion1 c= {pion1/.len pion1}
proof
let x be set;
assume x in L~do /\ L~pion1;
then x in L~do & x in L~pion1 by XBOOLE_0:def 3;
then x in L~pion1 /\ L~LS by A53,XBOOLE_0:def 3;
hence x in {pion1/.len pion1} by A4,A42,A79,A81,A118,SPPOL_2:21;
end;
then A120: L~do /\ L~pion1 = {pion1/.len pion1} by A119,XBOOLE_0:def 10;
A121: L~(go^'pion1) /\ L~do = (L~go \/ L~pion1) /\ L~do by A89,TOPREAL8:35
.= {go/.1} \/ {do/.1} by A68,A81,A118,A120,XBOOLE_1:23
.= {(go^'pion1)/.1} \/ {do/.1} by AMISTD_1:5
.= {(go^'pion1)/.1,do/.1} by ENUMSET1:41;
A122: do/.len do = (go^'pion1)/.1 by A60,AMISTD_1:5;
reconsider godo as non constant standard special_circular_sequence
by A91,A93,A94,A99,A111,A112,A116,A117,A121,A122,TOPREAL8:11,33;
A123: UA is_an_arc_of W-min C,E-max C by JORDAN6:def 8;
then A124: UA is connected by JORDAN6:11;
A125: W-min C in UA & E-max C in UA by A123,TOPREAL1:4;
set ff = Rotate(Cage(C,n),Wmin);
Wmin in rng Cage(C,n) by SPRECT_2:47;
then A126: ff/.1 = Wmin by FINSEQ_6:98;
A127: L~ff = L~Cage(C,n) by REVROT_1:33;
then A128: (W-max L~ff)..ff > 1 by A126,SPRECT_5:23;
(W-max L~ff)..ff <= (N-min L~ff)..ff by A126,A127,SPRECT_5:24;
then A129: (N-min L~ff)..ff > 1 by A128,AXIOMS:22;
(N-min L~ff)..ff < (N-max L~ff)..ff by A126,A127,SPRECT_5:25;
then A130: (N-max L~ff)..ff > 1 by A129,AXIOMS:22;
(N-max L~ff)..ff <= (E-max L~ff)..ff by A126,A127,SPRECT_5:26;
then A131: Emax..ff > 1 by A127,A130,AXIOMS:22;
A132: now assume A133: Gik..US <= 1;
Gik..US >= 1 by A32,FINSEQ_4:31;
then Gik..US = 1 by A133,AXIOMS:21;
then Gik = US/.1 by A32,FINSEQ_5:41;
hence contradiction by A17,A21,JORDAN1F:5;
end;
A134: Cage(C,n) is_sequence_on Ga by JORDAN9:def 1;
then A135: ff is_sequence_on Ga by REVROT_1:34;
A136: right_cell(godo,1,Ga)\L~godo c= RightComp godo by A87,A92,JORDAN9:29;
A137: L~godo = L~(go^'pion1) \/ L~do by A91,TOPREAL8:35
.= L~go \/ L~pion1 \/ L~do by A89,TOPREAL8:35;
L~Cage(C,n) = L~US \/ L~LS by JORDAN1E:17;
then A138: L~US c= L~Cage(C,n) & L~LS c= L~Cage(C,n) by XBOOLE_1:7;
then A139: L~go c= L~Cage(C,n) & L~do c= L~Cage(C,n)
by A46,A53,XBOOLE_1:1;
A140: W-min C in C by SPRECT_1:15;
A141: L~pion = LSeg(Gik,Gij) by SPPOL_2:21;
A142: now assume W-min C in L~godo;
then W-min C in L~go \/ L~pion1 or W-min C in L~do by A137,XBOOLE_0:def 2;
then A143: W-min C in L~go or W-min C in L~pion1 or W-min C in L~do
by XBOOLE_0:def 2;
per cases by A143;
suppose W-min C in L~go;
then C meets L~Cage(C,n) by A139,A140,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
suppose W-min C in L~pion1;
hence contradiction by A5,A79,A125,A141,XBOOLE_0:3;
suppose W-min C in L~do;
then C meets L~Cage(C,n) by A139,A140,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
end;
right_cell(Rotate(Cage(C,n),Wmin),1) =
right_cell(ff,1,GoB ff) by A84,JORDAN1H:29
.= right_cell(ff,1,GoB Cage(C,n)) by REVROT_1:28
.= right_cell(ff,1,Ga) by JORDAN1H:52
.= right_cell(ff-:Emax,1,Ga) by A131,A135,JORDAN1J:53
.= right_cell(US,1,Ga) by JORDAN1E:def 1
.= right_cell(R_Cut(US,Gik),1,Ga) by A32,A88,A132,JORDAN1J:52
.= right_cell(go^'pion1,1,Ga) by A39,A90,JORDAN1J:51
.= right_cell(godo,1,Ga) by A86,A92,JORDAN1J:51;
then W-min C in right_cell(godo,1,Ga) by JORDAN1I:8;
then W-min C in right_cell(godo,1,Ga)\L~godo by A142,XBOOLE_0:def 4;
then A144: W-min C in RightComp godo by A136;
A145: godo/.1 = (go^'pion1)/.1 by AMISTD_1:5
.= Wmin by A59,AMISTD_1:5;
A146: len US >= 2 by A16,AXIOMS:22;
A147: godo/.2 = (go^'pion1)/.2 by A85,AMISTD_1:9
.= US/.2 by A31,A72,AMISTD_1:9
.= (US^'LS)/.2 by A146,AMISTD_1:9
.= Rotate(Cage(C,n),Wmin)/.2 by JORDAN1E:15;
A148: L~godo = L~go \/ L~pion1 \/ L~do by A137;
A149: L~go \/ L~do is compact by COMPTS_1:19;
A150: L~go \/ L~do c= L~Cage(C,n) by A139,XBOOLE_1:8;
A151: Wmin in L~go by A61,A73;
Wmin in L~go \/ L~do by A151,XBOOLE_0:def 2;
then A152: W-min (L~go \/ L~do) = Wmin by A149,A150,JORDAN1J:21;
A153: (W-min (L~go \/ L~do))`1 = W-bound (L~go \/ L~do) & Wmin`1 = Wbo
by PSCOMP_1:84;
W-bound LSeg(Gik,Gij) = Gik`1 by A76,SPRECT_1:62;
then A154: W-bound L~pion1 = Gik`1 by A79,SPPOL_2:21;
Gik`1 >= Wbo by A7,A138,PSCOMP_1:71;
then Gik`1 > Wbo by A71,REAL_1:def 5;
then W-min (L~go\/L~do\/L~pion1) = W-min (L~go \/ L~do)
by A149,A152,A153,A154,JORDAN1J:
33;
then A155: W-min L~godo = Wmin by A148,A152,XBOOLE_1:4;
A156: rng godo c= L~godo by A87,SPPOL_2:18;
2 in dom godo by A87,FINSEQ_3:27;
then godo/.2 in rng godo by PARTFUN2:4;
then A157: godo/.2 in L~godo by A156;
godo/.2 in W-most L~Cage(C,n) by A147,JORDAN1I:27;
then (godo/.2)`1 = (W-min L~godo)`1 by A155,PSCOMP_1:88
.= W-bound L~godo by PSCOMP_1:84;
then godo/.2 in W-most L~godo by A157,SPRECT_2:16;
then Rotate(godo,W-min L~godo)/.2 in W-most L~godo by A145,A155,FINSEQ_6:95
;
then reconsider godo as clockwise_oriented non constant standard
special_circular_sequence by JORDAN1I:27;
len US in dom US by FINSEQ_5:6;
then A158: US.len US = US/.len US by FINSEQ_4:def 4
.= Emax by JORDAN1F:7;
A159: E-max C in E-most C by PSCOMP_1:111;
A160: east_halfline E-max C misses L~go
proof
assume east_halfline E-max C meets L~go;
then consider p be set such that
A161: p in east_halfline E-max C and
A162: p in L~go by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A161;
A163: p in L~US by A46,A162;
then p in east_halfline E-max C /\ L~Cage(C,n) by A138,A161,XBOOLE_0:def 3
;
then A164: p`1 = Ebo by A159,JORDAN1A:104;
then A165: p = Emax by A163,JORDAN1J:46;
then Emax = Gik by A7,A158,A162,JORDAN1J:43;
then Gik`1 = Ga*(len Ga,k)`1 by A10,A15,A164,A165,JORDAN1A:92;
hence contradiction by A1,A12,A28,JORDAN1G:7;
end;
now assume east_halfline E-max C meets L~godo;
then A166: east_halfline E-max C meets (L~go \/ L~pion1) or
east_halfline E-max C meets L~do by A137,XBOOLE_1:70;
per cases by A166,XBOOLE_1:70;
suppose east_halfline E-max C meets L~go;
hence contradiction by A160;
suppose east_halfline E-max C meets L~pion1;
then consider p be set such that
A167: p in east_halfline E-max C and
A168: p in L~pion1 by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A167;
A169: p`1 = Gik`1 by A76,A79,A141,A168,GOBOARD7:5;
i+1 <= len Ga by A1,NAT_1:38;
then i+1-1 <= len Ga-1 by REAL_1:49;
then A170: i <= len Ga-1 by XCMPLX_1:26;
then len Ga-1 > 0 by A1,AXIOMS:22;
then A171: i <= len Ga-'1 by A170,BINARITH:def 3;
len Ga-'1 <= len Ga by GOBOARD9:2;
then p`1 <= Ga*(len Ga-'1,1)`1 by A1,A10,A15,A19,A169,A171,JORDAN1A:39;
then p`1 <= E-bound C by A19,JORDAN8:15;
then A172: p`1 <= (E-max C)`1 by PSCOMP_1:104;
p`1 >= (E-max C)`1 by A167,JORDAN1A:def 3;
then A173: p`1 = (E-max C)`1 by A172,AXIOMS:21;
p`2 = (E-max C)`2 by A167,JORDAN1A:def 3;
then p = E-max C by A173,TOPREAL3:11;
hence contradiction by A5,A79,A125,A141,A168,XBOOLE_0:3;
suppose east_halfline E-max C meets L~do;
then consider p be set such that
A174: p in east_halfline E-max C and
A175: p in L~do by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A174;
p in L~LS by A53,A175;
then p in east_halfline E-max C /\ L~Cage(C,n)
by A138,A174,XBOOLE_0:def 3;
then A176: p`1 = Ebo by A159,JORDAN1A:104;
A177: (E-max C)`2 = p`2 by A174,JORDAN1A:def 3;
set RC = Rotate(Cage(C,n),Emax);
A178: E-max C in right_cell(RC,1) by JORDAN1I:9;
A179: 1+1 <= len LS by A22,AXIOMS:22;
LS = RC-:Wmin by JORDAN1G:26;
then A180: LSeg(LS,1) = LSeg(RC,1) by A179,SPPOL_2:9;
A181: L~RC = L~Cage(C,n) by REVROT_1:33;
A182: len RC = len Cage(C,n) by REVROT_1:14;
A183: GoB RC = GoB Cage(C,n) by REVROT_1:28
.= Ga by JORDAN1H:52;
A184: Emax in rng Cage(C,n) by SPRECT_2:50;
A185: RC is_sequence_on Ga by A134,REVROT_1:34;
A186: RC/.1 = E-max L~RC by A181,A184,FINSEQ_6:98;
then consider ii,jj be Nat such that
A187: [ii,jj+1] in Indices Ga and
A188: [ii,jj] in Indices Ga and
A189: RC/.1 = Ga*(ii,jj+1) and
A190: RC/.(1+1) = Ga*(ii,jj) by A83,A182,A185,JORDAN1I:25;
consider jj2 be Nat such that
A191: 1 <= jj2 & jj2 <= width Ga and
A192: Emax = Ga*(len Ga,jj2) by JORDAN1D:29;
A193: len Ga >= 4 by JORDAN8:13;
then len Ga >= 1 by AXIOMS:22;
then [len Ga,jj2] in Indices Ga by A191,GOBOARD7:10;
then A194: ii = len Ga by A181,A186,A187,A189,A192,GOBOARD1:21;
A195: 1 <= ii & ii <= len Ga & 1 <= jj+1 & jj+1 <= width Ga
by A187,GOBOARD5:1;
A196: 1 <= ii & ii <= len Ga & 1 <= jj & jj <= width Ga
by A188,GOBOARD5:1;
A197: ii+1 <> ii by NAT_1:38;
jj+1 > jj by NAT_1:38;
then jj+1+1 <> jj by NAT_1:38;
then A198: right_cell(RC,1) = cell(Ga,ii-'1,jj)
by A83,A182,A183,A187,A188,A189,A190,A197,GOBOARD5:
def 6;
A199: ii-'1+1 = ii by A195,AMI_5:4;
ii-1 >= 4-1 by A193,A194,REAL_1:49;
then A200: ii-1 >= 1 by AXIOMS:22;
then ii-1 >= 0 by AXIOMS:22;
then A201: 1 <= ii-'1 by A200,BINARITH:def 3;
then A202: Ga*(ii-'1,jj)`2 <= p`2 & p`2 <= Ga*(ii-'1,jj+1)`2
by A177,A178,A195,A196,A198,A199,JORDAN9:19;
A203: ii-'1 < len Ga by A195,A199,NAT_1:38;
then A204: Ga*(ii-'1,jj)`2 = Ga*(1,jj)`2 by A196,A201,GOBOARD5:2
.= Ga*(ii,jj)`2 by A196,GOBOARD5:2;
A205: Ga*(ii-'1,jj+1)`2 = Ga*(1,jj+1)`2 by A195,A201,A203,GOBOARD5:2
.= Ga*(ii,jj+1)`2 by A195,GOBOARD5:2;
Ga*(len Ga,jj)`1 = Ebo & Ebo = Ga*(len Ga,jj+1)`1
by A15,A195,A196,JORDAN1A:92;
then p in LSeg(RC/.1,RC/.(1+1))
by A176,A189,A190,A194,A202,A204,A205,GOBOARD7:8;
then A206: p in LSeg(LS,1) by A83,A180,A182,TOPREAL1:def 5;
A207: p in LSeg(do,Index(p,do)) by A175,JORDAN3:42;
A208: do = mid(LS,Gij..LS,len LS) by A36,JORDAN1J:37;
A209: 1<=Gij..LS & Gij..LS<=len LS by A36,FINSEQ_4:31;
Gij..LS <> len LS by A27,A36,FINSEQ_4:29;
then A210: Gij..LS < len LS by A209,REAL_1:def 5;
A211: 1<=Index(p,do) & Index(p,do) < len do by A175,JORDAN3:41;
A212: Index(Gij,LS)+1 = Gij..LS by A30,A36,JORDAN1J:56;
consider t be Nat such that
A213: t in dom LS and
A214: LS.t = Gij by A36,FINSEQ_2:11;
A215: 1 <= t & t <= len LS by A213,FINSEQ_3:27;
1 < t by A30,A214,A215,REAL_1:def 5;
then Index(Gij,LS)+1 = t by A214,A215,JORDAN3:45;
then A216: len L_Cut(LS,Gij) = len LS-Index(Gij,LS)
by A6,A27,A214,JORDAN3:61;
set tt = Index(p,do)+(Gij..LS)-'1;
A217: 1<=Index(Gij,LS) & 0+Index(Gij,LS) < len LS by A6,JORDAN3:41;
then A218: len LS-Index(Gij,LS) > 0 by REAL_1:86;
then Index(p,do) < len LS-'Index(Gij,LS) by A211,A216,BINARITH:def 3;
then Index(p,do)+1 <= len LS-'Index(Gij,LS) by NAT_1:38;
then Index(p,do) <= len LS-'Index(Gij,LS)-1 by REAL_1:84;
then Index(p,do) <= len LS-Index(Gij,LS)-1 by A218,BINARITH:def 3;
then A219: Index(p,do) <= len LS-Gij..LS by A212,XCMPLX_1:36;
then len LS-Gij..LS >= 1 by A211,AXIOMS:22;
then len LS-Gij..LS >= 0 by AXIOMS:22;
then Index(p,do) <= len LS-'Gij..LS by A219,BINARITH:def 3;
then Index(p,do) < len LS-'(Gij..LS)+1 by NAT_1:38;
then A220: LSeg(mid(LS,Gij..LS,len LS),Index(p,do)) =
LSeg(LS,Index(p,do)+(Gij..LS)-'1) by A209,A210,A211,JORDAN4:31;
A221: 1+1 <= Gij..LS by A212,A217,REAL_1:55;
then Index(p,do)+Gij..LS >= 1+1+1 by A211,REAL_1:55;
then A222: Index(p,do)+Gij..LS-1 >= 1+1+1-1 by REAL_1:49;
then A223: Index(p,do)+Gij..LS-1 >= 0 by AXIOMS:22;
then A224: tt >= 1+1 by A222,BINARITH:def 3;
A225: 2 in dom LS by A179,FINSEQ_3:27;
now per cases by A224,REAL_1:def 5;
suppose tt > 1+1;
then LSeg(LS,1) misses LSeg(LS,tt) by TOPREAL1:def 9;
hence contradiction by A206,A207,A208,A220,XBOOLE_0:3;
suppose A226: tt = 1+1;
then LSeg(LS,1) /\ LSeg(LS,tt) = {LS/.2} by A22,TOPREAL1:def 8;
then p in {LS/.2} by A206,A207,A208,A220,XBOOLE_0:def 3;
then A227: p = LS/.2 by TARSKI:def 1;
then A228: p..LS = 2 by A225,FINSEQ_5:44;
1+1 = Index(p,do)+(Gij..LS)-1 by A223,A226,BINARITH:def 3;
then 1+1+1 = Index(p,do)+(Gij..LS) by XCMPLX_1:27;
then A229: Gij..LS = 2 by A211,A221,JORDAN1E:10;
p in rng LS by A225,A227,PARTFUN2:4;
then p = Gij by A36,A228,A229,FINSEQ_5:10;
then Gij`1 = Ebo by A227,JORDAN1G:40;
then Gij`1 = Ga*(len Ga,j)`1 by A9,A15,JORDAN1A:92;
hence contradiction by A1,A11,A64,JORDAN1G:7;
end;
hence contradiction;
end;
then east_halfline E-max C c= (L~godo)` by SUBSET_1:43;
then consider W be Subset of TOP-REAL 2 such that
A230: W is_a_component_of (L~godo)` and
A231: east_halfline E-max C c= W by GOBOARD9:5;
east_halfline E-max C is not Bounded by JORDAN1C:9;
then W is not Bounded by A231,JORDAN2C:16;
then W is_outside_component_of L~godo by A230,JORDAN2C:def 4;
then W c= UBD L~godo by JORDAN2C:27;
then A232: east_halfline E-max C c= UBD L~godo by A231,XBOOLE_1:1;
E-max C in east_halfline E-max C by JORDAN1C:7;
then E-max C in UBD L~godo by A232;
then E-max C in LeftComp godo by GOBRD14:46;
then UA meets L~godo by A124,A125,A144,JORDAN1J:36;
then A233: UA meets (L~go \/ L~pion1) or UA meets L~do by A137,XBOOLE_1:70;
A234: UA c= C by JORDAN1A:16;
per cases by A233,XBOOLE_1:70;
suppose UA meets L~go;
then UA meets L~Cage(C,n) by A139,XBOOLE_1:63;
then C meets L~Cage(C,n) by A234,XBOOLE_1:63;
hence contradiction by JORDAN10:5;
suppose UA meets L~pion1;
hence contradiction by A5,A79,A141;
suppose UA meets L~do;
then UA meets L~Cage(C,n) by A139,XBOOLE_1:63;
then C meets L~Cage(C,n) by A234,XBOOLE_1:63;
hence contradiction by JORDAN10:5;
end;
theorem Th14:
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= k & k <= j & j <= width Gauge(C,n) &
LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,k)} &
LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,j)} holds
LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) meets Lower_Arc C
proof
let C be Simple_closed_curve;
let i,j,k be Nat;
set Ga = Gauge(C,n);
set US = Upper_Seq(C,n);
set LS = Lower_Seq(C,n);
set LA = Lower_Arc C;
set Wmin = W-min L~Cage(C,n);
set Emax = E-max L~Cage(C,n);
set Wbo = W-bound L~Cage(C,n);
set Ebo = E-bound L~Cage(C,n);
set Gik = Ga*(i,k);
set Gij = Ga*(i,j);
assume that
A1: 1 < i & i < len Ga and
A2: 1 <= k & k <= j & j <= width Ga and
A3: LSeg(Gik,Gij) /\ L~US = {Gik} and
A4: LSeg(Gik,Gij) /\ L~LS = {Gij} and
A5: LSeg(Gik,Gij) misses LA;
Gij in {Gij} by TARSKI:def 1;
then A6: Gij in L~LS by A4,XBOOLE_0:def 3;
Gik in {Gik} by TARSKI:def 1;
then A7: Gik in L~US by A3,XBOOLE_0:def 3;
A8: j <> k by A1,A2,A6,A7,JORDAN1J:57;
A9: 1 <= j & j <= width Ga by A2,AXIOMS:22;
A10: 1 <= k & k <= width Ga by A2,AXIOMS:22;
A11: [i,j] in Indices Ga by A1,A9,GOBOARD7:10;
A12: [i,k] in Indices Ga by A1,A10,GOBOARD7:10;
A13: LS is_sequence_on Ga by JORDAN1G:5;
A14: US is_sequence_on Ga by JORDAN1G:4;
set do = L_Cut(LS,Gij);
set go = R_Cut(US,Gik);
A15: len Ga = width Ga by JORDAN8:def 1;
A16: len US >= 3 by JORDAN1E:19;
then len US >= 1 by AXIOMS:22;
then 1 in dom US by FINSEQ_3:27;
then A17: US.1 = US/.1 by FINSEQ_4:def 4
.= Wmin by JORDAN1F:5;
A18: Wmin`1 = Wbo by PSCOMP_1:84
.= Ga*(1,k)`1 by A10,A15,JORDAN1A:94;
len Ga >= 4 by JORDAN8:13;
then A19: len Ga >= 1 by AXIOMS:22;
then A20: [1,k] in Indices Ga by A10,GOBOARD7:10;
then A21: Gik <> US.1 by A1,A12,A17,A18,JORDAN1G:7;
then reconsider go as being_S-Seq FinSequence of TOP-REAL 2
by A7,JORDAN3:70;
A22: len LS >= 1+2 by JORDAN1E:19;
then len LS >= 1 by AXIOMS:22;
then A23: 1 in dom LS & len LS in dom LS by FINSEQ_3:27;
then A24: LS.len LS = LS/.len LS by FINSEQ_4:def 4
.= Wmin by JORDAN1F:8;
A25: Wmin`1 = Wbo by PSCOMP_1:84
.= Ga*(1,k)`1 by A10,A15,JORDAN1A:94;
A26: [i,j] in Indices Ga by A1,A9,GOBOARD7:10;
then A27: Gij <> LS.len LS by A1,A20,A24,A25,JORDAN1G:7;
then reconsider do as being_S-Seq FinSequence of TOP-REAL 2
by A6,JORDAN3:69;
A28: [len Ga,k] in Indices Ga by A10,A19,GOBOARD7:10;
A29: LS.1 = LS/.1 by A23,FINSEQ_4:def 4
.= Emax by JORDAN1F:6;
Emax`1 = Ebo by PSCOMP_1:104
.= Ga*(len Ga,k)`1 by A10,A15,JORDAN1A:92;
then A30: Gij <> LS.1 by A1,A26,A28,A29,JORDAN1G:7;
A31: len go >= 1+1 by TOPREAL1:def 10;
A32: Gik in rng US by A1,A7,A10,A14,JORDAN1J:40;
then A33: go is_sequence_on Ga by A14,JORDAN1J:38;
A34: go is s.c.c. by JGRAPH_1:16;
A35: len do >= 1+1 by TOPREAL1:def 10;
A36: Gij in rng LS by A1,A6,A9,A13,JORDAN1J:40;
then A37: do is_sequence_on Ga by A13,JORDAN1J:39;
A38: do is s.c.c. by JGRAPH_1:16;
reconsider go as non constant s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2) by A31,A33,A34,JORDAN8:8;
reconsider do as non constant s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2) by A35,A37,A38,JORDAN8:8;
A39: len go > 1 by A31,NAT_1:38;
then A40: len go in dom go by FINSEQ_3:27;
then A41: go/.len go = go.len go by FINSEQ_4:def 4
.= Gik by A7,JORDAN3:59;
len do >= 1 by A35,AXIOMS:22;
then 1 in dom do by FINSEQ_3:27;
then A42: do/.1 = do.1 by FINSEQ_4:def 4
.= Gij by A6,JORDAN3:58;
reconsider m = len go - 1 as Nat by A40,FINSEQ_3:28;
A43: m+1 = len go by XCMPLX_1:27;
then A44: len go-'1 = m by BINARITH:39;
A45: LSeg(go,m) c= L~go by TOPREAL3:26;
A46: L~go c= L~US by A7,JORDAN3:76;
then LSeg(go,m) c= L~US by A45,XBOOLE_1:1;
then A47: LSeg(go,m) /\ LSeg(Gik,Gij) c= {Gik} by A3,XBOOLE_1:26;
m >= 1 by A31,REAL_1:84;
then A48: LSeg(go,m) = LSeg(go/.m,Gik) by A41,A43,TOPREAL1:def 5;
{Gik} c= LSeg(go,m) /\ LSeg(Gik,Gij)
proof
let x be set;
assume x in {Gik};
then A49: x = Gik by TARSKI:def 1;
A50: Gik in LSeg(go,m) by A48,TOPREAL1:6;
Gik in LSeg(Gik,Gij) by TOPREAL1:6;
hence x in LSeg(go,m) /\ LSeg(Gik,Gij) by A49,A50,XBOOLE_0:def 3;
end;
then A51: LSeg(go,m) /\ LSeg(Gik,Gij) = {Gik} by A47,XBOOLE_0:def 10;
A52: LSeg(do,1) c= L~do by TOPREAL3:26;
A53: L~do c= L~LS by A6,JORDAN3:77;
then LSeg(do,1) c= L~LS by A52,XBOOLE_1:1;
then A54: LSeg(do,1) /\ LSeg(Gik,Gij) c= {Gij} by A4,XBOOLE_1:26;
A55: LSeg(do,1) = LSeg(Gij,do/.(1+1)) by A35,A42,TOPREAL1:def 5;
{Gij} c= LSeg(do,1) /\ LSeg(Gik,Gij)
proof
let x be set;
assume x in {Gij};
then A56: x = Gij by TARSKI:def 1;
A57: Gij in LSeg(do,1) by A55,TOPREAL1:6;
Gij in LSeg(Gik,Gij) by TOPREAL1:6;
hence x in LSeg(do,1) /\ LSeg(Gik,Gij) by A56,A57,XBOOLE_0:def 3;
end;
then A58: LSeg(Gik,Gij) /\ LSeg(do,1) = {Gij} by A54,XBOOLE_0:def 10;
A59: go/.1 = US/.1 by A7,SPRECT_3:39
.= Wmin by JORDAN1F:5;
then A60: go/.1 = LS/.len LS by JORDAN1F:8
.= do/.len do by A6,JORDAN1J:35;
A61: rng go c= L~go & rng do c= L~do by A31,A35,SPPOL_2:18;
A62: {go/.1} c= L~go /\ L~do
proof
let x be set;
assume x in {go/.1};
then x = go/.1 by TARSKI:def 1;
then x in rng go & x in rng do by A60,FINSEQ_6:46,REVROT_1:3;
hence x in L~go /\ L~do by A61,XBOOLE_0:def 3;
end;
A63: LS.1 = LS/.1 by A23,FINSEQ_4:def 4
.= Emax by JORDAN1F:6;
A64: [len Ga,j] in Indices Ga by A9,A19,GOBOARD7:10;
L~go /\ L~do c= {go/.1}
proof
let x be set;
assume x in L~go /\ L~do;
then A65: x in L~go & x in L~do by XBOOLE_0:def 3;
then x in L~US /\ L~LS by A46,A53,XBOOLE_0:def 3;
then x in {Wmin,Emax} by JORDAN1E:20;
then A66: x = Wmin or x = Emax by TARSKI:def 2;
now assume x = Emax;
then A67: Emax = Gij by A6,A63,A65,JORDAN1E:11;
Ga*(len Ga,j)`1 = Ebo by A9,A15,JORDAN1A:92;
then Emax`1 <> Ebo by A1,A11,A64,A67,JORDAN1G:7;
hence contradiction by PSCOMP_1:104;
end;
hence x in {go/.1} by A59,A66,TARSKI:def 1;
end;
then A68: L~go /\ L~do = {go/.1} by A62,XBOOLE_0:def 10;
set W2 = go/.2;
A69: 2 in dom go by A31,FINSEQ_3:27;
A70: Gik..US >= 1 by A32,FINSEQ_4:31;
A71: now assume Gik`1 = Wbo;
then Ga*(1,k)`1 = Ga*(i,k)`1 by A10,A15,JORDAN1A:94;
hence contradiction by A1,A12,A20,JORDAN1G:7;
end;
go = mid(US,1,Gik..US) by A32,JORDAN1G:57
.= US|(Gik..US) by A70,JORDAN3:25;
then A72: W2 = US/.2 by A69,TOPREAL1:1;
A73: Wmin in rng go by A59,FINSEQ_6:46;
set pion = <*Gik,Gij*>;
A74: now let n be Nat;
assume n in dom pion;
then n in Seg 2 by FINSEQ_3:29;
then n = 1 or n = 2 by FINSEQ_1:4,TARSKI:def 2;
then pion/.n = Gik or pion/.n = Gij by FINSEQ_4:26;
hence ex i,j be Nat st [i,j] in Indices Ga & pion/.n = Ga*(i,j)
by A11,A12;
end;
A75: Gik <> Gij by A8,A11,A12,GOBOARD1:21;
A76: Gik`1 = Ga*(i,1)`1 by A1,A10,GOBOARD5:3
.= Gij`1 by A1,A9,GOBOARD5:3;
then LSeg(Gik,Gij) is vertical by SPPOL_1:37;
then pion is_S-Seq by A75,JORDAN1B:8;
then consider pion1 be FinSequence of TOP-REAL 2 such that
A77: pion1 is_sequence_on Ga and
A78: pion1 is_S-Seq and
A79: L~pion = L~pion1 and
A80: pion/.1 = pion1/.1 and
A81: pion/.len pion = pion1/.len pion1 and
A82: len pion <= len pion1 by A74,GOBOARD3:2;
reconsider pion1 as being_S-Seq FinSequence of TOP-REAL 2 by A78;
set godo = go^'pion1^'do;
len Cage(C,n) > 4 by GOBOARD7:36;
then A83: 1+1 <= len Cage(C,n) by AXIOMS:22;
then A84: 1+1 <= len Rotate(Cage(C,n),Wmin) by REVROT_1:14;
len (go^'pion1) >= len go by TOPREAL8:7;
then A85: len (go^'pion1) >= 1+1 by A31,AXIOMS:22;
then A86: len (go^'pion1) > 1+0 by NAT_1:38;
len godo >= len (go^'pion1) by TOPREAL8:7;
then A87: 1+1 <= len godo by A85,AXIOMS:22;
A88: US is_sequence_on Ga by JORDAN1G:4;
A89: go/.len go = pion1/.1 by A41,A80,FINSEQ_4:26;
then A90: go^'pion1 is_sequence_on Ga by A33,A77,TOPREAL8:12;
A91: (go^'pion1)/.len (go^'pion1) = pion/.len pion by A81,AMISTD_1:6
.= pion/.2 by FINSEQ_1:61
.= do/.1 by A42,FINSEQ_4:26;
then A92: godo is_sequence_on Ga by A37,A90,TOPREAL8:12;
then A93: godo is standard special by JORDAN8:7;
A94: godo is non constant by A87,A92,JORDAN8:8;
LSeg(pion1,1) c= L~<*Gik,Gij*> by A79,TOPREAL3:26;
then LSeg(pion1,1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then A95: LSeg(go,len go-'1) /\ LSeg(pion1,1) c= {Gik}
by A44,A51,XBOOLE_1:27;
A96: len pion1 >= 1+1 by A82,FINSEQ_1:61;
{Gik} c= LSeg(go,m) /\ LSeg(pion1,1)
proof
let x be set;
assume x in {Gik};
then A97: x = Gik by TARSKI:def 1;
A98: Gik in LSeg(go,m) by A48,TOPREAL1:6;
Gik in LSeg(pion1,1) by A41,A89,A96,TOPREAL1:27;
hence x in LSeg(go,m) /\ LSeg(pion1,1) by A97,A98,XBOOLE_0:def 3;
end;
then LSeg(go,len go-'1) /\ LSeg(pion1,1) = { go/.len go }
by A41,A44,A95,XBOOLE_0:def 10;
then A99: go^'pion1 is unfolded by A89,TOPREAL8:34;
len pion1 >= 2+0 by A82,FINSEQ_1:61;
then A100: len pion1-2 >= 0 by REAL_1:84;
A101: len (go^'pion1)-1 >= 0 by A86,REAL_1:84;
len (go^'pion1)+1-1 = len go+len pion1-1 by GRAPH_2:13;
then len (go^'pion1)-1 = len go+len pion1-1-1 by XCMPLX_1:26
.= len go + len pion1-(1+1) by XCMPLX_1:36
.= len go + (len pion1-2) by XCMPLX_1:29
.= len go + (len pion1-'2) by A100,BINARITH:def 3;
then A102: len (go^'pion1)-'1 = len go + (len pion1-'2)
by A101,BINARITH:def 3;
A103: len pion1-1 >= 1 by A96,REAL_1:84;
then len pion1-1 >= 0 by AXIOMS:22;
then A104: len pion1-'1 = len pion1-1 by BINARITH:def 3;
A105: len pion1-'2+1 = len pion1-2+1 by A100,BINARITH:def 3
.= len pion1-(2-1) by XCMPLX_1:37
.= len pion1-'1 by A104;
len pion1-1+1 <= len pion1 by XCMPLX_1:27;
then A106: len pion1-'1 < len pion1 by A104,NAT_1:38;
LSeg(pion1,len pion1-'1) c= L~<*Gik,Gij*> by A79,TOPREAL3:26;
then LSeg(pion1,len pion1-'1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then A107: LSeg(pion1,len pion1-'1) /\ LSeg(do,1) c= {Gij}
by A58,XBOOLE_1:27;
{Gij} c= LSeg(pion1,len pion1-'1) /\ LSeg(do,1)
proof
let x be set;
assume x in {Gij};
then A108: x = Gij by TARSKI:def 1;
A109: Gij in LSeg(do,1) by A55,TOPREAL1:6;
A110: len pion1-'1+1 = len pion1 by A104,XCMPLX_1:27;
then pion1/.(len pion1-'1+1) = pion/.2 by A81,FINSEQ_1:61
.= Gij by FINSEQ_4:26;
then Gij in LSeg(pion1,len pion1-'1) by A103,A104,A110,TOPREAL1:27;
hence x in LSeg(pion1,len pion1-'1) /\ LSeg(do,1)
by A108,A109,XBOOLE_0:def 3;
end;
then LSeg(pion1,len pion1-'1) /\ LSeg(do,1) = {Gij}
by A107,XBOOLE_0:def 10;
then LSeg(go^'pion1,len go+(len pion1-'2)) /\ LSeg(do,1) =
{(go^'pion1)/.len (go^'pion1)} by A42,A89,A91,A105,A106,TOPREAL8:31;
then A111: godo is unfolded by A91,A99,A102,TOPREAL8:34;
A112: (go^'pion1) is non trivial by A85,SPPOL_1:2;
A113: rng pion1 c= L~pion1 by A96,SPPOL_2:18;
A114: {pion1/.1} c= L~go /\ L~pion1
proof
let x be set;
assume x in {pion1/.1};
then x = pion1/.1 by TARSKI:def 1;
then x in rng go & x in rng pion1 by A89,FINSEQ_6:46,REVROT_1:3;
hence x in L~go /\ L~pion1 by A61,A113,XBOOLE_0:def 3;
end;
L~go /\ L~pion1 c= {pion1/.1}
proof
let x be set;
assume x in L~go /\ L~pion1;
then x in L~go & x in L~pion1 by XBOOLE_0:def 3;
then x in L~pion1 /\ L~US by A46,XBOOLE_0:def 3;
hence x in {pion1/.1} by A3,A41,A79,A89,SPPOL_2:21;
end;
then A115: L~go /\ L~pion1 = {pion1/.1} by A114,XBOOLE_0:def 10;
then A116: (go^'pion1) is s.n.c. by A89,JORDAN1J:54;
rng go /\ rng pion1 c= {pion1/.1} by A61,A113,A115,XBOOLE_1:27;
then A117: go^'pion1 is one-to-one by JORDAN1J:55;
A118: pion/.len pion = pion/.2 by FINSEQ_1:61
.= do/.1 by A42,FINSEQ_4:26;
A119: {pion1/.len pion1} c= L~do /\ L~pion1
proof
let x be set;
assume x in {pion1/.len pion1};
then x = pion1/.len pion1 by TARSKI:def 1;
then x in rng do & x in rng pion1 by A81,A118,FINSEQ_6:46,REVROT_1:3;
hence x in L~do /\ L~pion1 by A61,A113,XBOOLE_0:def 3;
end;
L~do /\ L~pion1 c= {pion1/.len pion1}
proof
let x be set;
assume x in L~do /\ L~pion1;
then x in L~do & x in L~pion1 by XBOOLE_0:def 3;
then x in L~pion1 /\ L~LS by A53,XBOOLE_0:def 3;
hence x in {pion1/.len pion1} by A4,A42,A79,A81,A118,SPPOL_2:21;
end;
then A120: L~do /\ L~pion1 = {pion1/.len pion1} by A119,XBOOLE_0:def 10;
A121: L~(go^'pion1) /\ L~do = (L~go \/ L~pion1) /\ L~do by A89,TOPREAL8:35
.= {go/.1} \/ {do/.1} by A68,A81,A118,A120,XBOOLE_1:23
.= {(go^'pion1)/.1} \/ {do/.1} by AMISTD_1:5
.= {(go^'pion1)/.1,do/.1} by ENUMSET1:41;
A122: do/.len do = (go^'pion1)/.1 by A60,AMISTD_1:5;
reconsider godo as non constant standard special_circular_sequence
by A91,A93,A94,A99,A111,A112,A116,A117,A121,A122,TOPREAL8:11,33;
A123: LA is_an_arc_of E-max C,W-min C by JORDAN6:def 9;
then A124: LA is connected by JORDAN6:11;
A125: W-min C in LA & E-max C in LA by A123,TOPREAL1:4;
set ff = Rotate(Cage(C,n),Wmin);
Wmin in rng Cage(C,n) by SPRECT_2:47;
then A126: ff/.1 = Wmin by FINSEQ_6:98;
A127: L~ff = L~Cage(C,n) by REVROT_1:33;
then A128: (W-max L~ff)..ff > 1 by A126,SPRECT_5:23;
(W-max L~ff)..ff <= (N-min L~ff)..ff by A126,A127,SPRECT_5:24;
then A129: (N-min L~ff)..ff > 1 by A128,AXIOMS:22;
(N-min L~ff)..ff < (N-max L~ff)..ff by A126,A127,SPRECT_5:25;
then A130: (N-max L~ff)..ff > 1 by A129,AXIOMS:22;
(N-max L~ff)..ff <= (E-max L~ff)..ff by A126,A127,SPRECT_5:26;
then A131: Emax..ff > 1 by A127,A130,AXIOMS:22;
A132: now assume A133: Gik..US <= 1;
Gik..US >= 1 by A32,FINSEQ_4:31;
then Gik..US = 1 by A133,AXIOMS:21;
then Gik = US/.1 by A32,FINSEQ_5:41;
hence contradiction by A17,A21,JORDAN1F:5;
end;
A134: Cage(C,n) is_sequence_on Ga by JORDAN9:def 1;
then A135: ff is_sequence_on Ga by REVROT_1:34;
A136: right_cell(godo,1,Ga)\L~godo c= RightComp godo by A87,A92,JORDAN9:29;
A137: L~godo = L~(go^'pion1) \/ L~do by A91,TOPREAL8:35
.= L~go \/ L~pion1 \/ L~do by A89,TOPREAL8:35;
L~Cage(C,n) = L~US \/ L~LS by JORDAN1E:17;
then A138: L~US c= L~Cage(C,n) & L~LS c= L~Cage(C,n) by XBOOLE_1:7;
then A139: L~go c= L~Cage(C,n) & L~do c= L~Cage(C,n)
by A46,A53,XBOOLE_1:1;
A140: W-min C in C by SPRECT_1:15;
A141: L~pion = LSeg(Gik,Gij) by SPPOL_2:21;
A142: now assume W-min C in L~godo;
then W-min C in L~go \/ L~pion1 or W-min C in L~do by A137,XBOOLE_0:def 2;
then A143: W-min C in L~go or W-min C in L~pion1 or W-min C in L~do
by XBOOLE_0:def 2;
per cases by A143;
suppose W-min C in L~go;
then C meets L~Cage(C,n) by A139,A140,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
suppose W-min C in L~pion1;
hence contradiction by A5,A79,A125,A141,XBOOLE_0:3;
suppose W-min C in L~do;
then C meets L~Cage(C,n) by A139,A140,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
end;
right_cell(Rotate(Cage(C,n),Wmin),1) =
right_cell(ff,1,GoB ff) by A84,JORDAN1H:29
.= right_cell(ff,1,GoB Cage(C,n)) by REVROT_1:28
.= right_cell(ff,1,Ga) by JORDAN1H:52
.= right_cell(ff-:Emax,1,Ga) by A131,A135,JORDAN1J:53
.= right_cell(US,1,Ga) by JORDAN1E:def 1
.= right_cell(R_Cut(US,Gik),1,Ga) by A32,A88,A132,JORDAN1J:52
.= right_cell(go^'pion1,1,Ga) by A39,A90,JORDAN1J:51
.= right_cell(godo,1,Ga) by A86,A92,JORDAN1J:51;
then W-min C in right_cell(godo,1,Ga) by JORDAN1I:8;
then W-min C in right_cell(godo,1,Ga)\L~godo by A142,XBOOLE_0:def 4;
then A144: W-min C in RightComp godo by A136;
A145: godo/.1 = (go^'pion1)/.1 by AMISTD_1:5
.= Wmin by A59,AMISTD_1:5;
A146: len US >= 2 by A16,AXIOMS:22;
A147: godo/.2 = (go^'pion1)/.2 by A85,AMISTD_1:9
.= US/.2 by A31,A72,AMISTD_1:9
.= (US^'LS)/.2 by A146,AMISTD_1:9
.= Rotate(Cage(C,n),Wmin)/.2 by JORDAN1E:15;
A148: L~godo = L~go \/ L~pion1 \/ L~do by A137;
A149: L~go \/ L~do is compact by COMPTS_1:19;
A150: L~go \/ L~do c= L~Cage(C,n) by A139,XBOOLE_1:8;
A151: Wmin in L~go by A61,A73;
Wmin in L~go \/ L~do by A151,XBOOLE_0:def 2;
then A152: W-min (L~go \/ L~do) = Wmin by A149,A150,JORDAN1J:21;
A153: (W-min (L~go \/ L~do))`1 = W-bound (L~go \/ L~do) & Wmin`1 = Wbo
by PSCOMP_1:84;
W-bound LSeg(Gik,Gij) = Gik`1 by A76,SPRECT_1:62;
then A154: W-bound L~pion1 = Gik`1 by A79,SPPOL_2:21;
Gik`1 >= Wbo by A7,A138,PSCOMP_1:71;
then Gik`1 > Wbo by A71,REAL_1:def 5;
then W-min (L~go\/L~do\/L~pion1) = W-min (L~go \/ L~do)
by A149,A152,A153,A154,JORDAN1J:
33;
then A155: W-min L~godo = Wmin by A148,A152,XBOOLE_1:4;
A156: rng godo c= L~godo by A87,SPPOL_2:18;
2 in dom godo by A87,FINSEQ_3:27;
then godo/.2 in rng godo by PARTFUN2:4;
then A157: godo/.2 in L~godo by A156;
godo/.2 in W-most L~Cage(C,n) by A147,JORDAN1I:27;
then (godo/.2)`1 = (W-min L~godo)`1 by A155,PSCOMP_1:88
.= W-bound L~godo by PSCOMP_1:84;
then godo/.2 in W-most L~godo by A157,SPRECT_2:16;
then Rotate(godo,W-min L~godo)/.2 in W-most L~godo by A145,A155,FINSEQ_6:95
;
then reconsider godo as clockwise_oriented non constant standard
special_circular_sequence by JORDAN1I:27;
len US in dom US by FINSEQ_5:6;
then A158: US.len US = US/.len US by FINSEQ_4:def 4
.= Emax by JORDAN1F:7;
A159: E-max C in E-most C by PSCOMP_1:111;
A160: east_halfline E-max C misses L~go
proof
assume east_halfline E-max C meets L~go;
then consider p be set such that
A161: p in east_halfline E-max C and
A162: p in L~go by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A161;
A163: p in L~US by A46,A162;
then p in east_halfline E-max C /\ L~Cage(C,n) by A138,A161,XBOOLE_0:def 3
;
then A164: p`1 = Ebo by A159,JORDAN1A:104;
then A165: p = Emax by A163,JORDAN1J:46;
then Emax = Gik by A7,A158,A162,JORDAN1J:43;
then Gik`1 = Ga*(len Ga,k)`1 by A10,A15,A164,A165,JORDAN1A:92;
hence contradiction by A1,A12,A28,JORDAN1G:7;
end;
now assume east_halfline E-max C meets L~godo;
then A166: east_halfline E-max C meets (L~go \/ L~pion1) or
east_halfline E-max C meets L~do by A137,XBOOLE_1:70;
per cases by A166,XBOOLE_1:70;
suppose east_halfline E-max C meets L~go;
hence contradiction by A160;
suppose east_halfline E-max C meets L~pion1;
then consider p be set such that
A167: p in east_halfline E-max C and
A168: p in L~pion1 by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A167;
A169: p`1 = Gik`1 by A76,A79,A141,A168,GOBOARD7:5;
i+1 <= len Ga by A1,NAT_1:38;
then i+1-1 <= len Ga-1 by REAL_1:49;
then A170: i <= len Ga-1 by XCMPLX_1:26;
then len Ga-1 > 0 by A1,AXIOMS:22;
then A171: i <= len Ga-'1 by A170,BINARITH:def 3;
len Ga-'1 <= len Ga by GOBOARD9:2;
then p`1 <= Ga*(len Ga-'1,1)`1 by A1,A10,A15,A19,A169,A171,JORDAN1A:39;
then p`1 <= E-bound C by A19,JORDAN8:15;
then A172: p`1 <= (E-max C)`1 by PSCOMP_1:104;
p`1 >= (E-max C)`1 by A167,JORDAN1A:def 3;
then A173: p`1 = (E-max C)`1 by A172,AXIOMS:21;
p`2 = (E-max C)`2 by A167,JORDAN1A:def 3;
then p = E-max C by A173,TOPREAL3:11;
hence contradiction by A5,A79,A125,A141,A168,XBOOLE_0:3;
suppose east_halfline E-max C meets L~do;
then consider p be set such that
A174: p in east_halfline E-max C and
A175: p in L~do by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A174;
p in L~LS by A53,A175;
then p in east_halfline E-max C /\ L~Cage(C,n)
by A138,A174,XBOOLE_0:def 3;
then A176: p`1 = Ebo by A159,JORDAN1A:104;
A177: (E-max C)`2 = p`2 by A174,JORDAN1A:def 3;
set RC = Rotate(Cage(C,n),Emax);
A178: E-max C in right_cell(RC,1) by JORDAN1I:9;
A179: 1+1 <= len LS by A22,AXIOMS:22;
LS = RC-:Wmin by JORDAN1G:26;
then A180: LSeg(LS,1) = LSeg(RC,1) by A179,SPPOL_2:9;
A181: L~RC = L~Cage(C,n) by REVROT_1:33;
A182: len RC = len Cage(C,n) by REVROT_1:14;
A183: GoB RC = GoB Cage(C,n) by REVROT_1:28
.= Ga by JORDAN1H:52;
A184: Emax in rng Cage(C,n) by SPRECT_2:50;
A185: RC is_sequence_on Ga by A134,REVROT_1:34;
A186: RC/.1 = E-max L~RC by A181,A184,FINSEQ_6:98;
then consider ii,jj be Nat such that
A187: [ii,jj+1] in Indices Ga and
A188: [ii,jj] in Indices Ga and
A189: RC/.1 = Ga*(ii,jj+1) and
A190: RC/.(1+1) = Ga*(ii,jj) by A83,A182,A185,JORDAN1I:25;
consider jj2 be Nat such that
A191: 1 <= jj2 & jj2 <= width Ga and
A192: Emax = Ga*(len Ga,jj2) by JORDAN1D:29;
A193: len Ga >= 4 by JORDAN8:13;
then len Ga >= 1 by AXIOMS:22;
then [len Ga,jj2] in Indices Ga by A191,GOBOARD7:10;
then A194: ii = len Ga by A181,A186,A187,A189,A192,GOBOARD1:21;
A195: 1 <= ii & ii <= len Ga & 1 <= jj+1 & jj+1 <= width Ga
by A187,GOBOARD5:1;
A196: 1 <= ii & ii <= len Ga & 1 <= jj & jj <= width Ga
by A188,GOBOARD5:1;
A197: ii+1 <> ii by NAT_1:38;
jj+1 > jj by NAT_1:38;
then jj+1+1 <> jj by NAT_1:38;
then A198: right_cell(RC,1) = cell(Ga,ii-'1,jj)
by A83,A182,A183,A187,A188,A189,A190,A197,GOBOARD5:
def 6;
A199: ii-'1+1 = ii by A195,AMI_5:4;
ii-1 >= 4-1 by A193,A194,REAL_1:49;
then A200: ii-1 >= 1 by AXIOMS:22;
then ii-1 >= 0 by AXIOMS:22;
then A201: 1 <= ii-'1 by A200,BINARITH:def 3;
then A202: Ga*(ii-'1,jj)`2 <= p`2 & p`2 <= Ga*(ii-'1,jj+1)`2
by A177,A178,A195,A196,A198,A199,JORDAN9:19;
A203: ii-'1 < len Ga by A195,A199,NAT_1:38;
then A204: Ga*(ii-'1,jj)`2 = Ga*(1,jj)`2 by A196,A201,GOBOARD5:2
.= Ga*(ii,jj)`2 by A196,GOBOARD5:2;
A205: Ga*(ii-'1,jj+1)`2 = Ga*(1,jj+1)`2 by A195,A201,A203,GOBOARD5:2
.= Ga*(ii,jj+1)`2 by A195,GOBOARD5:2;
Ga*(len Ga,jj)`1 = Ebo & Ebo = Ga*(len Ga,jj+1)`1
by A15,A195,A196,JORDAN1A:92;
then p in LSeg(RC/.1,RC/.(1+1))
by A176,A189,A190,A194,A202,A204,A205,GOBOARD7:8;
then A206: p in LSeg(LS,1) by A83,A180,A182,TOPREAL1:def 5;
A207: p in LSeg(do,Index(p,do)) by A175,JORDAN3:42;
A208: do = mid(LS,Gij..LS,len LS) by A36,JORDAN1J:37;
A209: 1<=Gij..LS & Gij..LS<=len LS by A36,FINSEQ_4:31;
Gij..LS <> len LS by A27,A36,FINSEQ_4:29;
then A210: Gij..LS < len LS by A209,REAL_1:def 5;
A211: 1<=Index(p,do) & Index(p,do) < len do by A175,JORDAN3:41;
A212: Index(Gij,LS)+1 = Gij..LS by A30,A36,JORDAN1J:56;
consider t be Nat such that
A213: t in dom LS and
A214: LS.t = Gij by A36,FINSEQ_2:11;
A215: 1 <= t & t <= len LS by A213,FINSEQ_3:27;
1 < t by A30,A214,A215,REAL_1:def 5;
then Index(Gij,LS)+1 = t by A214,A215,JORDAN3:45;
then A216: len L_Cut(LS,Gij) = len LS-Index(Gij,LS)
by A6,A27,A214,JORDAN3:61;
set tt = Index(p,do)+(Gij..LS)-'1;
A217: 1<=Index(Gij,LS) & 0+Index(Gij,LS) < len LS by A6,JORDAN3:41;
then A218: len LS-Index(Gij,LS) > 0 by REAL_1:86;
then Index(p,do) < len LS-'Index(Gij,LS) by A211,A216,BINARITH:def 3;
then Index(p,do)+1 <= len LS-'Index(Gij,LS) by NAT_1:38;
then Index(p,do) <= len LS-'Index(Gij,LS)-1 by REAL_1:84;
then Index(p,do) <= len LS-Index(Gij,LS)-1 by A218,BINARITH:def 3;
then A219: Index(p,do) <= len LS-Gij..LS by A212,XCMPLX_1:36;
then len LS-Gij..LS >= 1 by A211,AXIOMS:22;
then len LS-Gij..LS >= 0 by AXIOMS:22;
then Index(p,do) <= len LS-'Gij..LS by A219,BINARITH:def 3;
then Index(p,do) < len LS-'(Gij..LS)+1 by NAT_1:38;
then A220: LSeg(mid(LS,Gij..LS,len LS),Index(p,do)) =
LSeg(LS,Index(p,do)+(Gij..LS)-'1) by A209,A210,A211,JORDAN4:31;
A221: 1+1 <= Gij..LS by A212,A217,REAL_1:55;
then Index(p,do)+Gij..LS >= 1+1+1 by A211,REAL_1:55;
then A222: Index(p,do)+Gij..LS-1 >= 1+1+1-1 by REAL_1:49;
then A223: Index(p,do)+Gij..LS-1 >= 0 by AXIOMS:22;
then A224: tt >= 1+1 by A222,BINARITH:def 3;
A225: 2 in dom LS by A179,FINSEQ_3:27;
now per cases by A224,REAL_1:def 5;
suppose tt > 1+1;
then LSeg(LS,1) misses LSeg(LS,tt) by TOPREAL1:def 9;
hence contradiction by A206,A207,A208,A220,XBOOLE_0:3;
suppose A226: tt = 1+1;
then LSeg(LS,1) /\ LSeg(LS,tt) = {LS/.2} by A22,TOPREAL1:def 8;
then p in {LS/.2} by A206,A207,A208,A220,XBOOLE_0:def 3;
then A227: p = LS/.2 by TARSKI:def 1;
then A228: p..LS = 2 by A225,FINSEQ_5:44;
1+1 = Index(p,do)+(Gij..LS)-1 by A223,A226,BINARITH:def 3;
then 1+1+1 = Index(p,do)+(Gij..LS) by XCMPLX_1:27;
then A229: Gij..LS = 2 by A211,A221,JORDAN1E:10;
p in rng LS by A225,A227,PARTFUN2:4;
then p = Gij by A36,A228,A229,FINSEQ_5:10;
then Gij`1 = Ebo by A227,JORDAN1G:40;
then Gij`1 = Ga*(len Ga,j)`1 by A9,A15,JORDAN1A:92;
hence contradiction by A1,A11,A64,JORDAN1G:7;
end;
hence contradiction;
end;
then east_halfline E-max C c= (L~godo)` by SUBSET_1:43;
then consider W be Subset of TOP-REAL 2 such that
A230: W is_a_component_of (L~godo)` and
A231: east_halfline E-max C c= W by GOBOARD9:5;
east_halfline E-max C is not Bounded by JORDAN1C:9;
then W is not Bounded by A231,JORDAN2C:16;
then W is_outside_component_of L~godo by A230,JORDAN2C:def 4;
then W c= UBD L~godo by JORDAN2C:27;
then A232: east_halfline E-max C c= UBD L~godo by A231,XBOOLE_1:1;
E-max C in east_halfline E-max C by JORDAN1C:7;
then E-max C in UBD L~godo by A232;
then E-max C in LeftComp godo by GOBRD14:46;
then LA meets L~godo by A124,A125,A144,JORDAN1J:36;
then A233: LA meets (L~go \/ L~pion1) or LA meets L~do by A137,XBOOLE_1:70;
A234: LA c= C by JORDAN1A:16;
per cases by A233,XBOOLE_1:70;
suppose LA meets L~go;
then LA meets L~Cage(C,n) by A139,XBOOLE_1:63;
then C meets L~Cage(C,n) by A234,XBOOLE_1:63;
hence contradiction by JORDAN10:5;
suppose LA meets L~pion1;
hence contradiction by A5,A79,A141;
suppose LA meets L~do;
then LA meets L~Cage(C,n) by A139,XBOOLE_1:63;
then C meets L~Cage(C,n) by A234,XBOOLE_1:63;
hence contradiction by JORDAN10:5;
end;
theorem
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,k)} &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,j)} holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C
proof
let C be Simple_closed_curve;
let i,j,k be Nat;
assume that
A1: 1 < i & i < len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: n > 0 and
A4: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,k)} and
A5: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,j)};
A6: L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) by A3,JORDAN1G:64;
L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) by A3,JORDAN1G:63;
hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C
by A1,A2,A4,A5,A6,Th13;
end;
theorem
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,k)} &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,j)} holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C
proof
let C be Simple_closed_curve;
let i,j,k be Nat;
assume that
A1: 1 < i & i < len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: n > 0 and
A4: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,k)} and
A5: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,j)};
A6: L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) by A3,JORDAN1G:64;
L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) by A3,JORDAN1G:63;
hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C
by A1,A2,A4,A5,A6,Th14;
end;
theorem Th17:
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,k) in L~Lower_Seq(C,n) &
Gauge(C,n)*(i,j) in L~Upper_Seq(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C
proof
let C be Simple_closed_curve;
let i,j,k be Nat;
assume that
A1: 1 < i & i < len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: Gauge(C,n)*(i,k) in L~Lower_Seq(C,n) and
A4: Gauge(C,n)*(i,j) in L~Upper_Seq(C,n);
consider j1,k1 be Nat such that
A5: j <= j1 and
A6: j1 <= k1 and
A7: k1 <= k and
A8: LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,j1)} and
A9: LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,k1)} by A1,A2,A3,A4,JORDAN15:19;
A10: 1 <= j1 & k1 <= width Gauge(C,n) by A2,A5,A7,AXIOMS:22;
A11: LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) meets Upper_Arc C
by A1,A6,A8,A9,A10,Th13;
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) c=
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) by A1,A2,A5,A6,A7,JORDAN15:7;
hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C
by A11,XBOOLE_1:63;
end;
theorem Th18:
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,k) in L~Lower_Seq(C,n) &
Gauge(C,n)*(i,j) in L~Upper_Seq(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C
proof
let C be Simple_closed_curve;
let i,j,k be Nat;
assume that
A1: 1 < i & i < len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: Gauge(C,n)*(i,k) in L~Lower_Seq(C,n) and
A4: Gauge(C,n)*(i,j) in L~Upper_Seq(C,n);
consider j1,k1 be Nat such that
A5: j <= j1 and
A6: j1 <= k1 and
A7: k1 <= k and
A8: LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,j1)} and
A9: LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,k1)} by A1,A2,A3,A4,JORDAN15:19;
A10: 1 <= j1 & k1 <= width Gauge(C,n) by A2,A5,A7,AXIOMS:22;
A11: LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) meets Lower_Arc C
by A1,A6,A8,A9,A10,Th14;
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) c=
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) by A1,A2,A5,A6,A7,JORDAN15:7;
hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C
by A11,XBOOLE_1:63;
end;
theorem Th19:
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 &
Gauge(C,n)*(i,k) in Lower_Arc L~Cage(C,n) &
Gauge(C,n)*(i,j) in Upper_Arc L~Cage(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C
proof
let C be Simple_closed_curve;
let i,j,k be Nat;
assume that
A1: 1 < i & i < len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: n > 0 and
A4: Gauge(C,n)*(i,k) in Lower_Arc L~Cage(C,n) and
A5: Gauge(C,n)*(i,j) in Upper_Arc L~Cage(C,n);
A6: L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) by A3,JORDAN1G:64;
L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) by A3,JORDAN1G:63;
hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C
by A1,A2,A4,A5,A6,Th17;
end;
theorem Th20:
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 &
Gauge(C,n)*(i,k) in Lower_Arc L~Cage(C,n) &
Gauge(C,n)*(i,j) in Upper_Arc L~Cage(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C
proof
let C be Simple_closed_curve;
let i,j,k be Nat;
assume that
A1: 1 < i & i < len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: n > 0 and
A4: Gauge(C,n)*(i,k) in Lower_Arc L~Cage(C,n) and
A5: Gauge(C,n)*(i,j) in Upper_Arc L~Cage(C,n);
A6: L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) by A3,JORDAN1G:64;
L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) by A3,JORDAN1G:63;
hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C
by A1,A2,A4,A5,A6,Th18;
end;
theorem Th21:
for C be Simple_closed_curve
for i1,i2,j,k be Nat st
1 < i1 & i1 <= i2 & i2 < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i1,j)} &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i2,k)} holds
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Upper_Arc C
proof
let C be Simple_closed_curve;
let i1,i2,j,k be Nat;
set G = Gauge(C,n);
set pio = LSeg(G*(i1,j),G*(i1,k));
set poz = LSeg(G*(i1,k),G*(i2,k));
set US = Upper_Seq(C,n);
set LS = Lower_Seq(C,n);
assume that
A1: 1 < i1 & i1 <= i2 & i2 < len G and
A2: 1 <= j & j <= k & k <= width G and
A3: (pio \/ poz) /\ L~US = {G*(i1,j)} and
A4: (pio \/ poz) /\ L~LS = {G*(i2,k)} and
A5: (pio \/ poz) misses Upper_Arc C;
set UA = Upper_Arc C;
set Wmin = W-min L~Cage(C,n);
set Emax = E-max L~Cage(C,n);
set Wbo = W-bound L~Cage(C,n);
set Ebo = E-bound L~Cage(C,n);
set Gik = G*(i2,k);
set Gij = G*(i1,j);
set Gi1k = G*(i1,k);
A6: 1 < i1 & i1 < len G & 1 < i2 & i2 < len G by A1,AXIOMS:22;
A7: L~<*Gij,Gi1k,Gik*> = poz \/ pio by TOPREAL3:23;
Gik in {Gik} by TARSKI:def 1;
then A8: Gik in L~LS by A4,XBOOLE_0:def 3;
Gij in {Gij} by TARSKI:def 1;
then A9: Gij in L~US by A3,XBOOLE_0:def 3;
A10: 1 <= j & j <= width G by A2,AXIOMS:22;
A11: 1 <= k & k <= width G by A2,AXIOMS:22;
A12: [i1,j] in Indices G by A6,A10,GOBOARD7:10;
A13: [i2,k] in Indices G by A6,A11,GOBOARD7:10;
A14: [i1,k] in Indices G by A6,A11,GOBOARD7:10;
A15: US is_sequence_on G by JORDAN1G:4;
A16: LS is_sequence_on G by JORDAN1G:5;
set go = R_Cut(US,Gij);
set do = L_Cut(LS,Gik);
A17: len G = width G by JORDAN8:def 1;
A18: len US >= 3 by JORDAN1E:19;
then len US >= 1 by AXIOMS:22;
then 1 in dom US by FINSEQ_3:27;
then A19: US.1 = US/.1 by FINSEQ_4:def 4
.= Wmin by JORDAN1F:5;
A20: Wmin`1 = Wbo by PSCOMP_1:84
.= G*(1,k)`1 by A11,A17,JORDAN1A:94;
len G >= 4 by JORDAN8:13;
then A21: len G >= 1 by AXIOMS:22;
then A22: [1,k] in Indices G by A11,GOBOARD7:10;
then A23: Gij <> US.1 by A6,A12,A19,A20,JORDAN1G:7;
then reconsider go as being_S-Seq FinSequence of TOP-REAL 2
by A9,JORDAN3:70;
A24: [1,j] in Indices G by A10,A21,GOBOARD7:10;
A25: len LS >= 1+2 by JORDAN1E:19;
then len LS >= 1 by AXIOMS:22;
then A26: 1 in dom LS & len LS in dom LS by FINSEQ_3:27;
then A27: LS.len LS = LS/.len LS by FINSEQ_4:def 4
.= Wmin by JORDAN1F:8;
A28: Wmin`1 = Wbo by PSCOMP_1:84
.= G*(1,k)`1 by A11,A17,JORDAN1A:94;
A29: Gik <> LS.len LS by A6,A13,A22,A27,A28,JORDAN1G:7;
then reconsider do as being_S-Seq FinSequence of TOP-REAL 2
by A8,JORDAN3:69;
A30: [len G,k] in Indices G by A11,A21,GOBOARD7:10;
A31: LS.1 = LS/.1 by A26,FINSEQ_4:def 4
.= Emax by JORDAN1F:6;
Emax`1 = Ebo by PSCOMP_1:104
.= G*(len G,k)`1 by A11,A17,JORDAN1A:92;
then A32: Gik <> LS.1 by A6,A13,A30,A31,JORDAN1G:7;
A33: len go >= 1+1 by TOPREAL1:def 10;
A34: Gij in rng US by A6,A9,A10,A15,JORDAN1J:40;
then A35: go is_sequence_on G by A15,JORDAN1J:38;
A36: go is s.c.c. by JGRAPH_1:16;
A37: len do >= 1+1 by TOPREAL1:def 10;
A38: Gik in rng LS by A6,A8,A11,A16,JORDAN1J:40;
then A39: do is_sequence_on G by A16,JORDAN1J:39;
A40: do is s.c.c. by JGRAPH_1:16;
reconsider go as non constant s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2) by A33,A35,A36,JORDAN8:8;
reconsider do as non constant s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2) by A37,A39,A40,JORDAN8:8;
A41: len go > 1 by A33,NAT_1:38;
then A42: len go in dom go by FINSEQ_3:27;
then A43: go/.len go = go.len go by FINSEQ_4:def 4
.= Gij by A9,JORDAN3:59;
len do >= 1 by A37,AXIOMS:22;
then 1 in dom do by FINSEQ_3:27;
then A44: do/.1 = do.1 by FINSEQ_4:def 4
.= Gik by A8,JORDAN3:58;
reconsider m = len go - 1 as Nat by A42,FINSEQ_3:28;
A45: m+1 = len go by XCMPLX_1:27;
then A46: len go-'1 = m by BINARITH:39;
A47: LSeg(go,m) c= L~go by TOPREAL3:26;
A48: L~go c= L~US by A9,JORDAN3:76;
then LSeg(go,m) c= L~US by A47,XBOOLE_1:1;
then A49: LSeg(go,m) /\ L~<*Gij,Gi1k,Gik*> c= {Gij} by A3,A7,XBOOLE_1:26;
m >= 1 by A33,REAL_1:84;
then A50: LSeg(go,m) = LSeg(go/.m,Gij) by A43,A45,TOPREAL1:def 5;
{Gij} c= LSeg(go,m) /\ L~<*Gij,Gi1k,Gik*>
proof
let x be set;
assume x in {Gij};
then A51: x = Gij by TARSKI:def 1;
A52: Gij in LSeg(go,m) by A50,TOPREAL1:6;
Gij in LSeg(Gij,Gi1k) by TOPREAL1:6;
then Gij in LSeg(Gij,Gi1k) \/ LSeg(Gi1k,Gik) by XBOOLE_0:def 2;
then Gij in L~<*Gij,Gi1k,Gik*> by SPRECT_1:10;
hence x in LSeg(go,m) /\ L~<*Gij,Gi1k,Gik*> by A51,A52,XBOOLE_0:def 3;
end;
then A53: LSeg(go,m) /\ L~<*Gij,Gi1k,Gik*> = {Gij} by A49,XBOOLE_0:def 10;
A54: LSeg(do,1) c= L~do by TOPREAL3:26;
A55: L~do c= L~LS by A8,JORDAN3:77;
then LSeg(do,1) c= L~LS by A54,XBOOLE_1:1;
then A56: LSeg(do,1) /\ L~<*Gij,Gi1k,Gik*> c= {Gik} by A4,A7,XBOOLE_1:26;
A57: LSeg(do,1) = LSeg(Gik,do/.(1+1)) by A37,A44,TOPREAL1:def 5;
{Gik} c= LSeg(do,1) /\ L~<*Gij,Gi1k,Gik*>
proof
let x be set;
assume x in {Gik};
then A58: x = Gik by TARSKI:def 1;
A59: Gik in LSeg(do,1) by A57,TOPREAL1:6;
Gik in LSeg(Gi1k,Gik) by TOPREAL1:6;
then Gik in LSeg(Gij,Gi1k) \/ LSeg(Gi1k,Gik) by XBOOLE_0:def 2;
then Gik in L~<*Gij,Gi1k,Gik*> by SPRECT_1:10;
hence x in LSeg(do,1) /\ L~<*Gij,Gi1k,Gik*> by A58,A59,XBOOLE_0:def 3;
end;
then A60: L~<*Gij,Gi1k,Gik*> /\ LSeg(do,1) = {Gik} by A56,XBOOLE_0:def 10;
A61: go/.1 = US/.1 by A9,SPRECT_3:39
.= Wmin by JORDAN1F:5;
then A62: go/.1 = LS/.len LS by JORDAN1F:8
.= do/.len do by A8,JORDAN1J:35;
A63: rng go c= L~go & rng do c= L~do by A33,A37,SPPOL_2:18;
A64: {go/.1} c= L~go /\ L~do
proof
let x be set;
assume x in {go/.1};
then x = go/.1 by TARSKI:def 1;
then x in rng go & x in rng do by A62,FINSEQ_6:46,REVROT_1:3;
hence x in L~go /\ L~do by A63,XBOOLE_0:def 3;
end;
A65: LS.1 = LS/.1 by A26,FINSEQ_4:def 4
.= Emax by JORDAN1F:6;
A66: [len G,j] in Indices G by A10,A21,GOBOARD7:10;
L~go /\ L~do c= {go/.1}
proof
let x be set;
assume x in L~go /\ L~do;
then A67: x in L~go & x in L~do by XBOOLE_0:def 3;
then x in L~US /\ L~LS by A48,A55,XBOOLE_0:def 3;
then x in {Wmin,Emax} by JORDAN1E:20;
then A68: x = Wmin or x = Emax by TARSKI:def 2;
now assume x = Emax;
then A69: Emax = Gik by A8,A65,A67,JORDAN1E:11;
G*(len G,j)`1 = Ebo by A10,A17,JORDAN1A:92;
then Emax`1 <> Ebo by A6,A13,A66,A69,JORDAN1G:7;
hence contradiction by PSCOMP_1:104;
end;
hence x in {go/.1} by A61,A68,TARSKI:def 1;
end;
then A70: L~go /\ L~do = {go/.1} by A64,XBOOLE_0:def 10;
set W2 = go/.2;
A71: 2 in dom go by A33,FINSEQ_3:27;
A72: Gij..US >= 1 by A34,FINSEQ_4:31;
A73: now assume Gij`1 = Wbo;
then G*(1,j)`1 = G*(i1,j)`1 by A10,A17,JORDAN1A:94;
hence contradiction by A6,A12,A24,JORDAN1G:7;
end;
go = mid(US,1,Gij..US) by A34,JORDAN1G:57
.= US|(Gij..US) by A72,JORDAN3:25;
then A74: W2 = US/.2 by A71,TOPREAL1:1;
A75: Wmin in rng go by A61,FINSEQ_6:46;
set pion = <*Gij,Gi1k,Gik*>;
A76: now let n be Nat;
assume n in dom pion;
then n in {1,2,3} by FINSEQ_3:1,30;
then n = 1 or n = 2 or n = 3 by ENUMSET1:def 1;
then pion/.n = Gij or pion/.n = Gi1k or pion/.n = Gik by FINSEQ_4:27;
hence ex i,j be Nat st [i,j] in Indices G & pion/.n = G*(i,j)
by A12,A13,A14;
end;
A77: Gi1k`1 = G*(i1,1)`1 by A6,A11,GOBOARD5:3
.= Gij`1 by A6,A10,GOBOARD5:3;
Gi1k`2 = G*(1,k)`2 by A6,A11,GOBOARD5:2
.= Gik`2 by A6,A11,GOBOARD5:2;
then A78: Gi1k = |[Gij`1,Gik`2]| by A77,EUCLID:57;
A79: Gi1k in pio by TOPREAL1:6;
A80: Gi1k in poz by TOPREAL1:6;
now per cases;
suppose Gik`1 <> Gij`1 & Gik`2 <> Gij`2;
then pion is_S-Seq by A78,TOPREAL3:41;
then consider pion1 be FinSequence of TOP-REAL 2 such that
A81: pion1 is_sequence_on G and
A82: pion1 is_S-Seq and
A83: L~pion = L~pion1 and
A84: pion/.1 = pion1/.1 and
A85: pion/.len pion = pion1/.len pion1 and
A86: len pion <= len pion1 by A76,GOBOARD3:2;
reconsider pion1 as being_S-Seq FinSequence of TOP-REAL 2 by A82;
set godo = go^'pion1^'do;
A87: Gi1k`1 = G*(i1,1)`1 by A6,A11,GOBOARD5:3
.= Gij`1 by A6,A10,GOBOARD5:3;
A88: Gi1k`1 <= Gik`1 by A1,A11,JORDAN1A:39;
then A89: W-bound poz = Gi1k`1 by SPRECT_1:62;
A90: W-bound pio = Gij`1 by A87,SPRECT_1:62;
W-bound (poz \/ pio) = min(W-bound poz, W-bound pio) by SPRECT_1:54
.= Gij`1 by A87,A89,A90;
then A91: W-bound L~pion1 = Gij`1 by A83,TOPREAL3:23;
len Cage(C,n) > 4 by GOBOARD7:36;
then A92: 1+1 <= len Cage(C,n) by AXIOMS:22;
then A93: 1+1 <= len Rotate(Cage(C,n),Wmin) by REVROT_1:14;
len (go^'pion1) >= len go by TOPREAL8:7;
then A94: len (go^'pion1) >= 1+1 by A33,AXIOMS:22;
then A95: len (go^'pion1) > 1+0 by NAT_1:38;
len godo >= len (go^'pion1) by TOPREAL8:7;
then A96: 1+1 <= len godo by A94,AXIOMS:22;
A97: US is_sequence_on G by JORDAN1G:4;
A98: go/.len go = pion1/.1 by A43,A84,FINSEQ_4:27;
then A99: go^'pion1 is_sequence_on G by A35,A81,TOPREAL8:12;
A100: (go^'pion1)/.len (go^'pion1) = pion/.len pion by A85,AMISTD_1:6
.= pion/.3 by FINSEQ_1:62
.= do/.1 by A44,FINSEQ_4:27;
then A101: godo is_sequence_on G by A39,A99,TOPREAL8:12;
then A102: godo is standard special by JORDAN8:7;
A103: godo is non constant by A96,A101,JORDAN8:8;
LSeg(pion1,1) c= L~pion by A83,TOPREAL3:26;
then A104: LSeg(go,len go-'1) /\ LSeg(pion1,1) c={Gij}
by A46,A53,XBOOLE_1:27;
len pion1 >= 2+1 by A86,FINSEQ_1:62;
then A105: len pion1 > 1+1 by NAT_1:38;
{Gij} c= LSeg(go,m) /\ LSeg(pion1,1)
proof
let x be set;
assume x in {Gij};
then A106: x = Gij by TARSKI:def 1;
A107: Gij in LSeg(go,m) by A50,TOPREAL1:6;
Gij in LSeg(pion1,1) by A43,A98,A105,TOPREAL1:27;
hence x in LSeg(go,m) /\ LSeg(pion1,1) by A106,A107,XBOOLE_0:def 3;
end;
then LSeg(go,len go-'1) /\ LSeg(pion1,1) = { go/.len go }
by A43,A46,A104,XBOOLE_0:def 10;
then A108: go^'pion1 is unfolded by A98,TOPREAL8:34;
len pion1 >= 2+1 by A86,FINSEQ_1:62;
then len pion1 > 2+0 by NAT_1:38;
then A109: len pion1-2 >= 0 by REAL_1:84;
A110: len (go^'pion1)-1 >= 0 by A95,REAL_1:84;
len (go^'pion1)+1-1 = len go+len pion1-1 by GRAPH_2:13;
then len (go^'pion1)-1 = len go+len pion1-1-1 by XCMPLX_1:26
.= len go + len pion1-(1+1) by XCMPLX_1:36
.= len go + (len pion1-2) by XCMPLX_1:29
.= len go + (len pion1-'2) by A109,BINARITH:def 3;
then A111: len (go^'pion1)-'1 = len go + (len pion1-'2)
by A110,BINARITH:def 3;
A112: len pion1-1 >= 1 by A105,REAL_1:84;
then len pion1-1 >= 0 by AXIOMS:22;
then A113: len pion1-'1 = len pion1-1 by BINARITH:def 3;
A114: len pion1-'2+1 = len pion1-2+1 by A109,BINARITH:def 3
.= len pion1-(2-1) by XCMPLX_1:37
.= len pion1-'1 by A113;
len pion1-1+1 <= len pion1 by XCMPLX_1:27;
then A115: len pion1-'1 < len pion1 by A113,NAT_1:38;
LSeg(pion1,len pion1-'1) c= L~pion by A83,TOPREAL3:26;
then A116: LSeg(pion1,len pion1-'1) /\ LSeg(do,1) c= {Gik}
by A60,XBOOLE_1:27;
{Gik} c= LSeg(pion1,len pion1-'1) /\ LSeg(do,1)
proof
let x be set;
assume x in {Gik};
then A117: x = Gik by TARSKI:def 1;
A118: Gik in LSeg(do,1) by A57,TOPREAL1:6;
A119: len pion1-'1+1 = len pion1 by A113,XCMPLX_1:27;
then pion1/.(len pion1-'1+1) = pion/.3 by A85,FINSEQ_1:62
.= Gik by FINSEQ_4:27;
then Gik in LSeg(pion1,len pion1-'1) by A112,A113,A119,TOPREAL1:27;
hence x in LSeg(pion1,len pion1-'1) /\ LSeg(do,1)
by A117,A118,XBOOLE_0:def 3;
end;
then LSeg(pion1,len pion1-'1) /\ LSeg(do,1) = {Gik}
by A116,XBOOLE_0:def 10;
then LSeg(go^'pion1,len go+(len pion1-'2)) /\ LSeg(do,1) =
{(go^'pion1)/.len (go^'pion1)} by A44,A98,A100,A114,A115,TOPREAL8:31;
then A120: godo is unfolded by A100,A108,A111,TOPREAL8:34;
A121: (go^'pion1) is non trivial by A94,SPPOL_1:2;
A122: rng pion1 c= L~pion1 by A105,SPPOL_2:18;
A123: {pion1/.1} c= L~go /\ L~pion1
proof
let x be set;
assume x in {pion1/.1};
then x = pion1/.1 by TARSKI:def 1;
then x in rng go & x in rng pion1 by A98,FINSEQ_6:46,REVROT_1:3;
hence x in L~go /\ L~pion1 by A63,A122,XBOOLE_0:def 3;
end;
L~go /\ L~pion1 c= {pion1/.1}
proof
let x be set;
assume x in L~go /\ L~pion1;
then x in L~go & x in L~pion1 by XBOOLE_0:def 3;
hence x in {pion1/.1} by A3,A7,A43,A48,A83,A98,XBOOLE_0:def 3;
end;
then A124: L~go /\ L~pion1 = {pion1/.1} by A123,XBOOLE_0:def 10;
then A125: (go^'pion1) is s.n.c. by A98,JORDAN1J:54;
rng go /\ rng pion1 c= {pion1/.1} by A63,A122,A124,XBOOLE_1:27;
then A126: go^'pion1 is one-to-one by JORDAN1J:55;
A127: pion/.len pion = pion/.3 by FINSEQ_1:62
.= do/.1 by A44,FINSEQ_4:27;
A128: {pion1/.len pion1} c= L~do /\ L~pion1
proof
let x be set;
assume x in {pion1/.len pion1};
then x = pion1/.len pion1 by TARSKI:def 1;
then x in rng do & x in rng pion1 by A85,A127,FINSEQ_6:46,REVROT_1:3;
hence x in L~do /\ L~pion1 by A63,A122,XBOOLE_0:def 3;
end;
L~do /\ L~pion1 c= {pion1/.len pion1}
proof
let x be set;
assume x in L~do /\ L~pion1;
then x in L~do & x in L~pion1 by XBOOLE_0:def 3;
hence x in {pion1/.len pion1}
by A4,A7,A44,A55,A83,A85,A127,XBOOLE_0:def 3;
end;
then A129: L~do /\ L~pion1 = {pion1/.len pion1} by A128,XBOOLE_0:def 10;
A130: L~(go^'pion1) /\ L~do = (L~go \/ L~pion1) /\ L~do by A98,TOPREAL8:
35
.= {go/.1} \/ {do/.1} by A70,A85,A127,A129,XBOOLE_1:23
.= {(go^'pion1)/.1} \/ {do/.1} by AMISTD_1:5
.= {(go^'pion1)/.1,do/.1} by ENUMSET1:41;
A131: do/.len do = (go^'pion1)/.1 by A62,AMISTD_1:5;
reconsider godo as non constant standard special_circular_sequence
by A100,A102,A103,A108,A120,A121,A125,A126,A130,A131,TOPREAL8:11,33;
A132: UA is_an_arc_of W-min C,E-max C by JORDAN6:def 8;
then A133: UA is connected by JORDAN6:11;
A134: W-min C in UA & E-max C in UA by A132,TOPREAL1:4;
set ff = Rotate(Cage(C,n),Wmin);
Wmin in rng Cage(C,n) by SPRECT_2:47;
then A135: ff/.1 = Wmin by FINSEQ_6:98;
A136: L~ff = L~Cage(C,n) by REVROT_1:33;
then A137: (W-max L~ff)..ff > 1 by A135,SPRECT_5:23;
(W-max L~ff)..ff <= (N-min L~ff)..ff by A135,A136,SPRECT_5:24;
then A138: (N-min L~ff)..ff > 1 by A137,AXIOMS:22;
(N-min L~ff)..ff < (N-max L~ff)..ff by A135,A136,SPRECT_5:25;
then A139: (N-max L~ff)..ff > 1 by A138,AXIOMS:22;
(N-max L~ff)..ff <= (E-max L~ff)..ff by A135,A136,SPRECT_5:26;
then A140: Emax..ff > 1 by A136,A139,AXIOMS:22;
A141: now assume A142: Gij..US <= 1;
Gij..US >= 1 by A34,FINSEQ_4:31;
then Gij..US = 1 by A142,AXIOMS:21;
then Gij = US/.1 by A34,FINSEQ_5:41;
hence contradiction by A19,A23,JORDAN1F:5;
end;
A143: Cage(C,n) is_sequence_on G by JORDAN9:def 1;
then A144: ff is_sequence_on G by REVROT_1:34;
A145: right_cell(godo,1,G)\L~godo c= RightComp godo by A96,A101,JORDAN9:
29;
A146: L~godo = L~(go^'pion1) \/ L~do by A100,TOPREAL8:35
.= L~go \/ L~pion1 \/ L~do by A98,TOPREAL8:35;
L~Cage(C,n) = L~US \/ L~LS by JORDAN1E:17;
then A147: L~US c= L~Cage(C,n) & L~LS c= L~Cage(C,n) by XBOOLE_1:7;
then A148: L~go c=L~Cage(C,n) & L~do c=L~Cage(C,n)
by A48,A55,XBOOLE_1:1;
A149: W-min C in C by SPRECT_1:15;
A150: now assume W-min C in L~godo;
then W-min C in L~go \/ L~pion1 or W-min C in L~do
by A146,XBOOLE_0:def 2;
then A151: W-min C in L~go or W-min C in L~pion1 or W-min C in L~do
by XBOOLE_0:def 2;
per cases by A151;
suppose W-min C in L~go;
then C meets L~Cage(C,n) by A148,A149,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
suppose W-min C in L~pion1;
hence contradiction by A5,A7,A83,A134,XBOOLE_0:3;
suppose W-min C in L~do;
then C meets L~Cage(C,n) by A148,A149,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
end;
right_cell(Rotate(Cage(C,n),Wmin),1) =
right_cell(ff,1,GoB ff) by A93,JORDAN1H:29
.= right_cell(ff,1,GoB Cage(C,n)) by REVROT_1:28
.= right_cell(ff,1,G) by JORDAN1H:52
.= right_cell(ff-:Emax,1,G) by A140,A144,JORDAN1J:53
.= right_cell(US,1,G) by JORDAN1E:def 1
.= right_cell(R_Cut(US,Gij),1,G) by A34,A97,A141,JORDAN1J:52
.= right_cell(go^'pion1,1,G) by A41,A99,JORDAN1J:51
.= right_cell(godo,1,G) by A95,A101,JORDAN1J:51;
then W-min C in right_cell(godo,1,G) by JORDAN1I:8;
then W-min C in right_cell(godo,1,G)\L~godo by A150,XBOOLE_0:def 4;
then A152: W-min C in RightComp godo by A145;
A153: godo/.1 = (go^'pion1)/.1 by AMISTD_1:5
.= Wmin by A61,AMISTD_1:5;
A154: len US >= 2 by A18,AXIOMS:22;
A155: godo/.2 = (go^'pion1)/.2 by A94,AMISTD_1:9
.= US/.2 by A33,A74,AMISTD_1:9
.= (US^'LS)/.2 by A154,AMISTD_1:9
.= Rotate(Cage(C,n),Wmin)/.2 by JORDAN1E:15;
A156: L~godo = L~go \/ L~pion1 \/ L~do by A146;
A157: L~go \/ L~do is compact by COMPTS_1:19;
A158