Copyright (c) 2002 Association of Mizar Users
environ
vocabulary JORDAN8, PSCOMP_1, BOOLE, JORDAN1A, JORDAN9, GOBOARD1, GOBOARD5,
JORDAN6, SPRECT_2, JORDAN3, FINSEQ_5, JORDAN2C, SPPOL_2, GROUP_2,
RFINSEQ, REALSET1, JORDAN1E, SQUARE_1, FINSEQ_4, TOPREAL2, CONNSP_1,
COMPTS_1, TOPREAL1, SPPOL_1, FINSEQ_1, TREES_1, EUCLID, RELAT_1, MCART_1,
MATRIX_1, GOBOARD9, PRE_TOPC, RELAT_2, SEQM_3, SUBSET_1, FUNCT_1,
ARYTM_1, FINSEQ_6, CARD_1, GOBOARD2, GROUP_1, GRAPH_2;
notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, SQUARE_1,
FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_1,
FINSEQ_6, REALSET1, GRAPH_2, STRUCT_0, PRE_TOPC, TOPREAL2, CARD_1,
CARD_4, BINARITH, CONNSP_1, COMPTS_1, EUCLID, PSCOMP_1, SPRECT_2,
GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13, SPPOL_1,
SPPOL_2, JORDAN3, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A,
JORDAN1E;
constructors JORDAN8, REALSET1, GOBOARD9, JORDAN6, REAL_1, CARD_4, PSCOMP_1,
BINARITH, JORDAN2C, CONNSP_1, JORDAN9, JORDAN1A, SQUARE_1, FINSEQ_4,
GOBRD13, JORDAN1, JORDAN3, RFINSEQ, MATRIX_2, TOPREAL2, JORDAN5C,
PARTFUN1, GRAPH_2, SPRECT_1, GOBOARD2, INT_1, TOPS_1, FINSOP_1, JORDAN1E,
MEMBERED;
clusters SPRECT_1, TOPREAL6, JORDAN8, REVROT_1, INT_1, RELSET_1, SUBSET_1,
PRE_TOPC, SPRECT_3, GOBOARD2, FINSEQ_1, FINSEQ_5, SPPOL_2, JORDAN1A,
JORDAN1B, JORDAN1E, JORDAN1G, GOBRD11, FUNCT_7, XBOOLE_0, XREAL_0,
MEMBERED, ZFMISC_1, NUMBERS, ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, GOBOARD5, XBOOLE_0;
theorems AXIOMS, BINARITH, JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, REAL_1,
GOBOARD5, SQUARE_1, FINSEQ_1, FINSEQ_2, JORDAN4, JORDAN6, SPRECT_2,
FINSEQ_4, FINSEQ_5, FINSEQ_6, GOBOARD7, GOBOARD9, SPPOL_1, SPPOL_2,
TOPREAL4, REVROT_1, TOPREAL1, SPRECT_3, JORDAN5B, AMI_5, JORDAN3,
GOBRD13, INT_1, JORDAN9, RLVECT_1, 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, YELLOW_6, PRE_CIRC, ENUMSET1, GROUP_5, SPRECT_4,
JORDAN1B, SPRECT_5, SCMFSA_7, JORDAN1E, PARTFUN2, JORDAN1F, JORDAN1,
TDLAT_1, JORDAN1G, JORDAN1C, GOBOARD3, JORDAN1H, TOPREAL8, GOBRD14,
JORDAN1D, JORDAN1I, AMISTD_1, ALGSEQ_1, XBOOLE_0, XBOOLE_1, XCMPLX_1;
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,AXIOMS:22;
then G*(i2,j1)`1 = G*(i2,1)`1 by A1,A2,A7,GOBOARD5:3
.= G*(i2,j2)`1 by A3,A4,A7,A8,GOBOARD5:3;
hence G*(i1,j1)`1 < G*(i2,j2)`1 by A1,A2,A5,A6,A7,GOBOARD5:4;
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,AXIOMS:22;
then G*(i1,j2)`2 = G*(1,j2)`2 by A1,A2,A7,GOBOARD5:2
.= G*(i2,j2)`2 by A3,A4,A7,A8,GOBOARD5:2;
hence G*(i1,j1)`2 < G*(i2,j2)`2 by A1,A2,A5,A6,A7,GOBOARD5:5;
end;
definition
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 GRAPH_2:def 2;
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 in rng Cage(C,n) by SPRECT_2:50;
A2: pW..Cage(C,n) <= pW..Cage(C,n);
(f:-pW)/.len(f:-pW) = f/.len f by A1,FINSEQ_5:57
.= f/.1 by FINSEQ_6:def 1
.= pN by JORDAN9:34;
then A3: pN in rng (Cage(C,n):-pW) by REVROT_1:3;
A4: Cage(C,n)-:pW <> {} by A1,FINSEQ_5:50;
(Cage(C,n):-pW)/.1 = pW by FINSEQ_5:56;
then A5: E-max L~Cage(C,n) in rng (Cage(C,n):-E-max L~Cage(C,n))
by FINSEQ_6:46;
(Cage(C,n)-:pW)/.1 = Cage(C,n)/.1 by A1,FINSEQ_5:47
.= pN by JORDAN9:34;
then A6: N-min L~Cage(C,n) in rng (Cage(C,n)-:E-max L~Cage(C,n))
by A4,FINSEQ_6:46;
len(f-:pW) = pW..f by A1,FINSEQ_5:45;
then (f-:pW)/.len (f-:pW) = pW by A1,FINSEQ_5:48;
then A7: pW in rng (Cage(C,n)-:pW) by A4,REVROT_1:3;
N-max L~f in L~f & pW`1 = E-bound L~f by PSCOMP_1:104,SPRECT_1:13;
then (N-max L~f)`1 <= pW`1 by PSCOMP_1:71;
then A8: pN <> pW by SPRECT_2:55;
then A9: Card {pN,pW} = 2 by CARD_2:76;
{pN,pW} c= rng LS
proof
let x be set;
assume x in {pN,pW};
hence x in rng LS by A3,A5,TARSKI:def 2;
end;
then A10: Card {pN,pW} c= Card rng LS by CARD_1:27;
Card rng LS c= Card dom LS by YELLOW_6:3;
then Card rng LS c= len LS by PRE_CIRC:21;
then 2 c= len LS by A9,A10,XBOOLE_1:1;
then len LS >= 2 by CARD_1:56;
then A11: rng LS c= L~LS by SPPOL_2:18;
A12: E-max L~Cage(C,n) in rng LS by FINSEQ_6:66;
A13: Card {pN,pW} = 2 by A8,CARD_2:76;
{pN,pW} c= rng US
proof
let x be set;
assume x in {pN,pW};
hence x in rng US by A6,A7,TARSKI:def 2;
end;
then A14: Card {pN,pW} c= Card rng US by CARD_1:27;
Card rng US c= Card dom US by YELLOW_6:3;
then Card rng US c= len US by PRE_CIRC:21;
then A15: 2 c= len US by A13,A14,XBOOLE_1:1;
then A16: len US >= 2 by CARD_1:56;
then A17: rng US c= L~US by SPPOL_2:18;
len US <> 0 by A15,CARD_1:56;
then A18: US is non empty by FINSEQ_1:25;
A19: E-max L~Cage(C,n) in rng US by A1,A2,FINSEQ_5:49;
US/.1 = Cage(C,n)/.1 by A1,FINSEQ_5:47
.= N-min L~Cage(C,n) by JORDAN9:34;
then A20: N-min L~Cage(C,n) in rng US by A18,FINSEQ_6:46;
LS/.(len LS) = Cage(C,n)/.len Cage(C,n) by A1,FINSEQ_5:57
.= Cage(C,n)/.1 by FINSEQ_6:def 1
.= N-min L~Cage(C,n) by JORDAN9:34;
then A21: N-min L~Cage(C,n) in rng LS by REVROT_1:3;
thus L~US /\ L~LS c=
{N-min L~Cage(C,n),E-max L~Cage(C,n)}
proof
let x be set;
assume A22: x in L~US /\ L~LS;
then A23: x in L~US & x in L~LS by XBOOLE_0:def 3;
reconsider x1=x as Point of TOP-REAL 2 by A22;
consider i1 be Nat such that
A24: 1 <= i1 & i1+1 <= len US and
A25: x1 in LSeg(US,i1) by A23,SPPOL_2:13;
consider i2 be Nat such that
A26: 1 <= i2 & i2+1 <= len LS and
A27: x1 in LSeg(LS,i2) by A23,SPPOL_2:13;
A28: LSeg(US,i1) = LSeg(f,i1) by A24,SPPOL_2:9;
set i3=i2-'1;
A29: i3+1 = i2 by A26,AMI_5:4;
then A30: LSeg(LS,i2) = LSeg(f,i3+pW..f) by A1,SPPOL_2:10;
A31: len US = pW..f by A1,FINSEQ_5:45;
A32: len LS = len f-pW..f+1 by A1,FINSEQ_5:53;
A33: i2-1 >= 1-1 by A26,REAL_1:49;
i2 < len f-pW..f+1 by A26,A32,NAT_1:38;
then i2-1 < len f-pW..f by REAL_1:84;
then i2-1+pW..f < len f by REAL_1:86;
then A34: i3+pW..f < len f by A33,BINARITH:def 3;
A35: i3 >= 0 by NAT_1:18;
A36: pW..f >= 1 by A1,FINSEQ_4:31;
i3+1 < len f-pW..f+1 by A26,A29,A32,NAT_1:38;
then i3 < len f-pW..f by REAL_1:55;
then A37: i3+pW..f < len f by REAL_1:86;
A38: i1+1 < pW..f+1 by A24,A31,NAT_1:38;
1+pW..f <= i3+1+pW..f by A26,A29,REAL_1:55;
then i1+1 < i3+1+pW..f by A38,AXIOMS:22;
then i1+1 < i3+pW..f+1 by XCMPLX_1:1;
then A39: i1+1 <= i3+pW..f by NAT_1:38;
A40: i3+pW..f+1 <= len f by A37,NAT_1:38;
A41: len f > 4 by GOBOARD7:36;
A42: i3+pW..f >= 0 & i1 >= 0 by NAT_1:18;
A43: pW..f-'1+1 = pW..f by A36,AMI_5:4;
assume A44: not x in {N-min L~Cage(C,n),E-max L~Cage(C,n)};
now per cases by A24,A39,REAL_1:def 5;
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) = {} by XBOOLE_0:def 7;
hence contradiction by A25,A27,A28,A30,XBOOLE_0:def 3;
suppose A45: i1 = 1;
A46: i3+pW..f >= 0+2 by A16,A31,A35,REAL_1:55;
now per cases by A46,REAL_1:def 5;
suppose i3+pW..f > 2;
then A47: i1+1 < i3+pW..f by A45;
now per cases by A40,REAL_1:def 5;
suppose i3+pW..f+1 < len f;
then LSeg(f,i1) misses LSeg(f,i3+pW..f) by A47,GOBOARD5:def 4;
then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {} by XBOOLE_0:def 7;
hence contradiction by A25,A27,A28,A30,XBOOLE_0:def 3;
suppose i3+pW..f+1 = len f;
then i3+pW..f = len f-1 by XCMPLX_1:26;
then i3+pW..f = len f-'1 by A42,BINARITH:def 3;
then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {f/.1} by A41,A45,REVROT_1:30
;
then x1 in {f/.1} by A25,A27,A28,A30,XBOOLE_0:def 3;
then x1 = f/.1 by TARSKI:def 1
.= pN by JORDAN9:34;
hence contradiction by A44,TARSKI:def 2;
end;
hence contradiction;
suppose A48: i3+pW..f = 2;
then A49: x1 in LSeg(f,1) /\ LSeg(f,1+1)
by A25,A27,A28,A30,A45,XBOOLE_0:def 3;
1 + 2 <= len f by A41,AXIOMS:22;
then x1 in {f/.(1+1)} by A49,TOPREAL1:def 8;
then A50: x1 = f/.(1+1) by TARSKI:def 1;
A51: 0+1 in dom LS by FINSEQ_5:6;
0+pW..f >= i3+pW..f by A15,A31,A48,CARD_1:56;
then i3 <= 0 by REAL_1:53;
then i3 = 0 by NAT_1:18;
then LS/.1 = x1 by A1,A48,A50,A51,FINSEQ_5:55;
then x1 = pW by FINSEQ_5:56;
hence contradiction by A44,TARSKI:def 2;
end;
hence contradiction;
suppose A52: i1+1 = i3+pW..f;
0+pW..f <= i3+pW..f by A35,REAL_1:55;
then pW..f = i1+1 by A24,A31,A52,AXIOMS:21;
then i1 = pW..f-1 by XCMPLX_1:26;
then A53: i1 = pW..f-'1 by A42,BINARITH:def 3;
i3+pW..f >= pW..f by NAT_1:29;
then pW..f < len f by A34,AXIOMS:22;
then pW..f+1 <= len f by NAT_1:38;
then pW..f-'1 + (1+1) <= len f by A43,XCMPLX_1:1;
then LSeg(f,i1) /\ LSeg(f,i3+(pW..f)) = {f/.(pW..f)}
by A24,A43,A52,A53,TOPREAL1:def 8;
then x1 in {f/.(pW..f)} by A25,A27,A28,A30,XBOOLE_0:def 3;
then x1 = f/.(pW..f) by TARSKI:def 1
.= pW by A1,FINSEQ_5:41;
hence contradiction by A44,TARSKI:def 2;
end;
hence contradiction;
end;
thus {N-min L~Cage(C,n),E-max L~Cage(C,n)} c= L~US /\ L~LS
proof
let x be set;
assume A54: x in {N-min L~Cage(C,n),E-max L~Cage(C,n)};
per cases by A54,TARSKI:def 2;
suppose x = N-min L~Cage(C,n);
hence x in L~US /\ L~LS by A11,A17,A20,A21,XBOOLE_0:def 3;
suppose x = E-max L~Cage(C,n);
hence x in L~US /\ L~LS by A11,A12,A17,A19,XBOOLE_0:def 3;
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: Cage(C,n)/.1 = Nmi by JORDAN9:34;
A2: Nmi in rng Cage(C,n) by SPRECT_2:43;
A3: Wmi in rng Cage(C,n) by SPRECT_2:47;
A4: Ema in rng Cage(C,n) by SPRECT_2:50;
A5: Nmi..Cage(C,n) < Nma..Cage(C,n) by A1,SPRECT_2:72;
A6: Nma..Cage(C,n) <= Ema..Cage(C,n) by A1,SPRECT_2:74;
then A7: Nmi..Cage(C,n) < Ema..Cage(C,n) by A5,AXIOMS:22;
A8: Ema..Cage(C,n) < Emi..Cage(C,n) by A1,SPRECT_2:75;
A9: Emi..Cage(C,n) <= Sma..Cage(C,n) by A1,SPRECT_2:76;
A10: Sma..Cage(C,n) < Smi..Cage(C,n) by A1,SPRECT_2:77;
A11: Smi..Cage(C,n) <= Wmi..Cage(C,n) by A1,SPRECT_2:78;
Ema..Cage(C,n) < Sma..Cage(C,n) by A8,A9,AXIOMS:22;
then Ema..Cage(C,n) < Smi..Cage(C,n) by A10,AXIOMS:22;
then A12: Ema..Cage(C,n) < Wmi..Cage(C,n) by A11,AXIOMS:22;
then A13: Ema in rng (Cage(C,n)-:Wmi) by A3,A4,FINSEQ_5:49;
A14: Cage(C,n)-:Wmi <> {} by A3,FINSEQ_5:50;
(Cage(C,n)-:Wmi)/.1 = Cage(C,n)/.1 by A3,FINSEQ_5:47
.= Nmi by JORDAN9:34;
then A15: Nmi in rng (Cage(C,n)-:Wmi) by A14,FINSEQ_6:46;
len(Cage(C,n)-:Wmi) = Wmi..Cage(C,n) by A3,FINSEQ_5:45;
then (Cage(C,n)-:Wmi)/.len (Cage(C,n)-:Wmi) = Wmi by A3,FINSEQ_5:48;
then A16: Wmi in rng (Cage(C,n)-:Wmi) by A14,REVROT_1:3;
Wma in L~Cage(C,n) & Nmi`2 = N-bound L~Cage(C,n)
by PSCOMP_1:94,SPRECT_1:15;
then Wma`2 <= Nmi`2 by PSCOMP_1:71;
then A17: Nmi <> Wmi by SPRECT_2:61;
then A18: Card {Nmi,Wmi} = 2 by CARD_2:76;
{Nmi,Wmi} c= rng (Cage(C,n)-:Wmi)
proof
let x be set;
assume x in {Nmi,Wmi};
hence x in rng (Cage(C,n)-:Wmi) by A15,A16,TARSKI:def 2;
end;
then A19: Card {Nmi,Wmi} c= Card rng (Cage(C,n)-:Wmi) by CARD_1:27;
Card rng (Cage(C,n)-:Wmi) c= Card dom (Cage(C,n)-:Wmi) by YELLOW_6:3;
then Card rng (Cage(C,n)-:Wmi) c= len (Cage(C,n)-:Wmi) by PRE_CIRC:21;
then 2 c= len (Cage(C,n)-:Wmi) by A18,A19,XBOOLE_1:1;
then len (Cage(C,n)-:Wmi) >= 2 by CARD_1:56;
then A20: rng (Cage(C,n)-:Wmi) c= L~(Cage(C,n)-:Wmi) by SPPOL_2:18;
A21: Nmi..Cage(C,n) < Wmi..Cage(C,n) by A7,A12,AXIOMS:22;
then A22: Nmi in rng (Cage(C,n)-:Wmi) by A2,A3,FINSEQ_5:49;
A23: Ema..(Cage(C,n)-:Wmi) <> 1
proof
assume A24: Ema..(Cage(C,n)-:Wmi) = 1;
Nmi..(Cage(C,n)-:Wmi) = Nmi..Cage(C,n) by A2,A3,A21,SPRECT_5:3
.= 1 by A1,FINSEQ_6:47;
hence contradiction by A5,A6,A13,A22,A24,FINSEQ_5:10;
end;
then A25: Ema in rng (Cage(C,n)-:Wmi/^1) by A13,FINSEQ_6:83;
A26: Nmi`1 < Nma`1 by SPRECT_2:55;
Nma`1 <= (NE-corner L~Cage(C,n))`1 by PSCOMP_1:97;
then Nma`1 <= E-bound L~Cage(C,n) by PSCOMP_1:76;
then A27: Nmi <> Ema by A26,PSCOMP_1:104;
not Ema in rng (Cage(C,n):-Wmi)
proof
assume A28: Ema in rng (Cage(C,n):-Wmi);
(Cage(C,n):-Wmi)/.len(Cage(C,n):-Wmi) = Cage(C,n)/.len Cage(C,n)
by A3,FINSEQ_5:57
.= Cage(C,n)/.1 by FINSEQ_6:def 1
.= Nmi by JORDAN9:34;
then A29: Nmi in rng (Cage(C,n):-Wmi) by REVROT_1:3;
(Cage(C,n):-Wmi)/.1 = Wmi by FINSEQ_5:56;
then A30: Wmi in rng (Cage(C,n):-Wmi) by FINSEQ_6:46;
Wma in L~Cage(C,n) & Nmi`2 = N-bound L~Cage(C,n)
by PSCOMP_1:94,SPRECT_1:15;
then Wma`2 <= Nmi`2 by PSCOMP_1:71;
then Nmi <> Wmi by SPRECT_2:61;
then A31: Card {Nmi,Wmi} = 2 by CARD_2:76;
{Nmi,Wmi} c= rng (Cage(C,n):-Wmi)
proof
let x be set;
assume x in {Nmi,Wmi};
hence x in rng (Cage(C,n):-Wmi) by A29,A30,TARSKI:def 2;
end;
then A32: Card {Nmi,Wmi} c= Card rng (Cage(C,n):-Wmi) by CARD_1:27;
Card rng (Cage(C,n):-Wmi) c= Card dom (Cage(C,n):-Wmi) by YELLOW_6:3;
then Card rng (Cage(C,n):-Wmi) c= len (Cage(C,n):-Wmi) by PRE_CIRC:21;
then 2 c= len (Cage(C,n):-Wmi) by A31,A32,XBOOLE_1:1;
then len (Cage(C,n):-Wmi) >= 2 by CARD_1:56;
then rng (Cage(C,n):-Wmi) c= L~(Cage(C,n):-Wmi) by SPPOL_2:18;
then Ema in L~(Cage(C,n)-:Wmi) /\ L~(Cage(C,n):-Wmi)
by A13,A20,A28,XBOOLE_0:def
3;
then Ema in {Nmi,Wmi} by JORDAN1G:25;
then Ema = Wmi by A27,TARSKI:def 2;
hence contradiction by TOPREAL5:25;
end;
then A33: Ema in rng (Cage(C,n)-:Wmi/^1) \ rng (Cage(C,n):-Wmi)
by A25,XBOOLE_0:def 4
;
A34: Wmi in rng (Cage(C,n):-Ema) by A3,A4,A12,FINSEQ_6:67;
A35: Card {Nmi,Ema} = 2 by A27,CARD_2:76;
(Cage(C,n):-Ema)/.len(Cage(C,n):-Ema) = Cage(C,n)/.len Cage(C,n)
by A4,FINSEQ_5:57
.= Cage(C,n)/.1 by FINSEQ_6:def 1
.= Nmi by JORDAN9:34;
then A36: Nmi in rng (Cage(C,n):-Ema) by REVROT_1:3;
(Cage(C,n):-Ema)/.1 = Ema by FINSEQ_5:56;
then A37: Ema in rng (Cage(C,n):-Ema) by FINSEQ_6:46;
{Nmi,Ema} c= rng (Cage(C,n):-Ema)
proof
let x be set;
assume x in {Nmi,Ema};
hence x in rng (Cage(C,n):-Ema) by A36,A37,TARSKI:def 2;
end;
then A38: Card {Nmi,Ema} c= Card rng (Cage(C,n):-Ema) by CARD_1:27;
Card rng (Cage(C,n):-Ema) c= Card dom (Cage(C,n):-Ema) by YELLOW_6:3;
then Card rng (Cage(C,n):-Ema) c= len (Cage(C,n):-Ema) by PRE_CIRC:21;
then 2 c= len (Cage(C,n):-Ema) by A35,A38,XBOOLE_1:1;
then len (Cage(C,n):-Ema) >= 2 by CARD_1:56;
then A39: 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 A40: Wmi in rng (Cage(C,n)-:Ema);
then A41: Cage(C,n)-:Ema is non empty by FINSEQ_1:27;
(Cage(C,n)-:Ema)/.1 = Cage(C,n)/.1 by A4,FINSEQ_5:47
.= Nmi by JORDAN9:34;
then A42: Nmi in rng (Cage(C,n)-:Ema) by A41,FINSEQ_6:46;
(Cage(C,n)-:Ema)/.len (Cage(C,n)-:Ema) =
(Cage(C,n)-:Ema)/.(Ema..Cage(C,n)) by A4,FINSEQ_5:45
.= Ema by A4,FINSEQ_5:48;
then A43: Ema in rng (Cage(C,n)-:Ema) by A41,REVROT_1:3;
{Nmi,Ema} c= rng (Cage(C,n)-:Ema)
proof
let x be set;
assume x in {Nmi,Ema};
hence x in rng (Cage(C,n)-:Ema) by A42,A43,TARSKI:def 2;
end;
then A44: Card {Nmi,Ema} c= Card rng (Cage(C,n)-:Ema) by CARD_1:27;
Card rng (Cage(C,n)-:Ema) c= Card dom (Cage(C,n)-:Ema) by YELLOW_6:3;
then Card rng (Cage(C,n)-:Ema) c= len (Cage(C,n)-:Ema) by PRE_CIRC:21;
then 2 c= len (Cage(C,n)-:Ema) by A35,A44,XBOOLE_1:1;
then len (Cage(C,n)-:Ema) >= 2 by CARD_1:56;
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 A34,A39,A40,XBOOLE_0:def
3
;
then Wmi in {Nmi,Ema} by Th3;
then Wmi = Ema by A17,TARSKI:def 2;
hence contradiction by TOPREAL5:25;
end;
then A45: Wmi in rng Cage(C,n) \ rng(Cage(C,n)-:Ema) by A3,XBOOLE_0:def 4;
RotWmi-:Ema = ((Cage(C,n):-Wmi)^((Cage(C,n)-:Wmi)/^1))-:Ema
by A3,FINSEQ_6:def 2
.= (Cage(C,n):-Wmi)^(((Cage(C,n)-:Wmi)/^1)-:Ema) by A33,FINSEQ_6:72
.= (Cage(C,n):-Wmi)^(((Cage(C,n)-:Wmi)-:Ema)/^1) by A13,A23,FINSEQ_6:65
.= ((Cage(C,n):-Ema):-Wmi)^(((Cage(C,n)-:Wmi)-:Ema)/^1)
by A4,A45,FINSEQ_6:76
.= ((Cage(C,n):-Ema):-Wmi)^((Cage(C,n)-:Ema)/^1) by A3,A13,FINSEQ_6:80
.= ((Cage(C,n):-Ema)^((Cage(C,n)-:Ema)/^1)):-Wmi by A34,FINSEQ_6:69
.= RotEma:-Wmi by A4,FINSEQ_6:def 2;
hence Upper_Seq(C,n) = Rotate(Cage(C,n),E-max L~Cage(C,n)):-
W-min L~Cage(C,n) 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: Upper_Seq(C,n) = Rotate(Cage(C,n),p)-:E-max L~Cage(C,n)
by JORDAN1E:def 1;
A2: p in rng Cage(C,n) by SPRECT_2:47;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
then E-max L~Cage(C,n) in rng Rotate(Cage(C,n),p) by A2,FINSEQ_6:96;
then Upper_Seq(C,n)/.1 = Rotate(Cage(C,n),p)/.1 by A1,FINSEQ_5:47;
then Upper_Seq(C,n)/.1 = p by A2,FINSEQ_6:98;
hence A3: p in rng Upper_Seq(C,n) by FINSEQ_6:46;
len Upper_Seq(C,n) >= 2 by TOPREAL1:def 10;
then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18;
hence p in L~Upper_Seq(C,n) 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));
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
then A1: rng f = rng Cage(C,n) by FINSEQ_6:96;
A2: x in rng Cage(C,n) by SPRECT_2:48;
A3: p in rng Cage(C,n) by SPRECT_2:47;
A4: Lower_Seq(C,n) = f-:W-min L~Cage(C,n) by JORDAN1G:26;
A5: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
then W-min L~Cage(C,n) in rng f by A5,FINSEQ_6:96;
then A6: Lower_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:47;
A7: Lower_Seq(C,n)/.1 = E-max L~Cage(C,n) by JORDAN1F:6;
A8: L~Cage(C,n) = L~f by REVROT_1:33;
then (W-min L~f)..f < (W-max L~f)..f by A6,A7,SPRECT_5:43;
then x in rng(f:-p) by A1,A2,A3,A8,FINSEQ_6:67;
hence A9: x in rng Upper_Seq(C,n) by Th4;
len Upper_Seq(C,n) >= 2 by TOPREAL1:def 10;
then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18;
hence x in L~Upper_Seq(C,n) by A9;
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));
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
then A1: rng f = rng Cage(C,n) by FINSEQ_6:96;
A2: x in rng Cage(C,n) by SPRECT_2:43;
A3: p in rng Cage(C,n) by SPRECT_2:47;
A4: Lower_Seq(C,n) = f-:W-min L~Cage(C,n) by JORDAN1G:26;
A5: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
then W-min L~Cage(C,n) in rng f by A5,FINSEQ_6:96;
then A6: Lower_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:47;
A7: Lower_Seq(C,n)/.1 = E-max L~Cage(C,n) by JORDAN1F:6;
A8: L~Cage(C,n) = L~f by REVROT_1:33;
then A9: (W-min L~f)..f < (W-max L~f)..f by A6,A7,SPRECT_5:43;
(W-max L~f)..f <= (N-min L~f)..f by A6,A7,A8,SPRECT_5:44;
then p..f < x..f by A8,A9,AXIOMS:22;
then x in rng(f:-p) by A1,A2,A3,FINSEQ_6:67;
hence A10: x in rng Upper_Seq(C,n) by Th4;
len Upper_Seq(C,n) >= 2 by TOPREAL1:def 10;
then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18;
hence x in L~Upper_Seq(C,n) by A10;
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));
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
then A1: rng f = rng Cage(C,n) by FINSEQ_6:96;
A2: x in rng Cage(C,n) by SPRECT_2:44;
A3: p in rng Cage(C,n) by SPRECT_2:47;
A4: Lower_Seq(C,n) = f-:W-min L~Cage(C,n) by JORDAN1G:26;
A5: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
then W-min L~Cage(C,n) in rng f by A5,FINSEQ_6:96;
then A6: Lower_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:47;
A7: Lower_Seq(C,n)/.1 = E-max L~Cage(C,n) by JORDAN1F:6;
A8: L~Cage(C,n) = L~f by REVROT_1:33;
then A9: (W-min L~f)..f < (W-max L~f)..f by A6,A7,SPRECT_5:43;
A10: (W-max L~f)..f <= (N-min L~f)..f by A6,A7,A8,SPRECT_5:44;
per cases;
suppose N-max L~f <> E-max L~f;
then (N-min L~f)..f < (N-max L~f)..f by A6,A7,A8,SPRECT_5:45;
then (W-max L~f)..f < (N-max L~f)..f by A10,AXIOMS:22;
then p..f < x..f by A8,A9,AXIOMS:22;
then x in rng(f:-p) by A1,A2,A3,FINSEQ_6:67;
hence A11: x in rng Upper_Seq(C,n) by Th4;
len Upper_Seq(C,n) >= 2 by TOPREAL1:def 10;
then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18;
hence x in L~Upper_Seq(C,n) by A11;
suppose A12: N-max L~f = E-max L~f;
A13: Upper_Seq(C,n) = Rotate(Cage(C,n),p)-:E-max L~Cage(C,n)
by JORDAN1E:def 1;
A14: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
then A15: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A14,FINSEQ_6:96;
(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));
hence A16: x in rng Upper_Seq(C,n) by A8,A12,A13,A15,FINSEQ_5:49;
len Upper_Seq(C,n) >= 2 by TOPREAL1:def 10;
then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18;
hence x in L~Upper_Seq(C,n) by A16;
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: Upper_Seq(C,n) = Rotate(Cage(C,n),p)-:E-max L~Cage(C,n)
by JORDAN1E:def 1;
A2: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
then A3: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A2,FINSEQ_6:96;
(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));
hence A4: x in rng Upper_Seq(C,n) by A1,A3,FINSEQ_5:49;
len Upper_Seq(C,n) >= 2 by TOPREAL1:def 10;
then rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18;
hence x in L~Upper_Seq(C,n) by A4;
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:66;
len Lower_Seq(C,n) >= 2 by TOPREAL1:def 10;
then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18;
hence p in L~Lower_Seq(C,n) 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));
W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
then A1: rng f = rng Cage(C,n) by FINSEQ_6:96;
A2: x in rng Cage(C,n) by SPRECT_2:49;
A3: p in rng Cage(C,n) by SPRECT_2:50;
A4: Upper_Seq(C,n) = f-:E-max L~Cage(C,n) by JORDAN1E:def 1;
A5: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
then E-max L~Cage(C,n) in rng f by A5,FINSEQ_6:96;
then A6: Upper_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:47;
A7: Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by JORDAN1F:5;
A8: L~Cage(C,n) = L~f by REVROT_1:33;
then (E-max L~f)..f < (E-min L~f)..f by A6,A7,SPRECT_5:27;
then x in rng(f:-p) by A1,A2,A3,A8,FINSEQ_6:67;
hence A9: x in rng Lower_Seq(C,n) by JORDAN1E:def 2;
len Lower_Seq(C,n) >= 2 by TOPREAL1:def 10;
then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18;
hence x in L~Lower_Seq(C,n) by A9;
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));
W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
then A1: rng f = rng Cage(C,n) by FINSEQ_6:96;
A2: x in rng Cage(C,n) by SPRECT_2:46;
A3: p in rng Cage(C,n) by SPRECT_2:50;
A4: Upper_Seq(C,n) = f-:E-max L~Cage(C,n) by JORDAN1E:def 1;
A5: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
then E-max L~Cage(C,n) in rng f by A5,FINSEQ_6:96;
then A6: Upper_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:47;
A7: Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by JORDAN1F:5;
A8: L~Cage(C,n) = L~f by REVROT_1:33;
then A9: (E-max L~f)..f < (E-min L~f)..f by A6,A7,SPRECT_5:27;
(E-min L~f)..f <= (S-max L~f)..f by A6,A7,A8,SPRECT_5:28;
then p..f < x..f by A8,A9,AXIOMS:22;
then x in rng(f:-p) by A1,A2,A3,FINSEQ_6:67;
hence A10: x in rng Lower_Seq(C,n) by JORDAN1E:def 2;
len Lower_Seq(C,n) >= 2 by TOPREAL1:def 10;
then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18;
hence x in L~Lower_Seq(C,n) by A10;
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));
W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
then A1: rng f = rng Cage(C,n) by FINSEQ_6:96;
A2: x in rng Cage(C,n) by SPRECT_2:45;
A3: p in rng Cage(C,n) by SPRECT_2:50;
A4: Upper_Seq(C,n) = f-:E-max L~Cage(C,n) by JORDAN1E:def 1;
A5: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
then E-max L~Cage(C,n) in rng f by A5,FINSEQ_6:96;
then A6: Upper_Seq(C,n)/.1 = f/.1 by A4,FINSEQ_5:47;
A7: Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by JORDAN1F:5;
A8: L~Cage(C,n) = L~f by REVROT_1:33;
then A9: (E-max L~f)..f < (E-min L~f)..f by A6,A7,SPRECT_5:27;
A10: (E-min L~f)..f <= (S-max L~f)..f by A6,A7,A8,SPRECT_5:28;
per cases;
suppose S-min L~f <> W-min L~f;
then (S-max L~f)..f < (S-min L~f)..f by A6,A7,A8,SPRECT_5:29;
then (E-min L~f)..f < (S-min L~f)..f by A10,AXIOMS:22;
then p..f < x..f by A8,A9,AXIOMS:22;
then x in rng(f:-p) by A1,A2,A3,FINSEQ_6:67;
hence A11: x in rng Lower_Seq(C,n) by JORDAN1E:def 2;
len Lower_Seq(C,n) >= 2 by TOPREAL1:def 10;
then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18;
hence x in L~Lower_Seq(C,n) by A11;
suppose A12: 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 A13: x in rng Lower_Seq(C,n) by A8,A12,REVROT_1:3;
len Lower_Seq(C,n) >= 2 by TOPREAL1:def 10;
then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18;
hence x in L~Lower_Seq(C,n) by A13;
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 REVROT_1:3;
len Lower_Seq(C,n) >= 2 by TOPREAL1:def 10;
then rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18;
hence p in L~Lower_Seq(C,n) by A1;
end;
theorem
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-bound Y by A1,JORDAN1E:1;
A4: (N-min X)`2 = N-bound X & (N-min Y)`2 = N-bound Y by PSCOMP_1:94;
N-bound X >= (N-min Y)`2 by A2,PSCOMP_1:71;
then A5: N-bound X = N-bound Y by A3,A4,AXIOMS:21;
then N-min Y in N-most X by A2,A4,SPRECT_2:14;
then A6: (N-min X)`1 <= (N-min Y)`1 by PSCOMP_1:98;
N-min X in X by SPRECT_1:13;
then N-min X in N-most Y by A1,A4,A5,SPRECT_2:14;
then (N-min X)`1 >= (N-min Y)`1 by PSCOMP_1:98;
then (N-min X)`1 = (N-min Y)`1 by A6,AXIOMS:21;
hence N-min X = N-min Y by A4,A5,TOPREAL3:11;
end;
theorem
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-bound Y by A1,JORDAN1E:1;
A4: (N-max X)`2 = N-bound X & (N-max Y)`2 = N-bound Y by PSCOMP_1:94;
N-bound X >= (N-max Y)`2 by A2,PSCOMP_1:71;
then A5: N-bound X = N-bound Y by A3,A4,AXIOMS:21;
then N-max Y in N-most X by A2,A4,SPRECT_2:14;
then A6: (N-max X)`1 >= (N-max Y)`1 by PSCOMP_1:98;
N-max X in X by SPRECT_1:13;
then N-max X in N-most Y by A1,A4,A5,SPRECT_2:14;
then (N-max X)`1 <= (N-max Y)`1 by PSCOMP_1:98;
then (N-max X)`1 = (N-max Y)`1 by A6,AXIOMS:21;
hence N-max X = N-max Y by A4,A5,TOPREAL3:11;
end;
theorem
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-bound Y by A1,JORDAN1E:2;
A4: (E-min X)`1 = E-bound X & (E-min Y)`1 = E-bound Y by PSCOMP_1:104;
E-bound X >= (E-min Y)`1 by A2,PSCOMP_1:71;
then A5: E-bound X = E-bound Y by A3,A4,AXIOMS:21;
then E-min Y in E-most X by A2,A4,SPRECT_2:17;
then A6: (E-min X)`2 <= (E-min Y)`2 by PSCOMP_1:108;
E-min X in X by SPRECT_1:16;
then E-min X in E-most Y by A1,A4,A5,SPRECT_2:17;
then (E-min X)`2 >= (E-min Y)`2 by PSCOMP_1:108;
then (E-min X)`2 = (E-min Y)`2 by A6,AXIOMS:21;
hence E-min X = E-min Y by A4,A5,TOPREAL3:11;
end;
theorem
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-bound Y by A1,JORDAN1E:2;
A4: (E-max X)`1 = E-bound X & (E-max Y)`1 = E-bound Y by PSCOMP_1:104;
E-bound X >= (E-max Y)`1 by A2,PSCOMP_1:71;
then A5: E-bound X = E-bound Y by A3,A4,AXIOMS:21;
then E-max Y in E-most X by A2,A4,SPRECT_2:17;
then A6: (E-max X)`2 >= (E-max Y)`2 by PSCOMP_1:108;
E-max X in X by SPRECT_1:16;
then E-max X in E-most Y by A1,A4,A5,SPRECT_2:17;
then (E-max X)`2 <= (E-max Y)`2 by PSCOMP_1:108;
then (E-max X)`2 = (E-max Y)`2 by A6,AXIOMS:21;
hence E-max X = E-max Y by A4,A5,TOPREAL3:11;
end;
theorem
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-bound Y by A1,JORDAN1E:3;
A4: (S-min X)`2 = S-bound X & (S-min Y)`2 = S-bound Y by PSCOMP_1:114;
S-bound X <= (S-min Y)`2 by A2,PSCOMP_1:71;
then A5: S-bound X = S-bound Y by A3,A4,AXIOMS:21;
then S-min Y in S-most X by A2,A4,SPRECT_2:15;
then A6: (S-min X)`1 <= (S-min Y)`1 by PSCOMP_1:118;
S-min X in X by SPRECT_1:14;
then S-min X in S-most Y by A1,A4,A5,SPRECT_2:15;
then (S-min X)`1 >= (S-min Y)`1 by PSCOMP_1:118;
then (S-min X)`1 = (S-min Y)`1 by A6,AXIOMS:21;
hence S-min X = S-min Y by A4,A5,TOPREAL3:11;
end;
theorem
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-bound Y by A1,JORDAN1E:3;
A4: (S-max X)`2 = S-bound X & (S-max Y)`2 = S-bound Y by PSCOMP_1:114;
S-bound X <= (S-max Y)`2 by A2,PSCOMP_1:71;
then A5: S-bound X = S-bound Y by A3,A4,AXIOMS:21;
then S-max Y in S-most X by A2,A4,SPRECT_2:15;
then A6: (S-max X)`1 >= (S-max Y)`1 by PSCOMP_1:118;
S-max X in X by SPRECT_1:14;
then S-max X in S-most Y by A1,A4,A5,SPRECT_2:15;
then (S-max X)`1 <= (S-max Y)`1 by PSCOMP_1:118;
then (S-max X)`1 = (S-max Y)`1 by A6,AXIOMS:21;
hence S-max X = S-max Y by A4,A5,TOPREAL3:11;
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-bound Y by A1,JORDAN1E:4;
A4: (W-min X)`1 = W-bound X & (W-min Y)`1 = W-bound Y by PSCOMP_1:84;
W-bound X <= (W-min Y)`1 by A2,PSCOMP_1:71;
then A5: W-bound X = W-bound Y by A3,A4,AXIOMS:21;
then W-min Y in W-most X by A2,A4,SPRECT_2:16;
then A6: (W-min X)`2 <= (W-min Y)`2 by PSCOMP_1:88;
W-min X in X by SPRECT_1:15;
then W-min X in W-most Y by A1,A4,A5,SPRECT_2:16;
then (W-min X)`2 >= (W-min Y)`2 by PSCOMP_1:88;
then (W-min X)`2 = (W-min Y)`2 by A6,AXIOMS:21;
hence W-min X = W-min Y by A4,A5,TOPREAL3:11;
end;
theorem
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-bound Y by A1,JORDAN1E:4;
A4: (W-max X)`1 = W-bound X & (W-max Y)`1 = W-bound Y by PSCOMP_1:84;
W-bound X <= (W-max Y)`1 by A2,PSCOMP_1:71;
then A5: W-bound X = W-bound Y by A3,A4,AXIOMS:21;
then W-max Y in W-most X by A2,A4,SPRECT_2:16;
then A6: (W-max X)`2 >= (W-max Y)`2 by PSCOMP_1:88;
W-max X in X by SPRECT_1:15;
then W-max X in W-most Y by A1,A4,A5,SPRECT_2:16;
then (W-max X)`2 <= (W-max Y)`2 by PSCOMP_1:88;
then (W-max X)`2 = (W-max Y)`2 by A6,AXIOMS:21;
hence W-max X = W-max Y by A4,A5,TOPREAL3:11;
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 SQUARE_1:def 2;
hence N-bound (X\/Y) = N-bound Y by SPRECT_1:56;
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 SQUARE_1:def 2;
hence E-bound (X\/Y) = E-bound Y by SPRECT_1:57;
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 SQUARE_1:def 1;
hence S-bound (X\/Y) = S-bound X by SPRECT_1:55;
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 SQUARE_1:def 1;
hence W-bound (X\/Y) = W-bound X by SPRECT_1:54;
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: X\/Y is compact by COMPTS_1:19;
assume A2: N-bound X < N-bound Y;
then A3: N-bound (X\/Y) = N-bound Y by Th23;
A4: (N-min(X\/Y))`2 = N-bound (X\/Y) & (N-min Y)`2 = N-bound Y
by PSCOMP_1:94;
A5: Y c= X\/Y by XBOOLE_1:7;
N-min Y in Y by SPRECT_1:13;
then N-min Y in N-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:14;
then A6: (N-min(X\/Y))`1 <= (N-min Y)`1 by A1,PSCOMP_1:98;
A7: N-min(X\/Y) in X\/Y by A1,SPRECT_1:13;
per cases by A7,XBOOLE_0:def 2;
suppose N-min(X\/Y) in Y;
then N-min(X\/Y) in N-most Y by A3,A4,SPRECT_2:14;
then (N-min(X\/Y))`1 >= (N-min Y)`1 by PSCOMP_1:98;
then (N-min(X\/Y))`1 = (N-min Y)`1 by A6,AXIOMS:21;
hence N-min (X\/Y) = N-min Y by A3,A4,TOPREAL3:11;
suppose N-min(X\/Y) in X;
hence N-min (X\/Y) = N-min Y by A2,A3,A4,PSCOMP_1:71;
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: X\/Y is compact by COMPTS_1:19;
assume A2: N-bound X < N-bound Y;
then A3: N-bound (X\/Y) = N-bound Y by Th23;
A4: (N-max(X\/Y))`2 = N-bound (X\/Y) & (N-max Y)`2 = N-bound Y
by PSCOMP_1:94;
A5: Y c= X\/Y by XBOOLE_1:7;
N-max Y in Y by SPRECT_1:13;
then N-max Y in N-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:14;
then A6: (N-max(X\/Y))`1 >= (N-max Y)`1 by A1,PSCOMP_1:98;
A7: N-max(X\/Y) in X\/Y by A1,SPRECT_1:13;
per cases by A7,XBOOLE_0:def 2;
suppose N-max(X\/Y) in Y;
then N-max(X\/Y) in N-most Y by A3,A4,SPRECT_2:14;
then (N-max(X\/Y))`1 <= (N-max Y)`1 by PSCOMP_1:98;
then (N-max(X\/Y))`1 = (N-max Y)`1 by A6,AXIOMS:21;
hence N-max (X\/Y) = N-max Y by A3,A4,TOPREAL3:11;
suppose N-max(X\/Y) in X;
hence N-max (X\/Y) = N-max Y by A2,A3,A4,PSCOMP_1:71;
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: X\/Y is compact by COMPTS_1:19;
assume A2: E-bound X < E-bound Y;
then A3: E-bound (X\/Y) = E-bound Y by Th24;
A4: (E-min(X\/Y))`1 = E-bound (X\/Y) & (E-min Y)`1 = E-bound Y
by PSCOMP_1:104;
A5: Y c= X\/Y by XBOOLE_1:7;
E-min Y in Y by SPRECT_1:16;
then E-min Y in E-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:17;
then A6: (E-min(X\/Y))`2 <= (E-min Y)`2 by A1,PSCOMP_1:108;
A7: E-min(X\/Y) in X\/Y by A1,SPRECT_1:16;
per cases by A7,XBOOLE_0:def 2;
suppose E-min(X\/Y) in Y;
then E-min(X\/Y) in E-most Y by A3,A4,SPRECT_2:17;
then (E-min(X\/Y))`2 >= (E-min Y)`2 by PSCOMP_1:108;
then (E-min(X\/Y))`2 = (E-min Y)`2 by A6,AXIOMS:21;
hence E-min (X\/Y) = E-min Y by A3,A4,TOPREAL3:11;
suppose E-min(X\/Y) in X;
hence E-min (X\/Y) = E-min Y by A2,A3,A4,PSCOMP_1:71;
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: X\/Y is compact by COMPTS_1:19;
assume A2: E-bound X < E-bound Y;
then A3: E-bound (X\/Y) = E-bound Y by Th24;
A4: (E-max(X\/Y))`1 = E-bound (X\/Y) & (E-max Y)`1 = E-bound Y
by PSCOMP_1:104;
A5: Y c= X\/Y by XBOOLE_1:7;
E-max Y in Y by SPRECT_1:16;
then E-max Y in E-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:17;
then A6: (E-max(X\/Y))`2 >= (E-max Y)`2 by A1,PSCOMP_1:108;
A7: E-max(X\/Y) in X\/Y by A1,SPRECT_1:16;
per cases by A7,XBOOLE_0:def 2;
suppose E-max(X\/Y) in Y;
then E-max(X\/Y) in E-most Y by A3,A4,SPRECT_2:17;
then (E-max(X\/Y))`2 <= (E-max Y)`2 by PSCOMP_1:108;
then (E-max(X\/Y))`2 = (E-max Y)`2 by A6,AXIOMS:21;
hence E-max (X\/Y) = E-max Y by A3,A4,TOPREAL3:11;
suppose E-max(X\/Y) in X;
hence E-max (X\/Y) = E-max Y by A2,A3,A4,PSCOMP_1:71;
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: X\/Y is compact by COMPTS_1:19;
assume A2: S-bound X < S-bound Y;
then A3: S-bound (X\/Y) = S-bound X by Th25;
A4: (S-min(X\/Y))`2 = S-bound (X\/Y) & (S-min X)`2 = S-bound X
by PSCOMP_1:114;
A5: X c= X\/Y by XBOOLE_1:7;
S-min X in X by SPRECT_1:14;
then S-min X in S-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:15;
then A6: (S-min(X\/Y))`1 <= (S-min X)`1 by A1,PSCOMP_1:118;
A7: S-min(X\/Y) in X\/Y by A1,SPRECT_1:14;
per cases by A7,XBOOLE_0:def 2;
suppose S-min(X\/Y) in X;
then S-min(X\/Y) in S-most X by A3,A4,SPRECT_2:15;
then (S-min(X\/Y))`1 >= (S-min X)`1 by PSCOMP_1:118;
then (S-min(X\/Y))`1 = (S-min X)`1 by A6,AXIOMS:21;
hence S-min (X\/Y) = S-min X by A3,A4,TOPREAL3:11;
suppose S-min(X\/Y) in Y;
hence S-min (X\/Y) = S-min X by A2,A3,A4,PSCOMP_1:71;
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: X\/Y is compact by COMPTS_1:19;
assume A2: S-bound X < S-bound Y;
then A3: S-bound (X\/Y) = S-bound X by Th25;
A4: (S-max(X\/Y))`2 = S-bound (X\/Y) & (S-max X)`2 = S-bound X
by PSCOMP_1:114;
A5: X c= X\/Y by XBOOLE_1:7;
S-max X in X by SPRECT_1:14;
then S-max X in S-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:15;
then A6: (S-max(X\/Y))`1 >= (S-max X)`1 by A1,PSCOMP_1:118;
A7: S-max(X\/Y) in X\/Y by A1,SPRECT_1:14;
per cases by A7,XBOOLE_0:def 2;
suppose S-max(X\/Y) in X;
then S-max(X\/Y) in S-most X by A3,A4,SPRECT_2:15;
then (S-max(X\/Y))`1 <= (S-max X)`1 by PSCOMP_1:118;
then (S-max(X\/Y))`1 = (S-max X)`1 by A6,AXIOMS:21;
hence S-max (X\/Y) = S-max X by A3,A4,TOPREAL3:11;
suppose S-max(X\/Y) in Y;
hence S-max (X\/Y) = S-max X by A2,A3,A4,PSCOMP_1:71;
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: X\/Y is compact by COMPTS_1:19;
assume A2: W-bound X < W-bound Y;
then A3: W-bound (X\/Y) = W-bound X by Th26;
A4: (W-min(X\/Y))`1 = W-bound (X\/Y) & (W-min X)`1 = W-bound X
by PSCOMP_1:84;
A5: X c= X\/Y by XBOOLE_1:7;
W-min X in X by SPRECT_1:15;
then W-min X in W-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:16;
then A6: (W-min(X\/Y))`2 <= (W-min X)`2 by A1,PSCOMP_1:88;
A7: W-min(X\/Y) in X\/Y by A1,SPRECT_1:15;
per cases by A7,XBOOLE_0:def 2;
suppose W-min(X\/Y) in X;
then W-min(X\/Y) in W-most X by A3,A4,SPRECT_2:16;
then (W-min(X\/Y))`2 >= (W-min X)`2 by PSCOMP_1:88;
then (W-min(X\/Y))`2 = (W-min X)`2 by A6,AXIOMS:21;
hence W-min (X\/Y) = W-min X by A3,A4,TOPREAL3:11;
suppose W-min(X\/Y) in Y;
hence W-min (X\/Y) = W-min X by A2,A3,A4,PSCOMP_1:71;
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: X\/Y is compact by COMPTS_1:19;
assume A2: W-bound X < W-bound Y;
then A3: W-bound (X\/Y) = W-bound X by Th26;
A4: (W-max(X\/Y))`1 = W-bound (X\/Y) & (W-max X)`1 = W-bound X
by PSCOMP_1:84;
A5: X c= X\/Y by XBOOLE_1:7;
W-max X in X by SPRECT_1:15;
then W-max X in W-most(X\/Y) by A1,A3,A4,A5,SPRECT_2:16;
then A6: (W-max(X\/Y))`2 >= (W-max X)`2 by A1,PSCOMP_1:88;
A7: W-max(X\/Y) in X\/Y by A1,SPRECT_1:15;
per cases by A7,XBOOLE_0:def 2;
suppose W-max(X\/Y) in X;
then W-max(X\/Y) in W-most X by A3,A4,SPRECT_2:16;
then (W-max(X\/Y))`2 <= (W-max X)`2 by PSCOMP_1:88;
then (W-max(X\/Y))`2 = (W-max X)`2 by A6,AXIOMS:21;
hence W-max (X\/Y) = W-max X by A3,A4,TOPREAL3:11;
suppose W-max(X\/Y) in Y;
hence W-max (X\/Y) = W-max X by A2,A3,A4,PSCOMP_1:71;
end;
theorem Th35:
for f be non empty FinSequence of TOP-REAL 2
for p be Point of TOP-REAL 2 st f is_S-Seq & p in L~f holds
L_Cut(f,p)/.len L_Cut(f,p) = f/.len f
proof
let f be non empty FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume that
A1: f is_S-Seq and
A2: p in L~f;
A3: len f in dom f by SCMFSA_7:12;
L_Cut(f,p) <> {} by A2,JORDAN1E:7;
then len L_Cut(f,p) in dom L_Cut(f,p) by SCMFSA_7:12;
hence L_Cut(f,p)/.len L_Cut(f,p) = L_Cut(f,p).len L_Cut(f,p)
by FINSEQ_4:def 4
.= f.len f by A1,A2,JORDAN1B:5
.= f/.len f by A3,FINSEQ_4:def 4;
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 & q in LeftComp f and
A2: p in g & q in g;
assume g misses L~f;
then g c= (L~f)` by TDLAT_1:2;
then g c= (L~f)`;
then g c= the carrier of (TOP-REAL 2)|(L~f)` by JORDAN1:1;
then reconsider A = g as Subset of (TOP-REAL 2)|(L~f)`;
A3: A is connected by CONNSP_1:24;
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
A4: R = RightComp f and
A5: R is_a_component_of (TOP-REAL 2)|(L~f)` by CONNSP_1:def 6;
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
A6: L = LeftComp f and
A7: L is_a_component_of (TOP-REAL 2)|(L~f)` by CONNSP_1:def 6;
R /\ A <> {} & L /\ A <> {} by A1,A2,A4,A6,XBOOLE_0:def 3;
then R meets A & L meets A by XBOOLE_0:def 7;
then RightComp f = LeftComp f by A3,A4,A5,A6,A7,JORDAN2C:100;
hence contradiction by SPRECT_4:7;
end;
definition
cluster non constant standard s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2);
existence
proof
consider C be Simple_closed_curve;
consider n be Nat;
A1: len Upper_Seq(C,n) >= 2 by TOPREAL1:def 10;
A2: Upper_Seq(C,n) is_sequence_on Gauge(C,n) by JORDAN1G:4;
take Upper_Seq(C,n);
thus thesis by A1,A2,JGRAPH_1:16,JORDAN8:8;
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;
assume p in rng f;
then consider i be Nat such that
A1: i in dom f and
A2: f.i = p by FINSEQ_2:11;
A3: 0+1 <= i & i <= len f by A1,FINSEQ_3:27;
len f >= 2 by TOPREAL1:def 10;
then A4: len f >= 1 by AXIOMS:22;
per cases by A3,REAL_1:def 5;
suppose i > 1;
then A5: Index(p,f) + 1 = i by A2,A3,JORDAN3:45;
then L_Cut(f,p) = mid(f,Index(p,f)+1,len f) by A2,JORDAN3:def 4;
hence L_Cut(f,p) = mid(f,p..f,len f) by A1,A2,A5,FINSEQ_5:12;
suppose A6: i = 1;
thus L_Cut(f,p) = L_Cut(f,f/.i) by A1,A2,FINSEQ_4:def 4
.= f by A6,JORDAN5B:30
.= mid(f,1,len f) by A4,JORDAN3:29
.= mid(f,p..f,len f) by A1,A2,A6,FINSEQ_5:12;
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:57;
hence R_Cut(f,p) is_sequence_on M by A1,JORDAN1H:33;
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 L_Cut(f,p) is_sequence_on M by A1,JORDAN1H:33;
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 A2: 1 <= i & i <= len G & 1 <= j & j <= width G;
assume G*(i,j) in L~f;
then consider k be Nat such that
A3: 1 <= k and
A4: k+1 <= len f and
A5: G*(i,j) in LSeg(f/.k,f/.(k+1)) by SPPOL_2:14;
consider i1,j1,i2,j2 be Nat such that
A6: [i1,j1] in Indices G and
A7: f/.k = G*(i1,j1) and
A8: [i2,j2] in Indices G and
A9: f/.(k+1) = G*(i2,j2) and
A10: 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,A3,A4,JORDAN8:6;
A11: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A6,GOBOARD5:1;
A12: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A8,GOBOARD5:1;
k+1 >= 1 & k < len f by A4,NAT_1:29,38;
then A13: k in dom f & k+1 in dom f by A3,A4,FINSEQ_3:27;
per cases by A10;
suppose A14: i1 = i2 & j1+1 = j2;
j1 <= j1+1 by NAT_1:29;
then G*(i1,j1)`1 <= G*(i1,j1+1)`1 & G*(i1,j1)`2 <= G*(i1,j1+1)`2
by A11,A12,A14,JORDAN1A:39,40;
then G*(i1,j1)`1 <= G*(i,j)`1 & G*(i,j)`1 <= G*(i1,j1+1)`1 &
G*(i1,j1)`2 <= G*(i,j)`2 & G*(i,j)`2 <= G*(i1,j1+1)`2
by A5,A7,A9,A14,TOPREAL1:9,10;
then i1 <= i & i <= i1 & j1 <= j & j <= j1+1
by A2,A11,A12,A14,Th1,Th2;
then i = i1 & (j = j1 or j = j1+1) by AXIOMS:21,NAT_1:27;
hence G*(i,j) in rng f by A7,A9,A13,A14,PARTFUN2:4;
suppose A15: i1+1 = i2 & j1 = j2;
i1 <= i1+1 by NAT_1:29;
then G*(i1,j1)`1 <= G*(i1+1,j1)`1 & G*(i1,j1)`2 <= G*(i1+1,j1)`2
by A11,A12,A15,JORDAN1A:39,40;
then G*(i1,j1)`1 <= G*(i,j)`1 & G*(i,j)`1 <= G*(i1+1,j1)`1 &
G*(i1,j1)`2 <= G*(i,j)`2 & G*(i,j)`2 <= G*(i1+1,j1)`2
by A5,A7,A9,A15,TOPREAL1:9,10;
then j1 <= j & j <= j1 & i1 <= i & i <= i1+1
by A2,A11,A12,A15,Th1,Th2;
then j = j1 & (i = i1 or i = i1+1) by AXIOMS:21,NAT_1:27;
hence G*(i,j) in rng f by A7,A9,A13,A15,PARTFUN2:4;
suppose A16: i1 = i2+1 & j1 = j2;
i2 <= i2+1 by NAT_1:29;
then G*(i2,j1)`1 <= G*(i2+1,j1)`1 & G*(i2,j1)`2 <= G*(i2+1,j1)`2
by A11,A12,A16,JORDAN1A:39,40;
then G*(i2,j1)`1 <= G*(i,j)`1 & G*(i,j)`1 <= G*(i2+1,j1)`1 &
G*(i2,j1)`2 <= G*(i,j)`2 & G*(i,j)`2 <= G*(i2+1,j1)`2
by A5,A7,A9,A16,TOPREAL1:9,10;
then j1 <= j & j <= j1 & i2 <= i & i <= i2+1
by A2,A11,A12,A16,Th1,Th2;
then j = j1 & (i = i2 or i = i2+1) by AXIOMS:21,NAT_1:27;
hence G*(i,j) in rng f by A7,A9,A13,A16,PARTFUN2:4;
suppose A17: i1 = i2 & j1 = j2+1;
j2 <= j2+1 by NAT_1:29;
then G*(i1,j2)`1 <= G*(i1,j2+1)`1 & G*(i1,j2)`2 <= G*(i1,j2+1)`2
by A11,A12,A17,JORDAN1A:39,40;
then G*(i1,j2)`1 <= G*(i,j)`1 & G*(i,j)`1 <= G*(i1,j2+1)`1 &
G*(i1,j2)`2 <= G*(i,j)`2 & G*(i,j)`2 <= G*(i1,j2+1)`2
by A5,A7,A9,A17,TOPREAL1:9,10;
then i1 <= i & i <= i1 & j2 <= j & j <= j2+1
by A2,A11,A12,A17,Th1,Th2;
then i = i1 & (j = j2 or j = j2+1) by AXIOMS:21,NAT_1:27;
hence G*(i,j) in rng f by A7,A9,A13,A17,PARTFUN2:4;
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) = {};
A6: now let i be Nat;
assume 1 <= i & i+2 <= len f;
then LSeg(f,i) /\ LSeg(f/.len f,g/.1) = {} by A4;
hence LSeg(f,i) misses LSeg(f/.len f,g/.1) by XBOOLE_0:def 7;
end;
A7: now let i be Nat;
assume 2 <= i & i+1 <= len g;
then LSeg(g,i) /\ LSeg(f/.len f,g/.1) = {} by A5;
hence LSeg(g,i) misses LSeg(f/.len f,g/.1) by XBOOLE_0:def 7;
end;
let i,j be Nat such that
A8: i+1 < j and
A9: i > 1 & j < len (f^g) or j+1 < len (f^g);
A10: j+1 <= len (f^g) by A9,NAT_1:38;
per cases;
suppose i = 0;
then LSeg(f^g,i) = {} by TOPREAL1:def 5;
then LSeg(f^g,i) /\ LSeg(f^g,j) = {};
hence thesis by XBOOLE_0:def 7;
suppose A11: i <> 0;
A12: len(f^g) = len f + len g by FINSEQ_1:35;
A13: 1 <= i by A11,RLVECT_1:99;
i <= i+1 by NAT_1:29;
then A14: i < j by A8,AXIOMS:22;
now per cases;
suppose A15: j+1 <= len f;
j <= j+1 by NAT_1:29;
then i < j+1 by A14,AXIOMS:22;
then i < len f by A15,AXIOMS:22;
then i+1 <= len f by NAT_1:38;
then A16: LSeg(f^g,i) = LSeg(f,i) by SPPOL_2:6;
LSeg(f^g,j) = LSeg(f,j) by A15,SPPOL_2:6;
hence thesis by A8,A16,TOPREAL1:def 9;
suppose j+1 > len f;
then A17: len f <= j by NAT_1:38;
then reconsider j' = j - len f as Nat by INT_1:18;
A18: len f + j' = j by XCMPLX_1:27;
j+1-len f <= len g by A10,A12,REAL_1:86;
then A19: j'+1 <= len g by XCMPLX_1:29;
now per cases;
suppose A20: i <= len f;
now per cases;
suppose A21: i = len f;
then len f +1+1 <= j by A8,NAT_1:38;
then len f +(1+1) <= j by XCMPLX_1:1;
then A22: 1+1 <= j' by REAL_1:84;
then A23: 1 <= j' by AXIOMS:22;
then A24: LSeg(f^g,j) = LSeg(g,j') by A18,SPPOL_2:7;
g is non empty by A19,A23,GOBOARD2:3,RELAT_1:60;
then LSeg(f^g,i) = LSeg(f/.len f,g/.1) by A21,SPPOL_2:8;
hence thesis by A7,A19,A22,A24;
suppose i <> len f;
then i < len f by A20,REAL_1:def 5;
then i+1 <= len f by NAT_1:38;
then A25: LSeg(f^g,i) = LSeg(f,i) by SPPOL_2:6;
now per cases;
suppose A26: j = len f;
then i+1+1 <= len f by A8,NAT_1:38;
then A27: i+(1+1) <= len f by XCMPLX_1:1;
1 <= len g by A10,A12,A26,REAL_1:53;
then g is non empty by FINSEQ_3:27,RELAT_1:60;
then LSeg(f^g,j) = LSeg(f/.len f,g/.1) by A26,SPPOL_2:8;
hence thesis by A6,A13,A25,A27;
suppose j <> len f;
then len f < j by A17,REAL_1:def 5;
then len f+1 <= j by NAT_1:38;
then A28: 1 <= j' by REAL_1:84;
then A29: LSeg(f^g,len f+j') = LSeg(g,j') by SPPOL_2:7;
then A30: LSeg(f^g,j) c= L~g by A18,TOPREAL3:26;
LSeg(f^g,i) c= L~f by A25,TOPREAL3:26;
then A31: LSeg(f^g,i) /\ LSeg(f^g,j) c= {f/.1} by A2,A30,XBOOLE_1:
27;
A32: len f >= 2 by TOPREAL1:def 10;
now per cases by A31,ZFMISC_1:39;
suppose LSeg(f^g,i) /\ LSeg(f^g,j) = {};
hence thesis by XBOOLE_0:def 7;
suppose LSeg(f^g,i) /\ LSeg(f^g,j) = {f/.1};
then f/.1 in LSeg(f^g,i) /\ LSeg(f^g,j) by TARSKI:def 1;
then A33: f/.1 in LSeg(f^g,i) & f/.1 in LSeg(f^g,j)
by XBOOLE_0:def 3;
j'+1 >= 1 & j' < len g by A19,NAT_1:29,38;
then j' in dom g & j'+1 in dom g by A19,A28,FINSEQ_3:27;
then j'+1=len g by A1,A3,A18,A29,A33,GOBOARD2:7;
hence thesis by A9,A12,A18,A25,A32,A33,JORDAN5B:33,XCMPLX_1:1;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
suppose A34: i > len f;
then reconsider i' = i - len f as Nat by INT_1:18;
A35: len f + i' = i by XCMPLX_1:27;
len f + 1 <= i by A34,NAT_1:38;
then 1 <= i' by REAL_1:84;
then A36: LSeg(f^g,len f+i') = LSeg(g,i') by SPPOL_2:7;
i+1-len f < j' by A8,REAL_1:54;
then A37: i'+1 < j' by XCMPLX_1:29;
j <> len f by A8,A34,NAT_1:38;
then len f < j by A17,REAL_1:def 5;
then len f+1 <= j by NAT_1:38;
then 1 <= j' by REAL_1:84;
then LSeg(f^g,len f+j') = LSeg(g,j') by SPPOL_2:7;
hence thesis by A1,A18,A35,A36,A37,TOPREAL1:def 9;
end;
hence thesis;
end;
hence thesis;
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);
A1: len G = width G by JORDAN8:def 1;
defpred P[Nat] means 1 <= $1 & $1 < len G & G*(2,$1)`2 < (W-min C)`2;
A2: for k be Nat st P[k] holds k <= len G;
A3: len G = 2|^n+3 & len G = width G by JORDAN8:def 1;
A4: len G >= 4 by JORDAN8:13;
then A5: 1 < len G by AXIOMS:22;
(SW-corner C)`2 <= (W-min C)`2 by PSCOMP_1:87;
then A6: S-bound C <= (W-min C)`2 by PSCOMP_1:73;
A7: 2 <= len G by A4,AXIOMS:22;
then G*(2,2)`2 = S-bound C by JORDAN8:16;
then G*(2,1)`2 < S-bound C by A3,A7,GOBOARD5:5;
then G*(2,1)`2 < (W-min C)`2 by A6,AXIOMS:22;
then A8: ex k be Nat st P[k] by A5;
ex i being Nat st P[i] & for n st P[n] holds n <= i from Max(A2,A8);
then consider i being Nat such that
A9: 1 <= i & i < len G and
A10: G*(2,i)`2 < (W-min C)`2 and
A11: for n st P[n] holds n <= i;
take i;
thus 1 <= i & i+1 <= len G by A9,NAT_1:38;
A12: LSeg(G*(1+1,i),G*(1+1,i+1)) c= cell(G,1,i) by A1,A5,A9,GOBOARD5:19;
A13: i+1 <= len G by A9,NAT_1:38;
A14: 1 <= i+1 by NAT_1:37;
(W-min C)`1 = W-bound C by PSCOMP_1:84;
then A15: G*(2,i)`1 = (W-min C)`1 & (W-min C)`1 = G*(2,i+1)`1
by A9,A13,A14,JORDAN8:14;
now assume i+1 = len G;
then len G-'1 = i by BINARITH:39;
then A16: G*(2,i)`2 = N-bound C by A7,JORDAN8:17;
(NW-corner C)`2 >= (W-min C)`2 by PSCOMP_1:87;
hence contradiction by A10,A16,PSCOMP_1:75;
end;
then i+1 < len G & i < i+1 by A13,NAT_1:38,REAL_1:def 5;
then (W-min C)`2 <= G*(2,i+1)`2 by A11,A14;
then W-min C in LSeg(G*(2,i),G*(2,i+1)) by A10,A15,GOBOARD7:8;
hence W-min C in cell(G,1,i) by A12;
thus W-min C <> G*(2,i) 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:65;
A5: Rev f is_S-Seq by SPPOL_2:47;
L_Cut(Rev f,p) = Rev R_Cut(f,p) by A1,JORDAN3:57;
then (Rev f).1 in L~L_Cut(Rev f,p) by A2,A4,SPPOL_2:22;
hence f.len f = p by A1,A3,A4,A5,JORDAN1E:11;
end;
theorem Th44:
for f be non empty FinSequence of TOP-REAL 2
for p be Point of TOP-REAL 2 holds
R_Cut (f,p) <> {}
proof
let f be non empty 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 5; hence
thesis;
suppose p=f.1; then R_Cut (f,p) = <*p*> by JORDAN3:def 5;
hence thesis;
end;
theorem Th45:
for f be S-Sequence_in_R2
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 S-Sequence_in_R2;
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 FINSEQ_4:def 4
.= p by A1,JORDAN3:59;
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: 1 in dom US & 1 in dom LS by FINSEQ_5:6;
US/.1 = Wmin by JORDAN1F:5;
then A5: US.1 = Wmin by A4,FINSEQ_4:def 4;
LS/.1 = Emax by JORDAN1F:6;
then A6: LS.1 = Emax by A4,FINSEQ_4:def 4;
Wbo <> Ebo by SPRECT_1:33;
then p <> US.1 by A2,A5,PSCOMP_1:84;
then reconsider g = R_Cut(US,p) as being_S-Seq FinSequence of TOP-REAL 2
by A1,JORDAN3:70;
A7: US is_in_the_area_of Ca by JORDAN1E:21;
then <*p*> is_in_the_area_of Ca by A1,SPRECT_3:63;
then A8: g is_in_the_area_of Ca by A1,A7,SPRECT_3:69;
A9: (g/.1)`1 = (US/.1)`1 by A1,SPRECT_3:39
.= Wmin`1 by JORDAN1F:5
.= Wbo by PSCOMP_1:84;
len g in dom g by FINSEQ_5:6;
then g/.len g = g.len g by FINSEQ_4:def 4
.= p by A1,JORDAN3:59;
then A10: g is_a_h.c._for Ca by A2,A8,A9,SPRECT_2:def 2;
len Cage(C,n) > 4 by GOBOARD7:36;
then len Cage(C,n) >= 2 by AXIOMS:22;
then A11: rng Cage(C,n) c= L~Cage(C,n) by SPPOL_2:18;
now per cases;
suppose A12: Emax <> NE;
set h = Rev R_Cut(LS,Smax)^<*NE*>;
A13: not NE in rng Cage(C,n)
proof
assume A14: NE in rng Cage(C,n);
A15: NE`1 = E-bound L~Cage(C,n) & NE`2 = N-bound L~Cage(C,n)
by PSCOMP_1:76,77;
then NE`2 >= S-bound L~Cage(C,n) by SPRECT_1:24;
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 A15;
then NE in LSeg(SE-corner L~Cage(C,n), NE-corner L~Cage(C,n))
by SPRECT_1:25;
then NE in LSeg(SE-corner L~Cage(C,n), NE-corner L~Cage(C,n)) /\
L~Cage(C,n) by A11,A14,XBOOLE_0:def 3;
then NE in E-most L~Cage(C,n) by PSCOMP_1:def 40;
then A16: NE`2 <= (E-max L~Cage(C,n))`2 by PSCOMP_1:108;
(E-max L~Cage(C,n))`2 <= NE`2 by PSCOMP_1:107;
then A17: (E-max L~Cage(C,n))`2 = NE`2 by A16,AXIOMS:21;
(E-max L~Cage(C,n))`1 = NE`1 by PSCOMP_1:105;
hence contradiction by A12,A17,TOPREAL3:11;
end;
Smax in rng LS by Th12;
then R_Cut(LS,Smax) = mid(LS,1,Smax..LS) by JORDAN1G:57;
then A18: rng R_Cut(LS,Smax) c= rng LS by JORDAN3:28;
rng LS c= rng Ca by JORDAN1G:47;
then rng R_Cut(LS,Smax) c= rng Ca by A18,XBOOLE_1:1;
then not NE in rng R_Cut(LS,Smax) by A13;
then rng R_Cut(LS,Smax) misses {NE} by ZFMISC_1:56;
then rng R_Cut(LS,Smax) misses rng <*NE*> by FINSEQ_1:55;
then A19: rng Rev R_Cut(LS,Smax) misses rng <*NE*> by FINSEQ_5:60;
A20: Smax in L~LS by Th12;
A21: Emin`2 < Emax`2 by SPRECT_2:57;
Emin in L~Ca by SPRECT_1:16;
then Sbo <= Emin`2 by PSCOMP_1:71;
then A22: Smax <> LS.1 by A6,A21,PSCOMP_1:114;
then reconsider RCutLS = R_Cut(LS,Smax) as
being_S-Seq FinSequence of TOP-REAL 2 by A20,JORDAN3:70;
A23: <*NE*> is one-to-one by FINSEQ_3:102;
A24: Rev RCutLS is special by SPPOL_2:42;
A25: <*NE*> is special by SPPOL_2:39;
A26: Rev RCutLS/.len Rev RCutLS = Rev RCutLS/.len RCutLS
by FINSEQ_5:def 3
.= RCutLS/.1 by FINSEQ_5:68
.= LS/.1 by A20,SPRECT_3:39
.= Emax by JORDAN1F:6;
then (Rev RCutLS/.len Rev RCutLS)`1 = E-bound L~Ca by PSCOMP_1:104
.= NE`1 by PSCOMP_1:76
.= (<*NE*>/.1)`1 by FINSEQ_4:25;
then A27: h is one-to-one special by A19,A23,A24,A25,FINSEQ_3:98,GOBOARD2
:13;
A28: 2 <= len g by TOPREAL1:def 10;
A29: len h = len Rev R_Cut(LS,Smax) + 1 by FINSEQ_2:19
.= len R_Cut(LS,Smax) + 1 by FINSEQ_5:def 3
.= Index(Smax,LS)+1+1 by A20,A22,JORDAN3:60;
Index(Smax,LS) >= 0 by NAT_1:18;
then Index(Smax,LS)+1 >= 0+1 by REAL_1:55;
then A30: len h >= 1+1 by A29,REAL_1:55;
A31: LS is_in_the_area_of Ca by JORDAN1E:22;
then <*Smax*> is_in_the_area_of Ca by A20,SPRECT_3:63;
then R_Cut(LS,Smax) is_in_the_area_of Ca by A20,A31,SPRECT_3:69;
then A32: Rev R_Cut(LS,Smax) is_in_the_area_of Ca by SPRECT_3:68;
<*NE*> is_in_the_area_of Ca by SPRECT_2:29;
then A33: h is_in_the_area_of Ca by A32,SPRECT_2:28;
1 in dom Rev RCutLS by FINSEQ_5:6;
then h/.1 = Rev RCutLS/.1 by GROUP_5:95
.= R_Cut(LS,Smax)/.len R_Cut(LS,Smax) by FINSEQ_5:68
.= Smax by A20,Th45;
then A34: (h/.1)`2 = Sbo by PSCOMP_1:114;
(h/.len h)`2 = (h/.(len Rev R_Cut(LS,Smax)+1))`2 by FINSEQ_2:19
.= NE`2 by TOPREAL4:1
.= Nbo by PSCOMP_1:77;
then h is_a_v.c._for Ca by A33,A34,SPRECT_2:def 3;
then L~g meets L~h by A10,A27,A28,A30,SPRECT_2:33;
then consider x be set such that
A35: x in L~g and
A36: x in L~h by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A35;
A37: L~g c= L~US by A1,JORDAN3:76;
then A38: x in L~US by A35;
A39: L~h = L~Rev RCutLS \/ LSeg(Rev RCutLS/.len Rev RCutLS,NE)
by SPPOL_2:19;
A40: L~RCutLS c= L~LS by A20,JORDAN3:76;
A41: len US in dom US & len LS in dom LS by FINSEQ_5:6;
now per cases by A36,A39,XBOOLE_0:def 2;
suppose x in L~Rev RCutLS;
then A42: x in L~RCutLS by SPPOL_2:22;
then x in L~US /\ L~LS by A35,A37,A40,XBOOLE_0:def 3;
then A43: x in {Wmin,Emax} by JORDAN1E:20;
now per cases by A43,TARSKI:def 2;
suppose x = Wmin;
then LS/.len LS in L~R_Cut(LS,Smax) by A42,JORDAN1F:8;
then LS.len LS in L~R_Cut(LS,Smax) by A41,FINSEQ_4:def 4;
then LS.len LS = Smax by A20,Th43;
then LS/.len LS = Smax by A41,FINSEQ_4:def 4;
then A44: Wmin = Smax by JORDAN1F:8;
A45: Smin`1 < Smax`1 by SPRECT_2:59;
Smin in L~Ca by SPRECT_1:14;
then Wbo <= Smin`1 by PSCOMP_1:71;
hence contradiction by A44,A45,PSCOMP_1:84;
suppose x = Emax;
then US/.len US in L~R_Cut(US,p) by A35,JORDAN1F:7;
then US.len US in L~R_Cut(US,p) by A41,FINSEQ_4:def 4;
then US.len US = p by A1,Th43;
then US/.len US = p by A41,FINSEQ_4:def 4;
hence contradiction by A3,JORDAN1F:7;
end;
hence contradiction;
suppose A46: x in LSeg(Rev RCutLS/.len Rev RCutLS,NE);
A47: Emax`1 = Ebo by PSCOMP_1:104;
NE`1 = Ebo by PSCOMP_1:76;
then A48: x`1 = Ebo by A26,A46,A47,GOBOARD7:5;
Emax`2 <= NE`2 by PSCOMP_1:107;
then A49: Emax`2 <= x`2 by A26,A46,TOPREAL1:10;
L~Ca = L~US \/ L~LS by JORDAN1E:17;
then L~US c= L~Ca by XBOOLE_1:7;
then x in E-most L~Ca by A38,A48,SPRECT_2:17;
then x`2 <= Emax`2 by PSCOMP_1:108;
then x`2 = Emax`2 by A49,AXIOMS:21;
then x = Emax by A47,A48,TOPREAL3:11;
then US/.len US in L~R_Cut(US,p) by A35,JORDAN1F:7;
then US.len US in L~R_Cut(US,p) by A41,FINSEQ_4:def 4;
then US.len US = p by A1,Th43;
then US/.len US = p by A41,FINSEQ_4:def 4;
hence contradiction by A3,JORDAN1F:7;
end;
hence contradiction;
suppose A50: Emax = NE;
set h = Rev R_Cut(LS,Smax);
A51: Smax in L~LS by Th12;
A52: Emin`2 < Emax`2 by SPRECT_2:57;
Emin in L~Ca by SPRECT_1:16;
then Sbo <= Emin`2 by PSCOMP_1:71;
then Smax <> LS.1 by A6,A52,PSCOMP_1:114;
then reconsider RCutLS = R_Cut(LS,Smax) as
being_S-Seq FinSequence of TOP-REAL 2 by A51,JORDAN3:70;
A53: Rev RCutLS is special by SPPOL_2:42;
A54: Rev RCutLS/.len Rev RCutLS = Rev RCutLS/.len RCutLS
by FINSEQ_5:def 3
.= RCutLS/.1 by FINSEQ_5:68
.= LS/.1 by A51,SPRECT_3:39
.= Emax by JORDAN1F:6;
A55: 2 <= len g by TOPREAL1:def 10;
len RCutLS >= 2 by TOPREAL1:def 10;
then A56: len h >= 2 by FINSEQ_5:def 3;
A57: LS is_in_the_area_of Ca by JORDAN1E:22;
then <*Smax*> is_in_the_area_of Ca by A51,SPRECT_3:63;
then R_Cut(LS,Smax) is_in_the_area_of Ca by A51,A57,SPRECT_3:69;
then A58: h is_in_the_area_of Ca by SPRECT_3:68;
1 in dom Rev RCutLS by FINSEQ_5:6;
then h/.1 = R_Cut(LS,Smax)/.len R_Cut(LS,Smax) by FINSEQ_5:68
.= Smax by A51,Th45;
then A59: (h/.1)`2 = Sbo by PSCOMP_1:114;
(h/.len h)`2 = Nbo by A50,A54,PSCOMP_1:77;
then h is_a_v.c._for Ca by A58,A59,SPRECT_2:def 3;
then L~g meets L~h by A10,A53,A55,A56,SPRECT_2:33;
then consider x be set such that
A60: x in L~g and
A61: x in L~h by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A60;
A62: L~g c= L~US by A1,JORDAN3:76;
A63: L~RCutLS c= L~LS by A51,JORDAN3:76;
A64: len US in dom US & len LS in dom LS by FINSEQ_5:6;
A65: x in L~RCutLS by A61,SPPOL_2:22;
then x in L~US /\ L~LS by A60,A62,A63,XBOOLE_0:def 3;
then A66: x in {Wmin,Emax} by JORDAN1E:20;
now per cases by A66,TARSKI:def 2;
suppose x = Wmin;
then LS/.len LS in L~R_Cut(LS,Smax) by A65,JORDAN1F:8;
then LS.len LS in L~R_Cut(LS,Smax) by A64,FINSEQ_4:def 4;
then LS.len LS = Smax by A51,Th43;
then LS/.len LS = Smax by A64,FINSEQ_4:def 4;
then A67: Wmin = Smax by JORDAN1F:8;
A68: Smin`1 < Smax`1 by SPRECT_2:59;
Smin in L~Ca by SPRECT_1:14;
then Wbo <= Smin`1 by PSCOMP_1:71;
hence contradiction by A67,A68,PSCOMP_1:84;
suppose x = Emax;
then US/.len US in L~R_Cut(US,p) by A60,JORDAN1F:7;
then US.len US in L~R_Cut(US,p) by A64,FINSEQ_4:def 4;
then US.len US = p by A1,Th43;
then US/.len US = p by A64,FINSEQ_4:def 4;
hence contradiction by A3,JORDAN1F:7;
end;
hence contradiction;
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: 1 in dom LS & 1 in dom US by FINSEQ_5:6;
LS/.1 = Emax by JORDAN1F:6;
then A5: LS.1 = Emax by A4,FINSEQ_4:def 4;
US/.1 = Wmin by JORDAN1F:5;
then A6: US.1 = Wmin by A4,FINSEQ_4:def 4;
Ebo <> Wbo by SPRECT_1:33;
then p <> LS.1 by A2,A5,PSCOMP_1:104;
then reconsider g1 = R_Cut(LS,p) as being_S-Seq FinSequence of TOP-REAL 2
by A1,JORDAN3:70;
reconsider g = Rev g1 as being_S-Seq FinSequence of TOP-REAL 2
by SPPOL_2:47;
A7: L~g = L~g1 by SPPOL_2:22;
A8: LS is_in_the_area_of Ca by JORDAN1E:22;
then <*p*> is_in_the_area_of Ca by A1,SPRECT_3:63;
then g1 is_in_the_area_of Ca by A1,A8,SPRECT_3:69;
then A9: g is_in_the_area_of Ca by SPRECT_3:68;
A10: g/.1 = g1/.len g1 by FINSEQ_5:68;
A11: g/.len g = g/.len g1 by FINSEQ_5:def 3
.= g1/.1 by FINSEQ_5:68;
A12: (g1/.1)`1 = (LS/.1)`1 by A1,SPRECT_3:39
.= Emax`1 by JORDAN1F:6
.= Ebo by PSCOMP_1:104;
len g1 in dom g1 by FINSEQ_5:6;
then g1/.len g1 = g1.len g1 by FINSEQ_4:def 4
.= p by A1,JORDAN3:59;
then A13: g is_a_h.c._for Ca by A2,A9,A10,A11,A12,SPRECT_2:def 2;
len Cage(C,n) > 4 by GOBOARD7:36;
then len Cage(C,n) >= 2 by AXIOMS:22;
then A14: rng Cage(C,n) c= L~Cage(C,n) by SPPOL_2:18;
now per cases;
suppose A15: Wmin <> SW;
set h1 = Rev R_Cut(US,Nmin)^<*SW*>;
A16: not SW in rng Cage(C,n)
proof
assume A17: SW in rng Cage(C,n);
A18: SW`1 = W-bound L~Cage(C,n) & SW`2 = S-bound L~Cage(C,n)
by PSCOMP_1:72,73;
then SW`2 <= N-bound L~Cage(C,n) by SPRECT_1:24;
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 A18;
then SW in LSeg(SW-corner L~Cage(C,n), NW-corner L~Cage(C,n))
by SPRECT_1:28;
then SW in LSeg(SW-corner L~Cage(C,n), NW-corner L~Cage(C,n)) /\
L~Cage(C,n) by A14,A17,XBOOLE_0:def 3;
then SW in W-most L~Cage(C,n) by PSCOMP_1:def 38;
then A19: SW`2 >= (W-min L~Cage(C,n))`2 by PSCOMP_1:88;
(W-min L~Cage(C,n))`2 >= SW`2 by PSCOMP_1:87;
then A20: (W-min L~Cage(C,n))`2 = SW`2 by A19,AXIOMS:21;
(W-min L~Cage(C,n))`1 = SW`1 by PSCOMP_1:85;
hence contradiction by A15,A20,TOPREAL3:11;
end;
Nmin in rng US by Th7;
then R_Cut(US,Nmin) = mid(US,1,Nmin..US) by JORDAN1G:57;
then A21: rng R_Cut(US,Nmin) c= rng US by JORDAN3:28;
rng US c= rng Ca by JORDAN1G:47;
then rng R_Cut(US,Nmin) c= rng Ca by A21,XBOOLE_1:1;
then not SW in rng R_Cut(US,Nmin) by A16;
then rng R_Cut(US,Nmin) misses {SW} by ZFMISC_1:56;
then rng R_Cut(US,Nmin) misses rng <*SW*> by FINSEQ_1:55;
then A22: rng Rev R_Cut(US,Nmin) misses rng <*SW*> by FINSEQ_5:60;
A23: Nmin in L~US by Th7;
A24: Wmax`2 > Wmin`2 by SPRECT_2:61;
Wmax in L~Ca by SPRECT_1:15;
then Nbo >= Wmax`2 by PSCOMP_1:71;
then A25: Nmin <> US.1 by A6,A24,PSCOMP_1:94;
then reconsider RCutUS = R_Cut(US,Nmin) as
being_S-Seq FinSequence of TOP-REAL 2 by A23,JORDAN3:70;
A26: <*SW*> is one-to-one by FINSEQ_3:102;
A27: Rev RCutUS is special by SPPOL_2:42;
A28: <*SW*> is special by SPPOL_2:39;
A29: Rev RCutUS/.len Rev RCutUS = Rev RCutUS/.len RCutUS
by FINSEQ_5:def 3
.= RCutUS/.1 by FINSEQ_5:68
.= US/.1 by A23,SPRECT_3:39
.= Wmin by JORDAN1F:5;
then (Rev RCutUS/.len Rev RCutUS)`1 = W-bound L~Ca by PSCOMP_1:84
.= SW`1 by PSCOMP_1:72
.= (<*SW*>/.1)`1 by FINSEQ_4:25;
then reconsider h1 as one-to-one special FinSequence of TOP-REAL 2
by A22,A26,A27,A28,FINSEQ_3:
98,GOBOARD2:13;
set h = Rev h1;
A30: h is special by SPPOL_2:42;
A31: 2 <= len g by TOPREAL1:def 10;
A32: len h1 = len Rev R_Cut(US,Nmin) + 1 by FINSEQ_2:19
.= len R_Cut(US,Nmin) + 1 by FINSEQ_5:def 3
.= Index(Nmin,US)+1+1 by A23,A25,JORDAN3:60;
Index(Nmin,US) >= 0 by NAT_1:18;
then Index(Nmin,US)+1 >= 0+1 by REAL_1:55;
then len h1 >= 1+1 by A32,REAL_1:55;
then A33: len h >= 2 by FINSEQ_5:def 3;
A34: US is_in_the_area_of Ca by JORDAN1E:21;
then <*Nmin*> is_in_the_area_of Ca by A23,SPRECT_3:63;
then R_Cut(US,Nmin) is_in_the_area_of Ca by A23,A34,SPRECT_3:69;
then A35: Rev R_Cut(US,Nmin) is_in_the_area_of Ca by SPRECT_3:68;
<*SW*> is_in_the_area_of Ca by SPRECT_2:32;
then h1 is_in_the_area_of Ca by A35,SPRECT_2:28;
then A36: h is_in_the_area_of Ca by SPRECT_3:68;
1 in dom Rev RCutUS by FINSEQ_5:6;
then h1/.1 = Rev RCutUS/.1 by GROUP_5:95
.= R_Cut(US,Nmin)/.len R_Cut(US,Nmin) by FINSEQ_5:68
.= Nmin by A23,Th45;
then A37: (h1/.1)`2 = Nbo by PSCOMP_1:94;
A38: h/.len h = h/.len h1 by FINSEQ_5:def 3
.= h1/.1 by FINSEQ_5:68;
A39: h/.1 = h1/.len h1 by FINSEQ_5:68;
(h1/.len h1)`2 = (h1/.(len Rev R_Cut(US,Nmin)+1))`2 by FINSEQ_2:19
.= SW`2 by TOPREAL4:1
.= Sbo by PSCOMP_1:73;
then h is_a_v.c._for Ca by A36,A37,A38,A39,SPRECT_2:def 3;
then L~g meets L~h by A13,A30,A31,A33,SPRECT_2:33;
then consider x be set such that
A40: x in L~g and
A41: x in L~h by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A40;
A42: L~g c= L~LS by A1,A7,JORDAN3:76;
then A43: x in L~LS by A40;
L~h = L~h1 by SPPOL_2:22;
then A44: L~h = L~Rev RCutUS \/ LSeg(Rev RCutUS/.len Rev RCutUS,SW)
by SPPOL_2:19;
A45: L~RCutUS c= L~US by A23,JORDAN3:76;
A46: len LS in dom LS & len US in dom US by FINSEQ_5:6;
now per cases by A41,A44,XBOOLE_0:def 2;
suppose x in L~Rev RCutUS;
then A47: x in L~RCutUS by SPPOL_2:22;
then x in L~LS /\ L~US by A40,A42,A45,XBOOLE_0:def 3;
then A48: x in {Emax,Wmin} by JORDAN1E:20;
now per cases by A48,TARSKI:def 2;
suppose x = Emax;
then US/.len US in L~R_Cut(US,Nmin) by A47,JORDAN1F:7;
then US.len US in L~R_Cut(US,Nmin) by A46,FINSEQ_4:def 4;
then US.len US = Nmin by A23,Th43;
then US/.len US = Nmin by A46,FINSEQ_4:def 4;
then A49: Emax = Nmin by JORDAN1F:7;
A50: Nmax`1 > Nmin`1 by SPRECT_2:55;
Nmax in L~Ca by SPRECT_1:13;
then Ebo >= Nmax`1 by PSCOMP_1:71;
hence contradiction by A49,A50,PSCOMP_1:104;
suppose x = Wmin;
then LS/.len LS in L~R_Cut(LS,p) by A7,A40,JORDAN1F:8;
then LS.len LS in L~R_Cut(LS,p) by A46,FINSEQ_4:def 4;
then LS.len LS = p by A1,Th43;
then LS/.len LS = p by A46,FINSEQ_4:def 4;
hence contradiction by A3,JORDAN1F:8;
end;
hence contradiction;
suppose A51: x in LSeg(Rev RCutUS/.len Rev RCutUS,SW);
A52: Wmin`1 = Wbo by PSCOMP_1:84;
SW`1 = Wbo by PSCOMP_1:72;
then A53: x`1 = Wbo by A29,A51,A52,GOBOARD7:5;
Wmin`2 >= SW`2 by PSCOMP_1:87;
then A54: Wmin`2 >= x`2 by A29,A51,TOPREAL1:10;
L~Ca = L~LS \/ L~US by JORDAN1E:17;
then L~LS c= L~Ca by XBOOLE_1:7;
then x in W-most L~Ca by A43,A53,SPRECT_2:16;
then x`2 >= Wmin`2 by PSCOMP_1:88;
then x`2 = Wmin`2 by A54,AXIOMS:21;
then x = Wmin by A52,A53,TOPREAL3:11;
then LS/.len LS in L~R_Cut(LS,p) by A7,A40,JORDAN1F:8;
then LS.len LS in L~R_Cut(LS,p) by A46,FINSEQ_4:def 4;
then LS.len LS = p by A1,Th43;
then LS/.len LS = p by A46,FINSEQ_4:def 4;
hence contradiction by A3,JORDAN1F:8;
end;
hence contradiction;
suppose A55: Wmin = SW;
set h = R_Cut(US,Nmin);
A56: Nmin in L~US by Th7;
A57: Wmax`2 > Wmin`2 by SPRECT_2:61;
Wmax in L~Ca by SPRECT_1:15;
then Nbo >= Wmax`2 by PSCOMP_1:71;
then Nmin <> US.1 by A6,A57,PSCOMP_1:94;
then reconsider RCutUS = R_Cut(US,Nmin) as
being_S-Seq FinSequence of TOP-REAL 2 by A56,JORDAN3:70;
A58: RCutUS/.1 = US/.1 by A56,SPRECT_3:39
.= Wmin by JORDAN1F:5;
A59: 2 <= len g by TOPREAL1:def 10;
A60: len RCutUS >= 2 by TOPREAL1:def 10;
A61: US is_in_the_area_of Ca by JORDAN1E:21;
then <*Nmin*> is_in_the_area_of Ca by A56,SPRECT_3:63;
then A62: R_Cut(US,Nmin) is_in_the_area_of Ca by A56,A61,SPRECT_3:69;
R_Cut(US,Nmin)/.len R_Cut(US,Nmin) = Nmin by A56,Th45;
then A63: (h/.len h)`2 = Nbo by PSCOMP_1:94;
(h/.1)`2 = Sbo by A55,A58,PSCOMP_1:73;
then h is_a_v.c._for Ca by A62,A63,SPRECT_2:def 3;
then L~g meets L~h by A13,A59,A60,SPRECT_2:33;
then consider x be set such that
A64: x in L~g and
A65: x in L~h by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A64;
A66: L~g c= L~LS by A1,A7,JORDAN3:76;
A67: L~RCutUS c= L~US by A56,JORDAN3:76;
A68: len LS in dom LS & len US in dom US by FINSEQ_5:6;
x in L~LS /\ L~US by A64,A65,A66,A67,XBOOLE_0:def 3;
then A69: x in {Emax,Wmin} by JORDAN1E:20;
now per cases by A69,TARSKI:def 2;
suppose x = Emax;
then US/.len US in L~R_Cut(US,Nmin) by A65,JORDAN1F:7;
then US.len US in L~R_Cut(US,Nmin) by A68,FINSEQ_4:def 4;
then US.len US = Nmin by A56,Th43;
then US/.len US = Nmin by A68,FINSEQ_4:def 4;
then A70: Emax = Nmin by JORDAN1F:7;
A71: Nmax`1 > Nmin`1 by SPRECT_2:55;
Nmax in L~Ca by SPRECT_1:13;
then Ebo >= Nmax`1 by PSCOMP_1:71;
hence contradiction by A70,A71,PSCOMP_1:104;
suppose x = Wmin;
then LS/.len LS in L~R_Cut(LS,p) by A7,A64,JORDAN1F:8;
then LS.len LS in L~R_Cut(LS,p) by A68,FINSEQ_4:def 4;
then LS.len LS = p by A1,Th43;
then LS/.len LS = p by A68,FINSEQ_4:def 4;
hence contradiction by A3,JORDAN1F:8;
end;
hence contradiction;
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: (f^g)|len f = f by FINSEQ_5:26;
A5: k+1 <= len f by A2,NAT_1:38;
len f <= len f + len g by NAT_1:29;
then len f <= len (f^g) by FINSEQ_1:35;
then k+1 <= len (f^g) by A5,AXIOMS:22;
hence thesis by A1,A3,A4,A5,GOBRD13:32;
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 TOPREAL1:3;
per cases;
suppose A3: g <> {};
then len g <> 0 by FINSEQ_1:25;
then len g > 0 by NAT_1:19;
then len g >= 0+1 by NAT_1:38;
then i+1 <= len f+len g by A1,REAL_1:55;
then i+1 <= len(f^'g)+1 by A3,GRAPH_2:13;
then i <= len(f^'g) by REAL_1:53;
then A4: len((f^'g)|i) = i by TOPREAL1:3;
now let j be Nat;
assume A5: j in Seg i;
then j <= i by FINSEQ_1:3;
then A6: 1 <= j & j <= len f by A1,A5,AXIOMS:22,FINSEQ_1:3;
thus ((f^'g)|i).j = ((f^'g)|(Seg i)).j by TOPREAL1:def 1
.= (f^'g).j by A5,FUNCT_1:72
.= f.j by A6,GRAPH_2:14
.= (f|(Seg i)).j by A5,FUNCT_1:72
.= (f|i).j by TOPREAL1:def 1;
end;
hence (f^'g)|i = f|i by A2,A4,FINSEQ_2:10;
suppose g = {};
hence thesis by AMISTD_1:7;
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 TOPREAL1:def 1;
hence f = f|len f by FINSEQ_2:23
.= (f^'g)|(len f) by Th49;
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: (f^'g)|len f = f by Th50;
A5: k+1 <= len f by A2,NAT_1:38;
len f <= len (f^'g) by TOPREAL8:7;
then k+1 <= len (f^'g) by A5,AXIOMS:22;
hence thesis by A1,A3,A4,A5,GOBRD13:32;
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;
p..f >= 1 by A1,A2,AXIOMS:22;
then A5: f|(p..f) = mid(f,1,p..f) by JORDAN3:25
.= R_Cut(f,p) by A4,JORDAN1G:57;
A6: k+1 <= p..f by A2,NAT_1:38;
p..f <= len f by A4,FINSEQ_4:31;
then k+1 <= len f by A6,AXIOMS:22;
hence thesis by A1,A3,A5,A6,GOBRD13:32;
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: f|(p..f) = f-:p by FINSEQ_5:def 1;
A5: k+1 <= p..f by A2,NAT_1:38;
per cases by TOPREAL8:4;
suppose p in rng f;
then p..f <= len f by FINSEQ_4:31;
then k+1 <= len f by A5,AXIOMS:22;
hence thesis by A1,A3,A4,A5,GOBRD13:32;
suppose p..f = 0;
hence thesis by A2,NAT_1:18;
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 A7: LSeg(f^'g,j) = LSeg(f,j) by TOPREAL8:28;
i+1 < len f by A5,A6,AXIOMS:22;
then i < len f by NAT_1:38;
then LSeg(f^'g,i) = LSeg(f,i) by TOPREAL8:28;
hence LSeg(f^'g,i) misses LSeg(f^'g,j) by A1,A5,A7,TOPREAL1:def 9;
suppose j >= len f;
then consider k be Nat such that
A8: j = len f + k by NAT_1:28;
A9: now assume f is empty;
then len f = 0 by FINSEQ_1:25;
then L~f = {} by TOPREAL1:28;
hence contradiction by A4;
end;
A10: now assume g is trivial;
then len g < 2 by SPPOL_1:2;
then len g = 0 or len g = 1 by ALGSEQ_1:4;
then L~g = {} by TOPREAL1:28;
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:38;
then len f+k+1 < len f + len g by A8,A10,GRAPH_2:13;
then len f+(k+1) < len f + len g by XCMPLX_1:1;
then A12: k+1 < len g by REAL_1:55;
then A13: LSeg(f^'g,len f+k) = LSeg(g,k+1) by A3,A9,A10,TOPREAL8:31;
then A14: LSeg(f^'g,j) c= L~g by A8,TOPREAL3:26;
now per cases;
suppose A15: i < len f;
then A16: LSeg(f^'g,i) = LSeg(f,i) by TOPREAL8:28;
then LSeg(f^'g,i) c= L~f by TOPREAL3:26;
then A17: 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 set such that
A18: x in LSeg(f^'g,i) and
A19: x in LSeg(f^'g,j) by XBOOLE_0:3;
x in LSeg(f^'g,i) /\ LSeg(f^'g,j) by A18,A19,XBOOLE_0:def 3;
then A20: x = g/.1 by A17,TARSKI:def 1;
A21: i in dom f by A11,A15,FINSEQ_3:27;
i+1 > 1 & i+1 <= len f by A11,A15,NAT_1:38;
then i+1 in dom f by FINSEQ_3:27;
then len f+0 < len f+k by A1,A3,A5,A8,A16,A18,A20,A21,GOBOARD2:7;
then k > 0 by REAL_1:55;
then A22: k+1 > 0+1 by REAL_1:53;
len g >= 2 by A10,SPPOL_1:2;
hence contradiction by A2,A8,A13,A19,A20,A22,JORDAN5B:33;
suppose i >= len f;
then consider l be Nat such that
A23: i = len f + l by NAT_1:28;
len f+(l+1) < len f+k by A5,A8,A23,XCMPLX_1:1;
then l+1 < k by REAL_1:55;
then A24: l+1+1 < k+1 by REAL_1:53;
then l+1+1 < len g by A12,AXIOMS:22;
then l+1 < len g by NAT_1:38;
then LSeg(f^'g,len f+l) = LSeg(g,l+1) by A3,A9,A10,TOPREAL8:31;
hence LSeg(f^'g,i) misses LSeg(f^'g,j)
by A2,A8,A13,A23,A24,TOPREAL1:def 9;
end;
hence LSeg(f^'g,i) misses LSeg(f^'g,j);
suppose j+1 > len(f^'g);
then LSeg(f^'g,j) = {} by TOPREAL1:def 5;
hence LSeg(f^'g,i) misses LSeg(f^'g,j) by XBOOLE_1:65;
suppose i < 1;
then LSeg(f^'g,i) = {} by TOPREAL1:def 5;
hence LSeg(f^'g,i) misses LSeg(f^'g,j) by XBOOLE_1:65;
end;
hence LSeg(f^'g,i) misses LSeg(f^'g,j);
end;
hence LSeg(f^'g,i) misses LSeg(f^'g,j);
end;
hence f^'g is s.n.c. by TOPREAL1:def 9;
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 let i,j be Nat;
assume that
A5: i in dom (f^'g) and
A6: j in dom (f^'g) and
A7: (f^'g)/.i = (f^'g)/.j;
A8: 1 <= i & i <= len (f^'g) by A5,FINSEQ_3:27;
A9: 1 <= j & j <= len (f^'g) by A6,FINSEQ_3:27;
g <> {} by A4,FINSEQ_1:27;
then len (f^'g)+1 = len f + len g by GRAPH_2:13;
then A10: i < len f + len g & j < len f + len g by A8,A9,NAT_1:38;
A11: len f = len f + 0;
A12: 1 in dom g by A4,FINSEQ_3:34;
now per cases;
suppose A13: i <= len f & j <= len f;
then A14: (f^'g)/.i = f/.i & (f^'g)/.j = f/.j by A8,A9,AMISTD_1:9;
i in dom f & j in dom f by A8,A9,A13,FINSEQ_3:27;
hence i = j by A1,A7,A14,PARTFUN2:17;
suppose A15: i > len f & j > len f;
then consider k be Nat such that
A16: i = len f + k by NAT_1:28;
consider l be Nat such that
A17: j = len f + l by A15,NAT_1:28;
A18: k < len g & l < len g by A10,A16,A17,REAL_1:55;
k > 0 by A11,A15,A16,REAL_1:55;
then A19: k >= 0+1 by NAT_1:38;
then A20: (f^'g)/.i = g/.(k+1) by A16,A18,AMISTD_1:10;
l > 0 by A11,A15,A17,REAL_1:55;
then A21: l >= 0+1 by NAT_1:38;
then A22: (f^'g)/.j = g/.(l+1) by A17,A18,AMISTD_1:10;
A23: k+1 <= len g & l+1 <= len g by A18,NAT_1:38;
k+1 > 1 & l+1 > 1 by A19,A21,NAT_1:38;
then k+1 in dom g & l+1 in dom g by A23,FINSEQ_3:27;
then k+1 = l+1 by A2,A7,A20,A22,PARTFUN2:17;
hence i = j by A16,A17,XCMPLX_1:2;
suppose A24: i <= len f & j > len f;
then A25: (f^'g)/.i = f/.i by A8,AMISTD_1:9;
i in dom f by A8,A24,FINSEQ_3:27;
then A26: (f^'g)/.i in rng f by A25,PARTFUN2:4;
consider l be Nat such that
A27: j = len f + l by A24,NAT_1:28;
A28: l < len g by A10,A27,REAL_1:55;
l > 0 by A11,A24,A27,REAL_1:55;
then A29: l >= 0+1 by NAT_1:38;
then A30: (f^'g)/.j = g/.(l+1) by A27,A28,AMISTD_1:10;
A31: l+1 <= len g by A28,NAT_1:38;
A32: l+1 > 1 by A29,NAT_1:38;
then A33: l+1 in dom g by A31,FINSEQ_3:27;
then (f^'g)/.j in rng g by A30,PARTFUN2:4;
then (f^'g)/.j in rng f /\ rng g by A7,A26,XBOOLE_0:def 3;
then g/.(l+1) = g/.1 by A3,A30,TARSKI:def 1;
hence i = j by A2,A12,A32,A33,PARTFUN2:17;
suppose A34: j <= len f & i > len f;
then A35: (f^'g)/.j = f/.j by A9,AMISTD_1:9;
j in dom f by A9,A34,FINSEQ_3:27;
then A36: (f^'g)/.j in rng f by A35,PARTFUN2:4;
consider l be Nat such that
A37: i = len f + l by A34,NAT_1:28;
A38: l < len g by A10,A37,REAL_1:55;
l > 0 by A11,A34,A37,REAL_1:55;
then A39: l >= 0+1 by NAT_1:38;
then A40: (f^'g)/.i = g/.(l+1) by A37,A38,AMISTD_1:10;
A41: l+1 <= len g by A38,NAT_1:38;
A42: l+1 > 1 by A39,NAT_1:38;
then A43: l+1 in dom g by A41,FINSEQ_3:27;
then (f^'g)/.i in rng g by A40,PARTFUN2:4;
then (f^'g)/.i in rng f /\ rng g by A7,A36,XBOOLE_0:def 3;
then g/.(l+1) = g/.1 by A3,A40,TARSKI:def 1;
hence i = j by A2,A12,A42,A43,PARTFUN2:17;
end;
hence i = j;
end;
hence f^'g is one-to-one by PARTFUN2:16;
suppose rng g = {};
then g = {} by FINSEQ_1:27;
hence f^'g is one-to-one by A1,AMISTD_1:7;
end;
theorem Th56:
for f be FinSequence of TOP-REAL 2
for p be Point of TOP-REAL 2 st f is_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_S-Seq and
A2: p in rng f and
A3: p <> f.1;
A4: 1 <= p..f & p..f <= len f by A2,FINSEQ_4:31;
p..f <> 1 by A2,A3,FINSEQ_4:29;
then A5: 1 < p..f by A4,REAL_1:def 5;
f.(p..f) = p by A2,FINSEQ_4:29;
hence Index(p,f)+1 = p..f by A1,A4,A5,JORDAN3:45;
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 & i < len Gauge(C,n) and
A2: 1 <= j & k <= width Gauge(C,n) and
A3: Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) and
A4: Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) and
A5: j = k;
A6: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n)
by A3,A4,A5,XBOOLE_0:def 3;
then A7: Gauge(C,n)*(i,k) in {W-min L~Cage(C,n),E-max L~Cage(C,n)}
by JORDAN1E:20;
A8: [i,j] in Indices Gauge(C,n) by A1,A2,A5,GOBOARD7:10;
len Gauge(C,n) >= 4 by JORDAN8:13;
then A9: len Gauge(C,n) >= 1 by AXIOMS:22;
then A10: [len Gauge(C,n),j] in Indices Gauge(C,n) by A2,A5,GOBOARD7:10;
A11: [1,j] in Indices Gauge(C,n) by A2,A5,A9,GOBOARD7:10;
per cases by A7,TARSKI:def 2;
suppose A12: Gauge(C,n)*(i,k) = W-min L~Cage(C,n);
Gauge(C,n)*(1,j)`1 = W-bound L~Cage(C,n) by A2,A5,A6,JORDAN1A:94;
then (W-min L~Cage(C,n))`1 <> W-bound L~Cage(C,n)
by A1,A5,A8,A11,A12,JORDAN1G:7;
hence contradiction by PSCOMP_1:84;
suppose A13: 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 A2,A5,A6,JORDAN1A:92;
then (E-max L~Cage(C,n))`1 <> E-bound L~Cage(C,n)
by A1,A5,A8,A10,A13,JORDAN1G:7;
hence contradiction by PSCOMP_1:104;
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 & i < len Ga and
A2: 1 <= j & j <= k & k <= width Ga and
A3: LSeg(Gij,Gik) /\ L~US = {Gik} and
A4: LSeg(Gij,Gik) /\ L~LS = {Gij} and
A5: LSeg(Gij,Gik) misses LA;
Gij in {Gij} by TARSKI:def 1;
then A6: Gij in L~LS by A4,XBOOLE_0:def 3;
Gik in {Gik} by TARSKI:def 1;
then A7: Gik in L~US by A3,XBOOLE_0:def 3;
then A8: j <> k by A1,A2,A6,Th57;
A9: 1 <= j & j <= width Ga by A2,AXIOMS:22;
A10: 1 <= k & k <= width Ga by A2,AXIOMS:22;
A11: [i,j] in Indices Ga by A1,A9,GOBOARD7:10;
A12: [i,k] in Indices Ga by A1,A10,GOBOARD7:10;
A13: US is_sequence_on Ga by JORDAN1G:4;
A14: LS is_sequence_on Ga by JORDAN1G:5;
set go = R_Cut(US,Gik);
set do = L_Cut(LS,Gij);
A15: len Ga = width Ga by JORDAN8:def 1;
A16: len US >= 3 by JORDAN1E:19;
then len US >= 1 by AXIOMS:22;
then 1 in dom US by FINSEQ_3:27;
then A17: US.1 = US/.1 by FINSEQ_4:def 4
.= Wmin by JORDAN1F:5;
A18: Wmin`1 = Wbo by PSCOMP_1:84
.= Ga*(1,k)`1 by A10,A15,JORDAN1A:94;
len Ga >= 4 by JORDAN8:13;
then A19: len Ga >= 1 by AXIOMS:22;
then A20: [1,k] in Indices Ga by A10,GOBOARD7:10;
then A21: Gik <> US.1 by A1,A12,A17,A18,JORDAN1G:7;
then reconsider go as being_S-Seq FinSequence of TOP-REAL 2
by A7,JORDAN3:70;
A22: len LS >= 1+2 by JORDAN1E:19;
then len LS >= 1 by AXIOMS:22;
then A23: 1 in dom LS & len LS in dom LS by FINSEQ_3:27;
then A24: LS.len LS = LS/.len LS by FINSEQ_4:def 4
.= Wmin by JORDAN1F:8;
A25: Wmin`1 = Wbo by PSCOMP_1:84
.= Ga*(1,k)`1 by A10,A15,JORDAN1A:94;
A26: [i,j] in Indices Ga by A1,A9,GOBOARD7:10;
then A27: Gij <> LS.len LS by A1,A20,A24,A25,JORDAN1G:7;
then reconsider do as being_S-Seq FinSequence of TOP-REAL 2
by A6,JORDAN3:69;
A28: [len Ga,k] in Indices Ga by A10,A19,GOBOARD7:10;
A29: LS.1 = LS/.1 by A23,FINSEQ_4:def 4
.= Emax by JORDAN1F:6;
Emax`1 = Ebo by PSCOMP_1:104
.= Ga*(len Ga,k)`1 by A10,A15,JORDAN1A:92;
then A30: Gij <> LS.1 by A1,A26,A28,A29,JORDAN1G:7;
A31: len go >= 1+1 by TOPREAL1:def 10;
A32: Gik in rng US by A1,A7,A10,A13,Th40;
then A33: go is_sequence_on Ga by A13,Th38;
A34: len do >= 1+1 by TOPREAL1:def 10;
A35: Gij in rng LS by A1,A6,A9,A14,Th40;
then A36: do is_sequence_on Ga by A14,Th39;
reconsider go as non constant s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2) by A31,A33,JGRAPH_1:16,
JORDAN8:8;
reconsider do as non constant s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2) by A34,A36,JGRAPH_1:16,
JORDAN8:8;
A37: len go > 1 by A31,NAT_1:38;
then A38: len go in dom go by FINSEQ_3:27;
then A39: go/.len go = go.len go by FINSEQ_4:def 4
.= Gik by A7,JORDAN3:59;
len do >= 1 by A34,AXIOMS:22;
then 1 in dom do by FINSEQ_3:27;
then A40: do/.1 = do.1 by FINSEQ_4:def 4
.= Gij by A6,JORDAN3:58;
reconsider m = len go - 1 as Nat by A38,FINSEQ_3:28;
A41: m+1 = len go by XCMPLX_1:27;
then A42: len go-'1 = m by BINARITH:39;
A43: LSeg(go,m) c= L~go by TOPREAL3:26;
A44: L~go c= L~US by A7,JORDAN3:76;
then LSeg(go,m) c= L~US by A43,XBOOLE_1:1;
then A45: LSeg(go,m) /\ LSeg(Gik,Gij) c= {Gik} by A3,XBOOLE_1:26;
m >= 1 by A31,REAL_1:84;
then A46: LSeg(go,m) = LSeg(go/.m,Gik) by A39,A41,TOPREAL1:def 5;
{Gik} c= LSeg(go,m) /\ LSeg(Gik,Gij)
proof
let x be set;
assume x in {Gik};
then A47: x = Gik by TARSKI:def 1;
A48: Gik in LSeg(go,m) by A46,TOPREAL1:6;
Gik in LSeg(Gik,Gij) by TOPREAL1:6;
hence x in LSeg(go,m) /\ LSeg(Gik,Gij) by A47,A48,XBOOLE_0:def 3;
end;
then A49: LSeg(go,m) /\ LSeg(Gik,Gij) = {Gik} by A45,XBOOLE_0:def 10;
A50: LSeg(do,1) c= L~do by TOPREAL3:26;
A51: L~do c= L~LS by A6,JORDAN3:77;
then LSeg(do,1) c= L~LS by A50,XBOOLE_1:1;
then A52: LSeg(do,1) /\ LSeg(Gik,Gij) c= {Gij} by A4,XBOOLE_1:26;
A53: LSeg(do,1) = LSeg(Gij,do/.(1+1)) by A34,A40,TOPREAL1:def 5;
{Gij} c= LSeg(do,1) /\ LSeg(Gik,Gij)
proof
let x be set;
assume x in {Gij};
then A54: x = Gij by TARSKI:def 1;
A55: Gij in LSeg(do,1) by A53,TOPREAL1:6;
Gij in LSeg(Gik,Gij) by TOPREAL1:6;
hence x in LSeg(do,1) /\ LSeg(Gik,Gij) by A54,A55,XBOOLE_0:def 3;
end;
then A56: LSeg(Gik,Gij) /\ LSeg(do,1) = {Gij} by A52,XBOOLE_0:def 10;
A57: go/.1 = US/.1 by A7,SPRECT_3:39
.= Wmin by JORDAN1F:5;
then A58: go/.1 = LS/.len LS by JORDAN1F:8
.= do/.len do by A6,Th35;
A59: rng go c= L~go & rng do c= L~do by A31,A34,SPPOL_2:18;
A60: {go/.1} c= L~go /\ L~do
proof
let x be set;
assume x in {go/.1};
then x = go/.1 by TARSKI:def 1;
then x in rng go & x in rng do by A58,FINSEQ_6:46,REVROT_1:3;
hence x in L~go /\ L~do by A59,XBOOLE_0:def 3;
end;
A61: LS.1 = LS/.1 by A23,FINSEQ_4:def 4
.= Emax by JORDAN1F:6;
A62: [len Ga,j] in Indices Ga by A9,A19,GOBOARD7:10;
L~go /\ L~do c= {go/.1}
proof
let x be set;
assume x in L~go /\ L~do;
then A63: x in L~go & x in L~do by XBOOLE_0:def 3;
then x in L~US /\ L~LS by A44,A51,XBOOLE_0:def 3;
then x in {Wmin,Emax} by JORDAN1E:20;
then A64: x = Wmin or x = Emax by TARSKI:def 2;
now assume x = Emax;
then A65: Emax = Gij by A6,A61,A63,JORDAN1E:11;
Ga*(len Ga,j)`1 = Ebo by A9,A15,JORDAN1A:92;
then Emax`1 <> Ebo by A1,A11,A62,A65,JORDAN1G:7;
hence contradiction by PSCOMP_1:104;
end;
hence x in {go/.1} by A57,A64,TARSKI:def 1;
end;
then A66: L~go /\ L~do = {go/.1} by A60,XBOOLE_0:def 10;
set W2 = go/.2;
A67: 2 in dom go by A31,FINSEQ_3:27;
A68: Gik..US >= 1 by A32,FINSEQ_4:31;
A69: now assume Gik`1 = Wbo;
then Ga*(1,k)`1 = Ga*(i,k)`1 by A10,A15,JORDAN1A:94;
hence contradiction by A1,A12,A20,JORDAN1G:7;
end;
go = mid(US,1,Gik..US) by A32,JORDAN1G:57
.= US|(Gik..US) by A68,JORDAN3:25;
then A70: W2 = US/.2 by A67,TOPREAL1:1;
set pion = <*Gik,Gij*>;
A71: now let n be Nat;
assume n in dom pion;
then n in Seg 2 by FINSEQ_3:29;
then n = 1 or n = 2 by FINSEQ_1:4,TARSKI:def 2;
then pion/.n = Gik or pion/.n = Gij by FINSEQ_4:26;
hence ex i,j be Nat st [i,j] in Indices Ga & pion/.n = Ga*(i,j)
by A11,A12;
end;
A72: Gik <> Gij by A8,A11,A12,GOBOARD1:21;
A73: Gik`1 = Ga*(i,1)`1 by A1,A10,GOBOARD5:3
.= Gij`1 by A1,A9,GOBOARD5:3;
then LSeg(Gik,Gij) is vertical by SPPOL_1:37;
then pion is_S-Seq by A72,JORDAN1B:8;
then consider pion1 be FinSequence of TOP-REAL 2 such that
A74: pion1 is_sequence_on Ga and
A75: pion1 is_S-Seq and
A76: L~pion = L~pion1 and
A77: pion/.1 = pion1/.1 and
A78: pion/.len pion = pion1/.len pion1 and
A79: len pion <= len pion1 by A71,GOBOARD3:2;
reconsider pion1 as being_S-Seq FinSequence of TOP-REAL 2 by A75;
set godo = go^'pion1^'do;
len Cage(C,n) > 4 by GOBOARD7:36;
then A80: 1+1 <= len Cage(C,n) by AXIOMS:22;
then A81: 1+1 <= len Rotate(Cage(C,n),Wmin) by REVROT_1:14;
len (go^'pion1) >= len go by TOPREAL8:7;
then A82: len (go^'pion1) >= 1+1 by A31,AXIOMS:22;
then A83: len (go^'pion1) > 1+0 by NAT_1:38;
len godo >= len (go^'pion1) by TOPREAL8:7;
then A84: 1+1 <= len godo by A82,AXIOMS:22;
A85: US is_sequence_on Ga by JORDAN1G:4;
A86: go/.len go = pion1/.1 by A39,A77,FINSEQ_4:26;
then A87: go^'pion1 is_sequence_on Ga by A33,A74,TOPREAL8:12;
A88: (go^'pion1)/.len (go^'pion1) = pion/.len pion by A78,AMISTD_1:6
.= pion/.2 by FINSEQ_1:61
.= do/.1 by A40,FINSEQ_4:26;
then A89: godo is_sequence_on Ga by A36,A87,TOPREAL8:12;
LSeg(pion1,1) c= L~<*Gik,Gij*> by A76,TOPREAL3:26;
then LSeg(pion1,1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then A90: LSeg(go,len go-'1) /\ LSeg(pion1,1) c= {Gik} by A42,A49,XBOOLE_1:
27;
A91: len pion1 >= 1+1 by A79,FINSEQ_1:61;
{Gik} c= LSeg(go,m) /\ LSeg(pion1,1)
proof
let x be set;
assume x in {Gik};
then A92: x = Gik by TARSKI:def 1;
A93: Gik in LSeg(go,m) by A46,TOPREAL1:6;
Gik in LSeg(pion1,1) by A39,A86,A91,TOPREAL1:27;
hence x in LSeg(go,m) /\ LSeg(pion1,1) by A92,A93,XBOOLE_0:def 3;
end;
then LSeg(go,len go-'1) /\ LSeg(pion1,1) = { go/.len go }
by A39,A42,A90,XBOOLE_0:def 10
;
then A94: go^'pion1 is unfolded by A86,TOPREAL8:34;
len pion1 >= 2+0 by A79,FINSEQ_1:61;
then A95: len pion1-2 >= 0 by REAL_1:84;
A96: len (go^'pion1)-1 >= 0 by A83,REAL_1:84;
len (go^'pion1)+1-1 = len go+len pion1-1 by GRAPH_2:13;
then len (go^'pion1)-1 = len go+len pion1-1-1 by XCMPLX_1:26
.= len go + len pion1-(1+1) by XCMPLX_1:36
.= len go + (len pion1-2) by XCMPLX_1:29
.= len go + (len pion1-'2) by A95,BINARITH:def 3;
then A97: len (go^'pion1)-'1 = len go + (len pion1-'2)
by A96,BINARITH:def 3;
A98: len pion1-1 >= 1 by A91,REAL_1:84;
then A99: len pion1-1 >= 0 by AXIOMS:22;
then A100: len pion1-'1 = len pion1-1 by BINARITH:def 3;
A101: len pion1-'2+1 = len pion1-2+1 by A95,BINARITH:def 3
.= len pion1-(2-1) by XCMPLX_1:37
.= len pion1-'1 by A99,BINARITH:def 3;
len pion1-1+1 <= len pion1 by XCMPLX_1:27;
then A102: len pion1-'1 < len pion1 by A100,NAT_1:38;
LSeg(pion1,len pion1-'1) c= L~<*Gik,Gij*> by A76,TOPREAL3:26;
then LSeg(pion1,len pion1-'1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then A103: LSeg(pion1,len pion1-'1) /\ LSeg(do,1) c= {Gij} by A56,XBOOLE_1:
27;
{Gij} c= LSeg(pion1,len pion1-'1) /\ LSeg(do,1)
proof
let x be set;
assume x in {Gij};
then A104: x = Gij by TARSKI:def 1;
A105: Gij in LSeg(do,1) by A53,TOPREAL1:6;
A106: len pion1-'1+1 = len pion1 by A100,XCMPLX_1:27;
then pion1/.(len pion1-'1+1) = pion/.2 by A78,FINSEQ_1:61
.= Gij by FINSEQ_4:26;
then Gij in LSeg(pion1,len pion1-'1) by A98,A100,A106,TOPREAL1:27;
hence x in LSeg(pion1,len pion1-'1) /\ LSeg(do,1) by A104,A105,XBOOLE_0:
def 3;
end;
then LSeg(pion1,len pion1-'1) /\ LSeg(do,1) = {Gij} by A103,XBOOLE_0:def 10
;
then A107: LSeg(go^'pion1,len go+(len pion1-'2)) /\ LSeg(do,1) =
{(go^'pion1)/.len (go^'pion1)} by A40,A86,A88,A101,A102,TOPREAL8:31;
A108: (go^'pion1) is non trivial by A82,SPPOL_1:2;
A109: rng pion1 c= L~pion1 by A91,SPPOL_2:18;
A110: {pion1/.1} c= L~go /\ L~pion1
proof
let x be set;
assume x in {pion1/.1};
then x = pion1/.1 by TARSKI:def 1;
then x in rng go & x in rng pion1 by A86,FINSEQ_6:46,REVROT_1:3;
hence x in L~go /\ L~pion1 by A59,A109,XBOOLE_0:def 3;
end;
L~go /\ L~pion1 c= {pion1/.1}
proof
let x be set;
assume x in L~go /\ L~pion1;
then x in L~go & x in L~pion1 by XBOOLE_0:def 3;
then x in L~pion1 /\ L~US by A44,XBOOLE_0:def 3;
hence x in {pion1/.1} by A3,A39,A76,A86,SPPOL_2:21;
end;
then A111: L~go /\ L~pion1 = {pion1/.1} by A110,XBOOLE_0:def 10;
then A112: (go^'pion1) is s.n.c. by A86,Th54;
rng go /\ rng pion1 c= {pion1/.1} by A59,A109,A111,XBOOLE_1:27;
then A113: go^'pion1 is one-to-one by Th55;
A114: pion/.len pion = pion/.2 by FINSEQ_1:61
.= do/.1 by A40,FINSEQ_4:26;
A115: {pion1/.len pion1} c= L~do /\ L~pion1
proof
let x be set;
assume x in {pion1/.len pion1};
then x = pion1/.len pion1 by TARSKI:def 1;
then x in rng do & x in rng pion1 by A78,A114,FINSEQ_6:46,REVROT_1:3;
hence x in L~do /\ L~pion1 by A59,A109,XBOOLE_0:def 3;
end;
L~do /\ L~pion1 c= {pion1/.len pion1}
proof
let x be set;
assume x in L~do /\ L~pion1;
then x in L~do & x in L~pion1 by XBOOLE_0:def 3;
then x in L~pion1 /\ L~LS by A51,XBOOLE_0:def 3;
hence x in {pion1/.len pion1} by A4,A40,A76,A78,A114,SPPOL_2:21;
end;
then A116: L~do /\ L~pion1 = {pion1/.len pion1} by A115,XBOOLE_0:def 10;
A117: L~(go^'pion1) /\ L~do = (L~go \/ L~pion1) /\ L~do by A86,TOPREAL8:35
.= {go/.1} \/ {do/.1} by A66,A78,A114,A116,XBOOLE_1:23
.= {(go^'pion1)/.1} \/ {do/.1} by AMISTD_1:5
.= {(go^'pion1)/.1,do/.1} by ENUMSET1:41;
do/.len do = (go^'pion1)/.1 by A58,AMISTD_1:5;
then reconsider godo as non constant standard special_circular_sequence
by A84,A88,A89,A94,A97,A107,A108,
A112,A113,A117,JORDAN8:7,8,TOPREAL8:11,33,34;
A118: LA is_an_arc_of E-max C,W-min C by JORDAN6:def 9;
then A119: LA is connected by JORDAN6:11;
A120: W-min C in LA & E-max C in LA by A118,TOPREAL1:4;
set ff = Rotate(Cage(C,n),Wmin);
Wmin in rng Cage(C,n) by SPRECT_2:47;
then A121: ff/.1 = Wmin by FINSEQ_6:98;
A122: L~ff = L~Cage(C,n) by REVROT_1:33;
then A123: (W-max L~ff)..ff > 1 by A121,SPRECT_5:23;
(W-max L~ff)..ff <= (N-min L~ff)..ff by A121,A122,SPRECT_5:24;
then A124: (N-min L~ff)..ff > 1 by A123,AXIOMS:22;
(N-min L~ff)..ff < (N-max L~ff)..ff by A121,A122,SPRECT_5:25;
then A125: (N-max L~ff)..ff > 1 by A124,AXIOMS:22;
(N-max L~ff)..ff <= (E-max L~ff)..ff by A121,A122,SPRECT_5:26;
then A126: Emax..ff > 1 by A122,A125,AXIOMS:22;
A127: now assume A128: Gik..US <= 1;
Gik..US >= 1 by A32,FINSEQ_4:31;
then Gik..US = 1 by A128,AXIOMS:21;
then Gik = US/.1 by A32,FINSEQ_5:41;
hence contradiction by A17,A21,JORDAN1F:5;
end;
A129: Cage(C,n) is_sequence_on Ga by JORDAN9:def 1;
then A130: ff is_sequence_on Ga by REVROT_1:34;
A131: right_cell(godo,1,Ga)\L~godo c= RightComp godo by A84,A89,JORDAN9:29;
A132: L~godo = L~(go^'pion1) \/ L~do by A88,TOPREAL8:35
.= L~go \/ L~pion1 \/ L~do by A86,TOPREAL8:35;
L~Cage(C,n) = L~US \/ L~LS by JORDAN1E:17;
then A133: L~US c= L~Cage(C,n) & L~LS c= L~Cage(C,n) by XBOOLE_1:7;
then A134: L~go c= L~Cage(C,n) & L~do c= L~Cage(C,n) by A44,A51,XBOOLE_1:1;
A135: W-min C in C by SPRECT_1:15;
A136: L~pion = LSeg(Gik,Gij) by SPPOL_2:21;
A137: now assume W-min C in L~godo;
then A138: W-min C in L~go \/ L~pion1 or W-min C in L~do by A132,XBOOLE_0:
def 2;
per cases by A138,XBOOLE_0:def 2;
suppose W-min C in L~go;
then C meets L~Cage(C,n) by A134,A135,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
suppose W-min C in L~pion1;
hence contradiction by A5,A76,A120,A136,XBOOLE_0:3;
suppose W-min C in L~do;
then C meets L~Cage(C,n) by A134,A135,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
end;
right_cell(Rotate(Cage(C,n),Wmin),1) =
right_cell(ff,1,GoB ff) by A81,JORDAN1H:29
.= right_cell(ff,1,GoB Cage(C,n)) by REVROT_1:28
.= right_cell(ff,1,Ga) by JORDAN1H:52
.= right_cell(ff-:Emax,1,Ga) by A126,A130,Th53
.= right_cell(US,1,Ga) by JORDAN1E:def 1
.= right_cell(R_Cut(US,Gik),1,Ga) by A32,A85,A127,Th52
.= right_cell(go^'pion1,1,Ga) by A37,A87,Th51
.= right_cell(godo,1,Ga) by A83,A89,Th51;
then W-min C in right_cell(godo,1,Ga) by JORDAN1I:8;
then A139: W-min C in right_cell(godo,1,Ga)\L~godo by A137,XBOOLE_0:def 4;
A140: godo/.1 = (go^'pion1)/.1 by AMISTD_1:5
.= Wmin by A57,AMISTD_1:5;
A141: len US >= 2 by A16,AXIOMS:22;
A142: godo/.2 = (go^'pion1)/.2 by A82,AMISTD_1:9
.= US/.2 by A31,A70,AMISTD_1:9
.= (US^'LS)/.2 by A141,AMISTD_1:9
.= Rotate(Cage(C,n),Wmin)/.2 by JORDAN1E:15;
A143: L~go \/ L~do is compact by COMPTS_1:19;
A144: L~go \/ L~do c= L~Cage(C,n) by A134,XBOOLE_1:8;
Wmin in rng go by A57,FINSEQ_6:46;
then Wmin in L~go \/ L~do by A59,XBOOLE_0:def 2;
then A145: W-min (L~go \/ L~do) = Wmin by A143,A144,Th21;
A146: (W-min (L~go \/ L~do))`1 = W-bound (L~go \/ L~do) & Wmin`1 = Wbo
by PSCOMP_1:84;
W-bound LSeg(Gik,Gij) = Gik`1 by A73,SPRECT_1:62;
then A147: W-bound L~pion1 = Gik`1 by A76,SPPOL_2:21;
Gik`1 >= Wbo by A7,A133,PSCOMP_1:71;
then Gik`1 > Wbo by A69,REAL_1:def 5;
then W-min (L~go\/L~do\/L~pion1) = W-min (L~go \/ L~do)
by A143,A145,A146,A147,Th33;
then A148: W-min L~godo = Wmin by A132,A145,XBOOLE_1:4;
A149: rng godo c= L~godo by A84,SPPOL_2:18;
2 in dom godo by A84,FINSEQ_3:27;
then A150: godo/.2 in rng godo by PARTFUN2:4;
godo/.2 in W-most L~Cage(C,n) by A142,JORDAN1I:27;
then (godo/.2)`1 = (W-min L~godo)`1 by A148,PSCOMP_1:88
.= W-bound L~godo by PSCOMP_1:84;
then godo/.2 in W-most L~godo by A149,A150,SPRECT_2:16;
then Rotate(godo,W-min L~godo)/.2 in W-most L~godo by A140,A148,FINSEQ_6:95
;
then reconsider godo as clockwise_oriented non constant standard
special_circular_sequence by JORDAN1I:27;
len US in dom US by FINSEQ_5:6;
then A151: US.len US = US/.len US by FINSEQ_4:def 4
.= Emax by JORDAN1F:7;
A152: E-max C in E-most C by PSCOMP_1:111;
A153: east_halfline E-max C misses L~go
proof
assume east_halfline E-max C meets L~go;
then consider p be set such that
A154: p in east_halfline E-max C and
A155: p in L~go by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A154;
p in L~US by A44,A155;
then p in east_halfline E-max C /\ L~Cage(C,n) by A133,A154,XBOOLE_0:def 3
;
then A156: p`1 = Ebo by A152,JORDAN1A:104;
then A157: p = Emax by A44,A155,Th46;
then Emax = Gik by A7,A151,A155,Th43;
then Gik`1 = Ga*(len Ga,k)`1 by A10,A15,A156,A157,JORDAN1A:92;
hence contradiction by A1,A12,A28,JORDAN1G:7;
end;
now assume east_halfline E-max C meets L~godo;
then A158: east_halfline E-max C meets (L~go \/ L~pion1) or
east_halfline E-max C meets L~do by A132,XBOOLE_1:70;
per cases by A158,XBOOLE_1:70;
suppose east_halfline E-max C meets L~go;
hence contradiction by A153;
suppose east_halfline E-max C meets L~pion1;
then consider p be set such that
A159: p in east_halfline E-max C and
A160: p in L~pion1 by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A159;
A161: p`1 = Gik`1 by A73,A76,A136,A160,GOBOARD7:5;
i+1 <= len Ga by A1,NAT_1:38;
then i+1-1 <= len Ga-1 by REAL_1:49;
then A162: i <= len Ga-1 by XCMPLX_1:26;
then len Ga-1 > 0 by A1,AXIOMS:22;
then A163: i <= len Ga-'1 by A162,BINARITH:def 3;
len Ga-'1 <= len Ga by GOBOARD9:2;
then p`1 <= Ga*(len Ga-'1,1)`1 by A1,A10,A15,A19,A161,A163,JORDAN1A:39;
then p`1 <= E-bound C by A19,JORDAN8:15;
then A164: p`1 <= (E-max C)`1 by PSCOMP_1:104;
p`1 >= (E-max C)`1 by A159,JORDAN1A:def 3;
then A165: p`1 = (E-max C)`1 by A164,AXIOMS:21;
p`2 = (E-max C)`2 by A159,JORDAN1A:def 3;
then p = E-max C by A165,TOPREAL3:11;
hence contradiction by A5,A76,A120,A136,A160,XBOOLE_0:3;
suppose east_halfline E-max C meets L~do;
then consider p be set such that
A166: p in east_halfline E-max C and
A167: p in L~do by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A166;
p in L~LS by A51,A167;
then p in east_halfline E-max C /\ L~Cage(C,n) by A133,A166,XBOOLE_0:def
3;
then A168: p`1 = Ebo by A152,JORDAN1A:104;
A169: (E-max C)`2 = p`2 by A166,JORDAN1A:def 3;
set RC = Rotate(Cage(C,n),Emax);
A170: E-max C in right_cell(RC,1) by JORDAN1I:9;
A171: 1+1 <= len LS by A22,AXIOMS:22;
LS = RC-:Wmin by JORDAN1G:26;
then A172: LSeg(LS,1) = LSeg(RC,1) by A171,SPPOL_2:9;
A173: L~RC = L~Cage(C,n) by REVROT_1:33;
A174: len RC = len Cage(C,n) by REVROT_1:14;
A175: GoB RC = GoB Cage(C,n) by REVROT_1:28
.= Ga by JORDAN1H:52;
A176: Emax in rng Cage(C,n) by SPRECT_2:50;
A177: RC is_sequence_on Ga by A129,REVROT_1:34;
A178: RC/.1 = E-max L~RC by A173,A176,FINSEQ_6:98;
then consider ii,jj be Nat such that
A179: [ii,jj+1] in Indices Ga and
A180: [ii,jj] in Indices Ga and
A181: RC/.1 = Ga*(ii,jj+1) and
A182: RC/.(1+1) = Ga*(ii,jj) by A80,A174,A177,JORDAN1I:25;
consider jj2 be Nat such that
A183: 1 <= jj2 & jj2 <= width Ga and
A184: Emax = Ga*(len Ga,jj2) by JORDAN1D:29;
A185: len Ga >= 4 by JORDAN8:13;
then len Ga >= 1 by AXIOMS:22;
then [len Ga,jj2] in Indices Ga by A183,GOBOARD7:10;
then A186: ii = len Ga by A173,A178,A179,A181,A184,GOBOARD1:21;
A187: 1 <= ii & ii <= len Ga & 1 <= jj+1 & jj+1 <= width Ga
by A179,GOBOARD5:1;
A188: 1 <= ii & ii <= len Ga & 1 <= jj & jj <= width Ga
by A180,GOBOARD5:1;
A189: ii+1 <> ii by NAT_1:38;
jj+1 > jj by NAT_1:38;
then jj+1+1 <> jj by NAT_1:38;
then A190: right_cell(RC,1) = cell(Ga,ii-'1,jj)
by A80,A174,A175,A179,A180,A181,A182,A189,GOBOARD5:
def 6;
A191: ii-'1+1 = ii by A187,AMI_5:4;
A192: ii-1 >= 4-1 by A185,A186,REAL_1:49;
then A193: ii-1 >= 1 by AXIOMS:22;
ii-1 >= 0 by A192,AXIOMS:22;
then A194: 1 <= ii-'1 by A193,BINARITH:def 3;
then A195: Ga*(ii-'1,jj)`1 <= (E-max C)`1 & (E-max C)`1 <= Ga*(ii-'1+1,
jj)`1 &
Ga*(ii-'1,jj)`2 <= (E-max C)`2 & (E-max C)`2 <= Ga*(ii-'1,jj+1)`2
by A170,A187,A188,A190,A191,JORDAN9:19;
A196: ii-'1 < len Ga by A187,A191,NAT_1:38;
then A197: Ga*(ii-'1,jj)`2 = Ga*(1,jj)`2 by A188,A194,GOBOARD5:2
.= Ga*(ii,jj)`2 by A188,GOBOARD5:2;
A198: Ga*(ii-'1,jj+1)`2 = Ga*(1,jj+1)`2 by A187,A194,A196,GOBOARD5:2
.= Ga*(ii,jj+1)`2 by A187,GOBOARD5:2;
Ga*(len Ga,jj)`1 = Ebo & Ebo = Ga*(len Ga,jj+1)`1
by A15,A187,A188,JORDAN1A:92;
then p in LSeg(RC/.1,RC/.(1+1))
by A168,A169,A181,A182,A186,A195,A197,A198,
GOBOARD7:8;
then A199: p in LSeg(LS,1) by A80,A172,A174,TOPREAL1:def 5;
A200: p in LSeg(do,Index(p,do)) by A167,JORDAN3:42;
A201: do = mid(LS,Gij..LS,len LS) by A35,Th37;
A202: 1<=Gij..LS & Gij..LS<=len LS by A35,FINSEQ_4:31;
Gij..LS <> len LS by A27,A35,FINSEQ_4:29;
then A203: Gij..LS < len LS by A202,REAL_1:def 5;
A204: 1<=Index(p,do) & Index(p,do) < len do by A167,JORDAN3:41;
A205: Index(Gij,LS)+1 = Gij..LS by A30,A35,Th56;
consider t be Nat such that
A206: t in dom LS and
A207: LS.t = Gij by A35,FINSEQ_2:11;
A208: 1 <= t & t <= len LS by A206,FINSEQ_3:27;
then 1 < t by A30,A207,REAL_1:def 5;
then Index(Gij,LS)+1 = t by A207,A208,JORDAN3:45;
then A209: len L_Cut(LS,Gij) = len LS-Index(Gij,LS)
by A6,A27,A207,JORDAN3:61;
set tt = Index(p,do)+(Gij..LS)-'1;
A210: 1<=Index(Gij,LS) & 0+Index(Gij,LS) < len LS by A6,JORDAN3:41;
then A211: len LS-Index(Gij,LS) > 0 by REAL_1:86;
then Index(p,do) < len LS-'Index(Gij,LS) by A204,A209,BINARITH:def 3;
then Index(p,do)+1 <= len LS-'Index(Gij,LS) by NAT_1:38;
then Index(p,do) <= len LS-'Index(Gij,LS)-1 by REAL_1:84;
then Index(p,do) <= len LS-Index(Gij,LS)-1 by A211,BINARITH:def 3;
then A212: Index(p,do) <= len LS-Gij..LS by A205,XCMPLX_1:36;
then len LS-Gij..LS >= 1 by A204,AXIOMS:22;
then len LS-Gij..LS >= 0 by AXIOMS:22;
then Index(p,do) <= len LS-'Gij..LS by A212,BINARITH:def 3;
then Index(p,do) < len LS-'(Gij..LS)+1 by NAT_1:38;
then A213: LSeg(mid(LS,Gij..LS,len LS),Index(p,do)) =
LSeg(LS,Index(p,do)+(Gij..LS)-'1) by A202,A203,A204,JORDAN4:31;
A214: 1+1 <= Gij..LS by A205,A210,REAL_1:55;
then Index(p,do)+Gij..LS >= 1+1+1 by A204,REAL_1:55;
then A215: Index(p,do)+Gij..LS-1 >= 1+1+1-1 by REAL_1:49;
then A216: Index(p,do)+Gij..LS-1 >= 0 by AXIOMS:22;
then A217: tt >= 1+1 by A215,BINARITH:def 3;
A218: 2 in dom LS by A171,FINSEQ_3:27;
now per cases by A217,REAL_1:def 5;
suppose tt > 1+1;
then LSeg(LS,1) misses LSeg(LS,tt) by TOPREAL1:def 9;
hence contradiction by A199,A200,A201,A213,XBOOLE_0:3;
suppose A219: tt = 1+1;
then LSeg(LS,1) /\ LSeg(LS,tt) = {LS/.2} by A22,TOPREAL1:def 8;
then p in {LS/.2} by A199,A200,A201,A213,XBOOLE_0:def 3;
then A220: p = LS/.2 by TARSKI:def 1;
then A221: p..LS = 2 by A218,FINSEQ_5:44;
1+1 = Index(p,do)+(Gij..LS)-1 by A216,A219,BINARITH:def 3;
then 1+1+1 = Index(p,do)+(Gij..LS) by XCMPLX_1:27;
then A222: Gij..LS = 2 by A204,A214,JORDAN1E:10;
p in rng LS by A218,A220,PARTFUN2:4;
then p = Gij by A35,A221,A222,FINSEQ_5:10;
then Gij`1 = Ebo by A220,JORDAN1G:40;
then Gij`1 = Ga*(len Ga,j)`1 by A9,A15,JORDAN1A:92;
hence contradiction by A1,A11,A62,JORDAN1G:7;
end;
hence contradiction;
end;
then east_halfline E-max C c= (L~godo)` by SUBSET_1:43;
then consider W be Subset of TOP-REAL 2 such that
A223: W is_a_component_of (L~godo)` and
A224: east_halfline E-max C c= W by GOBOARD9:5;
east_halfline E-max C is not Bounded by JORDAN1C:9;
then W is not Bounded by A224,JORDAN2C:16;
then W is_outside_component_of L~godo by A223,JORDAN2C:def 4;
then W c= UBD L~godo by JORDAN2C:27;
then A225: east_halfline E-max C c= UBD L~godo by A224,XBOOLE_1:1;
E-max C in east_halfline E-max C by JORDAN1C:7;
then E-max C in UBD L~godo by A225;
then E-max C in LeftComp godo by GOBRD14:46;
then LA meets L~godo by A119,A120,A131,A139,Th36;
then A226: LA meets (L~go \/ L~pion1) or LA meets L~do by A132,XBOOLE_1:70;
A227: LA c= C by JORDAN1A:16;
per cases by A226,XBOOLE_1:70;
suppose LA meets L~go;
then LA meets L~Cage(C,n) by A134,XBOOLE_1:63;
then C meets L~Cage(C,n) by A227,XBOOLE_1:63;
hence contradiction by JORDAN10:5;
suppose LA meets L~pion1;
hence contradiction by A5,A76,A136;
suppose LA meets L~do;
then LA meets L~Cage(C,n) by A134,XBOOLE_1:63;
then C meets L~Cage(C,n) by A227,XBOOLE_1:63;
hence contradiction by JORDAN10:5;
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 & i < len Ga and
A2: 1 <= j & j <= k & k <= width Ga and
A3: LSeg(Gij,Gik) /\ L~US = {Gik} and
A4: LSeg(Gij,Gik) /\ L~LS = {Gij} and
A5: LSeg(Gij,Gik) misses UA;
Gij in {Gij} by TARSKI:def 1;
then A6: Gij in L~LS by A4,XBOOLE_0:def 3;
Gik in {Gik} by TARSKI:def 1;
then A7: Gik in L~US by A3,XBOOLE_0:def 3;
then A8: j <> k by A1,A2,A6,Th57;
A9: 1 <= j & j <= width Ga by A2,AXIOMS:22;
A10: 1 <= k & k <= width Ga by A2,AXIOMS:22;
A11: [i,j] in Indices Ga by A1,A9,GOBOARD7:10;
A12: [i,k] in Indices Ga by A1,A10,GOBOARD7:10;
A13: US is_sequence_on Ga by JORDAN1G:4;
A14: LS is_sequence_on Ga by JORDAN1G:5;
set go = R_Cut(US,Gik);
set do = L_Cut(LS,Gij);
A15: len Ga = width Ga by JORDAN8:def 1;
A16: len US >= 3 by JORDAN1E:19;
then len US >= 1 by AXIOMS:22;
then 1 in dom US by FINSEQ_3:27;
then A17: US.1 = US/.1 by FINSEQ_4:def 4
.= Wmin by JORDAN1F:5;
A18: Wmin`1 = Wbo by PSCOMP_1:84
.= Ga*(1,k)`1 by A10,A15,JORDAN1A:94;
len Ga >= 4 by JORDAN8:13;
then A19: len Ga >= 1 by AXIOMS:22;
then A20: [1,k] in Indices Ga by A10,GOBOARD7:10;
then A21: Gik <> US.1 by A1,A12,A17,A18,JORDAN1G:7;
then reconsider go as being_S-Seq FinSequence of TOP-REAL 2
by A7,JORDAN3:70;
A22: len LS >= 1+2 by JORDAN1E:19;
then len LS >= 1 by AXIOMS:22;
then A23: 1 in dom LS & len LS in dom LS by FINSEQ_3:27;
then A24: LS.len LS = LS/.len LS by FINSEQ_4:def 4
.= Wmin by JORDAN1F:8;
A25: Wmin`1 = Wbo by PSCOMP_1:84
.= Ga*(1,k)`1 by A10,A15,JORDAN1A:94;
A26: [i,j] in Indices Ga by A1,A9,GOBOARD7:10;
then A27: Gij <> LS.len LS by A1,A20,A24,A25,JORDAN1G:7;
then reconsider do as being_S-Seq FinSequence of TOP-REAL 2
by A6,JORDAN3:69;
A28: [len Ga,k] in Indices Ga by A10,A19,GOBOARD7:10;
A29: LS.1 = LS/.1 by A23,FINSEQ_4:def 4
.= Emax by JORDAN1F:6;
Emax`1 = Ebo by PSCOMP_1:104
.= Ga*(len Ga,k)`1 by A10,A15,JORDAN1A:92;
then A30: Gij <> LS.1 by A1,A26,A28,A29,JORDAN1G:7;
A31: len go >= 1+1 by TOPREAL1:def 10;
A32: Gik in rng US by A1,A7,A10,A13,Th40;
then A33: go is_sequence_on Ga by A13,Th38;
A34: len do >= 1+1 by TOPREAL1:def 10;
A35: Gij in rng LS by A1,A6,A9,A14,Th40;
then A36: do is_sequence_on Ga by A14,Th39;
reconsider go as non constant s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2) by A31,A33,JGRAPH_1:16,
JORDAN8:8;
reconsider do as non constant s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2) by A34,A36,JGRAPH_1:16,
JORDAN8:8;
A37: len go > 1 by A31,NAT_1:38;
then A38: len go in dom go by FINSEQ_3:27;
then A39: go/.len go = go.len go by FINSEQ_4:def 4
.= Gik by A7,JORDAN3:59;
len do >= 1 by A34,AXIOMS:22;
then 1 in dom do by FINSEQ_3:27;
then A40: do/.1 = do.1 by FINSEQ_4:def 4
.= Gij by A6,JORDAN3:58;
reconsider m = len go - 1 as Nat by A38,FINSEQ_3:28;
A41: m+1 = len go by XCMPLX_1:27;
then A42: len go-'1 = m by BINARITH:39;
A43: LSeg(go,m) c= L~go by TOPREAL3:26;
A44: L~go c= L~US by A7,JORDAN3:76;
then LSeg(go,m) c= L~US by A43,XBOOLE_1:1;
then A45: LSeg(go,m) /\ LSeg(Gik,Gij) c= {Gik} by A3,XBOOLE_1:26;
m >= 1 by A31,REAL_1:84;
then A46: LSeg(go,m) = LSeg(go/.m,Gik) by A39,A41,TOPREAL1:def 5;
{Gik} c= LSeg(go,m) /\ LSeg(Gik,Gij)
proof
let x be set;
assume x in {Gik};
then A47: x = Gik by TARSKI:def 1;
A48: Gik in LSeg(go,m) by A46,TOPREAL1:6;
Gik in LSeg(Gik,Gij) by TOPREAL1:6;
hence x in LSeg(go,m) /\ LSeg(Gik,Gij) by A47,A48,XBOOLE_0:def 3;
end;
then A49: LSeg(go,m) /\ LSeg(Gik,Gij) = {Gik} by A45,XBOOLE_0:def 10;
A50: LSeg(do,1) c= L~do by TOPREAL3:26;
A51: L~do c= L~LS by A6,JORDAN3:77;
then LSeg(do,1) c= L~LS by A50,XBOOLE_1:1;
then A52: LSeg(do,1) /\ LSeg(Gik,Gij) c= {Gij} by A4,XBOOLE_1:26;
A53: LSeg(do,1) = LSeg(Gij,do/.(1+1)) by A34,A40,TOPREAL1:def 5;
{Gij} c= LSeg(do,1) /\ LSeg(Gik,Gij)
proof
let x be set;
assume x in {Gij};
then A54: x = Gij by TARSKI:def 1;
A55: Gij in LSeg(do,1) by A53,TOPREAL1:6;
Gij in LSeg(Gik,Gij) by TOPREAL1:6;
hence x in LSeg(do,1) /\ LSeg(Gik,Gij) by A54,A55,XBOOLE_0:def 3;
end;
then A56: LSeg(Gik,Gij) /\ LSeg(do,1) = {Gij} by A52,XBOOLE_0:def 10;
A57: go/.1 = US/.1 by A7,SPRECT_3:39
.= Wmin by JORDAN1F:5;
then A58: go/.1 = LS/.len LS by JORDAN1F:8
.= do/.len do by A6,Th35;
A59: rng go c= L~go & rng do c= L~do by A31,A34,SPPOL_2:18;
A60: {go/.1} c= L~go /\ L~do
proof
let x be set;
assume x in {go/.1};
then x = go/.1 by TARSKI:def 1;
then x in rng go & x in rng do by A58,FINSEQ_6:46,REVROT_1:3;
hence x in L~go /\ L~do by A59,XBOOLE_0:def 3;
end;
A61: LS.1 = LS/.1 by A23,FINSEQ_4:def 4
.= Emax by JORDAN1F:6;
A62: [len Ga,j] in Indices Ga by A9,A19,GOBOARD7:10;
L~go /\ L~do c= {go/.1}
proof
let x be set;
assume x in L~go /\ L~do;
then A63: x in L~go & x in L~do by XBOOLE_0:def 3;
then x in L~US /\ L~LS by A44,A51,XBOOLE_0:def 3;
then x in {Wmin,Emax} by JORDAN1E:20;
then A64: x = Wmin or x = Emax by TARSKI:def 2;
now assume x = Emax;
then A65: Emax = Gij by A6,A61,A63,JORDAN1E:11;
Ga*(len Ga,j)`1 = Ebo by A9,A15,JORDAN1A:92;
then Emax`1 <> Ebo by A1,A11,A62,A65,JORDAN1G:7;
hence contradiction by PSCOMP_1:104;
end;
hence x in {go/.1} by A57,A64,TARSKI:def 1;
end;
then A66: L~go /\ L~do = {go/.1} by A60,XBOOLE_0:def 10;
set W2 = go/.2;
A67: 2 in dom go by A31,FINSEQ_3:27;
A68: Gik..US >= 1 by A32,FINSEQ_4:31;
A69: now assume Gik`1 = Wbo;
then Ga*(1,k)`1 = Ga*(i,k)`1 by A10,A15,JORDAN1A:94;
hence contradiction by A1,A12,A20,JORDAN1G:7;
end;
go = mid(US,1,Gik..US) by A32,JORDAN1G:57
.= US|(Gik..US) by A68,JORDAN3:25;
then A70: W2 = US/.2 by A67,TOPREAL1:1;
set pion = <*Gik,Gij*>;
A71: now let n be Nat;
assume n in dom pion;
then n in Seg 2 by FINSEQ_3:29;
then n = 1 or n = 2 by FINSEQ_1:4,TARSKI:def 2;
then pion/.n = Gik or pion/.n = Gij by FINSEQ_4:26;
hence ex i,j be Nat st [i,j] in Indices Ga & pion/.n = Ga*(i,j)
by A11,A12;
end;
A72: Gik <> Gij by A8,A11,A12,GOBOARD1:21;
A73: Gik`1 = Ga*(i,1)`1 by A1,A10,GOBOARD5:3
.= Gij`1 by A1,A9,GOBOARD5:3;
then LSeg(Gik,Gij) is vertical by SPPOL_1:37;
then pion is_S-Seq by A72,JORDAN1B:8;
then consider pion1 be FinSequence of TOP-REAL 2 such that
A74: pion1 is_sequence_on Ga and
A75: pion1 is_S-Seq and
A76: L~pion = L~pion1 and
A77: pion/.1 = pion1/.1 and
A78: pion/.len pion = pion1/.len pion1 and
A79: len pion <= len pion1 by A71,GOBOARD3:2;
reconsider pion1 as being_S-Seq FinSequence of TOP-REAL 2 by A75;
set godo = go^'pion1^'do;
len Cage(C,n) > 4 by GOBOARD7:36;
then A80: 1+1 <= len Cage(C,n) by AXIOMS:22;
then A81: 1+1 <= len Rotate(Cage(C,n),Wmin) by REVROT_1:14;
len (go^'pion1) >= len go by TOPREAL8:7;
then A82: len (go^'pion1) >= 1+1 by A31,AXIOMS:22;
then A83: len (go^'pion1) > 1+0 by NAT_1:38;
len godo >= len (go^'pion1) by TOPREAL8:7;
then A84: 1+1 <= len godo by A82,AXIOMS:22;
A85: US is_sequence_on Ga by JORDAN1G:4;
A86: go/.len go = pion1/.1 by A39,A77,FINSEQ_4:26;
then A87: go^'pion1 is_sequence_on Ga by A33,A74,TOPREAL8:12;
A88: (go^'pion1)/.len (go^'pion1) = pion/.len pion by A78,AMISTD_1:6
.= pion/.2 by FINSEQ_1:61
.= do/.1 by A40,FINSEQ_4:26;
then A89: godo is_sequence_on Ga by A36,A87,TOPREAL8:12;
LSeg(pion1,1) c= L~<*Gik,Gij*> by A76,TOPREAL3:26;
then LSeg(pion1,1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then A90: LSeg(go,len go-'1) /\ LSeg(pion1,1) c= {Gik} by A42,A49,XBOOLE_1:
27;
A91: len pion1 >= 1+1 by A79,FINSEQ_1:61;
{Gik} c= LSeg(go,m) /\ LSeg(pion1,1)
proof
let x be set;
assume x in {Gik};
then A92: x = Gik by TARSKI:def 1;
A93: Gik in LSeg(go,m) by A46,TOPREAL1:6;
Gik in LSeg(pion1,1) by A39,A86,A91,TOPREAL1:27;
hence x in LSeg(go,m) /\ LSeg(pion1,1) by A92,A93,XBOOLE_0:def 3;
end;
then LSeg(go,len go-'1) /\ LSeg(pion1,1) = { go/.len go }
by A39,A42,A90,XBOOLE_0:def 10;
then A94: go^'pion1 is unfolded by A86,TOPREAL8:34;
len pion1 >= 2+0 by A79,FINSEQ_1:61;
then A95: len pion1-2 >= 0 by REAL_1:84;
A96: len (go^'pion1)-1 >= 0 by A83,REAL_1:84;
len (go^'pion1)+1-1 = len go+len pion1-1 by GRAPH_2:13;
then len (go^'pion1)-1 = len go+len pion1-1-1 by XCMPLX_1:26
.= len go + len pion1-(1+1) by XCMPLX_1:36
.= len go + (len pion1-2) by XCMPLX_1:29
.= len go + (len pion1-'2) by A95,BINARITH:def 3;
then A97: len (go^'pion1)-'1 = len go + (len pion1-'2)
by A96,BINARITH:def 3;
A98: len pion1-1 >= 1 by A91,REAL_1:84;
then A99: len pion1-1 >= 0 by AXIOMS:22;
then A100: len pion1-'1 = len pion1-1 by BINARITH:def 3;
A101: len pion1-'2+1 = len pion1-2+1 by A95,BINARITH:def 3
.= len pion1-(2-1) by XCMPLX_1:37
.= len pion1-'1 by A99,BINARITH:def 3;
len pion1-1+1 <= len pion1 by XCMPLX_1:27;
then A102: len pion1-'1 < len pion1 by A100,NAT_1:38;
LSeg(pion1,len pion1-'1) c= L~<*Gik,Gij*> by A76,TOPREAL3:26;
then LSeg(pion1,len pion1-'1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then A103: LSeg(pion1,len pion1-'1) /\ LSeg(do,1) c= {Gij} by A56,XBOOLE_1:
27;
{Gij} c= LSeg(pion1,len pion1-'1) /\ LSeg(do,1)
proof
let x be set;
assume x in {Gij};
then A104: x = Gij by TARSKI:def 1;
A105: Gij in LSeg(do,1) by A53,TOPREAL1:6;
A106: len pion1-'1+1 = len pion1 by A100,XCMPLX_1:27;
then pion1/.(len pion1-'1+1) = pion/.2 by A78,FINSEQ_1:61
.= Gij by FINSEQ_4:26;
then Gij in LSeg(pion1,len pion1-'1) by A98,A100,A106,TOPREAL1:27;
hence x in LSeg(pion1,len pion1-'1) /\ LSeg(do,1) by A104,A105,XBOOLE_0:
def 3;
end;
then LSeg(pion1,len pion1-'1) /\ LSeg(do,1) = {Gij} by A103,XBOOLE_0:def 10
;
then A107: LSeg(go^'pion1,len go+(len pion1-'2)) /\ LSeg(do,1) =
{(go^'pion1)/.len (go^'pion1)} by A40,A86,A88,A101,A102,TOPREAL8:31;
A108: (go^'pion1) is non trivial by A82,SPPOL_1:2;
A109: rng pion1 c= L~pion1 by A91,SPPOL_2:18;
A110: {pion1/.1} c= L~go /\ L~pion1
proof
let x be set;
assume x in {pion1/.1};
then x = pion1/.1 by TARSKI:def 1;
then x in rng go & x in rng pion1 by A86,FINSEQ_6:46,REVROT_1:3;
hence x in L~go /\ L~pion1 by A59,A109,XBOOLE_0:def 3;
end;
L~go /\ L~pion1 c= {pion1/.1}
proof
let x be set;
assume x in L~go /\ L~pion1;
then x in L~go & x in L~pion1 by XBOOLE_0:def 3;
then x in L~pion1 /\ L~US by A44,XBOOLE_0:def 3;
hence x in {pion1/.1} by A3,A39,A76,A86,SPPOL_2:21;
end;
then A111: L~go /\ L~pion1 = {pion1/.1} by A110,XBOOLE_0:def 10;
then A112: (go^'pion1) is s.n.c. by A86,Th54;
rng go /\ rng pion1 c= {pion1/.1} by A59,A109,A111,XBOOLE_1:27;
then A113: go^'pion1 is one-to-one by Th55;
A114: pion/.len pion = pion/.2 by FINSEQ_1:61
.= do/.1 by A40,FINSEQ_4:26;
A115: {pion1/.len pion1} c= L~do /\ L~pion1
proof
let x be set;
assume x in {pion1/.len pion1};
then x = pion1/.len pion1 by TARSKI:def 1;
then x in rng do & x in rng pion1 by A78,A114,FINSEQ_6:46,REVROT_1:3;
hence x in L~do /\ L~pion1 by A59,A109,XBOOLE_0:def 3;
end;
L~do /\ L~pion1 c= {pion1/.len pion1}
proof
let x be set;
assume x in L~do /\ L~pion1;
then x in L~do & x in L~pion1 by XBOOLE_0:def 3;
then x in L~pion1 /\ L~LS by A51,XBOOLE_0:def 3;
hence x in {pion1/.len pion1} by A4,A40,A76,A78,A114,SPPOL_2:21;
end;
then A116: L~do /\ L~pion1 = {pion1/.len pion1} by A115,XBOOLE_0:def 10;
A117: L~(go^'pion1) /\ L~do = (L~go \/ L~pion1) /\ L~do by A86,TOPREAL8:35
.= {go/.1} \/ {do/.1} by A66,A78,A114,A116,XBOOLE_1:23
.= {(go^'pion1)/.1} \/ {do/.1} by AMISTD_1:5
.= {(go^'pion1)/.1,do/.1} by ENUMSET1:41;
do/.len do = (go^'pion1)/.1 by A58,AMISTD_1:5;
then reconsider godo as non constant standard special_circular_sequence
by A84,A88,A89,A94,A97,A107,A108,
A112,A113,A117,JORDAN8:7,8,TOPREAL8:11,33,34;
A118: UA is_an_arc_of W-min C,E-max C by JORDAN6:def 8;
then A119: UA is connected by JORDAN6:11;
A120: W-min C in UA & E-max C in UA by A118,TOPREAL1:4;
set ff = Rotate(Cage(C,n),Wmin);
Wmin in rng Cage(C,n) by SPRECT_2:47;
then A121: ff/.1 = Wmin by FINSEQ_6:98;
A122: L~ff = L~Cage(C,n) by REVROT_1:33;
then A123: (W-max L~ff)..ff > 1 by A121,SPRECT_5:23;
(W-max L~ff)..ff <= (N-min L~ff)..ff by A121,A122,SPRECT_5:24;
then A124: (N-min L~ff)..ff > 1 by A123,AXIOMS:22;
(N-min L~ff)..ff < (N-max L~ff)..ff by A121,A122,SPRECT_5:25;
then A125: (N-max L~ff)..ff > 1 by A124,AXIOMS:22;
(N-max L~ff)..ff <= (E-max L~ff)..ff by A121,A122,SPRECT_5:26;
then A126: Emax..ff > 1 by A122,A125,AXIOMS:22;
A127: now assume A128: Gik..US <= 1;
Gik..US >= 1 by A32,FINSEQ_4:31;
then Gik..US = 1 by A128,AXIOMS:21;
then Gik = US/.1 by A32,FINSEQ_5:41;
hence contradiction by A17,A21,JORDAN1F:5;
end;
A129: Cage(C,n) is_sequence_on Ga by JORDAN9:def 1;
then A130: ff is_sequence_on Ga by REVROT_1:34;
A131: right_cell(godo,1,Ga)\L~godo c= RightComp godo by A84,A89,JORDAN9:29;
A132: L~godo = L~(go^'pion1) \/ L~do by A88,TOPREAL8:35
.= L~go \/ L~pion1 \/ L~do by A86,TOPREAL8:35;
L~Cage(C,n) = L~US \/ L~LS by JORDAN1E:17;
then A133: L~US c= L~Cage(C,n) & L~LS c= L~Cage(C,n) by XBOOLE_1:7;
then A134: L~go c= L~Cage(C,n) & L~do c= L~Cage(C,n) by A44,A51,XBOOLE_1:1;
A135: W-min C in C by SPRECT_1:15;
A136: L~pion = LSeg(Gik,Gij) by SPPOL_2:21;
A137: now assume W-min C in L~godo;
then A138: W-min C in L~go \/ L~pion1 or W-min C in L~do by A132,XBOOLE_0:
def 2;
per cases by A138,XBOOLE_0:def 2;
suppose W-min C in L~go;
then C meets L~Cage(C,n) by A134,A135,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
suppose W-min C in L~pion1;
hence contradiction by A5,A76,A120,A136,XBOOLE_0:3;
suppose W-min C in L~do;
then C meets L~Cage(C,n) by A134,A135,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
end;
right_cell(Rotate(Cage(C,n),Wmin),1) =
right_cell(ff,1,GoB ff) by A81,JORDAN1H:29
.= right_cell(ff,1,GoB Cage(C,n)) by REVROT_1:28
.= right_cell(ff,1,Ga) by JORDAN1H:52
.= right_cell(ff-:Emax,1,Ga) by A126,A130,Th53
.= right_cell(US,1,Ga) by JORDAN1E:def 1
.= right_cell(R_Cut(US,Gik),1,Ga) by A32,A85,A127,Th52
.= right_cell(go^'pion1,1,Ga) by A37,A87,Th51
.= right_cell(godo,1,Ga) by A83,A89,Th51;
then W-min C in right_cell(godo,1,Ga) by JORDAN1I:8;
then A139: W-min C in right_cell(godo,1,Ga)\L~godo by A137,XBOOLE_0:def 4;
A140: godo/.1 = (go^'pion1)/.1 by AMISTD_1:5
.= Wmin by A57,AMISTD_1:5;
A141: len US >= 2 by A16,AXIOMS:22;
A142: godo/.2 = (go^'pion1)/.2 by A82,AMISTD_1:9
.= US/.2 by A31,A70,AMISTD_1:9
.= (US^'LS)/.2 by A141,AMISTD_1:9
.= Rotate(Cage(C,n),Wmin)/.2 by JORDAN1E:15;
A143: L~go \/ L~do is compact by COMPTS_1:19;
A144: L~go \/ L~do c= L~Cage(C,n) by A134,XBOOLE_1:8;
Wmin in rng go by A57,FINSEQ_6:46;
then Wmin in L~go \/ L~do by A59,XBOOLE_0:def 2;
then A145: W-min (L~go \/ L~do) = Wmin by A143,A144,Th21;
A146: (W-min (L~go \/ L~do))`1 = W-bound (L~go \/ L~do) & Wmin`1 = Wbo
by PSCOMP_1:84;
W-bound LSeg(Gik,Gij) = Gik`1 by A73,SPRECT_1:62;
then A147: W-bound L~pion1 = Gik`1 by A76,SPPOL_2:21;
Gik`1 >= Wbo by A7,A133,PSCOMP_1:71;
then Gik`1 > Wbo by A69,REAL_1:def 5;
then W-min (L~go\/L~do\/L~pion1) = W-min (L~go \/ L~do)
by A143,A145,A146,A147,Th33;
then A148: W-min L~godo = Wmin by A132,A145,XBOOLE_1:4;
A149: rng godo c= L~godo by A84,SPPOL_2:18;
2 in dom godo by A84,FINSEQ_3:27;
then A150: godo/.2 in rng godo by PARTFUN2:4;
godo/.2 in W-most L~Cage(C,n) by A142,JORDAN1I:27;
then (godo/.2)`1 = (W-min L~godo)`1 by A148,PSCOMP_1:88
.= W-bound L~godo by PSCOMP_1:84;
then godo/.2 in W-most L~godo by A149,A150,SPRECT_2:16;
then Rotate(godo,W-min L~godo)/.2 in W-most L~godo by A140,A148,FINSEQ_6:95
;
then reconsider godo as clockwise_oriented non constant standard
special_circular_sequence by JORDAN1I:27;
len US in dom US by FINSEQ_5:6;
then A151: US.len US = US/.len US by FINSEQ_4:def 4
.= Emax by JORDAN1F:7;
A152: E-max C in E-most C by PSCOMP_1:111;
A153: east_halfline E-max C misses L~go
proof
assume east_halfline E-max C meets L~go;
then consider p be set such that
A154: p in east_halfline E-max C and
A155: p in L~go by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A154;
p in L~US by A44,A155;
then p in east_halfline E-max C /\ L~Cage(C,n) by A133,A154,XBOOLE_0:def 3
;
then A156: p`1 = Ebo by A152,JORDAN1A:104;
then A157: p = Emax by A44,A155,Th46;
then Emax = Gik by A7,A151,A155,Th43;
then Gik`1 = Ga*(len Ga,k)`1 by A10,A15,A156,A157,JORDAN1A:92;
hence contradiction by A1,A12,A28,JORDAN1G:7;
end;
now assume east_halfline E-max C meets L~godo;
then A158: east_halfline E-max C meets (L~go \/ L~pion1) or
east_halfline E-max C meets L~do by A132,XBOOLE_1:70;
per cases by A158,XBOOLE_1:70;
suppose east_halfline E-max C meets L~go;
hence contradiction by A153;
suppose east_halfline E-max C meets L~pion1;
then consider p be set such that
A159: p in east_halfline E-max C and
A160: p in L~pion1 by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A159;
A161: p`1 = Gik`1 by A73,A76,A136,A160,GOBOARD7:5;
i+1 <= len Ga by A1,NAT_1:38;
then i+1-1 <= len Ga-1 by REAL_1:49;
then A162: i <= len Ga-1 by XCMPLX_1:26;
then len Ga-1 > 0 by A1,AXIOMS:22;
then A163: i <= len Ga-'1 by A162,BINARITH:def 3;
len Ga-'1 <= len Ga by GOBOARD9:2;
then p`1 <= Ga*(len Ga-'1,1)`1 by A1,A10,A15,A19,A161,A163,JORDAN1A:39;
then p`1 <= E-bound C by A19,JORDAN8:15;
then A164: p`1 <= (E-max C)`1 by PSCOMP_1:104;
p`1 >= (E-max C)`1 by A159,JORDAN1A:def 3;
then A165: p`1 = (E-max C)`1 by A164,AXIOMS:21;
p`2 = (E-max C)`2 by A159,JORDAN1A:def 3;
then p = E-max C by A165,TOPREAL3:11;
hence contradiction by A5,A76,A120,A136,A160,XBOOLE_0:3;
suppose east_halfline E-max C meets L~do;
then consider p be set such that
A166: p in east_halfline E-max C and
A167: p in L~do by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A166;
p in L~LS by A51,A167;
then p in east_halfline E-max C /\ L~Cage(C,n) by A133,A166,XBOOLE_0:def
3;
then A168: p`1 = Ebo by A152,JORDAN1A:104;
A169: (E-max C)`2 = p`2 by A166,JORDAN1A:def 3;
set RC = Rotate(Cage(C,n),Emax);
A170: E-max C in right_cell(RC,1) by JORDAN1I:9;
A171: 1+1 <= len LS by A22,AXIOMS:22;
LS = RC-:Wmin by JORDAN1G:26;
then A172: LSeg(LS,1) = LSeg(RC,1) by A171,SPPOL_2:9;
A173: L~RC = L~Cage(C,n) by REVROT_1:33;
A174: len RC = len Cage(C,n) by REVROT_1:14;
A175: GoB RC = GoB Cage(C,n) by REVROT_1:28
.= Ga by JORDAN1H:52;
A176: Emax in rng Cage(C,n) by SPRECT_2:50;
A177: RC is_sequence_on Ga by A129,REVROT_1:34;
A178: RC/.1 = E-max L~RC by A173,A176,FINSEQ_6:98;
then consider ii,jj be Nat such that
A179: [ii,jj+1] in Indices Ga and
A180: [ii,jj] in Indices Ga and
A181: RC/.1 = Ga*(ii,jj+1) and
A182: RC/.(1+1) = Ga*(ii,jj) by A80,A174,A177,JORDAN1I:25;
consider jj2 be Nat such that
A183: 1 <= jj2 & jj2 <= width Ga and
A184: Emax = Ga*(len Ga,jj2) by JORDAN1D:29;
A185: len Ga >= 4 by JORDAN8:13;
then len Ga >= 1 by AXIOMS:22;
then [len Ga,jj2] in Indices Ga by A183,GOBOARD7:10;
then A186: ii = len Ga by A173,A178,A179,A181,A184,GOBOARD1:21;
A187: 1 <= ii & ii <= len Ga & 1 <= jj+1 & jj+1 <= width Ga
by A179,GOBOARD5:1;
A188: 1 <= ii & ii <= len Ga & 1 <= jj & jj <= width Ga
by A180,GOBOARD5:1;
A189: ii+1 <> ii by NAT_1:38;
jj+1 > jj by NAT_1:38;
then jj+1+1 <> jj by NAT_1:38;
then A190: right_cell(RC,1) = cell(Ga,ii-'1,jj)
by A80,A174,A175,A179,A180,A181,A182,A189,GOBOARD5:
def 6;
A191: ii-'1+1 = ii by A187,AMI_5:4;
A192: ii-1 >= 4-1 by A185,A186,REAL_1:49;
then A193: ii-1 >= 1 by AXIOMS:22;
ii-1 >= 0 by A192,AXIOMS:22;
then A194: 1 <= ii-'1 by A193,BINARITH:def 3;
then A195: Ga*(ii-'1,jj)`1 <= (E-max C)`1 & (E-max C)`1 <= Ga*(ii-'1+1,
jj)`1 &
Ga*(ii-'1,jj)`2 <= (E-max C)`2 & (E-max C)`2 <= Ga*(ii-'1,jj+1)`2
by A170,A187,A188,A190,A191,JORDAN9:19;
A196: ii-'1 < len Ga by A187,A191,NAT_1:38;
then A197: Ga*(ii-'1,jj)`2 = Ga*(1,jj)`2 by A188,A194,GOBOARD5:2
.= Ga*(ii,jj)`2 by A188,GOBOARD5:2;
A198: Ga*(ii-'1,jj+1)`2 = Ga*(1,jj+1)`2 by A187,A194,A196,GOBOARD5:2
.= Ga*(ii,jj+1)`2 by A187,GOBOARD5:2;
Ga*(len Ga,jj)`1 = Ebo & Ebo = Ga*(len Ga,jj+1)`1
by A15,A187,A188,JORDAN1A:92;
then p in LSeg(RC/.1,RC/.(1+1))
by A168,A169,A181,A182,A186,A195,A197,A198,
GOBOARD7:8;
then A199: p in LSeg(LS,1) by A80,A172,A174,TOPREAL1:def 5;
A200: p in LSeg(do,Index(p,do)) by A167,JORDAN3:42;
A201: do = mid(LS,Gij..LS,len LS) by A35,Th37;
A202: 1<=Gij..LS & Gij..LS<=len LS by A35,FINSEQ_4:31;
Gij..LS <> len LS by A27,A35,FINSEQ_4:29;
then A203: Gij..LS < len LS by A202,REAL_1:def 5;
A204: 1<=Index(p,do) & Index(p,do) < len do by A167,JORDAN3:41;
A205: Index(Gij,LS)+1 = Gij..LS by A30,A35,Th56;
consider t be Nat such that
A206: t in dom LS and
A207: LS.t = Gij by A35,FINSEQ_2:11;
A208: 1 <= t & t <= len LS by A206,FINSEQ_3:27;
then 1 < t by A30,A207,REAL_1:def 5;
then Index(Gij,LS)+1 = t by A207,A208,JORDAN3:45;
then A209: len L_Cut(LS,Gij) = len LS-Index(Gij,LS)
by A6,A27,A207,JORDAN3:61;
set tt = Index(p,do)+(Gij..LS)-'1;
A210: 1<=Index(Gij,LS) & 0+Index(Gij,LS) < len LS by A6,JORDAN3:41;
then A211: len LS-Index(Gij,LS) > 0 by REAL_1:86;
then Index(p,do) < len LS-'Index(Gij,LS) by A204,A209,BINARITH:def 3;
then Index(p,do)+1 <= len LS-'Index(Gij,LS) by NAT_1:38;
then Index(p,do) <= len LS-'Index(Gij,LS)-1 by REAL_1:84;
then Index(p,do) <= len LS-Index(Gij,LS)-1 by A211,BINARITH:def 3;
then A212: Index(p,do) <= len LS-Gij..LS by A205,XCMPLX_1:36;
then len LS-Gij..LS >= 1 by A204,AXIOMS:22;
then len LS-Gij..LS >= 0 by AXIOMS:22;
then Index(p,do) <= len LS-'Gij..LS by A212,BINARITH:def 3;
then Index(p,do) < len LS-'(Gij..LS)+1 by NAT_1:38;
then A213: LSeg(mid(LS,Gij..LS,len LS),Index(p,do)) =
LSeg(LS,Index(p,do)+(Gij..LS)-'1) by A202,A203,A204,JORDAN4:31;
A214: 1+1 <= Gij..LS by A205,A210,REAL_1:55;
then Index(p,do)+Gij..LS >= 1+1+1 by A204,REAL_1:55;
then A215: Index(p,do)+Gij..LS-1 >= 1+1+1-1 by REAL_1:49;
then A216: Index(p,do)+Gij..LS-1 >= 0 by AXIOMS:22;
then A217: tt >= 1+1 by A215,BINARITH:def 3;
A218: 2 in dom LS by A171,FINSEQ_3:27;
now per cases by A217,REAL_1:def 5;
suppose tt > 1+1;
then LSeg(LS,1) misses LSeg(LS,tt) by TOPREAL1:def 9;
hence contradiction by A199,A200,A201,A213,XBOOLE_0:3;
suppose A219: tt = 1+1;
then LSeg(LS,1) /\ LSeg(LS,tt) = {LS/.2} by A22,TOPREAL1:def 8;
then p in {LS/.2} by A199,A200,A201,A213,XBOOLE_0:def 3;
then A220: p = LS/.2 by TARSKI:def 1;
then A221: p..LS = 2 by A218,FINSEQ_5:44;
1+1 = Index(p,do)+(Gij..LS)-1 by A216,A219,BINARITH:def 3;
then 1+1+1 = Index(p,do)+(Gij..LS) by XCMPLX_1:27;
then A222: Gij..LS = 2 by A204,A214,JORDAN1E:10;
p in rng LS by A218,A220,PARTFUN2:4;
then p = Gij by A35,A221,A222,FINSEQ_5:10;
then Gij`1 = Ebo by A220,JORDAN1G:40;
then Gij`1 = Ga*(len Ga,j)`1 by A9,A15,JORDAN1A:92;
hence contradiction by A1,A11,A62,JORDAN1G:7;
end;
hence contradiction;
end;
then east_halfline E-max C c= (L~godo)` by SUBSET_1:43;
then consider W be Subset of TOP-REAL 2 such that
A223: W is_a_component_of (L~godo)` and
A224: east_halfline E-max C c= W by GOBOARD9:5;
east_halfline E-max C is not Bounded by JORDAN1C:9;
then W is not Bounded by A224,JORDAN2C:16;
then W is_outside_component_of L~godo by A223,JORDAN2C:def 4;
then W c= UBD L~godo by JORDAN2C:27;
then A225: east_halfline E-max C c= UBD L~godo by A224,XBOOLE_1:1;
E-max C in east_halfline E-max C by JORDAN1C:7;
then E-max C in UBD L~godo by A225;
then E-max C in LeftComp godo by GOBRD14:46;
then UA meets L~godo by A119,A120,A131,A139,Th36;
then A226: UA meets (L~go \/ L~pion1) or UA meets L~do by A132,XBOOLE_1:70;
A227: UA c= C by JORDAN1A:16;
per cases by A226,XBOOLE_1:70;
suppose UA meets L~go;
then UA meets L~Cage(C,n) by A134,XBOOLE_1:63;
then C meets L~Cage(C,n) by A227,XBOOLE_1:63;
hence contradiction by JORDAN10:5;
suppose UA meets L~pion1;
hence contradiction by A5,A76,A136;
suppose UA meets L~do;
then UA meets L~Cage(C,n) by A134,XBOOLE_1:63;
then C meets L~Cage(C,n) by A227,XBOOLE_1:63;
hence contradiction by JORDAN10:5;
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 & i < len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: n > 0 and
A4: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,k)} and
A5: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,j)};
A6: L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) by A3,JORDAN1G:63;
L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) by A3,JORDAN1G:64;
hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C
by A1,A2,A4,A5,A6,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 & i < len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: n > 0 and
A4: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,k)} and
A5: LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,j)};
A6: L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) by A3,JORDAN1G:63;
L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) by A3,JORDAN1G:64;
hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C
by A1,A2,A4,A5,A6,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 & j <= width Gauge(C,n+1);
set in1 = Center Gauge(C,n+1);
A3: n+1 >= 0+1 by NAT_1:29;
then A4: n+1 > 0 by NAT_1:38;
A5: 1 <= in1 by JORDAN1B:12;
A6: in1 <= len Gauge(C,n+1) by JORDAN1B:14;
A7: LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),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:66;
Upper_Arc L~Cage(C,n+1) c= L~Cage(C,n+1) by JORDAN1A:16;
then LSeg(Gauge(C,n+1)*(in1,1),Gauge(C,n+1)*(in1,j))
meets Lower_Arc L~Cage(C,n+1) by A1,A2,A4,A5,A6,JORDAN1G:65;
hence thesis by A7,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 & j <= k & k <= width Gauge(C,n+1) and
A2: 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
A3: 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)};
n+1 >= 0+1 by NAT_1:29;
then A4: n+1 > 0 by NAT_1:38;
A5: len Gauge(C,n+1) >= 4 by JORDAN8:13;
then A6: len Gauge(C,n+1) >= 3 by AXIOMS:22;
len Gauge(C,n+1) >= 2 by A5,AXIOMS:22;
then A7: 1 < Center Gauge(C,n+1) by JORDAN1B:15;
Center Gauge(C,n+1) < len Gauge(C,n+1) by A6,JORDAN1B:16;
hence 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
by A1,A2,A3,A4,A7,Th60;
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 & j <= k & k <= width Gauge(C,n+1) and
A2: 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
A3: 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)};
n+1 >= 0+1 by NAT_1:29;
then A4: n+1 > 0 by NAT_1:38;
A5: len Gauge(C,n+1) >= 4 by JORDAN8:13;
then A6: len Gauge(C,n+1) >= 3 by AXIOMS:22;
len Gauge(C,n+1) >= 2 by A5,AXIOMS:22;
then A7: 1 < Center Gauge(C,n+1) by JORDAN1B:15;
Center Gauge(C,n+1) < len Gauge(C,n+1) by A6,JORDAN1B:16;
hence 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
by A1,A2,A3,A4,A7,Th61;
end;