Copyright (c) 2001 Association of Mizar Users
environ
vocabulary REALSET1, FINSEQ_1, BOOLE, RELAT_1, FINSEQ_5, MATRIX_1, GOBOARD1,
FINSEQ_4, RFINSEQ, COMPTS_1, RELAT_2, SPPOL_1, EUCLID, JORDAN1E, JORDAN8,
JORDAN9, FINSEQ_6, PSCOMP_1, TOPREAL1, GOBOARD5, MCART_1, TREES_1,
FUNCT_1, ARYTM_1, CARD_1, PRE_TOPC, ARYTM_3, GROUP_1, JORDAN1A, SPPOL_2,
JORDAN3, SPRECT_2, GROUP_2, JORDAN5C, JORDAN6;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, XREAL_0, REAL_1, NAT_1,
FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_1,
REALSET1, FINSEQ_6, STRUCT_0, PRE_TOPC, CARD_1, CARD_4, BINARITH,
CONNSP_1, COMPTS_1, EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1,
GOBOARD5, SPPOL_1, SPPOL_2, JORDAN3, JORDAN8, JORDAN5C, JORDAN6, JORDAN9,
JORDAN1A, JORDAN1E;
constructors JORDAN8, REALSET1, JORDAN6, REAL_1, CARD_4, PSCOMP_1, BINARITH,
CONNSP_1, JORDAN9, JORDAN1A, WSIERP_1, FINSEQ_4, GOBRD13, JORDAN3,
RFINSEQ, TOPS_2, TOPMETR, TOPREAL2, JORDAN5C, SPRECT_1, FINSEQ_5,
ENUMSET1, FINSOP_1, JORDAN1E, INT_1;
clusters XREAL_0, SPRECT_1, TOPREAL6, JORDAN8, REVROT_1, RELSET_1, ARYTM_3,
SUBSET_1, FINSEQ_6, SPRECT_3, AMISTD_1, GOBOARD1, FINSEQ_1, FINSEQ_5,
SPPOL_2, JORDAN1A, GOBOARD4, JORDAN1E, BINARITH, REALSET1, MEMBERED,
ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, XBOOLE_0;
theorems AXIOMS, BINARITH, EUCLID, JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, REAL_1,
GOBOARD5, REAL_2, 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, BOOLMARK, JORDAN5B, AMI_5,
JORDAN3, JORDAN9, ZFMISC_1, GOBOARD1, SPRECT_1, TARSKI, TOPREAL3,
FINSEQ_3, RELAT_1, FUNCT_1, TOPREAL5, JORDAN10, GOBOARD2, CARD_1, CARD_2,
YELLOW_6, PRE_CIRC, ENUMSET1, GROUP_5, SPRECT_4, JORDAN1B, SPRECT_5,
SCMFSA_7, JORDAN5D, JORDAN1E, PARTFUN2, JORDAN1F, JORDAN5C, REALSET1,
XBOOLE_0, XBOOLE_1, SQUARE_1, XCMPLX_0, XCMPLX_1, RLVECT_1;
schemes BINARITH;
begin
reserve n for Nat;
definition
cluster trivial FinSequence;
existence
proof
take {};
thus thesis;
end;
end;
theorem Th1:
for f be trivial FinSequence holds
f is empty or ex x be set st f = <*x*>
proof
let f be trivial FinSequence;
assume f is non empty;
then consider x be set such that
A1: f = {x} by REALSET1:def 12;
x in {x} by TARSKI:def 1;
then consider y,z be set such that
A2: x = [y,z] by A1,RELAT_1:def 1;
take z;
A3: 1 in dom f by A1,FINSEQ_5:6;
dom f = {y} by A1,A2,RELAT_1:23;
then 1 = y by A3,TARSKI:def 1;
hence f = <*z*> by A1,A2,FINSEQ_1:def 5;
end;
definition
let p be non trivial FinSequence;
cluster Rev p -> non trivial;
coherence
proof
assume A1: Rev p is trivial;
per cases by A1,Th1;
suppose Rev p is empty;
hence contradiction;
suppose ex x be set st Rev p = <*x*>;
then consider x be set such that
A2: Rev p = <*x*>;
p = Rev <*x*> by A2,FINSEQ_6:29
.= <*x*> by FINSEQ_5:63;
hence contradiction;
end;
end;
theorem Th2:
for D be non empty set
for f be FinSequence of D
for G be Matrix of D
for p be set holds
f is_sequence_on G implies f-:p is_sequence_on G
proof
let D be non empty set;
let f be FinSequence of D;
let G be Matrix of D;
let p be set;
assume f is_sequence_on G;
then f|(p..f) is_sequence_on G by GOBOARD1:38;
hence f-:p is_sequence_on G by FINSEQ_5:def 1;
end;
theorem Th3:
for D be non empty set
for f be FinSequence of D
for G be Matrix of D
for p be Element of D st p in rng f holds
f is_sequence_on G implies f:-p is_sequence_on G
proof
let D be non empty set;
let f be FinSequence of D;
let G be Matrix of D;
let p be Element of D;
assume that
A1: p in rng f and
A2: f is_sequence_on G;
consider i be Nat such that
i+1 = p..f and
A3: f:-p = f/^i by A1,FINSEQ_5:52;
thus f:-p is_sequence_on G by A2,A3,JORDAN8:5;
end;
theorem Th4:
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
Upper_Seq(C,n) is_sequence_on Gauge(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then Rotate(Cage(C,n),W-min L~Cage(C,n)) is_sequence_on Gauge(C,n)
by REVROT_1:34;
then Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n)
is_sequence_on Gauge(C,n) by Th2;
hence thesis by JORDAN1E:def 1;
end;
theorem Th5:
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
Lower_Seq(C,n) is_sequence_on Gauge(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
A1: 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 A2: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A1,FINSEQ_6:96;
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then Rotate(Cage(C,n),W-min L~Cage(C,n)) is_sequence_on Gauge(C,n)
by REVROT_1:34;
then Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n)
is_sequence_on Gauge(C,n) by A2,Th3;
hence thesis by JORDAN1E:def 2;
end;
definition
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
cluster Upper_Seq(C,n) -> standard;
coherence
proof
Upper_Seq(C,n) is_sequence_on Gauge(C,n) by Th4;
hence thesis by JORDAN8:7;
end;
cluster Lower_Seq(C,n) -> standard;
coherence
proof
Lower_Seq(C,n) is_sequence_on Gauge(C,n) by Th5;
hence thesis by JORDAN8:7;
end;
end;
theorem Th6:
for G be Y_equal-in-column Y_increasing-in-line Matrix of TOP-REAL 2
for i1,i2,j1,j2 be Nat st [i1,j1] in Indices G & [i2,j2] in Indices G holds
G*(i1,j1)`2 = G*(i2,j2)`2 implies j1 = j2
proof
let G be Y_equal-in-column Y_increasing-in-line Matrix of TOP-REAL 2;
let i1,i2,j1,j2 be Nat;
assume that
A1: [i1,j1] in Indices G and
A2: [i2,j2] in Indices G and
A3: G*(i1,j1)`2 = G*(i2,j2)`2 and
A4: j1 <> j2;
A5: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A1,GOBOARD5:1;
A6: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A2,GOBOARD5:1;
then A7: G*(i1,j2)`2 = G*(1,j2)`2 by A5,GOBOARD5:2
.= G*(i2,j2)`2 by A6,GOBOARD5:2;
j1 < j2 or j1 > j2 by A4,REAL_1:def 5;
hence contradiction by A3,A5,A6,A7,GOBOARD5:5;
end;
theorem Th7:
for G be X_equal-in-line X_increasing-in-column Matrix of TOP-REAL 2
for i1,i2,j1,j2 be Nat st [i1,j1] in Indices G & [i2,j2] in Indices G holds
G*(i1,j1)`1 = G*(i2,j2)`1 implies i1 = i2
proof
let G be X_equal-in-line X_increasing-in-column Matrix of TOP-REAL 2;
let i1,i2,j1,j2 be Nat;
assume that
A1: [i1,j1] in Indices G and
A2: [i2,j2] in Indices G and
A3: G*(i1,j1)`1 = G*(i2,j2)`1 and
A4: i1 <> i2;
A5: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A1,GOBOARD5:1;
A6: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A2,GOBOARD5:1;
A7: G*(i1,j1)`1 = G*(i1,1)`1 by A5,GOBOARD5:3
.= G*(i1,j2)`1 by A5,A6,GOBOARD5:3;
i1 < i2 or i1 > i2 by A4,REAL_1:def 5;
hence contradiction by A3,A5,A6,A7,GOBOARD5:4;
end;
canceled 8;
theorem Th16:
for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
st (f/.1 <> N-min L~f & f/.len f <> N-min L~f) or
(f/.1 <> N-max L~f & f/.len f <> N-max L~f) holds
(N-min L~f)`1 < (N-max L~f)`1
proof
let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2);
set p = N-min L~f;
set i = p..f;
assume A1: (f/.1 <> N-min L~f & f/.len f <> N-min L~f) or
(f/.1 <> N-max L~f & f/.len f <> N-max L~f);
A2: len f >= 2 by SPPOL_1:2;
A3: p in rng f by SPRECT_2:43;
then A4: i in dom f by FINSEQ_4:30;
A5: p = f.i by A3,FINSEQ_4:29
.= f/.i by A4,FINSEQ_4:def 4;
A6: 1 <= i & i <= len f by A4,FINSEQ_3:27;
A7: p`2 = N-bound L~f by PSCOMP_1:94;
per cases by A6,REAL_1:def 5;
suppose A8: i = 1;
p`2 = (N-max L~f)`2 by PSCOMP_1:95;
then A9: p`1 <> (N-max L~f)`1 by A1,A5,A8,TOPREAL3:11;
p`1 <= (N-max L~f)`1 by PSCOMP_1:97;
hence p`1 < (N-max L~f)`1 by A9,REAL_1:def 5;
suppose A10: i = len f;
p`2 = (N-max L~f)`2 by PSCOMP_1:95;
then A11: p`1 <> (N-max L~f)`1 by A1,A5,A10,TOPREAL3:11;
p`1 <= (N-max L~f)`1 by PSCOMP_1:97;
hence p`1 < (N-max L~f)`1 by A11,REAL_1:def 5;
suppose that
A12: 1 < i and
A13: i < len f;
A14: i-'1+1 = i by A12,AMI_5:4;
then A15: i-'1 >= 1 by A12,NAT_1:38;
i-'1 <= i by A14,NAT_1:29;
then i-'1 <= len f by A13,AXIOMS:22;
then A16: i-'1 in dom f by A15,FINSEQ_3:27;
A17: p in LSeg(f,i-'1) by A5,A13,A14,A15,TOPREAL1:27;
A18: i+1 <= len f by A13,NAT_1:38;
then A19: p in LSeg(f,i) by A5,A12,TOPREAL1:27;
A20: p <> f/.(i-'1) by A4,A5,A14,A16,GOBOARD7:31;
i+1 >= 1 by NAT_1:29;
then A21: i+1 in dom f by A18,FINSEQ_3:27;
then A22: p <> f/.(i+1) by A4,A5,GOBOARD7:31;
A23: f/.(i-'1) in LSeg(f,i-'1) by A13,A14,A15,TOPREAL1:27;
A24: f/.(i+1) in LSeg(f,i) by A12,A18,TOPREAL1:27;
A25: f/.(i-'1) in L~f by A2,A16,GOBOARD1:16;
A26: f/.(i+1) in L~f by A2,A21,GOBOARD1:16;
A27: not(LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical)
proof
assume that
A28: LSeg(f,i-'1) is vertical and
A29: LSeg(f,i) is vertical;
A30: i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1;
A31: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A12,A18,TOPREAL1:def 5;
A32: LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A13,A14,A15,TOPREAL1:def 5;
A33: p`1 = (f/.(i+1))`1 & p`1 = (f/.(i-'1))`1
by A17,A19,A23,A24,A28,A29,SPPOL_1:def 3;
A34: p`2 >= (f/.(i+1))`2 & p`2 >= (f/.(i-'1))`2
by A7,A25,A26,PSCOMP_1:71;
(f/.(i+1))`2 <= (f/.(i-'1))`2 or (f/.(i+1))`2 >= (f/.(i-'1))`2;
then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1)
by A5,A31,A32,A33,A34,GOBOARD7:8;
then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or
f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A23,A24,XBOOLE_0:def 3;
then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A20,A22,TARSKI:def 1;
hence contradiction by A14,A15,A18,A30,TOPREAL1:def 8;
end;
now per cases by A27,SPPOL_1:41;
suppose LSeg(f,i-'1) is horizontal;
then A35: p`2 = (f/.(i-'1))`2 by A17,A23,SPPOL_1:def 2;
then A36: (f/.(i-'1))`1 <> p`1 by A20,TOPREAL3:11;
A37: f/.(i-'1) in N-most L~f by A7,A25,A35,SPRECT_2:14;
then (f/.(i-'1))`1 >= p`1 by PSCOMP_1:98;
then A38: (f/.(i-'1))`1 > p`1 by A36,REAL_1:def 5;
(f/.(i-'1))`1 <= (N-max L~f)`1 by A37,PSCOMP_1:98;
hence thesis by A38,AXIOMS:22;
suppose LSeg(f,i) is horizontal;
then A39: p`2 = (f/.(i+1))`2 by A19,A24,SPPOL_1:def 2;
then A40: (f/.(i+1))`1 <> p`1 by A22,TOPREAL3:11;
A41: f/.(i+1) in N-most L~f by A7,A26,A39,SPRECT_2:14;
then (f/.(i+1))`1 >= p`1 by PSCOMP_1:98;
then A42: (f/.(i+1))`1 > p`1 by A40,REAL_1:def 5;
(f/.(i+1))`1 <= (N-max L~f)`1 by A41,PSCOMP_1:98;
hence thesis by A42,AXIOMS:22;
end;
hence thesis;
end;
theorem
for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
st (f/.1 <> N-min L~f & f/.len f <> N-min L~f) or
(f/.1 <> N-max L~f & f/.len f <> N-max L~f) holds
N-min L~f <> N-max L~f
proof
let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2);
assume (f/.1 <> N-min L~f & f/.len f <> N-min L~f) or
(f/.1 <> N-max L~f & f/.len f <> N-max L~f);
then (N-min L~f)`1 < (N-max L~f)`1 by Th16;
hence thesis;
end;
theorem Th18:
for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
st (f/.1 <> S-min L~f & f/.len f <> S-min L~f) or
(f/.1 <> S-max L~f & f/.len f <> S-max L~f) holds
(S-min L~f)`1 < (S-max L~f)`1
proof
let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2);
set p = S-min L~f;
set i = p..f;
assume A1: (f/.1 <> S-min L~f & f/.len f <> S-min L~f) or
(f/.1 <> S-max L~f & f/.len f <> S-max L~f);
A2: len f >= 2 by SPPOL_1:2;
A3: p in rng f by SPRECT_2:45;
then A4: i in dom f by FINSEQ_4:30;
A5: p = f.i by A3,FINSEQ_4:29
.= f/.i by A4,FINSEQ_4:def 4;
A6: 1 <= i & i <= len f by A4,FINSEQ_3:27;
A7: p`2 = S-bound L~f by PSCOMP_1:114;
per cases by A6,REAL_1:def 5;
suppose A8: i = 1;
p`2 = (S-max L~f)`2 by PSCOMP_1:115;
then A9: p`1 <> (S-max L~f)`1 by A1,A5,A8,TOPREAL3:11;
p`1 <= (S-max L~f)`1 by PSCOMP_1:117;
hence p`1 < (S-max L~f)`1 by A9,REAL_1:def 5;
suppose A10: i = len f;
p`2 = (S-max L~f)`2 by PSCOMP_1:115;
then A11: p`1 <> (S-max L~f)`1 by A1,A5,A10,TOPREAL3:11;
p`1 <= (S-max L~f)`1 by PSCOMP_1:117;
hence p`1 < (S-max L~f)`1 by A11,REAL_1:def 5;
suppose that
A12: 1 < i and
A13: i < len f;
A14: i-'1+1 = i by A12,AMI_5:4;
then A15: i-'1 >= 1 by A12,NAT_1:38;
i-'1 <= i by A14,NAT_1:29;
then i-'1 <= len f by A13,AXIOMS:22;
then A16: i-'1 in dom f by A15,FINSEQ_3:27;
A17: p in LSeg(f,i-'1) by A5,A13,A14,A15,TOPREAL1:27;
A18: i+1 <= len f by A13,NAT_1:38;
then A19: p in LSeg(f,i) by A5,A12,TOPREAL1:27;
A20: p <> f/.(i-'1) by A4,A5,A14,A16,GOBOARD7:31;
i+1 >= 1 by NAT_1:29;
then A21: i+1 in dom f by A18,FINSEQ_3:27;
then A22: p <> f/.(i+1) by A4,A5,GOBOARD7:31;
A23: f/.(i-'1) in LSeg(f,i-'1) by A13,A14,A15,TOPREAL1:27;
A24: f/.(i+1) in LSeg(f,i) by A12,A18,TOPREAL1:27;
A25: f/.(i-'1) in L~f by A2,A16,GOBOARD1:16;
A26: f/.(i+1) in L~f by A2,A21,GOBOARD1:16;
A27: not(LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical)
proof
assume that
A28: LSeg(f,i-'1) is vertical and
A29: LSeg(f,i) is vertical;
A30: i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1;
A31: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A12,A18,TOPREAL1:def 5;
A32: LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A13,A14,A15,TOPREAL1:def 5;
A33: p`1 = (f/.(i+1))`1 & p`1 = (f/.(i-'1))`1
by A17,A19,A23,A24,A28,A29,SPPOL_1:def 3;
A34: p`2 <= (f/.(i+1))`2 & p`2 <= (f/.(i-'1))`2
by A7,A25,A26,PSCOMP_1:71;
(f/.(i+1))`2 <= (f/.(i-'1))`2 or (f/.(i+1))`2 >= (f/.(i-'1))`2;
then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1)
by A5,A31,A32,A33,A34,GOBOARD7:8;
then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or
f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A23,A24,XBOOLE_0:def 3;
then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A20,A22,TARSKI:def 1;
hence contradiction by A14,A15,A18,A30,TOPREAL1:def 8;
end;
now per cases by A27,SPPOL_1:41;
suppose LSeg(f,i-'1) is horizontal;
then A35: p`2 = (f/.(i-'1))`2 by A17,A23,SPPOL_1:def 2;
then A36: (f/.(i-'1))`1 <> p`1 by A20,TOPREAL3:11;
A37: f/.(i-'1) in S-most L~f by A7,A25,A35,SPRECT_2:15;
then (f/.(i-'1))`1 >= p`1 by PSCOMP_1:118;
then A38: (f/.(i-'1))`1 > p`1 by A36,REAL_1:def 5;
(f/.(i-'1))`1 <= (S-max L~f)`1 by A37,PSCOMP_1:118;
hence thesis by A38,AXIOMS:22;
suppose LSeg(f,i) is horizontal;
then A39: p`2 = (f/.(i+1))`2 by A19,A24,SPPOL_1:def 2;
then A40: (f/.(i+1))`1 <> p`1 by A22,TOPREAL3:11;
A41: f/.(i+1) in S-most L~f by A7,A26,A39,SPRECT_2:15;
then (f/.(i+1))`1 >= p`1 by PSCOMP_1:118;
then A42: (f/.(i+1))`1 > p`1 by A40,REAL_1:def 5;
(f/.(i+1))`1 <= (S-max L~f)`1 by A41,PSCOMP_1:118;
hence thesis by A42,AXIOMS:22;
end;
hence thesis;
end;
theorem
for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
st (f/.1 <> S-min L~f & f/.len f <> S-min L~f) or
(f/.1 <> S-max L~f & f/.len f <> S-max L~f) holds
S-min L~f <> S-max L~f
proof
let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2);
assume (f/.1 <> S-min L~f & f/.len f <> S-min L~f) or
(f/.1 <> S-max L~f & f/.len f <> S-max L~f);
then (S-min L~f)`1 < (S-max L~f)`1 by Th18;
hence thesis;
end;
theorem Th20:
for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
st (f/.1 <> W-min L~f & f/.len f <> W-min L~f) or
(f/.1 <> W-max L~f & f/.len f <> W-max L~f) holds
(W-min L~f)`2 < (W-max L~f)`2
proof
let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2);
set p = W-min L~f;
set i = p..f;
assume A1: (f/.1 <> W-min L~f & f/.len f <> W-min L~f) or
(f/.1 <> W-max L~f & f/.len f <> W-max L~f);
A2: len f >= 2 by SPPOL_1:2;
A3: p in rng f by SPRECT_2:47;
then A4: i in dom f by FINSEQ_4:30;
A5: p = f.i by A3,FINSEQ_4:29
.= f/.i by A4,FINSEQ_4:def 4;
A6: 1 <= i & i <= len f by A4,FINSEQ_3:27;
A7: p`1 = W-bound L~f by PSCOMP_1:84;
per cases by A6,REAL_1:def 5;
suppose A8: i = 1;
p`1 = (W-max L~f)`1 by PSCOMP_1:85;
then A9: p`2 <> (W-max L~f)`2 by A1,A5,A8,TOPREAL3:11;
p`2 <= (W-max L~f)`2 by PSCOMP_1:87;
hence p`2 < (W-max L~f)`2 by A9,REAL_1:def 5;
suppose A10: i = len f;
p`1 = (W-max L~f)`1 by PSCOMP_1:85;
then A11: p`2 <> (W-max L~f)`2 by A1,A5,A10,TOPREAL3:11;
p`2 <= (W-max L~f)`2 by PSCOMP_1:87;
hence p`2 < (W-max L~f)`2 by A11,REAL_1:def 5;
suppose that
A12: 1 < i and
A13: i < len f;
A14: i-'1+1 = i by A12,AMI_5:4;
then A15: i-'1 >= 1 by A12,NAT_1:38;
i-'1 <= i by A14,NAT_1:29;
then i-'1 <= len f by A13,AXIOMS:22;
then A16: i-'1 in dom f by A15,FINSEQ_3:27;
A17: p in LSeg(f,i-'1) by A5,A13,A14,A15,TOPREAL1:27;
A18: i+1 <= len f by A13,NAT_1:38;
then A19: p in LSeg(f,i) by A5,A12,TOPREAL1:27;
A20: p <> f/.(i-'1) by A4,A5,A14,A16,GOBOARD7:31;
i+1 >= 1 by NAT_1:29;
then A21: i+1 in dom f by A18,FINSEQ_3:27;
then A22: p <> f/.(i+1) by A4,A5,GOBOARD7:31;
A23: f/.(i-'1) in LSeg(f,i-'1) by A13,A14,A15,TOPREAL1:27;
A24: f/.(i+1) in LSeg(f,i) by A12,A18,TOPREAL1:27;
A25: f/.(i-'1) in L~f by A2,A16,GOBOARD1:16;
A26: f/.(i+1) in L~f by A2,A21,GOBOARD1:16;
A27: not(LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal)
proof
assume that
A28: LSeg(f,i-'1) is horizontal and
A29: LSeg(f,i) is horizontal;
A30: i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1;
A31: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A12,A18,TOPREAL1:def 5;
A32: LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A13,A14,A15,TOPREAL1:def 5;
A33: p`2 = (f/.(i+1))`2 & p`2 = (f/.(i-'1))`2
by A17,A19,A23,A24,A28,A29,SPPOL_1:def 2;
A34: p`1 <= (f/.(i+1))`1 & p`1 <= (f/.(i-'1))`1
by A7,A25,A26,PSCOMP_1:71;
(f/.(i+1))`1 <= (f/.(i-'1))`1 or (f/.(i+1))`1 >= (f/.(i-'1))`1;
then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1)
by A5,A31,A32,A33,A34,GOBOARD7:9;
then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or
f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A23,A24,XBOOLE_0:def 3;
then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A20,A22,TARSKI:def 1;
hence contradiction by A14,A15,A18,A30,TOPREAL1:def 8;
end;
now per cases by A27,SPPOL_1:41;
suppose LSeg(f,i-'1) is vertical;
then A35: p`1 = (f/.(i-'1))`1 by A17,A23,SPPOL_1:def 3;
then A36: (f/.(i-'1))`2 <> p`2 by A20,TOPREAL3:11;
A37: f/.(i-'1) in W-most L~f by A7,A25,A35,SPRECT_2:16;
then (f/.(i-'1))`2 >= p`2 by PSCOMP_1:88;
then A38: (f/.(i-'1))`2 > p`2 by A36,REAL_1:def 5;
(f/.(i-'1))`2 <= (W-max L~f)`2 by A37,PSCOMP_1:88;
hence thesis by A38,AXIOMS:22;
suppose LSeg(f,i) is vertical;
then A39: p`1 = (f/.(i+1))`1 by A19,A24,SPPOL_1:def 3;
then A40: (f/.(i+1))`2 <> p`2 by A22,TOPREAL3:11;
A41: f/.(i+1) in W-most L~f by A7,A26,A39,SPRECT_2:16;
then (f/.(i+1))`2 >= p`2 by PSCOMP_1:88;
then A42: (f/.(i+1))`2 > p`2 by A40,REAL_1:def 5;
(f/.(i+1))`2 <= (W-max L~f)`2 by A41,PSCOMP_1:88;
hence thesis by A42,AXIOMS:22;
end;
hence thesis;
end;
theorem
for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
st (f/.1 <> W-min L~f & f/.len f <> W-min L~f) or
(f/.1 <> W-max L~f & f/.len f <> W-max L~f) holds
W-min L~f <> W-max L~f
proof
let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2);
assume (f/.1 <> W-min L~f & f/.len f <> W-min L~f) or
(f/.1 <> W-max L~f & f/.len f <> W-max L~f);
then (W-min L~f)`2 < (W-max L~f)`2 by Th20;
hence thesis;
end;
theorem Th22:
for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
st (f/.1 <> E-min L~f & f/.len f <> E-min L~f) or
(f/.1 <> E-max L~f & f/.len f <> E-max L~f) holds
(E-min L~f)`2 < (E-max L~f)`2
proof
let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2);
set p = E-min L~f;
set i = p..f;
assume A1: (f/.1 <> E-min L~f & f/.len f <> E-min L~f) or
(f/.1 <> E-max L~f & f/.len f <> E-max L~f);
A2: len f >= 2 by SPPOL_1:2;
A3: p in rng f by SPRECT_2:49;
then A4: i in dom f by FINSEQ_4:30;
A5: p = f.i by A3,FINSEQ_4:29
.= f/.i by A4,FINSEQ_4:def 4;
A6: 1 <= i & i <= len f by A4,FINSEQ_3:27;
A7: p`1 = E-bound L~f by PSCOMP_1:104;
per cases by A6,REAL_1:def 5;
suppose A8: i = 1;
p`1 = (E-max L~f)`1 by PSCOMP_1:105;
then A9: p`2 <> (E-max L~f)`2 by A1,A5,A8,TOPREAL3:11;
p`2 <= (E-max L~f)`2 by PSCOMP_1:107;
hence p`2 < (E-max L~f)`2 by A9,REAL_1:def 5;
suppose A10: i = len f;
p`1 = (E-max L~f)`1 by PSCOMP_1:105;
then A11: p`2 <> (E-max L~f)`2 by A1,A5,A10,TOPREAL3:11;
p`2 <= (E-max L~f)`2 by PSCOMP_1:107;
hence p`2 < (E-max L~f)`2 by A11,REAL_1:def 5;
suppose that
A12: 1 < i and
A13: i < len f;
A14: i-'1+1 = i by A12,AMI_5:4;
then A15: i-'1 >= 1 by A12,NAT_1:38;
i-'1 <= i by A14,NAT_1:29;
then i-'1 <= len f by A13,AXIOMS:22;
then A16: i-'1 in dom f by A15,FINSEQ_3:27;
A17: p in LSeg(f,i-'1) by A5,A13,A14,A15,TOPREAL1:27;
A18: i+1 <= len f by A13,NAT_1:38;
then A19: p in LSeg(f,i) by A5,A12,TOPREAL1:27;
A20: p <> f/.(i-'1) by A4,A5,A14,A16,GOBOARD7:31;
i+1 >= 1 by NAT_1:29;
then A21: i+1 in dom f by A18,FINSEQ_3:27;
then A22: p <> f/.(i+1) by A4,A5,GOBOARD7:31;
A23: f/.(i-'1) in LSeg(f,i-'1) by A13,A14,A15,TOPREAL1:27;
A24: f/.(i+1) in LSeg(f,i) by A12,A18,TOPREAL1:27;
A25: f/.(i-'1) in L~f by A2,A16,GOBOARD1:16;
A26: f/.(i+1) in L~f by A2,A21,GOBOARD1:16;
A27: not(LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal)
proof
assume that
A28: LSeg(f,i-'1) is horizontal and
A29: LSeg(f,i) is horizontal;
A30: i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1;
A31: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A12,A18,TOPREAL1:def 5;
A32: LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A13,A14,A15,TOPREAL1:def 5;
A33: p`2 = (f/.(i+1))`2 & p`2 = (f/.(i-'1))`2
by A17,A19,A23,A24,A28,A29,SPPOL_1:def 2;
A34: p`1 >= (f/.(i+1))`1 & p`1 >= (f/.(i-'1))`1
by A7,A25,A26,PSCOMP_1:71;
(f/.(i+1))`1 <= (f/.(i-'1))`1 or (f/.(i+1))`1 >= (f/.(i-'1))`1;
then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1)
by A5,A31,A32,A33,A34,GOBOARD7:9;
then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or
f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A23,A24,XBOOLE_0:def 3;
then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A20,A22,TARSKI:def 1;
hence contradiction by A14,A15,A18,A30,TOPREAL1:def 8;
end;
now per cases by A27,SPPOL_1:41;
suppose LSeg(f,i-'1) is vertical;
then A35: p`1 = (f/.(i-'1))`1 by A17,A23,SPPOL_1:def 3;
then A36: (f/.(i-'1))`2 <> p`2 by A20,TOPREAL3:11;
A37: f/.(i-'1) in E-most L~f by A7,A25,A35,SPRECT_2:17;
then (f/.(i-'1))`2 >= p`2 by PSCOMP_1:108;
then A38: (f/.(i-'1))`2 > p`2 by A36,REAL_1:def 5;
(f/.(i-'1))`2 <= (E-max L~f)`2 by A37,PSCOMP_1:108;
hence thesis by A38,AXIOMS:22;
suppose LSeg(f,i) is vertical;
then A39: p`1 = (f/.(i+1))`1 by A19,A24,SPPOL_1:def 3;
then A40: (f/.(i+1))`2 <> p`2 by A22,TOPREAL3:11;
A41: f/.(i+1) in E-most L~f by A7,A26,A39,SPRECT_2:17;
then (f/.(i+1))`2 >= p`2 by PSCOMP_1:108;
then A42: (f/.(i+1))`2 > p`2 by A40,REAL_1:def 5;
(f/.(i+1))`2 <= (E-max L~f)`2 by A41,PSCOMP_1:108;
hence thesis by A42,AXIOMS:22;
end;
hence thesis;
end;
theorem
for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
st (f/.1 <> E-min L~f & f/.len f <> E-min L~f) or
(f/.1 <> E-max L~f & f/.len f <> E-max L~f) holds
E-min L~f <> E-max L~f
proof
let f be standard special unfolded (non trivial FinSequence of TOP-REAL 2);
assume (f/.1 <> E-min L~f & f/.len f <> E-min L~f) or
(f/.1 <> E-max L~f & f/.len f <> E-max L~f);
then (E-min L~f)`2 < (E-max L~f)`2 by Th22;
hence thesis;
end;
theorem Th24:
for D be non empty set
for f be FinSequence of D
for p,q be Element of D st p in rng f & q in rng f & q..f <= p..f holds
(f-:p):-q = (f:-q)-:p
proof
let D be non empty set;
let f be FinSequence of D;
let p,q be Element of D;
A1: f-:p = f|(p..f) by FINSEQ_5:def 1;
assume that
A2: p in rng f and
A3: q in rng f and
A4: q..f <= p..f;
consider i be Nat such that
A5: i+1 = q..f and
A6: f:-q = f/^i by A3,FINSEQ_5:52;
q in rng (f-:p) by A2,A3,A4,FINSEQ_5:49;
then consider j be Nat such that
A7: j+1 = q..(f-:p) and
A8: (f-:p):-q = (f-:p)/^j by FINSEQ_5:52;
A9: (f:-q)-:p = (f:-q)|(p..(f:-q)) by FINSEQ_5:def 1;
A10: i < p..f by A4,A5,NAT_1:38;
then p..f = i + p..(f/^i) by A2,FINSEQ_6:61;
then A11: p..(f/^i) = p..f-i by XCMPLX_1:26
.= p..f-'i by A10,SCMFSA_7:3;
q..(f-:p) = q..f by A2,A3,A4,SPRECT_5:3;
then i = j by A5,A7,XCMPLX_1:2;
hence (f-:p):-q = (f:-q)-:p by A1,A6,A8,A9,A11,JORDAN3:21;
end;
theorem Th25:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for n be Nat holds
L~(Cage(C,n)-:W-min L~Cage(C,n)) /\ L~(Cage(C,n):-W-min L~Cage(C,n)) =
{N-min 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;
let n be Nat;
set US = Cage(C,n)-:W-min L~Cage(C,n);
set LS = Cage(C,n):-W-min L~Cage(C,n);
set f=Cage(C,n);
set pW=W-min L~Cage(C,n);
set pN=N-min L~Cage(C,n);
set pNa=N-max L~Cage(C,n);
set pSa=S-max L~Cage(C,n);
set pSi=S-min L~Cage(C,n);
set pEa=E-max L~Cage(C,n);
set pEi=E-min L~Cage(C,n);
A1: N-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:44;
A2: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
A3: (W-min L~Cage(C,n))..Cage(C,n) <= (W-min L~Cage(C,n))..Cage(C,n);
(f:-pW)/.len(f:-pW) = f/.len f by A2,FINSEQ_5:57
.= f/.1 by FINSEQ_6:def 1
.= pN by JORDAN9:34;
then A4: pN in rng (Cage(C,n):-pW) by REVROT_1:3;
A5: Cage(C,n)-:pW <> {} by A2,FINSEQ_5:50;
(Cage(C,n):-pW)/.1 = pW by FINSEQ_5:56;
then A6: W-min L~Cage(C,n) in rng (Cage(C,n):-W-min L~Cage(C,n))
by FINSEQ_6:46;
(Cage(C,n)-:pW)/.1 = Cage(C,n)/.1 by A2,FINSEQ_5:47
.= pN by JORDAN9:34;
then A7: N-min L~Cage(C,n) in rng (Cage(C,n)-:W-min L~Cage(C,n))
by A5,FINSEQ_6:46;
A8: f/.1 = pN by JORDAN9:34;
then A9: pNa..f <= pEa..f by SPRECT_2:74;
A10: pEa..f < pEi..f by A8,SPRECT_2:75;
A11: pEi..f <= pSa..f by A8,SPRECT_2:76;
A12: pSa..f < pSi..f by A8,SPRECT_2:77;
A13: pSi..f <= pW..f by A8,SPRECT_2:78;
pNa..f < pEi..f by A9,A10,AXIOMS:22;
then pNa..f < pSa..f by A11,AXIOMS:22;
then pNa..f < pSi..f by A12,AXIOMS:22;
then pNa..f <= pW..f by A13,AXIOMS:22;
then A14: pNa in rng (f-:pW) by A1,A2,FINSEQ_5:49;
len(f-:pW) = pW..f by A2,FINSEQ_5:45;
then (f-:pW)/.len (f-:pW) = pW by A2,FINSEQ_5:48;
then A15: pW in rng (Cage(C,n)-:pW) by A5,REVROT_1:3;
W-max L~f in L~f & pN`2 = N-bound L~f by PSCOMP_1:94,SPRECT_1:15;
then (W-max L~f)`2 <= pN`2 by PSCOMP_1:71;
then A16: pN <> pW by SPRECT_2:61;
then A17: 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 A4,A6,TARSKI:def 2;
end;
then A18: 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 A17,A18,XBOOLE_1:1;
then len LS >= 2 by CARD_1:56;
then A19: rng LS c= L~LS by SPPOL_2:18;
A20: W-min L~Cage(C,n) in rng LS by FINSEQ_6:66;
A21: pN <> pNa by SPRECT_2:56;
W-max L~f in L~f & pNa`2 = N-bound L~f by PSCOMP_1:94,SPRECT_1:15;
then (W-max L~f)`2 <= pNa`2 by PSCOMP_1:71;
then pNa <> pW by SPRECT_2:61;
then A22: Card {pN,pNa,pW} = 3 by A16,A21,CARD_2:77;
{pN,pNa,pW} c= rng US
proof
let x be set;
assume x in {pN,pNa,pW};
hence x in rng US by A7,A14,A15,ENUMSET1:def 1;
end;
then A23: Card {pN,pNa,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 A24: 3 c= len US by A22,A23,XBOOLE_1:1;
then A25: len US >= 3 by CARD_1:56;
then len US >= 2 by AXIOMS:22;
then A26: rng US c= L~US by SPPOL_2:18;
len US <> 0 by A24,CARD_1:56;
then A27: US is non empty by FINSEQ_1:25;
A28: W-min L~Cage(C,n) in rng US by A2,A3,FINSEQ_5:49;
US/.1 = Cage(C,n)/.1 by A2,FINSEQ_5:47
.= N-min L~Cage(C,n) by JORDAN9:34;
then A29: N-min L~Cage(C,n) in rng US by A27,FINSEQ_6:46;
LS/.(len LS) = Cage(C,n)/.len Cage(C,n) by A2,FINSEQ_5:57
.= Cage(C,n)/.1 by FINSEQ_6:def 1
.= N-min L~Cage(C,n) by JORDAN9:34;
then A30: 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),W-min L~Cage(C,n)}
proof
let x be set;
assume A31: x in L~US /\ L~LS;
then A32: x in L~US & x in L~LS by XBOOLE_0:def 3;
reconsider x1=x as Point of TOP-REAL 2 by A31;
consider i1 be Nat such that
A33: 1 <= i1 & i1+1 <= len US and
A34: x1 in LSeg(US,i1) by A32,SPPOL_2:13;
consider i2 be Nat such that
A35: 1 <= i2 & i2+1 <= len LS and
A36: x1 in LSeg(LS,i2) by A32,SPPOL_2:13;
A37: LSeg(US,i1) = LSeg(f,i1) by A33,SPPOL_2:9;
set i3=i2-'1;
A38: i3+1 = i2 by A35,AMI_5:4;
then A39: LSeg(LS,i2) = LSeg(f,i3+pW..f) by A2,SPPOL_2:10;
A40: len US = pW..f by A2,FINSEQ_5:45;
A41: len LS = len f-pW..f+1 by A2,FINSEQ_5:53;
A42: i2-1 >= 1-1 by A35,REAL_1:49;
i2 < len f-pW..f+1 by A35,A41,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 A43: i3+pW..f < len f by A42,BINARITH:def 3;
A44: i3 >= 0 by NAT_1:18;
A45: pW..f >= 1 by A2,FINSEQ_4:31;
i3+1 < len f-pW..f+1 by A35,A38,A41,NAT_1:38;
then i3 < len f-pW..f by REAL_1:55;
then A46: i3+pW..f < len f by REAL_1:86;
A47: i1+1 < pW..f+1 by A33,A40,NAT_1:38;
1+pW..f <= i3+1+pW..f by A35,A38,REAL_1:55;
then i1+1 < i3+1+pW..f by A47,AXIOMS:22;
then i1+1 < i3+pW..f+1 by XCMPLX_1:1;
then A48: i1+1 <= i3+pW..f by NAT_1:38;
A49: i3+pW..f+1 <= len f by A46,NAT_1:38;
A50: len f > 4 by GOBOARD7:36;
A51: i3+pW..f >= 0 & i1 >= 0 by NAT_1:18;
A52: pW..f-'1+1 = pW..f by A45,AMI_5:4;
assume A53: not x in {N-min L~Cage(C,n),W-min L~Cage(C,n)};
now per cases by A33,A48,REAL_1:def 5;
suppose i1+1 < i3+pW..f & i1 > 1;
then LSeg(f,i1) misses LSeg(f,i3+pW..f) by A46,GOBOARD5:def 4;
then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {} by XBOOLE_0:def 7;
hence contradiction by A34,A36,A37,A39,XBOOLE_0:def 3;
suppose A54: i1 = 1;
i3+pW..f >= 0+3 by A25,A40,A44,REAL_1:55;
then A55: i1+1 < i3+pW..f by A54,AXIOMS:22;
now per cases by A49,REAL_1:def 5;
suppose i3+pW..f+1 < len f;
then LSeg(f,i1) misses LSeg(f,i3+pW..f) by A55,GOBOARD5:def 4;
then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {} by XBOOLE_0:def 7;
hence contradiction by A34,A36,A37,A39,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 A51,BINARITH:def 3;
then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {f/.1} by A50,A54,REVROT_1:30;
then x1 in {f/.1} by A34,A36,A37,A39,XBOOLE_0:def 3;
then x1 = f/.1 by TARSKI:def 1
.= pN by JORDAN9:34;
hence contradiction by A53,TARSKI:def 2;
end;
hence contradiction;
suppose A56: i1+1 = i3+pW..f;
0+pW..f <= i3+pW..f by A44,REAL_1:55;
then pW..f = i1+1 by A33,A40,A56,AXIOMS:21;
then i1 = pW..f-1 by XCMPLX_1:26;
then A57: i1 = pW..f-'1 by A51,BINARITH:def 3;
i3+pW..f >= pW..f by NAT_1:29;
then pW..f < len f by A43,AXIOMS:22;
then pW..f+1 <= len f by NAT_1:38;
then pW..f-'1 + (1+1) <= len f by A52,XCMPLX_1:1;
then LSeg(f,i1) /\ LSeg(f,i3+(pW..f)) = {f/.(pW..f)}
by A33,A52,A56,A57,TOPREAL1:def 8;
then x1 in {f/.(pW..f)} by A34,A36,A37,A39,XBOOLE_0:def 3;
then x1 = f/.(pW..f) by TARSKI:def 1
.= pW by A2,FINSEQ_5:41;
hence contradiction by A53,TARSKI:def 2;
end;
hence contradiction;
end;
thus {N-min L~Cage(C,n),W-min L~Cage(C,n)} c= L~US /\ L~LS
proof
let x be set;
assume A58: x in {N-min L~Cage(C,n),W-min L~Cage(C,n)};
per cases by A58,TARSKI:def 2;
suppose x = N-min L~Cage(C,n);
hence x in L~US /\ L~LS by A19,A26,A29,A30,XBOOLE_0:def 3;
suppose x = W-min L~Cage(C,n);
hence x in L~US /\ L~LS by A19,A20,A26,A28,XBOOLE_0:def 3;
end;
end;
theorem Th26:
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
Lower_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 Nmi <> Wmi by SPRECT_2:61;
then A17: 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 A18: 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 A17,A18,XBOOLE_1:1;
then len (Cage(C,n)-:Wmi) >= 2 by CARD_1:56;
then A19: rng (Cage(C,n)-:Wmi) c= L~(Cage(C,n)-:Wmi) by SPPOL_2:18;
A20: Nmi..Cage(C,n) < Wmi..Cage(C,n) by A7,A12,AXIOMS:22;
then A21: Nmi in rng (Cage(C,n)-:Wmi) by A2,A3,FINSEQ_5:49;
A22: Ema..(Cage(C,n)-:Wmi) <> 1
proof
assume A23: Ema..(Cage(C,n)-:Wmi) = 1;
Nmi..(Cage(C,n)-:Wmi) = Nmi..Cage(C,n) by A2,A3,A20,SPRECT_5:3
.= 1 by A1,FINSEQ_6:47;
hence contradiction by A5,A6,A13,A21,A23,FINSEQ_5:10;
end;
then A24: Ema in rng (Cage(C,n)-:Wmi/^1) by A13,FINSEQ_6:83;
A25: 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 A26: Nmi <> Ema by A25,PSCOMP_1:104;
not Ema in rng (Cage(C,n):-Wmi)
proof
assume A27: 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 A28: Nmi in rng (Cage(C,n):-Wmi) by REVROT_1:3;
(Cage(C,n):-Wmi)/.1 = Wmi by FINSEQ_5:56;
then A29: 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 A30: 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 A28,A29,TARSKI:def 2;
end;
then A31: 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 A30,A31,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,A19,A27,XBOOLE_0:def
3;
then Ema in {Nmi,Wmi} by Th25;
then Ema = Wmi by A26,TARSKI:def 2;
hence contradiction by TOPREAL5:25;
end;
then A32: Ema in rng (Cage(C,n)-:Wmi/^1) \ rng (Cage(C,n):-Wmi)
by A24,XBOOLE_0:def 4
;
A33: Wmi in rng (Cage(C,n):-Ema) by A3,A4,A12,FINSEQ_6:67;
RotWmi:-Ema = ((Cage(C,n):-Wmi)^((Cage(C,n)-:Wmi)/^1)):-Ema
by A3,FINSEQ_6:def 2
.= ((Cage(C,n)-:Wmi)/^1):-Ema by A32,FINSEQ_6:70
.= (Cage(C,n)-:Wmi):-Ema by A13,A22,FINSEQ_6:89
.= (Cage(C,n):-Ema)-:Wmi by A3,A4,A12,Th24
.= ((Cage(C,n):-Ema)^((Cage(C,n)-:Ema)/^1))-:Wmi by A33,FINSEQ_6:71
.= RotEma-:Wmi by A4,FINSEQ_6:def 2;
hence Lower_Seq(C,n) = Rotate(Cage(C,n),E-max L~Cage(C,n))-:
W-min L~Cage(C,n) by JORDAN1E:def 2;
end;
theorem Th27:
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
(W-min L~Cage(C,n))..Upper_Seq(C,n) = 1
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by JORDAN1F:5;
hence (W-min L~Cage(C,n))..Upper_Seq(C,n) = 1 by FINSEQ_6:47;
end;
theorem Th28:
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
(W-min L~Cage(C,n))..Upper_Seq(C,n) < (W-max L~Cage(C,n))..Upper_Seq(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
set Wmi = W-min L~Cage(C,n);
set Wma = W-max L~Cage(C,n);
set Nmi = N-min L~Cage(C,n);
set Nma = N-max L~Cage(C,n);
set Ema = E-max L~Cage(C,n);
set Rot = Rotate(Cage(C,n),Wmi);
A1: Upper_Seq(C,n) = Rot-:Ema by JORDAN1E:def 1;
A2: L~Rot = L~Cage(C,n) by REVROT_1:33;
Wmi in rng Cage(C,n) by SPRECT_2:47;
then A3: Rot/.1 = Wmi by FINSEQ_6:98;
A4: Wmi in rng Rot by A2,SPRECT_2:47;
A5: Ema in rng Rot by A2,SPRECT_2:50;
A6: Wmi..Rot < Wma..Rot by A2,A3,SPRECT_5:22;
A7: Wma..Rot <= Nmi..Rot by A2,A3,SPRECT_5:24;
A8: Nmi..Rot < Nma..Rot by A2,A3,SPRECT_5:25;
A9: Nma..Rot <= Ema..Rot by A2,A3,SPRECT_5:26;
Wma..Rot < Nma..Rot by A7,A8,AXIOMS:22;
then A10: Wma..Rot < Ema..Rot by A9,AXIOMS:22;
then Wmi..Rot < Ema..Rot by A6,AXIOMS:22;
then A11: Wmi..(Rot-:Ema) = Wmi..Rot by A4,A5,SPRECT_5:3;
Wma in rng Rot by A2,SPRECT_2:48;
hence (W-min L~Cage(C,n))..Upper_Seq(C,n) <
(W-max L~Cage(C,n))..Upper_Seq(C,n) by A1,A5,A6,A10,A11,SPRECT_5:3;
end;
theorem Th29:
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
(W-max L~Cage(C,n))..Upper_Seq(C,n) <= (N-min L~Cage(C,n))..Upper_Seq(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
set Wmi = W-min L~Cage(C,n);
set Wma = W-max L~Cage(C,n);
set Nmi = N-min L~Cage(C,n);
set Nma = N-max L~Cage(C,n);
set Ema = E-max L~Cage(C,n);
set Rot = Rotate(Cage(C,n),Wmi);
A1: Upper_Seq(C,n) = Rot-:Ema by JORDAN1E:def 1;
A2: L~Rot = L~Cage(C,n) by REVROT_1:33;
Wmi in rng Cage(C,n) by SPRECT_2:47;
then A3: Rot/.1 = Wmi by FINSEQ_6:98;
A4: Wma in rng Rot by A2,SPRECT_2:48;
A5: Ema in rng Rot by A2,SPRECT_2:50;
A6: Wma..Rot <= Nmi..Rot by A2,A3,SPRECT_5:24;
A7: Nmi..Rot < Nma..Rot by A2,A3,SPRECT_5:25;
Nma..Rot <= Ema..Rot by A2,A3,SPRECT_5:26;
then A8: Nmi..Rot < Ema..Rot by A7,AXIOMS:22;
then Wma..Rot < Ema..Rot by A6,AXIOMS:22;
then A9: Wma..(Rot-:Ema) = Wma..Rot by A4,A5,SPRECT_5:3;
Nmi in rng Rot by A2,SPRECT_2:43;
hence (W-max L~Cage(C,n))..Upper_Seq(C,n) <=
(N-min L~Cage(C,n))..Upper_Seq(C,n) by A1,A5,A6,A8,A9,SPRECT_5:3;
end;
theorem Th30:
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
(N-min L~Cage(C,n))..Upper_Seq(C,n) < (N-max L~Cage(C,n))..Upper_Seq(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
set Wmi = W-min L~Cage(C,n);
set Nmi = N-min L~Cage(C,n);
set Nma = N-max L~Cage(C,n);
set Ema = E-max L~Cage(C,n);
set Rot = Rotate(Cage(C,n),Wmi);
A1: Upper_Seq(C,n) = Rot-:Ema by JORDAN1E:def 1;
A2: L~Rot = L~Cage(C,n) by REVROT_1:33;
Wmi in rng Cage(C,n) by SPRECT_2:47;
then A3: Rot/.1 = Wmi by FINSEQ_6:98;
A4: Nmi in rng Rot by A2,SPRECT_2:43;
A5: Ema in rng Rot by A2,SPRECT_2:50;
A6: Nmi..Rot < Nma..Rot by A2,A3,SPRECT_5:25;
A7: Nma..Rot <= Ema..Rot by A2,A3,SPRECT_5:26;
then Nmi..Rot < Ema..Rot by A6,AXIOMS:22;
then A8: Nmi..(Rot-:Ema) = Nmi..Rot by A4,A5,SPRECT_5:3;
Nma in rng Rot by A2,SPRECT_2:44;
hence (N-min L~Cage(C,n))..Upper_Seq(C,n) <
(N-max L~Cage(C,n))..Upper_Seq(C,n) by A1,A5,A6,A7,A8,SPRECT_5:3;
end;
theorem Th31:
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
(N-max L~Cage(C,n))..Upper_Seq(C,n) <= (E-max L~Cage(C,n))..Upper_Seq(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
set Wmi = W-min L~Cage(C,n);
set Nma = N-max L~Cage(C,n);
set Ema = E-max L~Cage(C,n);
set Rot = Rotate(Cage(C,n),Wmi);
A1: Upper_Seq(C,n) = Rot-:Ema by JORDAN1E:def 1;
A2: L~Rot = L~Cage(C,n) by REVROT_1:33;
Wmi in rng Cage(C,n) by SPRECT_2:47;
then A3: Rot/.1 = Wmi by FINSEQ_6:98;
A4: Nma in rng Rot by A2,SPRECT_2:44;
A5: Ema in rng Rot by A2,SPRECT_2:50;
A6: Nma..Rot <= Ema..Rot by A2,A3,SPRECT_5:26;
then Nma..(Rot-:Ema) = Nma..Rot by A4,A5,SPRECT_5:3;
hence thesis by A1,A5,A6,SPRECT_5:3;
end;
theorem Th32:
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
(E-max L~Cage(C,n))..Upper_Seq(C,n) = len Upper_Seq(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 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));
then E-max L~Cage(C,n) in rng Upper_Seq(C,n) by A1,A3,FINSEQ_5:49;
then A4: Upper_Seq(C,n) just_once_values E-max L~Cage(C,n) by FINSEQ_4:10;
Upper_Seq(C,n)/.len Upper_Seq(C,n) = E-max L~Cage(C,n) by JORDAN1F:7;
hence (E-max L~Cage(C,n))..Upper_Seq(C,n) = len Upper_Seq(C,n)
by A4,REVROT_1:1;
end;
theorem Th33:
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
(E-max L~Cage(C,n))..Lower_Seq(C,n) = 1
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
Lower_Seq(C,n)/.1 = E-max L~Cage(C,n) by JORDAN1F:6;
hence (E-max L~Cage(C,n))..Lower_Seq(C,n) = 1 by FINSEQ_6:47;
end;
theorem Th34:
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
(E-max L~Cage(C,n))..Lower_Seq(C,n) < (E-min L~Cage(C,n))..Lower_Seq(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
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 Wmi = W-min L~Cage(C,n);
set Rot = Rotate(Cage(C,n),Ema);
A1: Lower_Seq(C,n) = Rot-:Wmi by Th26;
A2: L~Rot = L~Cage(C,n) by REVROT_1:33;
Ema in rng Cage(C,n) by SPRECT_2:50;
then A3: Rot/.1 = Ema by FINSEQ_6:98;
A4: Ema in rng Rot by A2,SPRECT_2:50;
A5: Wmi in rng Rot by A2,SPRECT_2:47;
A6: Ema..Rot < Emi..Rot by A2,A3,SPRECT_5:38;
A7: Emi..Rot <= Sma..Rot by A2,A3,SPRECT_5:40;
A8: Sma..Rot < Smi..Rot by A2,A3,SPRECT_5:41;
A9: Smi..Rot <= Wmi..Rot by A2,A3,SPRECT_5:42;
Emi..Rot < Smi..Rot by A7,A8,AXIOMS:22;
then A10: Emi..Rot < Wmi..Rot by A9,AXIOMS:22;
then Ema..Rot < Wmi..Rot by A6,AXIOMS:22;
then A11: Ema..(Rot-:Wmi) = Ema..Rot by A4,A5,SPRECT_5:3;
Emi in rng Rot by A2,SPRECT_2:49;
hence (E-max L~Cage(C,n))..Lower_Seq(C,n) <
(E-min L~Cage(C,n))..Lower_Seq(C,n) by A1,A5,A6,A10,A11,SPRECT_5:3;
end;
theorem Th35:
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
(E-min L~Cage(C,n))..Lower_Seq(C,n) <= (S-max L~Cage(C,n))..Lower_Seq(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
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 Wmi = W-min L~Cage(C,n);
set Rot = Rotate(Cage(C,n),Ema);
A1: Lower_Seq(C,n) = Rot-:Wmi by Th26;
A2: L~Rot = L~Cage(C,n) by REVROT_1:33;
Ema in rng Cage(C,n) by SPRECT_2:50;
then A3: Rot/.1 = Ema by FINSEQ_6:98;
A4: Emi in rng Rot by A2,SPRECT_2:49;
A5: Wmi in rng Rot by A2,SPRECT_2:47;
A6: Emi..Rot <= Sma..Rot by A2,A3,SPRECT_5:40;
A7: Sma..Rot < Smi..Rot by A2,A3,SPRECT_5:41;
Smi..Rot <= Wmi..Rot by A2,A3,SPRECT_5:42;
then A8: Sma..Rot < Wmi..Rot by A7,AXIOMS:22;
then Emi..Rot < Wmi..Rot by A6,AXIOMS:22;
then A9: Emi..(Rot-:Wmi) = Emi..Rot by A4,A5,SPRECT_5:3;
Sma in rng Rot by A2,SPRECT_2:46;
hence (E-min L~Cage(C,n))..Lower_Seq(C,n) <=
(S-max L~Cage(C,n))..Lower_Seq(C,n) by A1,A5,A6,A8,A9,SPRECT_5:3;
end;
theorem Th36:
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
(S-max L~Cage(C,n))..Lower_Seq(C,n) < (S-min L~Cage(C,n))..Lower_Seq(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
set Ema = E-max L~Cage(C,n);
set Sma = S-max L~Cage(C,n);
set Smi = S-min L~Cage(C,n);
set Wmi = W-min L~Cage(C,n);
set Rot = Rotate(Cage(C,n),Ema);
A1: Lower_Seq(C,n) = Rot-:Wmi by Th26;
A2: L~Rot = L~Cage(C,n) by REVROT_1:33;
Ema in rng Cage(C,n) by SPRECT_2:50;
then A3: Rot/.1 = Ema by FINSEQ_6:98;
A4: Sma in rng Rot by A2,SPRECT_2:46;
A5: Wmi in rng Rot by A2,SPRECT_2:47;
A6: Sma..Rot < Smi..Rot by A2,A3,SPRECT_5:41;
A7: Smi..Rot <= Wmi..Rot by A2,A3,SPRECT_5:42;
then Sma..Rot < Wmi..Rot by A6,AXIOMS:22;
then A8: Sma..(Rot-:Wmi) = Sma..Rot by A4,A5,SPRECT_5:3;
Smi in rng Rot by A2,SPRECT_2:45;
hence thesis by A1,A5,A6,A7,A8,SPRECT_5:3;
end;
theorem Th37:
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
(S-min L~Cage(C,n))..Lower_Seq(C,n) <= (W-min L~Cage(C,n))..Lower_Seq(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
set Ema = E-max L~Cage(C,n);
set Smi = S-min L~Cage(C,n);
set Wmi = W-min L~Cage(C,n);
set Rot = Rotate(Cage(C,n),Ema);
A1: Lower_Seq(C,n) = Rot-:Wmi by Th26;
A2: L~Rot = L~Cage(C,n) by REVROT_1:33;
Ema in rng Cage(C,n) by SPRECT_2:50;
then A3: Rot/.1 = Ema by FINSEQ_6:98;
A4: Smi in rng Rot by A2,SPRECT_2:45;
A5: Wmi in rng Rot by A2,SPRECT_2:47;
A6: Smi..Rot <= Wmi..Rot by A2,A3,SPRECT_5:42;
then Smi..(Rot-:Wmi) = Smi..Rot by A4,A5,SPRECT_5:3;
hence thesis by A1,A5,A6,SPRECT_5:3;
end;
theorem Th38:
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
(W-min L~Cage(C,n))..Lower_Seq(C,n) = len Lower_Seq(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
A1: Lower_Seq(C,n) = Rotate(Cage(C,n),E-max L~Cage(C,n))-:W-min L~Cage(C,n)
by Th26;
A2: 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 A3: W-min L~Cage(C,n) in rng Rotate(Cage(C,n),E-max L~Cage(C,n))
by A2,FINSEQ_6:96;
(W-min L~Cage(C,n))..Rotate(Cage(C,n),E-max L~Cage(C,n)) <=
(W-min L~Cage(C,n))..Rotate(Cage(C,n),E-max L~Cage(C,n));
then W-min L~Cage(C,n) in rng Lower_Seq(C,n) by A1,A3,FINSEQ_5:49;
then A4: Lower_Seq(C,n) just_once_values W-min L~Cage(C,n) by FINSEQ_4:10;
Lower_Seq(C,n)/.len Lower_Seq(C,n) = W-min L~Cage(C,n) by JORDAN1F:8;
hence thesis by A4,REVROT_1:1;
end;
theorem Th39:
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
(Upper_Seq(C,n)/.2)`1 = W-bound L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
set Ca = Cage(C,n);
set US = Upper_Seq(C,n);
set Wmin = W-min L~Cage(C,n);
set Emax = E-max L~Cage(C,n);
set Nmin = N-min L~Cage(C,n);
A1: Emax in rng Ca by SPRECT_2:50;
A2: Wmin in rng Ca by SPRECT_2:47;
then A3: Emax in rng Rotate(Ca,Wmin) by A1,FINSEQ_6:96;
(Ca:-Wmin)/.len(Ca:-Wmin) = Ca/.len Ca by A2,FINSEQ_5:57
.= Ca/.1 by FINSEQ_6:def 1
.= Nmin by JORDAN9:34;
then A4: Nmin in rng (Ca:-Wmin) by REVROT_1:3;
(Ca:-Wmin)/.1 = Wmin by FINSEQ_5:56;
then A5: Wmin in rng (Ca:-Wmin) by FINSEQ_6:46;
W-max L~Ca in L~Ca & Nmin`2 = N-bound L~Ca by PSCOMP_1:94,SPRECT_1:15;
then (W-max L~Ca)`2 <= Nmin`2 by PSCOMP_1:71;
then Nmin <> Wmin by SPRECT_2:61;
then A6: Card {Nmin,Wmin} = 2 by CARD_2:76;
{Nmin,Wmin} c= rng (Ca:-Wmin)
proof
let x be set;
assume x in {Nmin,Wmin};
hence x in rng (Ca:-Wmin) by A4,A5,TARSKI:def 2;
end;
then A7: Card {Nmin,Wmin} c= Card rng (Ca:-Wmin) by CARD_1:27;
Card rng (Ca:-Wmin) c= Card dom (Ca:-Wmin) by YELLOW_6:3;
then Card rng (Ca:-Wmin) c= len (Ca:-Wmin) by PRE_CIRC:21;
then 2 c= len (Ca:-Wmin) by A6,A7,XBOOLE_1:1;
then A8: len (Ca:-Wmin) >= 2 by CARD_1:56;
then A9: len(Ca:-Wmin) >= 1 by AXIOMS:22;
len US >= 3 by JORDAN1E:19;
then len US >= 2 by AXIOMS:22;
then 2 in Seg len US by FINSEQ_1:3;
then A10: 2 in Seg(Emax..Rotate(Ca,Wmin)) by JORDAN1E:12;
A11: 1 <= Wmin..Ca by A2,FINSEQ_4:31;
Ca/.1 = Nmin by JORDAN9:34;
then Wmin..Ca < len Ca by SPRECT_2:80;
then A12: Wmin..Ca+1 <= len Ca by NAT_1:38;
A13: US/.2 = (Rotate(Ca,Wmin)-:Emax)/.2 by JORDAN1E:def 1
.= Rotate(Ca,Wmin)/.2 by A3,A10,FINSEQ_5:46
.= Ca/.(2-'1+Wmin..Ca) by A2,A8,REVROT_1:9
.= Ca/.(2-1+Wmin..Ca) by BINARITH:def 3;
US/.1 = (Rotate(Ca,Wmin)-:Emax)/.1 by JORDAN1E:def 1
.= Rotate(Ca,Wmin)/.1 by A3,FINSEQ_5:47
.= Ca/.(1-'1+Wmin..Ca) by A2,A9,REVROT_1:9
.= Ca/.(0+Wmin..Ca) by GOBOARD9:1;
then Ca/.(Wmin..Ca) = Wmin by JORDAN1F:5;
hence thesis by A11,A12,A13,JORDAN1E:26;
end;
theorem
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
(Lower_Seq(C,n)/.2)`1 = E-bound L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
set Ca = Cage(C,n);
set LS = Lower_Seq(C,n);
set Emax = E-max L~Cage(C,n);
set Emin = E-min L~Cage(C,n);
set Smax = S-max L~Cage(C,n);
set Smin = S-min L~Cage(C,n);
set Wmin = W-min L~Cage(C,n);
set Nmin = N-min L~Cage(C,n);
A1: Wmin in rng Ca by SPRECT_2:47;
A2: Emax in rng Ca by SPRECT_2:50;
then A3: Wmin in rng Rotate(Ca,Emax) by A1,FINSEQ_6:96;
(Ca:-Emax)/.len(Ca:-Emax) = Ca/.len Ca by A2,FINSEQ_5:57
.= Ca/.1 by FINSEQ_6:def 1
.= Nmin by JORDAN9:34;
then A4: Nmin in rng (Ca:-Emax) by REVROT_1:3;
(Ca:-Emax)/.1 = Emax by FINSEQ_5:56;
then A5: Emax in rng (Ca:-Emax) by FINSEQ_6:46;
N-max L~Ca in L~Ca & Emax`1 = E-bound L~Ca by PSCOMP_1:104,SPRECT_1:13;
then (N-max L~Ca)`1 <= Emax`1 by PSCOMP_1:71;
then Nmin <> Emax by SPRECT_2:55;
then A6: Card {Nmin,Emax} = 2 by CARD_2:76;
{Nmin,Emax} c= rng (Ca:-Emax)
proof
let x be set;
assume x in {Nmin,Emax};
hence x in rng (Ca:-Emax) by A4,A5,TARSKI:def 2;
end;
then A7: Card {Nmin,Emax} c= Card rng (Ca:-Emax) by CARD_1:27;
Card rng (Ca:-Emax) c= Card dom (Ca:-Emax) by YELLOW_6:3;
then Card rng (Ca:-Emax) c= len (Ca:-Emax) by PRE_CIRC:21;
then 2 c= len (Ca:-Emax) by A6,A7,XBOOLE_1:1;
then A8: len (Ca:-Emax) >= 2 by CARD_1:56;
then A9: len(Ca:-Emax) >= 1 by AXIOMS:22;
len LS >= 3 by JORDAN1E:19;
then len LS >= 2 by AXIOMS:22;
then 2 <= Wmin..LS by Th38;
then 2 <= Wmin..(Rotate(Ca,Emax)-:Wmin) by Th26;
then 2 <= Wmin..Rotate(Ca,Emax) by A3,FINSEQ_6:77;
then A10: 2 in Seg (Wmin..Rotate(Ca,Emax)) by FINSEQ_1:3;
A11: 1 <= Emax..Ca by A2,FINSEQ_4:31;
A12: Ca/.1 = Nmin by JORDAN9:34;
then A13: Emax..Ca < Emin..Ca by SPRECT_2:75;
Emin..Ca <= Smax..Ca by A12,SPRECT_2:76;
then A14: Emax..Ca < Smax..Ca by A13,AXIOMS:22;
Smax..Ca < Smin..Ca by A12,SPRECT_2:77;
then A15: Emax..Ca < Smin..Ca by A14,AXIOMS:22;
Smin..Ca <= Wmin..Ca by A12,SPRECT_2:78;
then A16: Emax..Ca < Wmin..Ca by A15,AXIOMS:22;
Wmin..Ca < len Ca by A12,SPRECT_2:80;
then Emax..Ca < len Ca by A16,AXIOMS:22;
then A17: Emax..Ca+1 <= len Ca by NAT_1:38;
A18: LS/.2 = (Rotate(Ca,Emax)-:Wmin)/.2 by Th26
.= Rotate(Ca,Emax)/.2 by A3,A10,FINSEQ_5:46
.= Ca/.(2-'1+Emax..Ca) by A2,A8,REVROT_1:9
.= Ca/.(2-1+Emax..Ca) by BINARITH:def 3;
LS/.1 = (Rotate(Ca,Emax)-:Wmin)/.1 by Th26
.= Rotate(Ca,Emax)/.1 by A3,FINSEQ_5:47
.= Ca/.(1-'1+Emax..Ca) by A2,A9,REVROT_1:9
.= Ca/.(0+Emax..Ca) by GOBOARD9:1;
then Ca/.(Emax..Ca) = Emax by JORDAN1F:6;
hence thesis by A11,A17,A18,JORDAN1E:24;
end;
theorem Th41:
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
W-bound L~Cage(C,n) + E-bound L~Cage(C,n) = W-bound C + E-bound C
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
thus W-bound L~Cage(C,n)+E-bound L~Cage(C,n) = W-bound L~Cage(C,n)+
(E-bound C + (E-bound C - W-bound C)/(2|^n)) by JORDAN1A:85
.= (W-bound C - (E-bound C - W-bound C)/(2|^n))+
(E-bound C + (E-bound C - W-bound C)/(2|^n)) by JORDAN1A:83
.= W-bound C + E-bound C by XCMPLX_1:28;
end;
theorem
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
S-bound L~Cage(C,n) + N-bound L~Cage(C,n) = S-bound C + N-bound C
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
thus S-bound L~Cage(C,n)+N-bound L~Cage(C,n) = S-bound L~Cage(C,n)+
(N-bound C + (N-bound C - S-bound C)/(2|^n)) by JORDAN10:6
.= (S-bound C - (N-bound C - S-bound C)/(2|^n))+
(N-bound C + (N-bound C - S-bound C)/(2|^n)) by JORDAN1A:84
.= S-bound C + N-bound C by XCMPLX_1:28;
end;
theorem Th43:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for n,i be Nat st 1 <= i & i <= width Gauge(C,n) & n > 0 holds
Gauge(C,n)*(Center Gauge(C,n),i)`1 = (W-bound C + E-bound C) / 2
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let n,i be Nat such that
A1: 1 <= i & i <= width Gauge(C,n);
A2: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
len Gauge(C,1) >= 4 by JORDAN8:13;
then A3: len Gauge(C,1) >= 1 by AXIOMS:22;
assume n > 0;
hence Gauge(C,n)*(Center Gauge(C,n),i)`1 =
Gauge(C,1)*(Center Gauge(C,1),1)`1 by A1,A2,A3,JORDAN1A:57
.= (W-bound C + E-bound C) / 2 by A3,JORDAN1A:59;
end;
theorem
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
for n,i be Nat st 1 <= i & i <= len Gauge(C,n) & n > 0 holds
Gauge(C,n)*(i,Center Gauge(C,n))`2 = (S-bound C + N-bound C) / 2
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let n,i be Nat such that
A1: 1 <= i & i <= len Gauge(C,n);
len Gauge(C,1) >= 4 by JORDAN8:13;
then A2: len Gauge(C,1) >= 1 by AXIOMS:22;
assume n > 0;
hence Gauge(C,n)*(i,Center Gauge(C,n))`2 =
Gauge(C,1)*(1,Center Gauge(C,1))`2 by A1,A2,JORDAN1A:58
.= (S-bound C + N-bound C) / 2 by A2,JORDAN1A:60;
end;
theorem Th45:
for f be S-Sequence_in_R2
for k1,k2 be Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f &
f/.1 in L~mid(f,k1,k2) holds k1 = 1 or k2 = 1
proof
let f be S-Sequence_in_R2;
let k1,k2 be Nat;
assume that
A1: 1 <= k1 and
A2: k1 <= len f and
A3: 1 <= k2 and
A4: k2 <= len f and
A5: f/.1 in L~mid(f,k1,k2);
assume A6: k1 <> 1 & k2 <> 1;
consider j be Nat such that
A7: 1 <= j and
A8: j+1 <= len mid(f,k1,k2) and
A9: f/.1 in LSeg(mid(f,k1,k2),j) by A5,SPPOL_2:13;
A10: len f >= 2 by TOPREAL1:def 10;
per cases by REAL_1:def 5;
suppose A11: k1 < k2;
then len mid(f,k1,k2) = k2-'k1 + 1 by A1,A2,A3,A4,JORDAN3:27;
then j < k2-'k1 + 1 by A8,NAT_1:38;
then LSeg(mid(f,k1,k2),j) = LSeg(f,j+k1-'1) by A1,A4,A7,A11,JORDAN4:31;
then A12: j+k1-'1 = 1 by A9,A10,JORDAN5B:33;
j+k1 >= 1+1 by A1,A7,REAL_1:55;
then j+k1-1 >= 1+1-1 by REAL_1:49;
then j+k1-1 >= 0 by AXIOMS:22;
then j+k1-'1 = j+k1-1 by BINARITH:def 3;
then j+(k1-1) = 1 by A12,XCMPLX_1:29;
then k1-1 = 1-j by XCMPLX_1:26;
then k1-1 <= 0 by A7,REAL_2:106;
then k1-1 = 0 by A1,SQUARE_1:12;
hence contradiction by A6,XCMPLX_1:15;
suppose A13: k1 > k2;
then len mid(f,k1,k2) = k1-'k2 + 1 by A1,A2,A3,A4,JORDAN3:27;
then A14: j < k1-'k2 + 1 by A8,NAT_1:38;
then LSeg(mid(f,k1,k2),j) = LSeg(f,k1-'j) by A2,A3,A7,A13,JORDAN4:32;
then A15: k1-'j = 1 by A9,A10,JORDAN5B:33;
k1-k2 > 0 by A13,SQUARE_1:11;
then k1-'k2 = k1-k2 by BINARITH:def 3;
then j-1 < k1-k2 by A14,REAL_1:84;
then j-1+k2 < k1 by REAL_1:86;
then j-(1-k2) < k1 by XCMPLX_1:37;
then j+-(1-k2) < k1 by XCMPLX_0:def 8;
then -(1-k2) < k1-j by REAL_1:86;
then A16: k2-1 < k1-j by XCMPLX_1:143;
then k1-j > 0 by A3,SQUARE_1:12;
then k1-j = 1 by A15,BINARITH:def 3;
then k2 < 1+1 by A16,REAL_1:84;
then k2 <= 1 by NAT_1:38;
hence contradiction by A3,A6,AXIOMS:21;
suppose k1 = k2;
then mid(f,k1,k2) = <*f/.k1*> by A1,A2,JORDAN4:27;
hence contradiction by A5,SPPOL_2:12;
end;
theorem Th46:
for f be S-Sequence_in_R2
for k1,k2 be Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f &
f/.(len f) in L~mid(f,k1,k2) holds k1 = len f or k2 = len f
proof
let f be S-Sequence_in_R2;
let k1,k2 be Nat;
assume that
A1: 1 <= k1 and
A2: k1 <= len f and
A3: 1 <= k2 and
A4: k2 <= len f and
A5: f/.len f in L~mid(f,k1,k2);
assume A6: k1 <> len f & k2 <> len f;
consider j be Nat such that
A7: 1 <= j and
A8: j+1 <= len mid(f,k1,k2) and
A9: f/.len f in LSeg(mid(f,k1,k2),j) by A5,SPPOL_2:13;
per cases by REAL_1:def 5;
suppose A10: k1 < k2;
then k2-k1 > 0 by SQUARE_1:11;
then A11: k2-'k1 = k2-k1 by BINARITH:def 3;
A12: j+k1 >= 1+1 by A1,A7,REAL_1:55;
then A13: j+k1-1 >= 1+1-1 by REAL_1:49;
then A14: j+k1-1 >= 0 by AXIOMS:22;
then A15: j+k1-'1 = j+k1-1 by BINARITH:def 3;
len mid(f,k1,k2) = k2-'k1 + 1 by A1,A2,A3,A4,A10,JORDAN3:27;
then A16: j < k2-'k1 + 1 by A8,NAT_1:38;
then j-1 < k2-k1 by A11,REAL_1:84;
then j-1+k1 < k2 by REAL_1:86;
then j+k1-1 < k2 by XCMPLX_1:29;
then A17: j+k1-1 < len f by A4,AXIOMS:22;
then A18: j+k1-'1 in dom f by A13,A15,FINSEQ_3:27;
A19: j+k1 >= 1 by A12,AXIOMS:22;
j+k1-1+1 <= len f by A15,A17,NAT_1:38;
then j+k1 <= len f by XCMPLX_1:27;
then j+k1 in Seg len f by A19,FINSEQ_1:3;
then j+k1-1+1 in Seg len f by XCMPLX_1:27;
then A20: j+k1-'1+1 in dom f by A15,FINSEQ_1:def 3;
LSeg(mid(f,k1,k2),j) = LSeg(f,j+k1-'1) by A1,A4,A7,A10,A16,JORDAN4:31;
then A21: j+k1-'1+1=len f by A9,A18,A20,GOBOARD2:7;
j+k1-'1 = j+k1-1 by A14,BINARITH:def 3;
then A22: len f = j+k1 by A21,XCMPLX_1:27;
j < k2+1-k1 by A11,A16,XCMPLX_1:29;
then len f < k2+1 by A22,REAL_1:86;
then len f <= k2 by NAT_1:38;
hence contradiction by A4,A6,AXIOMS:21;
suppose A23: k1 > k2;
then len mid(f,k1,k2) = k1-'k2 + 1 by A1,A2,A3,A4,JORDAN3:27;
then A24: j < k1-'k2 + 1 by A8,NAT_1:38;
k1-k2 > 0 by A23,SQUARE_1:11;
then k1-'k2 = k1-k2 by BINARITH:def 3;
then j-1 < k1-k2 by A24,REAL_1:84;
then j-1+k2 < k1 by REAL_1:86;
then j-(1-k2) < k1 by XCMPLX_1:37;
then j+-(1-k2) < k1 by XCMPLX_0:def 8;
then -(1-k2) < k1-j by REAL_1:86;
then A25: k2-1 < k1-j by XCMPLX_1:143;
A26: k2-1 >= 0 by A3,SQUARE_1:12;
A27: k1-j > 0 by A3,A25,SQUARE_1:12;
then A28: k1-'j = k1-j by BINARITH:def 3;
then A29: k1-j >= 0+1 by A25,A26,NAT_1:38;
k1-j <= k1-1 by A7,REAL_2:106;
then k1-j+1 <= k1-1+1 by REAL_1:55;
then k1-j+1 <= k1 by XCMPLX_1:27;
then k1-j < k1 by A28,NAT_1:38;
then A30: k1-j < len f by A2,AXIOMS:22;
then A31: k1-'j in dom f by A28,A29,FINSEQ_3:27;
A32: k1-j+1 > 0+1 by A25,A26,REAL_1:53;
k1-j+1 <= len f by A28,A30,NAT_1:38;
then A33: k1-'j+1 in dom f by A28,A32,FINSEQ_3:27;
LSeg(mid(f,k1,k2),j) = LSeg(f,k1-'j) by A2,A3,A7,A23,A24,JORDAN4:32;
then k1-'j+1=len f by A9,A31,A33,GOBOARD2:7;
then A34: k1-j+1=len f by A27,BINARITH:def 3;
k1-j <= k1-1 by A7,REAL_2:106;
then len f <= k1-1+1 by A34,REAL_1:55;
then len f <= k1 by XCMPLX_1:27;
hence contradiction by A2,A6,AXIOMS:21;
suppose k1 = k2;
then mid(f,k1,k2) = <*f/.k1*> by A1,A2,JORDAN4:27;
hence contradiction by A5,SPPOL_2:12;
end;
theorem Th47:
for C be compact non vertical non horizontal Subset of TOP-REAL 2
for n be Nat holds
rng Upper_Seq(C,n) c= rng Cage(C,n) &
rng Lower_Seq(C,n) c= rng Cage(C,n)
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;
Upper_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n)
by JORDAN1E:def 1;
then rng Upper_Seq(C,n) c= rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by FINSEQ_5:51;
hence rng Upper_Seq(C,n) c= rng Cage(C,n) by A1,FINSEQ_6:96;
Lower_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n)
by JORDAN1E:def 2;
then rng Lower_Seq(C,n) c= rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A2,FINSEQ_5:58;
hence rng Lower_Seq(C,n) c= rng Cage(C,n) by A1,FINSEQ_6:96;
end;
theorem Th48:
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
Upper_Seq(C,n) is_a_h.c._for Cage(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
A1: Upper_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:21;
A2: (Upper_Seq(C,n)/.1)`1 = (W-min L~Cage(C,n))`1 by JORDAN1F:5
.= W-bound L~Cage(C,n) by PSCOMP_1:84;
(Upper_Seq(C,n)/.len Upper_Seq(C,n))`1 = (E-max L~Cage(C,n))`1
by JORDAN1F:7
.= E-bound L~Cage(C,n) by PSCOMP_1:104;
hence Upper_Seq(C,n) is_a_h.c._for Cage(C,n) by A1,A2,SPRECT_2:def 2;
end;
theorem Th49:
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
Rev Lower_Seq(C,n) is_a_h.c._for Cage(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:22;
then A1: Rev Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by SPRECT_3:68;
A2: (Rev Lower_Seq(C,n)/.1)`1 = (Lower_Seq(C,n)/.len Lower_Seq(C,n))`1
by FINSEQ_5:68
.= (W-min L~Cage(C,n))`1 by JORDAN1F:8
.= W-bound L~Cage(C,n) by PSCOMP_1:84;
(Rev Lower_Seq(C,n)/.len Rev Lower_Seq(C,n))`1 =
(Rev Lower_Seq(C,n)/.len Lower_Seq(C,n))`1 by FINSEQ_5:def 3
.= (Lower_Seq(C,n)/.1)`1 by FINSEQ_5:68
.= (E-max L~Cage(C,n))`1 by JORDAN1F:6
.= E-bound L~Cage(C,n) by PSCOMP_1:104;
hence Rev Lower_Seq(C,n) is_a_h.c._for Cage(C,n) by A1,A2,SPRECT_2:def 2;
end;
theorem Th50:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i be Nat st 1 < i & i <= len Gauge(C,n) holds
not Gauge(C,n)*(i,1) in rng Upper_Seq(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i be Nat;
assume that
A1: 1 < i and
A2: i <= len Gauge(C,n) and
A3: Gauge(C,n)*(i,1) in rng Upper_Seq(C,n);
consider i2 be Nat such that
A4: i2 in dom Upper_Seq(C,n) and
A5: Upper_Seq(C,n).i2 = Gauge(C,n)*(i,1) by A3,FINSEQ_2:11;
set i1 = (N-min L~Cage(C,n))..Upper_Seq(C,n);
(W-min L~Cage(C,n))..Upper_Seq(C,n) = 1 by Th27;
then A6: 1 < (W-max L~Cage(C,n))..Upper_Seq(C,n) by Th28;
(W-max L~Cage(C,n))..Upper_Seq(C,n) <= i1 by Th29;
then A7: i1 > 1 by A6,AXIOMS:22;
A8: i1 < (N-max L~Cage(C,n))..Upper_Seq(C,n) by Th30;
(E-max L~Cage(C,n))..Upper_Seq(C,n) = len Upper_Seq(C,n) by Th32;
then (N-max L~Cage(C,n))..Upper_Seq(C,n) <= len Upper_Seq(C,n) by Th31;
then A9: i1 < len Upper_Seq(C,n) by A8,AXIOMS:22;
A10: 1 <= i2 & i2 <= len Upper_Seq(C,n) by A4,FINSEQ_3:27;
A11: i1 in dom Upper_Seq(C,n) by A7,A9,FINSEQ_3:27;
set f = Rotate(Cage(C,n),W-min L~Cage(C,n));
A12: Upper_Seq(C,n) = f-:E-max L~Cage(C,n) by JORDAN1E:def 1;
A13: N-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
A14: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
A15: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
then A16: rng f = rng Cage(C,n) by FINSEQ_6:96;
A17: f/.1 = W-min L~Cage(C,n) by A15,FINSEQ_6:98;
A18: L~Cage(C,n) = L~f by REVROT_1:33;
then A19: (N-min L~Cage(C,n))..f < (N-max L~Cage(C,n))..f
by A17,SPRECT_5:25;
(N-max L~Cage(C,n))..f <= (E-max L~Cage(C,n))..f by A17,A18,SPRECT_5:26;
then (N-min L~Cage(C,n))..f < (E-max L~Cage(C,n))..f by A19,AXIOMS:22;
then A20: N-min L~Cage(C,n) in rng Upper_Seq(C,n)
by A12,A13,A14,A16,FINSEQ_5:49;
then A21: Upper_Seq(C,n)/.i1 = N-min L~Cage(C,n) by FINSEQ_5:41;
A22: i1 <> i2
proof
assume i1 = i2;
then Gauge(C,n)*(i,1) = N-min L~Cage(C,n) by A5,A11,A21,FINSEQ_4:def 4;
then (Gauge(C,n)*(i,1))`2 = N-bound L~Cage(C,n) by PSCOMP_1:94;
then S-bound L~Cage(C,n) = N-bound L~Cage(C,n) by A1,A2,JORDAN1A:93;
hence contradiction by SPRECT_1:18;
end;
then mid(Upper_Seq(C,n),i1,i2) is_S-Seq by A7,A9,A10,JORDAN3:39;
then reconsider h1 = mid(Upper_Seq(C,n),i1,i2) as
one-to-one special FinSequence of TOP-REAL 2 by TOPREAL1:def 10;
set h = Rev h1;
3 <= len Lower_Seq(C,n) by JORDAN1E:19;
then A23: 2 <= len Lower_Seq(C,n) by AXIOMS:22;
A24: len Lower_Seq(C,n) = len Rev Lower_Seq(C,n) by FINSEQ_5:def 3;
A25: len h1 = len h by FINSEQ_5:def 3;
then A26: len h <> 1 by A4,A11,A22,SPRECT_2:10;
A27: len h >= 1 by A4,A11,A25,SPRECT_2:9;
then len h > 1 by A26,REAL_1:def 5;
then A28: 1+1 <= len h by NAT_1:38;
A29: Rev Lower_Seq(C,n) is_a_h.c._for Cage(C,n) by Th49;
A30: h is special by SPPOL_2:42;
Upper_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:21;
then h1 is_in_the_area_of Cage(C,n) by A4,A11,SPRECT_2:26;
then A31: h is_in_the_area_of Cage(C,n) by SPRECT_3:68;
len h > 0 by A27,AXIOMS:22;
then A32: h1 is non empty by A25,FINSEQ_1:25;
A33: Rev Lower_Seq(C,n) is special by SPPOL_2:42;
A34: L~Rev Lower_Seq(C,n) = L~Lower_Seq(C,n) by SPPOL_2:22;
A35: (h/.1)`2 = (h1/.len h1)`2 by A32,FINSEQ_5:68
.= (Upper_Seq(C,n)/.i2)`2 by A4,A11,SPRECT_2:13
.= (Gauge(C,n)*(i,1))`2 by A4,A5,FINSEQ_4:def 4
.= S-bound L~Cage(C,n) by A1,A2,JORDAN1A:93;
(h/.len h)`2 = (h1/.1)`2 by A25,A32,FINSEQ_5:68
.= (Upper_Seq(C,n)/.i1)`2 by A4,A11,SPRECT_2:12
.= (N-min L~Cage(C,n))`2 by A20,FINSEQ_5:41
.= N-bound L~Cage(C,n) by PSCOMP_1:94;
then h is_a_v.c._for Cage(C,n) by A31,A35,SPRECT_2:def 3;
then L~Rev Lower_Seq(C,n) meets L~h by A23,A24,A28,A29,A30,A33,SPRECT_2:33
;
then consider x be set such that
A36: x in L~Lower_Seq(C,n) and
A37: x in L~h by A34,XBOOLE_0:3;
A38: L~h = L~h1 by SPPOL_2:22;
L~mid(Upper_Seq(C,n),i1,i2) c= L~Upper_Seq(C,n) by A7,A9,A10,JORDAN4:47;
then x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) by A36,A37,A38,XBOOLE_0:def
3;
then A39: x in {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:20;
4 <= len Gauge(C,n) by JORDAN8:13;
then A40: 1 <= len Gauge(C,n) by AXIOMS:22;
A41: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
per cases by A39,TARSKI:def 2;
suppose x = W-min L~Cage(C,n);
then x = Upper_Seq(C,n)/.1 by JORDAN1F:5;
then i2 = 1 by A7,A9,A10,A37,A38,Th45;
then Upper_Seq(C,n)/.1 = Gauge(C,n)*(i,1) by A4,A5,FINSEQ_4:def 4;
then W-min(L~Cage(C,n)) = Gauge(C,n)*(i,1) by JORDAN1F:5;
then Gauge(C,n)*(i,1)`1 = W-bound(L~Cage(C,n)) by PSCOMP_1:84
.= Gauge(C,n)*(1,1)`1 by A40,JORDAN1A:94;
hence contradiction by A1,A2,A40,A41,GOBOARD5:4;
suppose x = E-max L~Cage(C,n);
then x = Upper_Seq(C,n)/.len Upper_Seq(C,n) by JORDAN1F:7;
then i2 = len Upper_Seq(C,n) by A7,A9,A10,A37,A38,Th46;
then Upper_Seq(C,n)/.len Upper_Seq(C,n) = Gauge(C,n)*(i,1)
by A4,A5,FINSEQ_4:def 4;
then A42: E-max(L~Cage(C,n)) = Gauge(C,n)*(i,1) by JORDAN1F:7;
A43: (E-min L~Cage(C,n))`2 < (E-max L~Cage(C,n))`2 by SPRECT_2:57;
(SE-corner L~Cage(C,n))`2 <= (E-min L~Cage(C,n))`2 by PSCOMP_1:107;
then (SE-corner L~Cage(C,n))`2 < (E-max L~Cage(C,n))`2 by A43,AXIOMS:22;
then S-bound L~Cage(C,n) < (Gauge(C,n)*(i,1))`2 by A42,PSCOMP_1:79;
hence contradiction by A1,A2,JORDAN1A:93;
end;
theorem Th51:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i be Nat st 1 <= i & i < len Gauge(C,n) holds
not Gauge(C,n)*(i,width Gauge(C,n)) in rng Lower_Seq(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i be Nat;
set wi = width Gauge(C,n);
assume that
A1: 1 <= i and
A2: i < len Gauge(C,n) and
A3: Gauge(C,n)*(i,wi) in rng Lower_Seq(C,n);
consider i2 be Nat such that
A4: i2 in dom Lower_Seq(C,n) and
A5: Lower_Seq(C,n).i2 = Gauge(C,n)*(i,wi) by A3,FINSEQ_2:11;
set i1 = (S-max L~Cage(C,n))..Lower_Seq(C,n);
A6: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
(E-max L~Cage(C,n))..Lower_Seq(C,n) = 1 by Th33;
then A7: 1 < (E-min L~Cage(C,n))..Lower_Seq(C,n) by Th34;
(E-min L~Cage(C,n))..Lower_Seq(C,n) <= i1 by Th35;
then A8: i1 > 1 by A7,AXIOMS:22;
A9: i1 < (S-min L~Cage(C,n))..Lower_Seq(C,n) by Th36;
(W-min L~Cage(C,n))..Lower_Seq(C,n) = len Lower_Seq(C,n) by Th38;
then (S-min L~Cage(C,n))..Lower_Seq(C,n) <= len Lower_Seq(C,n) by Th37;
then A10: i1 < len Lower_Seq(C,n) by A9,AXIOMS:22;
A11: 1 <= i2 & i2 <= len Lower_Seq(C,n) by A4,FINSEQ_3:27;
A12: i1 in dom Lower_Seq(C,n) by A8,A10,FINSEQ_3:27;
set f = Rotate(Cage(C,n),E-max L~Cage(C,n));
A13: Lower_Seq(C,n) = f-:W-min L~Cage(C,n) by Th26;
A14: S-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
A15: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
A16: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
then A17: rng f = rng Cage(C,n) by FINSEQ_6:96;
A18: f/.1 = E-max L~Cage(C,n) by A16,FINSEQ_6:98;
A19: L~Cage(C,n) = L~f by REVROT_1:33;
then A20: (S-max L~Cage(C,n))..f < (S-min L~Cage(C,n))..f
by A18,SPRECT_5:41;
(S-min L~Cage(C,n))..f <= (W-min L~Cage(C,n))..f by A18,A19,SPRECT_5:42;
then (S-max L~Cage(C,n))..f < (W-min L~Cage(C,n))..f by A20,AXIOMS:22;
then A21: S-max L~Cage(C,n) in rng Lower_Seq(C,n)
by A13,A14,A15,A17,FINSEQ_5:49;
then A22: Lower_Seq(C,n)/.i1 = S-max L~Cage(C,n) by FINSEQ_5:41;
A23: i1 <> i2
proof
assume i1 = i2;
then Gauge(C,n)*(i,wi) = S-max L~Cage(C,n) by A5,A12,A22,FINSEQ_4:def 4;
then (Gauge(C,n)*(i,wi))`2 = S-bound L~Cage(C,n) by PSCOMP_1:114;
then N-bound L~Cage(C,n) = S-bound L~Cage(C,n) by A1,A2,A6,JORDAN1A:91;
hence contradiction by SPRECT_1:18;
end;
then mid(Lower_Seq(C,n),i1,i2) is_S-Seq by A8,A10,A11,JORDAN3:39;
then reconsider h = mid(Lower_Seq(C,n),i1,i2) as
one-to-one special FinSequence of TOP-REAL 2 by TOPREAL1:def 10;
3 <= len Upper_Seq(C,n) by JORDAN1E:19;
then A24: 2 <= len Upper_Seq(C,n) by AXIOMS:22;
A25: len h <> 1 by A4,A12,A23,SPRECT_2:10;
len h >= 1 by A4,A12,SPRECT_2:9;
then len h > 1 by A25,REAL_1:def 5;
then A26: 1+1 <= len h by NAT_1:38;
A27: Upper_Seq(C,n) is_a_h.c._for Cage(C,n) by Th48;
Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:22;
then A28: h is_in_the_area_of Cage(C,n) by A4,A12,SPRECT_2:26;
A29: (h/.len h)`2 = (Lower_Seq(C,n)/.i2)`2 by A4,A12,SPRECT_2:13
.= (Gauge(C,n)*(i,wi))`2 by A4,A5,FINSEQ_4:def 4
.= N-bound L~Cage(C,n) by A1,A2,A6,JORDAN1A:91;
(h/.1)`2 = (Lower_Seq(C,n)/.i1)`2 by A4,A12,SPRECT_2:12
.= (S-max L~Cage(C,n))`2 by A21,FINSEQ_5:41
.= S-bound L~Cage(C,n) by PSCOMP_1:114;
then h is_a_v.c._for Cage(C,n) by A28,A29,SPRECT_2:def 3;
then L~Upper_Seq(C,n) meets L~h by A24,A26,A27,SPRECT_2:33;
then consider x be set such that
A30: x in L~Upper_Seq(C,n) and
A31: x in L~h by XBOOLE_0:3;
L~mid(Lower_Seq(C,n),i1,i2) c= L~Lower_Seq(C,n) by A8,A10,A11,JORDAN4:47;
then x in L~Lower_Seq(C,n) /\ L~Upper_Seq(C,n) by A30,A31,XBOOLE_0:def 3;
then A32: x in {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:20;
4 <= len Gauge(C,n) by JORDAN8:13;
then A33: 1 <= len Gauge(C,n) by AXIOMS:22;
per cases by A32,TARSKI:def 2;
suppose x = E-max L~Cage(C,n);
then x = Lower_Seq(C,n)/.1 by JORDAN1F:6;
then i2 = 1 by A8,A10,A11,A31,Th45;
then Lower_Seq(C,n)/.1 = Gauge(C,n)*(i,wi) by A4,A5,FINSEQ_4:def 4;
then E-max(L~Cage(C,n)) = Gauge(C,n)*(i,wi) by JORDAN1F:6;
then Gauge(C,n)*(i,wi)`1 = E-bound(L~Cage(C,n)) by PSCOMP_1:104
.= Gauge(C,n)*(len Gauge(C,n),wi)`1 by A6,A33,JORDAN1A:92;
hence contradiction by A1,A2,A6,A33,GOBOARD5:4;
suppose x = W-min L~Cage(C,n);
then x = Lower_Seq(C,n)/.len Lower_Seq(C,n) by JORDAN1F:8;
then i2 = len Lower_Seq(C,n) by A8,A10,A11,A31,Th46;
then Lower_Seq(C,n)/.len Lower_Seq(C,n) = Gauge(C,n)*(i,wi)
by A4,A5,FINSEQ_4:def 4;
then A34: W-min(L~Cage(C,n)) = Gauge(C,n)*(i,wi) by JORDAN1F:8;
A35: (W-max L~Cage(C,n))`2 > (W-min L~Cage(C,n))`2 by SPRECT_2:61;
(NW-corner L~Cage(C,n))`2 >= (W-max L~Cage(C,n))`2 by PSCOMP_1:87;
then (NW-corner L~Cage(C,n))`2 > (W-min L~Cage(C,n))`2 by A35,AXIOMS:22;
then N-bound L~Cage(C,n) > (Gauge(C,n)*(i,wi))`2 by A34,PSCOMP_1:75;
hence contradiction by A1,A2,A6,JORDAN1A:91;
end;
theorem Th52:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i be Nat st 1 < i & i <= len Gauge(C,n) holds
not Gauge(C,n)*(i,1) in L~Upper_Seq(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i be Nat such that
A1: 1 < i & i <= len Gauge(C,n) and
A2: Gauge(C,n)*(i,1) in L~Upper_Seq(C,n);
set Gi1 = Gauge(C,n)*(i,1);
consider ii be Nat such that
A3: 1 <= ii & ii+1 <= len Upper_Seq(C,n) and
A4: Gi1 in LSeg(Upper_Seq(C,n),ii) by A2,SPPOL_2:13;
A5: LSeg(Upper_Seq(C,n),ii) =
LSeg(Upper_Seq(C,n)/.ii,Upper_Seq(C,n)/.(ii+1)) by A3,TOPREAL1:def 5;
Upper_Seq(C,n) is_sequence_on Gauge(C,n) by Th4;
then consider i1,j1,i2,j2 being Nat such that
A6: [i1,j1] in Indices Gauge(C,n) and
A7: Upper_Seq(C,n)/.ii = Gauge(C,n)*(i1,j1) and
A8: [i2,j2] in Indices Gauge(C,n) and
A9: Upper_Seq(C,n)/.(ii+1) = Gauge(C,n)*(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 A3,JORDAN8:6;
A11: 1 <= i1 & i1 <= len Gauge(C,n) & 1 <= j1 & j1 <= width Gauge(C,n)
by A6,GOBOARD5:1;
A12: 1 <= i2 & i2 <= len Gauge(C,n) & 1 <= j2 & j2 <= width Gauge(C,n)
by A8,GOBOARD5:1;
A13: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
len Gauge(C,n) >= 4 by JORDAN8:13;
then len Gauge(C,n) > 1 by AXIOMS:22;
then A14: [i,1] in Indices Gauge(C,n) by A1,A13,GOBOARD7:10;
ii+1 >= 1 by NAT_1:29;
then A15: ii+1 in dom Upper_Seq(C,n) by A3,FINSEQ_3:27;
ii < len Upper_Seq(C,n) by A3,NAT_1:38;
then A16: ii in dom Upper_Seq(C,n) by A3,FINSEQ_3:27;
A17: not Gi1 in rng Upper_Seq(C,n) by A1,Th50;
per cases by A10;
suppose A18: i1 = i2 & j1+1 = j2;
then Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A11,GOBOARD5:3
.= Gauge(C,n)*(i2,j2)`1 by A12,GOBOARD5:3;
then LSeg(Upper_Seq(C,n)/.ii,Upper_Seq(C,n)/.(ii+1)) is vertical
by A7,A9,SPPOL_1:37;
then Gi1`1 = Gauge(C,n)*(i1,j1)`1 by A4,A5,A7,SPRECT_3:20;
then A19: i1 = i by A6,A14,Th7;
j1 <= j2 by A18,NAT_1:29;
then Gauge(C,n)*(i1,j1)`2 <= Gauge(C,n)*(i2,j2)`2
by A11,A12,A18,SPRECT_3:24;
then A20: Gauge(C,n)*(i1,j1)`2 <= Gi1`2 by A4,A5,A7,A9,TOPREAL1:10;
Gi1`2 <= Gauge(C,n)*(i1,j1)`2 by A11,A19,SPRECT_3:24;
then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A20,AXIOMS:21;
then j1 = 1 by A6,A14,Th6;
hence contradiction by A7,A16,A17,A19,PARTFUN2:4;
suppose A21: i1+1 = i2 & j1 = j2;
then Gauge(C,n)*(i1,j1)`2 = Gauge(C,n)*(1,j2)`2 by A11,GOBOARD5:2
.= Gauge(C,n)*(i2,j2)`2 by A12,GOBOARD5:2;
then LSeg(Upper_Seq(C,n)/.ii,Upper_Seq(C,n)/.(ii+1)) is horizontal
by A7,A9,SPPOL_1:36;
then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A4,A5,A7,SPRECT_3:19;
then A22: j1 = 1 by A6,A14,Th6;
i2 > 1 by A11,A21,NAT_1:38;
then not Upper_Seq(C,n)/.(ii+1) in rng Upper_Seq(C,n)
by A9,A12,A21,A22,Th50;
hence contradiction by A15,PARTFUN2:4;
suppose A23: i1 = i2+1 & j1 = j2;
then Gauge(C,n)*(i1,j1)`2 = Gauge(C,n)*(1,j2)`2 by A11,GOBOARD5:2
.= Gauge(C,n)*(i2,j2)`2 by A12,GOBOARD5:2;
then LSeg(Upper_Seq(C,n)/.ii,Upper_Seq(C,n)/.(ii+1)) is horizontal
by A7,A9,SPPOL_1:36;
then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A4,A5,A7,SPRECT_3:19;
then A24: j1 = 1 by A6,A14,Th6;
i1 > 1 by A12,A23,NAT_1:38;
then not Upper_Seq(C,n)/.ii in rng Upper_Seq(C,n) by A7,A11,A24,Th50;
hence contradiction by A16,PARTFUN2:4;
suppose A25: i1 = i2 & j1 = j2+1;
then Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A11,GOBOARD5:3
.= Gauge(C,n)*(i2,j2)`1 by A12,GOBOARD5:3;
then LSeg(Upper_Seq(C,n)/.ii,Upper_Seq(C,n)/.(ii+1)) is vertical
by A7,A9,SPPOL_1:37;
then Gi1`1 = Gauge(C,n)*(i1,j1)`1 by A4,A5,A7,SPRECT_3:20;
then A26: i1 = i by A6,A14,Th7;
j2 <= j1 by A25,NAT_1:29;
then Gauge(C,n)*(i2,j2)`2 <= Gauge(C,n)*(i1,j1)`2
by A11,A12,A25,SPRECT_3:24;
then A27: Gauge(C,n)*(i2,j2)`2 <= Gi1`2 by A4,A5,A7,A9,TOPREAL1:10;
Gi1`2 <= Gauge(C,n)*(i2,j2)`2 by A12,A25,A26,SPRECT_3:24;
then Gi1`2 = Gauge(C,n)*(i2,j2)`2 by A27,AXIOMS:21;
then j2 = 1 by A8,A14,Th6;
hence contradiction by A9,A15,A17,A25,A26,PARTFUN2:4;
end;
theorem
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
for i be Nat st 1 <= i & i < len Gauge(C,n) holds
not Gauge(C,n)*(i,width Gauge(C,n)) in L~Lower_Seq(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
set wi = width Gauge(C,n);
let i be Nat such that
A1: 1 <= i & i < len Gauge(C,n) and
A2: Gauge(C,n)*(i,wi) in L~Lower_Seq(C,n);
set Gi1 = Gauge(C,n)*(i,wi);
consider ii be Nat such that
A3: 1 <= ii & ii+1 <= len Lower_Seq(C,n) and
A4: Gi1 in LSeg(Lower_Seq(C,n),ii) by A2,SPPOL_2:13;
A5: LSeg(Lower_Seq(C,n),ii) =
LSeg(Lower_Seq(C,n)/.ii,Lower_Seq(C,n)/.(ii+1)) by A3,TOPREAL1:def 5;
Lower_Seq(C,n) is_sequence_on Gauge(C,n) by Th5;
then consider i1,j1,i2,j2 being Nat such that
A6: [i1,j1] in Indices Gauge(C,n) and
A7: Lower_Seq(C,n)/.ii = Gauge(C,n)*(i1,j1) and
A8: [i2,j2] in Indices Gauge(C,n) and
A9: Lower_Seq(C,n)/.(ii+1) = Gauge(C,n)*(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 A3,JORDAN8:6;
A11: 1 <= i1 & i1 <= len Gauge(C,n) & 1 <= j1 & j1 <= width Gauge(C,n)
by A6,GOBOARD5:1;
A12: 1 <= i2 & i2 <= len Gauge(C,n) & 1 <= j2 & j2 <= width Gauge(C,n)
by A8,GOBOARD5:1;
A13: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
len Gauge(C,n) >= 4 by JORDAN8:13;
then len Gauge(C,n) > 1 by AXIOMS:22;
then A14: [i,wi] in Indices Gauge(C,n) by A1,A13,GOBOARD7:10;
ii+1 >= 1 by NAT_1:29;
then A15: ii+1 in dom Lower_Seq(C,n) by A3,FINSEQ_3:27;
ii < len Lower_Seq(C,n) by A3,NAT_1:38;
then A16: ii in dom Lower_Seq(C,n) by A3,FINSEQ_3:27;
A17: not Gi1 in rng Lower_Seq(C,n) by A1,Th51;
per cases by A10;
suppose A18: i1 = i2 & j2+1 = j1;
then Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A11,GOBOARD5:3
.= Gauge(C,n)*(i2,j2)`1 by A12,GOBOARD5:3;
then LSeg(Lower_Seq(C,n)/.ii,Lower_Seq(C,n)/.(ii+1)) is vertical
by A7,A9,SPPOL_1:37;
then Gi1`1 = Gauge(C,n)*(i1,j1)`1 by A4,A5,A7,SPRECT_3:20;
then A19: i1 = i by A6,A14,Th7;
j1 >= j2 by A18,NAT_1:29;
then Gauge(C,n)*(i1,j1)`2 >= Gauge(C,n)*(i2,j2)`2
by A11,A12,A18,SPRECT_3:24;
then A20: Gauge(C,n)*(i1,j1)`2 >= Gi1`2 by A4,A5,A7,A9,TOPREAL1:10;
Gi1`2 >= Gauge(C,n)*(i1,j1)`2 by A11,A19,SPRECT_3:24;
then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A20,AXIOMS:21;
then j1 = wi by A6,A14,Th6;
hence contradiction by A7,A16,A17,A19,PARTFUN2:4;
suppose A21: i2+1 = i1 & j1 = j2;
then Gauge(C,n)*(i1,j1)`2 = Gauge(C,n)*(1,j2)`2 by A11,GOBOARD5:2
.= Gauge(C,n)*(i2,j2)`2 by A12,GOBOARD5:2;
then LSeg(Lower_Seq(C,n)/.ii,Lower_Seq(C,n)/.(ii+1)) is horizontal
by A7,A9,SPPOL_1:36;
then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A4,A5,A7,SPRECT_3:19;
then A22: j1 = wi by A6,A14,Th6;
i2 < len Gauge(C,n) by A11,A21,NAT_1:38;
then not Lower_Seq(C,n)/.(ii+1) in rng Lower_Seq(C,n)
by A9,A12,A21,A22,Th51;
hence contradiction by A15,PARTFUN2:4;
suppose A23: i2 = i1+1 & j1 = j2;
then Gauge(C,n)*(i1,j1)`2 = Gauge(C,n)*(1,j2)`2 by A11,GOBOARD5:2
.= Gauge(C,n)*(i2,j2)`2 by A12,GOBOARD5:2;
then LSeg(Lower_Seq(C,n)/.ii,Lower_Seq(C,n)/.(ii+1)) is horizontal
by A7,A9,SPPOL_1:36;
then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A4,A5,A7,SPRECT_3:19;
then A24: j1 = wi by A6,A14,Th6;
i1 < len Gauge(C,n) by A12,A23,NAT_1:38;
then not Lower_Seq(C,n)/.ii in rng Lower_Seq(C,n) by A7,A11,A24,Th51;
hence contradiction by A16,PARTFUN2:4;
suppose A25: i1 = i2 & j2 = j1+1;
then Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A11,GOBOARD5:3
.= Gauge(C,n)*(i2,j2)`1 by A12,GOBOARD5:3;
then LSeg(Lower_Seq(C,n)/.ii,Lower_Seq(C,n)/.(ii+1)) is vertical
by A7,A9,SPPOL_1:37;
then Gi1`1 = Gauge(C,n)*(i1,j1)`1 by A4,A5,A7,SPRECT_3:20;
then A26: i1 = i by A6,A14,Th7;
j2 >= j1 by A25,NAT_1:29;
then Gauge(C,n)*(i2,j2)`2 >= Gauge(C,n)*(i1,j1)`2
by A11,A12,A25,SPRECT_3:24;
then A27: Gauge(C,n)*(i2,j2)`2 >= Gi1`2 by A4,A5,A7,A9,TOPREAL1:10;
Gi1`2 >= Gauge(C,n)*(i2,j2)`2 by A12,A25,A26,SPRECT_3:24;
then Gi1`2 = Gauge(C,n)*(i2,j2)`2 by A27,AXIOMS:21;
then j2 = wi by A8,A14,Th6;
hence contradiction by A9,A15,A17,A25,A26,PARTFUN2:4;
end;
theorem Th54:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j be Nat st 1 <= i & i <= len Gauge(C,n) &
1 <= j & j <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Cage(C,n) holds
LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,j)) meets L~Lower_Seq(C,n)
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i,j be Nat;
set Gij = Gauge(C,n)*(i,j);
assume that
A1: 1 <= i & i <= len Gauge(C,n) and
A2: 1 <= j & j <= width Gauge(C,n) and
A3: Gij in L~Cage(C,n);
set NE = NE-corner L~Cage(C,n);
set v1 = L_Cut(Upper_Seq(C,n),Gij);
set Gv1 = <*Gauge(C,n)*(i,1)*>^v1;
set v = Gv1^<*NE*>;
set h = mid(Lower_Seq(C,n),2,len Lower_Seq(C,n));
A4: L~Cage(C,n) = L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n) by JORDAN1E:17;
A5: Lower_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n)):-
E-max L~Cage(C,n) by JORDAN1E:def 2;
A6: Upper_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n))-:
E-max L~Cage(C,n) by JORDAN1E:def 1;
len Lower_Seq(C,n) >= 3 & len Upper_Seq(C,n) >= 3 by JORDAN1E:19;
then A7: len Lower_Seq(C,n) >= 2 & len Lower_Seq(C,n) >= 1 &
len Upper_Seq(C,n) >= 2 & len Upper_Seq(C,n) >= 1 by AXIOMS:22;
A8: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
A9: Gauge(C,n)*(i,1)`2 = S-bound L~Cage(C,n) by A1,JORDAN1A:93;
set Wmi = W-min L~Cage(C,n);
now per cases by A1,A3,A4,REAL_1:def 5,XBOOLE_0:def 2;
suppose A10: Gij in L~Upper_Seq(C,n) & i = 1;
set G11 = Gauge(C,n)*(1,1);
A11: G11`1 = W-bound L~Cage(C,n) by A1,A10,JORDAN1A:94;
A12: Wmi`1 = W-bound L~Cage(C,n) by PSCOMP_1:84;
A13: S-bound L~Cage(C,n) = G11`2 by A1,A10,JORDAN1A:93;
Wmi in L~Cage(C,n) by SPRECT_1:15;
then A14: G11`2 <= Wmi`2 by A13,PSCOMP_1:71;
A15: Gij`1 = W-bound L~Cage(C,n) by A2,A8,A10,JORDAN1A:94;
then Gij in W-most L~Cage(C,n) by A3,SPRECT_2:16;
then Wmi`2 <= Gij`2 by PSCOMP_1:88;
then A16: Wmi in LSeg(Gauge(C,n)*(1,1),Gauge(C,n)*(1,j))
by A10,A11,A12,A14,A15,GOBOARD7:8;
A17: rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by A7,SPPOL_2:18;
Lower_Seq(C,n)/.(len Lower_Seq(C,n)) = Wmi by JORDAN1F:8;
then Wmi in rng Lower_Seq(C,n) by REVROT_1:3;
hence LSeg(Gauge(C,n)*(i,1),Gij) meets L~Lower_Seq(C,n)
by A10,A16,A17,XBOOLE_0:3;
suppose A18: Gij in L~Upper_Seq(C,n) &
Gij <> Upper_Seq(C,n).len Upper_Seq(C,n)
& E-max L~Cage(C,n) <> NE & i > 1;
then A19: v1 is non empty by JORDAN1E:7;
then len v1 <> 0 by FINSEQ_1:25;
then len v1 > 0 by NAT_1:19;
then A20: 0+1 <= len v1 by NAT_1:38;
then A21: 1 in dom v1 by FINSEQ_3:27;
A22: len v1 in dom v1 & len Upper_Seq(C,n) in dom Upper_Seq(C,n)
by A7,A20,FINSEQ_3:27;
A23: 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 A24: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A23,FINSEQ_6:96;
A25: v1/.(len v1) = v1.(len v1) by A22,FINSEQ_4:def 4
.= Upper_Seq(C,n).len Upper_Seq(C,n) by A18,JORDAN1B:5
.= Upper_Seq(C,n)/.len Upper_Seq(C,n) by A22,FINSEQ_4:def 4
.= (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,A24,FINSEQ_5:45
.= E-max L~Cage(C,n) by A24,FINSEQ_5:48;
then A26: Gv1/.len Gv1 = E-max L~Cage(C,n) by A19,SPRECT_3:11;
A27: v1/.1 = v1.1 by A21,FINSEQ_4:def 4
.= Gij by A18,JORDAN3:58;
then A28: (v1^<*NE*>)/.1 = Gij by A20,BOOLMARK:8;
A29: 1+len v1 >= 1+1 by A20,REAL_1:55;
len v = len Gv1 + 1 by FINSEQ_2:19
.= 1 + len v1 + 1 by FINSEQ_5:8;
then A30: 2 < len v by A29,NAT_1:38;
S-bound L~Cage(C,n) < N-bound L~Cage(C,n) by SPRECT_1:34;
then NE <> Gauge(C,n)*(i,1) by A9,PSCOMP_1:77;
then not NE in {Gauge(C,n)*(i,1)} by TARSKI:def 1;
then A31: not NE in rng <*Gauge(C,n)*(i,1)*> by FINSEQ_1:56;
len Cage(C,n) > 4 by GOBOARD7:36;
then len Cage(C,n) >= 2 by AXIOMS:22;
then A32: rng Cage(C,n) c= L~Cage(C,n) by SPPOL_2:18;
A33: not NE in rng Cage(C,n)
proof
assume A34: NE in rng Cage(C,n);
A35: 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 { p where p is Point of TOP-REAL 2 :
p`1 = E-bound L~Cage(C,n) & p`2 <= N-bound L~Cage(C,n) &
p`2 >= S-bound L~Cage(C,n) } by A35;
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 A32,A34,XBOOLE_0:def 3;
then NE in E-most L~Cage(C,n) by PSCOMP_1:def 40;
then A36: 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 A37: (E-max L~Cage(C,n))`2 = NE`2 by A36,AXIOMS:21;
(E-max L~Cage(C,n))`1 = NE`1 by PSCOMP_1:105;
hence contradiction by A18,A37,TOPREAL3:11;
end;
now per cases;
suppose Gij <> Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1);
then v1 = <*Gij*>^mid(Upper_Seq(C,n),
Index(Gij,Upper_Seq(C,n))+1,len Upper_Seq(C,n)) by JORDAN3:def 4;
then rng v1 = rng <*Gij*> \/ rng mid(Upper_Seq(C,n),
Index(Gij,Upper_Seq(C,n))+1,len Upper_Seq(C,n)) by FINSEQ_1:44;
then A38: rng v1 = {Gij} \/ rng mid(Upper_Seq(C,n),
Index(Gij,Upper_Seq(C,n))+1,len Upper_Seq(C,n)) by FINSEQ_1:55;
not NE in L~Cage(C,n)
proof
assume NE in L~Cage(C,n);
then consider i be Nat such that
A39: 1 <= i and
A40: i+1 <= len Cage(C,n) and
A41: NE in LSeg(Cage(C,n)/.i,Cage(C,n)/.(i+1)) by SPPOL_2:14;
per cases by A39,A40,TOPREAL1:def 7;
suppose A42: (Cage(C,n)/.i)`1 = (Cage(C,n)/.(i+1))`1;
then A43: NE`1 = (Cage(C,n)/.i)`1 by A41,GOBOARD7:5;
A44: NE`2 = N-bound L~Cage(C,n) by PSCOMP_1:77;
A45: i < len Cage(C,n) by A40,NAT_1:38;
then A46: (Cage(C,n)/.i)`2 <= NE`2 by A39,A44,JORDAN5D:13;
A47: 1 <= i+1 by NAT_1:29;
then A48: (Cage(C,n)/.(i+1))`2 <= NE`2 by A40,A44,JORDAN5D:13;
A49: i in dom Cage(C,n) & i+1 in dom Cage(C,n)
by A39,A40,A45,A47,FINSEQ_3:27;
(Cage(C,n)/.i)`2 <= (Cage(C,n)/.(i+1))`2 or
(Cage(C,n)/.i)`2 >= (Cage(C,n)/.(i+1))`2;
then NE`2 <= (Cage(C,n)/.(i+1))`2 or NE`2 <= (Cage(C,n)/.i)`2
by A41,TOPREAL1:10;
then NE`2 = (Cage(C,n)/.(i+1))`2 or NE`2 = (Cage(C,n)/.i)`2
by A46,A48,AXIOMS:21;
then NE = (Cage(C,n)/.(i+1)) or NE = (Cage(C,n)/.i)
by A42,A43,TOPREAL3:11;
hence contradiction by A33,A49,PARTFUN2:4;
suppose A50: (Cage(C,n)/.i)`2 = (Cage(C,n)/.(i+1))`2;
then A51: NE`2 = (Cage(C,n)/.i)`2 by A41,GOBOARD7:6;
A52: NE`1 = E-bound L~Cage(C,n) by PSCOMP_1:76;
A53: i < len Cage(C,n) by A40,NAT_1:38;
then A54: (Cage(C,n)/.i)`1 <= NE`1 by A39,A52,JORDAN5D:14;
A55: 1 <= i+1 by NAT_1:29;
then A56: (Cage(C,n)/.(i+1))`1 <= NE`1 by A40,A52,JORDAN5D:14;
A57: i in dom Cage(C,n) & i+1 in dom Cage(C,n)
by A39,A40,A53,A55,FINSEQ_3:27;
(Cage(C,n)/.i)`1 <= (Cage(C,n)/.(i+1))`1 or
(Cage(C,n)/.i)`1 >= (Cage(C,n)/.(i+1))`1;
then NE`1 <= (Cage(C,n)/.(i+1))`1 or NE`1 <= (Cage(C,n)/.i)`1
by A41,TOPREAL1:9;
then NE`1 = (Cage(C,n)/.(i+1))`1 or NE`1 = (Cage(C,n)/.i)`1
by A54,A56,AXIOMS:21;
then NE = (Cage(C,n)/.(i+1)) or NE = (Cage(C,n)/.i)
by A50,A51,TOPREAL3:11;
hence contradiction by A33,A57,PARTFUN2:4;
end;
then A58: not NE in {Gij} by A3,TARSKI:def 1;
A59: rng mid(Upper_Seq(C,n),Index(Gij,Upper_Seq(C,n))+1,
len Upper_Seq(C,n)) c= rng Upper_Seq(C,n) by JORDAN3:28;
rng Upper_Seq(C,n) c= rng Cage(C,n) by Th47;
then rng mid(Upper_Seq(C,n),Index(Gij,Upper_Seq(C,n))+1,
len Upper_Seq(C,n)) c= rng Cage(C,n) by A59,XBOOLE_1:1;
then not NE in rng mid(Upper_Seq(C,n),Index(Gij,Upper_Seq(C,n))+1,
len Upper_Seq(C,n)) by A33;
hence not NE in rng v1 by A38,A58,XBOOLE_0:def 2;
suppose Gij = Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1);
then v1 = mid(Upper_Seq(C,n),
Index(Gij,Upper_Seq(C,n))+1,len Upper_Seq(C,n)) by JORDAN3:def 4;
then A60: rng v1 c= rng Upper_Seq(C,n) by JORDAN3:28;
rng Upper_Seq(C,n) c= rng Cage(C,n) by Th47;
then rng v1 c= rng Cage(C,n) by A60,XBOOLE_1:1;
hence not NE in rng v1 by A33;
end;
then not NE in rng <*Gauge(C,n)*(i,1)*> \/ rng v1 by A31,XBOOLE_0:def 2;
then not NE in rng Gv1 by FINSEQ_1:44;
then rng Gv1 misses {NE} by ZFMISC_1:56;
then A61: rng Gv1 misses rng <*NE*> by FINSEQ_1:55;
A62: not Gauge(C,n)*(i,1) in L~Upper_Seq(C,n) by A1,A18,Th52;
rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by A7,SPPOL_2:18;
then A63: not Gauge(C,n)*(i,1) in rng Upper_Seq(C,n) by A1,A18,Th52;
not Gauge(C,n)*(i,1) in {Gij} by A18,A62,TARSKI:def 1;
then A64: not Gauge(C,n)*(i,1) in rng <*Gij*> by FINSEQ_1:55;
set ci = mid(Upper_Seq(C,n),Index(Gij,Upper_Seq(C,n))+1,
len Upper_Seq(C,n));
now per cases;
suppose A65: Gij <> Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1);
rng ci c= rng Upper_Seq(C,n) by JORDAN3:28;
then not Gauge(C,n)*(i,1) in rng ci by A63;
then not Gauge(C,n)*(i,1) in rng <*Gij*> \/ rng ci by A64,XBOOLE_0:def
2;
then not Gauge(C,n)*(i,1) in rng(<*Gij*>^ci) by FINSEQ_1:44;
hence not Gauge(C,n)*(i,1) in rng v1 by A65,JORDAN3:def 4;
suppose Gij = Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1);
then v1 = ci by JORDAN3:def 4;
then rng v1 c= rng Upper_Seq(C,n) by JORDAN3:28;
hence not Gauge(C,n)*(i,1) in rng v1 by A63;
end;
then {Gauge(C,n)*(i,1)} misses rng v1 by ZFMISC_1:56;
then A66: rng <*Gauge(C,n)*(i,1)*> misses rng v1 by FINSEQ_1:55;
A67: <*Gauge(C,n)*(i,1)*> is one-to-one by FINSEQ_3:102;
A68: v1 is_S-Seq by A18,JORDAN3:69;
then v1 is one-to-one by TOPREAL1:def 10;
then A69: Gv1 is one-to-one by A66,A67,FINSEQ_3:98;
<*NE*> is one-to-one by FINSEQ_3:102;
then A70: v is one-to-one by A61,A69,FINSEQ_3:98;
A71: <*Gauge(C,n)*(i,1)*> is special by SPPOL_2:39;
A72: v1 is special by A68,TOPREAL1:def 10;
(<*Gauge(C,n)*(i,1)*>/.len <*Gauge(C,n)*(i,1)*>)`1 =
(<*Gauge(C,n)*(i,1)*>/.1)`1 by FINSEQ_1:56
.= Gauge(C,n)*(i,1)`1 by FINSEQ_4:25
.= (v1/.1)`1 by A1,A2,A27,GOBOARD5:3;
then A73: Gv1 is special by A71,A72,GOBOARD2:13;
A74: <*NE*> is special by SPPOL_2:39;
(Gv1/.len Gv1)`1 = NE`1 by A26,PSCOMP_1:105
.= (<*NE*>/.1)`1 by FINSEQ_4:25;
then A75: v is special by A73,A74,GOBOARD2:13;
A76: len Lower_Seq(C,n) >= 2+1 by JORDAN1E:19;
then A77: len Lower_Seq(C,n) > 2 by NAT_1:38;
A78: len Lower_Seq(C,n) > 1 by A76,AXIOMS:22;
then h is S-Sequence_in_R2 by A77,JORDAN3:39;
then Rev h is S-Sequence_in_R2 by SPPOL_2:47;
then A79: 2 <= len Rev h & Rev h is one-to-one & Rev h is special
by TOPREAL1:def 10;
A80: Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:22;
3 <= len Lower_Seq(C,n) by JORDAN1E:19;
then 2 <= len Lower_Seq(C,n) by AXIOMS:22;
then A81: 2 in dom Lower_Seq(C,n) by FINSEQ_3:27;
A82: len Lower_Seq(C,n) in dom Lower_Seq(C,n) by SCMFSA_7:12;
then h is_in_the_area_of Cage(C,n) by A80,A81,SPRECT_2:26;
then A83: Rev h is_in_the_area_of Cage(C,n) by SPRECT_3:68;
A84: h is non empty by A77,A78,JORDAN1B:3;
A85: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
A86: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
then A87: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A85,FINSEQ_6:96;
then 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,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 A85,FINSEQ_6:98;
then (Lower_Seq(C,n)/.len Lower_Seq(C,n))`1 = W-bound L~Cage(C,n)
by PSCOMP_1:84;
then (h/.len h)`1 = W-bound L~Cage(C,n) by A81,A82,SPRECT_2:13;
then A88: (Rev h/.1)`1 = W-bound L~Cage(C,n) by A84,FINSEQ_5:68;
A89: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:34;
then A90: (E-max L~Cage(C,n))..Cage(C,n) < (E-min L~Cage(C,n))..Cage(C,n)
by SPRECT_2:75;
A91: (E-min L~Cage(C,n))..Cage(C,n) <= (S-max L~Cage(C,n))..Cage(C,n)
by A89,SPRECT_2:76;
A92: (S-max L~Cage(C,n))..Cage(C,n) < (S-min L~Cage(C,n))..Cage(C,n)
by A89,SPRECT_2:77;
A93: (S-min L~Cage(C,n))..Cage(C,n) <= (W-min L~Cage(C,n))..Cage(C,n)
by A89,SPRECT_2:78;
(E-max L~Cage(C,n))..Cage(C,n) < (S-max L~Cage(C,n))..Cage(C,n)
by A90,A91,AXIOMS:22;
then (E-max L~Cage(C,n))..Cage(C,n) < (S-min L~Cage(C,n))..Cage(C,n)
by A92,AXIOMS:22;
then A94: (E-max L~Cage(C,n))..Cage(C,n) < (W-min L~Cage(C,n))..Cage(C,n)
by A93,AXIOMS:22;
then A95: (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) =
len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)-
(W-min L~Cage(C,n))..Cage(C,n) by A85,A86,SPRECT_5:10;
0 <= (E-max L~Cage(C,n))..Cage(C,n) by NAT_1:18;
then len Cage(C,n)+0 <= len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)
by AXIOMS:24;
then len Cage(C,n)-(W-min L~Cage(C,n))..Cage(C,n) <=
(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))
by A95,REAL_1:49;
then len Cage(C,n)-(W-min L~Cage(C,n))..Cage(C,n)+1 <=
1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) by AXIOMS:24;
then A96: len(Cage(C,n):-W-min L~Cage(C,n)) <=
1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))
by A85,FINSEQ_5:53;
1+(E-max L~Cage(C,n))..Cage(C,n)<=0+(W-min L~Cage(C,n))..Cage(C,n)
by A94,NAT_1:38;
then 1+(E-max L~Cage(C,n))..Cage(C,n)-(W-min L~Cage(C,n))..Cage(C,n)<=0
by REAL_1:86;
then len Cage(C,n)+(1+(E-max L~Cage(C,n))..Cage(C,n)-
(W-min L~Cage(C,n))..Cage(C,n)) <= len Cage(C,n)+0 by AXIOMS:24;
then len Cage(C,n)+(1+(E-max L~Cage(C,n))..Cage(C,n))-
(W-min L~Cage(C,n))..Cage(C,n) <= len Cage(C,n) by XCMPLX_1:29;
then 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))-
(W-min L~Cage(C,n))..Cage(C,n) <= len Cage(C,n) by XCMPLX_1:1;
then A97: 1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) <=
len Cage(C,n) by A95,XCMPLX_1:29;
A98: 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)-
(W-min L~Cage(C,n))..Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)-
len Cage(C,n) = 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))-
(W-min L~Cage(C,n))..Cage(C,n)+(W-min L~Cage(C,n))..Cage(C,n)-
len Cage(C,n) by XCMPLX_1:29
.= 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))+(-
(W-min L~Cage(C,n))..Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)-
len Cage(C,n) by XCMPLX_0:def 8
.= 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))-len Cage(C,n)
by XCMPLX_1:
139
.= 1+len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)-len Cage(C,n)
by XCMPLX_1:1
.= 1+len Cage(C,n)-len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)
by XCMPLX_1:29
.= 1+(E-max L~Cage(C,n))..Cage(C,n) by XCMPLX_1:26;
then A99: 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)-
(W-min L~Cage(C,n))..Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)-
len Cage(C,n) >= 0 by NAT_1:18;
A100: Lower_Seq(C,n)/.(1+1) = Rotate(Cage(C,n),W-min L~Cage(C,n))/.
(1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)))
by A5,A81,A87,FINSEQ_5:55
.= Cage(C,n)/.(1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),
W-min L~Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)-'len Cage(C,n))
by A85,A96,A97,REVROT_1:17
.= Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)+1)
by A95,A98,A99,BINARITH:def 3;
A101: (N-max L~Cage(C,n))..Cage(C,n) <= (E-max L~Cage(C,n))..Cage(C,n)
by A89,SPRECT_2:74;
(N-max L~Cage(C,n))..Cage(C,n) > 1 by A89,SPRECT_2:73;
then A102: (E-max L~Cage(C,n))..Cage(C,n) > 1 by A101,AXIOMS:22;
(W-min L~Cage(C,n))..Cage(C,n) < len Cage(C,n) by A89,SPRECT_2:80;
then (E-max L~Cage(C,n))..Cage(C,n) < len Cage(C,n) by A94,AXIOMS:22;
then A103: (E-max L~Cage(C,n))..Cage(C,n)+1 <= len Cage(C,n) by NAT_1:38;
Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)) = E-max L~Cage(C,n)
by A86,FINSEQ_5:41;
then (Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)+1))`1 =
E-bound L~Cage(C,n) by A102,A103,JORDAN1E:24;
then (h/.1)`1 = E-bound L~Cage(C,n) by A81,A82,A100,SPRECT_2:12;
then (Rev h/.len h)`1 = E-bound L~Cage(C,n) by A84,FINSEQ_5:68;
then (Rev h/.len Rev h)`1 = E-bound L~Cage(C,n) by FINSEQ_5:def 3;
then A104: Rev h is_a_h.c._for Cage(C,n) by A83,A88,SPRECT_2:def 2;
now let m be Nat;
assume A105: m in dom <*Gauge(C,n)*(i,1)*>;
then m in Seg 1 by FINSEQ_1:55;
then m = 1 by FINSEQ_1:4,TARSKI:def 1;
then <*Gauge(C,n)*(i,1)*>.m = Gauge(C,n)*(i,1) by FINSEQ_1:57;
then A106: <*Gauge(C,n)*(i,1)*>/.m = Gauge(C,n)*(i,1)
by A105,FINSEQ_4:def 4;
width Gauge(C,n) >= 4 by A8,JORDAN8:13;
then A107: 1 <= width Gauge(C,n) by AXIOMS:22;
then Gauge(C,n)*(1,1)`1 <= Gauge(C,n)*(i,1)`1 by A1,SPRECT_3:25;
hence W-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,1)*>/.m)`1
by A8,A106,A107,JORDAN1A:94;
(Gauge(C,n)*(i,1))`1 <= Gauge(C,n)*(len Gauge(C,n),1)`1
by A1,A107,SPRECT_3:25;
hence (<*Gauge(C,n)*(i,1)*>/.m)`1 <= E-bound L~Cage(C,n)
by A8,A106,A107,JORDAN1A:92;
thus S-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,1)*>/.m)`2
by A1,A106,JORDAN1A:93;
S-bound L~Cage(C,n) = Gauge(C,n)*(i,1)`2 by A1,JORDAN1A:93;
hence (<*Gauge(C,n)*(i,1)*>/.m)`2 <= N-bound L~Cage(C,n)
by A106,SPRECT_1:24;
end;
then A108: <*Gauge(C,n)*(i,1)*> is_in_the_area_of Cage(C,n)
by SPRECT_2:def 1;
A109: Upper_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:21;
then <*Gij*> is_in_the_area_of Cage(C,n) by A18,SPRECT_3:63;
then v1 is_in_the_area_of Cage(C,n) by A18,A109,SPRECT_3:73;
then A110: Gv1 is_in_the_area_of Cage(C,n) by A108,SPRECT_2:28;
<*NE*> is_in_the_area_of Cage(C,n) by SPRECT_2:29;
then A111: v is_in_the_area_of Cage(C,n) by A110,SPRECT_2:28;
v = <*Gauge(C,n)*(i,1)*>^(v1^<*NE*>) by FINSEQ_1:45;
then v/.1 = Gauge(C,n)*(i,1) by FINSEQ_5:16;
then A112: (v/.1)`2 = S-bound L~Cage(C,n) by A1,JORDAN1A:93;
len v = len Gv1 + 1 by FINSEQ_2:19;
then v/.(len v) = NE by TOPREAL4:1;
then (v/.len v)`2 = N-bound L~Cage(C,n) by PSCOMP_1:77;
then v is_a_v.c._for Cage(C,n) by A111,A112,SPRECT_2:def 3;
then L~Rev h meets L~v by A30,A70,A75,A79,A104,SPRECT_2:33;
then L~h meets L~v by SPPOL_2:22;
then consider x be set such that
A113: x in L~h and
A114: x in L~v by XBOOLE_0:3;
A115: L~h c= L~Lower_Seq(C,n) by A7,JORDAN4:47;
A116: L~v1 c= L~Upper_Seq(C,n) by A18,JORDAN3:77;
L~v = L~(<*Gauge(C,n)*(i,1)*>^(v1^<*NE*>)) by FINSEQ_1:45
.= LSeg(Gauge(C,n)*(i,1),(v1^<*NE*>)/.1) \/ L~(v1^<*NE*>)
by SPPOL_2:20
.= LSeg(Gauge(C,n)*(i,1),(v1^<*NE*>)/.1) \/
(L~v1 \/ LSeg(v1/.(len v1),NE)) by A19,SPPOL_2:19;
then A117: x in LSeg(Gauge(C,n)*(i,1),(v1^<*NE*>)/.1) or
x in L~v1 \/ LSeg(v1/.(len v1),NE) by A114,XBOOLE_0:def 2;
Lower_Seq(C,n)/.1 = (Rotate(Cage(C,n),W-min L~Cage(C,n)):-
E-max L~Cage(C,n))/.1 by JORDAN1E:def 2
.= E-max L~Cage(C,n) by FINSEQ_5:56;
then A118: not E-max L~Cage(C,n) in L~h by A77,JORDAN5B:16;
now per cases by A117,XBOOLE_0:def 2;
suppose x in LSeg(Gauge(C,n)*(i,1),(v1^<*NE*>)/.1);
then x in L~<*Gauge(C,n)*(i,1),Gij*> by A28,SPPOL_2:21;
hence L~Lower_Seq(C,n) meets L~<*Gauge(C,n)*(i,1),Gij*>
by A113,A115,XBOOLE_0:3;
suppose A119: x in L~v1;
then x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n)
by A113,A115,A116,XBOOLE_0:def 3;
then x in {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:20;
then A120: x = W-min L~Cage(C,n) by A113,A118,TARSKI:def 2;
1 in dom Upper_Seq(C,n) by A7,FINSEQ_3:27;
then Upper_Seq(C,n).1 = Upper_Seq(C,n)/.1 by FINSEQ_4:def 4
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by A6,A24,FINSEQ_5:47
.= W-min L~Cage(C,n) by A23,FINSEQ_6:98;
then x = Gij by A18,A119,A120,JORDAN1E:11;
then x in LSeg(Gauge(C,n)*(i,1),Gij) by TOPREAL1:6;
then x in L~<*Gauge(C,n)*(i,1),Gij*> by SPPOL_2:21;
hence L~Lower_Seq(C,n) meets L~<*Gauge(C,n)*(i,1),Gij*>
by A113,A115,XBOOLE_0:3;
suppose A121: x in LSeg(v1/.(len v1),NE);
x in L~Cage(C,n) by A4,A113,A115,XBOOLE_0:def 2;
then x in LSeg(E-max L~Cage(C,n), NE) /\ L~Cage(C,n)
by A25,A121,XBOOLE_0:def 3;
then x in {E-max L~Cage(C,n)} by PSCOMP_1:112;
hence L~Lower_Seq(C,n) meets L~<*Gauge(C,n)*(i,1),Gij*>
by A113,A118,TARSKI:def 1;
end;
then L~<*Gauge(C,n)*(i,1),Gij*> meets L~Lower_Seq(C,n);
hence LSeg(Gauge(C,n)*(i,1),Gij) meets L~Lower_Seq(C,n) by SPPOL_2:21;
suppose A122: Gij in L~Upper_Seq(C,n) &
Gij <> Upper_Seq(C,n).len Upper_Seq(C,n)
& E-max L~Cage(C,n) = NE & i > 1;
then A123: v1 is non empty by JORDAN1E:7;
then len v1 <> 0 by FINSEQ_1:25;
then len v1 > 0 by NAT_1:19;
then A124: 0+1 <= len v1 by NAT_1:38;
then A125: 1 in dom v1 by FINSEQ_3:27;
A126: len v1 in dom v1 & len Upper_Seq(C,n) in dom Upper_Seq(C,n)
by A7,A124,FINSEQ_3:27;
A127: 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 A128: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A127,FINSEQ_6:96;
v1/.(len v1) = v1.(len v1) by A126,FINSEQ_4:def 4
.= Upper_Seq(C,n).len Upper_Seq(C,n) by A122,JORDAN1B:5
.= Upper_Seq(C,n)/.len Upper_Seq(C,n) by A126,FINSEQ_4:def 4
.= (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,A128,FINSEQ_5:45
.= E-max L~Cage(C,n) by A128,FINSEQ_5:48;
then A129: Gv1/.len Gv1 = E-max L~Cage(C,n) by A123,SPRECT_3:11;
A130: v1/.1 = v1.1 by A125,FINSEQ_4:def 4
.= Gij by A122,JORDAN3:58;
1+len v1 >= 1+1 by A124,REAL_1:55;
then A131: len Gv1 >= 2 by FINSEQ_5:8;
A132: not Gauge(C,n)*(i,1) in L~Upper_Seq(C,n) by A1,A122,Th52;
rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by A7,SPPOL_2:18;
then A133: not Gauge(C,n)*(i,1) in rng Upper_Seq(C,n) by A1,A122,Th52;
not Gauge(C,n)*(i,1) in {Gij} by A122,A132,TARSKI:def 1;
then A134: not Gauge(C,n)*(i,1) in rng <*Gij*> by FINSEQ_1:55;
set ci = mid(Upper_Seq(C,n),Index(Gij,Upper_Seq(C,n))+1,
len Upper_Seq(C,n));
now per cases;
suppose A135: Gij <> Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1);
rng ci c= rng Upper_Seq(C,n) by JORDAN3:28;
then not Gauge(C,n)*(i,1) in rng ci by A133;
then not Gauge(C,n)*(i,1) in rng <*Gij*> \/ rng ci by A134,XBOOLE_0:def
2;
then not Gauge(C,n)*(i,1) in rng(<*Gij*>^ci) by FINSEQ_1:44;
hence not Gauge(C,n)*(i,1) in rng v1 by A135,JORDAN3:def 4;
suppose Gij = Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1);
then v1 = ci by JORDAN3:def 4;
then rng v1 c= rng Upper_Seq(C,n) by JORDAN3:28;
hence not Gauge(C,n)*(i,1) in rng v1 by A133;
end;
then {Gauge(C,n)*(i,1)} misses rng v1 by ZFMISC_1:56;
then A136: rng <*Gauge(C,n)*(i,1)*> misses rng v1 by FINSEQ_1:55;
A137: <*Gauge(C,n)*(i,1)*> is one-to-one by FINSEQ_3:102;
A138: v1 is_S-Seq by A122,JORDAN3:69;
then v1 is one-to-one by TOPREAL1:def 10;
then A139: Gv1 is one-to-one by A136,A137,FINSEQ_3:98;
A140: <*Gauge(C,n)*(i,1)*> is special by SPPOL_2:39;
A141: v1 is special by A138,TOPREAL1:def 10;
(<*Gauge(C,n)*(i,1)*>/.len <*Gauge(C,n)*(i,1)*>)`1 =
(<*Gauge(C,n)*(i,1)*>/.1)`1 by FINSEQ_1:56
.= Gauge(C,n)*(i,1)`1 by FINSEQ_4:25
.= (v1/.1)`1 by A1,A2,A130,GOBOARD5:3;
then A142: Gv1 is special by A140,A141,GOBOARD2:13;
A143: len Lower_Seq(C,n) >= 2+1 by JORDAN1E:19;
then A144: len Lower_Seq(C,n) > 2 by NAT_1:38;
A145: len Lower_Seq(C,n) > 1 by A143,AXIOMS:22;
then h is S-Sequence_in_R2 by A144,JORDAN3:39;
then Rev h is S-Sequence_in_R2 by SPPOL_2:47;
then A146: 2 <= len Rev h & Rev h is one-to-one & Rev h is special
by TOPREAL1:def 10;
A147: Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:22;
3 <= len Lower_Seq(C,n) by JORDAN1E:19;
then 2 <= len Lower_Seq(C,n) by AXIOMS:22;
then A148: 2 in dom Lower_Seq(C,n) by FINSEQ_3:27;
A149: len Lower_Seq(C,n) in dom Lower_Seq(C,n) by SCMFSA_7:12;
then h is_in_the_area_of Cage(C,n) by A147,A148,SPRECT_2:26;
then A150: Rev h is_in_the_area_of Cage(C,n) by SPRECT_3:68;
A151: h is non empty by A144,A145,JORDAN1B:3;
A152: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
A153: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
then A154: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A152,FINSEQ_6:96;
then 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,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 A152,FINSEQ_6:98;
then (Lower_Seq(C,n)/.len Lower_Seq(C,n))`1 = W-bound L~Cage(C,n)
by PSCOMP_1:84;
then (h/.len h)`1 = W-bound L~Cage(C,n) by A148,A149,SPRECT_2:13;
then A155: (Rev h/.1)`1 = W-bound L~Cage(C,n) by A151,FINSEQ_5:68;
A156: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:34;
then A157: (E-max L~Cage(C,n))..Cage(C,n) < (E-min L~Cage(C,n))..Cage(C,n
)
by SPRECT_2:75;
A158: (E-min L~Cage(C,n))..Cage(C,n) <= (S-max L~Cage(C,n))..Cage(C,n)
by A156,SPRECT_2:76;
A159: (S-max L~Cage(C,n))..Cage(C,n) < (S-min L~Cage(C,n))..Cage(C,n)
by A156,SPRECT_2:77;
A160: (S-min L~Cage(C,n))..Cage(C,n) <= (W-min L~Cage(C,n))..Cage(C,n)
by A156,SPRECT_2:78;
(E-max L~Cage(C,n))..Cage(C,n) < (S-max L~Cage(C,n))..Cage(C,n)
by A157,A158,AXIOMS:
22;
then (E-max L~Cage(C,n))..Cage(C,n) < (S-min L~Cage(C,n))..Cage(C,n)
by A159,AXIOMS:22;
then A161: (E-max L~Cage(C,n))..Cage(C,n) < (W-min L~Cage(C,n))..Cage(C,n
)
by A160,AXIOMS:22;
then A162: (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) =
len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)-
(W-min L~Cage(C,n))..Cage(C,n) by A152,A153,SPRECT_5:10;
0 <= (E-max L~Cage(C,n))..Cage(C,n) by NAT_1:18;
then len Cage(C,n)+0 <= len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)
by AXIOMS:24;
then len Cage(C,n)-(W-min L~Cage(C,n))..Cage(C,n) <=
(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))
by A162,REAL_1:49;
then len Cage(C,n)-(W-min L~Cage(C,n))..Cage(C,n)+1 <=
1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) by AXIOMS:24;
then A163: len(Cage(C,n):-W-min L~Cage(C,n)) <=
1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))
by A152,FINSEQ_5:53;
1+(E-max L~Cage(C,n))..Cage(C,n)<=0+(W-min L~Cage(C,n))..Cage(C,n)
by A161,NAT_1:38;
then 1+(E-max L~Cage(C,n))..Cage(C,n)-(W-min L~Cage(C,n))..Cage(C,n)<=0
by REAL_1:86;
then len Cage(C,n)+(1+(E-max L~Cage(C,n))..Cage(C,n)-
(W-min L~Cage(C,n))..Cage(C,n)) <= len Cage(C,n)+0 by AXIOMS:24;
then len Cage(C,n)+(1+(E-max L~Cage(C,n))..Cage(C,n))-
(W-min L~Cage(C,n))..Cage(C,n) <= len Cage(C,n) by XCMPLX_1:29;
then 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))-
(W-min L~Cage(C,n))..Cage(C,n) <= len Cage(C,n) by XCMPLX_1:1;
then A164: 1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) <=
len Cage(C,n) by A162,XCMPLX_1:29;
A165: 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)-
(W-min L~Cage(C,n))..Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)-
len Cage(C,n) = 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))-
(W-min L~Cage(C,n))..Cage(C,n)+(W-min L~Cage(C,n))..Cage(C,n)-
len Cage(C,n) by XCMPLX_1:29
.= 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))+(-
(W-min L~Cage(C,n))..Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)-
len Cage(C,n) by XCMPLX_0:def 8
.= 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n))-len Cage(C,n)
by XCMPLX_1:
139
.= 1+len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)-len Cage(C,n)
by XCMPLX_1:1
.= 1+len Cage(C,n)-len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)
by XCMPLX_1:29
.= 1+(E-max L~Cage(C,n))..Cage(C,n) by XCMPLX_1:26;
then A166: 1+(len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n)-
(W-min L~Cage(C,n))..Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)-
len Cage(C,n) >= 0 by NAT_1:18;
A167: Lower_Seq(C,n)/.(1+1) = Rotate(Cage(C,n),W-min L~Cage(C,n))/.
(1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)))
by A5,A148,A154,FINSEQ_5:55
.= Cage(C,n)/.(1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),
W-min L~Cage(C,n))+(W-min L~Cage(C,n))..Cage(C,n)-'len Cage(C,n))
by A152,A163,A164,REVROT_1:17
.= Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)+1)
by A162,A165,A166,BINARITH:def 3;
A168: (N-max L~Cage(C,n))..Cage(C,n) <= (E-max L~Cage(C,n))..Cage(C,n)
by A156,SPRECT_2:74;
(N-max L~Cage(C,n))..Cage(C,n) > 1 by A156,SPRECT_2:73;
then A169: (E-max L~Cage(C,n))..Cage(C,n) > 1 by A168,AXIOMS:22;
(W-min L~Cage(C,n))..Cage(C,n) < len Cage(C,n) by A156,SPRECT_2:80;
then (E-max L~Cage(C,n))..Cage(C,n) < len Cage(C,n) by A161,AXIOMS:22;
then A170: (E-max L~Cage(C,n))..Cage(C,n)+1 <= len Cage(C,n) by NAT_1:38;
Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)) = E-max L~Cage(C,n)
by A153,FINSEQ_5:41;
then (Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)+1))`1 =
E-bound L~Cage(C,n) by A169,A170,JORDAN1E:24;
then (h/.1)`1 = E-bound L~Cage(C,n) by A148,A149,A167,SPRECT_2:12;
then (Rev h/.len h)`1 = E-bound L~Cage(C,n) by A151,FINSEQ_5:68;
then (Rev h/.len Rev h)`1 = E-bound L~Cage(C,n) by FINSEQ_5:def 3;
then A171: Rev h is_a_h.c._for Cage(C,n) by A150,A155,SPRECT_2:def 2;
now let m be Nat;
assume A172: m in dom <*Gauge(C,n)*(i,1)*>;
then m in Seg 1 by FINSEQ_1:55;
then m = 1 by FINSEQ_1:4,TARSKI:def 1;
then <*Gauge(C,n)*(i,1)*>.m = Gauge(C,n)*(i,1) by FINSEQ_1:57;
then A173: <*Gauge(C,n)*(i,1)*>/.m = Gauge(C,n)*(i,1)
by A172,FINSEQ_4:def 4;
width Gauge(C,n) >= 4 by A8,JORDAN8:13;
then A174: 1 <= width Gauge(C,n) by AXIOMS:22;
then Gauge(C,n)*(1,1)`1 <= Gauge(C,n)*(i,1)`1 by A1,SPRECT_3:25;
hence W-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,1)*>/.m)`1
by A8,A173,A174,JORDAN1A:94;
(Gauge(C,n)*(i,1))`1 <= Gauge(C,n)*(len Gauge(C,n),1)`1
by A1,A174,SPRECT_3:25;
hence (<*Gauge(C,n)*(i,1)*>/.m)`1 <= E-bound L~Cage(C,n)
by A8,A173,A174,JORDAN1A:92;
thus S-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,1)*>/.m)`2
by A1,A173,J