Copyright (c) 2001 Association of Mizar Users
environ
vocabulary EUCLID, COMPTS_1, PSCOMP_1, ORDINAL2, FUNCT_5, REALSET1, FINSEQ_1,
SPRECT_2, RELAT_1, FINSEQ_5, FINSEQ_4, ARYTM_1, PRE_TOPC, TOPREAL1,
JORDAN3, BOOLE, GROUP_2, FUNCT_1, SPPOL_1, FINSEQ_6, JORDAN9, GRAPH_2,
TOPREAL2, CARD_1, RELAT_2, MCART_1, GOBOARD1, JORDAN8, MATRIX_1, TREES_1,
JORDAN1E;
notation TARSKI, XBOOLE_0, ENUMSET1, XCMPLX_0, XREAL_0, NAT_1, FUNCT_1,
FINSEQ_1, FINSEQ_4, FINSEQ_5, MATRIX_1, FINSEQ_6, STRUCT_0, GRAPH_2,
PRE_TOPC, TOPREAL2, CARD_1, BINARITH, CONNSP_1, COMPTS_1, EUCLID,
PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, SPPOL_1, JORDAN3, JORDAN8,
JORDAN9;
constructors JORDAN8, REALSET1, REAL_1, CARD_4, PSCOMP_1, BINARITH, CONNSP_1,
JORDAN9, FINSEQ_4, GOBRD13, JORDAN3, TOPREAL2, FINSEQ_5, ENUMSET1,
FINSOP_1, GRAPH_2, PARTFUN1;
clusters XREAL_0, SPRECT_1, TOPREAL6, JORDAN8, REVROT_1, RELSET_1, ARYTM_3,
PSCOMP_1, SPRECT_3, FINSEQ_5, SPPOL_2, JORDAN1A, GOBOARD4, JORDAN1B,
MEMBERED;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, TOPREAL1, SPRECT_2, XBOOLE_0;
theorems AXIOMS, BINARITH, JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, REAL_1,
GOBOARD5, REAL_2, FINSEQ_1, FINSEQ_2, SPRECT_2, FINSEQ_4, FINSEQ_5,
FINSEQ_6, GOBOARD7, SPPOL_2, REVROT_1, TOPREAL1, SPRECT_3, JORDAN5B,
AMI_5, JORDAN3, JORDAN9, GOBOARD1, TARSKI, FINSEQ_3, FUNCT_1, TOPREAL5,
JORDAN10, GRAPH_2, CARD_1, CARD_2, YELLOW_6, PRE_CIRC, ENUMSET1,
JORDAN1B, SPRECT_5, SCMFSA_7, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
begin :: Preliminaries
reserve n for Nat;
theorem
for X be non empty Subset of TOP-REAL 2
for Y be compact Subset of TOP-REAL 2 st X c= Y holds
N-bound X <= N-bound Y
proof
let X be non empty Subset of TOP-REAL 2;
let Y be compact Subset of TOP-REAL 2;
assume X c= Y;
then sup (proj2||X) <= sup (proj2||Y) by PSCOMP_1:63;
then sup (proj2||X) <= N-bound Y by PSCOMP_1:def 31;
hence N-bound X <= N-bound Y by PSCOMP_1:def 31;
end;
theorem
for X be non empty Subset of TOP-REAL 2
for Y be compact Subset of TOP-REAL 2 st X c= Y holds
E-bound X <= E-bound Y
proof
let X be non empty Subset of TOP-REAL 2;
let Y be compact Subset of TOP-REAL 2;
assume X c= Y;
then sup (proj1||X) <= sup (proj1||Y) by PSCOMP_1:63;
then sup (proj1||X) <= E-bound Y by PSCOMP_1:def 32;
hence E-bound X <= E-bound Y by PSCOMP_1:def 32;
end;
theorem
for X be non empty Subset of TOP-REAL 2
for Y be compact Subset of TOP-REAL 2 st X c= Y holds
S-bound X >= S-bound Y
proof
let X be non empty Subset of TOP-REAL 2;
let Y be compact Subset of TOP-REAL 2;
assume X c= Y;
then inf (proj2||X) >= inf (proj2||Y) by PSCOMP_1:62;
then inf (proj2||X) >= S-bound Y by PSCOMP_1:def 33;
hence S-bound X >= S-bound Y by PSCOMP_1:def 33;
end;
theorem
for X be non empty Subset of TOP-REAL 2
for Y be compact Subset of TOP-REAL 2 st X c= Y holds
W-bound X >= W-bound Y
proof
let X be non empty Subset of TOP-REAL 2;
let Y be compact Subset of TOP-REAL 2;
assume X c= Y;
then inf (proj1||X) >= inf (proj1||Y) by PSCOMP_1:62;
then inf (proj1||X) >= W-bound Y by PSCOMP_1:def 30;
hence W-bound X >= W-bound Y by PSCOMP_1:def 30;
end;
theorem Th5:
for f,g be FinSequence of TOP-REAL 2 st f is_in_the_area_of g
for p be Element of TOP-REAL 2 st p in rng f holds
f-:p is_in_the_area_of g
proof
let f,g be FinSequence of TOP-REAL 2;
assume A1: f is_in_the_area_of g;
let p be Element of TOP-REAL 2;
assume A2: p in rng f;
let n be Nat;
assume A3: n in dom(f-:p);
A4: p..f <= len f by A2,FINSEQ_4:31;
A5: len(f-:p) = p..f by A2,FINSEQ_5:45;
then n in Seg(p..f) by A3,FINSEQ_1:def 3;
then A6: (f-:p)/.n = f/.n by A2,FINSEQ_5:46;
n in Seg len(f-:p) by A3,FINSEQ_1:def 3;
then 1 <= n & n <= p..f by A5,FINSEQ_1:3;
then 1 <= n & n <= len f by A4,AXIOMS:22;
then n in dom f by FINSEQ_3:27;
hence thesis by A1,A6,SPRECT_2:def 1;
end;
theorem Th6:
for f,g be FinSequence of TOP-REAL 2 st f is_in_the_area_of g
for p be Element of TOP-REAL 2 st p in rng f holds
f:-p is_in_the_area_of g
proof
let f,g be FinSequence of TOP-REAL 2;
assume A1: f is_in_the_area_of g;
let p be Element of TOP-REAL 2;
assume A2: p in rng f;
let n be Nat;
assume A3: n in dom(f:-p);
A4: len(f:-p) = len f - p..f + 1 by A2,FINSEQ_5:53;
n in Seg len(f:-p) by A3,FINSEQ_1:def 3;
then A5: 0+1 <= n & n <= len f - p..f + 1 by A4,FINSEQ_1:3;
A6: n-'1 >= 0 by NAT_1:18;
1 <= p..f by A2,FINSEQ_4:31;
then A7: 0+1 <= n-'1+p..f by A6,REAL_1:55;
A8: n-1 >= 0 by A5,REAL_1:84;
n - 1 <= len f - p..f by A5,REAL_1:86;
then n - 1 + p..f <= len f by REAL_1:84;
then n-'1+p..f <= len f by A8,BINARITH:def 3;
then A9: n-'1+p..f in dom f by A7,FINSEQ_3:27;
n-'1+1 = n by A5,AMI_5:4;
then (f:-p)/.n = f/.(n-'1+p..f) by A2,A3,FINSEQ_5:55;
hence thesis by A1,A9,SPRECT_2:def 1;
end;
theorem
for f be non empty FinSequence of TOP-REAL 2
for p be Point of TOP-REAL 2 st p in L~f holds
L_Cut (f,p) <> {}
proof
let f be non empty FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume that
A1: p in L~f and
A2: L_Cut (f,p) = {};
<*p*>^mid(f,Index(p,f)+1,len f) is non empty &
(p<>f.(Index(p,f)+1) or p=f.(Index(p,f)+1));
then A3: L_Cut(f,p) = mid(f,Index(p,f)+1,len f) & p=f.(Index(p,f)+1)
by A2,JORDAN3:def 4;
len f in dom f by SCMFSA_7:12;
then not Index(p,f)+1 in dom f by A2,A3,SPRECT_2:11;
then not Index(p,f)+1 in Seg len f by FINSEQ_1:def 3;
then Index(p,f)+1 < 1 or Index(p,f)+1 > len f by FINSEQ_1:3;
then Index(p,f) >= len f by NAT_1:29,38;
hence contradiction by A1,JORDAN3:41;
end;
theorem
for f be non empty FinSequence of TOP-REAL 2
for p be Point of TOP-REAL 2 st p in L~f & len R_Cut(f,p) >= 2 holds
f.1 in L~R_Cut(f,p)
proof
let f be non empty FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
len f <> 0 by FINSEQ_1:25;
then len f > 0 by NAT_1:19;
then A1: 0+1 <= len f by NAT_1:38;
assume p in L~f;
then A2: R_Cut(f,p).1 = f.1 by A1,JORDAN1B:4;
assume 2 <= len R_Cut(f,p);
hence f.1 in L~R_Cut(f,p) by A2,JORDAN3:34;
end;
theorem Th9:
for f be non empty FinSequence of TOP-REAL 2 st f is_S-Seq
for p be Point of TOP-REAL 2
st p in L~f holds not f.1 in L~mid(f,Index(p,f)+1,len f)
proof
let f be non empty FinSequence of TOP-REAL 2 such that
A1: f is_S-Seq;
let p be Point of TOP-REAL 2 such that
A2: p in L~f and
A3: f.1 in L~mid(f,Index(p,f)+1,len f);
A4: 1 <= Index(p,f)+1 by NAT_1:29;
Index(p,f) < len f by A2,JORDAN3:41;
then A5: Index(p,f)+1 <= len f by NAT_1:38;
1 in dom f by FINSEQ_5:6;
then f/.1 in L~mid(f,Index(p,f)+1,len f) by A3,FINSEQ_4:def 4;
then Index(p,f)+1 = 0+1 by A1,A4,A5,JORDAN5B:16;
then Index(p,f) = 0 by XCMPLX_1:2;
hence contradiction by A2,JORDAN3:41;
end;
theorem Th10:
for i,j,m,n be Nat holds
i+j = m+n & i <= m & j <= n implies i = m
proof
let i,j,m,n be Nat;
assume that
A1: i+j = m+n and
A2: i <= m and
A3: j <= n;
consider k be Nat such that
A4: m = i + k by A2,NAT_1:28;
consider l be Nat such that
A5: n = j + l by A3,NAT_1:28;
i+(k+n) = i+j by A1,A4,XCMPLX_1:1;
then k+n = j by XCMPLX_1:2;
then j + (l+k) = j+0 by A5,XCMPLX_1:1;
then l+k = 0 by XCMPLX_1:2;
then k = 0 by NAT_1:23;
hence i = m by A4;
end;
theorem
for f be non empty FinSequence of TOP-REAL 2 st f is_S-Seq
for p be Point of TOP-REAL 2 st p in L~f & f.1 in L~L_Cut(f,p) holds
f.1 = p
proof
let f be non empty FinSequence of TOP-REAL 2; assume
A1: f is_S-Seq;
then A2:f is one-to-one unfolded s.n.c. special & len f >= 2 by TOPREAL1:def 10
;
let p be Point of TOP-REAL 2 such that
A3: p in L~f and
A4: f.1 in L~L_Cut(f,p) and
A5: f.1 <> p;
set g = mid(f,Index(p,f)+1,len f);
A6: len f in dom f by FINSEQ_5:6;
1 in dom f by FINSEQ_5:6;
then A7: f/.1 = f.1 by FINSEQ_4:def 4;
A8: not f.1 in L~g by A1,A3,Th9;
then p<>f.(Index(p,f)+1) by A4,JORDAN3:def 4;
then A9: L_Cut(f,p) = <*p*>^g by JORDAN3:def 4;
per cases;
suppose g is empty;
then L_Cut(f,p) = <*p*> by A9,FINSEQ_1:47;
then len L_Cut(f,p) = 1 by FINSEQ_1:56;
hence contradiction by A4,TOPREAL1:28;
suppose g is non empty;
then L~L_Cut(f,p) = LSeg(p,g/.1) \/ L~g by A9,SPPOL_2:20;
then A10: f.1 in LSeg(p,g/.1) by A4,A8,XBOOLE_0:def 2;
consider i being Nat such that
A11: 1 <= i & i+1 <= len(<*p*>^g) and
A12: f/.1 in LSeg(<*p*>^g,i) by A4,A7,A9,SPPOL_2:13;
A13: 1 <= Index(p,f) by A3,JORDAN3:41;
LSeg(<*p*>^g,i) c= LSeg(f,Index(p,f)+i-'1) by A3,A11,JORDAN3:49;
then A14: Index(p,f)+i-'1 = 1 by A2,A12,JORDAN5B:33;
1+1 <= Index(p,f)+i by A11,A13,REAL_1:55;
then 1 <= Index(p,f)+i by AXIOMS:22;
then A15: Index(p,f)+i = 1+1 by A14,AMI_5:4;
then Index(p,f) = 1 by A11,A13,Th10;
then A16: p in LSeg(f,1) by A3,JORDAN3:42;
A17: i = 1 by A11,A13,A15,Th10;
A18: 1+1 <= len f by A1,TOPREAL1:def 10;
then A19: p in LSeg(f/.1,f/.(1+1)) by A16,TOPREAL1:def 5;
2 in dom f by A18,FINSEQ_3:27;
then g/.1 = f/.(1+1) by A6,A15,A17,SPRECT_2:12;
hence contradiction by A5,A7,A10,A19,SPRECT_3:16;
end;
begin :: About Upper and Lower Sequence of a Cage
definition
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
func Upper_Seq(C,n) -> FinSequence of TOP-REAL 2 equals :Def1:
Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n);
coherence;
end;
theorem Th12:
for C be compact non vertical non horizontal Subset of TOP-REAL 2
for n be Nat holds len Upper_Seq(C,n) =
(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))
proof
let C be compact non vertical non horizontal non empty
Subset of TOP-REAL 2;
let n be Nat;
A1: 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 A2: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A1,FINSEQ_6:96;
thus len Upper_Seq(C,n) =
len (Rotate(Cage(C,n),W-min L~Cage(C,n))-:(E-max L~Cage(C,n)))
by Def1
.= (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))
by A2,FINSEQ_5:45;
end;
definition
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
func Lower_Seq(C,n) -> FinSequence of TOP-REAL 2 equals :Def2:
Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n);
coherence;
end;
theorem Th13:
for C be compact non vertical non horizontal Subset of TOP-REAL 2
for n be Nat holds len Lower_Seq(C,n) =
len 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))+1
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
A1: 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 A2: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A1,FINSEQ_6:96;
thus len Lower_Seq(C,n) =
len (Rotate(Cage(C,n),W-min L~Cage(C,n)):-(E-max L~Cage(C,n)))
by Def2
.= len 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))+1
by A2,FINSEQ_5:53;
end;
definition
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
cluster Upper_Seq(C,n) -> non empty;
coherence
proof
A1: 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 A2: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A1,FINSEQ_6:96;
len Upper_Seq(C,n) = (E-max L~Cage(C,n))..Rotate(Cage(C,n),
W-min L~Cage(C,n)) by Th12;
then len Upper_Seq(C,n) >= 0+1 by A2,FINSEQ_4:31;
then len Upper_Seq(C,n) > 0 by NAT_1:38;
hence thesis by FINSEQ_1:25;
end;
cluster Lower_Seq(C,n) -> non empty;
coherence
proof
A3: 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 A4: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A3,FINSEQ_6:96;
len Lower_Seq(C,n) = len 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))+1 by Th13;
then len Lower_Seq(C,n)-1 = len 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)) by XCMPLX_1:26
.= len 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)) by XCMPLX_0:def 8
;
then len Lower_Seq(C,n)-1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),
W-min L~Cage(C,n)) = len Rotate(Cage(C,n),W-min L~Cage(C,n)) by XCMPLX_1:
139;
then (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) =
len Rotate(Cage(C,n),W-min L~Cage(C,n))-(len Lower_Seq(C,n)-1)
by XCMPLX_1:26
.= len Rotate(Cage(C,n),W-min L~Cage(C,n))-len Lower_Seq(C,n)+1
by XCMPLX_1:37;
then len Rotate(Cage(C,n),W-min L~Cage(C,n))-len Lower_Seq(C,n)+1 <=
len Rotate(Cage(C,n),W-min L~Cage(C,n)) by A4,FINSEQ_4:31;
then len Rotate(Cage(C,n),W-min L~Cage(C,n))-len Lower_Seq(C,n) <=
len Rotate(Cage(C,n),W-min L~Cage(C,n))-1 by REAL_1:84;
then len Lower_Seq(C,n) >= 0+1 by REAL_2:105;
then len Lower_Seq(C,n) > 0 by NAT_1:38;
hence thesis by FINSEQ_1:25;
end;
end;
definition
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
cluster Upper_Seq(C,n) -> one-to-one special unfolded s.n.c.;
coherence
proof
A1: Upper_Seq(C,n) =
Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n) by Def1;
set f = Rotate(Cage(C,n),W-min L~Cage(C,n));
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 f by A2,FINSEQ_6:96;
A4: len Upper_Seq(C,n) = (E-max L~Cage(C,n))..f by Th12;
now let i1,j1 be set;
assume that
A5: i1 in dom Upper_Seq(C,n) and
A6: j1 in dom Upper_Seq(C,n) and
A7: Upper_Seq(C,n).i1 = Upper_Seq(C,n).j1 and
A8: i1 <> j1;
A9: L~Cage(C,n) = L~f by REVROT_1:33;
reconsider i2 = i1, j2 = j1 as Nat by A5,A6;
A10: i2 in Seg((E-max L~Cage(C,n))..f) & j2 in Seg((E-max L~Cage(C,n))..f)
by A4,A5,A6,FINSEQ_1:def 3;
A11: Upper_Seq(C,n).i1 = Upper_Seq(C,n)/.i2 by A5,FINSEQ_4:def 4
.= f/.i2 by A1,A3,A10,FINSEQ_5:46;
A12: Upper_Seq(C,n).j1 = Upper_Seq(C,n)/.j2 by A6,FINSEQ_4:def 4
.= f/.j2 by A1,A3,A10,FINSEQ_5:46;
A13: 1 <= i2 & 1 <= j2 by A10,FINSEQ_1:3;
A14: j2 <= (E-max L~Cage(C,n))..f & i2 <= (E-max L~Cage(C,n))..f
by A10,FINSEQ_1:3;
(E-max L~f)..f < len f by SPRECT_5:17;
then A15: j2 < len f & i2 < len f by A9,A14,AXIOMS:22;
per cases by A8,AXIOMS:21;
suppose i2 < j2;
hence contradiction by A7,A11,A12,A13,A15,GOBOARD7:38;
suppose j2 < i2;
hence contradiction by A7,A11,A12,A13,A15,GOBOARD7:38;
end;
hence Upper_Seq(C,n) is one-to-one by FUNCT_1:def 8;
thus Upper_Seq(C,n) is special by A1;
thus Upper_Seq(C,n) is unfolded by A1;
let i,j be Nat;
assume A16: i+1 < j;
len f <> 0 by FINSEQ_1:25;
then len f > 0 by NAT_1:19;
then 0+1 <= len f by NAT_1:38;
then A17: len f in dom f by FINSEQ_3:27;
now per cases;
suppose A18: j+1 <= len Upper_Seq(C,n);
then A19: LSeg(Upper_Seq(C,n),j) = LSeg(f,j) by A1,SPPOL_2:9;
j < len Upper_Seq(C,n) by A18,NAT_1:38;
then i+1 <= len Upper_Seq(C,n) by A16,AXIOMS:22;
then A20: LSeg(Upper_Seq(C,n),i) = LSeg(f,i) by A1,SPPOL_2:9;
A21: j+1 <= (E-max L~Cage(C,n))..f by A1,A3,A18,FINSEQ_5:45;
A22: (E-max L~Cage(C,n))..f <= len f by A3,FINSEQ_4:31;
now per cases by A21,REAL_1:def 5;
suppose j+1 < (E-max L~Cage(C,n))..f;
hence j+1 < len f by A22,AXIOMS:22;
suppose A23: j+1 = (E-max L~Cage(C,n))..f;
assume j+1 >= len f;
then (E-max L~Cage(C,n))..f = len f by A22,A23,AXIOMS:21;
then E-max L~Cage(C,n) = f.(len f) by A3,FINSEQ_4:29
.= f/.(len f) by A17,FINSEQ_4:def 4
.= f/.1 by FINSEQ_6:def 1
.= W-min L~Cage(C,n) by A2,FINSEQ_6:98;
hence contradiction by TOPREAL5:25;
end;
hence LSeg(Upper_Seq(C,n),i) misses LSeg(Upper_Seq(C,n),j)
by A16,A19,A20,GOBOARD5:def 4;
suppose j+1 > len Upper_Seq(C,n);
then LSeg(Upper_Seq(C,n),j) = {} by TOPREAL1:def 5;
then LSeg(Upper_Seq(C,n),i) /\ LSeg(Upper_Seq(C,n),j) = {};
hence LSeg(Upper_Seq(C,n),i) misses LSeg(Upper_Seq(C,n),j)
by XBOOLE_0:def 7;
end;
hence thesis;
end;
cluster Lower_Seq(C,n) -> one-to-one special unfolded s.n.c.;
coherence
proof
A24: 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 A25: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A24,FINSEQ_6:96;
A26: Lower_Seq(C,n) =
Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n) by Def2;
set f = Rotate(Cage(C,n),W-min L~Cage(C,n));
A27: 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 A28: E-max L~Cage(C,n) in rng f by A27,FINSEQ_6:96;
A29: len Lower_Seq(C,n) = len f-(E-max L~Cage(C,n))..f+1 by Th13;
A30: L~Cage(C,n) = L~f by REVROT_1:33;
then A31: f/.1 = W-min L~f by A27,FINSEQ_6:98;
then A32: (W-max L~Cage(C,n))..f <= (N-min L~Cage(C,n))..f
by A30,SPRECT_5:24;
A33: (N-min L~Cage(C,n))..f < (N-max L~Cage(C,n))..f
by A30,A31,SPRECT_5:25;
A34: (N-max L~Cage(C,n))..f <= (E-max L~Cage(C,n))..f
by A30,A31,SPRECT_5:26;
(W-max L~Cage(C,n))..f > 1 by A30,A31,SPRECT_5:23;
then (N-min L~Cage(C,n))..f > 1 by A32,AXIOMS:22;
then (N-max L~Cage(C,n))..f > 1 by A33,AXIOMS:22;
then A35: (E-max L~Cage(C,n))..f > 1 by A34,AXIOMS:22;
now let i1,j1 be set;
assume that
A36: i1 in dom Lower_Seq(C,n) and
A37: j1 in dom Lower_Seq(C,n) and
A38: Lower_Seq(C,n).i1 = Lower_Seq(C,n).j1 and
A39: i1 <> j1;
reconsider i2 = i1, j2 = j1 as Nat by A36,A37;
A40: i2 in Seg len Lower_Seq(C,n) & j2 in Seg len Lower_Seq(C,n)
by A36,A37,FINSEQ_1:def 3;
then i2 >= 1 & j2 >= 1 by FINSEQ_1:3;
then A41: i2 = i2-'1+1 & j2 = j2-'1+1 by AMI_5:4;
A42: Lower_Seq(C,n).i1 = Lower_Seq(C,n)/.i2 by A36,FINSEQ_4:def 4
.= f/.(i2-'1+(E-max L~Cage(C,n))..f) by A26,A28,A36,A41,FINSEQ_5:55;
A43: Lower_Seq(C,n).j1 = Lower_Seq(C,n)/.j2 by A37,FINSEQ_4:def 4
.= f/.(j2-'1+(E-max L~Cage(C,n))..f) by A26,A28,A37,A41,FINSEQ_5:55;
0+1 <= i2 & 0+1 <= j2 by A40,FINSEQ_1:3;
then A44: i2-1 >= 0 & j2-1 >= 0 by REAL_1:84;
j2 <= len f-(E-max L~Cage(C,n))..f+1 &
i2 <= len f-(E-max L~Cage(C,n))..f+1 by A29,A40,FINSEQ_1:3;
then j2-1 <= len f-(E-max L~Cage(C,n))..f &
i2-1 <= len f-(E-max L~Cage(C,n))..f by REAL_1:86;
then j2-1+(E-max L~Cage(C,n))..f <= len f &
i2-1+(E-max L~Cage(C,n))..f <= len f by REAL_1:84;
then A45: j2-'1+(E-max L~Cage(C,n))..f <= len f &
i2-'1+(E-max L~Cage(C,n))..f <= len f by A44,BINARITH:def 3;
i2-'1+(E-max L~Cage(C,n))..f >= (E-max L~Cage(C,n))..f &
j2-'1+(E-max L~Cage(C,n))..f >= (E-max L~Cage(C,n))..f by NAT_1:29;
then A46: 1 < i2-'1+(E-max L~Cage(C,n))..f &
1 < j2-'1+(E-max L~Cage(C,n))..f by A35,AXIOMS:22;
per cases by A39,AXIOMS:21;
suppose i2 < j2;
then i2-1 < j2-1 by REAL_1:54;
then i2-1 < j2-'1 by A44,BINARITH:def 3;
then i2-'1 < j2-'1 by A44,BINARITH:def 3;
then i2-'1+(E-max L~Cage(C,n))..f < j2-'1+(E-max L~Cage(C,n))..f
by REAL_1:53;
hence contradiction by A38,A42,A43,A45,A46,GOBOARD7:39;
suppose j2 < i2;
then j2-1 < i2-1 by REAL_1:54;
then j2-1 < i2-'1 by A44,BINARITH:def 3;
then j2-'1 < i2-'1 by A44,BINARITH:def 3;
then j2-'1+(E-max L~Cage(C,n))..f < i2-'1+(E-max L~Cage(C,n))..f
by REAL_1:53;
hence contradiction by A38,A42,A43,A45,A46,GOBOARD7:39;
end;
hence Lower_Seq(C,n) is one-to-one by FUNCT_1:def 8;
thus Lower_Seq(C,n) is special by A25,A26,SPPOL_2:41;
thus Lower_Seq(C,n) is unfolded by A25,A26,SPPOL_2:28;
let i,j be Nat;
assume A47: i+1 < j;
i+1 >= 1 by NAT_1:29;
then A48: j > 0+1 by A47,AXIOMS:22;
then j = j-'1+1 by AMI_5:4;
then A49: LSeg(Lower_Seq(C,n),j) = LSeg(f,j-'1+(E-max L~Cage(C,n))..f)
by A25,A26,SPPOL_2:10;
now per cases by NAT_1:18;
suppose i > 0;
then A50: i >= 0+1 by NAT_1:38;
then i = i-'1+1 by AMI_5:4;
then A51: LSeg(Lower_Seq(C,n),i) = LSeg(f,i-'1+(E-max L~Cage(C,n))..f)
by A26,A28,SPPOL_2:10;
A52: j-1 > 0 by A48,REAL_1:86;
A53: i-1 >= 0 by A50,REAL_1:84;
i+1-1 < j-1 by A47,REAL_1:54;
then i-1+1 < j-1 by XCMPLX_1:29;
then i-1+1 < j-'1 by A52,BINARITH:def 3;
then i-'1+1 < j-'1 by A53,BINARITH:def 3;
then i-'1+1+(E-max L~Cage(C,n))..f < j-'1+(E-max L~Cage(C,n))..f
by REAL_1:53;
then A54: i-'1+(E-max L~Cage(C,n))..f+1 < j-'1+(E-max L~Cage(C,n))..f
by XCMPLX_1:1;
i-'1 >= 0 by NAT_1:18;
then A55: i-'1+(E-max L~Cage(C,n))..f > 0+1 by A35,REAL_1:67;
now per cases;
suppose j-'1+(E-max L~Cage(C,n))..f+1 <= len f;
then j-'1+(E-max L~Cage(C,n))..f < len f by NAT_1:38;
then LSeg(Lower_Seq(C,n),i) misses LSeg(Lower_Seq(C,n),j)
by A49,A51,A54,A55,GOBOARD5:def 4;
hence LSeg(Lower_Seq(C,n),i) /\ LSeg(Lower_Seq(C,n),j) = {}
by XBOOLE_0:def 7;
suppose j-'1+(E-max L~Cage(C,n))..f+1 > len f;
then LSeg(Lower_Seq(C,n),j) = {} by A49,TOPREAL1:def 5;
hence LSeg(Lower_Seq(C,n),i) /\ LSeg(Lower_Seq(C,n),j) = {};
end;
hence LSeg(Lower_Seq(C,n),i) /\ LSeg(Lower_Seq(C,n),j) = {};
suppose i = 0;
then LSeg(Lower_Seq(C,n),i) = {} by TOPREAL1:def 5;
hence LSeg(Lower_Seq(C,n),i) /\ LSeg(Lower_Seq(C,n),j) = {};
end;
hence thesis by XBOOLE_0:def 7;
end;
end;
theorem Th14:
for C be compact non vertical non horizontal Subset of TOP-REAL 2
for n be Nat holds
len Upper_Seq(C,n) + len Lower_Seq(C,n) = len Cage(C,n)+1
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
thus len Upper_Seq(C,n) + len Lower_Seq(C,n) =
(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))+
len Lower_Seq(C,n) by Th12
.= (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))+
(len 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))+1)
by Th13
.= (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))+
(len 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)))+1
by XCMPLX_1:1
.= (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))+
len 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))+1
by XCMPLX_1:29
.= len Rotate(Cage(C,n),W-min L~Cage(C,n))+1 by XCMPLX_1:26
.= len Cage(C,n)+1 by REVROT_1:14;
end;
theorem Th15:
for C be compact non vertical non horizontal Subset of TOP-REAL 2
for n be Nat holds
Rotate(Cage(C,n),W-min L~Cage(C,n)) = Upper_Seq(C,n) ^' Lower_Seq(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
A1: len (Upper_Seq(C,n) ^' Lower_Seq(C,n)) +1 =
len Upper_Seq(C,n) + len Lower_Seq(C,n) by GRAPH_2:13
.= len Cage(C,n)+1 by Th14
.= len Rotate(Cage(C,n),W-min L~Cage(C,n))+1 by REVROT_1:14;
then A2: len (Upper_Seq(C,n) ^' Lower_Seq(C,n)) =
len Rotate(Cage(C,n),W-min L~Cage(C,n)) by XCMPLX_1:2;
now let i be Nat;
assume A3: i in Seg len Rotate(Cage(C,n),W-min L~Cage(C,n));
then A4: 1 <= i & i <= len Rotate(Cage(C,n),W-min L~Cage(C,n))
by FINSEQ_1:3;
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 A6: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A5,FINSEQ_6:96;
A7: i in dom Rotate(Cage(C,n),W-min L~Cage(C,n)) by A3,FINSEQ_1:def 3;
per cases;
suppose A8: i <= len Upper_Seq(C,n);
then i <= (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))
by Th12;
then A9: i in Seg ((E-max L~Cage(C,n))..Rotate(Cage(C,n),
W-min L~Cage(C,n))) by A4,FINSEQ_1:3;
len (Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n)) =
(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))
by A6,FINSEQ_5:45;
then A10: i in dom (Rotate(Cage(C,n),W-min L~Cage(C,n))-:
E-max L~Cage(C,n)) by A9,FINSEQ_1:def 3;
thus (Upper_Seq(C,n) ^' Lower_Seq(C,n)).i = Upper_Seq(C,n).i
by A4,A8,GRAPH_2:14
.= (Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n)).i
by Def1
.= (Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n))/.i
by A10,FINSEQ_4:def 4
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.i by A6,A9,FINSEQ_5:46
.= Rotate(Cage(C,n),W-min L~Cage(C,n)).i by A7,FINSEQ_4:def 4;
suppose i > len Upper_Seq(C,n);
then i >= len Upper_Seq(C,n)+1 by NAT_1:38;
then consider j be Nat such that
A11: i = len Upper_Seq(C,n)+1+j by NAT_1:28;
A12: i = len Upper_Seq(C,n)+(j+1) by A11,XCMPLX_1:1;
A13: j+1 >= 1 by NAT_1:29;
i < len (Upper_Seq(C,n) ^' Lower_Seq(C,n))+1 by A1,A4,NAT_1:38;
then i < len Lower_Seq(C,n) + len Upper_Seq(C,n) by GRAPH_2:13;
then i-len Upper_Seq(C,n) < len Lower_Seq(C,n) by REAL_1:84;
then A14: j+1 < len Lower_Seq(C,n) by A12,XCMPLX_1:26;
A15: i = (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))+(j+1)
by A12,Th12;
A16: j+1+1 >= 1 by NAT_1:29;
A17: len (Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n)) =
len 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))+1
by A6,FINSEQ_5:53;
j+1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) <=
len Rotate(Cage(C,n),W-min L~Cage(C,n)) by A4,A12,Th12;
then j+1 <= len 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)) by REAL_1:84;
then j+1+1 <= len (Rotate(Cage(C,n),W-min L~Cage(C,n)):-
(E-max L~Cage(C,n))) by A17,REAL_1:55;
then j+1+1 in Seg len (Rotate(Cage(C,n),W-min L~Cage(C,n)):-
(E-max L~Cage(C,n))) by A16,FINSEQ_1:3;
then A18: j+1+1 in dom (Rotate(Cage(C,n),W-min L~Cage(C,n)):-
(E-max L~Cage(C,n))) by FINSEQ_1:def 3;
thus (Upper_Seq(C,n) ^' Lower_Seq(C,n)).i = Lower_Seq(C,n).(j+1+1)
by A12,A13,A14,GRAPH_2:15
.= (Rotate(Cage(C,n),W-min L~Cage(C,n)):-(E-max L~Cage(C,n))).
(j+1+1) by Def2
.= (Rotate(Cage(C,n),W-min L~Cage(C,n)):-(E-max L~Cage(C,n)))/.
(j+1+1) by A18,FINSEQ_4:def 4
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.
(j+1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)))
by A6,A18,FINSEQ_5:55
.= Rotate(Cage(C,n),W-min L~Cage(C,n)).i by A7,A15,FINSEQ_4:def 4;
end;
hence Rotate(Cage(C,n),W-min L~Cage(C,n)) =
Upper_Seq(C,n) ^' Lower_Seq(C,n) by A2,FINSEQ_2:10;
end;
theorem
for C be compact non vertical non horizontal Subset of TOP-REAL 2
for n be Nat holds
L~Cage(C,n) = L~(Upper_Seq(C,n) ^' Lower_Seq(C,n))
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
Rotate(Cage(C,n),W-min L~Cage(C,n)) = Upper_Seq(C,n) ^' Lower_Seq(C,n)
by Th15;
hence L~Cage(C,n) = L~(Upper_Seq(C,n) ^' Lower_Seq(C,n)) by REVROT_1:33;
end;
theorem
for C be compact non vertical non horizontal non empty Subset of TOP-REAL
2
for n be Nat holds
L~Cage(C,n) = L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n)
proof
let C be compact non vertical non horizontal non empty
Subset of TOP-REAL 2;
let n be Nat;
A1: Upper_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n)
by Def1;
A2: Lower_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n)
by Def2;
A3: 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 Rotate(Cage(C,n),W-min L~Cage(C,n))
by A3,FINSEQ_6:96;
then L~Rotate(Cage(C,n),W-min L~Cage(C,n)) =
L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n) by A1,A2,SPPOL_2:25;
hence thesis by REVROT_1:33;
end;
theorem Th18:
for P be Simple_closed_curve holds W-min(P) <> E-min(P)
proof
let P be Simple_closed_curve;
now assume A1: W-min(P) = E-min(P);
A2:|[W-bound P, inf (proj2||W-most P)]|=W-min(P) by PSCOMP_1:def 42;
|[E-bound P, inf (proj2||E-most P)]|=E-min(P) by PSCOMP_1:def 47;
then W-bound P= E-bound P by A1,A2,SPPOL_2:1;
hence contradiction by TOPREAL5:23;
end;
hence W-min(P) <> E-min(P);
end;
theorem Th19:
for C be compact non vertical non horizontal Subset of TOP-REAL 2
for n be Nat holds
len Upper_Seq(C,n) >= 3 & len Lower_Seq(C,n) >= 3
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
set pWi = W-min L~Cage(C,n);
set pWa = W-max L~Cage(C,n);
set pEi = E-min L~Cage(C,n);
set pEa = E-max L~Cage(C,n);
A1: pWi <> pWa by SPRECT_2:62;
A2: pWa <> pEa by JORDAN1B:6;
pWi <> pEa by TOPREAL5:25;
then A3: Card {pWi,pWa,pEa} = 3 by A1,A2,CARD_2:77;
A4: Upper_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n)
by Def1;
A5: Lower_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n)
by Def2;
A6: 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 A7: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A6,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));
then A8: pEa in rng Upper_Seq(C,n) by A4,A7,FINSEQ_5:49;
A9: Upper_Seq(C,n)/.1 = Rotate(Cage(C,n),W-min L~Cage(C,n))/.1
by A4,A7,FINSEQ_5:47;
then A10: Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by A6,FINSEQ_6:98;
then A11: pWi in rng Upper_Seq(C,n) by FINSEQ_6:46;
pWa in rng Cage(C,n) by SPRECT_2:48;
then A12: pWa in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A6,FINSEQ_6:96;
set f=Rotate(Cage(C,n),W-min L~Cage(C,n));
A13: L~Cage(C,n) = L~f by REVROT_1:33;
then A14: (W-max L~f)..f <= (N-min L~f)..f by A9,A10,SPRECT_5:24;
(N-min L~f)..f < (N-max L~f)..f by A9,A10,A13,SPRECT_5:25;
then A15: (W-max L~f)..f < (N-max L~f)..f by A14,AXIOMS:22;
(N-max L~f)..f <= (E-max L~f)..f by A9,A10,A13,SPRECT_5:26;
then pWa..Rotate(Cage(C,n),W-min L~Cage(C,n)) <
pEa..Rotate(Cage(C,n),W-min L~Cage(C,n)) by A13,A15,AXIOMS:22;
then A16: pWa in rng Upper_Seq(C,n) by A4,A7,A12,FINSEQ_5:49;
{pWi,pWa,pEa} c= rng Upper_Seq(C,n)
proof
let x be set;
assume x in {pWi,pWa,pEa};
hence x in rng Upper_Seq(C,n) by A8,A11,A16,ENUMSET1:def 1;
end;
then A17: Card {pWi,pWa,pEa} c= Card rng Upper_Seq(C,n) by CARD_1:27;
Card rng Upper_Seq(C,n) c= Card dom Upper_Seq(C,n) by YELLOW_6:3;
then Card rng Upper_Seq(C,n) c= len Upper_Seq(C,n) by PRE_CIRC:21;
then 3 c= len Upper_Seq(C,n) by A3,A17,XBOOLE_1:1;
hence len Upper_Seq(C,n) >= 3 by CARD_1:56;
A18: pWi <> pEi by Th18;
A19: pEi <> pEa by SPRECT_2:58;
pWi <> pEa by TOPREAL5:25;
then A20: Card {pWi,pEi,pEa} = 3 by A18,A19,CARD_2:77;
A21: pEa in rng Lower_Seq(C,n) by A5,FINSEQ_6:66;
Lower_Seq(C,n)/.(len Lower_Seq(C,n)) =
Rotate(Cage(C,n),W-min L~Cage(C,n))/.
(len Rotate(Cage(C,n),W-min L~Cage(C,n))) by A5,A7,FINSEQ_5:57
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by FINSEQ_6:def 1
.= W-min L~Cage(C,n) by A6,FINSEQ_6:98;
then A22: pWi in rng Lower_Seq(C,n) by REVROT_1:3;
pEi in rng Cage(C,n) by SPRECT_2:49;
then A23: pEi in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A6,FINSEQ_6:96;
pEi..Rotate(Cage(C,n),W-min L~Cage(C,n)) >
pEa..Rotate(Cage(C,n),W-min L~Cage(C,n)) by A9,A10,A13,SPRECT_5:27;
then A24: pEi in rng Lower_Seq(C,n) by A5,A7,A23,FINSEQ_6:67;
{pWi,pEi,pEa} c= rng Lower_Seq(C,n)
proof
let x be set;
assume x in {pWi,pEi,pEa};
hence x in rng Lower_Seq(C,n) by A21,A22,A24,ENUMSET1:def 1;
end;
then A25: Card {pWi,pEi,pEa} c= Card rng Lower_Seq(C,n) by CARD_1:27;
Card rng Lower_Seq(C,n) c= Card dom Lower_Seq(C,n) by YELLOW_6:3;
then Card rng Lower_Seq(C,n) c= len Lower_Seq(C,n) by PRE_CIRC:21;
then 3 c= len Lower_Seq(C,n) by A20,A25,XBOOLE_1:1;
hence len Lower_Seq(C,n) >= 3 by CARD_1:56;
end;
definition
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
cluster Upper_Seq(C,n) -> being_S-Seq;
coherence
proof
len Upper_Seq(C,n) >= 3 by Th19;
then len Upper_Seq(C,n) >= 2 by AXIOMS:22;
hence thesis by TOPREAL1:def 10;
end;
cluster Lower_Seq(C,n) -> being_S-Seq;
coherence
proof
len Lower_Seq(C,n) >= 3 by Th19;
then len Lower_Seq(C,n) >= 2 by AXIOMS:22;
hence thesis by TOPREAL1:def 10;
end;
end;
theorem
for C be compact non vertical non horizontal Subset of TOP-REAL 2
for n be Nat holds
L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) =
{W-min L~Cage(C,n),E-max L~Cage(C,n)}
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
A1: Upper_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n)
by Def1;
A2: Lower_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n)
by Def2;
A3: 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 A4: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A3,FINSEQ_6:96;
A5: (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));
len Lower_Seq(C,n) >= 3 by Th19;
then len Lower_Seq(C,n) >= 2 by AXIOMS:22;
then A6: rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18;
A7: E-max L~Cage(C,n) in rng Lower_Seq(C,n) by A2,FINSEQ_6:66;
A8: len Upper_Seq(C,n) >= 3 by Th19;
then len Upper_Seq(C,n) >= 2 by AXIOMS:22;
then A9: rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18;
A10: E-max L~Cage(C,n) in rng Upper_Seq(C,n) by A1,A4,A5,FINSEQ_5:49;
Upper_Seq(C,n)/.1 = Rotate(Cage(C,n),W-min L~Cage(C,n))/.1
by A1,A4,FINSEQ_5:47
.= W-min L~Cage(C,n) by A3,FINSEQ_6:98;
then A11: W-min L~Cage(C,n) in rng Upper_Seq(C,n) by FINSEQ_6:46;
Lower_Seq(C,n)/.(len Lower_Seq(C,n)) =
Rotate(Cage(C,n),W-min L~Cage(C,n))/.
(len Rotate(Cage(C,n),W-min L~Cage(C,n))) by A2,A4,FINSEQ_5:57
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by FINSEQ_6:def 1
.= W-min L~Cage(C,n) by A3,FINSEQ_6:98;
then A12: W-min L~Cage(C,n) in rng Lower_Seq(C,n) by REVROT_1:3;
thus L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) c=
{W-min L~Cage(C,n),E-max L~Cage(C,n)}
proof
let x be set;
assume A13: x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n);
then A14: x in L~Upper_Seq(C,n) & x in L~Lower_Seq(C,n) by XBOOLE_0:def 3;
reconsider x1=x as Point of TOP-REAL 2 by A13;
consider i1 be Nat such that
A15: 1 <= i1 & i1+1 <= len Upper_Seq(C,n) and
A16: x1 in LSeg(Upper_Seq(C,n),i1) by A14,SPPOL_2:13;
consider i2 be Nat such that
A17: 1 <= i2 & i2+1 <= len Lower_Seq(C,n) and
A18: x1 in LSeg(Lower_Seq(C,n),i2) by A14,SPPOL_2:13;
set f=Rotate(Cage(C,n),W-min L~Cage(C,n));
set pE=E-max L~Cage(C,n);
set pW=W-min L~Cage(C,n);
A19: LSeg(Upper_Seq(C,n),i1) = LSeg(f,i1) by A1,A15,SPPOL_2:9;
set i3=i2-'1;
A20: i3+1 = i2 by A17,AMI_5:4;
then A21: LSeg(Lower_Seq(C,n),i2) = LSeg(f,i3+pE..f) by A2,A4,SPPOL_2:10;
A22: len Upper_Seq(C,n) = pE..f by Th12;
A23: len Lower_Seq(C,n) = len f-pE..f+1 by Th13;
A24: i2-1 >= 1-1 by A17,REAL_1:49;
i2 < len f-pE..f+1 by A17,A23,NAT_1:38;
then i2-1 < len f-pE..f by REAL_1:84;
then i2-1+pE..f < len f by REAL_1:86;
then A25: i3+pE..f < len f by A24,BINARITH:def 3;
A26: i3 >= 0 by NAT_1:18;
A27: pE..f >= 1 by A4,FINSEQ_4:31;
i3+1 < len f-pE..f+1 by A17,A20,A23,NAT_1:38;
then i3 < len f-pE..f by REAL_1:55;
then A28: i3+pE..f < len f by REAL_1:86;
A29: i1+1 < pE..f+1 by A15,A22,NAT_1:38;
1+pE..f <= i3+1+pE..f by A17,A20,REAL_1:55;
then i1+1 < i3+1+pE..f by A29,AXIOMS:22;
then i1+1 < i3+pE..f+1 by XCMPLX_1:1;
then A30: i1+1 <= i3+pE..f by NAT_1:38;
A31: i3+pE..f+1 <= len f by A28,NAT_1:38;
A32: len f > 4 by GOBOARD7:36;
A33: i3+pE..f >= 0 & i1 >= 0 by NAT_1:18;
A34: pE..f-'1+1 = pE..f by A27,AMI_5:4;
assume A35: not x in {W-min L~Cage(C,n),E-max L~Cage(C,n)};
now per cases by A15,A30,REAL_1:def 5;
suppose i1+1 < i3+pE..f & i1 > 1;
then LSeg(f,i1) misses LSeg(f,i3+pE..f) by A28,GOBOARD5:def 4;
then LSeg(f,i1) /\ LSeg(f,i3+pE..f) = {} by XBOOLE_0:def 7;
hence contradiction by A16,A18,A19,A21,XBOOLE_0:def 3;
suppose A36: i1 = 1;
i3+pE..f >= 0+3 by A8,A22,A26,REAL_1:55;
then A37: i1+1 < i3+pE..f by A36,AXIOMS:22;
now per cases by A31,REAL_1:def 5;
suppose i3+pE..f+1 < len f;
then LSeg(f,i1) misses LSeg(f,i3+pE..f) by A37,GOBOARD5:def 4;
then LSeg(f,i1) /\ LSeg(f,i3+pE..f) = {} by XBOOLE_0:def 7;
hence contradiction by A16,A18,A19,A21,XBOOLE_0:def 3;
suppose i3+pE..f+1 = len f;
then i3+pE..f = len f-1 by XCMPLX_1:26;
then i3+pE..f = len f-'1 by A33,BINARITH:def 3;
then LSeg(f,i1) /\ LSeg(f,i3+pE..f) = {f/.1} by A32,A36,REVROT_1:30;
then x1 in {f/.1} by A16,A18,A19,A21,XBOOLE_0:def 3;
then x1 = f/.1 by TARSKI:def 1
.= pW by A3,FINSEQ_6:98;
hence contradiction by A35,TARSKI:def 2;
end;
hence contradiction;
suppose A38: i1+1 = i3+pE..f;
0+pE..f <= i3+pE..f by A26,REAL_1:55;
then pE..f = i1+1 by A15,A22,A38,AXIOMS:21;
then i1 = pE..f-1 by XCMPLX_1:26;
then A39: i1 = pE..f-'1 by A33,BINARITH:def 3;
i3+pE..f >= pE..f by NAT_1:29;
then pE..f < len f by A25,AXIOMS:22;
then pE..f+1 <= len f by NAT_1:38;
then pE..f-'1 + (1+1) <= len f by A34,XCMPLX_1:1;
then LSeg(f,i1) /\ LSeg(f,i3+(pE..f)) = {f/.(pE..f)}
by A15,A34,A38,A39,TOPREAL1:def 8;
then x1 in {f/.(pE..f)} by A16,A18,A19,A21,XBOOLE_0:def 3;
then x1 = f/.(pE..f) by TARSKI:def 1
.= pE by A4,FINSEQ_5:41;
hence contradiction by A35,TARSKI:def 2;
end;
hence contradiction;
end;
thus {W-min L~Cage(C,n),E-max L~Cage(C,n)} c=
L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n)
proof
let x be set;
assume A40: x in {W-min L~Cage(C,n),E-max L~Cage(C,n)};
per cases by A40,TARSKI:def 2;
suppose x = W-min L~Cage(C,n);
hence x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n)
by A6,A9,A11,A12,XBOOLE_0:def 3;
suppose x = E-max L~Cage(C,n);
hence x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n)
by A6,A7,A9,A10,XBOOLE_0:def 3;
end;
end;
theorem
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
Upper_Seq(C,n) is_in_the_area_of Cage(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
A1: Upper_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n)
by Def1;
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;
Rotate(Cage(C,n),W-min L~Cage(C,n)) is_in_the_area_of Cage(C,n)
by JORDAN1B:11;
hence Upper_Seq(C,n) is_in_the_area_of Cage(C,n) by A1,A3,Th5;
end;
theorem
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
Lower_Seq(C,n) is_in_the_area_of Cage(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
A1: Lower_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n)
by Def2;
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;
Rotate(Cage(C,n),W-min L~Cage(C,n)) is_in_the_area_of Cage(C,n)
by JORDAN1B:11;
hence thesis by A1,A3,Th6;
end;
theorem
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
holds (Cage(C,n)/.2)`2 = N-bound L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:34;
then Cage(C,n)/.2 in N-most L~Cage(C,n) by SPRECT_2:34;
then (Cage(C,n)/.2)`2 = (N-min L~Cage(C,n))`2 by PSCOMP_1:98;
hence thesis by PSCOMP_1:94;
end;
theorem
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
for k be Nat st 1 <= k & k+1 <= len Cage(C,n) &
Cage(C,n)/.k = E-max L~Cage(C,n) holds
(Cage(C,n)/.(k+1))`1 = E-bound L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
A1: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
let k be Nat;
assume that
A2: 1 <= k and
A3: k+1 <= len Cage(C,n) and
A4: Cage(C,n)/.k = E-max L~Cage(C,n);
A5: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:34;
then A6: 1 < (N-max L~Cage(C,n))..Cage(C,n) by SPRECT_2:73;
(N-max L~Cage(C,n))..Cage(C,n) <= (E-max L~Cage(C,n))..Cage(C,n)
by A5,SPRECT_2:74;
then A7: (E-max L~Cage(C,n))..Cage(C,n) > 1 by A6,AXIOMS:22;
A8: k < len Cage(C,n) by A3,NAT_1:38;
then A9: k in dom Cage(C,n) by A2,FINSEQ_3:27;
then (E-max L~Cage(C,n))..Cage(C,n) <= k by A4,FINSEQ_5:42;
then A10: k > 1 by A7,AXIOMS:22;
then consider i1,j1,i2,j2 be Nat such that
A11: [i1,j1] in Indices Gauge(C,n) and
A12: Cage(C,n)/.k = Gauge(C,n)*(i1,j1) and
A13: [i2,j2] in Indices Gauge(C,n) and
A14: Cage(C,n)/.(k+1) = Gauge(C,n)*(i2,j2) and
A15: 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,JORDAN8:6;
A16: 1 <= i1 & i1 <= len Gauge(C,n) & 1 <= j1 & j1 <= width Gauge(C,n)
by A11,GOBOARD5:1;
A17: 1 <= i2 & i2 <= len Gauge(C,n) & 1 <= j2 & j2 <= width Gauge(C,n)
by A13,GOBOARD5:1;
A18: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
Gauge(C,n)*(i1,j1)`1 = E-bound L~Cage(C,n) by A4,A12,PSCOMP_1:104
.= Gauge(C,n)*(len Gauge(C,n),j1)`1 by A16,A18,JORDAN1A:92;
then A19: i1 <= len Gauge(C,n) & i1 >= len Gauge(C,n) by A16,GOBOARD5:4;
then A20: i1 = len Gauge(C,n) by AXIOMS:21;
reconsider k'=k-1 as Nat by A9,FINSEQ_3:28;
k >= 1+1 by A10,NAT_1:38;
then A21: k' >= 1+1-1 by REAL_1:49;
A22: k'+1 < len Cage(C,n) by A8,XCMPLX_1:27;
then consider i3,j3,i4,j4 be Nat such that
A23: [i3,j3] in Indices Gauge(C,n) and
A24: Cage(C,n)/.k' = Gauge(C,n)*(i3,j3) and
A25: [i4,j4] in Indices Gauge(C,n) and
A26: Cage(C,n)/.(k'+1) = Gauge(C,n)*(i4,j4) and
A27: i3 = i4 & j3+1 = j4 or i3+1 = i4 & j3 = j4 or
i3 = i4+1 & j3 = j4 or i3 = i4 & j3 = j4+1 by A1,A21,JORDAN8:6;
A28: k'+1 = k by XCMPLX_1:27;
then A29: i1 = i4 & j1 = j4 by A11,A12,A25,A26,GOBOARD1:21;
A30: 1 <= i3 & i3 <= len Gauge(C,n) & 1 <= j3 & j3 <= width Gauge(C,n)
by A23,GOBOARD5:1;
A31: j3 = j4
proof
assume A32: j3 <> j4;
per cases by A27,A32;
suppose i3 = i4 & j3+1 = j4;
hence contradiction by A19,A21,A22,A23,A24,A25,A26,A29,JORDAN10:1;
suppose A33: i3 = i4 & j3 = j4+1;
k' < len Cage(C,n) by A22,NAT_1:38;
then Gauge(C,n)*(i3,j3) in E-most L~Cage(C,n)
by A20,A21,A24,A29,A30,A33,JORDAN1A:82;
then A34: (Gauge(C,n)*(i4,j4+1))`2 <= (Gauge(C,n)*(i4,j4))`2
by A4,A26,A28,A33,PSCOMP_1:108;
j4 < j4+1 by NAT_1:38;
hence contradiction by A16,A29,A30,A33,A34,GOBOARD5:5;
end;
i1 = i2
proof
assume A35: i1 <> i2;
per cases by A15,A35;
suppose i1+1 = i2 & j1 = j2;
hence contradiction by A17,A19,NAT_1:38;
suppose i1 = i2+1 & j1 = j2;
then A36: Cage(C,n)/.(k+1) = Cage(C,n)/.k'
by A14,A19,A24,A27,A29,A30,A31,NAT_1:38,XCMPLX_1:2
;
k'+1+1 <= len Cage(C,n) by A22,NAT_1:38;
then k'+(1+1) <= len Cage(C,n) by XCMPLX_1:1;
then A37: LSeg(Cage(C,n),k') /\ LSeg(Cage(C,n),k) = {Cage(C,n)/.k}
by A21,A28,TOPREAL1:def 8;
Cage(C,n)/.k' in LSeg(Cage(C,n),k') &
Cage(C,n)/.(k+1) in LSeg(Cage(C,n),k) by A2,A3,A8,A21,A28,TOPREAL1:27;
then Cage(C,n)/.(k+1) in {Cage(C,n)/.k} by A36,A37,XBOOLE_0:def 3;
then Cage(C,n)/.(k+1) = Cage(C,n)/.k by TARSKI:def 1;
hence contradiction by A11,A12,A13,A14,A35,GOBOARD1:21;
end;
then Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A16,GOBOARD5:3
.= Gauge(C,n)*(i2,j2)`1 by A17,GOBOARD5:3;
hence thesis by A4,A12,A14,PSCOMP_1:104;
end;
theorem
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
for k be Nat st 1 <= k & k+1 <= len Cage(C,n) &
Cage(C,n)/.k = S-max L~Cage(C,n) holds
(Cage(C,n)/.(k+1))`2 = S-bound L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
A1: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
let k be Nat;
assume that
A2: 1 <= k and
A3: k+1 <= len Cage(C,n) and
A4: Cage(C,n)/.k = S-max L~Cage(C,n);
A5: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:34;
then A6: 1 < (N-max L~Cage(C,n))..Cage(C,n) by SPRECT_2:73;
(N-max L~Cage(C,n))..Cage(C,n) <= (E-max L~Cage(C,n))..Cage(C,n)
by A5,SPRECT_2:74;
then A7: 1 < (E-max L~Cage(C,n))..Cage(C,n) by A6,AXIOMS:22;
(E-max L~Cage(C,n))..Cage(C,n) < (E-min L~Cage(C,n))..Cage(C,n)
by A5,SPRECT_2:75;
then A8: 1 < (E-min L~Cage(C,n))..Cage(C,n) by A7,AXIOMS:22;
(E-min L~Cage(C,n))..Cage(C,n) <= (S-max L~Cage(C,n))..Cage(C,n)
by A5,SPRECT_2:76;
then A9: (S-max L~Cage(C,n))..Cage(C,n) > 1 by A8,AXIOMS:22;
A10: k < len Cage(C,n) by A3,NAT_1:38;
then A11: k in dom Cage(C,n) by A2,FINSEQ_3:27;
then (S-max L~Cage(C,n))..Cage(C,n) <= k by A4,FINSEQ_5:42;
then A12: k > 1 by A9,AXIOMS:22;
then consider i1,j1,i2,j2 be Nat such that
A13: [i1,j1] in Indices Gauge(C,n) and
A14: Cage(C,n)/.k = Gauge(C,n)*(i1,j1) and
A15: [i2,j2] in Indices Gauge(C,n) and
A16: Cage(C,n)/.(k+1) = Gauge(C,n)*(i2,j2) and
A17: 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,JORDAN8:6;
A18: 1 <= i1 & i1 <= len Gauge(C,n) & 1 <= j1 & j1 <= width Gauge(C,n)
by A13,GOBOARD5:1;
A19: 1 <= i2 & i2 <= len Gauge(C,n) & 1 <= j2 & j2 <= width Gauge(C,n)
by A15,GOBOARD5:1;
Gauge(C,n)*(i1,j1)`2 = S-bound L~Cage(C,n) by A4,A14,PSCOMP_1:114
.= Gauge(C,n)*(i1,1)`2 by A18,JORDAN1A:93;
then A20: j1 <= 1 & j1 >= 1 by A18,GOBOARD5:5;
then A21: j1 = 1 by AXIOMS:21;
reconsider k'=k-1 as Nat by A11,FINSEQ_3:28;
k >= 1+1 by A12,NAT_1:38;
then A22: k' >= 1+1-1 by REAL_1:49;
A23: k'+1 < len Cage(C,n) by A10,XCMPLX_1:27;
then consider i3,j3,i4,j4 be Nat such that
A24: [i3,j3] in Indices Gauge(C,n) and
A25: Cage(C,n)/.k' = Gauge(C,n)*(i3,j3) and
A26: [i4,j4] in Indices Gauge(C,n) and
A27: Cage(C,n)/.(k'+1) = Gauge(C,n)*(i4,j4) and
A28: i3 = i4 & j3+1 = j4 or i3+1 = i4 & j3 = j4 or
i3 = i4+1 & j3 = j4 or i3 = i4 & j3 = j4+1 by A1,A22,JORDAN8:6;
A29: k'+1 = k by XCMPLX_1:27;
then A30: i1 = i4 & j1 = j4 by A13,A14,A26,A27,GOBOARD1:21;
A31: 1 <= i3 & i3 <= len Gauge(C,n) & 1 <= j3 & j3 <= width Gauge(C,n)
by A24,GOBOARD5:1;
A32: i3 = i4
proof
assume A33: i3 <> i4;
per cases by A28,A33;
suppose j3 = j4 & i3+1 = i4;
hence contradiction by A20,A22,A23,A24,A25,A26,A27,A30,JORDAN10:3;
suppose A34: j3 = j4 & i3 = i4+1;
k' < len Cage(C,n) by A23,NAT_1:38;
then Gauge(C,n)*(i3,j3) in S-most L~Cage(C,n)
by A21,A22,A25,A30,A31,A34,JORDAN1A:81;
then A35: (Gauge(C,n)*(i4+1,j4))`1 <= (Gauge(C,n)*(i4,j4))`1
by A4,A27,A29,A34,PSCOMP_1:118;
i4 < i4+1 by NAT_1:38;
hence contradiction by A18,A30,A31,A34,A35,GOBOARD5:4;
end;
j1 = j2
proof
assume A36: j1 <> j2;
per cases by A17,A36;
suppose j1 = j2+1 & i1 = i2;
hence contradiction by A19,A20,NAT_1:38;
suppose A37: j1+1 = j2 & i1 = i2;
k'+1+1 <= len Cage(C,n) by A23,NAT_1:38;
then k'+(1+1) <= len Cage(C,n) by XCMPLX_1:1;
then A38: LSeg(Cage(C,n),k') /\ LSeg(Cage(C,n),k) = {Cage(C,n)/.k}
by A22,A29,TOPREAL1:def 8;
Cage(C,n)/.k' in LSeg(Cage(C,n),k') &
Cage(C,n)/.(k+1) in LSeg(Cage(C,n),k) by A2,A3,A10,A22,A29,TOPREAL1:27;
then Cage(C,n)/.(k+1) in {Cage(C,n)/.k}
by A16,A20,A25,A28,A30,A31,A32,A37,A38,NAT_1:38,XBOOLE_0:def
3;
then Cage(C,n)/.(k+1) = Cage(C,n)/.k by TARSKI:def 1;
hence contradiction by A13,A14,A15,A16,A36,GOBOARD1:21;
end;
then Gauge(C,n)*(i1,j1)`2 = Gauge(C,n)*(1,j2)`2 by A18,GOBOARD5:2
.= Gauge(C,n)*(i2,j2)`2 by A19,GOBOARD5:2;
hence thesis by A4,A14,A16,PSCOMP_1:114;
end;
theorem
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
for k be Nat st 1 <= k & k+1 <= len Cage(C,n) &
Cage(C,n)/.k = W-min L~Cage(C,n) holds
(Cage(C,n)/.(k+1))`1 = W-bound L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
A1: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
let k be Nat;
assume that
A2: 1 <= k and
A3: k+1 <= len Cage(C,n) and
A4: Cage(C,n)/.k = W-min L~Cage(C,n);
A5: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:34;
then A6: 1 < (N-max L~Cage(C,n))..Cage(C,n) by SPRECT_2:73;
(N-max L~Cage(C,n))..Cage(C,n) <= (E-max L~Cage(C,n))..Cage(C,n)
by A5,SPRECT_2:74;
then A7: 1 < (E-max L~Cage(C,n))..Cage(C,n) by A6,AXIOMS:22;
(E-max L~Cage(C,n))..Cage(C,n) < (E-min L~Cage(C,n))..Cage(C,n)
by A5,SPRECT_2:75;
then A8: 1 < (E-min L~Cage(C,n))..Cage(C,n) by A7,AXIOMS:22;
(E-min L~Cage(C,n))..Cage(C,n) <= (S-max L~Cage(C,n))..Cage(C,n)
by A5,SPRECT_2:76;
then A9: 1 < (S-max L~Cage(C,n))..Cage(C,n) by A8,AXIOMS:22;
(S-max L~Cage(C,n))..Cage(C,n) < (S-min L~Cage(C,n))..Cage(C,n)
by A5,SPRECT_2:77;
then A10: 1 < (S-min L~Cage(C,n))..Cage(C,n) by A9,AXIOMS:22;
(S-min L~Cage(C,n))..Cage(C,n) <= (W-min L~Cage(C,n))..Cage(C,n)
by A5,SPRECT_2:78;
then A11: (W-min L~Cage(C,n))..Cage(C,n) > 1 by A10,AXIOMS:22;
A12: k < len Cage(C,n) by A3,NAT_1:38;
then A13: k in dom Cage(C,n) by A2,FINSEQ_3:27;
then (W-min L~Cage(C,n))..Cage(C,n) <= k by A4,FINSEQ_5:42;
then A14: k > 1 by A11,AXIOMS:22;
then consider i1,j1,i2,j2 be Nat such that
A15: [i1,j1] in Indices Gauge(C,n) and
A16: Cage(C,n)/.k = Gauge(C,n)*(i1,j1) and
A17: [i2,j2] in Indices Gauge(C,n) and
A18: Cage(C,n)/.(k+1) = Gauge(C,n)*(i2,j2) and
A19: 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,JORDAN8:6;
A20: 1 <= i1 & i1 <= len Gauge(C,n) & 1 <= j1 & j1 <= width Gauge(C,n)
by A15,GOBOARD5:1;
A21: 1 <= i2 & i2 <= len Gauge(C,n) & 1 <= j2 & j2 <= width Gauge(C,n)
by A17,GOBOARD5:1;
A22: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
Gauge(C,n)*(i1,j1)`1 = W-bound L~Cage(C,n) by A4,A16,PSCOMP_1:84
.= Gauge(C,n)*(1,j1)`1 by A20,A22,JORDAN1A:94;
then A23: i1 <= 1 & i1 >= 1 by A20,GOBOARD5:4;
then A24: i1 = 1 by AXIOMS:21;
reconsider k'=k-1 as Nat by A13,FINSEQ_3:28;
k >= 1+1 by A14,NAT_1:38;
then A25: k' >= 1+1-1 by REAL_1:49;
A26: k'+1 < len Cage(C,n) by A12,XCMPLX_1:27;
then consider i3,j3,i4,j4 be Nat such that
A27: [i3,j3] in Indices Gauge(C,n) and
A28: Cage(C,n)/.k' = Gauge(C,n)*(i3,j3) and
A29: [i4,j4] in Indices Gauge(C,n) and
A30: Cage(C,n)/.(k'+1) = Gauge(C,n)*(i4,j4) and
A31: i3 = i4 & j3+1 = j4 or i3+1 = i4 & j3 = j4 or
i3 = i4+1 & j3 = j4 or i3 = i4 & j3 = j4+1 by A1,A25,JORDAN8:6;
A32: k'+1 = k by XCMPLX_1:27;
then A33: i1 = i4 & j1 = j4 by A15,A16,A29,A30,GOBOARD1:21;
A34: 1 <= i3 & i3 <= len Gauge(C,n) & 1 <= j3 & j3 <= width Gauge(C,n)
by A27,GOBOARD5:1;
A35: j3 = j4
proof
assume A36: j3 <> j4;
per cases by A31,A36;
suppose i3 = i4 & j3 = j4+1;
hence contradiction by A23,A25,A26,A27,A28,A29,A30,A33,JORDAN10:2;
suppose A37: i3 = i4 & j3+1 = j4;
k' < len Cage(C,n) by A26,NAT_1:38;
then Gauge(C,n)*(i3,j3) in W-most L~Cage(C,n)
by A24,A25,A28,A33,A34,A37,JORDAN1A:80;
then A38: (Gauge(C,n)*(i3,j3+1))`2 <= (Gauge(C,n)*(i3,j3))`2
by A4,A30,A32,A37,PSCOMP_1:88;
j3 < j3+1 by NAT_1:38;
hence contradiction by A20,A33,A34,A37,A38,GOBOARD5:5;
end;
i1 = i2
proof
assume A39: i1 <> i2;
per cases by A19,A39;
suppose i1 = i2+1 & j1 = j2;
hence contradiction by A21,A23,NAT_1:38;
suppose A40: i1+1 = i2 & j1 = j2;
k'+1+1 <= len Cage(C,n) by A26,NAT_1:38;
then k'+(1+1) <= len Cage(C,n) by XCMPLX_1:1;
then A41: LSeg(Cage(C,n),k') /\ LSeg(Cage(C,n),k) = {Cage(C,n)/.k}
by A25,A32,TOPREAL1:def 8;
Cage(C,n)/.k' in LSeg(Cage(C,n),k') &
Cage(C,n)/.(k+1) in LSeg(Cage(C,n),k) by A2,A3,A12,A25,A32,TOPREAL1:27;
then Cage(C,n)/.(k+1) in {Cage(C,n)/.k}
by A18,A23,A28,A31,A33,A34,A35,A40,A41,NAT_1:38,XBOOLE_0:def
3;
then Cage(C,n)/.(k+1) = Cage(C,n)/.k by TARSKI:def 1;
hence contradiction by A15,A16,A17,A18,A39,GOBOARD1:21;
end;
then Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A20,GOBOARD5:3
.= Gauge(C,n)*(i2,j2)`1 by A21,GOBOARD5:3;
hence thesis by A4,A16,A18,PSCOMP_1:84;
end;