:: Upper and Lower Sequence on the Cage, Upper and Lower Arcs
:: by Robert Milewski
::
:: Received April 5, 2002
:: Copyright (c) 2002-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, GOBOARD1, XXREAL_0, TREES_1, ARYTM_3,
FINSEQ_1, RELAT_1, MCART_1, XBOOLE_0, GRAPH_2, ORDINAL4, RCOMP_1,
RELAT_2, SPPOL_1, EUCLID, TOPREAL1, JORDAN9, FINSEQ_5, PSCOMP_1,
PARTFUN1, TARSKI, CARD_1, FINSEQ_4, PRE_TOPC, RLTOPSP1, ARYTM_1,
JORDAN1E, FINSEQ_6, RFINSEQ, JORDAN3, FUNCT_1, GOBOARD5, GOBOARD9,
CONNSP_1, TOPREAL2, JORDAN8, SPPOL_2, NAT_1, GROUP_2, MATRIX_1, SPRECT_2,
ZFMISC_1, JORDAN6, GOBOARD2, JORDAN2C, JORDAN1A, XXREAL_2;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5,
RFINSEQ, MATRIX_0, FINSEQ_6, GRAPH_2, ZFMISC_1, STRUCT_0, PRE_TOPC,
TOPREAL2, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, PSCOMP_1, SPRECT_2,
GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13, SPPOL_1,
SPPOL_2, JORDAN3, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A,
JORDAN1E;
constructors REAL_1, FINSEQ_4, NEWTON, RFINSEQ, TOPS_1, CONNSP_1, MATRIX_1,
GOBOARD2, PSCOMP_1, GRAPH_2, GOBOARD9, JORDAN3, JORDAN5C, JORDAN6,
JORDAN2C, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, NAT_D, RELSET_1,
CONVEX1, DOMAIN_1;
registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1,
FINSEQ_5, FINSEQ_6, STRUCT_0, PRE_TOPC, TOPREAL1, TOPREAL2, GOBOARD2,
JORDAN1, SPPOL_2, GOBRD11, TOPREAL5, SPRECT_1, SPRECT_2, REVROT_1,
TOPREAL6, JORDAN8, JORDAN1E, JORDAN1G, CARD_1, FUNCT_1, EUCLID, JORDAN2C,
INT_1, ORDINAL1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, GOBOARD5, XBOOLE_0;
equalities PSCOMP_1, ORDINAL1;
expansions TARSKI, XBOOLE_0;
theorems JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, GOBOARD5, FINSEQ_1, FINSEQ_2,
JORDAN4, JORDAN6, SPRECT_2, FINSEQ_4, FINSEQ_5, FINSEQ_6, GOBOARD7,
GOBOARD9, SPPOL_1, SPPOL_2, REVROT_1, TOPREAL1, SPRECT_3, JORDAN5B,
JORDAN3, GOBRD13, INT_1, JORDAN9, JORDAN2C, SUBSET_1, CONNSP_1, ZFMISC_1,
JGRAPH_1, GOBOARD1, SPRECT_1, TARSKI, TOPREAL3, FINSEQ_3, RELAT_1,
COMPTS_1, FUNCT_1, TOPREAL5, JORDAN10, GRAPH_2, GOBOARD2, CARD_1, CARD_2,
ENUMSET1, SPRECT_4, JORDAN1B, SPRECT_5, JORDAN1E, PARTFUN2, JORDAN1F,
TDLAT_1, JORDAN1G, GOBOARD3, JORDAN1H, TOPREAL8, GOBRD14, JORDAN1D,
JORDAN1I, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, EUCLID, PRE_TOPC,
ORDINAL1, PARTFUN1, MATRIX_0, XREAL_0, NAT_D, RLTOPSP1;
schemes NAT_1;
begin
reserve n for Nat;
theorem Th1:
for G be Go-board for i1,i2,j1,j2 be Nat st 1 <= j1 &
j1 <= width G & 1 <= j2 & j2 <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds
G*(i1,j1)`1 < G*(i2,j2)`1
proof
let G be Go-board;
let i1,i2,j1,j2 be Nat;
assume that
A1: 1 <= j1 and
A2: j1 <= width G and
A3: 1 <= j2 and
A4: j2 <= width G and
A5: 1 <= i1 and
A6: i1 < i2 and
A7: i2 <= len G;
A8: 1 <= i2 by A5,A6,XXREAL_0:2;
then G*(i2,j1)`1 = G*(i2,1)`1 by A1,A2,A7,GOBOARD5:2
.= G*(i2,j2)`1 by A3,A4,A7,A8,GOBOARD5:2;
hence thesis by A1,A2,A5,A6,A7,GOBOARD5:3;
end;
theorem Th2:
for G be Go-board for i1,i2,j1,j2 be Nat st 1 <= i1 &
i1 <= len G & 1 <= i2 & i2 <= len G & 1 <= j1 & j1 < j2 & j2 <= width G holds G
*(i1,j1)`2 < G*(i2,j2)`2
proof
let G be Go-board;
let i1,i2,j1,j2 be Nat;
assume that
A1: 1 <= i1 and
A2: i1 <= len G and
A3: 1 <= i2 and
A4: i2 <= len G and
A5: 1 <= j1 and
A6: j1 < j2 and
A7: j2 <= width G;
A8: 1 <= j2 by A5,A6,XXREAL_0:2;
then G*(i1,j2)`2 = G*(1,j2)`2 by A1,A2,A7,GOBOARD5:1
.= G*(i2,j2)`2 by A3,A4,A7,A8,GOBOARD5:1;
hence thesis by A1,A2,A5,A6,A7,GOBOARD5:4;
end;
registration
let f be non empty FinSequence;
let g be FinSequence;
cluster f^'g -> non empty;
coherence
proof
f^'g = f^(2,len g)-cut g by FINSEQ_6:def 5;
hence thesis;
end;
end;
theorem Th3:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for n be Nat holds L~(Cage(C,n)-:E-max L~Cage(C,n)) /\ L~
(Cage(C,n):-E-max L~Cage(C,n)) = {N-min L~Cage(C,n),E-max L~Cage(C,n)}
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
set US = Cage(C,n)-:E-max L~Cage(C,n);
set LS = Cage(C,n):-E-max L~Cage(C,n);
set f=Cage(C,n);
set pW=E-max L~Cage(C,n);
set pN=N-min L~Cage(C,n);
A1: pW`1 = E-bound L~f by EUCLID:52;
A2: pW in rng Cage(C,n) by SPRECT_2:46;
then
A3: Cage(C,n)-:pW <> {} by FINSEQ_5:47;
(Cage(C,n):-pW)/.1 = pW by FINSEQ_5:53;
then
A4: E-max L~Cage(C,n) in rng (Cage(C,n):-E-max L~Cage(C,n)) by FINSEQ_6:42;
(f:-pW)/.len(f:-pW) = f/.len f by A2,FINSEQ_5:54
.= f/.1 by FINSEQ_6:def 1
.= pN by JORDAN9:32;
then
A5: pN in rng (Cage(C,n):-pW) by FINSEQ_6:168;
{pN,pW} c= rng LS
by A5,A4,TARSKI:def 2;
then
A6: card {pN,pW} c= card rng LS by CARD_1:11;
card rng LS c= card dom LS by CARD_2:61;
then
A7: card rng LS c= len LS by CARD_1:62;
N-max L~f in L~f by SPRECT_1:11;
then (N-max L~f)`1 <= pW`1 by A1,PSCOMP_1:24;
then
A8: pN <> pW by SPRECT_2:51;
then card {pN,pW} = 2 by CARD_2:57;
then Segm 2 c= Segm len LS by A6,A7;
then len LS >= 2 by NAT_1:39;
then
A9: rng LS c= L~LS by SPPOL_2:18;
len(f-:pW) = pW..f by A2,FINSEQ_5:42;
then (f-:pW)/.len (f-:pW) = pW by A2,FINSEQ_5:45;
then
A10: pW in rng (Cage(C,n)-:pW) by A3,FINSEQ_6:168;
(Cage(C,n)-:pW)/.1 = Cage(C,n)/.1 by A2,FINSEQ_5:44
.= pN by JORDAN9:32;
then
A11: N-min L~Cage(C,n) in rng (Cage(C,n)-:E-max L~Cage(C,n)) by A3,FINSEQ_6:42;
{pN,pW} c= rng US
by A11,A10,TARSKI:def 2;
then
A12: card {pN,pW} c= card rng US by CARD_1:11;
card rng US c= card dom US by CARD_2:61;
then
A13: card rng US c= len US by CARD_1:62;
LS/.(len LS) = Cage(C,n)/.len Cage(C,n) by A2,FINSEQ_5:54
.= Cage(C,n)/.1 by FINSEQ_6:def 1
.= N-min L~Cage(C,n) by JORDAN9:32;
then
A14: N-min L~Cage(C,n) in rng LS by FINSEQ_6:168;
pW..Cage(C,n) <= pW..Cage(C,n);
then
A15: E-max L~Cage(C,n) in rng US by A2,FINSEQ_5:46;
card {pN,pW} = 2 by A8,CARD_2:57;
then
A16: Segm 2 c= Segm len US by A12,A13;
then
A17: len US >= 2 by NAT_1:39;
then
A18: rng US c= L~US by SPPOL_2:18;
thus L~US /\ L~LS c= {N-min L~Cage(C,n),E-max L~Cage(C,n)}
proof
let x be object;
assume
A19: x in L~US /\ L~LS;
then reconsider x1=x as Point of TOP-REAL 2;
assume
A20: not x in {N-min L~Cage(C,n),E-max L~Cage(C,n)};
x in L~US by A19,XBOOLE_0:def 4;
then consider i1 be Nat such that
A21: 1 <= i1 and
A22: i1+1 <= len US and
A23: x1 in LSeg(US,i1) by SPPOL_2:13;
A24: LSeg(US,i1) = LSeg(f,i1) by A22,SPPOL_2:9;
x in L~LS by A19,XBOOLE_0:def 4;
then consider i2 be Nat such that
A25: 1 <= i2 and
A26: i2+1 <= len LS and
A27: x1 in LSeg(LS,i2) by SPPOL_2:13;
set i3=i2-'1;
A28: i3+1 = i2 by A25,XREAL_1:235;
then
A29: 1+pW..f <= i3+1+pW..f by A25,XREAL_1:7;
A30: len LS = len f-pW..f+1 by A2,FINSEQ_5:50;
then i2 < len f-pW..f+1 by A26,NAT_1:13;
then i2-1 < len f-pW..f by XREAL_1:19;
then
A31: i2-1+pW..f < len f by XREAL_1:20;
i2-1 >= 1-1 by A25,XREAL_1:9;
then
A32: i3+pW..f < len f by A31,XREAL_0:def 2;
A33: LSeg(LS,i2) = LSeg(f,i3+pW..f) by A2,A28,SPPOL_2:10;
A34: len US = pW..f by A2,FINSEQ_5:42;
then i1+1 < pW..f+1 by A22,NAT_1:13;
then i1+1 < i3+pW..f+1 by A29,XXREAL_0:2;
then
A35: i1+1 <= i3+pW..f by NAT_1:13;
A36: pW..f-'1+1 = pW..f by A2,FINSEQ_4:21,XREAL_1:235;
i3+1 < len f-pW..f+1 by A26,A28,A30,NAT_1:13;
then i3 < len f-pW..f by XREAL_1:7;
then
A37: i3+pW..f < len f by XREAL_1:20;
then
A38: i3+pW..f+1 <= len f by NAT_1:13;
now
per cases by A21,A35,XXREAL_0:1;
suppose
i1+1 < i3+pW..f & i1 > 1;
then LSeg(f,i1) misses LSeg(f,i3+pW..f) by A37,GOBOARD5:def 4;
then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {};
hence contradiction by A23,A27,A24,A33,XBOOLE_0:def 4;
end;
suppose
A39: i1 = 1;
A40: i3+pW..f >= 0+2 by A17,A34,XREAL_1:7;
now
per cases by A40,XXREAL_0:1;
suppose
i3+pW..f > 2;
then
A41: i1+1 < i3+pW..f by A39;
now
per cases by A38,XXREAL_0:1;
suppose
i3+pW..f+1 < len f;
then LSeg(f,i1) misses LSeg(f,i3+pW..f) by A41,GOBOARD5:def 4;
then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {};
hence contradiction by A23,A27,A24,A33,XBOOLE_0:def 4;
end;
suppose
i3+pW..f+1 = len f;
then i3+pW..f = len f-1;
then i3+pW..f = len f-'1 by XREAL_0:def 2;
then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {f/.1} by A39,GOBOARD7:34
,REVROT_1:30;
then x1 in {f/.1} by A23,A27,A24,A33,XBOOLE_0:def 4;
then x1 = f/.1 by TARSKI:def 1
.= pN by JORDAN9:32;
hence contradiction by A20,TARSKI:def 2;
end;
end;
hence contradiction;
end;
suppose
A42: i3+pW..f = 2;
A43: 1 + 2 <= len f by GOBOARD7:34,XXREAL_0:2;
x1 in LSeg(f,1) /\ LSeg(f,1+1) by A23,A27,A24,A33,A39,A42,
XBOOLE_0:def 4;
then x1 in {f/.(1+1)} by A43,TOPREAL1:def 6;
then
A44: x1 = f/.(1+1) by TARSKI:def 1;
0+pW..f >= i3+pW..f by A16,A34,A42,NAT_1:39;
then
A45: i3 = 0 by XREAL_1:6;
0+1 in dom LS by FINSEQ_5:6;
then LS/.1 = x1 by A2,A42,A44,A45,FINSEQ_5:52;
then x1 = pW by FINSEQ_5:53;
hence contradiction by A20,TARSKI:def 2;
end;
end;
hence contradiction;
end;
suppose
A46: i1+1 = i3+pW..f;
i3+pW..f >= pW..f by NAT_1:11;
then pW..f < len f by A32,XXREAL_0:2;
then pW..f+1 <= len f by NAT_1:13;
then
A47: pW..f-'1 + (1+1) <= len f by A36;
0+pW..f <= i3+pW..f by XREAL_1:7;
then pW..f = i1+1 by A22,A34,A46,XXREAL_0:1;
then LSeg(f,i1) /\ LSeg(f,i3+(pW..f)) = {f/.(pW..f)} by A21,A36,A46,A47
,TOPREAL1:def 6;
then x1 in {f/.(pW..f)} by A23,A27,A24,A33,XBOOLE_0:def 4;
then x1 = f/.(pW..f) by TARSKI:def 1
.= pW by A2,FINSEQ_5:38;
hence contradiction by A20,TARSKI:def 2;
end;
end;
hence contradiction;
end;
A48: US/.1 = Cage(C,n)/.1 by A2,FINSEQ_5:44
.= N-min L~Cage(C,n) by JORDAN9:32;
US is non empty by A16,NAT_1:39;
then
A49: N-min L~Cage(C,n) in rng US by A48,FINSEQ_6:42;
A50: E-max L~Cage(C,n) in rng LS by FINSEQ_6:61;
thus {N-min L~Cage(C,n),E-max L~Cage(C,n)} c= L~US /\ L~LS
proof
let x be object;
assume
A51: x in {N-min L~Cage(C,n),E-max L~Cage(C,n)};
per cases by A51,TARSKI:def 2;
suppose
x = N-min L~Cage(C,n);
hence thesis by A9,A18,A49,A14,XBOOLE_0:def 4;
end;
suppose
x = E-max L~Cage(C,n);
hence thesis by A9,A50,A18,A15,XBOOLE_0:def 4;
end;
end;
end;
theorem Th4:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 holds Upper_Seq(C,n) = Rotate(Cage(C,n),E-max L~Cage(C,n)):-W-min L~
Cage(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
set Nmi = N-min L~Cage(C,n);
set Nma = N-max L~Cage(C,n);
set Wmi = W-min L~Cage(C,n);
set Wma = W-max L~Cage(C,n);
set Ema = E-max L~Cage(C,n);
set Emi = E-min L~Cage(C,n);
set Sma = S-max L~Cage(C,n);
set Smi = S-min L~Cage(C,n);
set RotWmi = Rotate(Cage(C,n),Wmi);
set RotEma = Rotate(Cage(C,n),Ema);
A1: Nmi in rng Cage(C,n) by SPRECT_2:39;
A2: Cage(C,n)/.1 = Nmi by JORDAN9:32;
then Emi..Cage(C,n) <= Sma..Cage(C,n) by SPRECT_2:72;
then Ema..Cage(C,n) < Sma..Cage(C,n) by A2,SPRECT_2:71,XXREAL_0:2;
then
A3: Ema..Cage(C,n) < Smi..Cage(C,n) by A2,SPRECT_2:73,XXREAL_0:2;
then
A4: Ema..Cage(C,n) < Wmi..Cage(C,n) by A2,SPRECT_2:74,XXREAL_0:2;
(Cage(C,n):-Ema)/.1 = Ema by FINSEQ_5:53;
then
A5: Ema in rng (Cage(C,n):-Ema) by FINSEQ_6:42;
A6: Ema in rng Cage(C,n) by SPRECT_2:46;
then (Cage(C,n):-Ema)/.len(Cage(C,n):-Ema) = Cage(C,n)/.len Cage(C,n) by
FINSEQ_5:54
.= Cage(C,n)/.1 by FINSEQ_6:def 1
.= Nmi by JORDAN9:32;
then
A7: Nmi in rng (Cage(C,n):-Ema) by FINSEQ_6:168;
{Nmi,Ema} c= rng (Cage(C,n):-Ema)
by A7,A5,TARSKI:def 2;
then
A8: card {Nmi,Ema} c= card rng (Cage(C,n):-Ema) by CARD_1:11;
A9: Wmi in rng Cage(C,n) by SPRECT_2:43;
then
A10: Cage(C,n)-:Wmi <> {} by FINSEQ_5:47;
len(Cage(C,n)-:Wmi) = Wmi..Cage(C,n) by A9,FINSEQ_5:42;
then (Cage(C,n)-:Wmi)/.len (Cage(C,n)-:Wmi) = Wmi by A9,FINSEQ_5:45;
then
A11: Wmi in rng (Cage(C,n)-:Wmi) by A10,FINSEQ_6:168;
(Cage(C,n)-:Wmi)/.1 = Cage(C,n)/.1 by A9,FINSEQ_5:44
.= Nmi by JORDAN9:32;
then
A12: Nmi in rng (Cage(C,n)-:Wmi) by A10,FINSEQ_6:42;
{Nmi,Wmi} c= rng (Cage(C,n)-:Wmi)
by A12,A11,TARSKI:def 2;
then
A13: card {Nmi,Wmi} c= card rng (Cage(C,n)-:Wmi) by CARD_1:11;
card rng (Cage(C,n)-:Wmi) c= card dom (Cage(C,n)-:Wmi) by CARD_2:61;
then
A14: card rng (Cage(C,n)-:Wmi) c= len (Cage(C,n)-:Wmi) by CARD_1:62;
A15: Nmi`2 = N-bound L~Cage(C,n) by EUCLID:52;
Nma`1 <= (NE-corner L~Cage(C,n))`1 by PSCOMP_1:38;
then
A16: Nma`1 <= E-bound L~Cage(C,n) by EUCLID:52;
Nmi`1 < Nma`1 by SPRECT_2:51;
then
A17: Nmi <> Ema by A16,EUCLID:52;
then
A18: card {Nmi,Ema} = 2 by CARD_2:57;
A19: Smi..Cage(C,n) <= Wmi..Cage(C,n) by A2,SPRECT_2:74;
then
A20: Ema in rng (Cage(C,n)-:Wmi) by A9,A6,A3,FINSEQ_5:46,XXREAL_0:2;
A21: Wmi in rng (Cage(C,n):-Ema) by A9,A6,A19,A3,FINSEQ_6:62,XXREAL_0:2;
Wma in L~Cage(C,n) by SPRECT_1:13;
then Wma`2 <= Nmi`2 by A15,PSCOMP_1:24;
then
A22: Nmi <> Wmi by SPRECT_2:57;
then card {Nmi,Wmi} = 2 by CARD_2:57;
then Segm 2 c= Segm len (Cage(C,n)-:Wmi) by A13,A14;
then len (Cage(C,n)-:Wmi) >= 2 by NAT_1:39;
then
A23: rng (Cage(C,n)-:Wmi) c= L~(Cage(C,n)-:Wmi) by SPPOL_2:18;
A24: not Ema in rng (Cage(C,n):-Wmi)
proof
(Cage(C,n):-Wmi)/.1 = Wmi by FINSEQ_5:53;
then
A25: Wmi in rng (Cage(C,n):-Wmi) by FINSEQ_6:42;
(Cage(C,n):-Wmi)/.len(Cage(C,n):-Wmi) = Cage(C,n)/.len Cage(C,n) by A9,
FINSEQ_5:54
.= Cage(C,n)/.1 by FINSEQ_6:def 1
.= Nmi by JORDAN9:32;
then
A26: Nmi in rng (Cage(C,n):-Wmi) by FINSEQ_6:168;
{Nmi,Wmi} c= rng (Cage(C,n):-Wmi)
by A26,A25,TARSKI:def 2;
then
A27: card {Nmi,Wmi} c= card rng (Cage(C,n):-Wmi) by CARD_1:11;
A28: Nmi`2 = N-bound L~Cage(C,n) by EUCLID:52;
Wma in L~Cage(C,n) by SPRECT_1:13;
then Wma`2 <= Nmi`2 by A28,PSCOMP_1:24;
then Nmi <> Wmi by SPRECT_2:57;
then
A29: card {Nmi,Wmi} = 2 by CARD_2:57;
card rng (Cage(C,n):-Wmi) c= card dom (Cage(C,n):-Wmi) by CARD_2:61;
then card rng (Cage(C,n):-Wmi) c= len (Cage(C,n):-Wmi) by CARD_1:62;
then Segm 2 c= Segm len (Cage(C,n):-Wmi) by A29,A27;
then len (Cage(C,n):-Wmi) >= 2 by NAT_1:39;
then
A30: rng (Cage(C,n):-Wmi) c= L~(Cage(C,n):-Wmi) by SPPOL_2:18;
assume Ema in rng (Cage(C,n):-Wmi);
then Ema in L~(Cage(C,n)-:Wmi) /\ L~(Cage(C,n):-Wmi) by A20,A23,A30,
XBOOLE_0:def 4;
then Ema in {Nmi,Wmi} by JORDAN1G:17;
then Ema = Wmi by A17,TARSKI:def 2;
hence contradiction by TOPREAL5:19;
end;
A31: Nma..Cage(C,n) <= Ema..Cage(C,n) by A2,SPRECT_2:70;
A32: Nmi..Cage(C,n) < Nma..Cage(C,n) by A2,SPRECT_2:68;
then
A33: Nmi..Cage(C,n) < Ema..Cage(C,n) by A2,SPRECT_2:70,XXREAL_0:2;
then
A34: Nmi in rng (Cage(C,n)-:Wmi) by A1,A9,A4,FINSEQ_5:46,XXREAL_0:2;
A35: Ema..(Cage(C,n)-:Wmi) <> 1
proof
assume
A36: Ema..(Cage(C,n)-:Wmi) = 1;
Nmi..(Cage(C,n)-:Wmi) = Nmi..Cage(C,n) by A1,A9,A33,A4,SPRECT_5:3
,XXREAL_0:2
.= 1 by A2,FINSEQ_6:43;
hence contradiction by A32,A31,A20,A34,A36,FINSEQ_5:9;
end;
then Ema in rng (Cage(C,n)-:Wmi/^1) by A20,FINSEQ_6:78;
then
A37: Ema in rng (Cage(C,n)-:Wmi/^1) \ rng (Cage(C,n):-Wmi) by A24,
XBOOLE_0:def 5;
card rng (Cage(C,n):-Ema) c= card dom (Cage(C,n):-Ema) by CARD_2:61;
then card rng (Cage(C,n):-Ema) c= len (Cage(C,n):-Ema) by CARD_1:62;
then Segm 2 c= Segm len (Cage(C,n):-Ema) by A18,A8;
then len (Cage(C,n):-Ema) >= 2 by NAT_1:39;
then
A38: rng (Cage(C,n):-Ema) c= L~(Cage(C,n):-Ema) by SPPOL_2:18;
not Wmi in rng (Cage(C,n)-:Ema)
proof
assume
A39: Wmi in rng (Cage(C,n)-:Ema);
(Cage(C,n)-:Ema)/.len (Cage(C,n)-:Ema) = (Cage(C,n)-:Ema)/.(Ema..Cage
(C,n)) by A6,FINSEQ_5:42
.= Ema by A6,FINSEQ_5:45;
then
A40: Ema in rng (Cage(C,n)-:Ema) by A39,RELAT_1:38,FINSEQ_6:168;
(Cage(C,n)-:Ema)/.1 = Cage(C,n)/.1 by A6,FINSEQ_5:44
.= Nmi by JORDAN9:32;
then
A41: Nmi in rng (Cage(C,n)-:Ema) by A39,FINSEQ_6:42,RELAT_1:38;
{Nmi,Ema} c= rng (Cage(C,n)-:Ema)
by A41,A40,TARSKI:def 2;
then
A42: card {Nmi,Ema} c= card rng (Cage(C,n)-:Ema) by CARD_1:11;
card rng (Cage(C,n)-:Ema) c= card dom (Cage(C,n)-:Ema) by CARD_2:61;
then card rng (Cage(C,n)-:Ema) c= len (Cage(C,n)-:Ema) by CARD_1:62;
then Segm 2 c= Segm len (Cage(C,n)-:Ema) by A18,A42;
then len (Cage(C,n)-:Ema) >= 2 by NAT_1:39;
then rng (Cage(C,n)-:Ema) c= L~(Cage(C,n)-:Ema) by SPPOL_2:18;
then Wmi in L~(Cage(C,n)-:Ema) /\ L~(Cage(C,n):-Ema) by A21,A38,A39,
XBOOLE_0:def 4;
then Wmi in {Nmi,Ema} by Th3;
then Wmi = Ema by A22,TARSKI:def 2;
hence contradiction by TOPREAL5:19;
end;
then
A43: Wmi in rng Cage(C,n) \ rng(Cage(C,n)-:Ema) by A9,XBOOLE_0:def 5;
RotWmi-:Ema = ((Cage(C,n):-Wmi)^((Cage(C,n)-:Wmi)/^1))-:Ema by A9,
FINSEQ_6:def 2
.= (Cage(C,n):-Wmi)^(((Cage(C,n)-:Wmi)/^1)-:Ema) by A37,FINSEQ_6:67
.= (Cage(C,n):-Wmi)^(((Cage(C,n)-:Wmi)-:Ema)/^1) by A20,A35,FINSEQ_6:60
.= ((Cage(C,n):-Ema):-Wmi)^(((Cage(C,n)-:Wmi)-:Ema)/^1) by A43,FINSEQ_6:71
,SPRECT_2:46
.= ((Cage(C,n):-Ema):-Wmi)^((Cage(C,n)-:Ema)/^1) by A9,A20,FINSEQ_6:75
.= ((Cage(C,n):-Ema)^((Cage(C,n)-:Ema)/^1)):-Wmi by A21,FINSEQ_6:64
.= RotEma:-Wmi by A6,FINSEQ_6:def 2;
hence thesis by JORDAN1E:def 1;
end;
theorem
for C be compact non vertical non horizontal Subset of TOP-REAL 2
holds W-min L~Cage(C,n) in rng Upper_Seq(C,n) & W-min L~Cage(C,n) in L~
Upper_Seq(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
set p = W-min L~Cage(C,n);
A1: p in rng Cage(C,n) by SPRECT_2:43;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A2: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),p) by FINSEQ_6:90,SPRECT_2:43;
Upper_Seq(C,n) = Rotate(Cage(C,n),p)-:E-max L~Cage(C,n) by JORDAN1E:def 1;
then Upper_Seq(C,n)/.1 = Rotate(Cage(C,n),p)/.1 by A2,FINSEQ_5:44;
then Upper_Seq(C,n)/.1 = p by A1,FINSEQ_6:92;
hence
A3: p in rng Upper_Seq(C,n) by FINSEQ_6:42;
len Upper_Seq(C,n) >= 2 by TOPREAL1:def 8;
then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18;
hence thesis by A3;
end;
theorem
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 holds W-max L~Cage(C,n) in rng Upper_Seq(C,n) & W-max L~Cage(C,n) in
L~Upper_Seq(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
set x = W-max L~Cage(C,n);
set p = W-min L~Cage(C,n);
set f = Rotate(Cage(C,n),E-max L~Cage(C,n));
A1: rng f = rng Cage(C,n) by FINSEQ_6:90,SPRECT_2:46;
A2: x in rng Cage(C,n) by SPRECT_2:44;
A3: L~Cage(C,n) = L~f by REVROT_1:33;
W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
then
A4: W-min L~Cage(C,n) in rng f by FINSEQ_6:90,SPRECT_2:46;
A5: p in rng Cage(C,n) by SPRECT_2:43;
Lower_Seq(C,n) = f-:W-min L~Cage(C,n) by JORDAN1G:18;
then Lower_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:44;
then (W-min L~f)..f < (W-max L~f)..f by A3,JORDAN1F:6,SPRECT_5:42;
then x in rng(f:-p) by A1,A2,A5,A3,FINSEQ_6:62;
hence
A6: x in rng Upper_Seq(C,n) by Th4;
len Upper_Seq(C,n) >= 2 by TOPREAL1:def 8;
then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18;
hence thesis by A6;
end;
theorem Th7:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 holds N-min L~Cage(C,n) in rng Upper_Seq(C,n) & N-min L~Cage(C,n) in
L~Upper_Seq(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
set x = N-min L~Cage(C,n);
set p = W-min L~Cage(C,n);
set f = Rotate(Cage(C,n),E-max L~Cage(C,n));
A1: rng f = rng Cage(C,n) by FINSEQ_6:90,SPRECT_2:46;
A2: x in rng Cage(C,n) by SPRECT_2:39;
A3: L~Cage(C,n) = L~f by REVROT_1:33;
W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
then
A4: W-min L~Cage(C,n) in rng f by FINSEQ_6:90,SPRECT_2:46;
A5: p in rng Cage(C,n) by SPRECT_2:43;
Lower_Seq(C,n) = f-:W-min L~Cage(C,n) by JORDAN1G:18;
then
A6: Lower_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:44;
then
A7: (W-max L~f)..f <= (N-min L~f)..f by A3,JORDAN1F:6,SPRECT_5:43;
(W-min L~f)..f < (W-max L~f)..f by A6,A3,JORDAN1F:6,SPRECT_5:42;
then x in rng(f:-p) by A1,A2,A5,A3,A7,FINSEQ_6:62,XXREAL_0:2;
hence
A8: x in rng Upper_Seq(C,n) by Th4;
len Upper_Seq(C,n) >= 2 by TOPREAL1:def 8;
then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18;
hence thesis by A8;
end;
theorem
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 holds N-max L~Cage(C,n) in rng Upper_Seq(C,n) & N-max L~Cage(C,n) in
L~Upper_Seq(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
set x = N-max L~Cage(C,n);
set p = W-min L~Cage(C,n);
set f = Rotate(Cage(C,n),E-max L~Cage(C,n));
A1: rng f = rng Cage(C,n) by FINSEQ_6:90,SPRECT_2:46;
A2: x in rng Cage(C,n) by SPRECT_2:40;
A3: Lower_Seq(C,n)/.1 = E-max L~Cage(C,n) by JORDAN1F:6;
A4: L~Cage(C,n) = L~f by REVROT_1:33;
W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
then
A5: W-min L~Cage(C,n) in rng f by FINSEQ_6:90,SPRECT_2:46;
A6: p in rng Cage(C,n) by SPRECT_2:43;
Lower_Seq(C,n) = f-:W-min L~Cage(C,n) by JORDAN1G:18;
then
A7: Lower_Seq(C,n)/.1 = f/.1 by A5,FINSEQ_5:44;
then
A8: (W-min L~f)..f < (W-max L~f)..f by A4,JORDAN1F:6,SPRECT_5:42;
A9: (W-max L~f)..f <= (N-min L~f)..f by A7,A4,JORDAN1F:6,SPRECT_5:43;
per cases;
suppose
N-max L~f <> E-max L~f;
then (W-max L~f)..f < (N-max L~f)..f by A7,A3,A4,A9,SPRECT_5:44,XXREAL_0:2;
then x in rng(f:-p) by A1,A2,A6,A4,A8,FINSEQ_6:62,XXREAL_0:2;
hence
A10: x in rng Upper_Seq(C,n) by Th4;
len Upper_Seq(C,n) >= 2 by TOPREAL1:def 8;
then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18;
hence thesis by A10;
end;
suppose
A11: N-max L~f = E-max L~f;
A12: (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) <= (E-max L~
Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n));
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A13: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by
FINSEQ_6:90,SPRECT_2:43;
Upper_Seq(C,n) = Rotate(Cage(C,n),p)-:E-max L~Cage(C,n) by JORDAN1E:def 1;
hence
A14: x in rng Upper_Seq(C,n) by A4,A11,A13,A12,FINSEQ_5:46;
len Upper_Seq(C,n) >= 2 by TOPREAL1:def 8;
then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18;
hence thesis by A14;
end;
end;
theorem
for C be compact non vertical non horizontal Subset of TOP-REAL 2
holds E-max L~Cage(C,n) in rng Upper_Seq(C,n) & E-max L~Cage(C,n) in L~
Upper_Seq(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
set x = E-max L~Cage(C,n);
set p = W-min L~Cage(C,n);
A1: (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) <= (E-max L~
Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n));
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A2: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_6:90
,SPRECT_2:43;
Upper_Seq(C,n) = Rotate(Cage(C,n),p)-:E-max L~Cage(C,n) by JORDAN1E:def 1;
hence
A3: x in rng Upper_Seq(C,n) by A2,A1,FINSEQ_5:46;
len Upper_Seq(C,n) >= 2 by TOPREAL1:def 8;
then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18;
hence thesis by A3;
end;
theorem
for C be compact non vertical non horizontal Subset of TOP-REAL 2
holds E-max L~Cage(C,n) in rng Lower_Seq(C,n) & E-max L~Cage(C,n) in L~
Lower_Seq(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
set p = E-max L~Cage(C,n);
Lower_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n)):-p by JORDAN1E:def 2;
hence
A1: p in rng Lower_Seq(C,n) by FINSEQ_6:61;
len Lower_Seq(C,n) >= 2 by TOPREAL1:def 8;
then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18;
hence thesis by A1;
end;
theorem
for C be compact non vertical non horizontal Subset of TOP-REAL 2
holds E-min L~Cage(C,n) in rng Lower_Seq(C,n) & E-min L~Cage(C,n) in L~
Lower_Seq(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
set x = E-min L~Cage(C,n);
set p = E-max L~Cage(C,n);
set f = Rotate(Cage(C,n),W-min L~Cage(C,n));
A1: rng f = rng Cage(C,n) by FINSEQ_6:90,SPRECT_2:43;
A2: x in rng Cage(C,n) by SPRECT_2:45;
A3: L~Cage(C,n) = L~f by REVROT_1:33;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A4: E-max L~Cage(C,n) in rng f by FINSEQ_6:90,SPRECT_2:43;
A5: p in rng Cage(C,n) by SPRECT_2:46;
Upper_Seq(C,n) = f-:E-max L~Cage(C,n) by JORDAN1E:def 1;
then Upper_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:44;
then (E-max L~f)..f < (E-min L~f)..f by A3,JORDAN1F:5,SPRECT_5:26;
then x in rng(f:-p) by A1,A2,A5,A3,FINSEQ_6:62;
hence
A6: x in rng Lower_Seq(C,n) by JORDAN1E:def 2;
len Lower_Seq(C,n) >= 2 by TOPREAL1:def 8;
then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18;
hence thesis by A6;
end;
theorem Th12:
for C be compact non vertical non horizontal Subset of TOP-REAL
2 holds S-max L~Cage(C,n) in rng Lower_Seq(C,n) & S-max L~Cage(C,n) in L~
Lower_Seq(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
set x = S-max L~Cage(C,n);
set p = E-max L~Cage(C,n);
set f = Rotate(Cage(C,n),W-min L~Cage(C,n));
A1: rng f = rng Cage(C,n) by FINSEQ_6:90,SPRECT_2:43;
A2: x in rng Cage(C,n) by SPRECT_2:42;
A3: L~Cage(C,n) = L~f by REVROT_1:33;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A4: E-max L~Cage(C,n) in rng f by FINSEQ_6:90,SPRECT_2:43;
A5: p in rng Cage(C,n) by SPRECT_2:46;
Upper_Seq(C,n) = f-:E-max L~Cage(C,n) by JORDAN1E:def 1;
then
A6: Upper_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:44;
then
A7: (E-min L~f)..f <= (S-max L~f)..f by A3,JORDAN1F:5,SPRECT_5:27;
(E-max L~f)..f < (E-min L~f)..f by A6,A3,JORDAN1F:5,SPRECT_5:26;
then x in rng(f:-p) by A1,A2,A5,A3,A7,FINSEQ_6:62,XXREAL_0:2;
hence
A8: x in rng Lower_Seq(C,n) by JORDAN1E:def 2;
len Lower_Seq(C,n) >= 2 by TOPREAL1:def 8;
then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18;
hence thesis by A8;
end;
theorem
for C be compact non vertical non horizontal Subset of TOP-REAL 2
holds S-min L~Cage(C,n) in rng Lower_Seq(C,n) & S-min L~Cage(C,n) in L~
Lower_Seq(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
set x = S-min L~Cage(C,n);
set p = E-max L~Cage(C,n);
set f = Rotate(Cage(C,n),W-min L~Cage(C,n));
A1: rng f = rng Cage(C,n) by FINSEQ_6:90,SPRECT_2:43;
A2: x in rng Cage(C,n) by SPRECT_2:41;
A3: Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by JORDAN1F:5;
A4: L~Cage(C,n) = L~f by REVROT_1:33;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A5: E-max L~Cage(C,n) in rng f by FINSEQ_6:90,SPRECT_2:43;
A6: p in rng Cage(C,n) by SPRECT_2:46;
Upper_Seq(C,n) = f-:E-max L~Cage(C,n) by JORDAN1E:def 1;
then
A7: Upper_Seq(C,n)/.1 = f/.1 by A5,FINSEQ_5:44;
then
A8: (E-max L~f)..f < (E-min L~f)..f by A4,JORDAN1F:5,SPRECT_5:26;
A9: (E-min L~f)..f <= (S-max L~f)..f by A7,A4,JORDAN1F:5,SPRECT_5:27;
per cases;
suppose
S-min L~f <> W-min L~f;
then (E-min L~f)..f < (S-min L~f)..f by A7,A3,A4,A9,SPRECT_5:28,XXREAL_0:2;
then x in rng(f:-p) by A1,A2,A6,A4,A8,FINSEQ_6:62,XXREAL_0:2;
hence
A10: x in rng Lower_Seq(C,n) by JORDAN1E:def 2;
len Lower_Seq(C,n) >= 2 by TOPREAL1:def 8;
then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18;
hence thesis by A10;
end;
suppose
A11: S-min L~f = W-min L~f;
Lower_Seq(C,n)/.(len Lower_Seq(C,n)) = W-min L~Cage(C,n) by JORDAN1F:8;
hence
A12: x in rng Lower_Seq(C,n) by A4,A11,FINSEQ_6:168;
len Lower_Seq(C,n) >= 2 by TOPREAL1:def 8;
then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18;
hence thesis by A12;
end;
end;
theorem
for C be compact non vertical non horizontal Subset of TOP-REAL 2
holds W-min L~Cage(C,n) in rng Lower_Seq(C,n) & W-min L~Cage(C,n) in L~
Lower_Seq(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
set p = W-min L~Cage(C,n);
Lower_Seq(C,n)/.(len Lower_Seq(C,n)) = p by JORDAN1F:8;
hence
A1: p in rng Lower_Seq(C,n) by FINSEQ_6:168;
len Lower_Seq(C,n) >= 2 by TOPREAL1:def 8;
then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18;
hence thesis by A1;
end;
theorem Th15:
for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y &
N-min Y in X holds N-min X = N-min Y
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
assume that
A1: X c= Y and
A2: N-min Y in X;
A3: N-bound X >= (N-min Y)`2 by A2,PSCOMP_1:24;
A4: (N-min X)`2 = N-bound X by EUCLID:52;
A5: (N-min Y)`2 = N-bound Y by EUCLID:52;
A6: N-bound X <= N-bound Y by A1,PSCOMP_1:66;
then
A7: N-bound X = N-bound Y by A5,A3,XXREAL_0:1;
N-min Y in N-most X by A2,A6,A5,A3,SPRECT_2:10,XXREAL_0:1;
then
A8: (N-min X)`1 <= (N-min Y)`1 by PSCOMP_1:39;
N-min X in X by SPRECT_1:11;
then N-min X in N-most Y by A1,A6,A4,A5,A3,SPRECT_2:10,XXREAL_0:1;
then (N-min X)`1 >= (N-min Y)`1 by PSCOMP_1:39;
then (N-min X)`1 = (N-min Y)`1 by A8,XXREAL_0:1;
hence thesis by A4,A5,A7,TOPREAL3:6;
end;
theorem Th16:
for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y &
N-max Y in X holds N-max X = N-max Y
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
assume that
A1: X c= Y and
A2: N-max Y in X;
A3: N-bound X >= (N-max Y)`2 by A2,PSCOMP_1:24;
A4: (N-max X)`2 = N-bound X by EUCLID:52;
A5: (N-max Y)`2 = N-bound Y by EUCLID:52;
A6: N-bound X <= N-bound Y by A1,PSCOMP_1:66;
then
A7: N-bound X = N-bound Y by A5,A3,XXREAL_0:1;
N-max Y in N-most X by A2,A6,A5,A3,SPRECT_2:10,XXREAL_0:1;
then
A8: (N-max X)`1 >= (N-max Y)`1 by PSCOMP_1:39;
N-max X in X by SPRECT_1:11;
then N-max X in N-most Y by A1,A6,A4,A5,A3,SPRECT_2:10,XXREAL_0:1;
then (N-max X)`1 <= (N-max Y)`1 by PSCOMP_1:39;
then (N-max X)`1 = (N-max Y)`1 by A8,XXREAL_0:1;
hence thesis by A4,A5,A7,TOPREAL3:6;
end;
theorem Th17:
for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y &
E-min Y in X holds E-min X = E-min Y
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
assume that
A1: X c= Y and
A2: E-min Y in X;
A3: E-bound X >= (E-min Y)`1 by A2,PSCOMP_1:24;
A4: (E-min X)`1 = E-bound X by EUCLID:52;
A5: (E-min Y)`1 = E-bound Y by EUCLID:52;
A6: E-bound X <= E-bound Y by A1,PSCOMP_1:67;
then
A7: E-bound X = E-bound Y by A5,A3,XXREAL_0:1;
E-min Y in E-most X by A2,A6,A5,A3,SPRECT_2:13,XXREAL_0:1;
then
A8: (E-min X)`2 <= (E-min Y)`2 by PSCOMP_1:47;
E-min X in X by SPRECT_1:14;
then E-min X in E-most Y by A1,A6,A4,A5,A3,SPRECT_2:13,XXREAL_0:1;
then (E-min X)`2 >= (E-min Y)`2 by PSCOMP_1:47;
then (E-min X)`2 = (E-min Y)`2 by A8,XXREAL_0:1;
hence thesis by A4,A5,A7,TOPREAL3:6;
end;
theorem Th18:
for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y &
E-max Y in X holds E-max X = E-max Y
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
assume that
A1: X c= Y and
A2: E-max Y in X;
A3: E-bound X >= (E-max Y)`1 by A2,PSCOMP_1:24;
A4: (E-max X)`1 = E-bound X by EUCLID:52;
A5: (E-max Y)`1 = E-bound Y by EUCLID:52;
A6: E-bound X <= E-bound Y by A1,PSCOMP_1:67;
then
A7: E-bound X = E-bound Y by A5,A3,XXREAL_0:1;
E-max Y in E-most X by A2,A6,A5,A3,SPRECT_2:13,XXREAL_0:1;
then
A8: (E-max X)`2 >= (E-max Y)`2 by PSCOMP_1:47;
E-max X in X by SPRECT_1:14;
then E-max X in E-most Y by A1,A6,A4,A5,A3,SPRECT_2:13,XXREAL_0:1;
then (E-max X)`2 <= (E-max Y)`2 by PSCOMP_1:47;
then (E-max X)`2 = (E-max Y)`2 by A8,XXREAL_0:1;
hence thesis by A4,A5,A7,TOPREAL3:6;
end;
theorem Th19:
for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y &
S-min Y in X holds S-min X = S-min Y
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
assume that
A1: X c= Y and
A2: S-min Y in X;
A3: S-bound X <= (S-min Y)`2 by A2,PSCOMP_1:24;
A4: (S-min X)`2 = S-bound X by EUCLID:52;
A5: (S-min Y)`2 = S-bound Y by EUCLID:52;
A6: S-bound X >= S-bound Y by A1,PSCOMP_1:68;
then
A7: S-bound X = S-bound Y by A5,A3,XXREAL_0:1;
S-min Y in S-most X by A2,A6,A5,A3,SPRECT_2:11,XXREAL_0:1;
then
A8: (S-min X)`1 <= (S-min Y)`1 by PSCOMP_1:55;
S-min X in X by SPRECT_1:12;
then S-min X in S-most Y by A1,A6,A4,A5,A3,SPRECT_2:11,XXREAL_0:1;
then (S-min X)`1 >= (S-min Y)`1 by PSCOMP_1:55;
then (S-min X)`1 = (S-min Y)`1 by A8,XXREAL_0:1;
hence thesis by A4,A5,A7,TOPREAL3:6;
end;
theorem Th20:
for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y &
S-max Y in X holds S-max X = S-max Y
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
assume that
A1: X c= Y and
A2: S-max Y in X;
A3: S-bound X <= (S-max Y)`2 by A2,PSCOMP_1:24;
A4: (S-max X)`2 = S-bound X by EUCLID:52;
A5: (S-max Y)`2 = S-bound Y by EUCLID:52;
A6: S-bound X >= S-bound Y by A1,PSCOMP_1:68;
then
A7: S-bound X = S-bound Y by A5,A3,XXREAL_0:1;
S-max Y in S-most X by A2,A6,A5,A3,SPRECT_2:11,XXREAL_0:1;
then
A8: (S-max X)`1 >= (S-max Y)`1 by PSCOMP_1:55;
S-max X in X by SPRECT_1:12;
then S-max X in S-most Y by A1,A6,A4,A5,A3,SPRECT_2:11,XXREAL_0:1;
then (S-max X)`1 <= (S-max Y)`1 by PSCOMP_1:55;
then (S-max X)`1 = (S-max Y)`1 by A8,XXREAL_0:1;
hence thesis by A4,A5,A7,TOPREAL3:6;
end;
theorem Th21:
for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y &
W-min Y in X holds W-min X = W-min Y
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
assume that
A1: X c= Y and
A2: W-min Y in X;
A3: W-bound X <= (W-min Y)`1 by A2,PSCOMP_1:24;
A4: (W-min X)`1 = W-bound X by EUCLID:52;
A5: (W-min Y)`1 = W-bound Y by EUCLID:52;
A6: W-bound X >= W-bound Y by A1,PSCOMP_1:69;
then
A7: W-bound X = W-bound Y by A5,A3,XXREAL_0:1;
W-min Y in W-most X by A2,A6,A5,A3,SPRECT_2:12,XXREAL_0:1;
then
A8: (W-min X)`2 <= (W-min Y)`2 by PSCOMP_1:31;
W-min X in X by SPRECT_1:13;
then W-min X in W-most Y by A1,A6,A4,A5,A3,SPRECT_2:12,XXREAL_0:1;
then (W-min X)`2 >= (W-min Y)`2 by PSCOMP_1:31;
then (W-min X)`2 = (W-min Y)`2 by A8,XXREAL_0:1;
hence thesis by A4,A5,A7,TOPREAL3:6;
end;
theorem Th22:
for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y &
W-max Y in X holds W-max X = W-max Y
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
assume that
A1: X c= Y and
A2: W-max Y in X;
A3: W-bound X <= (W-max Y)`1 by A2,PSCOMP_1:24;
A4: (W-max X)`1 = W-bound X by EUCLID:52;
A5: (W-max Y)`1 = W-bound Y by EUCLID:52;
A6: W-bound X >= W-bound Y by A1,PSCOMP_1:69;
then
A7: W-bound X = W-bound Y by A5,A3,XXREAL_0:1;
W-max Y in W-most X by A2,A6,A5,A3,SPRECT_2:12,XXREAL_0:1;
then
A8: (W-max X)`2 >= (W-max Y)`2 by PSCOMP_1:31;
W-max X in X by SPRECT_1:13;
then W-max X in W-most Y by A1,A6,A4,A5,A3,SPRECT_2:12,XXREAL_0:1;
then (W-max X)`2 <= (W-max Y)`2 by PSCOMP_1:31;
then (W-max X)`2 = (W-max Y)`2 by A8,XXREAL_0:1;
hence thesis by A4,A5,A7,TOPREAL3:6;
end;
theorem Th23:
for X,Y be non empty compact Subset of TOP-REAL 2 st N-bound X
<= N-bound Y holds N-bound (X\/Y) = N-bound Y
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
assume N-bound X <= N-bound Y;
then max(N-bound X,N-bound Y) = N-bound Y by XXREAL_0:def 10;
hence thesis by SPRECT_1:49;
end;
theorem Th24:
for X,Y be non empty compact Subset of TOP-REAL 2 st E-bound X
<= E-bound Y holds E-bound (X\/Y) = E-bound Y
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
assume E-bound X <= E-bound Y;
then max(E-bound X,E-bound Y) = E-bound Y by XXREAL_0:def 10;
hence thesis by SPRECT_1:50;
end;
theorem Th25:
for X,Y be non empty compact Subset of TOP-REAL 2 st S-bound X
<= S-bound Y holds S-bound (X\/Y) = S-bound X
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
assume S-bound X <= S-bound Y;
then min(S-bound X,S-bound Y) = S-bound X by XXREAL_0:def 9;
hence thesis by SPRECT_1:48;
end;
theorem Th26:
for X,Y be non empty compact Subset of TOP-REAL 2 st W-bound X
<= W-bound Y holds W-bound (X\/Y) = W-bound X
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
assume W-bound X <= W-bound Y;
then min(W-bound X,W-bound Y) = W-bound X by XXREAL_0:def 9;
hence thesis by SPRECT_1:47;
end;
theorem
for X,Y be non empty compact Subset of TOP-REAL 2 st N-bound X <
N-bound Y holds N-min (X\/Y) = N-min Y
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
A1: (N-min(X\/Y))`2 = N-bound (X\/Y) by EUCLID:52;
A2: X\/Y is compact by COMPTS_1:10;
then
A3: N-min(X\/Y) in X\/Y by SPRECT_1:11;
A4: N-min Y in Y by SPRECT_1:11;
A5: (N-min Y)`2 = N-bound Y by EUCLID:52;
assume
A6: N-bound X < N-bound Y;
then
A7: N-bound (X\/Y) = N-bound Y by Th23;
Y c= X\/Y by XBOOLE_1:7;
then N-min Y in N-most(X\/Y) by A2,A7,A5,A4,SPRECT_2:10;
then
A8: (N-min(X\/Y))`1 <= (N-min Y)`1 by A2,PSCOMP_1:39;
per cases by A3,XBOOLE_0:def 3;
suppose
N-min(X\/Y) in Y;
then N-min(X\/Y) in N-most Y by A6,A1,Th23,SPRECT_2:10;
then (N-min(X\/Y))`1 >= (N-min Y)`1 by PSCOMP_1:39;
then (N-min(X\/Y))`1 = (N-min Y)`1 by A8,XXREAL_0:1;
hence thesis by A6,A1,A5,Th23,TOPREAL3:6;
end;
suppose
N-min(X\/Y) in X;
hence thesis by A6,A7,A1,PSCOMP_1:24;
end;
end;
theorem
for X,Y be non empty compact Subset of TOP-REAL 2 st N-bound X <
N-bound Y holds N-max (X\/Y) = N-max Y
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
A1: (N-max(X\/Y))`2 = N-bound (X\/Y) by EUCLID:52;
A2: X\/Y is compact by COMPTS_1:10;
then
A3: N-max(X\/Y) in X\/Y by SPRECT_1:11;
A4: N-max Y in Y by SPRECT_1:11;
A5: (N-max Y)`2 = N-bound Y by EUCLID:52;
assume
A6: N-bound X < N-bound Y;
then
A7: N-bound (X\/Y) = N-bound Y by Th23;
Y c= X\/Y by XBOOLE_1:7;
then N-max Y in N-most(X\/Y) by A2,A7,A5,A4,SPRECT_2:10;
then
A8: (N-max(X\/Y))`1 >= (N-max Y)`1 by A2,PSCOMP_1:39;
per cases by A3,XBOOLE_0:def 3;
suppose
N-max(X\/Y) in Y;
then N-max(X\/Y) in N-most Y by A6,A1,Th23,SPRECT_2:10;
then (N-max(X\/Y))`1 <= (N-max Y)`1 by PSCOMP_1:39;
then (N-max(X\/Y))`1 = (N-max Y)`1 by A8,XXREAL_0:1;
hence thesis by A6,A1,A5,Th23,TOPREAL3:6;
end;
suppose
N-max(X\/Y) in X;
hence thesis by A6,A7,A1,PSCOMP_1:24;
end;
end;
theorem
for X,Y be non empty compact Subset of TOP-REAL 2 st E-bound X <
E-bound Y holds E-min (X\/Y) = E-min Y
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
A1: (E-min(X\/Y))`1 = E-bound (X\/Y) by EUCLID:52;
A2: X\/Y is compact by COMPTS_1:10;
then
A3: E-min(X\/Y) in X\/Y by SPRECT_1:14;
A4: E-min Y in Y by SPRECT_1:14;
A5: (E-min Y)`1 = E-bound Y by EUCLID:52;
assume
A6: E-bound X < E-bound Y;
then
A7: E-bound (X\/Y) = E-bound Y by Th24;
Y c= X\/Y by XBOOLE_1:7;
then E-min Y in E-most(X\/Y) by A2,A7,A5,A4,SPRECT_2:13;
then
A8: (E-min(X\/Y))`2 <= (E-min Y)`2 by A2,PSCOMP_1:47;
per cases by A3,XBOOLE_0:def 3;
suppose
E-min(X\/Y) in Y;
then E-min(X\/Y) in E-most Y by A6,A1,Th24,SPRECT_2:13;
then (E-min(X\/Y))`2 >= (E-min Y)`2 by PSCOMP_1:47;
then (E-min(X\/Y))`2 = (E-min Y)`2 by A8,XXREAL_0:1;
hence thesis by A6,A1,A5,Th24,TOPREAL3:6;
end;
suppose
E-min(X\/Y) in X;
hence thesis by A6,A7,A1,PSCOMP_1:24;
end;
end;
theorem
for X,Y be non empty compact Subset of TOP-REAL 2 st E-bound X <
E-bound Y holds E-max (X\/Y) = E-max Y
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
A1: (E-max(X\/Y))`1 = E-bound (X\/Y) by EUCLID:52;
A2: X\/Y is compact by COMPTS_1:10;
then
A3: E-max(X\/Y) in X\/Y by SPRECT_1:14;
A4: E-max Y in Y by SPRECT_1:14;
A5: (E-max Y)`1 = E-bound Y by EUCLID:52;
assume
A6: E-bound X < E-bound Y;
then
A7: E-bound (X\/Y) = E-bound Y by Th24;
Y c= X\/Y by XBOOLE_1:7;
then E-max Y in E-most(X\/Y) by A2,A7,A5,A4,SPRECT_2:13;
then
A8: (E-max(X\/Y))`2 >= (E-max Y)`2 by A2,PSCOMP_1:47;
per cases by A3,XBOOLE_0:def 3;
suppose
E-max(X\/Y) in Y;
then E-max(X\/Y) in E-most Y by A6,A1,Th24,SPRECT_2:13;
then (E-max(X\/Y))`2 <= (E-max Y)`2 by PSCOMP_1:47;
then (E-max(X\/Y))`2 = (E-max Y)`2 by A8,XXREAL_0:1;
hence thesis by A6,A1,A5,Th24,TOPREAL3:6;
end;
suppose
E-max(X\/Y) in X;
hence thesis by A6,A7,A1,PSCOMP_1:24;
end;
end;
theorem
for X,Y be non empty compact Subset of TOP-REAL 2 st S-bound X <
S-bound Y holds S-min (X\/Y) = S-min X
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
A1: (S-min(X\/Y))`2 = S-bound (X\/Y) by EUCLID:52;
A2: X\/Y is compact by COMPTS_1:10;
then
A3: S-min(X\/Y) in X\/Y by SPRECT_1:12;
A4: S-min X in X by SPRECT_1:12;
A5: (S-min X)`2 = S-bound X by EUCLID:52;
assume
A6: S-bound X < S-bound Y;
then
A7: S-bound (X\/Y) = S-bound X by Th25;
X c= X\/Y by XBOOLE_1:7;
then S-min X in S-most(X\/Y) by A2,A7,A5,A4,SPRECT_2:11;
then
A8: (S-min(X\/Y))`1 <= (S-min X)`1 by A2,PSCOMP_1:55;
per cases by A3,XBOOLE_0:def 3;
suppose
S-min(X\/Y) in X;
then S-min(X\/Y) in S-most X by A6,A1,Th25,SPRECT_2:11;
then (S-min(X\/Y))`1 >= (S-min X)`1 by PSCOMP_1:55;
then (S-min(X\/Y))`1 = (S-min X)`1 by A8,XXREAL_0:1;
hence thesis by A6,A1,A5,Th25,TOPREAL3:6;
end;
suppose
S-min(X\/Y) in Y;
hence thesis by A6,A7,A1,PSCOMP_1:24;
end;
end;
theorem
for X,Y be non empty compact Subset of TOP-REAL 2 st S-bound X <
S-bound Y holds S-max (X\/Y) = S-max X
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
A1: (S-max(X\/Y))`2 = S-bound (X\/Y) by EUCLID:52;
A2: X\/Y is compact by COMPTS_1:10;
then
A3: S-max(X\/Y) in X\/Y by SPRECT_1:12;
A4: S-max X in X by SPRECT_1:12;
A5: (S-max X)`2 = S-bound X by EUCLID:52;
assume
A6: S-bound X < S-bound Y;
then
A7: S-bound (X\/Y) = S-bound X by Th25;
X c= X\/Y by XBOOLE_1:7;
then S-max X in S-most(X\/Y) by A2,A7,A5,A4,SPRECT_2:11;
then
A8: (S-max(X\/Y))`1 >= (S-max X)`1 by A2,PSCOMP_1:55;
per cases by A3,XBOOLE_0:def 3;
suppose
S-max(X\/Y) in X;
then S-max(X\/Y) in S-most X by A6,A1,Th25,SPRECT_2:11;
then (S-max(X\/Y))`1 <= (S-max X)`1 by PSCOMP_1:55;
then (S-max(X\/Y))`1 = (S-max X)`1 by A8,XXREAL_0:1;
hence thesis by A6,A1,A5,Th25,TOPREAL3:6;
end;
suppose
S-max(X\/Y) in Y;
hence thesis by A6,A7,A1,PSCOMP_1:24;
end;
end;
theorem Th33:
for X,Y be non empty compact Subset of TOP-REAL 2 st W-bound X <
W-bound Y holds W-min (X\/Y) = W-min X
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
A1: (W-min(X\/Y))`1 = W-bound (X\/Y) by EUCLID:52;
A2: X\/Y is compact by COMPTS_1:10;
then
A3: W-min(X\/Y) in X\/Y by SPRECT_1:13;
A4: W-min X in X by SPRECT_1:13;
A5: (W-min X)`1 = W-bound X by EUCLID:52;
assume
A6: W-bound X < W-bound Y;
then
A7: W-bound (X\/Y) = W-bound X by Th26;
X c= X\/Y by XBOOLE_1:7;
then W-min X in W-most(X\/Y) by A2,A7,A5,A4,SPRECT_2:12;
then
A8: (W-min(X\/Y))`2 <= (W-min X)`2 by A2,PSCOMP_1:31;
per cases by A3,XBOOLE_0:def 3;
suppose
W-min(X\/Y) in X;
then W-min(X\/Y) in W-most X by A6,A1,Th26,SPRECT_2:12;
then (W-min(X\/Y))`2 >= (W-min X)`2 by PSCOMP_1:31;
then (W-min(X\/Y))`2 = (W-min X)`2 by A8,XXREAL_0:1;
hence thesis by A6,A1,A5,Th26,TOPREAL3:6;
end;
suppose
W-min(X\/Y) in Y;
hence thesis by A6,A7,A1,PSCOMP_1:24;
end;
end;
theorem
for X,Y be non empty compact Subset of TOP-REAL 2 st W-bound X <
W-bound Y holds W-max (X\/Y) = W-max X
proof
let X,Y be non empty compact Subset of TOP-REAL 2;
A1: (W-max(X\/Y))`1 = W-bound (X\/Y) by EUCLID:52;
A2: X\/Y is compact by COMPTS_1:10;
then
A3: W-max(X\/Y) in X\/Y by SPRECT_1:13;
A4: W-max X in X by SPRECT_1:13;
A5: (W-max X)`1 = W-bound X by EUCLID:52;
assume
A6: W-bound X < W-bound Y;
then
A7: W-bound (X\/Y) = W-bound X by Th26;
X c= X\/Y by XBOOLE_1:7;
then W-max X in W-most(X\/Y) by A2,A7,A5,A4,SPRECT_2:12;
then
A8: (W-max(X\/Y))`2 >= (W-max X)`2 by A2,PSCOMP_1:31;
per cases by A3,XBOOLE_0:def 3;
suppose
W-max(X\/Y) in X;
then W-max(X\/Y) in W-most X by A6,A1,Th26,SPRECT_2:12;
then (W-max(X\/Y))`2 <= (W-max X)`2 by PSCOMP_1:31;
then (W-max(X\/Y))`2 = (W-max X)`2 by A8,XXREAL_0:1;
hence thesis by A6,A1,A5,Th26,TOPREAL3:6;
end;
suppose
W-max(X\/Y) in Y;
hence thesis by A6,A7,A1,PSCOMP_1:24;
end;
end;
theorem Th35:
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st f is being_S-Seq & p in L~f holds L_Cut(f,p)/.len L_Cut(f,p) = f/.len f
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume that
A1: f is being_S-Seq and
A2: p in L~f;
A3: len f in dom f by A1,FINSEQ_5:6;
L_Cut(f,p) <> {} by A2,JORDAN1E:3;
then len L_Cut(f,p) in dom L_Cut(f,p) by FINSEQ_5:6;
hence L_Cut(f,p)/.len L_Cut(f,p) = L_Cut(f,p).len L_Cut(f,p) by
PARTFUN1:def 6
.= f.len f by A1,A2,JORDAN1B:4
.= f/.len f by A3,PARTFUN1:def 6;
end;
theorem Th36:
for f be non constant standard special_circular_sequence for p,q
be Point of TOP-REAL 2 for g be connected Subset of TOP-REAL 2 st p in
RightComp f & q in LeftComp f & p in g & q in g holds g meets L~f
proof
let f be non constant standard special_circular_sequence;
let p,q be Point of TOP-REAL 2;
let g be connected Subset of TOP-REAL 2;
assume that
A1: p in RightComp f and
A2: q in LeftComp f and
A3: p in g and
A4: q in g;
assume g misses L~f;
then g c= (L~f)` by TDLAT_1:2;
then reconsider A = g as Subset of (TOP-REAL 2)|(L~f)` by PRE_TOPC:8;
RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
then consider R being Subset of (TOP-REAL 2)|(L~f)` such that
A5: R = RightComp f and
A6: R is a_component by CONNSP_1:def 6;
R /\ A <> {} by A1,A3,A5,XBOOLE_0:def 4;
then
A7: R meets A;
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
then consider L being Subset of (TOP-REAL 2)|(L~f)` such that
A8: L = LeftComp f and
A9: L is a_component by CONNSP_1:def 6;
L /\ A <> {} by A2,A4,A8,XBOOLE_0:def 4;
then
A10: L meets A;
A is connected by CONNSP_1:23;
hence contradiction by A5,A6,A8,A9,A7,A10,JORDAN2C:92,SPRECT_4:6;
end;
registration
cluster non constant standard s.c.c. for
being_S-Seq FinSequence of TOP-REAL 2;
existence
proof
set n = the Nat;
set C = the Simple_closed_curve;
A1: Upper_Seq(C,n) is_sequence_on Gauge(C,n) by JORDAN1G:4;
take Upper_Seq(C,n);
len Upper_Seq(C,n) >= 2 by TOPREAL1:def 8;
hence thesis by A1,JGRAPH_1:12,JORDAN8:5;
end;
end;
theorem Th37:
for f be S-Sequence_in_R2 for p be Point of TOP-REAL 2 st p in
rng f holds L_Cut(f,p) = mid(f,p..f,len f)
proof
let f be S-Sequence_in_R2;
let p be Point of TOP-REAL 2;
A1: len f >= 2 by TOPREAL1:def 8;
assume p in rng f;
then consider i be Nat such that
A2: i in dom f and
A3: f.i = p by FINSEQ_2:10;
A4: 0+1 <= i by A2,FINSEQ_3:25;
A5: i <= len f by A2,FINSEQ_3:25;
per cases by A4,XXREAL_0:1;
suppose
i > 1;
then
A6: Index(p,f) + 1 = i by A3,A5,JORDAN3:12;
then L_Cut(f,p) = mid(f,Index(p,f)+1,len f) by A3,JORDAN3:def 3;
hence thesis by A2,A3,A6,FINSEQ_5:11;
end;
suppose
A7: i = 1;
thus L_Cut(f,p) = L_Cut(f,f/.i) by A2,A3,PARTFUN1:def 6
.= f by A7,JORDAN5B:27
.= mid(f,1,len f) by A1,FINSEQ_6:120,XXREAL_0:2
.= mid(f,p..f,len f) by A2,A3,A7,FINSEQ_5:11;
end;
end;
theorem Th38:
for M be Go-board for f be S-Sequence_in_R2 st f is_sequence_on
M for p be Point of TOP-REAL 2 st p in rng f holds R_Cut(f,p) is_sequence_on M
proof
let M be Go-board;
let f be S-Sequence_in_R2;
assume
A1: f is_sequence_on M;
let p be Point of TOP-REAL 2;
assume p in rng f;
then R_Cut(f,p) = mid(f,1,p..f) by JORDAN1G:49;
hence thesis by A1,JORDAN1H:27;
end;
theorem Th39:
for M be Go-board for f be S-Sequence_in_R2 st f is_sequence_on
M for p be Point of TOP-REAL 2 st p in rng f holds L_Cut(f,p) is_sequence_on M
proof
let M be Go-board;
let f be S-Sequence_in_R2;
assume
A1: f is_sequence_on M;
let p be Point of TOP-REAL 2;
assume p in rng f;
then L_Cut(f,p) = mid(f,p..f,len f) by Th37;
hence thesis by A1,JORDAN1H:27;
end;
theorem Th40:
for G be Go-board for f be FinSequence of TOP-REAL 2 st f
is_sequence_on G for i,j be Nat st 1 <= i & i <= len G & 1 <= j & j
<= width G holds G*(i,j) in L~f implies G*(i,j) in rng f
proof
let G be Go-board;
let f be FinSequence of TOP-REAL 2;
assume
A1: f is_sequence_on G;
let i,j be Nat;
assume that
A2: 1 <= i and
A3: i <= len G and
A4: 1 <= j and
A5: j <= width G;
assume G*(i,j) in L~f;
then consider k be Nat such that
A6: 1 <= k and
A7: k+1 <= len f and
A8: G*(i,j) in LSeg(f/.k,f/.(k+1)) by SPPOL_2:14;
consider i1,j1,i2,j2 be Nat such that
A9: [i1,j1] in Indices G and
A10: f/.k = G*(i1,j1) and
A11: [i2,j2] in Indices G and
A12: f/.(k+1) = G*(i2,j2) and
A13: 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,A6,A7,JORDAN8:3;
A14: 1 <= i1 by A9,MATRIX_0:32;
A15: 1 <= j2 by A11,MATRIX_0:32;
A16: i2 <= len G by A11,MATRIX_0:32;
k+1 >= 1 by NAT_1:11;
then
A17: k+1 in dom f by A7,FINSEQ_3:25;
A18: 1 <= j1 by A9,MATRIX_0:32;
k < len f by A7,NAT_1:13;
then
A19: k in dom f by A6,FINSEQ_3:25;
A20: i1 <= len G by A9,MATRIX_0:32;
A21: j2 <= width G by A11,MATRIX_0:32;
A22: 1 <= i2 by A11,MATRIX_0:32;
A23: j1 <= width G by A9,MATRIX_0:32;
per cases by A13;
suppose
A24: i1 = i2 & j1+1 = j2;
j1 <= j1+1 by NAT_1:11;
then
A25: G*(i1,j1)`2 <= G*(i1,j1+1)`2 by A14,A20,A18,A21,A24,JORDAN1A:19;
then G*(i1,j1)`2 <= G*(i,j)`2 by A8,A10,A12,A24,TOPREAL1:4;
then
A26: j1 <= j by A2,A3,A4,A14,A20,A23,Th2;
A27: G*(i1,j1)`1 <= G*(i1,j1+1)`1 by A14,A20,A18,A23,A15,A21,A24,JORDAN1A:18;
then G*(i1,j1)`1 <= G*(i,j)`1 by A8,A10,A12,A24,TOPREAL1:3;
then
A28: i1 <= i by A2,A4,A5,A20,A18,A23,Th1;
G*(i,j)`2 <= G*(i1,j1+1)`2 by A8,A10,A12,A24,A25,TOPREAL1:4;
then j <= j1+1 by A2,A3,A5,A14,A20,A15,A24,Th2;
then
A29: j = j1 or j = j1+1 by A26,NAT_1:9;
G*(i,j)`1 <= G*(i1,j1+1)`1 by A8,A10,A12,A24,A27,TOPREAL1:3;
then i <= i1 by A3,A4,A5,A14,A15,A21,A24,Th1;
then i = i1 by A28,XXREAL_0:1;
hence thesis by A10,A12,A19,A17,A24,A29,PARTFUN2:2;
end;
suppose
A30: i1+1 = i2 & j1 = j2;
i1 <= i1+1 by NAT_1:11;
then
A31: G*(i1,j1)`1 <= G*(i1+1,j1)`1 by A14,A18,A23,A16,A30,JORDAN1A:18;
then G*(i1,j1)`1 <= G*(i,j)`1 by A8,A10,A12,A30,TOPREAL1:3;
then
A32: i1 <= i by A2,A4,A5,A20,A18,A23,Th1;
A33: G*(i1,j1)`2 <= G*(i1+1,j1)`2 by A14,A20,A18,A23,A22,A16,A30,JORDAN1A:19;
then G*(i1,j1)`2 <= G*(i,j)`2 by A8,A10,A12,A30,TOPREAL1:4;
then
A34: j1 <= j by A2,A3,A4,A14,A20,A23,Th2;
G*(i,j)`1 <= G*(i1+1,j1)`1 by A8,A10,A12,A30,A31,TOPREAL1:3;
then i <= i1+1 by A3,A4,A5,A18,A23,A22,A30,Th1;
then
A35: i = i1 or i = i1+1 by A32,NAT_1:9;
G*(i,j)`2 <= G*(i1+1,j1)`2 by A8,A10,A12,A30,A33,TOPREAL1:4;
then j <= j1 by A2,A3,A5,A18,A22,A16,A30,Th2;
then j = j1 by A34,XXREAL_0:1;
hence thesis by A10,A12,A19,A17,A30,A35,PARTFUN2:2;
end;
suppose
A36: i1 = i2+1 & j1 = j2;
i2 <= i2+1 by NAT_1:11;
then
A37: G*(i2,j1)`1 <= G*(i2+1,j1)`1 by A20,A18,A23,A22,A36,JORDAN1A:18;
then G*(i2,j1)`1 <= G*(i,j)`1 by A8,A10,A12,A36,TOPREAL1:3;
then
A38: i2 <= i by A2,A4,A5,A18,A23,A16,Th1;
A39: G*(i2,j1)`2 <= G*(i2+1,j1)`2 by A14,A20,A18,A23,A22,A16,A36,JORDAN1A:19;
then G*(i2,j1)`2 <= G*(i,j)`2 by A8,A10,A12,A36,TOPREAL1:4;
then
A40: j1 <= j by A2,A3,A4,A23,A22,A16,Th2;
G*(i,j)`1 <= G*(i2+1,j1)`1 by A8,A10,A12,A36,A37,TOPREAL1:3;
then i <= i2+1 by A3,A4,A5,A14,A18,A23,A36,Th1;
then
A41: i = i2 or i = i2+1 by A38,NAT_1:9;
G*(i,j)`2 <= G*(i2+1,j1)`2 by A8,A10,A12,A36,A39,TOPREAL1:4;
then j <= j1 by A2,A3,A5,A14,A20,A18,A36,Th2;
then j = j1 by A40,XXREAL_0:1;
hence thesis by A10,A12,A19,A17,A36,A41,PARTFUN2:2;
end;
suppose
A42: i1 = i2 & j1 = j2+1;
j2 <= j2+1 by NAT_1:11;
then
A43: G*(i1,j2)`2 <= G*(i1,j2+1)`2 by A14,A20,A23,A15,A42,JORDAN1A:19;
then G*(i1,j2)`2 <= G*(i,j)`2 by A8,A10,A12,A42,TOPREAL1:4;
then
A44: j2 <= j by A2,A3,A4,A14,A20,A21,Th2;
A45: G*(i1,j2)`1 <= G*(i1,j2+1)`1 by A14,A20,A18,A23,A15,A21,A42,JORDAN1A:18;
then G*(i1,j2)`1 <= G*(i,j)`1 by A8,A10,A12,A42,TOPREAL1:3;
then
A46: i1 <= i by A2,A4,A5,A20,A15,A21,Th1;
G*(i,j)`2 <= G*(i1,j2+1)`2 by A8,A10,A12,A42,A43,TOPREAL1:4;
then j <= j2+1 by A2,A3,A5,A14,A20,A18,A42,Th2;
then
A47: j = j2 or j = j2+1 by A44,NAT_1:9;
G*(i,j)`1 <= G*(i1,j2+1)`1 by A8,A10,A12,A42,A45,TOPREAL1:3;
then i <= i1 by A3,A4,A5,A14,A18,A23,A42,Th1;
then i = i1 by A46,XXREAL_0:1;
hence thesis by A10,A12,A19,A17,A42,A47,PARTFUN2:2;
end;
end;
theorem
for f be S-Sequence_in_R2 for g be FinSequence of TOP-REAL 2 holds g
is unfolded s.n.c. one-to-one & L~f /\ L~g = {f/.1} & f/.1 = g/.len g & (for i
be Nat st 1<=i & i+2 <= len f holds LSeg(f,i) /\ LSeg(f/.len f,g/.1)
= {}) & (for i be Nat st 2<=i & i+1 <= len g holds LSeg(g,i) /\ LSeg
(f/.len f,g/.1) = {}) implies f^g is s.c.c.
proof
let f be S-Sequence_in_R2;
let g be FinSequence of TOP-REAL 2;
assume that
A1: g is unfolded s.n.c. one-to-one and
A2: L~f /\ L~g = {f/.1} and
A3: f/.1 = g/.len g and
A4: for i be Nat st 1<=i & i+2<=len f holds LSeg(f,i) /\ LSeg
(f/.len f,g/.1) = {} and
A5: for i be Nat st 2<=i & i+1 <= len g holds LSeg(g,i) /\
LSeg(f/.len f,g/.1) = {};
let i,j be Nat such that
A6: i+1 < j and
A7: i > 1 & j < len (f^g) or j+1 < len (f^g);
A8: j+1 <= len (f^g) by A7,NAT_1:13;
A9: for i be Nat st 2 <= i & i+1 <= len g holds
LSeg(g,i) misses LSeg(f/.len f,g/.1) by A5;
A10: for i be Nat st 1 <= i & i+2 <= len f holds
LSeg(f,i) misses LSeg(f/.len f,g/.1) by A4;
per cases;
suppose
i = 0;
then LSeg(f^g,i) = {} by TOPREAL1:def 3;
then LSeg(f^g,i) /\ LSeg(f^g,j) = {};
hence thesis;
end;
suppose
A11: i <> 0;
A12: len(f^g) = len f + len g by FINSEQ_1:22;
i <= i+1 by NAT_1:11;
then
A13: i < j by A6,XXREAL_0:2;
now
per cases;
suppose
A14: j+1 <= len f;
j <= j+1 by NAT_1:11;
then i < j+1 by A13,XXREAL_0:2;
then i < len f by A14,XXREAL_0:2;
then i+1 <= len f by NAT_1:13;
then
A15: LSeg(f^g,i) = LSeg(f,i) by SPPOL_2:6;
LSeg(f^g,j) = LSeg(f,j) by A14,SPPOL_2:6;
hence thesis by A6,A15,TOPREAL1:def 7;
end;
suppose
j+1 > len f;
then
A16: len f <= j by NAT_1:13;
then reconsider j9 = j - len f as Element of NAT by INT_1:5;
A17: j+1-len f <= len g by A8,A12,XREAL_1:20;
then
A18: j9+1 <= len g;
A19: len f + j9 = j;
now
per cases;
suppose
A20: i <= len f;
now
per cases;
suppose
A21: i = len f;
g is non empty by A18;
then
A22: LSeg(f^g,i) = LSeg(f/.len f,g/.1) by A21,SPPOL_2:8;
len f +1+1 <= j by A6,A21,NAT_1:13;
then len f +(1+1) <= j;
then
A23: 1+1 <= j9 by XREAL_1:19;
then LSeg(f^g,j) = LSeg(g,j9) by A19,SPPOL_2:7,XXREAL_0:2;
hence thesis by A9,A18,A23,A22;
end;
suppose
i <> len f;
then i < len f by A20,XXREAL_0:1;
then i+1 <= len f by NAT_1:13;
then
A24: LSeg(f^g,i) = LSeg(f,i) by SPPOL_2:6;
now
per cases;
suppose
A25: j = len f;
then i+1+1 <= len f by A6,NAT_1:13;
then
A26: i+(1+1) <= len f;
g is non empty by A8,A12,A25,XREAL_1:6;
then LSeg(f^g,j) = LSeg(f/.len f,g/.1) by A25,SPPOL_2:8;
hence thesis by A10,A11,A24,A26,NAT_1:14;
end;
suppose
A27: j <> len f;
A28: len f >= 2 by TOPREAL1:def 8;
A29: LSeg(f^g,i) c= L~f by A24,TOPREAL3:19;
len f < j by A16,A27,XXREAL_0:1;
then len f+1 <= j by NAT_1:13;
then
A30: 1 <= j9 by XREAL_1:19;
then
A31: LSeg(f^g,len f+j9) = LSeg(g,j9) by SPPOL_2:7;
then LSeg(f^g,j) c= L~g by TOPREAL3:19;
then
A32: LSeg(f^g,i) /\ LSeg(f^g,j) c= {f/. 1} by A2,A29,XBOOLE_1:27
;
now
per cases by A32,ZFMISC_1:33;
suppose
LSeg(f^g,i) /\ LSeg(f^g,j) = {};
hence thesis;
end;
suppose
LSeg(f^g,i) /\ LSeg(f^g,j) = {f/.1};
then
A33: f/.1 in LSeg(f^g,i) /\ LSeg(f^g,j) by TARSKI:def 1;
then
A34: f/.1 in LSeg(f^g,i) by XBOOLE_0:def 4;
j9 < len g by A18,NAT_1:13;
then
A35: j9 in dom g by A30,FINSEQ_3:25;
j9+1 >= 1 by NAT_1:11;
then
A36: j9+1 in dom g by A17,FINSEQ_3:25;
f/.1 in LSeg(f^g,j) by A33,XBOOLE_0:def 4;
then j9+1=len g by A1,A3,A31,A35,A36,GOBOARD2:2;
hence thesis by A7,A12,A24,A28,A34,JORDAN5B:30;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A37: i > len f;
then j <> len f by A6,NAT_1:13;
then len f < j by A16,XXREAL_0:1;
then len f+1 <= j by NAT_1:13;
then 1 <= j9 by XREAL_1:19;
then
A38: LSeg(f^g,len f+j9) = LSeg(g,j9) by SPPOL_2:7;
reconsider i9 = i - len f as Element of NAT by A37,INT_1:5;
len f + 1 <= i by A37,NAT_1:13;
then 1 <= i9 by XREAL_1:19;
then
A39: LSeg(f^g,len f+i9) = LSeg(g,i9) by SPPOL_2:7;
i+1-len f < j9 by A6,XREAL_1:9;
then i9+1 < j9;
hence thesis by A1,A39,A38,TOPREAL1:def 7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
theorem
for C be compact non vertical non horizontal non empty Subset of
TOP-REAL 2 ex i be Nat st 1 <= i & i+1 <= len Gauge(C,n) & W-min C
in cell(Gauge(C,n),1,i) & W-min C <> Gauge(C,n)*(2,i)
proof
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
set G = Gauge(C,n);
defpred P[Nat] means 1 <= $1 & $1 < len G & G*(2,$1)`2 < (W-min C)`2;
A1: for k be Nat st P[k] holds k <= len G;
A2: len G = width G by JORDAN8:def 1;
(SW-corner C)`2 <= (W-min C)`2 by PSCOMP_1:30;
then
A3: S-bound C <= (W-min C)`2 by EUCLID:52;
A4: len G >= 4 by JORDAN8:10;
then
A5: 1 < len G by XXREAL_0:2;
A6: 2 <= len G by A4,XXREAL_0:2;
then G*(2,2)`2 = S-bound C by JORDAN8:13;
then G*(2,1)`2 < S-bound C by A2,A6,GOBOARD5:4;
then G*(2,1)`2 < (W-min C)`2 by A3,XXREAL_0:2;
then
A7: ex k be Nat st P[k] by A5;
ex i being Nat st P[i] & for n be Nat st P[n] holds n <= i from NAT_1:
sch 6(A1,A7);
then consider i being Nat such that
A8: 1 <= i and
A9: i < len G and
A10: G*(2,i)`2 < (W-min C)`2 and
A11: for n be Nat st P[n] holds n <= i;
reconsider i as Nat;
A12: (W-min C)`1 = W-bound C by EUCLID:52;
then
A13: G*(2,i)`1 = (W-min C)`1 by A8,A9,JORDAN8:11;
A14: i+1 <= len G by A9,NAT_1:13;
then
A15: (W-min C)`1 = G*(2,i+1)`1 by A12,JORDAN8:11,NAT_1:12;
A16: i < i+1 by NAT_1:13;
A17: 1 <= i+1 by NAT_1:12;
now
assume i+1 = len G;
then len G-'1 = i by NAT_D:34;
then
A18: G*(2,i)`2 = N-bound C by A6,JORDAN8:14;
(NW-corner C)`2 >= (W-min C)`2 by PSCOMP_1:30;
hence contradiction by A10,A18,EUCLID:52;
end;
then i+1 < len G by A14,XXREAL_0:1;
then (W-min C)`2 <= G*(2,i+1)`2 by A11,A17,A16;
then
A19: W-min C in LSeg(G*(2,i),G*(2,i+1)) by A10,A13,A15,GOBOARD7:7;
take i;
thus 1 <= i & i+1 <= len G by A8,A9,NAT_1:13;
len G = width G by JORDAN8:def 1;
then LSeg(G*(1+1,i),G*(1+1,i+1)) c= cell(G,1,i) by A5,A8,A9,GOBOARD5:18;
hence W-min C in cell(G,1,i) by A19;
thus thesis by A10;
end;
theorem Th43:
for f be S-Sequence_in_R2 for p be Point of TOP-REAL 2 st p in
L~f & f.len f in L~R_Cut(f,p) holds f.len f = p
proof
let f be S-Sequence_in_R2;
let p be Point of TOP-REAL 2;
assume that
A1: p in L~f and
A2: f.len f in L~R_Cut(f,p);
A3: L~f = L~(Rev f) by SPPOL_2:22;
A4: (Rev f).1 = f.len f by FINSEQ_5:62;
L_Cut(Rev f,p) = Rev R_Cut(f,p) by A1,JORDAN3:22;
then (Rev f).1 in L~L_Cut(Rev f,p) by A2,A4,SPPOL_2:22;
hence thesis by A1,A3,A4,JORDAN1E:7;
end;
theorem Th44:
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
holds R_Cut (f,p) <> {}
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
per cases;
suppose
p<>f.1;
then R_Cut (f,p) = mid(f,1,Index(p,f))^<*p*> by JORDAN3:def 4;
hence thesis;
end;
suppose
p=f.1;
then R_Cut (f,p) = <*p*> by JORDAN3:def 4;
hence thesis;
end;
end;
theorem Th45:
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st p in L~f holds R_Cut(f,p)/.(len R_Cut(f,p)) = p
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume
A1: p in L~f;
R_Cut(f,p) is non empty by Th44;
then len R_Cut(f,p) in dom R_Cut(f,p) by FINSEQ_5:6;
hence R_Cut(f,p)/.len R_Cut(f,p) = R_Cut(f,p).len R_Cut(f,p) by
PARTFUN1:def 6
.= p by A1,JORDAN3:24;
end;
theorem Th46:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for p be Point of TOP-REAL 2 holds p in L~Upper_Seq(C,n) & p`1 =
E-bound L~Cage(C,n) implies p = E-max L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
let p be Point of TOP-REAL 2;
set Ca = Cage(C,n);
set US = Upper_Seq(C,n);
set LS = Lower_Seq(C,n);
set Wmin = W-min L~Ca;
set Smax = S-max L~Ca;
set Smin = S-min L~Ca;
set Emin = E-min L~Ca;
set Emax = E-max L~Ca;
set Wbo = W-bound L~Cage(C,n);
set Nbo = N-bound L~Cage(C,n);
set Ebo = E-bound L~Cage(C,n);
set Sbo = S-bound L~Cage(C,n);
set NE = NE-corner L~Ca;
assume that
A1: p in L~Upper_Seq(C,n) and
A2: p`1 = E-bound L~Cage(C,n) and
A3: p <> E-max L~Cage(C,n);
A4: US/.1 = Wmin by JORDAN1F:5;
1 in dom US by FINSEQ_5:6;
then
A5: US.1 = Wmin by A4,PARTFUN1:def 6;
Wbo <> Ebo by SPRECT_1:31;
then p <> US.1 by A2,A5,EUCLID:52;
then reconsider
g = R_Cut(US,p) as being_S-Seq FinSequence of TOP-REAL 2 by A1,JORDAN3:35;
<*p*> is_in_the_area_of Ca by A1,JORDAN1E:17,SPRECT_3:46;
then
A6: g is_in_the_area_of Ca by A1,JORDAN1E:17,SPRECT_3:52;
len g in dom g by FINSEQ_5:6;
then
A7: g/.len g = g.len g by PARTFUN1:def 6
.= p by A1,JORDAN3:24;
(g/.1)`1 = (US/.1)`1 by A1,SPRECT_3:22
.= Wmin`1 by JORDAN1F:5
.= Wbo by EUCLID:52;
then
A8: g is_a_h.c._for Ca by A2,A6,A7,SPRECT_2:def 2;
A9: LS/.1 = Emax by JORDAN1F:6;
1 in dom LS by FINSEQ_5:6;
then
A10: LS.1 = Emax by A9,PARTFUN1:def 6;
len Cage(C,n) > 4 by GOBOARD7:34;
then
A11: rng Cage(C,n) c= L~Cage(C,n) by SPPOL_2:18,XXREAL_0:2;
now
per cases;
suppose
A12: Emax <> NE;
A13: not NE in rng Cage(C,n)
proof
A14: NE`1 = E-bound L~Cage(C,n) by EUCLID:52;
A15: NE`2 = N-bound L~Cage(C,n) by EUCLID:52;
then NE`2 >= S-bound L~Cage(C,n) by SPRECT_1:22;
then NE in { p1 where p1 is Point of TOP-REAL 2 : p1`1 = E-bound L~
Cage(C,n) & p1`2 <= N-bound L~Cage(C,n) & p1`2 >= S-bound L~Cage(C,n) } by A14
,A15;
then
A16: NE in LSeg(SE-corner L~Cage(C,n), NE-corner L~Cage(C,n)) by SPRECT_1:23
;
assume NE in rng Cage(C,n);
then NE in LSeg(SE-corner L~Cage(C,n), NE-corner L~Cage(C,n)) /\ L~
Cage(C,n) by A11,A16,XBOOLE_0:def 4;
then
A17: NE`2 <= (E-max L~Cage(C,n))`2 by PSCOMP_1:47;
A18: (E-max L~Cage(C,n))`1 = NE`1 by PSCOMP_1:45;
(E-max L~Cage(C,n))`2 <= NE`2 by PSCOMP_1:46;
then (E-max L~Cage(C,n))`2 = NE`2 by A17,XXREAL_0:1;
hence contradiction by A12,A18,TOPREAL3:6;
end;
Smax in rng LS by Th12;
then R_Cut(LS,Smax) = mid(LS,1,Smax..LS) by JORDAN1G:49;
then
A19: rng R_Cut(LS,Smax) c= rng LS by FINSEQ_6:119;
rng LS c= rng Ca by JORDAN1G:39;
then rng R_Cut(LS,Smax) c= rng Ca by A19;
then not NE in rng R_Cut(LS,Smax) by A13;
then rng R_Cut(LS,Smax) misses {NE} by ZFMISC_1:50;
then rng R_Cut(LS,Smax) misses rng <*NE*> by FINSEQ_1:38;
then
A20: rng Rev R_Cut(LS,Smax) misses rng <*NE*> by FINSEQ_5:57;
set h = Rev R_Cut(LS,Smax)^<*NE*>;
A21: <*NE*> is one-to-one by FINSEQ_3:93;
A22: (h/.len h)`2 = (h/.(len Rev R_Cut(LS,Smax)+1))`2 by FINSEQ_2:16
.= NE`2 by FINSEQ_4:67
.= Nbo by EUCLID:52;
Emin in L~Ca by SPRECT_1:14;
then
A23: Sbo <= Emin`2 by PSCOMP_1:24;
A24: Index(Smax,LS)+1 >= 0+1 by XREAL_1:7;
A25: Smax in L~LS by Th12;
then <*Smax*> is_in_the_area_of Ca by JORDAN1E:18,SPRECT_3:46;
then R_Cut(LS,Smax) is_in_the_area_of Ca by A25,JORDAN1E:18,SPRECT_3:52;
then
A26: Rev R_Cut(LS,Smax) is_in_the_area_of Ca by SPRECT_3:51;
Emin`2 < Emax`2 by SPRECT_2:53;
then
A27: Smax <> LS.1 by A10,A23,EUCLID:52;
then reconsider RCutLS = R_Cut(LS,Smax) as being_S-Seq FinSequence of
TOP-REAL 2 by A25,JORDAN3:35;
len h = len Rev R_Cut(LS,Smax) + 1 by FINSEQ_2:16
.= len R_Cut(LS,Smax) + 1 by FINSEQ_5:def 3
.= Index(Smax,LS)+1+1 by A25,A27,JORDAN3:25;
then
A28: len h >= 1+1 by A24,XREAL_1:7;
A29: 2 <= len g by TOPREAL1:def 8;
1 in dom Rev RCutLS by FINSEQ_5:6;
then h/.1 = Rev RCutLS/.1 by FINSEQ_4:68
.= R_Cut(LS,Smax)/.len R_Cut(LS,Smax) by FINSEQ_5:65
.= Smax by A25,Th45;
then
A30: (h/.1)`2 = Sbo by EUCLID:52;
<*NE*> is_in_the_area_of Ca by SPRECT_2:25;
then h is_in_the_area_of Ca by A26,SPRECT_2:24;
then
A31: h is_a_v.c._for Ca by A30,A22,SPRECT_2:def 3;
A32: len LS in dom LS by FINSEQ_5:6;
A33: Rev RCutLS/.len Rev RCutLS = Rev RCutLS/.len RCutLS by FINSEQ_5:def 3
.= RCutLS/.1 by FINSEQ_5:65
.= LS/.1 by A25,SPRECT_3:22
.= Emax by JORDAN1F:6;
then (Rev RCutLS/.len Rev RCutLS)`1 = E-bound L~Ca by EUCLID:52
.= NE`1 by EUCLID:52
.= (<*NE*>/.1)`1 by FINSEQ_4:16;
then h is one-to-one special by A20,A21,FINSEQ_3:91,GOBOARD2:8;
then L~g meets L~h by A8,A29,A28,A31,SPRECT_2:29;
then consider x be object such that
A34: x in L~g and
A35: x in L~h by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A34;
A36: L~h = L~Rev RCutLS \/ LSeg(Rev RCutLS/.len Rev RCutLS,NE) by SPPOL_2:19;
A37: L~RCutLS c= L~LS by Th12,JORDAN3:41;
A38: len US in dom US by FINSEQ_5:6;
A39: L~g c= L~US by A1,JORDAN3:41;
then
A40: x in L~US by A34;
now
per cases by A35,A36,XBOOLE_0:def 3;
suppose
x in L~Rev RCutLS;
then
A41: x in L~RCutLS by SPPOL_2:22;
then x in L~US /\ L~LS by A34,A39,A37,XBOOLE_0:def 4;
then
A42: x in {Wmin,Emax} by JORDAN1E:16;
now
per cases by A42,TARSKI:def 2;
suppose
x = Wmin;
then LS/.len LS in L~R_Cut(LS,Smax) by A41,JORDAN1F:8;
then LS.len LS in L~R_Cut(LS,Smax) by A32,PARTFUN1:def 6;
then LS.len LS = Smax by A25,Th43;
then LS/.len LS = Smax by A32,PARTFUN1:def 6;
then
A43: Wmin = Smax by JORDAN1F:8;
Smin in L~Ca by SPRECT_1:12;
then
A44: Wbo <= Smin`1 by PSCOMP_1:24;
Smin`1 < Smax`1 by SPRECT_2:55;
hence contradiction by A43,A44,EUCLID:52;
end;
suppose
x = Emax;
then US/.len US in L~R_Cut(US,p) by A34,JORDAN1F:7;
then US.len US in L~R_Cut(US,p) by A38,PARTFUN1:def 6;
then US.len US = p by A1,Th43;
then US/.len US = p by A38,PARTFUN1:def 6;
hence contradiction by A3,JORDAN1F:7;
end;
end;
hence contradiction;
end;
suppose
A45: x in LSeg(Rev RCutLS/.len Rev RCutLS,NE);
Emax`2 <= NE`2 by PSCOMP_1:46;
then
A46: Emax`2 <= x`2 by A33,A45,TOPREAL1:4;
A47: Emax`1 = Ebo by EUCLID:52;
NE`1 = Ebo by EUCLID:52;
then
A48: x`1 = Ebo by A33,A45,A47,GOBOARD7:5;
L~Ca = L~US \/ L~LS by JORDAN1E:13;
then L~US c= L~Ca by XBOOLE_1:7;
then x in E-most L~Ca by A40,A48,SPRECT_2:13;
then x`2 <= Emax`2 by PSCOMP_1:47;
then x`2 = Emax`2 by A46,XXREAL_0:1;
then x = Emax by A47,A48,TOPREAL3:6;
then US/.len US in L~R_Cut(US,p) by A34,JORDAN1F:7;
then US.len US in L~R_Cut(US,p) by A38,PARTFUN1:def 6;
then US.len US = p by A1,Th43;
then US/.len US = p by A38,PARTFUN1:def 6;
hence contradiction by A3,JORDAN1F:7;
end;
end;
hence contradiction;
end;
suppose
A49: Emax = NE;
Emin in L~Ca by SPRECT_1:14;
then
A50: Sbo <= Emin`2 by PSCOMP_1:24;
set h = Rev R_Cut(LS,Smax);
A51: 2 <= len g by TOPREAL1:def 8;
A52: Smax in L~LS by Th12;
then <*Smax*> is_in_the_area_of Ca by JORDAN1E:18,SPRECT_3:46;
then R_Cut(LS,Smax) is_in_the_area_of Ca by A52,JORDAN1E:18,SPRECT_3:52;
then
A53: h is_in_the_area_of Ca by SPRECT_3:51;
Emin`2 < Emax`2 by SPRECT_2:53;
then Smax <> LS.1 by A10,A50,EUCLID:52;
then reconsider RCutLS = R_Cut(LS,Smax) as being_S-Seq FinSequence of
TOP-REAL 2 by A52,JORDAN3:35;
1 in dom Rev RCutLS by FINSEQ_5:6;
then h/.1 = R_Cut(LS,Smax)/.len R_Cut(LS,Smax) by FINSEQ_5:65
.= Smax by A52,Th45;
then
A54: (h/.1)`2 = Sbo by EUCLID:52;
A55: Rev RCutLS is special;
len RCutLS >= 2 by TOPREAL1:def 8;
then
A56: len h >= 2 by FINSEQ_5:def 3;
Rev RCutLS/.len Rev RCutLS = Rev RCutLS/.len RCutLS by FINSEQ_5:def 3
.= RCutLS/.1 by FINSEQ_5:65
.= LS/.1 by A52,SPRECT_3:22
.= Emax by JORDAN1F:6;
then (h/.len h)`2 = Nbo by A49,EUCLID:52;
then h is_a_v.c._for Ca by A53,A54,SPRECT_2:def 3;
then L~g meets L~h by A8,A55,A51,A56,SPRECT_2:29;
then consider x be object such that
A57: x in L~g and
A58: x in L~h by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A57;
A59: x in L~RCutLS by A58,SPPOL_2:22;
A60: L~g c= L~US by A1,JORDAN3:41;
A61: len US in dom US by FINSEQ_5:6;
A62: len LS in dom LS by FINSEQ_5:6;
L~RCutLS c= L~LS by Th12,JORDAN3:41;
then x in L~US /\ L~LS by A57,A60,A59,XBOOLE_0:def 4;
then
A63: x in {Wmin,Emax} by JORDAN1E:16;
now
per cases by A63,TARSKI:def 2;
suppose
x = Wmin;
then LS/.len LS in L~R_Cut(LS,Smax) by A59,JORDAN1F:8;
then LS.len LS in L~R_Cut(LS,Smax) by A62,PARTFUN1:def 6;
then LS.len LS = Smax by A52,Th43;
then LS/.len LS = Smax by A62,PARTFUN1:def 6;
then
A64: Wmin = Smax by JORDAN1F:8;
Smin in L~Ca by SPRECT_1:12;
then
A65: Wbo <= Smin`1 by PSCOMP_1:24;
Smin`1 < Smax`1 by SPRECT_2:55;
hence contradiction by A64,A65,EUCLID:52;
end;
suppose
x = Emax;
then US/.len US in L~R_Cut(US,p) by A57,JORDAN1F:7;
then US.len US in L~R_Cut(US,p) by A61,PARTFUN1:def 6;
then US.len US = p by A1,Th43;
then US/.len US = p by A61,PARTFUN1:def 6;
hence contradiction by A3,JORDAN1F:7;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
theorem
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for p be Point of TOP-REAL 2 holds p in L~Lower_Seq(C,n) & p`1 =
W-bound L~Cage(C,n) implies p = W-min L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
let p be Point of TOP-REAL 2;
set Ca = Cage(C,n);
set LS = Lower_Seq(C,n);
set US = Upper_Seq(C,n);
set Emax = E-max L~Ca;
set Nmin = N-min L~Ca;
set Nmax = N-max L~Ca;
set Wmax = W-max L~Ca;
set Wmin = W-min L~Ca;
set Ebo = E-bound L~Cage(C,n);
set Sbo = S-bound L~Cage(C,n);
set Wbo = W-bound L~Cage(C,n);
set Nbo = N-bound L~Cage(C,n);
set SW = SW-corner L~Ca;
assume that
A1: p in L~Lower_Seq(C,n) and
A2: p`1 = W-bound L~Cage(C,n) and
A3: p <> W-min L~Cage(C,n);
A4: LS/.1 = Emax by JORDAN1F:6;
1 in dom LS by FINSEQ_5:6;
then
A5: LS.1 = Emax by A4,PARTFUN1:def 6;
Ebo <> Wbo by SPRECT_1:31;
then p <> LS.1 by A2,A5,EUCLID:52;
then reconsider
g1 = R_Cut(LS,p) as being_S-Seq FinSequence of TOP-REAL 2 by A1,JORDAN3:35;
len g1 in dom g1 by FINSEQ_5:6;
then
A6: g1/.len g1 = g1.len g1 by PARTFUN1:def 6
.= p by A1,JORDAN3:24;
reconsider g = Rev g1 as being_S-Seq FinSequence of TOP-REAL 2;
<*p*> is_in_the_area_of Ca by A1,JORDAN1E:18,SPRECT_3:46;
then g1 is_in_the_area_of Ca by A1,JORDAN1E:18,SPRECT_3:52;
then
A7: g is_in_the_area_of Ca by SPRECT_3:51;
A8: g/.1 = g1/.len g1 by FINSEQ_5:65;
A9: g/.len g = g/.len g1 by FINSEQ_5:def 3
.= g1/.1 by FINSEQ_5:65;
(g1/.1)`1 = (LS/.1)`1 by A1,SPRECT_3:22
.= Emax`1 by JORDAN1F:6
.= Ebo by EUCLID:52;
then
A10: g is_a_h.c._for Ca by A2,A7,A8,A9,A6,SPRECT_2:def 2;
A11: US/.1 = Wmin by JORDAN1F:5;
1 in dom US by FINSEQ_5:6;
then
A12: US.1 = Wmin by A11,PARTFUN1:def 6;
A13: L~g = L~g1 by SPPOL_2:22;
len Cage(C,n) > 4 by GOBOARD7:34;
then
A14: rng Cage(C,n) c= L~Cage(C,n) by SPPOL_2:18,XXREAL_0:2;
now
per cases;
suppose
A15: Wmin <> SW;
A16: not SW in rng Cage(C,n)
proof
A17: SW`1 = W-bound L~Cage(C,n) by EUCLID:52;
A18: SW`2 = S-bound L~Cage(C,n) by EUCLID:52;
then SW`2 <= N-bound L~Cage(C,n) by SPRECT_1:22;
then SW in { p1 where p1 is Point of TOP-REAL 2 : p1`1 = W-bound L~
Cage(C,n) & p1`2 <= N-bound L~Cage(C,n) & p1`2 >= S-bound L~Cage(C,n) } by A17
,A18;
then
A19: SW in LSeg(SW-corner L~Cage(C,n), NW-corner L~Cage(C,n)) by SPRECT_1:26
;
assume SW in rng Cage(C,n);
then SW in LSeg(SW-corner L~Cage(C,n), NW-corner L~Cage(C,n)) /\ L~
Cage(C,n) by A14,A19,XBOOLE_0:def 4;
then
A20: SW`2 >= (W-min L~Cage(C,n))`2 by PSCOMP_1:31;
A21: (W-min L~Cage(C,n))`1 = SW`1 by PSCOMP_1:29;
(W-min L~Cage(C,n))`2 >= SW`2 by PSCOMP_1:30;
then (W-min L~Cage(C,n))`2 = SW`2 by A20,XXREAL_0:1;
hence contradiction by A15,A21,TOPREAL3:6;
end;
Nmin in rng US by Th7;
then R_Cut(US,Nmin) = mid(US,1,Nmin..US) by JORDAN1G:49;
then
A22: rng R_Cut(US,Nmin) c= rng US by FINSEQ_6:119;
rng US c= rng Ca by JORDAN1G:39;
then rng R_Cut(US,Nmin) c= rng Ca by A22;
then not SW in rng R_Cut(US,Nmin) by A16;
then rng R_Cut(US,Nmin) misses {SW} by ZFMISC_1:50;
then rng R_Cut(US,Nmin) misses rng <*SW*> by FINSEQ_1:38;
then
A23: rng Rev R_Cut(US,Nmin) misses rng <*SW*> by FINSEQ_5:57;
set h1 = Rev R_Cut(US,Nmin)^<*SW*>;
A24: <*SW*> is one-to-one by FINSEQ_3:93;
Wmax in L~Ca by SPRECT_1:13;
then
A25: Nbo >= Wmax`2 by PSCOMP_1:24;
A26: Nmin in L~US by Th7;
then <*Nmin*> is_in_the_area_of Ca by JORDAN1E:17,SPRECT_3:46;
then R_Cut(US,Nmin) is_in_the_area_of Ca by A26,JORDAN1E:17,SPRECT_3:52;
then
A27: Rev R_Cut(US,Nmin) is_in_the_area_of Ca by SPRECT_3:51;
Wmax`2 > Wmin`2 by SPRECT_2:57;
then
A28: Nmin <> US.1 by A12,A25,EUCLID:52;
then reconsider RCutUS = R_Cut(US,Nmin) as being_S-Seq FinSequence of
TOP-REAL 2 by A26,JORDAN3:35;
A29: Rev RCutUS/.len Rev RCutUS = Rev RCutUS/.len RCutUS by FINSEQ_5:def 3
.= RCutUS/.1 by FINSEQ_5:65
.= US/.1 by A26,SPRECT_3:22
.= Wmin by JORDAN1F:5;
then (Rev RCutUS/.len Rev RCutUS)`1 = W-bound L~Ca by EUCLID:52
.= SW`1 by EUCLID:52
.= (<*SW*>/.1)`1 by FINSEQ_4:16;
then reconsider
h1 as one-to-one special FinSequence of TOP-REAL 2 by A23,A24,FINSEQ_3:91
,GOBOARD2:8;
set h = Rev h1;
A30: h is special by SPPOL_2:40;
<*SW*> is_in_the_area_of Ca by SPRECT_2:28;
then h1 is_in_the_area_of Ca by A27,SPRECT_2:24;
then
A31: h is_in_the_area_of Ca by SPRECT_3:51;
L~h = L~h1 by SPPOL_2:22;
then
A32: L~h = L~Rev RCutUS \/ LSeg(Rev RCutUS/.len Rev RCutUS,SW) by SPPOL_2:19;
A33: Index(Nmin,US)+1 >= 0+1 by XREAL_1:7;
A34: 2 <= len g by TOPREAL1:def 8;
len h1 = len Rev R_Cut(US,Nmin) + 1 by FINSEQ_2:16
.= len R_Cut(US,Nmin) + 1 by FINSEQ_5:def 3
.= Index(Nmin,US)+1+1 by A26,A28,JORDAN3:25;
then len h1 >= 1+1 by A33,XREAL_1:7;
then
A35: len h >= 2 by FINSEQ_5:def 3;
A36: h/.1 = h1/.len h1 by FINSEQ_5:65;
A37: len US in dom US by FINSEQ_5:6;
1 in dom Rev RCutUS by FINSEQ_5:6;
then h1/.1 = Rev RCutUS/.1 by FINSEQ_4:68
.= R_Cut(US,Nmin)/.len R_Cut(US,Nmin) by FINSEQ_5:65
.= Nmin by A26,Th45;
then
A38: (h1/.1)`2 = Nbo by EUCLID:52;
A39: (h1/.len h1)`2 = (h1/.(len Rev R_Cut(US,Nmin)+1))`2 by FINSEQ_2:16
.= SW`2 by FINSEQ_4:67
.= Sbo by EUCLID:52;
A40: len LS in dom LS by FINSEQ_5:6;
h/.len h = h/.len h1 by FINSEQ_5:def 3
.= h1/.1 by FINSEQ_5:65;
then h is_a_v.c._for Ca by A31,A38,A36,A39,SPRECT_2:def 3;
then L~g meets L~h by A10,A30,A34,A35,SPRECT_2:29;
then consider x be object such that
A41: x in L~g and
A42: x in L~h by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A41;
A43: L~RCutUS c= L~US by Th7,JORDAN3:41;
A44: L~g c= L~LS by A1,A13,JORDAN3:41;
then
A45: x in L~LS by A41;
now
per cases by A42,A32,XBOOLE_0:def 3;
suppose
x in L~Rev RCutUS;
then
A46: x in L~RCutUS by SPPOL_2:22;
then x in L~LS /\ L~US by A41,A44,A43,XBOOLE_0:def 4;
then
A47: x in {Emax,Wmin} by JORDAN1E:16;
now
per cases by A47,TARSKI:def 2;
suppose
x = Emax;
then US/.len US in L~R_Cut(US,Nmin) by A46,JORDAN1F:7;
then US.len US in L~R_Cut(US,Nmin) by A37,PARTFUN1:def 6;
then US.len US = Nmin by A26,Th43;
then US/.len US = Nmin by A37,PARTFUN1:def 6;
then
A48: Emax = Nmin by JORDAN1F:7;
Nmax in L~Ca by SPRECT_1:11;
then
A49: Ebo >= Nmax`1 by PSCOMP_1:24;
Nmax`1 > Nmin`1 by SPRECT_2:51;
hence contradiction by A48,A49,EUCLID:52;
end;
suppose
x = Wmin;
then LS/.len LS in L~R_Cut(LS,p) by A13,A41,JORDAN1F:8;
then LS.len LS in L~R_Cut(LS,p) by A40,PARTFUN1:def 6;
then LS.len LS = p by A1,Th43;
then LS/.len LS = p by A40,PARTFUN1:def 6;
hence contradiction by A3,JORDAN1F:8;
end;
end;
hence contradiction;
end;
suppose
A50: x in LSeg(Rev RCutUS/.len Rev RCutUS,SW);
Wmin`2 >= SW`2 by PSCOMP_1:30;
then
A51: Wmin`2 >= x`2 by A29,A50,TOPREAL1:4;
A52: Wmin`1 = Wbo by EUCLID:52;
SW`1 = Wbo by EUCLID:52;
then
A53: x`1 = Wbo by A29,A50,A52,GOBOARD7:5;
L~Ca = L~LS \/ L~US by JORDAN1E:13;
then L~LS c= L~Ca by XBOOLE_1:7;
then x in W-most L~Ca by A45,A53,SPRECT_2:12;
then x`2 >= Wmin`2 by PSCOMP_1:31;
then x`2 = Wmin`2 by A51,XXREAL_0:1;
then x = Wmin by A52,A53,TOPREAL3:6;
then LS/.len LS in L~R_Cut(LS,p) by A13,A41,JORDAN1F:8;
then LS.len LS in L~R_Cut(LS,p) by A40,PARTFUN1:def 6;
then LS.len LS = p by A1,Th43;
then LS/.len LS = p by A40,PARTFUN1:def 6;
hence contradiction by A3,JORDAN1F:8;
end;
end;
hence contradiction;
end;
suppose
A54: Wmin = SW;
set h = R_Cut(US,Nmin);
A55: 2 <= len g by TOPREAL1:def 8;
Wmax in L~Ca by SPRECT_1:13;
then
A56: Nbo >= Wmax`2 by PSCOMP_1:24;
A57: Nmin in L~US by Th7;
then <*Nmin*> is_in_the_area_of Ca by JORDAN1E:17,SPRECT_3:46;
then
A58: R_Cut(US,Nmin) is_in_the_area_of Ca by A57,JORDAN1E:17,SPRECT_3:52;
Wmax`2 > Wmin`2 by SPRECT_2:57;
then Nmin <> US.1 by A12,A56,EUCLID:52;
then reconsider RCutUS = R_Cut(US,Nmin) as being_S-Seq FinSequence of
TOP-REAL 2 by A57,JORDAN3:35;
A59: len RCutUS >= 2 by TOPREAL1:def 8;
R_Cut(US,Nmin)/.len R_Cut(US,Nmin) = Nmin by A57,Th45;
then
A60: (h/.len h)`2 = Nbo by EUCLID:52;
RCutUS/.1 = US/.1 by A57,SPRECT_3:22
.= Wmin by JORDAN1F:5;
then (h/.1)`2 = Sbo by A54,EUCLID:52;
then h is_a_v.c._for Ca by A58,A60,SPRECT_2:def 3;
then L~g meets L~h by A10,A55,A59,SPRECT_2:29;
then consider x be object such that
A61: x in L~g and
A62: x in L~h by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A61;
A63: len LS in dom LS by FINSEQ_5:6;
A64: L~g c= L~LS by A1,A13,JORDAN3:41;
A65: len US in dom US by FINSEQ_5:6;
L~RCutUS c= L~US by Th7,JORDAN3:41;
then x in L~LS /\ L~US by A61,A62,A64,XBOOLE_0:def 4;
then
A66: x in {Emax,Wmin} by JORDAN1E:16;
now
per cases by A66,TARSKI:def 2;
suppose
x = Emax;
then US/.len US in L~R_Cut(US,Nmin) by A62,JORDAN1F:7;
then US.len US in L~R_Cut(US,Nmin) by A65,PARTFUN1:def 6;
then US.len US = Nmin by A57,Th43;
then US/.len US = Nmin by A65,PARTFUN1:def 6;
then
A67: Emax = Nmin by JORDAN1F:7;
Nmax in L~Ca by SPRECT_1:11;
then
A68: Ebo >= Nmax`1 by PSCOMP_1:24;
Nmax`1 > Nmin`1 by SPRECT_2:51;
hence contradiction by A67,A68,EUCLID:52;
end;
suppose
x = Wmin;
then LS/.len LS in L~R_Cut(LS,p) by A13,A61,JORDAN1F:8;
then LS.len LS in L~R_Cut(LS,p) by A63,PARTFUN1:def 6;
then LS.len LS = p by A1,Th43;
then LS/.len LS = p by A63,PARTFUN1:def 6;
hence contradiction by A3,JORDAN1F:8;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
theorem
for G be Go-board for f,g be FinSequence of TOP-REAL 2 for k be
Nat holds 1 <= k & k < len f & f^g is_sequence_on G implies
left_cell(f^g,k,G) = left_cell(f,k,G) & right_cell(f^g,k,G) = right_cell(f,k,G)
proof
let G be Go-board;
let f,g be FinSequence of TOP-REAL 2;
let k be Nat;
assume that
A1: 1 <= k and
A2: k < len f and
A3: f^g is_sequence_on G;
A4: k+1 <= len f by A2,NAT_1:13;
A5: (f^g)|len f = f by FINSEQ_5:23;
len f <= len f + len g by NAT_1:11;
then len f <= len (f^g) by FINSEQ_1:22;
then k+1 <= len (f^g) by A4,XXREAL_0:2;
hence thesis by A1,A3,A5,A4,GOBRD13:31;
end;
theorem Th49:
for D be set for f,g be FinSequence of D for i be Nat
st i <= len f holds (f^'g)|i = f|i
proof
let D be set;
let f,g be FinSequence of D;
let i be Nat;
assume
A1: i <= len f;
then
A2: len(f|i) = i by FINSEQ_1:59;
per cases;
suppose
A3: g <> {};
then len g >= 0+1 by NAT_1:13;
then i+1 <= len f+len g by A1,XREAL_1:7;
then i+1 <= len(f^'g)+1 by A3,FINSEQ_6:139;
then i <= len(f^'g) by XREAL_1:6;
then
A4: len((f^'g)|i) = i by FINSEQ_1:59;
then
A5: dom ((f^'g)|i) = Seg i by FINSEQ_1:def 3;
now
let j be Nat;
assume
A6: j in dom((f^'g)|i);
then
A7: 1 <= j by A5,FINSEQ_1:1;
j <= i by A5,A6,FINSEQ_1:1;
then
A8: j <= len f by A1,XXREAL_0:2;
thus ((f^'g)|i).j = ((f^'g)|(Seg i)).j by FINSEQ_1:def 16
.= (f^'g).j by A5,A6,FUNCT_1:49
.= f.j by A7,A8,FINSEQ_6:140
.= (f|(Seg i)).j by A5,A6,FUNCT_1:49
.= (f|i).j by FINSEQ_1:def 16;
end;
hence thesis by A2,A4,FINSEQ_2:9;
end;
suppose
g = {};
hence thesis by FINSEQ_6:157;
end;
end;
theorem Th50:
for D be set for f,g be FinSequence of D holds (f^'g)|(len f) = f
proof
let D be set;
let f,g be FinSequence of D;
f|len f = f|(Seg len f) by FINSEQ_1:def 16;
hence thesis by Th49,FINSEQ_2:20;
end;
theorem Th51:
for G be Go-board for f,g be FinSequence of TOP-REAL 2 for k be
Nat holds 1 <= k & k < len f & f^'g is_sequence_on G implies
left_cell(f^'g,k,G) = left_cell(f,k,G) & right_cell(f^'g,k,G) = right_cell(f,k,
G)
proof
let G be Go-board;
let f,g be FinSequence of TOP-REAL 2;
let k be Nat;
assume that
A1: 1 <= k and
A2: k < len f and
A3: f^'g is_sequence_on G;
A4: k+1 <= len f by A2,NAT_1:13;
A5: (f^'g)|len f = f by Th50;
len f <= len (f^'g) by TOPREAL8:7;
then k+1 <= len (f^'g) by A4,XXREAL_0:2;
hence thesis by A1,A3,A5,A4,GOBRD13:31;
end;
theorem Th52:
for G be Go-board for f be S-Sequence_in_R2 for p be Point of
TOP-REAL 2 for k be Nat st 1 <= k & k < p..f & f is_sequence_on G &
p in rng f holds left_cell(R_Cut(f,p),k,G) = left_cell(f,k,G) & right_cell(
R_Cut(f,p),k,G) = right_cell(f,k,G)
proof
let G be Go-board;
let f be S-Sequence_in_R2;
let p be Point of TOP-REAL 2;
let k be Nat;
assume that
A1: 1 <= k and
A2: k < p..f and
A3: f is_sequence_on G and
A4: p in rng f;
A5: f|(p..f) = mid(f,1,p..f) by A1,A2,FINSEQ_6:116,XXREAL_0:2
.= R_Cut(f,p) by A4,JORDAN1G:49;
A6: k+1 <= p..f by A2,NAT_1:13;
p..f <= len f by A4,FINSEQ_4:21;
then k+1 <= len f by A6,XXREAL_0:2;
hence thesis by A1,A3,A5,A6,GOBRD13:31;
end;
theorem Th53:
for G be Go-board for f be FinSequence of TOP-REAL 2 for p be
Point of TOP-REAL 2 for k be Nat st 1 <= k & k < p..f & f
is_sequence_on G holds left_cell(f-:p,k,G) = left_cell(f,k,G) & right_cell(f-:p
,k,G) = right_cell(f,k,G)
proof
let G be Go-board;
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
let k be Nat;
assume that
A1: 1 <= k and
A2: k < p..f and
A3: f is_sequence_on G;
A4: k+1 <= p..f by A2,NAT_1:13;
A5: f|(p..f) = f-:p by FINSEQ_5:def 1;
per cases by TOPREAL8:4;
suppose
p in rng f;
then p..f <= len f by FINSEQ_4:21;
then k+1 <= len f by A4,XXREAL_0:2;
hence thesis by A1,A3,A5,A4,GOBRD13:31;
end;
suppose
p..f = 0;
hence thesis by A2;
end;
end;
theorem Th54:
for f,g be FinSequence of TOP-REAL 2 st f is unfolded s.n.c.
one-to-one & g is unfolded s.n.c. one-to-one & f/.len f = g/.1 & L~f /\ L~g = {
g/.1} holds f^'g is s.n.c.
proof
let f,g be FinSequence of TOP-REAL 2;
assume that
A1: f is unfolded s.n.c. one-to-one and
A2: g is unfolded s.n.c. one-to-one and
A3: f/.len f = g/.1 and
A4: L~f /\ L~g = {g/.1};
now
let i,j be Nat;
assume
A5: i+1 < j;
now
per cases;
suppose
A6: j < len f;
then i+1 < len f by A5,XXREAL_0:2;
then i < len f by NAT_1:13;
then
A7: LSeg(f^'g,i) = LSeg(f,i) by TOPREAL8:28;
LSeg(f^'g,j) = LSeg(f,j) by A6,TOPREAL8:28;
hence LSeg(f^'g,i) misses LSeg(f^'g,j) by A1,A5,A7,TOPREAL1:def 7;
end;
suppose
j >= len f;
then consider k be Nat such that
A8: j = len f + k by NAT_1:10;
A9: now
assume g is trivial;
then len g < 2 by NAT_D:60;
then len g = 0 or len g = 1 by NAT_1:23;
then L~g = {} by TOPREAL1:22;
hence contradiction by A4;
end;
reconsider k as Nat;
A10: now
assume f is empty;
then len f = 0;
then L~f = {} by TOPREAL1:22;
hence contradiction by A4;
end;
now
per cases;
suppose
A11: i >= 1 & j+1 <= len(f^'g);
then j+1 < len(f^'g)+1 by NAT_1:13;
then len f+(k+1) < len f + len g by A8,A9,FINSEQ_6:139;
then
A12: k+1 < len g by XREAL_1:7;
then
A13: LSeg(f^'g,len f+k) = LSeg(g,k+1) by A3,A10,A9,TOPREAL8:31;
then
A14: LSeg(f^'g,j) c= L~g by A8,TOPREAL3:19;
now
per cases;
suppose
A15: i < len f;
then
A16: i+1 <= len f by NAT_1:13;
i+1 > 1 by A11,NAT_1:13;
then
A17: i+1 in dom f by A16,FINSEQ_3:25;
A18: len g >= 2 by A9,NAT_D:60;
A19: LSeg(f^'g,i) = LSeg(f,i) by A15,TOPREAL8:28;
then LSeg(f^'g,i) c= L~f by TOPREAL3:19;
then
A20: LSeg(f^'g,i) /\ LSeg(f^'g,j) c= {g/.1} by A4,A14,XBOOLE_1:27;
assume LSeg(f^'g,i) meets LSeg(f^'g,j);
then consider x be object such that
A21: x in LSeg(f^'g,i) and
A22: x in LSeg(f^'g,j) by XBOOLE_0:3;
x in LSeg(f^'g,i) /\ LSeg(f^'g,j) by A21,A22,XBOOLE_0:def 4;
then
A23: x = g/.1 by A20,TARSKI:def 1;
i in dom f by A11,A15,FINSEQ_3:25;
then len f+0 < len f+k by A1,A3,A5,A8,A19,A21,A23,A17,
GOBOARD2:2;
then k > 0;
then k+1 > 0+1 by XREAL_1:6;
hence contradiction by A2,A8,A13,A22,A23,A18,JORDAN5B:30;
end;
suppose
i >= len f;
then consider l be Nat such that
A24: i = len f + l by NAT_1:10;
reconsider l as Nat;
len f+(l+1) < len f+k by A5,A8,A24;
then l+1 < k by XREAL_1:7;
then
A25: l+1+1 < k+1 by XREAL_1:6;
then l+1+1 < len g by A12,XXREAL_0:2;
then l+1 < len g by NAT_1:13;
then LSeg(f^'g,len f+l) = LSeg(g,l+1) by A3,A10,A9,TOPREAL8:31;
hence LSeg(f^'g,i) misses LSeg(f^'g,j) by A2,A8,A13,A24,A25,
TOPREAL1:def 7;
end;
end;
hence LSeg(f^'g,i) misses LSeg(f^'g,j);
end;
suppose
j+1 > len(f^'g);
then LSeg(f^'g,j) = {} by TOPREAL1:def 3;
hence LSeg(f^'g,i) misses LSeg(f^'g,j);
end;
suppose
i < 1;
then LSeg(f^'g,i) = {} by TOPREAL1:def 3;
hence LSeg(f^'g,i) misses LSeg(f^'g,j);
end;
end;
hence LSeg(f^'g,i) misses LSeg(f^'g,j);
end;
end;
hence LSeg(f^'g,i) misses LSeg(f^'g,j);
end;
hence thesis by TOPREAL1:def 7;
end;
theorem Th55:
for f,g be FinSequence of TOP-REAL 2 st f is one-to-one & g is
one-to-one & rng f /\ rng g c= {g/.1} holds f^'g is one-to-one
proof
let f,g be FinSequence of TOP-REAL 2;
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: rng f /\ rng g c= {g/.1};
per cases;
suppose
A4: rng g <> {};
now
A5: len (f^'g)+1 = len f + len g by A4,FINSEQ_6:139,RELAT_1:38;
let i,j be Element of NAT;
assume that
A6: i in dom (f^'g) and
A7: j in dom (f^'g) and
A8: (f^'g)/.i = (f^'g)/.j;
A9: 1 <= i by A6,FINSEQ_3:25;
j <= len (f^'g) by A7,FINSEQ_3:25;
then
A10: j < len f + len g by A5,NAT_1:13;
A11: len f = len f + 0;
i <= len (f^'g) by A6,FINSEQ_3:25;
then
A12: i < len f + len g by A5,NAT_1:13;
A13: 1 <= j by A7,FINSEQ_3:25;
A14: 1 in dom g by A4,FINSEQ_3:32;
now
per cases;
suppose
A15: i <= len f & j <= len f;
then
A16: i in dom f by A9,FINSEQ_3:25;
A17: (f^'g)/.j = f/.j by A13,A15,FINSEQ_6:159;
A18: j in dom f by A13,A15,FINSEQ_3:25;
(f^'g)/.i = f/.i by A9,A15,FINSEQ_6:159;
hence i = j by A1,A8,A17,A16,A18,PARTFUN2:10;
end;
suppose
A19: i > len f & j > len f;
then consider l be Nat such that
A20: j = len f + l by NAT_1:10;
consider k be Nat such that
A21: i = len f + k by A19,NAT_1:10;
reconsider k,l as Element of NAT by ORDINAL1:def 12;
l > 0 by A11,A19,A20;
then
A22: l >= 0+1 by NAT_1:13;
then
A23: l+1 > 1 by NAT_1:13;
k > 0 by A11,A19,A21;
then
A24: k >= 0+1 by NAT_1:13;
then
A25: k+1 > 1 by NAT_1:13;
A26: l < len g by A10,A20,XREAL_1:7;
then
A27: (f^'g)/.j = g/.(l+1) by A20,A22,FINSEQ_6:160;
A28: k < len g by A12,A21,XREAL_1:7;
then k+1 <= len g by NAT_1:13;
then
A29: k+1 in dom g by A25,FINSEQ_3:25;
l+1 <= len g by A26,NAT_1:13;
then
A30: l+1 in dom g by A23,FINSEQ_3:25;
(f^'g)/.i = g/.(k+1) by A21,A28,A24,FINSEQ_6:160;
then k+1 = l+1 by A2,A8,A27,A29,A30,PARTFUN2:10;
hence i = j by A21,A20;
end;
suppose
A31: i <= len f & j > len f;
then
A32: i in dom f by A9,FINSEQ_3:25;
(f^'g)/.i = f/.i by A9,A31,FINSEQ_6:159;
then
A33: (f^'g)/.i in rng f by A32,PARTFUN2:2;
consider l be Nat such that
A34: j = len f + l by A31,NAT_1:10;
reconsider l as Element of NAT by ORDINAL1:def 12;
l > 0 by A11,A31,A34;
then
A35: l >= 0+1 by NAT_1:13;
then
A36: l+1 > 1 by NAT_1:13;
A37: l < len g by A10,A34,XREAL_1:7;
then l+1 <= len g by NAT_1:13;
then
A38: l+1 in dom g by A36,FINSEQ_3:25;
A39: (f^'g)/.j = g/.(l+1) by A34,A37,A35,FINSEQ_6:160;
then (f^'g)/.j in rng g by A38,PARTFUN2:2;
then (f^'g)/.j in rng f /\ rng g by A8,A33,XBOOLE_0:def 4;
then g/.(l+1) = g/.1 by A3,A39,TARSKI:def 1;
hence i = j by A2,A14,A36,A38,PARTFUN2:10;
end;
suppose
A40: j <= len f & i > len f;
then
A41: j in dom f by A13,FINSEQ_3:25;
(f^'g)/.j = f/.j by A13,A40,FINSEQ_6:159;
then
A42: (f^'g)/.j in rng f by A41,PARTFUN2:2;
consider l be Nat such that
A43: i = len f + l by A40,NAT_1:10;
reconsider l as Element of NAT by ORDINAL1:def 12;
l > 0 by A11,A40,A43;
then
A44: l >= 0+1 by NAT_1:13;
then
A45: l+1 > 1 by NAT_1:13;
A46: l < len g by A12,A43,XREAL_1:7;
then l+1 <= len g by NAT_1:13;
then
A47: l+1 in dom g by A45,FINSEQ_3:25;
A48: (f^'g)/.i = g/.(l+1) by A43,A46,A44,FINSEQ_6:160;
then (f^'g)/.i in rng g by A47,PARTFUN2:2;
then (f^'g)/.i in rng f /\ rng g by A8,A42,XBOOLE_0:def 4;
then g/.(l+1) = g/.1 by A3,A48,TARSKI:def 1;
hence i = j by A2,A14,A45,A47,PARTFUN2:10;
end;
end;
hence i = j;
end;
hence thesis by PARTFUN2:9;
end;
suppose
rng g = {};
then g = {} by RELAT_1:41;
hence thesis by A1,FINSEQ_6:157;
end;
end;
theorem Th56:
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st f is being_S-Seq & p in rng f & p <> f.1 holds Index(p,f)+1 = p..f
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume that
A1: f is being_S-Seq and
A2: p in rng f and
A3: p <> f.1;
A4: 1 <= p..f by A2,FINSEQ_4:21;
p..f <> 1 by A2,A3,FINSEQ_4:19;
then
A5: 1 < p..f by A4,XXREAL_0:1;
A6: f.(p..f) = p by A2,FINSEQ_4:19;
p..f <= len f by A2,FINSEQ_4:21;
hence thesis by A1,A5,A6,JORDAN3:12;
end;
theorem Th57:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= j &
k <= width Gauge(C,n) & Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) & Gauge(C,n)*(i,j)
in L~Lower_Seq(C,n) holds j <> k
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
let i,j,k be Nat;
assume that
A1: 1 < i and
A2: i < len Gauge(C,n) and
A3: 1 <= j and
A4: k <= width Gauge(C,n) and
A5: Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) and
A6: Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) and
A7: j = k;
A8: [i,j] in Indices Gauge(C,n) by A1,A2,A3,A4,A7,MATRIX_0:30;
Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) by A5,A6,A7,
XBOOLE_0:def 4;
then
A9: Gauge(C,n)*(i,k) in {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:16;
A10: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
len Gauge(C,n) >= 4 by JORDAN8:10;
then
A11: len Gauge(C,n) >= 1 by XXREAL_0:2;
then
A12: [len Gauge(C,n),j] in Indices Gauge(C,n) by A3,A4,A7,MATRIX_0:30;
A13: [1,j] in Indices Gauge(C,n) by A3,A4,A7,A11,MATRIX_0:30;
per cases by A9,TARSKI:def 2;
suppose
A14: Gauge(C,n)*(i,k) = W-min L~Cage(C,n);
Gauge(C,n)*(1,j)`1 = W-bound L~Cage(C,n) by A3,A4,A7,A10,JORDAN1A:73;
then
(W-min L~Cage(C,n))`1 <> W-bound L~Cage(C,n) by A1,A7,A8,A13,A14,JORDAN1G:7;
hence contradiction by EUCLID:52;
end;
suppose
A15: Gauge(C,n)*(i,k) = E-max L~Cage(C,n);
Gauge(C,n)*(len Gauge(C,n),j)`1 = E-bound L~Cage(C,n) by A3,A4,A7,A10,
JORDAN1A:71;
then
(E-max L~Cage(C,n))`1 <> E-bound L~Cage(C,n) by A2,A7,A8,A12,A15,JORDAN1G:7;
hence contradiction by EUCLID:52;
end;
end;
theorem Th58:
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) & LSeg(Gauge(C
,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i,k)} & LSeg(
Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Lower_Seq(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;
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 Gij = Ga*(i,j);
set Gik = Ga*(i,k);
assume that
A1: 1 < i and
A2: i < len Ga and
A3: 1 <= j and
A4: j <= k and
A5: k <= width Ga and
A6: LSeg(Gij,Gik) /\ L~US = {Gik} and
A7: LSeg(Gij,Gik) /\ L~LS = {Gij} and
A8: LSeg(Gij,Gik) misses LA;
Gij in {Gij} by TARSKI:def 1;
then
A9: Gij in L~LS by A7,XBOOLE_0:def 4;
Gik in {Gik} by TARSKI:def 1;
then
A10: Gik in L~US by A6,XBOOLE_0:def 4;
then
A11: j <> k by A1,A2,A3,A5,A9,Th57;
A12: j <= width Ga by A4,A5,XXREAL_0:2;
A13: 1 <= k by A3,A4,XXREAL_0:2;
A14: [i,j] in Indices Ga by A1,A2,A3,A12,MATRIX_0:30;
A15: [i,k] in Indices Ga by A1,A2,A5,A13,MATRIX_0:30;
set go = R_Cut(US,Gik);
set co = L_Cut(LS,Gij);
A16: len Ga = width Ga by JORDAN8:def 1;
A17: len US >= 3 by JORDAN1E:15;
then len US >= 1 by XXREAL_0:2;
then 1 in dom US by FINSEQ_3:25;
then
A18: US.1 = US/.1 by PARTFUN1:def 6
.= Wmin by JORDAN1F:5;
A19: Wmin`1 = Wbo by EUCLID:52
.= Ga*(1,k)`1 by A5,A13,A16,JORDAN1A:73;
len Ga >= 4 by JORDAN8:10;
then
A20: len Ga >= 1 by XXREAL_0:2;
then
A21: [1,k] in Indices Ga by A5,A13,MATRIX_0:30;
then
A22: Gik <> US.1 by A1,A15,A18,A19,JORDAN1G:7;
then reconsider go as being_S-Seq FinSequence of TOP-REAL 2 by A10,JORDAN3:35
;
A23: len LS >= 1+2 by JORDAN1E:15;
then
A24: len LS >= 1 by XXREAL_0:2;
then
A25: 1 in dom LS by FINSEQ_3:25;
len LS in dom LS by A24,FINSEQ_3:25;
then
A26: LS.len LS = LS/.len LS by PARTFUN1:def 6
.= Wmin by JORDAN1F:8;
A27: Wmin`1 = Wbo by EUCLID:52
.= Ga*(1,k)`1 by A5,A13,A16,JORDAN1A:73;
A28: [i,j] in Indices Ga by A1,A2,A3,A12,MATRIX_0:30;
then
A29: Gij <> LS.len LS by A1,A21,A26,A27,JORDAN1G:7;
then reconsider co as being_S-Seq FinSequence of TOP-REAL 2 by A9,JORDAN3:34;
A30: [len Ga,k] in Indices Ga by A5,A13,A20,MATRIX_0:30;
A31: LS.1 = LS/.1 by A25,PARTFUN1:def 6
.= Emax by JORDAN1F:6;
Emax`1 = Ebo by EUCLID:52
.= Ga*(len Ga,k)`1 by A5,A13,A16,JORDAN1A:71;
then
A32: Gij <> LS.1 by A2,A28,A30,A31,JORDAN1G:7;
A33: len go >= 1+1 by TOPREAL1:def 8;
A34: Gik in rng US by A1,A2,A5,A10,A13,Th40,JORDAN1G:4;
then
A35: go is_sequence_on Ga by Th38,JORDAN1G:4;
A36: len co >= 1+1 by TOPREAL1:def 8;
A37: Gij in rng LS by A1,A2,A3,A9,A12,Th40,JORDAN1G:5;
then
A38: co is_sequence_on Ga by Th39,JORDAN1G:5;
reconsider go as non constant s.c.c. being_S-Seq FinSequence of TOP-REAL 2
by A33,A35,JGRAPH_1:12,JORDAN8:5;
reconsider co as non constant s.c.c. being_S-Seq FinSequence of TOP-REAL 2
by A36,A38,JGRAPH_1:12,JORDAN8:5;
A39: len go > 1 by A33,NAT_1:13;
then
A40: len go in dom go by FINSEQ_3:25;
then
A41: go/.len go = go.len go by PARTFUN1:def 6
.= Gik by A10,JORDAN3:24;
len co >= 1 by A36,XXREAL_0:2;
then 1 in dom co by FINSEQ_3:25;
then
A42: co/.1 = co.1 by PARTFUN1:def 6
.= Gij by A9,JORDAN3:23;
reconsider m = len go - 1 as Nat by A40,FINSEQ_3:26;
A43: m+1 = len go;
then
A44: len go-'1 = m by NAT_D:34;
A45: LSeg(go,m) c= L~go by TOPREAL3:19;
A46: L~go c= L~US by A10,JORDAN3:41;
then LSeg(go,m) c= L~US by A45;
then
A47: LSeg(go,m) /\ LSeg(Gik,Gij) c= {Gik} by A6,XBOOLE_1:26;
m >= 1 by A33,XREAL_1:19;
then
A48: LSeg(go,m) = LSeg(go/.m,Gik) by A41,A43,TOPREAL1:def 3;
{Gik} c= LSeg(go,m) /\ LSeg(Gik,Gij)
proof
let x be object;
A49: Gik in LSeg(Gik,Gij) by RLTOPSP1:68;
assume x in {Gik};
then
A50: x = Gik by TARSKI:def 1;
Gik in LSeg(go,m) by A48,RLTOPSP1:68;
hence thesis by A50,A49,XBOOLE_0:def 4;
end;
then
A51: LSeg(go,m) /\ LSeg(Gik,Gij) = {Gik} by A47;
A52: LSeg(co,1) c= L~co by TOPREAL3:19;
A53: L~co c= L~LS by A9,JORDAN3:42;
then LSeg(co,1) c= L~LS by A52;
then
A54: LSeg(co,1) /\ LSeg(Gik,Gij) c= {Gij} by A7,XBOOLE_1:26;
A55: LSeg(co,1) = LSeg(Gij,co/.(1+1)) by A36,A42,TOPREAL1:def 3;
{Gij} c= LSeg(co,1) /\ LSeg(Gik,Gij)
proof
let x be object;
A56: Gij in LSeg(Gik,Gij) by RLTOPSP1:68;
assume x in {Gij};
then
A57: x = Gij by TARSKI:def 1;
Gij in LSeg(co,1) by A55,RLTOPSP1:68;
hence thesis by A57,A56,XBOOLE_0:def 4;
end;
then
A58: LSeg(Gik,Gij) /\ LSeg(co,1) = {Gij} by A54;
A59: go/.1 = US/.1 by A10,SPRECT_3:22
.= Wmin by JORDAN1F:5;
then
A60: go/.1 = LS/.len LS by JORDAN1F:8
.= co/.len co by A9,Th35;
A61: rng go c= L~go by A33,SPPOL_2:18;
A62: rng co c= L~co by A36,SPPOL_2:18;
A63: {go/.1} c= L~go /\ L~co
proof
let x be object;
assume x in {go/.1};
then
A64: x = go/.1 by TARSKI:def 1;
then
A65: x in rng go by FINSEQ_6:42;
x in rng co by A60,A64,FINSEQ_6:168;
hence thesis by A61,A62,A65,XBOOLE_0:def 4;
end;
A66: LS.1 = LS/.1 by A25,PARTFUN1:def 6
.= Emax by JORDAN1F:6;
A67: [len Ga,j] in Indices Ga by A3,A12,A20,MATRIX_0:30;
L~go /\ L~co c= {go/.1}
proof
let x be object;
assume
A68: x in L~go /\ L~co;
then
A69: x in L~co by XBOOLE_0:def 4;
A70: now
assume x = Emax;
then
A71: Emax = Gij by A9,A66,A69,JORDAN1E:7;
Ga*(len Ga,j)`1 = Ebo by A3,A12,A16,JORDAN1A:71;
then Emax`1 <> Ebo by A2,A14,A67,A71,JORDAN1G:7;
hence contradiction by EUCLID:52;
end;
x in L~go by A68,XBOOLE_0:def 4;
then x in L~US /\ L~LS by A46,A53,A69,XBOOLE_0:def 4;
then x in {Wmin,Emax} by JORDAN1E:16;
then x = Wmin or x = Emax by TARSKI:def 2;
hence thesis by A59,A70,TARSKI:def 1;
end;
then
A72: L~go /\ L~co = {go/.1} by A63;
set W2 = go/.2;
A73: 2 in dom go by A33,FINSEQ_3:25;
A74: now
assume Gik`1 = Wbo;
then Ga*(1,k)`1 = Ga*(i,k)`1 by A5,A13,A16,JORDAN1A:73;
hence contradiction by A1,A15,A21,JORDAN1G:7;
end;
go = mid(US,1,Gik..US) by A34,JORDAN1G:49
.= US|(Gik..US) by A34,FINSEQ_4:21,FINSEQ_6:116;
then
A75: W2 = US/.2 by A73,FINSEQ_4:70;
set pion = <*Gik,Gij*>;
A76: now
let n be Nat;
assume n in dom pion;
then n in Seg 2 by FINSEQ_1:89;
then n = 1 or n = 2 by FINSEQ_1:2,TARSKI:def 2;
hence ex i,j be Nat st [i,j] in Indices Ga & pion/.n = Ga*(i,j)
by A14,A15,FINSEQ_4:17;
end;
A77: Gik <> Gij by A11,A14,A15,GOBOARD1:5;
A78: Gik`1 = Ga*(i,1)`1 by A1,A2,A5,A13,GOBOARD5:2
.= Gij`1 by A1,A2,A3,A12,GOBOARD5:2;
then LSeg(Gik,Gij) is vertical by SPPOL_1:16;
then pion is being_S-Seq by A77,JORDAN1B:7;
then consider pion1 be FinSequence of TOP-REAL 2 such that
A79: pion1 is_sequence_on Ga and
A80: pion1 is being_S-Seq and
A81: L~pion = L~pion1 and
A82: pion/.1 = pion1/.1 and
A83: pion/.len pion = pion1/.len pion1 and
A84: len pion <= len pion1 by A76,GOBOARD3:2;
reconsider pion1 as being_S-Seq FinSequence of TOP-REAL 2 by A80;
set godo = go^'pion1^'co;
A85: 1+1 <= len Cage(C,n) by GOBOARD7:34,XXREAL_0:2;
A86: 1+1 <= len Rotate(Cage(C,n),Wmin) by GOBOARD7:34,XXREAL_0:2;
len (go^'pion1) >= len go by TOPREAL8:7;
then
A87: len (go^'pion1) >= 1+1 by A33,XXREAL_0:2;
then
A88: len (go^'pion1) > 1+0 by NAT_1:13;
A89: len godo >= len (go^'pion1) by TOPREAL8:7;
then
A90: 1+1 <= len godo by A87,XXREAL_0:2;
A91: US is_sequence_on Ga by JORDAN1G:4;
A92: go/.len go = pion1/.1 by A41,A82,FINSEQ_4:17;
then
A93: go^'pion1 is_sequence_on Ga by A35,A79,TOPREAL8:12;
A94: (go^'pion1)/.len (go^'pion1) = pion/.len pion by A83,FINSEQ_6:156
.= pion/.2 by FINSEQ_1:44
.= co/.1 by A42,FINSEQ_4:17;
then
A95: godo is_sequence_on Ga by A38,A93,TOPREAL8:12;
LSeg(pion1,1) c= L~<*Gik,Gij*> by A81,TOPREAL3:19;
then LSeg(pion1,1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then
A96: LSeg(go,len go-'1) /\ LSeg(pion1,1) c= {Gik} by A44,A51,XBOOLE_1:27;
A97: len pion1 >= 1+1 by A84,FINSEQ_1:44;
{Gik} c= LSeg(go,m) /\ LSeg(pion1,1)
proof
let x be object;
assume x in {Gik};
then
A98: x = Gik by TARSKI:def 1;
A99: Gik in LSeg(go,m) by A48,RLTOPSP1:68;
Gik in LSeg(pion1,1) by A41,A92,A97,TOPREAL1:21;
hence thesis by A98,A99,XBOOLE_0:def 4;
end;
then LSeg(go,len go-'1) /\ LSeg(pion1,1) = { go/.len go } by A41,A44,A96;
then
A100: go^'pion1 is unfolded by A92,TOPREAL8:34;
len pion1 >= 2+0 by A84,FINSEQ_1:44;
then
A101: len pion1-2 >= 0 by XREAL_1:19;
len (go^'pion1)+1-1 = len go+len pion1-1 by FINSEQ_6:139;
then len (go^'pion1)-1 = len go + (len pion1-2)
.= len go + (len pion1-'2) by A101,XREAL_0:def 2;
then
A102: len (go^'pion1)-'1 = len go + (len pion1-'2) by XREAL_0:def 2;
A103: len pion1-1 >= 1 by A97,XREAL_1:19;
then
A104: len pion1-'1 = len pion1-1 by XREAL_0:def 2;
A105: len pion1-'2+1 = len pion1-2+1 by A101,XREAL_0:def 2
.= len pion1-'1 by A103,XREAL_0:def 2;
len pion1-1+1 <= len pion1;
then
A106: len pion1-'1 < len pion1 by A104,NAT_1:13;
LSeg(pion1,len pion1-'1) c= L~<*Gik,Gij*> by A81,TOPREAL3:19;
then LSeg(pion1,len pion1-'1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then
A107: LSeg(pion1,len pion1-'1) /\ LSeg(co,1) c= {Gij} by A58,XBOOLE_1:27;
{Gij} c= LSeg(pion1,len pion1-'1) /\ LSeg(co,1)
proof
let x be object;
assume x in {Gij};
then
A108: x = Gij by TARSKI:def 1;
pion1/.(len pion1-'1+1) = pion/.2 by A83,A104,FINSEQ_1:44
.= Gij by FINSEQ_4:17;
then
A109: Gij in LSeg(pion1,len pion1-'1) by A103,A104,TOPREAL1:21;
Gij in LSeg(co,1) by A55,RLTOPSP1:68;
hence thesis by A108,A109,XBOOLE_0:def 4;
end;
then LSeg(pion1,len pion1-'1) /\ LSeg(co,1) = {Gij} by A107;
then
A110: LSeg(go^'pion1,len go+(len pion1-'2)) /\ LSeg(co,1) = {(go^'pion1)/.
len (go^'pion1)} by A42,A92,A94,A105,A106,TOPREAL8:31;
A111: (go^'pion1) is non trivial by A87,NAT_D:60;
A112: rng pion1 c= L~pion1 by A97,SPPOL_2:18;
A113: {pion1/.1} c= L~go /\ L~pion1
proof
let x be object;
assume x in {pion1/.1};
then
A114: x = pion1/.1 by TARSKI:def 1;
then
A115: x in rng pion1 by FINSEQ_6:42;
x in rng go by A92,A114,FINSEQ_6:168;
hence thesis by A61,A112,A115,XBOOLE_0:def 4;
end;
L~go /\ L~pion1 c= {pion1/.1}
proof
let x be object;
assume
A116: x in L~go /\ L~pion1;
then
A117: x in L~pion1 by XBOOLE_0:def 4;
x in L~go by A116,XBOOLE_0:def 4;
then x in L~pion1 /\ L~US by A46,A117,XBOOLE_0:def 4;
hence thesis by A6,A41,A81,A92,SPPOL_2:21;
end;
then
A118: L~go /\ L~pion1 = {pion1/.1} by A113;
then
A119: (go^'pion1) is s.n.c. by A92,Th54;
rng go /\ rng pion1 c= {pion1/.1} by A61,A112,A118,XBOOLE_1:27;
then
A120: go^'pion1 is one-to-one by Th55;
A121: pion/.len pion = pion/.2 by FINSEQ_1:44
.= co/.1 by A42,FINSEQ_4:17;
A122: {pion1/.len pion1} c= L~co /\ L~pion1
proof
let x be object;
assume x in {pion1/.len pion1};
then
A123: x = pion1/.len pion1 by TARSKI:def 1;
then
A124: x in rng pion1 by FINSEQ_6:168;
x in rng co by A83,A121,A123,FINSEQ_6:42;
hence thesis by A62,A112,A124,XBOOLE_0:def 4;
end;
L~co /\ L~pion1 c= {pion1/.len pion1}
proof
let x be object;
assume
A125: x in L~co /\ L~pion1;
then
A126: x in L~pion1 by XBOOLE_0:def 4;
x in L~co by A125,XBOOLE_0:def 4;
then x in L~pion1 /\ L~LS by A53,A126,XBOOLE_0:def 4;
hence thesis by A7,A42,A81,A83,A121,SPPOL_2:21;
end;
then
A127: L~co /\ L~pion1 = {pion1/.len pion1} by A122;
A128: L~(go^'pion1) /\ L~co = (L~go \/ L~pion1) /\ L~co by A92,TOPREAL8:35
.= {go/.1} \/ {co/.1} by A72,A83,A121,A127,XBOOLE_1:23
.= {(go^'pion1)/.1} \/ {co/.1} by FINSEQ_6:155
.= {(go^'pion1)/.1,co/.1} by ENUMSET1:1;
co/.len co = (go^'pion1)/.1 by A60,FINSEQ_6:155;
then reconsider
godo as non constant standard special_circular_sequence by A90,A94,A95,A100
,A102,A110,A111,A119,A120,A128,JORDAN8:4,5,TOPREAL8:11,33,34;
A129: LA is_an_arc_of E-max C,W-min C by JORDAN6:def 9;
then
A130: LA is connected by JORDAN6:10;
A131: W-min C in LA by A129,TOPREAL1:1;
A132: E-max C in LA by A129,TOPREAL1:1;
set ff = Rotate(Cage(C,n),Wmin);
Wmin in rng Cage(C,n) by SPRECT_2:43;
then
A133: ff/.1 = Wmin by FINSEQ_6:92;
A134: L~ff = L~Cage(C,n) by REVROT_1:33;
then (W-max L~ff)..ff > 1 by A133,SPRECT_5:22;
then (N-min L~ff)..ff > 1 by A133,A134,SPRECT_5:23,XXREAL_0:2;
then (N-max L~ff)..ff > 1 by A133,A134,SPRECT_5:24,XXREAL_0:2;
then
A135: Emax..ff > 1 by A133,A134,SPRECT_5:25,XXREAL_0:2;
A136: now
assume
A137: Gik..US <= 1;
Gik..US >= 1 by A34,FINSEQ_4:21;
then Gik..US = 1 by A137,XXREAL_0:1;
then Gik = US/.1 by A34,FINSEQ_5:38;
hence contradiction by A18,A22,JORDAN1F:5;
end;
A138: Cage(C,n) is_sequence_on Ga by JORDAN9:def 1;
then
A139: ff is_sequence_on Ga by REVROT_1:34;
A140: right_cell(godo,1,Ga)\L~godo c= RightComp godo by A90,A95,JORDAN9:27;
A141: L~godo = L~(go^'pion1) \/ L~co by A94,TOPREAL8:35
.= L~go \/ L~pion1 \/ L~co by A92,TOPREAL8:35;
A142: L~Cage(C,n) = L~US \/ L~LS by JORDAN1E:13;
then
A143: L~US c= L~Cage(C,n) by XBOOLE_1:7;
A144: L~LS c= L~Cage(C,n) by A142,XBOOLE_1:7;
A145: L~go c= L~Cage(C,n) by A46,A143;
A146: L~co c= L~Cage(C,n) by A53,A144;
A147: W-min C in C by SPRECT_1:13;
A148: L~pion = LSeg(Gik,Gij) by SPPOL_2:21;
A149: now
assume W-min C in L~godo;
then
A150: W-min C in L~go \/ L~pion1 or W-min C in L~co by A141,XBOOLE_0:def 3;
per cases by A150,XBOOLE_0:def 3;
suppose
W-min C in L~go;
then C meets L~Cage(C,n) by A145,A147,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
end;
suppose
W-min C in L~pion1;
hence contradiction by A8,A81,A131,A148,XBOOLE_0:3;
end;
suppose
W-min C in L~co;
then C meets L~Cage(C,n) by A146,A147,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
end;
end;
right_cell(Rotate(Cage(C,n),Wmin),1) = right_cell(ff,1,GoB ff) by A86,
JORDAN1H:23
.= right_cell(ff,1,GoB Cage(C,n)) by REVROT_1:28
.= right_cell(ff,1,Ga) by JORDAN1H:44
.= right_cell(ff-:Emax,1,Ga) by A135,A139,Th53
.= right_cell(US,1,Ga) by JORDAN1E:def 1
.= right_cell(R_Cut(US,Gik),1,Ga) by A34,A91,A136,Th52
.= right_cell(go^'pion1,1,Ga) by A39,A93,Th51
.= right_cell(godo,1,Ga) by A88,A95,Th51;
then W-min C in right_cell(godo,1,Ga) by JORDAN1I:6;
then
A151: W-min C in right_cell(godo,1,Ga)\L~godo by A149,XBOOLE_0:def 5;
A152: godo/.1 = (go^'pion1)/.1 by FINSEQ_6:155
.= Wmin by A59,FINSEQ_6:155;
A153: len US >= 2 by A17,XXREAL_0:2;
A154: godo/.2 = (go^'pion1)/.2 by A87,FINSEQ_6:159
.= US/.2 by A33,A75,FINSEQ_6:159
.= (US^'LS)/.2 by A153,FINSEQ_6:159
.= Rotate(Cage(C,n),Wmin)/.2 by JORDAN1E:11;
A155: L~go \/ L~co is compact by COMPTS_1:10;
Wmin in rng go by A59,FINSEQ_6:42;
then Wmin in L~go \/ L~co by A61,XBOOLE_0:def 3;
then
A156: W-min (L~go \/ L~co) = Wmin by A145,A146,A155,Th21,XBOOLE_1:8;
A157: (W-min (L~go \/ L~co))`1 = W-bound (L~go \/ L~co) by EUCLID:52;
A158: Wmin`1 = Wbo by EUCLID:52;
W-bound LSeg(Gik,Gij) = Gik`1 by A78,SPRECT_1:54;
then
A159: W-bound L~pion1 = Gik`1 by A81,SPPOL_2:21;
Gik`1 >= Wbo by A10,A143,PSCOMP_1:24;
then Gik`1 > Wbo by A74,XXREAL_0:1;
then W-min (L~go\/L~co\/L~pion1) = W-min (L~go \/ L~co) by A155,A156,A157
,A158,A159,Th33;
then
A160: W-min L~godo = Wmin by A141,A156,XBOOLE_1:4;
A161: rng godo c= L~godo by A87,A89,SPPOL_2:18,XXREAL_0:2;
2 in dom godo by A90,FINSEQ_3:25;
then
A162: godo/.2 in rng godo by PARTFUN2:2;
godo/.2 in W-most L~Cage(C,n) by A154,JORDAN1I:25;
then (godo/.2)`1 = (W-min L~godo)`1 by A160,PSCOMP_1:31
.= W-bound L~godo by EUCLID:52;
then godo/.2 in W-most L~godo by A161,A162,SPRECT_2:12;
then Rotate(godo,W-min L~godo)/.2 in W-most L~godo by A152,A160,FINSEQ_6:89;
then reconsider godo as clockwise_oriented non constant standard
special_circular_sequence by JORDAN1I:25;
len US in dom US by FINSEQ_5:6;
then
A163: US.len US = US/.len US by PARTFUN1:def 6
.= Emax by JORDAN1F:7;
A164: east_halfline E-max C misses L~go
proof
assume east_halfline E-max C meets L~go;
then consider p be object such that
A165: p in east_halfline E-max C and
A166: p in L~go by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A165;
p in L~US by A46,A166;
then p in east_halfline E-max C /\ L~Cage(C,n) by A143,A165,XBOOLE_0:def 4;
then
A167: p`1 = Ebo by JORDAN1A:83,PSCOMP_1:50;
then
A168: p = Emax by A46,A166,Th46;
then Emax = Gik by A10,A163,A166,Th43;
then Gik`1 = Ga*(len Ga,k)`1 by A5,A13,A16,A167,A168,JORDAN1A:71;
hence contradiction by A2,A15,A30,JORDAN1G:7;
end;
now
assume east_halfline E-max C meets L~godo;
then
A169: east_halfline E-max C meets (L~go \/ L~pion1) or east_halfline E-max
C meets L~co by A141,XBOOLE_1:70;
per cases by A169,XBOOLE_1:70;
suppose
east_halfline E-max C meets L~go;
hence contradiction by A164;
end;
suppose
east_halfline E-max C meets L~pion1;
then consider p be object such that
A170: p in east_halfline E-max C and
A171: p in L~pion1 by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A170;
A172: p`2 = (E-max C)`2 by A170,TOPREAL1:def 11;
i+1 <= len Ga by A2,NAT_1:13;
then i+1-1 <= len Ga-1 by XREAL_1:9;
then
A173: i <= len Ga-'1 by XREAL_0:def 2;
A174: len Ga-'1 <= len Ga by NAT_D:35;
p`1 = Gik`1 by A78,A81,A148,A171,GOBOARD7:5;
then p`1 <= Ga*(len Ga-'1,1)`1 by A1,A5,A13,A16,A20,A173,A174,JORDAN1A:18
;
then p`1 <= E-bound C by A20,JORDAN8:12;
then
A175: p`1 <= (E-max C)`1 by EUCLID:52;
p`1 >= (E-max C)`1 by A170,TOPREAL1:def 11;
then p`1 = (E-max C)`1 by A175,XXREAL_0:1;
then p = E-max C by A172,TOPREAL3:6;
hence contradiction by A8,A81,A132,A148,A171,XBOOLE_0:3;
end;
suppose
east_halfline E-max C meets L~co;
then consider p be object such that
A176: p in east_halfline E-max C and
A177: p in L~co by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A176;
A178: (E-max C)`2 = p`2 by A176,TOPREAL1:def 11;
set tt = Index(p,co)+(Gij..LS)-'1;
set RC = Rotate(Cage(C,n),Emax);
A179: L~RC = L~Cage(C,n) by REVROT_1:33;
consider t be Nat such that
A180: t in dom LS and
A181: LS.t = Gij by A37,FINSEQ_2:10;
1 <= t by A180,FINSEQ_3:25;
then
A182: 1 < t by A32,A181,XXREAL_0:1;
t <= len LS by A180,FINSEQ_3:25;
then Index(Gij,LS)+1 = t by A181,A182,JORDAN3:12;
then
A183: len L_Cut(LS,Gij) = len LS-Index(Gij,LS) by A9,A181,JORDAN3:26;
Index(p,co) < len co by A177,JORDAN3:8;
then Index(p,co) < len LS-'Index(Gij,LS) by A183,XREAL_0:def 2;
then Index(p,co)+1 <= len LS-'Index(Gij,LS) by NAT_1:13;
then
A184: Index(p,co) <= len LS-'Index(Gij,LS)-1 by XREAL_1:19;
A185: co = mid(LS,Gij..LS,len LS) by A37,Th37;
A186: len RC = len Cage(C,n) by FINSEQ_6:179;
p in L~LS by A53,A177;
then p in east_halfline E-max C /\ L~Cage(C,n) by A144,A176,
XBOOLE_0:def 4;
then
A187: p`1 = Ebo by JORDAN1A:83,PSCOMP_1:50;
A188: GoB RC = GoB Cage(C,n) by REVROT_1:28
.= Ga by JORDAN1H:44;
A189: 1+1 <= len LS by A23,XXREAL_0:2;
then
A190: 2 in dom LS by FINSEQ_3:25;
consider jj2 be Nat such that
A191: 1 <= jj2 and
A192: jj2 <= width Ga and
A193: Emax = Ga*(len Ga,jj2) by JORDAN1D:25;
A194: len Ga >= 4 by JORDAN8:10;
then len Ga >= 1 by XXREAL_0:2;
then
A195: [len Ga,jj2] in Indices Ga by A191,A192,MATRIX_0:30;
A196: 1<=Index(p,co) by A177,JORDAN3:8;
LS = RC-:Wmin by JORDAN1G:18;
then
A197: LSeg(LS,1) = LSeg(RC,1) by A189,SPPOL_2:9;
A198: Emax in rng Cage(C,n) by SPRECT_2:46;
RC is_sequence_on Ga by A138,REVROT_1:34;
then consider ii,jj be Nat such that
A199: [ii,jj+1] in Indices Ga and
A200: [ii,jj] in Indices Ga and
A201: RC/.1 = Ga*(ii,jj+1) and
A202: RC/.(1+1) = Ga*(ii,jj) by A85,A179,A186,A198,FINSEQ_6:92,JORDAN1I:23;
A203: jj+1+1 <> jj;
A204: 1 <= jj by A200,MATRIX_0:32;
RC/.1 = E-max L~RC by A179,A198,FINSEQ_6:92;
then
A205: ii = len Ga by A179,A199,A201,A193,A195,GOBOARD1:5;
then ii-1 >= 4-1 by A194,XREAL_1:9;
then
A206: ii-1 >= 1 by XXREAL_0:2;
then
A207: 1 <= ii-'1 by XREAL_0:def 2;
A208: jj <= width Ga by A200,MATRIX_0:32;
then
A209: Ga*(len Ga,jj)`1 = Ebo by A16,A204,JORDAN1A:71;
A210: jj+1 <= width Ga by A199,MATRIX_0:32;
ii+1 <> ii;
then
A211: right_cell(RC,1) = cell(Ga,ii-'1,jj) by A85,A186,A188,A199,A200,A201,A202
,A203,GOBOARD5:def 6;
A212: ii <= len Ga by A200,MATRIX_0:32;
A213: 1 <= ii by A200,MATRIX_0:32;
A214: ii <= len Ga by A199,MATRIX_0:32;
A215: 1 <= jj+1 by A199,MATRIX_0:32;
then
A216: Ebo = Ga*(len Ga,jj+1)`1 by A16,A210,JORDAN1A:71;
A217: 1 <= ii by A199,MATRIX_0:32;
then
A218: ii-'1+1 = ii by XREAL_1:235;
then
A219: ii-'1 < len Ga by A214,NAT_1:13;
then
A220: Ga*(ii-'1,jj+1)`2 = Ga*(1,jj+1)`2 by A215,A210,A207,GOBOARD5:1
.= Ga*(ii,jj+1)`2 by A217,A214,A215,A210,GOBOARD5:1;
A221: E-max C in right_cell(RC,1) by JORDAN1I:7;
then
A222: Ga*(ii-'1,jj)`2 <= (E-max C)`2 by A214,A210,A204,A211,A218,A206,
JORDAN9:17;
A223: (E-max C)`2 <= Ga*(ii-'1,jj+1)`2 by A221,A214,A210,A204,A211,A218,A206,
JORDAN9:17;
Ga*(ii-'1,jj)`2 = Ga*(1,jj)`2 by A204,A208,A207,A219,GOBOARD5:1
.= Ga*(ii,jj)`2 by A213,A212,A204,A208,GOBOARD5:1;
then p in LSeg(RC/.1,RC/.(1+1)) by A187,A178,A201,A202,A205,A222,A223
,A220,A209,A216,GOBOARD7:7;
then
A224: p in LSeg(LS,1) by A85,A197,A186,TOPREAL1:def 3;
A225: Gij..LS<=len LS by A37,FINSEQ_4:21;
Gij..LS <> len LS by A29,A37,FINSEQ_4:19;
then
A226: Gij..LS < len LS by A225,XXREAL_0:1;
A227: Index(Gij,LS)+1 = Gij..LS by A32,A37,Th56;
0+Index(Gij,LS) < len LS by A9,JORDAN3:8;
then len LS-Index(Gij,LS) > 0 by XREAL_1:20;
then Index(p,co) <= len LS-Index(Gij,LS)-1 by A184,XREAL_0:def 2;
then Index(p,co) <= len LS-Gij..LS by A227;
then Index(p,co) <= len LS-'Gij..LS by XREAL_0:def 2;
then
A228: Index(p,co) < len LS-'(Gij..LS)+1 by NAT_1:13;
A229: p in LSeg(co,Index(p,co)) by A177,JORDAN3:9;
1<=Gij..LS by A37,FINSEQ_4:21;
then
A230: LSeg(mid(LS,Gij..LS,len LS),Index(p,co)) = LSeg(LS,Index(p,co)+(
Gij..LS)-'1) by A226,A196,A228,JORDAN4:19;
1<=Index(Gij,LS) by A9,JORDAN3:8;
then
A231: 1+1 <= Gij..LS by A227,XREAL_1:7;
then Index(p,co)+Gij..LS >= 1+1+1 by A196,XREAL_1:7;
then Index(p,co)+Gij..LS-1 >= 1+1+1-1 by XREAL_1:9;
then
A232: tt >= 1+1 by XREAL_0:def 2;
now
per cases by A232,XXREAL_0:1;
suppose
tt > 1+1;
then LSeg(LS,1) misses LSeg(LS,tt) by TOPREAL1:def 7;
hence contradiction by A224,A229,A185,A230,XBOOLE_0:3;
end;
suppose
A233: tt = 1+1;
then 1+1 = Index(p,co)+(Gij..LS)-1 by XREAL_0:def 2;
then 1+1+1 = Index(p,co)+(Gij..LS);
then
A234: Gij..LS = 2 by A196,A231,JORDAN1E:6;
LSeg(LS,1) /\ LSeg(LS,tt) = {LS/.2} by A23,A233,TOPREAL1:def 6;
then p in {LS/.2} by A224,A229,A185,A230,XBOOLE_0:def 4;
then
A235: p = LS/.2 by TARSKI:def 1;
then
A236: p in rng LS by A190,PARTFUN2:2;
p..LS = 2 by A190,A235,FINSEQ_5:41;
then p = Gij by A37,A234,A236,FINSEQ_5:9;
then Gij`1 = Ebo by A235,JORDAN1G:32;
then Gij`1 = Ga*(len Ga,j)`1 by A3,A12,A16,JORDAN1A:71;
hence contradiction by A2,A14,A67,JORDAN1G:7;
end;
end;
hence contradiction;
end;
end;
then east_halfline E-max C c= (L~godo)` by SUBSET_1:23;
then consider W be Subset of TOP-REAL 2 such that
A237: W is_a_component_of (L~godo)` and
A238: east_halfline E-max C c= W by GOBOARD9:3;
W is not bounded by A238,JORDAN2C:121,RLTOPSP1:42;
then W is_outside_component_of L~godo by A237,JORDAN2C:def 3;
then W c= UBD L~godo by JORDAN2C:23;
then
A239: east_halfline E-max C c= UBD L~godo by A238;
E-max C in east_halfline E-max C by TOPREAL1:38;
then E-max C in UBD L~godo by A239;
then E-max C in LeftComp godo by GOBRD14:36;
then LA meets L~godo by A130,A131,A132,A140,A151,Th36;
then
A240: LA meets (L~go \/ L~pion1) or LA meets L~co by A141,XBOOLE_1:70;
A241: LA c= C by JORDAN6:61;
per cases by A240,XBOOLE_1:70;
suppose
LA meets L~go;
then LA meets L~Cage(C,n) by A46,A143,XBOOLE_1:1,63;
hence contradiction by A241,JORDAN10:5,XBOOLE_1:63;
end;
suppose
LA meets L~pion1;
hence contradiction by A8,A81,A148;
end;
suppose
LA meets L~co;
then LA meets L~Cage(C,n) by A53,A144,XBOOLE_1:1,63;
hence contradiction by A241,JORDAN10:5,XBOOLE_1:63;
end;
end;
theorem Th59:
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) & LSeg(Gauge(C
,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i,k)} & LSeg(
Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Lower_Seq(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;
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 Gij = Ga*(i,j);
set Gik = Ga*(i,k);
assume that
A1: 1 < i and
A2: i < len Ga and
A3: 1 <= j and
A4: j <= k and
A5: k <= width Ga and
A6: LSeg(Gij,Gik) /\ L~US = {Gik} and
A7: LSeg(Gij,Gik) /\ L~LS = {Gij} and
A8: LSeg(Gij,Gik) misses UA;
Gij in {Gij} by TARSKI:def 1;
then
A9: Gij in L~LS by A7,XBOOLE_0:def 4;
Gik in {Gik} by TARSKI:def 1;
then
A10: Gik in L~US by A6,XBOOLE_0:def 4;
then
A11: j <> k by A1,A2,A3,A5,A9,Th57;
A12: j <= width Ga by A4,A5,XXREAL_0:2;
A13: 1 <= k by A3,A4,XXREAL_0:2;
A14: [i,j] in Indices Ga by A1,A2,A3,A12,MATRIX_0:30;
A15: [i,k] in Indices Ga by A1,A2,A5,A13,MATRIX_0:30;
set go = R_Cut(US,Gik);
set co = L_Cut(LS,Gij);
A16: len Ga = width Ga by JORDAN8:def 1;
A17: len US >= 3 by JORDAN1E:15;
then len US >= 1 by XXREAL_0:2;
then 1 in dom US by FINSEQ_3:25;
then
A18: US.1 = US/.1 by PARTFUN1:def 6
.= Wmin by JORDAN1F:5;
A19: Wmin`1 = Wbo by EUCLID:52
.= Ga*(1,k)`1 by A5,A13,A16,JORDAN1A:73;
len Ga >= 4 by JORDAN8:10;
then
A20: len Ga >= 1 by XXREAL_0:2;
then
A21: [1,k] in Indices Ga by A5,A13,MATRIX_0:30;
then
A22: Gik <> US.1 by A1,A15,A18,A19,JORDAN1G:7;
then reconsider go as being_S-Seq FinSequence of TOP-REAL 2 by A10,JORDAN3:35
;
A23: len LS >= 1+2 by JORDAN1E:15;
then
A24: len LS >= 1 by XXREAL_0:2;
then
A25: 1 in dom LS by FINSEQ_3:25;
len LS in dom LS by A24,FINSEQ_3:25;
then
A26: LS.len LS = LS/.len LS by PARTFUN1:def 6
.= Wmin by JORDAN1F:8;
A27: Wmin`1 = Wbo by EUCLID:52
.= Ga*(1,k)`1 by A5,A13,A16,JORDAN1A:73;
A28: [i,j] in Indices Ga by A1,A2,A3,A12,MATRIX_0:30;
then
A29: Gij <> LS.len LS by A1,A21,A26,A27,JORDAN1G:7;
then reconsider co as being_S-Seq FinSequence of TOP-REAL 2 by A9,JORDAN3:34;
A30: [len Ga,k] in Indices Ga by A5,A13,A20,MATRIX_0:30;
A31: LS.1 = LS/.1 by A25,PARTFUN1:def 6
.= Emax by JORDAN1F:6;
Emax`1 = Ebo by EUCLID:52
.= Ga*(len Ga,k)`1 by A5,A13,A16,JORDAN1A:71;
then
A32: Gij <> LS.1 by A2,A28,A30,A31,JORDAN1G:7;
A33: len go >= 1+1 by TOPREAL1:def 8;
A34: Gik in rng US by A1,A2,A5,A10,A13,Th40,JORDAN1G:4;
then
A35: go is_sequence_on Ga by Th38,JORDAN1G:4;
A36: len co >= 1+1 by TOPREAL1:def 8;
A37: Gij in rng LS by A1,A2,A3,A9,A12,Th40,JORDAN1G:5;
then
A38: co is_sequence_on Ga by Th39,JORDAN1G:5;
reconsider go as non constant s.c.c. being_S-Seq FinSequence of TOP-REAL 2
by A33,A35,JGRAPH_1:12,JORDAN8:5;
reconsider co as non constant s.c.c. being_S-Seq FinSequence of TOP-REAL 2
by A36,A38,JGRAPH_1:12,JORDAN8:5;
A39: len go > 1 by A33,NAT_1:13;
then
A40: len go in dom go by FINSEQ_3:25;
then
A41: go/.len go = go.len go by PARTFUN1:def 6
.= Gik by A10,JORDAN3:24;
len co >= 1 by A36,XXREAL_0:2;
then 1 in dom co by FINSEQ_3:25;
then
A42: co/.1 = co.1 by PARTFUN1:def 6
.= Gij by A9,JORDAN3:23;
reconsider m = len go - 1 as Nat by A40,FINSEQ_3:26;
A43: m+1 = len go;
then
A44: len go-'1 = m by NAT_D:34;
A45: LSeg(go,m) c= L~go by TOPREAL3:19;
A46: L~go c= L~US by A10,JORDAN3:41;
then LSeg(go,m) c= L~US by A45;
then
A47: LSeg(go,m) /\ LSeg(Gik,Gij) c= {Gik} by A6,XBOOLE_1:26;
m >= 1 by A33,XREAL_1:19;
then
A48: LSeg(go,m) = LSeg(go/.m,Gik) by A41,A43,TOPREAL1:def 3;
{Gik} c= LSeg(go,m) /\ LSeg(Gik,Gij)
proof
let x be object;
A49: Gik in LSeg(Gik,Gij) by RLTOPSP1:68;
assume x in {Gik};
then
A50: x = Gik by TARSKI:def 1;
Gik in LSeg(go,m) by A48,RLTOPSP1:68;
hence thesis by A50,A49,XBOOLE_0:def 4;
end;
then
A51: LSeg(go,m) /\ LSeg(Gik,Gij) = {Gik} by A47;
A52: LSeg(co,1) c= L~co by TOPREAL3:19;
A53: L~co c= L~LS by A9,JORDAN3:42;
then LSeg(co,1) c= L~LS by A52;
then
A54: LSeg(co,1) /\ LSeg(Gik,Gij) c= {Gij} by A7,XBOOLE_1:26;
A55: LSeg(co,1) = LSeg(Gij,co/.(1+1)) by A36,A42,TOPREAL1:def 3;
{Gij} c= LSeg(co,1) /\ LSeg(Gik,Gij)
proof
let x be object;
A56: Gij in LSeg(Gik,Gij) by RLTOPSP1:68;
assume x in {Gij};
then
A57: x = Gij by TARSKI:def 1;
Gij in LSeg(co,1) by A55,RLTOPSP1:68;
hence thesis by A57,A56,XBOOLE_0:def 4;
end;
then
A58: LSeg(Gik,Gij) /\ LSeg(co,1) = {Gij} by A54;
A59: go/.1 = US/.1 by A10,SPRECT_3:22
.= Wmin by JORDAN1F:5;
then
A60: go/.1 = LS/.len LS by JORDAN1F:8
.= co/.len co by A9,Th35;
A61: rng go c= L~go by A33,SPPOL_2:18;
A62: rng co c= L~co by A36,SPPOL_2:18;
A63: {go/.1} c= L~go /\ L~co
proof
let x be object;
assume x in {go/.1};
then
A64: x = go/.1 by TARSKI:def 1;
then
A65: x in rng go by FINSEQ_6:42;
x in rng co by A60,A64,FINSEQ_6:168;
hence thesis by A61,A62,A65,XBOOLE_0:def 4;
end;
A66: LS.1 = LS/.1 by A25,PARTFUN1:def 6
.= Emax by JORDAN1F:6;
A67: [len Ga,j] in Indices Ga by A3,A12,A20,MATRIX_0:30;
L~go /\ L~co c= {go/.1}
proof
let x be object;
assume
A68: x in L~go /\ L~co;
then
A69: x in L~co by XBOOLE_0:def 4;
A70: now
assume x = Emax;
then
A71: Emax = Gij by A9,A66,A69,JORDAN1E:7;
Ga*(len Ga,j)`1 = Ebo by A3,A12,A16,JORDAN1A:71;
then Emax`1 <> Ebo by A2,A14,A67,A71,JORDAN1G:7;
hence contradiction by EUCLID:52;
end;
x in L~go by A68,XBOOLE_0:def 4;
then x in L~US /\ L~LS by A46,A53,A69,XBOOLE_0:def 4;
then x in {Wmin,Emax} by JORDAN1E:16;
then x = Wmin or x = Emax by TARSKI:def 2;
hence thesis by A59,A70,TARSKI:def 1;
end;
then
A72: L~go /\ L~co = {go/.1} by A63;
set W2 = go/.2;
A73: 2 in dom go by A33,FINSEQ_3:25;
A74: now
assume Gik`1 = Wbo;
then Ga*(1,k)`1 = Ga*(i,k)`1 by A5,A13,A16,JORDAN1A:73;
hence contradiction by A1,A15,A21,JORDAN1G:7;
end;
go = mid(US,1,Gik..US) by A34,JORDAN1G:49
.= US|(Gik..US) by A34,FINSEQ_4:21,FINSEQ_6:116;
then
A75: W2 = US/.2 by A73,FINSEQ_4:70;
set pion = <*Gik,Gij*>;
A76: now
let n be Nat;
assume n in dom pion;
then n in Seg 2 by FINSEQ_1:89;
then n = 1 or n = 2 by FINSEQ_1:2,TARSKI:def 2;
hence ex i,j be Nat st [i,j] in Indices Ga & pion/.n = Ga*(i,j)
by A14,A15,FINSEQ_4:17;
end;
A77: Gik <> Gij by A11,A14,A15,GOBOARD1:5;
A78: Gik`1 = Ga*(i,1)`1 by A1,A2,A5,A13,GOBOARD5:2
.= Gij`1 by A1,A2,A3,A12,GOBOARD5:2;
then LSeg(Gik,Gij) is vertical by SPPOL_1:16;
then pion is being_S-Seq by A77,JORDAN1B:7;
then consider pion1 be FinSequence of TOP-REAL 2 such that
A79: pion1 is_sequence_on Ga and
A80: pion1 is being_S-Seq and
A81: L~pion = L~pion1 and
A82: pion/.1 = pion1/.1 and
A83: pion/.len pion = pion1/.len pion1 and
A84: len pion <= len pion1 by A76,GOBOARD3:2;
reconsider pion1 as being_S-Seq FinSequence of TOP-REAL 2 by A80;
set godo = go^'pion1^'co;
A85: 1+1 <= len Cage(C,n) by GOBOARD7:34,XXREAL_0:2;
A86: 1+1 <= len Rotate(Cage(C,n),Wmin) by GOBOARD7:34,XXREAL_0:2;
len (go^'pion1) >= len go by TOPREAL8:7;
then
A87: len (go^'pion1) >= 1+1 by A33,XXREAL_0:2;
then
A88: len (go^'pion1) > 1+0 by NAT_1:13;
A89: len godo >= len (go^'pion1) by TOPREAL8:7;
then
A90: 1+1 <= len godo by A87,XXREAL_0:2;
A91: US is_sequence_on Ga by JORDAN1G:4;
A92: go/.len go = pion1/.1 by A41,A82,FINSEQ_4:17;
then
A93: go^'pion1 is_sequence_on Ga by A35,A79,TOPREAL8:12;
A94: (go^'pion1)/.len (go^'pion1) = pion/.len pion by A83,FINSEQ_6:156
.= pion/.2 by FINSEQ_1:44
.= co/.1 by A42,FINSEQ_4:17;
then
A95: godo is_sequence_on Ga by A38,A93,TOPREAL8:12;
LSeg(pion1,1) c= L~<*Gik,Gij*> by A81,TOPREAL3:19;
then LSeg(pion1,1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then
A96: LSeg(go,len go-'1) /\ LSeg(pion1,1) c= {Gik} by A44,A51,XBOOLE_1:27;
A97: len pion1 >= 1+1 by A84,FINSEQ_1:44;
{Gik} c= LSeg(go,m) /\ LSeg(pion1,1)
proof
let x be object;
assume x in {Gik};
then
A98: x = Gik by TARSKI:def 1;
A99: Gik in LSeg(go,m) by A48,RLTOPSP1:68;
Gik in LSeg(pion1,1) by A41,A92,A97,TOPREAL1:21;
hence thesis by A98,A99,XBOOLE_0:def 4;
end;
then LSeg(go,len go-'1) /\ LSeg(pion1,1) = { go/.len go } by A41,A44,A96;
then
A100: go^'pion1 is unfolded by A92,TOPREAL8:34;
len pion1 >= 2+0 by A84,FINSEQ_1:44;
then
A101: len pion1-2 >= 0 by XREAL_1:19;
len (go^'pion1)+1-1 = len go+len pion1-1 by FINSEQ_6:139;
then len (go^'pion1)-1 = len go + (len pion1-2)
.= len go + (len pion1-'2) by A101,XREAL_0:def 2;
then
A102: len (go^'pion1)-'1 = len go + (len pion1-'2) by XREAL_0:def 2;
A103: len pion1-1 >= 1 by A97,XREAL_1:19;
then
A104: len pion1-'1 = len pion1-1 by XREAL_0:def 2;
A105: len pion1-'2+1 = len pion1-2+1 by A101,XREAL_0:def 2
.= len pion1-'1 by A103,XREAL_0:def 2;
len pion1-1+1 <= len pion1;
then
A106: len pion1-'1 < len pion1 by A104,NAT_1:13;
LSeg(pion1,len pion1-'1) c= L~<*Gik,Gij*> by A81,TOPREAL3:19;
then LSeg(pion1,len pion1-'1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then
A107: LSeg(pion1,len pion1-'1) /\ LSeg(co,1) c= {Gij} by A58,XBOOLE_1:27;
{Gij} c= LSeg(pion1,len pion1-'1) /\ LSeg(co,1)
proof
let x be object;
assume x in {Gij};
then
A108: x = Gij by TARSKI:def 1;
pion1/.(len pion1-'1+1) = pion/.2 by A83,A104,FINSEQ_1:44
.= Gij by FINSEQ_4:17;
then
A109: Gij in LSeg(pion1,len pion1-'1) by A103,A104,TOPREAL1:21;
Gij in LSeg(co,1) by A55,RLTOPSP1:68;
hence thesis by A108,A109,XBOOLE_0:def 4;
end;
then LSeg(pion1,len pion1-'1) /\ LSeg(co,1) = {Gij} by A107;
then
A110: LSeg(go^'pion1,len go+(len pion1-'2)) /\ LSeg(co,1) = {(go^'pion1)/.
len (go^'pion1)} by A42,A92,A94,A105,A106,TOPREAL8:31;
A111: (go^'pion1) is non trivial by A87,NAT_D:60;
A112: rng pion1 c= L~pion1 by A97,SPPOL_2:18;
A113: {pion1/.1} c= L~go /\ L~pion1
proof
let x be object;
assume x in {pion1/.1};
then
A114: x = pion1/.1 by TARSKI:def 1;
then
A115: x in rng pion1 by FINSEQ_6:42;
x in rng go by A92,A114,FINSEQ_6:168;
hence thesis by A61,A112,A115,XBOOLE_0:def 4;
end;
L~go /\ L~pion1 c= {pion1/.1}
proof
let x be object;
assume
A116: x in L~go /\ L~pion1;
then
A117: x in L~pion1 by XBOOLE_0:def 4;
x in L~go by A116,XBOOLE_0:def 4;
then x in L~pion1 /\ L~US by A46,A117,XBOOLE_0:def 4;
hence thesis by A6,A41,A81,A92,SPPOL_2:21;
end;
then
A118: L~go /\ L~pion1 = {pion1/.1} by A113;
then
A119: (go^'pion1) is s.n.c. by A92,Th54;
rng go /\ rng pion1 c= {pion1/.1} by A61,A112,A118,XBOOLE_1:27;
then
A120: go^'pion1 is one-to-one by Th55;
A121: pion/.len pion = pion/.2 by FINSEQ_1:44
.= co/.1 by A42,FINSEQ_4:17;
A122: {pion1/.len pion1} c= L~co /\ L~pion1
proof
let x be object;
assume x in {pion1/.len pion1};
then
A123: x = pion1/.len pion1 by TARSKI:def 1;
then
A124: x in rng pion1 by FINSEQ_6:168;
x in rng co by A83,A121,A123,FINSEQ_6:42;
hence thesis by A62,A112,A124,XBOOLE_0:def 4;
end;
L~co /\ L~pion1 c= {pion1/.len pion1}
proof
let x be object;
assume
A125: x in L~co /\ L~pion1;
then
A126: x in L~pion1 by XBOOLE_0:def 4;
x in L~co by A125,XBOOLE_0:def 4;
then x in L~pion1 /\ L~LS by A53,A126,XBOOLE_0:def 4;
hence thesis by A7,A42,A81,A83,A121,SPPOL_2:21;
end;
then
A127: L~co /\ L~pion1 = {pion1/.len pion1} by A122;
A128: L~(go^'pion1) /\ L~co = (L~go \/ L~pion1) /\ L~co by A92,TOPREAL8:35
.= {go/.1} \/ {co/.1} by A72,A83,A121,A127,XBOOLE_1:23
.= {(go^'pion1)/.1} \/ {co/.1} by FINSEQ_6:155
.= {(go^'pion1)/.1,co/.1} by ENUMSET1:1;
co/.len co = (go^'pion1)/.1 by A60,FINSEQ_6:155;
then reconsider
godo as non constant standard special_circular_sequence by A90,A94,A95,A100
,A102,A110,A111,A119,A120,A128,JORDAN8:4,5,TOPREAL8:11,33,34;
A129: UA is_an_arc_of W-min C,E-max C by JORDAN6:def 8;
then
A130: UA is connected by JORDAN6:10;
A131: W-min C in UA by A129,TOPREAL1:1;
A132: E-max C in UA by A129,TOPREAL1:1;
set ff = Rotate(Cage(C,n),Wmin);
Wmin in rng Cage(C,n) by SPRECT_2:43;
then
A133: ff/.1 = Wmin by FINSEQ_6:92;
A134: L~ff = L~Cage(C,n) by REVROT_1:33;
then (W-max L~ff)..ff > 1 by A133,SPRECT_5:22;
then (N-min L~ff)..ff > 1 by A133,A134,SPRECT_5:23,XXREAL_0:2;
then (N-max L~ff)..ff > 1 by A133,A134,SPRECT_5:24,XXREAL_0:2;
then
A135: Emax..ff > 1 by A133,A134,SPRECT_5:25,XXREAL_0:2;
A136: now
assume
A137: Gik..US <= 1;
Gik..US >= 1 by A34,FINSEQ_4:21;
then Gik..US = 1 by A137,XXREAL_0:1;
then Gik = US/.1 by A34,FINSEQ_5:38;
hence contradiction by A18,A22,JORDAN1F:5;
end;
A138: Cage(C,n) is_sequence_on Ga by JORDAN9:def 1;
then
A139: ff is_sequence_on Ga by REVROT_1:34;
A140: right_cell(godo,1,Ga)\L~godo c= RightComp godo by A90,A95,JORDAN9:27;
A141: L~godo = L~(go^'pion1) \/ L~co by A94,TOPREAL8:35
.= L~go \/ L~pion1 \/ L~co by A92,TOPREAL8:35;
A142: L~Cage(C,n) = L~US \/ L~LS by JORDAN1E:13;
then
A143: L~US c= L~Cage(C,n) by XBOOLE_1:7;
A144: L~LS c= L~Cage(C,n) by A142,XBOOLE_1:7;
A145: L~go c= L~Cage(C,n) by A46,A143;
A146: L~co c= L~Cage(C,n) by A53,A144;
A147: W-min C in C by SPRECT_1:13;
A148: L~pion = LSeg(Gik,Gij) by SPPOL_2:21;
A149: now
assume W-min C in L~godo;
then
A150: W-min C in L~go \/ L~pion1 or W-min C in L~co by A141,XBOOLE_0:def 3;
per cases by A150,XBOOLE_0:def 3;
suppose
W-min C in L~go;
then C meets L~Cage(C,n) by A145,A147,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
end;
suppose
W-min C in L~pion1;
hence contradiction by A8,A81,A131,A148,XBOOLE_0:3;
end;
suppose
W-min C in L~co;
then C meets L~Cage(C,n) by A146,A147,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
end;
end;
right_cell(Rotate(Cage(C,n),Wmin),1) = right_cell(ff,1,GoB ff) by A86,
JORDAN1H:23
.= right_cell(ff,1,GoB Cage(C,n)) by REVROT_1:28
.= right_cell(ff,1,Ga) by JORDAN1H:44
.= right_cell(ff-:Emax,1,Ga) by A135,A139,Th53
.= right_cell(US,1,Ga) by JORDAN1E:def 1
.= right_cell(R_Cut(US,Gik),1,Ga) by A34,A91,A136,Th52
.= right_cell(go^'pion1,1,Ga) by A39,A93,Th51
.= right_cell(godo,1,Ga) by A88,A95,Th51;
then W-min C in right_cell(godo,1,Ga) by JORDAN1I:6;
then
A151: W-min C in right_cell(godo,1,Ga)\L~godo by A149,XBOOLE_0:def 5;
A152: godo/.1 = (go^'pion1)/.1 by FINSEQ_6:155
.= Wmin by A59,FINSEQ_6:155;
A153: len US >= 2 by A17,XXREAL_0:2;
A154: godo/.2 = (go^'pion1)/.2 by A87,FINSEQ_6:159
.= US/.2 by A33,A75,FINSEQ_6:159
.= (US^'LS)/.2 by A153,FINSEQ_6:159
.= Rotate(Cage(C,n),Wmin)/.2 by JORDAN1E:11;
A155: L~go \/ L~co is compact by COMPTS_1:10;
Wmin in rng go by A59,FINSEQ_6:42;
then Wmin in L~go \/ L~co by A61,XBOOLE_0:def 3;
then
A156: W-min (L~go \/ L~co) = Wmin by A145,A146,A155,Th21,XBOOLE_1:8;
A157: (W-min (L~go \/ L~co))`1 = W-bound (L~go \/ L~co) by EUCLID:52;
A158: Wmin`1 = Wbo by EUCLID:52;
W-bound LSeg(Gik,Gij) = Gik`1 by A78,SPRECT_1:54;
then
A159: W-bound L~pion1 = Gik`1 by A81,SPPOL_2:21;
Gik`1 >= Wbo by A10,A143,PSCOMP_1:24;
then Gik`1 > Wbo by A74,XXREAL_0:1;
then W-min (L~go\/L~co\/L~pion1) = W-min (L~go \/ L~co) by A155,A156,A157
,A158,A159,Th33;
then
A160: W-min L~godo = Wmin by A141,A156,XBOOLE_1:4;
A161: rng godo c= L~godo by A87,A89,SPPOL_2:18,XXREAL_0:2;
2 in dom godo by A90,FINSEQ_3:25;
then
A162: godo/.2 in rng godo by PARTFUN2:2;
godo/.2 in W-most L~Cage(C,n) by A154,JORDAN1I:25;
then (godo/.2)`1 = (W-min L~godo)`1 by A160,PSCOMP_1:31
.= W-bound L~godo by EUCLID:52;
then godo/.2 in W-most L~godo by A161,A162,SPRECT_2:12;
then Rotate(godo,W-min L~godo)/.2 in W-most L~godo by A152,A160,FINSEQ_6:89;
then reconsider godo as clockwise_oriented non constant standard
special_circular_sequence by JORDAN1I:25;
len US in dom US by FINSEQ_5:6;
then
A163: US.len US = US/.len US by PARTFUN1:def 6
.= Emax by JORDAN1F:7;
A164: east_halfline E-max C misses L~go
proof
assume east_halfline E-max C meets L~go;
then consider p be object such that
A165: p in east_halfline E-max C and
A166: p in L~go by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A165;
p in L~US by A46,A166;
then p in east_halfline E-max C /\ L~Cage(C,n) by A143,A165,XBOOLE_0:def 4;
then
A167: p`1 = Ebo by JORDAN1A:83,PSCOMP_1:50;
then
A168: p = Emax by A46,A166,Th46;
then Emax = Gik by A10,A163,A166,Th43;
then Gik`1 = Ga*(len Ga,k)`1 by A5,A13,A16,A167,A168,JORDAN1A:71;
hence contradiction by A2,A15,A30,JORDAN1G:7;
end;
now
assume east_halfline E-max C meets L~godo;
then
A169: east_halfline E-max C meets (L~go \/ L~pion1) or east_halfline E-max
C meets L~co by A141,XBOOLE_1:70;
per cases by A169,XBOOLE_1:70;
suppose
east_halfline E-max C meets L~go;
hence contradiction by A164;
end;
suppose
east_halfline E-max C meets L~pion1;
then consider p be object such that
A170: p in east_halfline E-max C and
A171: p in L~pion1 by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A170;
A172: p`2 = (E-max C)`2 by A170,TOPREAL1:def 11;
i+1 <= len Ga by A2,NAT_1:13;
then i+1-1 <= len Ga-1 by XREAL_1:9;
then
A173: i <= len Ga-'1 by XREAL_0:def 2;
A174: len Ga-'1 <= len Ga by NAT_D:35;
p`1 = Gik`1 by A78,A81,A148,A171,GOBOARD7:5;
then p`1 <= Ga*(len Ga-'1,1)`1 by A1,A5,A13,A16,A20,A173,A174,JORDAN1A:18
;
then p`1 <= E-bound C by A20,JORDAN8:12;
then
A175: p`1 <= (E-max C)`1 by EUCLID:52;
p`1 >= (E-max C)`1 by A170,TOPREAL1:def 11;
then p`1 = (E-max C)`1 by A175,XXREAL_0:1;
then p = E-max C by A172,TOPREAL3:6;
hence contradiction by A8,A81,A132,A148,A171,XBOOLE_0:3;
end;
suppose
east_halfline E-max C meets L~co;
then consider p be object such that
A176: p in east_halfline E-max C and
A177: p in L~co by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A176;
A178: (E-max C)`2 = p`2 by A176,TOPREAL1:def 11;
set tt = Index(p,co)+(Gij..LS)-'1;
set RC = Rotate(Cage(C,n),Emax);
A179: L~RC = L~Cage(C,n) by REVROT_1:33;
consider t be Nat such that
A180: t in dom LS and
A181: LS.t = Gij by A37,FINSEQ_2:10;
1 <= t by A180,FINSEQ_3:25;
then
A182: 1 < t by A32,A181,XXREAL_0:1;
t <= len LS by A180,FINSEQ_3:25;
then Index(Gij,LS)+1 = t by A181,A182,JORDAN3:12;
then
A183: len L_Cut(LS,Gij) = len LS-Index(Gij,LS) by A9,A181,JORDAN3:26;
Index(p,co) < len co by A177,JORDAN3:8;
then Index(p,co) < len LS-'Index(Gij,LS) by A183,XREAL_0:def 2;
then Index(p,co)+1 <= len LS-'Index(Gij,LS) by NAT_1:13;
then
A184: Index(p,co) <= len LS-'Index(Gij,LS)-1 by XREAL_1:19;
A185: co = mid(LS,Gij..LS,len LS) by A37,Th37;
A186: len RC = len Cage(C,n) by FINSEQ_6:179;
p in L~LS by A53,A177;
then p in east_halfline E-max C /\ L~Cage(C,n) by A144,A176,
XBOOLE_0:def 4;
then
A187: p`1 = Ebo by JORDAN1A:83,PSCOMP_1:50;
A188: GoB RC = GoB Cage(C,n) by REVROT_1:28
.= Ga by JORDAN1H:44;
A189: 1+1 <= len LS by A23,XXREAL_0:2;
then
A190: 2 in dom LS by FINSEQ_3:25;
consider jj2 be Nat such that
A191: 1 <= jj2 and
A192: jj2 <= width Ga and
A193: Emax = Ga*(len Ga,jj2) by JORDAN1D:25;
A194: len Ga >= 4 by JORDAN8:10;
then len Ga >= 1 by XXREAL_0:2;
then
A195: [len Ga,jj2] in Indices Ga by A191,A192,MATRIX_0:30;
A196: 1<=Index(p,co) by A177,JORDAN3:8;
LS = RC-:Wmin by JORDAN1G:18;
then
A197: LSeg(LS,1) = LSeg(RC,1) by A189,SPPOL_2:9;
A198: Emax in rng Cage(C,n) by SPRECT_2:46;
RC is_sequence_on Ga by A138,REVROT_1:34;
then consider ii,jj be Nat such that
A199: [ii,jj+1] in Indices Ga and
A200: [ii,jj] in Indices Ga and
A201: RC/.1 = Ga*(ii,jj+1) and
A202: RC/.(1+1) = Ga*(ii,jj) by A85,A179,A186,A198,FINSEQ_6:92,JORDAN1I:23;
A203: jj+1+1 <> jj;
A204: 1 <= jj by A200,MATRIX_0:32;
RC/.1 = E-max L~RC by A179,A198,FINSEQ_6:92;
then
A205: ii = len Ga by A179,A199,A201,A193,A195,GOBOARD1:5;
then ii-1 >= 4-1 by A194,XREAL_1:9;
then
A206: ii-1 >= 1 by XXREAL_0:2;
then
A207: 1 <= ii-'1 by XREAL_0:def 2;
A208: jj <= width Ga by A200,MATRIX_0:32;
then
A209: Ga*(len Ga,jj)`1 = Ebo by A16,A204,JORDAN1A:71;
A210: jj+1 <= width Ga by A199,MATRIX_0:32;
ii+1 <> ii;
then
A211: right_cell(RC,1) = cell(Ga,ii-'1,jj) by A85,A186,A188,A199,A200,A201,A202
,A203,GOBOARD5:def 6;
A212: ii <= len Ga by A200,MATRIX_0:32;
A213: 1 <= ii by A200,MATRIX_0:32;
A214: ii <= len Ga by A199,MATRIX_0:32;
A215: 1 <= jj+1 by A199,MATRIX_0:32;
then
A216: Ebo = Ga*(len Ga,jj+1)`1 by A16,A210,JORDAN1A:71;
A217: 1 <= ii by A199,MATRIX_0:32;
then
A218: ii-'1+1 = ii by XREAL_1:235;
then
A219: ii-'1 < len Ga by A214,NAT_1:13;
then
A220: Ga*(ii-'1,jj+1)`2 = Ga*(1,jj+1)`2 by A215,A210,A207,GOBOARD5:1
.= Ga*(ii,jj+1)`2 by A217,A214,A215,A210,GOBOARD5:1;
A221: E-max C in right_cell(RC,1) by JORDAN1I:7;
then
A222: Ga*(ii-'1,jj)`2 <= (E-max C)`2 by A214,A210,A204,A211,A218,A206,
JORDAN9:17;
A223: (E-max C)`2 <= Ga*(ii-'1,jj+1)`2 by A221,A214,A210,A204,A211,A218,A206,
JORDAN9:17;
Ga*(ii-'1,jj)`2 = Ga*(1,jj)`2 by A204,A208,A207,A219,GOBOARD5:1
.= Ga*(ii,jj)`2 by A213,A212,A204,A208,GOBOARD5:1;
then p in LSeg(RC/.1,RC/.(1+1)) by A187,A178,A201,A202,A205,A222,A223
,A220,A209,A216,GOBOARD7:7;
then
A224: p in LSeg(LS,1) by A85,A197,A186,TOPREAL1:def 3;
A225: Gij..LS<=len LS by A37,FINSEQ_4:21;
Gij..LS <> len LS by A29,A37,FINSEQ_4:19;
then
A226: Gij..LS < len LS by A225,XXREAL_0:1;
A227: Index(Gij,LS)+1 = Gij..LS by A32,A37,Th56;
0+Index(Gij,LS) < len LS by A9,JORDAN3:8;
then len LS-Index(Gij,LS) > 0 by XREAL_1:20;
then Index(p,co) <= len LS-Index(Gij,LS)-1 by A184,XREAL_0:def 2;
then Index(p,co) <= len LS-Gij..LS by A227;
then Index(p,co) <= len LS-'Gij..LS by XREAL_0:def 2;
then
A228: Index(p,co) < len LS-'(Gij..LS)+1 by NAT_1:13;
A229: p in LSeg(co,Index(p,co)) by A177,JORDAN3:9;
1<=Gij..LS by A37,FINSEQ_4:21;
then
A230: LSeg(mid(LS,Gij..LS,len LS),Index(p,co)) = LSeg(LS,Index(p,co)+(
Gij..LS)-'1) by A226,A196,A228,JORDAN4:19;
1<=Index(Gij,LS) by A9,JORDAN3:8;
then
A231: 1+1 <= Gij..LS by A227,XREAL_1:7;
then Index(p,co)+Gij..LS >= 1+1+1 by A196,XREAL_1:7;
then Index(p,co)+Gij..LS-1 >= 1+1+1-1 by XREAL_1:9;
then
A232: tt >= 1+1 by XREAL_0:def 2;
now
per cases by A232,XXREAL_0:1;
suppose
tt > 1+1;
then LSeg(LS,1) misses LSeg(LS,tt) by TOPREAL1:def 7;
hence contradiction by A224,A229,A185,A230,XBOOLE_0:3;
end;
suppose
A233: tt = 1+1;
then 1+1 = Index(p,co)+(Gij..LS)-1 by XREAL_0:def 2;
then 1+1+1 = Index(p,co)+(Gij..LS);
then
A234: Gij..LS = 2 by A196,A231,JORDAN1E:6;
LSeg(LS,1) /\ LSeg(LS,tt) = {LS/.2} by A23,A233,TOPREAL1:def 6;
then p in {LS/.2} by A224,A229,A185,A230,XBOOLE_0:def 4;
then
A235: p = LS/.2 by TARSKI:def 1;
then
A236: p in rng LS by A190,PARTFUN2:2;
p..LS = 2 by A190,A235,FINSEQ_5:41;
then p = Gij by A37,A234,A236,FINSEQ_5:9;
then Gij`1 = Ebo by A235,JORDAN1G:32;
then Gij`1 = Ga*(len Ga,j)`1 by A3,A12,A16,JORDAN1A:71;
hence contradiction by A2,A14,A67,JORDAN1G:7;
end;
end;
hence contradiction;
end;
end;
then east_halfline E-max C c= (L~godo)` by SUBSET_1:23;
then consider W be Subset of TOP-REAL 2 such that
A237: W is_a_component_of (L~godo)` and
A238: east_halfline E-max C c= W by GOBOARD9:3;
W is not bounded by A238,JORDAN2C:121,RLTOPSP1:42;
then W is_outside_component_of L~godo by A237,JORDAN2C:def 3;
then W c= UBD L~godo by JORDAN2C:23;
then
A239: east_halfline E-max C c= UBD L~godo by A238;
E-max C in east_halfline E-max C by TOPREAL1:38;
then E-max C in UBD L~godo by A239;
then E-max C in LeftComp godo by GOBRD14:36;
then UA meets L~godo by A130,A131,A132,A140,A151,Th36;
then
A240: UA meets (L~go \/ L~pion1) or UA meets L~co by A141,XBOOLE_1:70;
A241: UA c= C by JORDAN6:61;
per cases by A240,XBOOLE_1:70;
suppose
UA meets L~go;
then UA meets L~Cage(C,n) by A46,A143,XBOOLE_1:1,63;
hence contradiction by A241,JORDAN10:5,XBOOLE_1:63;
end;
suppose
UA meets L~pion1;
hence contradiction by A8,A81,A148;
end;
suppose
UA meets L~co;
then UA meets L~Cage(C,n) by A53,A144,XBOOLE_1:1,63;
hence contradiction by A241,JORDAN10:5,XBOOLE_1:63;
end;
end;
theorem Th60:
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)) /\ Upper_Arc L~Cage(C,n) = {Gauge(C,n)*(i,k
)} & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_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 and
A2: i < len Gauge(C,n) and
A3: 1 <= j and
A4: j <= k and
A5: k <= width Gauge(C,n) and
A6: n > 0 and
A7: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) = {
Gauge(C,n)*(i,k)} and
A8: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) = {
Gauge(C,n)*(i,j)};
A9: L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) by A6,JORDAN1G:56;
L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) by A6,JORDAN1G:55;
hence thesis by A1,A2,A3,A4,A5,A7,A8,A9,Th58;
end;
theorem Th61:
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)) /\ Upper_Arc L~Cage(C,n) = {Gauge(C,n)*(i,k
)} & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_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 and
A2: i < len Gauge(C,n) and
A3: 1 <= j and
A4: j <= k and
A5: k <= width Gauge(C,n) and
A6: n > 0 and
A7: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) = {
Gauge(C,n)*(i,k)} and
A8: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) = {
Gauge(C,n)*(i,j)};
A9: L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) by A6,JORDAN1G:56;
L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) by A6,JORDAN1G:55;
hence thesis by A1,A2,A3,A4,A5,A7,A8,A9,Th59;
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 Upper_Arc L~Cage(C,n+1) & 1 <= j & j <= width Gauge(C,n+1) implies LSeg(
Gauge(C,1)*(Center Gauge(C,1),1),Gauge(C,n+1)*(Center Gauge(C,n+1),j)) meets
Lower_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 Upper_Arc L~Cage(C,n+1) and
A2: 1 <= j and
A3: j <= width Gauge(C,n+1);
set in1 = Center Gauge(C,n+1);
A4: 1 <= in1 by JORDAN1B:11;
A5: Upper_Arc L~Cage(C,n+1) c= L~Cage(C,n+1) by JORDAN6:61;
A6: in1 <= len Gauge(C,n+1) by JORDAN1B:13;
n+1 >= 0+1 by NAT_1:11;
then
LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),1), Gauge(C,n+1)*(Center Gauge(C,
n+1),j)) c= LSeg(Gauge(C,1)*(Center Gauge(C,1),1), Gauge(C,n+1)*(Center Gauge(C
,n+1),j)) by A2,A3,JORDAN1A:45;
hence thesis by A1,A2,A3,A4,A6,A5,JORDAN1G:57,XBOOLE_1:63;
end;
theorem
for C be Simple_closed_curve for j,k be Nat holds 1 <= j &
j <= k & k <= width Gauge(C,n+1) & LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Upper_Arc L~Cage(C,n+1) = {Gauge(C,n+1
)*(Center Gauge(C,n+1),k)} & LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C
,n+1)*(Center Gauge(C,n+1),k)) /\ Lower_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*(
Center Gauge(C,n+1),j)} implies LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Lower_Arc C
proof
let C be Simple_closed_curve;
let j,k be Nat;
assume that
A1: 1 <= j and
A2: j <= k and
A3: k <= width Gauge(C,n+1) and
A4: LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center
Gauge(C,n+1),k)) /\ Upper_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*(Center Gauge(C,n+1
),k)} and
A5: LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center
Gauge(C,n+1),k)) /\ Lower_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*(Center Gauge(C,n+1
),j)};
A6: len Gauge(C,n+1) >= 4 by JORDAN8:10;
then len Gauge(C,n+1) >= 2 by XXREAL_0:2;
then
A7: 1 < Center Gauge(C,n+1) by JORDAN1B:14;
len Gauge(C,n+1) >= 3 by A6,XXREAL_0:2;
hence thesis by A1,A2,A3,A4,A5,A7,Th60,JORDAN1B:15;
end;
theorem
for C be Simple_closed_curve for j,k be Nat holds 1 <= j &
j <= k & k <= width Gauge(C,n+1) & LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Upper_Arc L~Cage(C,n+1) = {Gauge(C,n+1
)*(Center Gauge(C,n+1),k)} & LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C
,n+1)*(Center Gauge(C,n+1),k)) /\ Lower_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*(
Center Gauge(C,n+1),j)} implies LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Upper_Arc C
proof
let C be Simple_closed_curve;
let j,k be Nat;
assume that
A1: 1 <= j and
A2: j <= k and
A3: k <= width Gauge(C,n+1) and
A4: LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center
Gauge(C,n+1),k)) /\ Upper_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*(Center Gauge(C,n+1
),k)} and
A5: LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center
Gauge(C,n+1),k)) /\ Lower_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*(Center Gauge(C,n+1
),j)};
A6: len Gauge(C,n+1) >= 4 by JORDAN8:10;
then len Gauge(C,n+1) >= 2 by XXREAL_0:2;
then
A7: 1 < Center Gauge(C,n+1) by JORDAN1B:14;
len Gauge(C,n+1) >= 3 by A6,XXREAL_0:2;
hence thesis by A1,A2,A3,A4,A5,A7,Th61,JORDAN1B:15;
end;
:: Moved from JORDAN, AG 20.01.2006
theorem
for X, Y being non empty compact Subset of TOP-REAL 2 st X c= Y & (
W-min Y in X or W-max Y in X) holds W-bound X = W-bound Y
proof
let X, Y be non empty compact Subset of TOP-REAL 2;
assume that
A1: X c= Y and
A2: W-min Y in X or W-max Y in X;
A3: (W-max X)`1 = W-bound X by EUCLID:52;
A4: (W-max Y)`1 = W-bound Y by EUCLID:52;
A5: (W-min Y)`1 = W-bound Y by EUCLID:52;
(W-min X)`1 = W-bound X by EUCLID:52;
hence thesis by A1,A2,A3,A5,A4,Th21,Th22;
end;
theorem
for X, Y being non empty compact Subset of TOP-REAL 2 st X c= Y & (
E-min Y in X or E-max Y in X) holds E-bound X = E-bound Y
proof
let X, Y be non empty compact Subset of TOP-REAL 2;
assume that
A1: X c= Y and
A2: E-min Y in X or E-max Y in X;
A3: (E-max X)`1 = E-bound X by EUCLID:52;
A4: (E-max Y)`1 = E-bound Y by EUCLID:52;
A5: (E-min Y)`1 = E-bound Y by EUCLID:52;
(E-min X)`1 = E-bound X by EUCLID:52;
hence thesis by A1,A2,A3,A5,A4,Th17,Th18;
end;
theorem
for X, Y being non empty compact Subset of TOP-REAL 2 st X c= Y & (
N-min Y in X or N-max Y in X) holds N-bound X = N-bound Y
proof
let X, Y be non empty compact Subset of TOP-REAL 2;
assume that
A1: X c= Y and
A2: N-min Y in X or N-max Y in X;
A3: (N-max X)`2 = N-bound X by EUCLID:52;
A4: (N-max Y)`2 = N-bound Y by EUCLID:52;
A5: (N-min Y)`2 = N-bound Y by EUCLID:52;
(N-min X)`2 = N-bound X by EUCLID:52;
hence thesis by A1,A2,A3,A5,A4,Th15,Th16;
end;
theorem
for X, Y being non empty compact Subset of TOP-REAL 2 st X c= Y & (
S-min Y in X or S-max Y in X) holds S-bound X = S-bound Y
proof
let X, Y be non empty compact Subset of TOP-REAL 2;
assume that
A1: X c= Y and
A2: S-min Y in X or S-max Y in X;
A3: (S-max X)`2 = S-bound X by EUCLID:52;
A4: (S-max Y)`2 = S-bound Y by EUCLID:52;
A5: (S-min Y)`2 = S-bound Y by EUCLID:52;
(S-min X)`2 = S-bound X by EUCLID:52;
hence thesis by A1,A2,A3,A5,A4,Th19,Th20;
end;