:: Upper and Lower Sequence on the Cage. Part II
:: by Robert Milewski
::
:: Received September 28, 2001
:: Copyright (c) 2001-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, ZFMISC_1, FINSEQ_1, XBOOLE_0, RELAT_1,
FINSEQ_5, MATRIX_1, GOBOARD1, FINSEQ_4, ARYTM_3, RFINSEQ, RCOMP_1,
RELAT_2, SPPOL_1, EUCLID, JORDAN1E, JORDAN8, JORDAN9, FINSEQ_6, PSCOMP_1,
TOPREAL1, GOBOARD5, MCART_1, XXREAL_0, TREES_1, PARTFUN1, FUNCT_1,
ARYTM_1, RLTOPSP1, TARSKI, CARD_1, PRE_TOPC, ORDINAL4, NEWTON, NAT_1,
JORDAN1A, SPPOL_2, JORDAN3, SPRECT_2, GROUP_2, JORDAN5C, JORDAN6,
XCMPLX_0;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1,
NUMBERS, XCMPLX_0, XXREAL_0, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1,
FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_0, MATRIX_1, FINSEQ_6, STRUCT_0,
PRE_TOPC, NEWTON, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, PSCOMP_1,
SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD5, SPPOL_1, SPPOL_2, JORDAN3,
JORDAN8, JORDAN5C, JORDAN6, JORDAN9, JORDAN1A, JORDAN1E, NAT_1;
constructors REAL_1, FINSEQ_4, NEWTON, RFINSEQ, FINSEQ_5, CONNSP_1, TOPS_2,
MATRIX_1, TOPMETR, PSCOMP_1, JORDAN3, JORDAN5C, JORDAN6, JORDAN8,
GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, NAT_D;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1,
FINSEQ_5, FINSEQ_6, STRUCT_0, PRE_TOPC, GOBOARD1, SPPOL_2, SPRECT_1,
SPRECT_2, SPRECT_3, REVROT_1, TOPREAL6, JORDAN8, JORDAN1A, JORDAN1E,
CARD_1, EUCLID, SPPOL_1, NEWTON, ORDINAL1, SUBSET_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities PSCOMP_1, ORDINAL1;
expansions TARSKI, XBOOLE_0;
theorems EUCLID, JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, GOBOARD5, FINSEQ_1,
FINSEQ_2, JORDAN4, JORDAN6, SPRECT_2, FINSEQ_4, FINSEQ_5, FINSEQ_6,
GOBOARD7, SPPOL_1, SPPOL_2, REVROT_1, TOPREAL1, SPRECT_3, BOOLMARK,
JORDAN5B, JORDAN3, JORDAN9, ZFMISC_1, GOBOARD1, SPRECT_1, TARSKI,
TOPREAL3, FINSEQ_3, RELAT_1, FUNCT_1, TOPREAL5, JORDAN10, GOBOARD2,
CARD_1, CARD_2, ENUMSET1, SPRECT_4, JORDAN1B, SPRECT_5, JORDAN5D,
JORDAN1E, PARTFUN2, JORDAN1F, JORDAN5C, XBOOLE_0, XBOOLE_1, XREAL_1,
XXREAL_0, ORDINAL1, PARTFUN1, MATRIX_0, XREAL_0, NAT_D, RLTOPSP1;
schemes NAT_1;
begin
reserve n for Nat;
registration
cluster trivial for FinSequence;
existence
proof
take {};
thus thesis;
end;
end;
theorem Th1:
for f be trivial FinSequence
holds f is empty or ex x be object st f = <*x*>
proof
let f be trivial FinSequence;
assume f is non empty;
then consider x be object such that
A1: f = {x} by ZFMISC_1:131;
x in {x} by TARSKI:def 1;
then consider y,z be object such that
A2: x = [y,z] by A1,RELAT_1:def 1;
A3: 1 in dom f by A1,FINSEQ_5:6;
take z;
dom f = {y} by A1,A2,RELAT_1:9;
then 1 = y by A3,TARSKI:def 1;
hence thesis by A1,A2,FINSEQ_1:def 5;
end;
registration
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;
end;
suppose
ex x be object st Rev p = <*x*>;
then consider x be object such that
A2: Rev p = <*x*>;
p = Rev <*x*> by A2
.= <*x*> by FINSEQ_5:60;
hence contradiction;
end;
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:22;
hence thesis 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;
ex i be Element of NAT st i+1 = p..f & f:-p = f/^i by A1,FINSEQ_5:49;
hence thesis by A2,JORDAN8:2;
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;
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then
A1: Rotate(Cage(C,n),W-min L~Cage(C,n)) is_sequence_on Gauge(C,n) by
REVROT_1:34;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by
FINSEQ_6:90,SPRECT_2:43;
then Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n) is_sequence_on
Gauge(C,n) by A1,Th3;
hence thesis by JORDAN1E:def 2;
end;
registration
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:4;
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:4;
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 <= j1 & j1 <= width G by A1,MATRIX_0:32;
A6: j1 < j2 or j1 > j2 by A4,XXREAL_0:1;
A7: 1 <= i2 & i2 <= len G by A2,MATRIX_0:32;
A8: 1 <= j2 & j2 <= width G by A2,MATRIX_0:32;
A9: 1 <= i1 & i1 <= len G by A1,MATRIX_0:32;
then G*(i1,j2)`2 = G*(1,j2)`2 by A8,GOBOARD5:1
.= G*(i2,j2)`2 by A7,A8,GOBOARD5:1;
hence contradiction by A3,A9,A5,A8,A6,GOBOARD5:4;
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 by A1,MATRIX_0:32;
A6: 1 <= i2 & i2 <= len G by A2,MATRIX_0:32;
A7: 1 <= j2 & j2 <= width G by A2,MATRIX_0:32;
A8: i1 < i2 or i1 > i2 by A4,XXREAL_0:1;
1 <= j1 & j1 <= width G by A1,MATRIX_0:32;
then G*(i1,j1)`1 = G*(i1,1)`1 by A5,GOBOARD5:2
.= G*(i1,j2)`1 by A5,A7,GOBOARD5:2;
hence contradiction by A3,A5,A6,A7,A8,GOBOARD5:3;
end;
theorem Th8:
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 NAT_D:60;
A3: p`2 = N-bound L~f by EUCLID:52;
A4: p in rng f by SPRECT_2:39;
then
A5: i in dom f by FINSEQ_4:20;
then
A6: 1 <= i & i <= len f by FINSEQ_3:25;
A7: p = f.i by A4,FINSEQ_4:19
.= f/.i by A5,PARTFUN1:def 6;
per cases by A6,XXREAL_0:1;
suppose
A8: i = 1;
p`2 = (N-max L~f)`2 by PSCOMP_1:37;
then
A9: p`1 <> (N-max L~f)`1 by A1,A7,A8,TOPREAL3:6;
p`1 <= (N-max L~f)`1 by PSCOMP_1:38;
hence thesis by A9,XXREAL_0:1;
end;
suppose
A10: i = len f;
p`2 = (N-max L~f)`2 by PSCOMP_1:37;
then
A11: p`1 <> (N-max L~f)`1 by A1,A7,A10,TOPREAL3:6;
p`1 <= (N-max L~f)`1 by PSCOMP_1:38;
hence thesis by A11,XXREAL_0:1;
end;
suppose that
A12: 1 < i and
A13: i < len f;
A14: i-'1+1 = i by A12,XREAL_1:235;
then
A15: i-'1 >= 1 by A12,NAT_1:13;
then
A16: f/.(i-'1) in LSeg(f,i-'1) by A13,A14,TOPREAL1:21;
i-'1 <= i by A14,NAT_1:11;
then i-'1 <= len f by A13,XXREAL_0:2;
then
A17: i-'1 in dom f by A15,FINSEQ_3:25;
then
A18: f/.(i-'1) in L~f by A2,GOBOARD1:1;
A19: i+1 <= len f by A13,NAT_1:13;
then
A20: f/.(i+1) in LSeg(f,i) by A12,TOPREAL1:21;
i+1 >= 1 by NAT_1:11;
then
A21: i+1 in dom f by A19,FINSEQ_3:25;
then
A22: f/.(i+1) in L~f by A2,GOBOARD1:1;
A23: p <> f/.(i+1) by A4,A7,A21,FINSEQ_4:20,GOBOARD7:29;
A24: p in LSeg(f,i) by A7,A12,A19,TOPREAL1:21;
A25: p in LSeg(f,i-'1) by A7,A13,A14,A15,TOPREAL1:21;
A26: p <> f/.(i-'1) by A5,A7,A14,A17,GOBOARD7:29;
A27: not(LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical)
proof
assume LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical;
then
A28: p`1 = (f/.(i+1))`1 & p`1 = (f/.(i-'1))`1 by A25,A24,A16,A20,SPPOL_1:def 3
;
A29: (f/.(i+1))`2 <= (f/.(i-'1))`2 or (f/.(i+1))`2 >= (f/.(i-'1))`2;
A30: p`2 >= (f/.(i+1))`2 & p`2 >= (f/.(i-'1))`2 by A3,A18,A22,PSCOMP_1:24;
LSeg(f,i) = LSeg(f/.i,f/.(i+1)) & LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1
)) by A12,A13,A14,A15,A19,TOPREAL1:def 3;
then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A7,A28,A30,A29
,GOBOARD7:7;
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 A16,A20,XBOOLE_0:def 4;
then i-'1+1+1 = i-'1+(1+1) & LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A7
,A26,A23,TARSKI:def 1;
hence contradiction by A14,A15,A19,TOPREAL1:def 6;
end;
now
per cases by A27,SPPOL_1:19;
suppose
LSeg(f,i-'1) is horizontal;
then
A31: p`2 = (f/.(i-'1))`2 by A25,A16,SPPOL_1:def 2;
then
A32: f/.(i-'1) in N-most L~f by A2,A3,A17,GOBOARD1:1,SPRECT_2:10;
then
A33: (f/.(i-'1))`1 >= p`1 by PSCOMP_1:39;
(f/.(i-'1))`1 <> p`1 by A5,A7,A14,A17,A31,GOBOARD7:29,TOPREAL3:6;
then
A34: (f/.(i-'1))`1 > p`1 by A33,XXREAL_0:1;
(f/.(i-'1))`1 <= (N-max L~f)`1 by A32,PSCOMP_1:39;
hence thesis by A34,XXREAL_0:2;
end;
suppose
LSeg(f,i) is horizontal;
then
A35: p`2 = (f/.(i+1))`2 by A24,A20,SPPOL_1:def 2;
then
A36: f/.(i+1) in N-most L~f by A2,A3,A21,GOBOARD1:1,SPRECT_2:10;
then
A37: (f/.(i+1))`1 >= p`1 by PSCOMP_1:39;
(f/.(i+1))`1 <> p`1 by A5,A7,A21,A35,GOBOARD7:29,TOPREAL3:6;
then
A38: (f/.(i+1))`1 > p`1 by A37,XXREAL_0:1;
(f/.(i+1))`1 <= (N-max L~f)`1 by A36,PSCOMP_1:39;
hence thesis by A38,XXREAL_0:2;
end;
end;
hence thesis;
end;
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 Th8;
hence thesis;
end;
theorem Th10:
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 NAT_D:60;
A3: p`2 = S-bound L~f by EUCLID:52;
A4: p in rng f by SPRECT_2:41;
then
A5: i in dom f by FINSEQ_4:20;
then
A6: 1 <= i & i <= len f by FINSEQ_3:25;
A7: p = f.i by A4,FINSEQ_4:19
.= f/.i by A5,PARTFUN1:def 6;
per cases by A6,XXREAL_0:1;
suppose
A8: i = 1;
p`2 = (S-max L~f)`2 by PSCOMP_1:53;
then
A9: p`1 <> (S-max L~f)`1 by A1,A7,A8,TOPREAL3:6;
p`1 <= (S-max L~f)`1 by PSCOMP_1:54;
hence thesis by A9,XXREAL_0:1;
end;
suppose
A10: i = len f;
p`2 = (S-max L~f)`2 by PSCOMP_1:53;
then
A11: p`1 <> (S-max L~f)`1 by A1,A7,A10,TOPREAL3:6;
p`1 <= (S-max L~f)`1 by PSCOMP_1:54;
hence thesis by A11,XXREAL_0:1;
end;
suppose that
A12: 1 < i and
A13: i < len f;
A14: i-'1+1 = i by A12,XREAL_1:235;
then
A15: i-'1 >= 1 by A12,NAT_1:13;
then
A16: f/.(i-'1) in LSeg(f,i-'1) by A13,A14,TOPREAL1:21;
i-'1 <= i by A14,NAT_1:11;
then i-'1 <= len f by A13,XXREAL_0:2;
then
A17: i-'1 in dom f by A15,FINSEQ_3:25;
then
A18: f/.(i-'1) in L~f by A2,GOBOARD1:1;
A19: i+1 <= len f by A13,NAT_1:13;
then
A20: f/.(i+1) in LSeg(f,i) by A12,TOPREAL1:21;
i+1 >= 1 by NAT_1:11;
then
A21: i+1 in dom f by A19,FINSEQ_3:25;
then
A22: f/.(i+1) in L~f by A2,GOBOARD1:1;
A23: p <> f/.(i+1) by A4,A7,A21,FINSEQ_4:20,GOBOARD7:29;
A24: p in LSeg(f,i) by A7,A12,A19,TOPREAL1:21;
A25: p in LSeg(f,i-'1) by A7,A13,A14,A15,TOPREAL1:21;
A26: p <> f/.(i-'1) by A5,A7,A14,A17,GOBOARD7:29;
A27: not(LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical)
proof
assume LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical;
then
A28: p`1 = (f/.(i+1))`1 & p`1 = (f/.(i-'1))`1 by A25,A24,A16,A20,SPPOL_1:def 3
;
A29: (f/.(i+1))`2 <= (f/.(i-'1))`2 or (f/.(i+1))`2 >= (f/.(i-'1))`2;
A30: p`2 <= (f/.(i+1))`2 & p`2 <= (f/.(i-'1))`2 by A3,A18,A22,PSCOMP_1:24;
LSeg(f,i) = LSeg(f/.i,f/.(i+1)) & LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1
)) by A12,A13,A14,A15,A19,TOPREAL1:def 3;
then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A7,A28,A30,A29
,GOBOARD7:7;
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 A16,A20,XBOOLE_0:def 4;
then i-'1+1+1 = i-'1+(1+1) & LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A7
,A26,A23,TARSKI:def 1;
hence contradiction by A14,A15,A19,TOPREAL1:def 6;
end;
now
per cases by A27,SPPOL_1:19;
suppose
LSeg(f,i-'1) is horizontal;
then
A31: p`2 = (f/.(i-'1))`2 by A25,A16,SPPOL_1:def 2;
then
A32: f/.(i-'1) in S-most L~f by A2,A3,A17,GOBOARD1:1,SPRECT_2:11;
then
A33: (f/.(i-'1))`1 >= p`1 by PSCOMP_1:55;
(f/.(i-'1))`1 <> p`1 by A5,A7,A14,A17,A31,GOBOARD7:29,TOPREAL3:6;
then
A34: (f/.(i-'1))`1 > p`1 by A33,XXREAL_0:1;
(f/.(i-'1))`1 <= (S-max L~f)`1 by A32,PSCOMP_1:55;
hence thesis by A34,XXREAL_0:2;
end;
suppose
LSeg(f,i) is horizontal;
then
A35: p`2 = (f/.(i+1))`2 by A24,A20,SPPOL_1:def 2;
then
A36: f/.(i+1) in S-most L~f by A2,A3,A21,GOBOARD1:1,SPRECT_2:11;
then
A37: (f/.(i+1))`1 >= p`1 by PSCOMP_1:55;
(f/.(i+1))`1 <> p`1 by A5,A7,A21,A35,GOBOARD7:29,TOPREAL3:6;
then
A38: (f/.(i+1))`1 > p`1 by A37,XXREAL_0:1;
(f/.(i+1))`1 <= (S-max L~f)`1 by A36,PSCOMP_1:55;
hence thesis by A38,XXREAL_0:2;
end;
end;
hence thesis;
end;
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 Th10;
hence thesis;
end;
theorem Th12:
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 NAT_D:60;
A3: p`1 = W-bound L~f by EUCLID:52;
A4: p in rng f by SPRECT_2:43;
then
A5: i in dom f by FINSEQ_4:20;
then
A6: 1 <= i & i <= len f by FINSEQ_3:25;
A7: p = f.i by A4,FINSEQ_4:19
.= f/.i by A5,PARTFUN1:def 6;
per cases by A6,XXREAL_0:1;
suppose
A8: i = 1;
p`1 = (W-max L~f)`1 by PSCOMP_1:29;
then
A9: p`2 <> (W-max L~f)`2 by A1,A7,A8,TOPREAL3:6;
p`2 <= (W-max L~f)`2 by PSCOMP_1:30;
hence thesis by A9,XXREAL_0:1;
end;
suppose
A10: i = len f;
p`1 = (W-max L~f)`1 by PSCOMP_1:29;
then
A11: p`2 <> (W-max L~f)`2 by A1,A7,A10,TOPREAL3:6;
p`2 <= (W-max L~f)`2 by PSCOMP_1:30;
hence thesis by A11,XXREAL_0:1;
end;
suppose that
A12: 1 < i and
A13: i < len f;
A14: i-'1+1 = i by A12,XREAL_1:235;
then
A15: i-'1 >= 1 by A12,NAT_1:13;
then
A16: f/.(i-'1) in LSeg(f,i-'1) by A13,A14,TOPREAL1:21;
i-'1 <= i by A14,NAT_1:11;
then i-'1 <= len f by A13,XXREAL_0:2;
then
A17: i-'1 in dom f by A15,FINSEQ_3:25;
then
A18: f/.(i-'1) in L~f by A2,GOBOARD1:1;
A19: i+1 <= len f by A13,NAT_1:13;
then
A20: f/.(i+1) in LSeg(f,i) by A12,TOPREAL1:21;
i+1 >= 1 by NAT_1:11;
then
A21: i+1 in dom f by A19,FINSEQ_3:25;
then
A22: f/.(i+1) in L~f by A2,GOBOARD1:1;
A23: p <> f/.(i+1) by A4,A7,A21,FINSEQ_4:20,GOBOARD7:29;
A24: p in LSeg(f,i) by A7,A12,A19,TOPREAL1:21;
A25: p in LSeg(f,i-'1) by A7,A13,A14,A15,TOPREAL1:21;
A26: p <> f/.(i-'1) by A5,A7,A14,A17,GOBOARD7:29;
A27: not(LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal)
proof
assume LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal;
then
A28: p`2 = (f/.(i+1))`2 & p`2 = (f/.(i-'1))`2 by A25,A24,A16,A20,SPPOL_1:def 2
;
A29: (f/.(i+1))`1 <= (f/.(i-'1))`1 or (f/.(i+1))`1 >= (f/.(i-'1))`1;
A30: p`1 <= (f/.(i+1))`1 & p`1 <= (f/.(i-'1))`1 by A3,A18,A22,PSCOMP_1:24;
LSeg(f,i) = LSeg(f/.i,f/.(i+1)) & LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1
)) by A12,A13,A14,A15,A19,TOPREAL1:def 3;
then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A7,A28,A30,A29
,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 A16,A20,XBOOLE_0:def 4;
then i-'1+1+1 = i-'1+(1+1) & LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A7
,A26,A23,TARSKI:def 1;
hence contradiction by A14,A15,A19,TOPREAL1:def 6;
end;
now
per cases by A27,SPPOL_1:19;
suppose
LSeg(f,i-'1) is vertical;
then
A31: p`1 = (f/.(i-'1))`1 by A25,A16,SPPOL_1:def 3;
then
A32: f/.(i-'1) in W-most L~f by A2,A3,A17,GOBOARD1:1,SPRECT_2:12;
then
A33: (f/.(i-'1))`2 >= p`2 by PSCOMP_1:31;
(f/.(i-'1))`2 <> p`2 by A5,A7,A14,A17,A31,GOBOARD7:29,TOPREAL3:6;
then
A34: (f/.(i-'1))`2 > p`2 by A33,XXREAL_0:1;
(f/.(i-'1))`2 <= (W-max L~f)`2 by A32,PSCOMP_1:31;
hence thesis by A34,XXREAL_0:2;
end;
suppose
LSeg(f,i) is vertical;
then
A35: p`1 = (f/.(i+1))`1 by A24,A20,SPPOL_1:def 3;
then
A36: f/.(i+1) in W-most L~f by A2,A3,A21,GOBOARD1:1,SPRECT_2:12;
then
A37: (f/.(i+1))`2 >= p`2 by PSCOMP_1:31;
(f/.(i+1))`2 <> p`2 by A5,A7,A21,A35,GOBOARD7:29,TOPREAL3:6;
then
A38: (f/.(i+1))`2 > p`2 by A37,XXREAL_0:1;
(f/.(i+1))`2 <= (W-max L~f)`2 by A36,PSCOMP_1:31;
hence thesis by A38,XXREAL_0:2;
end;
end;
hence thesis;
end;
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 Th12;
hence thesis;
end;
theorem Th14:
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 NAT_D:60;
A3: p`1 = E-bound L~f by EUCLID:52;
A4: p in rng f by SPRECT_2:45;
then
A5: i in dom f by FINSEQ_4:20;
then
A6: 1 <= i & i <= len f by FINSEQ_3:25;
A7: p = f.i by A4,FINSEQ_4:19
.= f/.i by A5,PARTFUN1:def 6;
per cases by A6,XXREAL_0:1;
suppose
A8: i = 1;
p`1 = (E-max L~f)`1 by PSCOMP_1:45;
then
A9: p`2 <> (E-max L~f)`2 by A1,A7,A8,TOPREAL3:6;
p`2 <= (E-max L~f)`2 by PSCOMP_1:46;
hence thesis by A9,XXREAL_0:1;
end;
suppose
A10: i = len f;
p`1 = (E-max L~f)`1 by PSCOMP_1:45;
then
A11: p`2 <> (E-max L~f)`2 by A1,A7,A10,TOPREAL3:6;
p`2 <= (E-max L~f)`2 by PSCOMP_1:46;
hence thesis by A11,XXREAL_0:1;
end;
suppose that
A12: 1 < i and
A13: i < len f;
A14: i-'1+1 = i by A12,XREAL_1:235;
then
A15: i-'1 >= 1 by A12,NAT_1:13;
then
A16: f/.(i-'1) in LSeg(f,i-'1) by A13,A14,TOPREAL1:21;
i-'1 <= i by A14,NAT_1:11;
then i-'1 <= len f by A13,XXREAL_0:2;
then
A17: i-'1 in dom f by A15,FINSEQ_3:25;
then
A18: f/.(i-'1) in L~f by A2,GOBOARD1:1;
A19: i+1 <= len f by A13,NAT_1:13;
then
A20: f/.(i+1) in LSeg(f,i) by A12,TOPREAL1:21;
i+1 >= 1 by NAT_1:11;
then
A21: i+1 in dom f by A19,FINSEQ_3:25;
then
A22: f/.(i+1) in L~f by A2,GOBOARD1:1;
A23: p <> f/.(i+1) by A4,A7,A21,FINSEQ_4:20,GOBOARD7:29;
A24: p in LSeg(f,i) by A7,A12,A19,TOPREAL1:21;
A25: p in LSeg(f,i-'1) by A7,A13,A14,A15,TOPREAL1:21;
A26: p <> f/.(i-'1) by A5,A7,A14,A17,GOBOARD7:29;
A27: not(LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal)
proof
assume LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal;
then
A28: p`2 = (f/.(i+1))`2 & p`2 = (f/.(i-'1))`2 by A25,A24,A16,A20,SPPOL_1:def 2
;
A29: (f/.(i+1))`1 <= (f/.(i-'1))`1 or (f/.(i+1))`1 >= (f/.(i-'1))`1;
A30: p`1 >= (f/.(i+1))`1 & p`1 >= (f/.(i-'1))`1 by A3,A18,A22,PSCOMP_1:24;
LSeg(f,i) = LSeg(f/.i,f/.(i+1)) & LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1
)) by A12,A13,A14,A15,A19,TOPREAL1:def 3;
then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A7,A28,A30,A29
,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 A16,A20,XBOOLE_0:def 4;
then i-'1+1+1 = i-'1+(1+1) & LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A7
,A26,A23,TARSKI:def 1;
hence contradiction by A14,A15,A19,TOPREAL1:def 6;
end;
now
per cases by A27,SPPOL_1:19;
suppose
LSeg(f,i-'1) is vertical;
then
A31: p`1 = (f/.(i-'1))`1 by A25,A16,SPPOL_1:def 3;
then
A32: f/.(i-'1) in E-most L~f by A2,A3,A17,GOBOARD1:1,SPRECT_2:13;
then
A33: (f/.(i-'1))`2 >= p`2 by PSCOMP_1:47;
(f/.(i-'1))`2 <> p`2 by A5,A7,A14,A17,A31,GOBOARD7:29,TOPREAL3:6;
then
A34: (f/.(i-'1))`2 > p`2 by A33,XXREAL_0:1;
(f/.(i-'1))`2 <= (E-max L~f)`2 by A32,PSCOMP_1:47;
hence thesis by A34,XXREAL_0:2;
end;
suppose
LSeg(f,i) is vertical;
then
A35: p`1 = (f/.(i+1))`1 by A24,A20,SPPOL_1:def 3;
then
A36: f/.(i+1) in E-most L~f by A2,A3,A21,GOBOARD1:1,SPRECT_2:13;
then
A37: (f/.(i+1))`2 >= p`2 by PSCOMP_1:47;
(f/.(i+1))`2 <> p`2 by A5,A7,A21,A35,GOBOARD7:29,TOPREAL3:6;
then
A38: (f/.(i+1))`2 > p`2 by A37,XXREAL_0:1;
(f/.(i+1))`2 <= (E-max L~f)`2 by A36,PSCOMP_1:47;
hence thesis by A38,XXREAL_0:2;
end;
end;
hence thesis;
end;
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 Th14;
hence thesis;
end;
theorem Th16:
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;
assume that
A1: p in rng f and
A2: q in rng f and
A3: q..f <= p..f;
A4: f-:p = f|(p..f) & (f:-q)-:p = (f:-q)|(p..(f:-q)) by FINSEQ_5:def 1;
consider i be Element of NAT such that
A5: i+1 = q..f and
A6: f:-q = f/^i by A2,FINSEQ_5:49;
A7: i < p..f by A3,A5,NAT_1:13;
then p..f = i + p..(f/^i) by A1,FINSEQ_6:56;
then
A8: p..(f/^i) = p..f-i .= p..f-'i by A7,XREAL_1:233;
q in rng (f-:p) by A1,A2,A3,FINSEQ_5:46;
then
A9: ex j be Element of NAT st j+1 = q..(f-:p) & (f-:p):-q = ( f-:p)/^j by
FINSEQ_5:49;
q..(f-:p) = q..f by A1,A2,A3,SPRECT_5:3;
hence thesis by A5,A6,A9,A4,A8,FINSEQ_5:80;
end;
theorem Th17:
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: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
then
A2: Cage(C,n)-:pW <> {} by FINSEQ_5:47;
len(f-:pW) = pW..f by A1,FINSEQ_5:42;
then (f-:pW)/.len (f-:pW) = pW by A1,FINSEQ_5:45;
then
A3: pW in rng (Cage(C,n)-:pW) by A2,FINSEQ_6:168;
A4: f/.1 = pN by JORDAN9:32;
then pEa..f < pEi..f by SPRECT_2:71;
then pNa..f < pEi..f by A4,SPRECT_2:70,XXREAL_0:2;
then pNa..f < pSa..f by A4,SPRECT_2:72,XXREAL_0:2;
then
A5: pNa..f < pSi..f by A4,SPRECT_2:73,XXREAL_0:2;
(Cage(C,n)-:pW)/.1 = Cage(C,n)/.1 by A1,FINSEQ_5:44
.= pN by JORDAN9:32;
then
A6: N-min L~Cage(C,n) in rng (Cage(C,n)-:W-min L~Cage(C,n)) by A2,FINSEQ_6:42;
N-max L~Cage(C,n) in rng Cage(C,n) & pSi..f <= pW..f by A4,SPRECT_2:40,74;
then
A7: pNa in rng (f-:pW) by A1,A5,FINSEQ_5:46,XXREAL_0:2;
A8: {pN,pNa,pW} c= rng US
by A6,A7,A3,ENUMSET1:def 1;
then
A9: card {pN,pNa,pW} c= card rng US by CARD_1:11;
(Cage(C,n):-pW)/.1 = pW by FINSEQ_5:53;
then
A10: W-min L~Cage(C,n) in rng (Cage(C,n):-W-min L~Cage(C,n)) by FINSEQ_6:42;
(f:-pW)/.len(f:-pW) = f/.len f by A1,FINSEQ_5:54
.= f/.1 by FINSEQ_6:def 1
.= pN by JORDAN9:32;
then
A11: pN in rng (Cage(C,n):-pW) by FINSEQ_6:168;
{pN,pW} c= rng LS
by A11,A10,TARSKI:def 2;
then
A12: card {pN,pW} c= card rng LS by CARD_1:11;
card rng LS c= card dom LS by CARD_2:61;
then
A13: card rng LS c= len LS by CARD_1:62;
W-max L~f in L~f & pN`2 = N-bound L~f by EUCLID:52,SPRECT_1:13;
then (W-max L~f)`2 <= pN`2 by PSCOMP_1:24;
then
A14: pN <> pW by SPRECT_2:57;
then card {pN,pW} = 2 by CARD_2:57;
then Segm 2 c= Segm len LS by A12,A13;
then len LS >= 2 by NAT_1:39;
then
A15: rng LS c= L~LS by SPPOL_2:18;
LS/.(len LS) = Cage(C,n)/.len Cage(C,n) by A1,FINSEQ_5:54
.= Cage(C,n)/.1 by FINSEQ_6:def 1
.= N-min L~Cage(C,n) by JORDAN9:32;
then
A16: N-min L~Cage(C,n) in rng LS by FINSEQ_6:168;
(W-min L~Cage(C,n))..Cage(C,n) <= (W-min L~Cage(C,n))..Cage(C,n);
then
A17: W-min L~Cage(C,n) in rng LS & W-min L~Cage(C,n) in rng US by A1,
FINSEQ_5:46,FINSEQ_6:61;
W-max L~f in L~f & pNa`2 = N-bound L~f by EUCLID:52,SPRECT_1:13;
then (W-max L~f)`2 <= pNa`2 by PSCOMP_1:24;
then pN <> pNa & pNa <> pW by SPRECT_2:52,57;
then
A18: card {pN,pNa,pW} = 3 by A14,CARD_2:58;
card rng US c= card dom US by CARD_2:61;
then card rng US c= len US by CARD_1:62;
then Segm 3 c= Segm len US by A18,A9;
then
A19: len US >= 3 by NAT_1:39;
then
A20: rng US c= L~US by SPPOL_2:18,XXREAL_0:2;
thus L~US /\ L~LS c= {N-min L~Cage(C,n),W-min L~Cage(C,n)}
proof
let x be object;
assume
A21: x in L~US /\ L~LS;
then reconsider x1=x as Point of TOP-REAL 2;
assume
A22: not x in {N-min L~Cage(C,n),W-min L~Cage(C,n)};
x in L~US by A21,XBOOLE_0:def 4;
then consider i1 be Nat such that
A23: 1 <= i1 and
A24: i1+1 <= len US and
A25: x1 in LSeg(US,i1) by SPPOL_2:13;
A26: LSeg(US,i1) = LSeg(f,i1) by A24,SPPOL_2:9;
x in L~LS by A21,XBOOLE_0:def 4;
then consider i2 be Nat such that
A27: 1 <= i2 and
A28: i2+1 <= len LS and
A29: x1 in LSeg(LS,i2) by SPPOL_2:13;
set i3=i2-'1;
A30: i3+1 = i2 by A27,XREAL_1:235;
then
A31: 1+pW..f <= i3+1+pW..f by A27,XREAL_1:7;
A32: len LS = len f-pW..f+1 by A1,FINSEQ_5:50;
then i2 < len f-pW..f+1 by A28,NAT_1:13;
then i2-1 < len f-pW..f by XREAL_1:19;
then
A33: i2-1+pW..f < len f by XREAL_1:20;
i2-1 >= 1-1 by A27,XREAL_1:9;
then
A34: i3+pW..f < len f by A33,XREAL_0:def 2;
A35: LSeg(LS,i2) = LSeg(f,i3+pW..f) by A1,A30,SPPOL_2:10;
A36: len US = pW..f by A1,FINSEQ_5:42;
then i1+1 < pW..f+1 by A24,NAT_1:13;
then i1+1 < i3+pW..f+1 by A31,XXREAL_0:2;
then
A37: i1+1 <= i3+pW..f by NAT_1:13;
A38: pW..f-'1+1 = pW..f by A1,FINSEQ_4:21,XREAL_1:235;
i3+1 < len f-pW..f+1 by A28,A30,A32,NAT_1:13;
then i3 < len f-pW..f by XREAL_1:7;
then
A39: i3+pW..f < len f by XREAL_1:20;
then
A40: i3+pW..f+1 <= len f by NAT_1:13;
now
per cases by A23,A37,XXREAL_0:1;
suppose
i1+1 < i3+pW..f & i1 > 1;
then LSeg(f,i1) misses LSeg(f,i3+pW..f) by A39,GOBOARD5:def 4;
then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {};
hence contradiction by A25,A29,A26,A35,XBOOLE_0:def 4;
end;
suppose
A41: i1 = 1;
i3+pW..f >= 0+3 by A19,A36,XREAL_1:7;
then
A42: i1+1 < i3+pW..f by A41,XXREAL_0:2;
now
per cases by A40,XXREAL_0:1;
suppose
i3+pW..f+1 < len f;
then LSeg(f,i1) misses LSeg(f,i3+pW..f) by A42,GOBOARD5:def 4;
then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {};
hence contradiction by A25,A29,A26,A35,XBOOLE_0:def 4;
end;
suppose
i3+pW..f+1 = len f;
then i3+pW..f = len f-1;
then i3+pW..f = len f-'1 by XREAL_0:def 2;
then LSeg(f,i1) /\ LSeg(f,i3+pW..f) = {f/.1} by A41,GOBOARD7:34
,REVROT_1:30;
then x1 in {f/.1} by A25,A29,A26,A35,XBOOLE_0:def 4;
then x1 = f/.1 by TARSKI:def 1
.= pN by JORDAN9:32;
hence contradiction by A22,TARSKI:def 2;
end;
end;
hence contradiction;
end;
suppose
A43: i1+1 = i3+pW..f;
i3+pW..f >= pW..f by NAT_1:11;
then pW..f < len f by A34,XXREAL_0:2;
then pW..f+1 <= len f by NAT_1:13;
then
A44: pW..f-'1 + (1+1) <= len f by A38;
0+pW..f <= i3+pW..f by XREAL_1:7;
then pW..f = i1+1 by A24,A36,A43,XXREAL_0:1;
then LSeg(f,i1) /\ LSeg(f,i3+(pW..f)) = {f/.(pW..f)} by A23,A38,A43,A44
,TOPREAL1:def 6;
then x1 in {f/.(pW..f)} by A25,A29,A26,A35,XBOOLE_0:def 4;
then x1 = f/.(pW..f) by TARSKI:def 1
.= pW by A1,FINSEQ_5:38;
hence contradiction by A22,TARSKI:def 2;
end;
end;
hence contradiction;
end;
A45: US/.1 = Cage(C,n)/.1 by A1,FINSEQ_5:44
.= N-min L~Cage(C,n) by JORDAN9:32;
US is non empty by A8;
then
A46: N-min L~Cage(C,n) in rng US by A45,FINSEQ_6:42;
thus {N-min L~Cage(C,n),W-min L~Cage(C,n)} c= L~US /\ L~LS
proof
let x be object;
assume
A47: x in {N-min L~Cage(C,n),W-min L~Cage(C,n)};
per cases by A47,TARSKI:def 2;
suppose
x = N-min L~Cage(C,n);
hence thesis by A15,A20,A46,A16,XBOOLE_0:def 4;
end;
suppose
x = W-min L~Cage(C,n);
hence thesis by A15,A20,A17,XBOOLE_0:def 4;
end;
end;
end;
theorem Th18:
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: Ema in rng Cage(C,n) by SPRECT_2:46;
Wma in L~Cage(C,n) & Nmi`2 = N-bound L~Cage(C,n) by EUCLID:52,SPRECT_1:13;
then Wma`2 <= Nmi`2 by PSCOMP_1:24;
then Nmi <> Wmi by SPRECT_2:57;
then
A2: card {Nmi,Wmi} = 2 by CARD_2:57;
A3: Wmi in rng Cage(C,n) by SPRECT_2:43;
then
A4: Cage(C,n)-:Wmi <> {} by FINSEQ_5:47;
len(Cage(C,n)-:Wmi) = Wmi..Cage(C,n) by A3,FINSEQ_5:42;
then (Cage(C,n)-:Wmi)/.len (Cage(C,n)-:Wmi) = Wmi by A3,FINSEQ_5:45;
then
A5: Wmi in rng (Cage(C,n)-:Wmi) by A4,FINSEQ_6:168;
(Cage(C,n)-:Wmi)/.1 = Cage(C,n)/.1 by A3,FINSEQ_5:44
.= Nmi by JORDAN9:32;
then
A6: Nmi in rng (Cage(C,n)-:Wmi) by A4,FINSEQ_6:42;
{Nmi,Wmi} c= rng (Cage(C,n)-:Wmi)
by A6,A5,TARSKI:def 2;
then
A7: card {Nmi,Wmi} c= card rng (Cage(C,n)-:Wmi) by CARD_1:11;
card rng (Cage(C,n)-:Wmi) c= card dom (Cage(C,n)-:Wmi) by CARD_2:61;
then card rng (Cage(C,n)-:Wmi) c= len (Cage(C,n)-:Wmi) by CARD_1:62;
then Segm 2 c= Segm len (Cage(C,n)-:Wmi) by A2,A7;
then len (Cage(C,n)-:Wmi) >= 2 by NAT_1:39;
then
A8: rng (Cage(C,n)-:Wmi) c= L~(Cage(C,n)-:Wmi) by SPPOL_2:18;
A9: Cage(C,n)/.1 = Nmi by JORDAN9:32;
then Emi..Cage(C,n) <= Sma..Cage(C,n) by SPRECT_2:72;
then Ema..Cage(C,n) < Sma..Cage(C,n) by A9,SPRECT_2:71,XXREAL_0:2;
then
A10: Ema..Cage(C,n) < Smi..Cage(C,n) by A9,SPRECT_2:73,XXREAL_0:2;
then
A11: Ema..Cage(C,n) < Wmi..Cage(C,n) by A9,SPRECT_2:74,XXREAL_0:2;
A12: Smi..Cage(C,n) <= Wmi..Cage(C,n) by A9,SPRECT_2:74;
then
A13: Ema in rng (Cage(C,n)-:Wmi) by A3,A1,A10,FINSEQ_5:46,XXREAL_0:2;
Nma`1 <= (NE-corner L~Cage(C,n))`1 by PSCOMP_1:38;
then Nmi`1 < Nma`1 & Nma`1 <= E-bound L~Cage(C,n) by EUCLID:52,SPRECT_2:51;
then
A14: Nmi <> Ema by EUCLID:52;
A15: not Ema in rng (Cage(C,n):-Wmi)
proof
(Cage(C,n):-Wmi)/.1 = Wmi by FINSEQ_5:53;
then
A16: Wmi in rng (Cage(C,n):-Wmi) by FINSEQ_6:42;
(Cage(C,n):-Wmi)/.len(Cage(C,n):-Wmi) = Cage(C,n)/.len Cage(C,n) by A3,
FINSEQ_5:54
.= Cage(C,n)/.1 by FINSEQ_6:def 1
.= Nmi by JORDAN9:32;
then
A17: Nmi in rng (Cage(C,n):-Wmi) by FINSEQ_6:168;
{Nmi,Wmi} c= rng (Cage(C,n):-Wmi)
by A17,A16,TARSKI:def 2;
then
A18: card {Nmi,Wmi} c= card rng (Cage(C,n):-Wmi) by CARD_1:11;
Wma in L~Cage(C,n) & Nmi`2 = N-bound L~Cage(C,n) by EUCLID:52,SPRECT_1:13;
then Wma`2 <= Nmi`2 by PSCOMP_1:24;
then Nmi <> Wmi by SPRECT_2:57;
then
A19: card {Nmi,Wmi} = 2 by CARD_2:57;
card rng (Cage(C,n):-Wmi) c= card dom (Cage(C,n):-Wmi) by CARD_2:61;
then card rng (Cage(C,n):-Wmi) c= len (Cage(C,n):-Wmi) by CARD_1:62;
then Segm 2 c= Segm len (Cage(C,n):-Wmi) by A19,A18;
then len (Cage(C,n):-Wmi) >= 2 by NAT_1:39;
then
A20: rng (Cage(C,n):-Wmi) c= L~(Cage(C,n):-Wmi) by SPPOL_2:18;
assume Ema in rng (Cage(C,n):-Wmi);
then Ema in L~(Cage(C,n)-:Wmi) /\ L~(Cage(C,n):-Wmi) by A13,A8,A20,
XBOOLE_0:def 4;
then Ema in {Nmi,Wmi} by Th17;
then Ema = Wmi by A14,TARSKI:def 2;
hence contradiction by TOPREAL5:19;
end;
A21: Nma..Cage(C,n) <= Ema..Cage(C,n) by A9,SPRECT_2:70;
A22: Nmi..Cage(C,n) < Nma..Cage(C,n) by A9,SPRECT_2:68;
then
A23: Nmi in rng Cage(C,n) & Nmi..Cage(C,n) < Ema..Cage(C,n) by A9,SPRECT_2:39
,70,XXREAL_0:2;
then
A24: Nmi in rng (Cage(C,n)-:Wmi) by A3,A11,FINSEQ_5:46,XXREAL_0:2;
A25: Ema..(Cage(C,n)-:Wmi) <> 1
proof
assume
A26: Ema..(Cage(C,n)-:Wmi) = 1;
Nmi..(Cage(C,n)-:Wmi) = Nmi..Cage(C,n) by A3,A23,A11,SPRECT_5:3,XXREAL_0:2
.= 1 by A9,FINSEQ_6:43;
hence contradiction by A22,A21,A13,A24,A26,FINSEQ_5:9;
end;
then Ema in rng (Cage(C,n)-:Wmi/^1) by A13,FINSEQ_6:78;
then
A27: Ema in rng (Cage(C,n)-:Wmi/^1) \ rng (Cage(C,n):-Wmi) by A15,
XBOOLE_0:def 5;
A28: Wmi in rng (Cage(C,n):-Ema) by A3,A1,A12,A10,FINSEQ_6:62,XXREAL_0:2;
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 A27,FINSEQ_6:65
.= (Cage(C,n)-:Wmi):-Ema by A13,A25,FINSEQ_6:83
.= (Cage(C,n):-Ema)-:Wmi by A3,A1,A12,A10,Th16,XXREAL_0:2
.= ((Cage(C,n):-Ema)^((Cage(C,n)-:Ema)/^1))-:Wmi by A28,FINSEQ_6:66
.= RotEma-:Wmi by A1,FINSEQ_6:def 2;
hence thesis by JORDAN1E:def 2;
end;
theorem Th19:
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 thesis by FINSEQ_6:43;
end;
theorem Th20:
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: L~Rot = L~Cage(C,n) by REVROT_1:33;
then
A2: Wmi in rng Rot by SPRECT_2:43;
A3: Wma in rng Rot by A1,SPRECT_2:44;
A4: Ema in rng Rot by A1,SPRECT_2:46;
Wmi in rng Cage(C,n) by SPRECT_2:43;
then
A5: Rot/.1 = Wmi by FINSEQ_6:92;
then
A6: Wmi..Rot < Wma..Rot by A1,SPRECT_5:21;
A7: Upper_Seq(C,n) = Rot-:Ema & Nma..Rot <= Ema..Rot by A1,A5,JORDAN1E:def 1
,SPRECT_5:25;
Nmi..Rot < Nma..Rot by A1,A5,SPRECT_5:24;
then
A8: Wma..Rot < Nma..Rot by A1,A5,SPRECT_5:23,XXREAL_0:2;
then Wma..Rot < Ema..Rot by A1,A5,SPRECT_5:25,XXREAL_0:2;
then Wmi..(Rot-:Ema) = Wmi..Rot by A2,A4,A6,SPRECT_5:3,XXREAL_0:2;
hence thesis by A4,A6,A7,A8,A3,SPRECT_5:3,XXREAL_0:2;
end;
theorem Th21:
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: L~Rot = L~Cage(C,n) by REVROT_1:33;
then
A2: Wma in rng Rot by SPRECT_2:44;
A3: Nmi in rng Rot by A1,SPRECT_2:39;
A4: Ema in rng Rot by A1,SPRECT_2:46;
Wmi in rng Cage(C,n) by SPRECT_2:43;
then
A5: Rot/.1 = Wmi by FINSEQ_6:92;
then
A6: Wma..Rot <= Nmi..Rot by A1,SPRECT_5:23;
A7: Upper_Seq(C,n) = Rot-:Ema & Nma..Rot <= Ema..Rot by A1,A5,JORDAN1E:def 1
,SPRECT_5:25;
A8: Nmi..Rot < Nma..Rot by A1,A5,SPRECT_5:24;
then Nmi..Rot < Ema..Rot by A1,A5,SPRECT_5:25,XXREAL_0:2;
then Wma..(Rot-:Ema) = Wma..Rot by A2,A4,A6,SPRECT_5:3,XXREAL_0:2;
hence thesis by A4,A6,A8,A7,A3,SPRECT_5:3,XXREAL_0:2;
end;
theorem Th22:
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: L~Rot = L~Cage(C,n) by REVROT_1:33;
then
A2: Ema in rng Rot by SPRECT_2:46;
Wmi in rng Cage(C,n) by SPRECT_2:43;
then Rot/.1 = Wmi by FINSEQ_6:92;
then
A3: Nmi..Rot < Nma..Rot & Nma..Rot <= Ema..Rot by A1,SPRECT_5:24,25;
A4: Nma in rng Rot by A1,SPRECT_2:40;
Nmi in rng Rot by A1,SPRECT_2:39;
then Upper_Seq(C,n) = Rot-:Ema & Nmi..(Rot-:Ema) = Nmi..Rot by A2,A3,
JORDAN1E:def 1,SPRECT_5:3,XXREAL_0:2;
hence thesis by A2,A3,A4,SPRECT_5:3;
end;
theorem Th23:
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: L~Rot = L~Cage(C,n) by REVROT_1:33;
then
A2: Ema in rng Rot by SPRECT_2:46;
Wmi in rng Cage(C,n) by SPRECT_2:43;
then Rot/.1 = Wmi by FINSEQ_6:92;
then
A3: Nma..Rot <= Ema..Rot by A1,SPRECT_5:25;
Nma in rng Rot by A1,SPRECT_2:40;
then Upper_Seq(C,n) = Rot-:Ema & Nma..(Rot-:Ema) = Nma..Rot by A2,A3,
JORDAN1E:def 1,SPRECT_5:3;
hence thesis by A2,A3,SPRECT_5:3;
end;
theorem Th24:
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;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A1: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_6:90
,SPRECT_2:43;
Upper_Seq(C,n) = Rotate(Cage(C,n),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)) <= (E-max L~Cage(C,
n)) ..Rotate(Cage(C,n),W-min L~Cage(C,n)) by JORDAN1E:def 1;
then E-max L~Cage(C,n) in rng Upper_Seq(C,n) by A1,FINSEQ_5:46;
then
A2: Upper_Seq(C,n) just_once_values E-max L~Cage(C,n) by FINSEQ_4:8;
Upper_Seq(C,n)/.len Upper_Seq(C,n) = E-max L~Cage(C,n) by JORDAN1F:7;
hence thesis by A2,FINSEQ_6:166;
end;
theorem Th25:
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 thesis by FINSEQ_6:43;
end;
theorem Th26:
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 Th18;
A2: L~Rot = L~Cage(C,n) by REVROT_1:33;
then
A3: Ema in rng Rot by SPRECT_2:46;
A4: Emi in rng Rot by A2,SPRECT_2:45;
A5: Wmi in rng Rot by A2,SPRECT_2:43;
Ema in rng Cage(C,n) by SPRECT_2:46;
then
A6: Rot/.1 = Ema by FINSEQ_6:92;
then
A7: Ema..Rot < Emi..Rot by A2,SPRECT_5:37;
A8: Smi..Rot <= Wmi..Rot by A2,A6,SPRECT_5:41;
Sma..Rot < Smi..Rot by A2,A6,SPRECT_5:40;
then
A9: Emi..Rot < Smi..Rot by A2,A6,SPRECT_5:39,XXREAL_0:2;
then Emi..Rot < Wmi..Rot by A2,A6,SPRECT_5:41,XXREAL_0:2;
then Ema..(Rot-:Wmi) = Ema..Rot by A3,A5,A7,SPRECT_5:3,XXREAL_0:2;
hence thesis by A1,A5,A7,A8,A9,A4,SPRECT_5:3,XXREAL_0:2;
end;
theorem Th27:
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 Th18;
A2: L~Rot = L~Cage(C,n) by REVROT_1:33;
then
A3: Emi in rng Rot by SPRECT_2:45;
A4: Sma in rng Rot by A2,SPRECT_2:42;
A5: Wmi in rng Rot by A2,SPRECT_2:43;
Ema in rng Cage(C,n) by SPRECT_2:46;
then
A6: Rot/.1 = Ema by FINSEQ_6:92;
then
A7: Emi..Rot <= Sma..Rot by A2,SPRECT_5:39;
A8: Smi..Rot <= Wmi..Rot by A2,A6,SPRECT_5:41;
A9: Sma..Rot < Smi..Rot by A2,A6,SPRECT_5:40;
then Sma..Rot < Wmi..Rot by A2,A6,SPRECT_5:41,XXREAL_0:2;
then Emi..(Rot-:Wmi) = Emi..Rot by A3,A5,A7,SPRECT_5:3,XXREAL_0:2;
hence thesis by A1,A5,A7,A9,A8,A4,SPRECT_5:3,XXREAL_0:2;
end;
theorem Th28:
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 Th18;
A2: L~Rot = L~Cage(C,n) by REVROT_1:33;
then
A3: Wmi in rng Rot by SPRECT_2:43;
Ema in rng Cage(C,n) by SPRECT_2:46;
then Rot/.1 = Ema by FINSEQ_6:92;
then
A4: Sma..Rot < Smi..Rot & Smi..Rot <= Wmi..Rot by A2,SPRECT_5:40,41;
A5: Smi in rng Rot by A2,SPRECT_2:41;
Sma in rng Rot by A2,SPRECT_2:42;
then Sma..(Rot-:Wmi) = Sma..Rot by A3,A4,SPRECT_5:3,XXREAL_0:2;
hence thesis by A1,A3,A4,A5,SPRECT_5:3;
end;
theorem Th29:
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 Th18;
A2: L~Rot = L~Cage(C,n) by REVROT_1:33;
then
A3: Wmi in rng Rot by SPRECT_2:43;
Ema in rng Cage(C,n) by SPRECT_2:46;
then Rot/.1 = Ema by FINSEQ_6:92;
then
A4: Smi..Rot <= Wmi..Rot by A2,SPRECT_5:41;
Smi in rng Rot by A2,SPRECT_2:41;
then Smi..(Rot-:Wmi) = Smi..Rot by A3,A4,SPRECT_5:3;
hence thesis by A1,A3,A4,SPRECT_5:3;
end;
theorem Th30:
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;
W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
then
A1: W-min L~Cage(C,n) in rng Rotate(Cage(C,n),E-max L~Cage(C,n)) by FINSEQ_6:90
,SPRECT_2:46;
Lower_Seq(C,n) = Rotate(Cage(C,n),E-max L~Cage(C,n))-:W-min L~Cage(C,n)
& ( 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)) by Th18;
then W-min L~Cage(C,n) in rng Lower_Seq(C,n) by A1,FINSEQ_5:46;
then
A2: Lower_Seq(C,n) just_once_values W-min L~Cage(C,n) by FINSEQ_4:8;
Lower_Seq(C,n)/.len Lower_Seq(C,n) = W-min L~Cage(C,n) by JORDAN1F:8;
hence thesis by A2,FINSEQ_6:166;
end;
theorem Th31:
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);
Emax in rng Ca by SPRECT_2:46;
then
A1: Emax in rng Rotate(Ca,Wmin) by FINSEQ_6:90,SPRECT_2:43;
len US >= 3 by JORDAN1E:15;
then len US >= 2 by XXREAL_0:2;
then 2 in Seg len US by FINSEQ_1:1;
then
A2: 2 in Seg(Emax..Rotate(Ca,Wmin)) by JORDAN1E:8;
(Ca:-Wmin)/.1 = Wmin by FINSEQ_5:53;
then
A3: Wmin in rng (Ca:-Wmin) by FINSEQ_6:42;
Ca/.1 = Nmin by JORDAN9:32;
then Wmin..Ca < len Ca by SPRECT_2:76;
then
A4: Wmin..Ca+1 <= len Ca by NAT_1:13;
W-max L~Ca in L~Ca & Nmin`2 = N-bound L~Ca by EUCLID:52,SPRECT_1:13;
then (W-max L~Ca)`2 <= Nmin`2 by PSCOMP_1:24;
then Nmin <> Wmin by SPRECT_2:57;
then
A5: card {Nmin,Wmin} = 2 by CARD_2:57;
A6: Wmin in rng Ca by SPRECT_2:43;
then
A7: 1 <= Wmin..Ca by FINSEQ_4:21;
(Ca:-Wmin)/.len(Ca:-Wmin) = Ca/.len Ca by A6,FINSEQ_5:54
.= Ca/.1 by FINSEQ_6:def 1
.= Nmin by JORDAN9:32;
then
A8: Nmin in rng (Ca:-Wmin) by FINSEQ_6:168;
{Nmin,Wmin} c= rng (Ca:-Wmin)
by A8,A3,TARSKI:def 2;
then
A9: card {Nmin,Wmin} c= card rng (Ca:-Wmin) by CARD_1:11;
card rng (Ca:-Wmin) c= card dom (Ca:-Wmin) by CARD_2:61;
then card rng (Ca:-Wmin) c= len (Ca:-Wmin) by CARD_1:62;
then Segm 2 c= Segm len (Ca:-Wmin) by A5,A9;
then
A10: len (Ca:-Wmin) >= 2 by NAT_1:39;
then
A11: len(Ca:-Wmin) >= 1 by XXREAL_0:2;
A12: US/.1 = (Rotate(Ca,Wmin)-:Emax)/.1 by JORDAN1E:def 1
.= Rotate(Ca,Wmin)/.1 by A1,FINSEQ_5:44
.= Ca/.(1-'1+Wmin..Ca) by A6,A11,FINSEQ_6:174
.= Ca/.(0+Wmin..Ca) by XREAL_1:232;
US/.2 = (Rotate(Ca,Wmin)-:Emax)/.2 by JORDAN1E:def 1
.= Rotate(Ca,Wmin)/.2 by A1,A2,FINSEQ_5:43
.= Ca/.(2-'1+Wmin..Ca) by A6,A10,FINSEQ_6:174
.= Ca/.(2-1+Wmin..Ca) by XREAL_0:def 2;
hence thesis by A7,A4,A12,JORDAN1E:22,JORDAN1F:5;
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);
Wmin in rng Ca by SPRECT_2:43;
then
A1: Wmin in rng Rotate(Ca,Emax) by FINSEQ_6:90,SPRECT_2:46;
len LS >= 3 by JORDAN1E:15;
then len LS >= 2 by XXREAL_0:2;
then 2 <= Wmin..LS by Th30;
then 2 <= Wmin..(Rotate(Ca,Emax)-:Wmin) by Th18;
then 2 <= Wmin..Rotate(Ca,Emax) by A1,FINSEQ_6:72;
then
A2: 2 in Seg (Wmin..Rotate(Ca,Emax)) by FINSEQ_1:1;
(Ca:-Emax)/.1 = Emax by FINSEQ_5:53;
then
A3: Emax in rng (Ca:-Emax) by FINSEQ_6:42;
N-max L~Ca in L~Ca & Emax`1 = E-bound L~Ca by EUCLID:52,SPRECT_1:11;
then (N-max L~Ca)`1 <= Emax`1 by PSCOMP_1:24;
then Nmin <> Emax by SPRECT_2:51;
then
A4: card {Nmin,Emax} = 2 by CARD_2:57;
A5: Ca/.1 = Nmin by JORDAN9:32;
then Emax..Ca < Emin..Ca by SPRECT_2:71;
then Emax..Ca < Smax..Ca by A5,SPRECT_2:72,XXREAL_0:2;
then Emax..Ca < Smin..Ca by A5,SPRECT_2:73,XXREAL_0:2;
then Emax..Ca < Wmin..Ca by A5,SPRECT_2:74,XXREAL_0:2;
then Emax..Ca < len Ca by A5,SPRECT_2:76,XXREAL_0:2;
then
A6: Emax..Ca+1 <= len Ca by NAT_1:13;
A7: Emax in rng Ca by SPRECT_2:46;
then
A8: 1 <= Emax..Ca by FINSEQ_4:21;
(Ca:-Emax)/.len(Ca:-Emax) = Ca/.len Ca by A7,FINSEQ_5:54
.= Ca/.1 by FINSEQ_6:def 1
.= Nmin by JORDAN9:32;
then
A9: Nmin in rng (Ca:-Emax) by FINSEQ_6:168;
{Nmin,Emax} c= rng (Ca:-Emax)
by A9,A3,TARSKI:def 2;
then
A10: card {Nmin,Emax} c= card rng (Ca:-Emax) by CARD_1:11;
card rng (Ca:-Emax) c= card dom (Ca:-Emax) by CARD_2:61;
then card rng (Ca:-Emax) c= len (Ca:-Emax) by CARD_1:62;
then Segm 2 c= Segm len (Ca:-Emax) by A4,A10;
then
A11: len (Ca:-Emax) >= 2 by NAT_1:39;
then
A12: len(Ca:-Emax) >= 1 by XXREAL_0:2;
A13: LS/.1 = (Rotate(Ca,Emax)-:Wmin)/.1 by Th18
.= Rotate(Ca,Emax)/.1 by A1,FINSEQ_5:44
.= Ca/.(1-'1+Emax..Ca) by A7,A12,FINSEQ_6:174
.= Ca/.(0+Emax..Ca) by XREAL_1:232;
LS/.2 = (Rotate(Ca,Emax)-:Wmin)/.2 by Th18
.= Rotate(Ca,Emax)/.2 by A1,A2,FINSEQ_5:43
.= Ca/.(2-'1+Emax..Ca) by A7,A11,FINSEQ_6:174
.= Ca/.(2-1+Emax..Ca) by XREAL_0:def 2;
hence thesis by A8,A6,A13,JORDAN1E:20,JORDAN1F:6;
end;
theorem Th33:
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:64
.= (W-bound C - (E-bound C - W-bound C)/(2|^n))+ (E-bound C + (E-bound C
- W-bound C)/(2|^n)) by JORDAN1A:62
.= W-bound C + E-bound C;
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:63
.= S-bound C + N-bound C;
end;
theorem Th35:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for n be Nat, 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 be Nat, i be Nat such that
A1: 1 <= i & i <= width Gauge(C,n);
reconsider ii=i as Nat;
A2: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
assume
A3: n > 0;
len Gauge(C,1) >= 4 by JORDAN8:10;
then
A4: len Gauge(C,1) >= 1 by XXREAL_0:2;
thus Gauge(C,n)*(Center Gauge(C,n),i)`1 = Gauge(C,n)*(Center Gauge(C,n),ii)
`1
.= Gauge(C,1)*(Center Gauge(C,1),1)`1 by A1,A2,A4,A3,JORDAN1A:36
.= (W-bound C + E-bound C) / 2 by A4,JORDAN1A:38;
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:10;
then
A2: len Gauge(C,1) >= 1 by XXREAL_0:2;
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:37
.= (S-bound C + N-bound C) / 2 by A2,JORDAN1A:39;
end;
theorem Th37:
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);
AA: k1 in dom f by FINSEQ_3:25,A1,A2;
assume that
A6: k1 <> 1 and
A7: k2 <> 1;
A8: len f >= 2 by TOPREAL1:def 8;
consider j be Nat such that
A9: 1 <= j and
A10: j+1 <= len mid(f,k1,k2) and
A11: f/.1 in LSeg(mid(f,k1,k2),j) by A5,SPPOL_2:13;
per cases by XXREAL_0:1;
suppose
A12: k1 < k2;
then len mid(f,k1,k2) = k2-'k1 + 1 by A1,A2,A3,A4,FINSEQ_6:118;
then j < k2-'k1 + 1 by A10,NAT_1:13;
then LSeg(mid(f,k1,k2),j) = LSeg(f,j+k1-'1) by A1,A4,A9,A12,JORDAN4:19;
then
A13: j+k1-'1 = 1 by A11,A8,JORDAN5B:30;
j+k1 >= 1+1 by A1,A9,XREAL_1:7;
then j+k1-1 >= 1+1-1 by XREAL_1:9;
then j+(k1-1) = 1 by A13,XREAL_0:def 2;
then k1-1 = 1-j;
then k1-1 <= 0 by A9,XREAL_1:47;
then k1-1 = 0 by A1,XREAL_1:48;
hence contradiction by A6;
end;
suppose
A14: k1 > k2;
then len mid(f,k1,k2) = k1-'k2 + 1 by A1,A2,A3,A4,FINSEQ_6:118;
then
A15: j < k1-'k2 + 1 by A10,NAT_1:13;
k1-k2 > 0 by A14,XREAL_1:50;
then k1-'k2 = k1-k2 by XREAL_0:def 2;
then j-1 < k1-k2 by A15,XREAL_1:19;
then j-1+k2 < k1 by XREAL_1:20;
then j+-(1-k2) < k1;
then
A16: k2-1 < k1-j by XREAL_1:20;
LSeg(mid(f,k1,k2),j) = LSeg(f,k1-'j) by A2,A3,A9,A14,A15,JORDAN4:20;
then k1-'j = 1 by A11,A8,JORDAN5B:30;
then k1-j = 1 by XREAL_0:def 2;
then k2 < 1+1 by A16,XREAL_1:19;
then k2 <= 1 by NAT_1:13;
hence contradiction by A3,A7,XXREAL_0:1;
end;
suppose
k1 = k2;
then mid(f,k1,k2) = <*f.k1*> by AA,FINSEQ_6:193
.= <*f/.k1*> by AA,PARTFUN1:def 6;
hence contradiction by A5,SPPOL_2:12;
end;
end;
theorem Th38:
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);
AA: k1 in dom f by A1,A2,FINSEQ_3:25;
assume that
A6: k1 <> len f and
A7: k2 <> len f;
consider j be Nat such that
A8: 1 <= j and
A9: j+1 <= len mid(f,k1,k2) and
A10: f/.len f in LSeg(mid(f,k1,k2),j) by A5,SPPOL_2:13;
per cases by XXREAL_0:1;
suppose
A11: k1 < k2;
then
A12: len mid(f,k1,k2) = k2-'k1 + 1 by A1,A2,A3,A4,FINSEQ_6:118;
then
A13: j < k2-'k1 + 1 by A9,NAT_1:13;
A14: j+k1 >= 1+1 by A1,A8,XREAL_1:7;
then
A15: j+k1-1 >= 1+1-1 by XREAL_1:9;
then
A16: j+k1-'1 = j+k1-1 by XREAL_0:def 2;
k2-k1 > 0 by A11,XREAL_1:50;
then
A17: k2-'k1 = k2-k1 by XREAL_0:def 2;
then j-1 < k2-k1 by A13,XREAL_1:19;
then j-1+k1 < k2 by XREAL_1:20;
then
A18: j+k1-1 < len f by A4,XXREAL_0:2;
then
A19: j+k1-'1 in dom f by A15,A16,FINSEQ_3:25;
A20: j+k1 >= 1 by A14,XXREAL_0:2;
j+k1-1+1 <= len f by A16,A18,NAT_1:13;
then j+k1 in Seg len f by A20,FINSEQ_1:1;
then
A21: j+k1-'1+1 in dom f by A16,FINSEQ_1:def 3;
LSeg(mid(f,k1,k2),j) = LSeg(f,j+k1-'1) by A1,A4,A8,A11,A13,JORDAN4:19;
then
A22: j+k1-'1+1=len f by A10,A19,A21,GOBOARD2:2;
A23: j+k1-'1 = j+k1-1 by A15,XREAL_0:def 2;
j < k2+1-k1 by A9,A17,A12,NAT_1:13;
then len f < k2+1 by A22,A23,XREAL_1:20;
then len f <= k2 by NAT_1:13;
hence contradiction by A4,A7,XXREAL_0:1;
end;
suppose
A24: k1 > k2;
then len mid(f,k1,k2) = k1-'k2 + 1 by A1,A2,A3,A4,FINSEQ_6:118;
then
A25: j < k1-'k2 + 1 by A9,NAT_1:13;
k1-k2 > 0 by A24,XREAL_1:50;
then k1-'k2 = k1-k2 by XREAL_0:def 2;
then j-1 < k1-k2 by A25,XREAL_1:19;
then j-1+k2 < k1 by XREAL_1:20;
then
A26: j+-(1-k2) < k1;
then
A27: -(1-k2) < k1-j by XREAL_1:20;
A28: k2-1 >= 0 by A3,XREAL_1:48;
then
A29: k1-j+1 > 0+1 by A27,XREAL_1:6;
k2-1 < k1-j by A26,XREAL_1:20;
then
A30: k1-j > 0 by A3,XREAL_1:48;
then
A31: k1-'j = k1-j by XREAL_0:def 2;
k1-j <= k1-1 by A8,XREAL_1:10;
then k1-j+1 <= k1-1+1 by XREAL_1:7;
then k1-j < k1 by A31,NAT_1:13;
then
A32: k1-j < len f by A2,XXREAL_0:2;
then k1-j+1 <= len f by A31,NAT_1:13;
then
A33: k1-'j+1 in dom f by A31,A29,FINSEQ_3:25;
k1-j >= 0+1 by A27,A28,A31,NAT_1:13;
then
A34: k1-'j in dom f by A31,A32,FINSEQ_3:25;
LSeg(mid(f,k1,k2),j) = LSeg(f,k1-'j) by A2,A3,A8,A24,A25,JORDAN4:20;
then k1-'j+1=len f by A10,A34,A33,GOBOARD2:2;
then
A35: k1-j+1=len f by A30,XREAL_0:def 2;
k1-j <= k1-1 by A8,XREAL_1:10;
then len f <= k1-1+1 by A35,XREAL_1:7;
hence contradiction by A2,A6,XXREAL_0:1;
end;
suppose
k1 = k2;
then mid(f,k1,k2) = <*f.k1*> by AA,FINSEQ_6:193
.= <*f/.k1*> by AA,PARTFUN1:def 6;
hence contradiction by A5,SPPOL_2:12;
end;
end;
theorem Th39:
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;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A1: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_6:90
,SPRECT_2:43;
Upper_Seq(C,n) = Rotate(Cage(C,n),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:48;
hence rng Upper_Seq(C,n) c= rng Cage(C,n) by FINSEQ_6:90,SPRECT_2:43;
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 A1,
FINSEQ_5:55;
hence thesis by FINSEQ_6:90,SPRECT_2:43;
end;
theorem Th40:
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)/.1)`1 = (W-min L~Cage(C,n))`1 by JORDAN1F:5
.= W-bound L~Cage(C,n) by EUCLID:52;
A2: (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 EUCLID:52;
Upper_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:17;
hence thesis by A1,A2,SPRECT_2:def 2;
end;
theorem Th41:
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;
A1: (Rev Lower_Seq(C,n)/.1)`1 = (Lower_Seq(C,n)/.len Lower_Seq(C,n))`1 by
FINSEQ_5:65
.= (W-min L~Cage(C,n))`1 by JORDAN1F:8
.= W-bound L~Cage(C,n) by EUCLID:52;
A2: (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:65
.= (E-max L~Cage(C,n))`1 by JORDAN1F:6
.= E-bound L~Cage(C,n) by EUCLID:52;
Rev Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:18,SPRECT_3:51;
hence thesis by A1,A2,SPRECT_2:def 2;
end;
theorem Th42:
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 & i <= len Gauge(C,n) and
A2: Gauge(C,n)*(i,1) in rng Upper_Seq(C,n);
consider i2 be Nat such that
A3: i2 in dom Upper_Seq(C,n) and
A4: Upper_Seq(C,n).i2 = Gauge(C,n)*(i,1) by A2,FINSEQ_2:10;
reconsider i2 as Nat;
A5: 1 <= i2 & i2 <= len Upper_Seq(C,n) by A3,FINSEQ_3:25;
set f = Rotate(Cage(C,n),W-min L~Cage(C,n));
set i1 = (N-min L~Cage(C,n))..Upper_Seq(C,n);
A6: E-max L~Cage(C,n) in rng Cage(C,n) & rng f = rng Cage(C,n) by FINSEQ_6:90
,SPRECT_2:43,46;
W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
then
A7: f/.1 = W-min L~Cage(C,n) by FINSEQ_6:92;
L~Cage(C,n) = L~f by REVROT_1:33;
then
A8: (N-min L~Cage(C,n))..f < (N-max L~Cage(C,n))..f & (N-max L~Cage(C,n))..
f <= (E-max L~Cage(C,n))..f by A7,SPRECT_5:24,25;
(E-max L~Cage(C,n))..Upper_Seq(C,n) = len Upper_Seq(C,n) by Th24;
then (N-max L~Cage(C,n))..Upper_Seq(C,n) <= len Upper_Seq(C,n) by Th23;
then
A9: i1 < len Upper_Seq(C,n) by Th22,XXREAL_0:2;
3 <= len Lower_Seq(C,n) by JORDAN1E:15;
then
A10: 2 <= len Lower_Seq(C,n) by XXREAL_0:2;
A11: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
4 <= len Gauge(C,n) by JORDAN8:10;
then
A12: 1 <= len Gauge(C,n) by XXREAL_0:2;
(W-min L~Cage(C,n))..Upper_Seq(C,n) = 1 & (W-max L~Cage(C,n))..Upper_Seq
(C,n ) <= i1 by Th19,Th21;
then
A13: i1 > 1 by Th20,XXREAL_0:2;
then
A14: i1 in dom Upper_Seq(C,n) by A9,FINSEQ_3:25;
Upper_Seq(C,n) = f-:E-max L~Cage(C,n) & N-min L~Cage(C,n) in rng Cage(C
,n) by JORDAN1E:def 1,SPRECT_2:39;
then
A15: N-min L~Cage(C,n) in rng Upper_Seq(C,n) by A6,A8,FINSEQ_5:46,XXREAL_0:2;
then
A16: Upper_Seq(C,n)/.i1 = N-min L~Cage(C,n) by FINSEQ_5:38;
A17: i1 in NAT & i2 in NAT by ORDINAL1:def 12;
A18: i1 <> i2
proof
assume i1 = i2;
then Gauge(C,n)*(i,1) = N-min L~Cage(C,n) by A4,A14,A16,PARTFUN1:def 6;
then (Gauge(C,n)*(i,1))`2 = N-bound L~Cage(C,n) by EUCLID:52;
then S-bound L~Cage(C,n) = N-bound L~Cage(C,n) by A1,JORDAN1A:72;
hence contradiction by SPRECT_1:16;
end;
then mid(Upper_Seq(C,n),i1,i2) is being_S-Seq by A13,A9,A5,JORDAN3:6,A17;
then reconsider
h1 = mid(Upper_Seq(C,n),i1,i2) as one-to-one special FinSequence
of TOP-REAL 2;
set h = Rev h1;
A19: len h1 = len h by FINSEQ_5:def 3;
then
A20: h1 is non empty by A3,A14,SPRECT_2:5;
then
A21: (h/.len h)`2 = (h1/.1)`2 by A19,FINSEQ_5:65
.= (Upper_Seq(C,n)/.i1)`2 by A3,A14,SPRECT_2:8
.= (N-min L~Cage(C,n))`2 by A15,FINSEQ_5:38
.= N-bound L~Cage(C,n) by EUCLID:52;
h1 is_in_the_area_of Cage(C,n) by A3,A14,JORDAN1E:17,SPRECT_2:22;
then
A22: h is_in_the_area_of Cage(C,n) by SPRECT_3:51;
(h/.1)`2 = (h1/.len h1)`2 by A20,FINSEQ_5:65
.= (Upper_Seq(C,n)/.i2)`2 by A3,A14,SPRECT_2:9
.= (Gauge(C,n)*(i,1))`2 by A3,A4,PARTFUN1:def 6
.= S-bound L~Cage(C,n) by A1,JORDAN1A:72;
then
A23: Rev Lower_Seq(C,n) is special & h is_a_v.c._for Cage(C,n) by A22,A21,
SPRECT_2:def 3;
len h >= 1 by A3,A14,A19,SPRECT_2:5;
then len h > 1 by A3,A14,A18,A19,SPRECT_2:6,XXREAL_0:1;
then
A24: 1+1 <= len h by NAT_1:13;
len Lower_Seq(C,n) = len Rev Lower_Seq(C,n) & h is special by FINSEQ_5:def 3
,SPPOL_2:40;
then
L~Rev Lower_Seq(C,n) = L~Lower_Seq(C,n) & L~Rev Lower_Seq(C,n) meets L~
h by A10,A24,A23,Th41,SPPOL_2:22,SPRECT_2:29;
then consider x be object such that
A25: x in L~Lower_Seq(C,n) and
A26: x in L~h by XBOOLE_0:3;
A27: L~h = L~h1 by SPPOL_2:22;
L~mid(Upper_Seq(C,n),i1,i2) c= L~Upper_Seq(C,n) by A13,A9,A5,JORDAN4:35;
then x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) by A25,A26,A27,XBOOLE_0:def 4;
then
A28: x in {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:16;
per cases by A28,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 A13,A9,A5,A26,A27,Th37;
then Upper_Seq(C,n)/.1 = Gauge(C,n)*(i,1) by A3,A4,PARTFUN1:def 6;
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 EUCLID:52
.= Gauge(C,n)*(1,1)`1 by A12,JORDAN1A:73;
hence contradiction by A1,A12,A11,GOBOARD5:3;
end;
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 A13,A9,A5,A26,A27,Th38;
then Upper_Seq(C,n)/.len Upper_Seq(C,n) = Gauge(C,n)*(i,1) by A3,A4,
PARTFUN1:def 6;
then
A29: E-max(L~Cage(C,n)) = Gauge(C,n)*(i,1) by JORDAN1F:7;
(SE-corner L~Cage(C,n))`2 <= (E-min L~Cage(C,n))`2 by PSCOMP_1:46;
then (SE-corner L~Cage(C,n))`2 < (E-max L~Cage(C,n))`2 by SPRECT_2:53
,XXREAL_0:2;
then S-bound L~Cage(C,n) < (Gauge(C,n)*(i,1))`2 by A29,EUCLID:52;
hence contradiction by A1,JORDAN1A:72;
end;
end;
theorem Th43:
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 & i < len Gauge(C,n) and
A2: Gauge(C,n)*(i,wi) in rng Lower_Seq(C,n);
consider i2 be Nat such that
A3: i2 in dom Lower_Seq(C,n) and
A4: Lower_Seq(C,n).i2 = Gauge(C,n)*(i,wi) by A2,FINSEQ_2:10;
reconsider i2 as Nat;
A5: 1 <= i2 & i2 <= len Lower_Seq(C,n) by A3,FINSEQ_3:25;
3 <= len Upper_Seq(C,n) by JORDAN1E:15;
then
A6: 2 <= len Upper_Seq(C,n) by XXREAL_0:2;
set f = Rotate(Cage(C,n),E-max L~Cage(C,n));
set i1 = (S-max L~Cage(C,n))..Lower_Seq(C,n);
A7: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A8: f/.1 = E-max L~Cage(C,n) by FINSEQ_6:92;
L~Cage(C,n) = L~f by REVROT_1:33;
then
A9: (S-max L~Cage(C,n))..f < (S-min L~Cage(C,n))..f & (S-min L~Cage(C,n))..
f <= (W-min L~Cage(C,n))..f by A8,SPRECT_5:40,41;
A10: W-min L~Cage(C,n) in rng Cage(C,n) & rng f = rng Cage(C,n) by FINSEQ_6:90
,SPRECT_2:43,46;
(W-min L~Cage(C,n))..Lower_Seq(C,n) = len Lower_Seq(C,n) by Th30;
then (S-min L~Cage(C,n))..Lower_Seq(C,n) <= len Lower_Seq(C,n) by Th29;
then
A11: i1 < len Lower_Seq(C,n) by Th28,XXREAL_0:2;
(E-max L~Cage(C,n))..Lower_Seq(C,n) = 1 & (E-min L~Cage(C,n))..Lower_Seq
(C,n ) <= i1 by Th25,Th27;
then
A12: i1 > 1 by Th26,XXREAL_0:2;
then
A13: i1 in dom Lower_Seq(C,n) by A11,FINSEQ_3:25;
Lower_Seq(C,n) = f-:W-min L~Cage(C,n) & S-max L~Cage(C,n) in rng Cage(C
,n) by Th18,SPRECT_2:42;
then
A14: S-max L~Cage(C,n) in rng Lower_Seq(C,n) by A10,A9,FINSEQ_5:46,XXREAL_0:2;
then
A15: Lower_Seq(C,n)/.i1 = S-max L~Cage(C,n) by FINSEQ_5:38;
A16: i1 in NAT & i2 in NAT by ORDINAL1:def 12;
A17: i1 <> i2
proof
assume i1 = i2;
then Gauge(C,n)*(i,wi) = S-max L~Cage(C,n) by A4,A13,A15,PARTFUN1:def 6;
then (Gauge(C,n)*(i,wi))`2 = S-bound L~Cage(C,n) by EUCLID:52;
then N-bound L~Cage(C,n) = S-bound L~Cage(C,n) by A1,A7,JORDAN1A:70;
hence contradiction by SPRECT_1:16;
end;
then mid(Lower_Seq(C,n),i1,i2) is being_S-Seq by A12,A11,A5,JORDAN3:6,A16;
then reconsider
h = mid(Lower_Seq(C,n),i1,i2) as one-to-one special FinSequence
of TOP-REAL 2;
A18: (h/.1)`2 = (Lower_Seq(C,n)/.i1)`2 by A3,A13,SPRECT_2:8
.= (S-max L~Cage(C,n))`2 by A14,FINSEQ_5:38
.= S-bound L~Cage(C,n) by EUCLID:52;
len h >= 1 by A3,A13,SPRECT_2:5;
then len h > 1 by A3,A13,A17,SPRECT_2:6,XXREAL_0:1;
then
A19: 1+1 <= len h by NAT_1:13;
A20: h is_in_the_area_of Cage(C,n) by A3,A13,JORDAN1E:18,SPRECT_2:22;
(h/.len h)`2 = (Lower_Seq(C,n)/.i2)`2 by A3,A13,SPRECT_2:9
.= (Gauge(C,n)*(i,wi))`2 by A3,A4,PARTFUN1:def 6
.= N-bound L~Cage(C,n) by A1,A7,JORDAN1A:70;
then h is_a_v.c._for Cage(C,n) by A20,A18,SPRECT_2:def 3;
then L~Upper_Seq(C,n) meets L~h by A6,A19,Th40,SPRECT_2:29;
then consider x be object such that
A21: x in L~Upper_Seq(C,n) and
A22: x in L~h by XBOOLE_0:3;
L~mid(Lower_Seq(C,n),i1,i2) c= L~Lower_Seq(C,n) by A12,A11,A5,JORDAN4:35;
then x in L~Lower_Seq(C,n) /\ L~Upper_Seq(C,n) by A21,A22,XBOOLE_0:def 4;
then
A23: x in {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:16;
4 <= len Gauge(C,n) by JORDAN8:10;
then
A24: 1 <= len Gauge(C,n) by XXREAL_0:2;
per cases by A23,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 A12,A11,A5,A22,Th37;
then Lower_Seq(C,n)/.1 = Gauge(C,n)*(i,wi) by A3,A4,PARTFUN1:def 6;
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 EUCLID:52
.= Gauge(C,n)*(len Gauge(C,n),wi)`1 by A7,A24,JORDAN1A:71;
hence contradiction by A1,A7,A24,GOBOARD5:3;
end;
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 A12,A11,A5,A22,Th38;
then Lower_Seq(C,n)/.len Lower_Seq(C,n) = Gauge(C,n)*(i,wi) by A3,A4,
PARTFUN1:def 6;
then
A25: W-min(L~Cage(C,n)) = Gauge(C,n)*(i,wi) by JORDAN1F:8;
(NW-corner L~Cage(C,n))`2 >= (W-max L~Cage(C,n))`2 by PSCOMP_1:30;
then (NW-corner L~Cage(C,n))`2 > (W-min L~Cage(C,n))`2 by SPRECT_2:57
,XXREAL_0:2;
then N-bound L~Cage(C,n) > (Gauge(C,n)*(i,wi))`2 by A25,EUCLID:52;
hence contradiction by A1,A7,JORDAN1A:70;
end;
end;
theorem Th44:
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 and
A4: ii+1 <= len Upper_Seq(C,n) and
A5: Gi1 in LSeg(Upper_Seq(C,n),ii) by A2,SPPOL_2:13;
A6: LSeg(Upper_Seq(C,n),ii) = LSeg(Upper_Seq(C,n)/.ii,Upper_Seq(C,n)/.(ii+1)
) by A3,A4,TOPREAL1:def 3;
ii+1 >= 1 by NAT_1:11;
then
A7: ii+1 in dom Upper_Seq(C,n) by A4,FINSEQ_3:25;
len Gauge(C,n) >= 4 by JORDAN8:10;
then len Gauge(C,n) = width Gauge(C,n) & len Gauge(C,n) > 1 by JORDAN8:def 1
,XXREAL_0:2;
then
A8: [i,1] in Indices Gauge(C,n) by A1,MATRIX_0:30;
ii < len Upper_Seq(C,n) by A4,NAT_1:13;
then
A9: ii in dom Upper_Seq(C,n) by A3,FINSEQ_3:25;
A10: not Gi1 in rng Upper_Seq(C,n) by A1,Th42;
Upper_Seq(C,n) is_sequence_on Gauge(C,n) by Th4;
then consider i1,j1,i2,j2 being Nat such that
A11: [i1,j1] in Indices Gauge(C,n) and
A12: Upper_Seq(C,n)/.ii = Gauge(C,n)*(i1,j1) and
A13: [i2,j2] in Indices Gauge(C,n) and
A14: Upper_Seq(C,n)/.(ii+1) = Gauge(C,n)*(i2,j2) and
A15: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A3,A4,JORDAN8:3;
A16: 1 <= i1 by A11,MATRIX_0:32;
A17: j2 <= width Gauge(C,n) by A13,MATRIX_0:32;
A18: 1 <= j1 by A11,MATRIX_0:32;
A19: i1 <= len Gauge(C,n) by A11,MATRIX_0:32;
A20: 1 <= j2 by A13,MATRIX_0:32;
A21: i2 <= len Gauge(C,n) by A13,MATRIX_0:32;
A22: 1 <= i2 by A13,MATRIX_0:32;
A23: j1 <= width Gauge(C,n) by A11,MATRIX_0:32;
per cases by A15;
suppose
A24: i1 = i2 & j1+1 = j2;
then j1 <= j2 by NAT_1:11;
then Gauge(C,n)*(i1,j1)`2 <= Gauge(C,n)*(i2,j2)`2 by A16,A19,A18,A17,A24,
SPRECT_3:12;
then
A25: Gauge(C,n)*(i1,j1)`2 <= Gi1`2 by A5,A6,A12,A14,TOPREAL1:4;
Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A16,A19,A18,A23,A24,
GOBOARD5:2
.= Gauge(C,n)*(i2,j2)`1 by A22,A21,A20,A17,GOBOARD5:2;
then
LSeg(Upper_Seq(C,n)/.ii,Upper_Seq(C,n)/.(ii+1)) is vertical by A12,A14,
SPPOL_1:16;
then Gi1`1 = Gauge(C,n)*(i1,j1)`1 by A5,A6,A12,SPPOL_1:41;
then
A26: i1 = i by A11,A8,Th7;
then Gi1`2 <= Gauge(C,n)*(i1,j1)`2 by A16,A19,A18,A23,SPRECT_3:12;
then j1 = 1 by A11,A8,A25,Th6,XXREAL_0:1;
hence contradiction by A12,A9,A10,A26,PARTFUN2:2;
end;
suppose
A27: i1+1 = i2 & j1 = j2;
then Gauge(C,n)*(i1,j1)`2 = Gauge(C,n)*(1,j2)`2 by A16,A19,A18,A23,
GOBOARD5:1
.= Gauge(C,n)*(i2,j2)`2 by A22,A21,A20,A17,GOBOARD5:1;
then LSeg(Upper_Seq(C,n)/.ii,Upper_Seq(C,n)/.(ii+1)) is horizontal by A12
,A14,SPPOL_1:15;
then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A5,A6,A12,SPPOL_1:40;
then
A28: j1 = 1 by A11,A8,Th6;
i2 > 1 by A16,A27,NAT_1:13;
then not Upper_Seq(C,n)/.(ii+1) in rng Upper_Seq(C,n) by A14,A21,A27,A28
,Th42;
hence contradiction by A7,PARTFUN2:2;
end;
suppose
A29: i1 = i2+1 & j1 = j2;
then Gauge(C,n)*(i1,j1)`2 = Gauge(C,n)*(1,j2)`2 by A16,A19,A18,A23,
GOBOARD5:1
.= Gauge(C,n)*(i2,j2)`2 by A22,A21,A20,A17,GOBOARD5:1;
then LSeg(Upper_Seq(C,n)/.ii,Upper_Seq(C,n)/.(ii+1)) is horizontal by A12
,A14,SPPOL_1:15;
then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A5,A6,A12,SPPOL_1:40;
then
A30: j1 = 1 by A11,A8,Th6;
i1 > 1 by A22,A29,NAT_1:13;
then not Upper_Seq(C,n)/.ii in rng Upper_Seq(C,n) by A12,A19,A30,Th42;
hence contradiction by A9,PARTFUN2:2;
end;
suppose
A31: i1 = i2 & j1 = j2+1;
then j2 <= j1 by NAT_1:11;
then Gauge(C,n)*(i2,j2)`2 <= Gauge(C,n)*(i1,j1)`2 by A16,A19,A23,A20,A31,
SPRECT_3:12;
then
A32: Gauge(C,n)*(i2,j2)`2 <= Gi1`2 by A5,A6,A12,A14,TOPREAL1:4;
Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A16,A19,A18,A23,A31,
GOBOARD5:2
.= Gauge(C,n)*(i2,j2)`1 by A22,A21,A20,A17,GOBOARD5:2;
then
LSeg(Upper_Seq(C,n)/.ii,Upper_Seq(C,n)/.(ii+1)) is vertical by A12,A14,
SPPOL_1:16;
then Gi1`1 = Gauge(C,n)*(i1,j1)`1 by A5,A6,A12,SPPOL_1:41;
then
A33: i1 = i by A11,A8,Th7;
then Gi1`2 <= Gauge(C,n)*(i2,j2)`2 by A22,A21,A20,A17,A31,SPRECT_3:12;
then j2 = 1 by A13,A8,A32,Th6,XXREAL_0:1;
hence contradiction by A14,A7,A10,A31,A33,PARTFUN2:2;
end;
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 and
A4: ii+1 <= len Lower_Seq(C,n) and
A5: Gi1 in LSeg(Lower_Seq(C,n),ii) by A2,SPPOL_2:13;
A6: LSeg(Lower_Seq(C,n),ii) = LSeg(Lower_Seq(C,n)/.ii,Lower_Seq(C,n)/.(ii+1)
) by A3,A4,TOPREAL1:def 3;
ii+1 >= 1 by NAT_1:11;
then
A7: ii+1 in dom Lower_Seq(C,n) by A4,FINSEQ_3:25;
len Gauge(C,n) >= 4 by JORDAN8:10;
then len Gauge(C,n) = width Gauge(C,n) & len Gauge(C,n) > 1 by JORDAN8:def 1
,XXREAL_0:2;
then
A8: [i,wi] in Indices Gauge(C,n) by A1,MATRIX_0:30;
ii < len Lower_Seq(C,n) by A4,NAT_1:13;
then
A9: ii in dom Lower_Seq(C,n) by A3,FINSEQ_3:25;
A10: not Gi1 in rng Lower_Seq(C,n) by A1,Th43;
Lower_Seq(C,n) is_sequence_on Gauge(C,n) by Th5;
then consider i1,j1,i2,j2 being Nat such that
A11: [i1,j1] in Indices Gauge(C,n) and
A12: Lower_Seq(C,n)/.ii = Gauge(C,n)*(i1,j1) and
A13: [i2,j2] in Indices Gauge(C,n) and
A14: Lower_Seq(C,n)/.(ii+1) = Gauge(C,n)*(i2,j2) and
A15: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A3,A4,JORDAN8:3;
A16: 1 <= i1 by A11,MATRIX_0:32;
A17: j2 <= width Gauge(C,n) by A13,MATRIX_0:32;
A18: 1 <= j1 by A11,MATRIX_0:32;
A19: i1 <= len Gauge(C,n) by A11,MATRIX_0:32;
A20: 1 <= j2 by A13,MATRIX_0:32;
A21: i2 <= len Gauge(C,n) by A13,MATRIX_0:32;
A22: 1 <= i2 by A13,MATRIX_0:32;
A23: j1 <= width Gauge(C,n) by A11,MATRIX_0:32;
per cases by A15;
suppose
A24: i1 = i2 & j2+1 = j1;
then j1 >= j2 by NAT_1:11;
then Gauge(C,n)*(i1,j1)`2 >= Gauge(C,n)*(i2,j2)`2 by A16,A19,A23,A20,A24,
SPRECT_3:12;
then
A25: Gauge(C,n)*(i1,j1)`2 >= Gi1`2 by A5,A6,A12,A14,TOPREAL1:4;
Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A16,A19,A18,A23,A24,
GOBOARD5:2
.= Gauge(C,n)*(i2,j2)`1 by A22,A21,A20,A17,GOBOARD5:2;
then
LSeg(Lower_Seq(C,n)/.ii,Lower_Seq(C,n)/.(ii+1)) is vertical by A12,A14,
SPPOL_1:16;
then Gi1`1 = Gauge(C,n)*(i1,j1)`1 by A5,A6,A12,SPPOL_1:41;
then
A26: i1 = i by A11,A8,Th7;
then Gi1`2 >= Gauge(C,n)*(i1,j1)`2 by A16,A19,A18,A23,SPRECT_3:12;
then j1 = wi by A11,A8,A25,Th6,XXREAL_0:1;
hence contradiction by A12,A9,A10,A26,PARTFUN2:2;
end;
suppose
A27: i2+1 = i1 & j1 = j2;
then Gauge(C,n)*(i1,j1)`2 = Gauge(C,n)*(1,j2)`2 by A16,A19,A18,A23,
GOBOARD5:1
.= Gauge(C,n)*(i2,j2)`2 by A22,A21,A20,A17,GOBOARD5:1;
then LSeg(Lower_Seq(C,n)/.ii,Lower_Seq(C,n)/.(ii+1)) is horizontal by A12
,A14,SPPOL_1:15;
then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A5,A6,A12,SPPOL_1:40;
then
A28: j1 = wi by A11,A8,Th6;
i2 < len Gauge(C,n) by A19,A27,NAT_1:13;
then not Lower_Seq(C,n)/.(ii+1) in rng Lower_Seq(C,n) by A14,A22,A27,A28
,Th43;
hence contradiction by A7,PARTFUN2:2;
end;
suppose
A29: i2 = i1+1 & j1 = j2;
then Gauge(C,n)*(i1,j1)`2 = Gauge(C,n)*(1,j2)`2 by A16,A19,A18,A23,
GOBOARD5:1
.= Gauge(C,n)*(i2,j2)`2 by A22,A21,A20,A17,GOBOARD5:1;
then LSeg(Lower_Seq(C,n)/.ii,Lower_Seq(C,n)/.(ii+1)) is horizontal by A12
,A14,SPPOL_1:15;
then Gi1`2 = Gauge(C,n)*(i1,j1)`2 by A5,A6,A12,SPPOL_1:40;
then
A30: j1 = wi by A11,A8,Th6;
i1 < len Gauge(C,n) by A21,A29,NAT_1:13;
then not Lower_Seq(C,n)/.ii in rng Lower_Seq(C,n) by A12,A16,A30,Th43;
hence contradiction by A9,PARTFUN2:2;
end;
suppose
A31: i1 = i2 & j2 = j1+1;
then j2 >= j1 by NAT_1:11;
then Gauge(C,n)*(i2,j2)`2 >= Gauge(C,n)*(i1,j1)`2 by A16,A19,A18,A17,A31,
SPRECT_3:12;
then
A32: Gauge(C,n)*(i2,j2)`2 >= Gi1`2 by A5,A6,A12,A14,TOPREAL1:4;
Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A16,A19,A18,A23,A31,
GOBOARD5:2
.= Gauge(C,n)*(i2,j2)`1 by A22,A21,A20,A17,GOBOARD5:2;
then
LSeg(Lower_Seq(C,n)/.ii,Lower_Seq(C,n)/.(ii+1)) is vertical by A12,A14,
SPPOL_1:16;
then Gi1`1 = Gauge(C,n)*(i1,j1)`1 by A5,A6,A12,SPPOL_1:41;
then
A33: i1 = i by A11,A8,Th7;
then Gi1`2 >= Gauge(C,n)*(i2,j2)`2 by A22,A21,A20,A17,A31,SPRECT_3:12;
then j2 = wi by A13,A8,A32,Th6,XXREAL_0:1;
hence contradiction by A14,A7,A10,A31,A33,PARTFUN2:2;
end;
end;
theorem Th46:
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 and
A2: i <= len Gauge(C,n) and
A3: 1 <= j & j <= width Gauge(C,n) and
A4: Gij in L~Cage(C,n);
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;
set Wmi = W-min L~Cage(C,n);
set h = mid(Lower_Seq(C,n),2,len Lower_Seq(C,n));
set v1 = L_Cut(Upper_Seq(C,n),Gij);
set NE = NE-corner L~Cage(C,n);
set Gv1 = <*Gauge(C,n)*(i,1)*>^v1;
set v = Gv1^<*NE*>;
A6: L~Cage(C,n) = L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n) by JORDAN1E:13;
A7: Upper_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n))-: E-max L~Cage(C,n)
by JORDAN1E:def 1;
A8: len Upper_Seq(C,n) >= 3 by JORDAN1E:15;
then
A9: len Upper_Seq(C,n) >= 1 by XXREAL_0:2;
A10: len Lower_Seq(C,n) >= 3 by JORDAN1E:15;
then
A11: len Lower_Seq(C,n) >= 2 & len Lower_Seq(C,n) >= 1 by XXREAL_0:2;
A12: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
A13: Gauge(C,n)*(i,1)`2 = S-bound L~Cage(C,n) by A1,A2,JORDAN1A:72;
now
per cases by A1,A4,A6,XBOOLE_0:def 3,XXREAL_0:1;
suppose
A14: Gij in L~Upper_Seq(C,n) & i = 1;
set G11 = Gauge(C,n)*(1,1);
A15: Wmi in L~Cage(C,n) by SPRECT_1:13;
S-bound L~Cage(C,n) = G11`2 by A2,A14,JORDAN1A:72;
then
A16: Wmi`1 = W-bound L~Cage(C,n) & G11`2 <= Wmi`2 by A15,EUCLID:52,PSCOMP_1:24
;
A17: rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by A10,SPPOL_2:18,XXREAL_0:2;
A18: Gij`1 = W-bound L~Cage(C,n) by A3,A12,A14,JORDAN1A:73;
then Gij in W-most L~Cage(C,n) by A4,SPRECT_2:12;
then
A19: Wmi`2 <= Gij`2 by PSCOMP_1:31;
Lower_Seq(C,n)/.(len Lower_Seq(C,n)) = Wmi by JORDAN1F:8;
then
A20: Wmi in rng Lower_Seq(C,n) by FINSEQ_6:168;
G11`1 = W-bound L~Cage(C,n) by A2,A14,JORDAN1A:73;
then Wmi in LSeg(Gauge(C,n)*(1,1),Gauge(C,n)*(1,j)) by A14,A16,A18,A19,
GOBOARD7:7;
hence thesis by A14,A17,A20,XBOOLE_0:3;
end;
suppose
A21: 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;
len Cage(C,n) > 4 by GOBOARD7:34;
then
A22: rng Cage(C,n) c= L~Cage(C,n) by SPPOL_2:18,XXREAL_0:2;
A23: not NE in rng Cage(C,n)
proof
A24: NE`2 = N-bound L~Cage(C,n) by EUCLID:52;
then NE`1 = E-bound L~Cage(C,n) & NE`2 >= S-bound L~Cage(C,n) by
EUCLID:52,SPRECT_1:22;
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 A24;
then
A25: NE in LSeg(SE-corner L~Cage(C,n), NE-corner L~Cage(C,n)) by SPRECT_1:23
;
assume NE in rng Cage(C,n);
then NE in LSeg(SE-corner L~Cage(C,n), NE-corner L~Cage(C,n)) /\ L~
Cage(C,n) by A22,A25,XBOOLE_0:def 4;
then
A26: NE`2 <= (E-max L~Cage(C,n))`2 by PSCOMP_1:47;
A27: (E-max L~Cage(C,n))`1 = NE`1 by PSCOMP_1:45;
(E-max L~Cage(C,n))`2 <= NE`2 by PSCOMP_1:46;
then (E-max L~Cage(C,n))`2 = NE`2 by A26,XXREAL_0:1;
hence contradiction by A21,A27,TOPREAL3:6;
end;
A28: 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 3;
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:31;
then
A29: rng v1 = {Gij} \/ rng mid(Upper_Seq(C,n), Index(Gij,Upper_Seq(C
,n))+1,len Upper_Seq(C,n)) by FINSEQ_1:38;
not NE in L~Cage(C,n)
proof
assume NE in L~Cage(C,n);
then consider i be Nat such that
A30: 1 <= i and
A31: i+1 <= len Cage(C,n) and
A32: NE in LSeg(Cage(C,n)/.i,Cage(C,n)/.(i+1)) by SPPOL_2:14;
per cases by A30,A31,TOPREAL1:def 5;
suppose
A33: (Cage(C,n)/.i)`1 = (Cage(C,n)/.(i+1))`1;
(Cage(C,n)/.i)`2 <= (Cage(C,n)/.(i+1))`2 or (Cage(C,n)/.i)
`2 >= (Cage(C,n)/.(i+1))`2;
then
A34: NE`2 <= (Cage(C,n)/.(i+1))`2 or NE`2 <= (Cage(C,n)/.i)`2 by A32,
TOPREAL1:4;
A35: NE`1 = (Cage(C,n)/.i)`1 by A32,A33,GOBOARD7:5;
A36: 1 <= i+1 by NAT_1:11;
then
A37: i+1 in dom Cage(C,n) by A31,FINSEQ_3:25;
A38: NE`2 = N-bound L~Cage(C,n) by EUCLID:52;
then
A39: (Cage(C,n)/.(i+1))`2 <= NE`2 by A31,A36,JORDAN5D:11;
A40: i < len Cage(C,n) by A31,NAT_1:13;
then (Cage(C,n)/.i)`2 <= NE`2 by A30,A38,JORDAN5D:11;
then NE`2 = (Cage(C,n)/.(i+1))`2 or NE`2 = (Cage(C,n)/.i)`2 by
A39,A34,XXREAL_0:1;
then
A41: NE = (Cage(C,n)/.(i+1)) or NE = (Cage(C,n)/.i) by A33,A35,
TOPREAL3:6;
i in dom Cage(C,n) by A30,A40,FINSEQ_3:25;
hence contradiction by A23,A37,A41,PARTFUN2:2;
end;
suppose
A42: (Cage(C,n)/.i)`2 = (Cage(C,n)/.(i+1))`2;
(Cage(C,n)/.i)`1 <= (Cage(C,n)/.(i+1))`1 or (Cage(C,n)/.i)
`1 >= (Cage(C,n)/.(i+1))`1;
then
A43: NE`1 <= (Cage(C,n)/.(i+1))`1 or NE`1 <= (Cage(C,n)/.i)`1 by A32,
TOPREAL1:3;
A44: NE`2 = (Cage(C,n)/.i)`2 by A32,A42,GOBOARD7:6;
A45: 1 <= i+1 by NAT_1:11;
then
A46: i+1 in dom Cage(C,n) by A31,FINSEQ_3:25;
A47: NE`1 = E-bound L~Cage(C,n) by EUCLID:52;
then
A48: (Cage(C,n)/.(i+1))`1 <= NE`1 by A31,A45,JORDAN5D:12;
A49: i < len Cage(C,n) by A31,NAT_1:13;
then (Cage(C,n)/.i)`1 <= NE`1 by A30,A47,JORDAN5D:12;
then NE`1 = (Cage(C,n)/.(i+1))`1 or NE`1 = (Cage(C,n)/.i)`1 by
A48,A43,XXREAL_0:1;
then
A50: NE = (Cage(C,n)/.(i+1)) or NE = (Cage(C,n)/.i) by A42,A44,
TOPREAL3:6;
i in dom Cage(C,n) by A30,A49,FINSEQ_3:25;
hence contradiction by A23,A46,A50,PARTFUN2:2;
end;
end;
then
A51: not NE in {Gij} by A4,TARSKI:def 1;
rng mid(Upper_Seq(C,n),Index(Gij,Upper_Seq(C,n))+1, len
Upper_Seq(C,n)) c= rng Upper_Seq(C,n) & rng Upper_Seq(C,n) c= rng Cage(C,n) by
Th39,FINSEQ_6:119;
then rng mid(Upper_Seq(C,n),Index(Gij,Upper_Seq(C,n))+1, len
Upper_Seq(C,n)) c= rng Cage(C,n);
then not NE in rng mid(Upper_Seq(C,n),Index(Gij,Upper_Seq(C,n))+1,
len Upper_Seq(C,n)) by A23;
hence not NE in rng v1 by A29,A51,XBOOLE_0:def 3;
end;
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 3;
then
A52: rng v1 c= rng Upper_Seq(C,n) by FINSEQ_6:119;
rng Upper_Seq(C,n) c= rng Cage(C,n) by Th39;
then rng v1 c= rng Cage(C,n) by A52;
hence not NE in rng v1 by A23;
end;
end;
S-bound L~Cage(C,n) < N-bound L~Cage(C,n) by SPRECT_1:32;
then NE <> Gauge(C,n)*(i,1) by A13,EUCLID:52;
then not NE in {Gauge(C,n)*(i,1)} by TARSKI:def 1;
then not NE in rng <*Gauge(C,n)*(i,1)*> by FINSEQ_1:39;
then not NE in rng <*Gauge(C,n)*(i,1)*> \/ rng v1 by A28,XBOOLE_0:def 3;
then not NE in rng Gv1 by FINSEQ_1:31;
then rng Gv1 misses {NE} by ZFMISC_1:50;
then
A53: rng Gv1 misses rng <*NE*> by FINSEQ_1:38;
A54: len v = len Gv1 + 1 by FINSEQ_2:16
.= 1 + len v1 + 1 by FINSEQ_5:8;
A55: v1 is non empty by A21,JORDAN1E:3;
then
A56: 0+1 <= len v1 by NAT_1:13;
then 1 in dom v1 by FINSEQ_3:25;
then
A57: v1/.1 = v1.1 by PARTFUN1:def 6
.= Gij by A21,JORDAN3:23;
then
A58: (v1^<*NE*>)/.1 = Gij by A56,BOOLMARK:7;
1+len v1 >= 1+1 by A56,XREAL_1:7;
then
A59: 2 < len v by A54,NAT_1:13;
A60: v1 is being_S-Seq by A21,JORDAN3:34;
v = <*Gauge(C,n)*(i,1)*>^(v1^<*NE*>) by FINSEQ_1:32;
then v/.1 = Gauge(C,n)*(i,1) by FINSEQ_5:15;
then
A61: (v/.1)`2 = S-bound L~Cage(C,n) by A1,A2,JORDAN1A:72;
len v = len Gv1 + 1 by FINSEQ_2:16;
then v/.(len v) = NE by FINSEQ_4:67;
then
A62: (v/.len v)`2 = N-bound L~Cage(C,n) by EUCLID:52;
A63: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:32;
then (N-max L~Cage(C,n))..Cage(C,n) <= (E-max L~Cage(C,n))..Cage(C,n)
by SPRECT_2:70;
then
A64: (E-max L~Cage(C,n))..Cage(C,n) > 1 by A63,SPRECT_2:69,XXREAL_0:2;
(E-min L~Cage(C,n))..Cage(C,n) <= (S-max L~Cage(C,n))..Cage(C,n)
by A63,SPRECT_2:72;
then (E-max L~Cage(C,n))..Cage(C,n) < (S-max L~Cage(C,n))..Cage(C,n) by
A63,SPRECT_2:71,XXREAL_0:2;
then (E-max L~Cage(C,n))..Cage(C,n) < (S-min L~Cage(C,n))..Cage(C,n) by
A63,SPRECT_2:73,XXREAL_0:2;
then
A65: (E-max L~Cage(C,n))..Cage(C,n) < (W-min L~Cage(C,n))..Cage(C,n )
by A63,SPRECT_2:74,XXREAL_0:2;
then (E-max L~Cage(C,n))..Cage(C,n) < len Cage(C,n) by A63,SPRECT_2:76
,XXREAL_0:2;
then
A66: (E-max L~Cage(C,n))..Cage(C,n)+1 <= len Cage(C,n) by NAT_1:13;
A67: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)) = E-max L~Cage(C,n) by
FINSEQ_5:38;
then
A68: (Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)+1))`1 = E-bound L~Cage
(C,n) by A64,A66,JORDAN1E:20;
A69: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
then
A70: (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 A67
,A65,SPRECT_5:9;
now
let m be Nat;
assume
A71: m in dom <*Gauge(C,n)*(i,1)*>;
then m in Seg 1 by FINSEQ_1:38;
then m = 1 by FINSEQ_1:2,TARSKI:def 1;
then <*Gauge(C,n)*(i,1)*>.m = Gauge(C,n)*(i,1);
then
A72: <*Gauge(C,n)*(i,1)*>/.m = Gauge(C,n)*(i,1) by A71,PARTFUN1:def 6;
width Gauge(C,n) >= 4 by A12,JORDAN8:10;
then
A73: 1 <= width Gauge(C,n) by XXREAL_0:2;
then Gauge(C,n)*(1,1)`1 <= Gauge(C,n)*(i,1)`1 by A1,A2,SPRECT_3:13;
hence W-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,1)*>/.m)`1 by A12,A72,A73
,JORDAN1A:73;
(Gauge(C,n)*(i,1))`1 <= Gauge(C,n)*(len Gauge(C,n),1)`1 by A1,A2,A73,
SPRECT_3:13;
hence (<*Gauge(C,n)*(i,1)*>/.m)`1 <= E-bound L~Cage(C,n) by A12,A72,A73
,JORDAN1A:71;
thus S-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,1)*>/.m)`2 by A1,A2,A72,
JORDAN1A:72;
S-bound L~Cage(C,n) = Gauge(C,n)*(i,1)`2 by A1,A2,JORDAN1A:72;
hence (<*Gauge(C,n)*(i,1)*>/.m)`2 <= N-bound L~Cage(C,n) by A72,
SPRECT_1:22;
end;
then
A74: <*Gauge(C,n)*(i,1)*> is_in_the_area_of Cage(C,n) by SPRECT_2:def 1;
A75: <*NE*> is_in_the_area_of Cage(C,n) by SPRECT_2:25;
3 <= len Lower_Seq(C,n) by JORDAN1E:15;
then 2 <= len Lower_Seq(C,n) by XXREAL_0:2;
then
A76: 2 in dom Lower_Seq(C,n) by FINSEQ_3:25;
<*Gij*> is_in_the_area_of Cage(C,n) by A21,JORDAN1E:17,SPRECT_3:46;
then v1 is_in_the_area_of Cage(C,n) by A21,JORDAN1E:17,SPRECT_3:56;
then Gv1 is_in_the_area_of Cage(C,n) by A74,SPRECT_2:24;
then v is_in_the_area_of Cage(C,n) by A75,SPRECT_2:24;
then
A77: v is_a_v.c._for Cage(C,n) by A61,A62,SPRECT_2:def 3;
A78: 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+(E-max L~Cage(
C,n))..Cage(C,n);
A79: len Lower_Seq(C,n) in dom Lower_Seq(C,n) by FINSEQ_5:6;
then h is_in_the_area_of Cage(C,n) by A76,JORDAN1E:18,SPRECT_2:22;
then
A80: Rev h is_in_the_area_of Cage(C,n) by SPRECT_3:51;
1+(E-max L~Cage(C,n))..Cage(C,n)<=0+(W-min L~Cage(C,n))..Cage(C,n)
by A65,NAT_1:13;
then 1+(E-max L~Cage(C,n))..Cage(C,n)-(W-min L~Cage(C,n))..Cage(C,n)<=0
by XREAL_1:20;
then
A81: 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 XREAL_1:6;
A82: len Lower_Seq(C,n) >= 2+1 by JORDAN1E:15;
then
A83: len Lower_Seq(C,n) > 2 by NAT_1:13;
len Cage(C,n)+0 <= len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n) by
XREAL_1:6;
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 A70,XREAL_1:9;
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 XREAL_1:6;
then
A84: 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 A69,FINSEQ_5:50;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A85: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by
FINSEQ_6:90,SPRECT_2:43;
A86: L~v1 c= L~Upper_Seq(C,n) by A21,JORDAN3:42;
A87: len Lower_Seq(C,n) > 1 by A82,XXREAL_0:2;
then
A88: h is non empty by A83,JORDAN1B:2;
A89: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by A67,
FINSEQ_6:90,SPRECT_2:43;
then 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,A76,
FINSEQ_5:52
.= 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 A69,A70,A84,A81,
FINSEQ_6:182
.= Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)+1) by A70,A78,
XREAL_0:def 2;
then (h/.1)`1 = E-bound L~Cage(C,n) by A76,A79,A68,SPRECT_2:8;
then (Rev h/.len h)`1 = E-bound L~Cage(C,n) by A88,FINSEQ_5:65;
then
A90: (Rev h/.len Rev h)`1 = E-bound L~Cage(C,n) by FINSEQ_5:def 3;
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,A89,FINSEQ_5:54
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by FINSEQ_6:def 1
.= W-min L~Cage(C,n) by A69,FINSEQ_6:92;
then (Lower_Seq(C,n)/.len Lower_Seq(C,n))`1 = W-bound L~Cage(C,n) by
EUCLID:52;
then (h/.len h)`1 = W-bound L~Cage(C,n) by A76,A79,SPRECT_2:9;
then (Rev h/.1)`1 = W-bound L~Cage(C,n) by A88,FINSEQ_5:65;
then
A91: Rev h is_a_h.c._for Cage(C,n) by A80,A90,SPRECT_2:def 2;
A92: len Upper_Seq(C,n) in dom Upper_Seq(C,n) by A9,FINSEQ_3:25;
set ci = mid(Upper_Seq(C,n),Index(Gij,Upper_Seq(C,n))+1, len Upper_Seq(C
,n));
rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by A8,SPPOL_2:18,XXREAL_0:2;
then
A93: not Gauge(C,n)*(i,1) in rng Upper_Seq(C,n) by A2,A21,Th44;
not Gauge(C,n)*(i,1) in L~Upper_Seq(C,n) by A2,A21,Th44;
then not Gauge(C,n)*(i,1) in {Gij} by A21,TARSKI:def 1;
then
A94: not Gauge(C,n)*(i,1) in rng <*Gij*> by FINSEQ_1:38;
now
per cases;
suppose
A95: Gij <> Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1);
rng ci c= rng Upper_Seq(C,n) by FINSEQ_6:119;
then not Gauge(C,n)*(i,1) in rng ci by A93;
then not Gauge(C,n)*(i,1) in rng <*Gij*> \/ rng ci by A94,
XBOOLE_0:def 3;
then not Gauge(C,n)*(i,1) in rng(<*Gij*>^ci) by FINSEQ_1:31;
hence not Gauge(C,n)*(i,1) in rng v1 by A95,JORDAN3:def 3;
end;
suppose
Gij = Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1);
then v1 = ci by JORDAN3:def 3;
then rng v1 c= rng Upper_Seq(C,n) by FINSEQ_6:119;
hence not Gauge(C,n)*(i,1) in rng v1 by A93;
end;
end;
then {Gauge(C,n)*(i,1)} misses rng v1 by ZFMISC_1:50;
then
A96: rng <*Gauge(C,n)*(i,1)*> misses rng v1 by FINSEQ_1:38;
A97: <*NE*> is one-to-one by FINSEQ_3:93;
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:53;
then
A98: not E-max L~Cage(C,n) in L~h by A83,JORDAN5B:16;
<*Gauge(C,n)*(i,1)*> is one-to-one by FINSEQ_3:93;
then Gv1 is one-to-one by A96,A60,FINSEQ_3:91;
then
A99: v is one-to-one by A53,A97,FINSEQ_3:91;
A100: L~h c= L~Lower_Seq(C,n) by A11,JORDAN4:35;
(<*Gauge(C,n)*(i,1)*>/.len <*Gauge(C,n)*(i,1)*>)`1 = (<*Gauge(C,n)
*(i,1)*>/.1)`1 by FINSEQ_1:39
.= Gauge(C,n)*(i,1)`1 by FINSEQ_4:16
.= (v1/.1)`1 by A1,A2,A3,A57,GOBOARD5:2;
then
A101: Gv1 is special by A60,GOBOARD2:8;
len v1 in dom v1 by A56,FINSEQ_3:25;
then
A102: v1/.(len v1) = v1.(len v1) by PARTFUN1:def 6
.= Upper_Seq(C,n).len Upper_Seq(C,n) by A21,JORDAN1B:4
.= Upper_Seq(C,n)/.len Upper_Seq(C,n) by A92,PARTFUN1:def 6
.= (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 A7,A85,FINSEQ_5:42
.= E-max L~Cage(C,n) by A85,FINSEQ_5:45;
then Gv1/.len Gv1 = E-max L~Cage(C,n) by A55,SPRECT_3:1;
then (Gv1/.len Gv1)`1 = NE`1 by PSCOMP_1:45
.= (<*NE*>/.1)`1 by FINSEQ_4:16;
then
A103: v is special by A101,GOBOARD2:8;
h is S-Sequence_in_R2 by A83,A87,JORDAN3:6;
then
A104: Rev h is S-Sequence_in_R2;
then 2 <= len Rev h by TOPREAL1:def 8;
then L~Rev h meets L~v by A59,A99,A103,A104,A91,A77,SPRECT_2:29;
then L~h meets L~v by SPPOL_2:22;
then consider x be object such that
A105: x in L~h and
A106: x in L~v by XBOOLE_0:3;
A107: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
L~v = L~(<*Gauge(C,n)*(i,1)*>^(v1^<*NE*>)) by FINSEQ_1:32
.= 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 A55,SPPOL_2:19;
then
A108: x in LSeg(Gauge(C,n)*(i,1),(v1^<*NE*>)/.1) or x in L~v1 \/ LSeg(v1
/.(len v1),NE) by A106,XBOOLE_0:def 3;
now
per cases by A108,XBOOLE_0:def 3;
suppose
x in LSeg(Gauge(C,n)*(i,1),(v1^<*NE*>)/.1);
then x in L~<*Gauge(C,n)*(i,1),Gij*> by A58,SPPOL_2:21;
hence
L~Lower_Seq(C,n) meets L~<*Gauge(C,n)*(i,1),Gij*> by A105,A100,
XBOOLE_0:3;
end;
suppose
A109: x in L~v1;
then x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) by A105,A100,A86,
XBOOLE_0:def 4;
then x in {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:16;
then
A110: x = W-min L~Cage(C,n) by A105,A98,TARSKI:def 2;
1 in dom Upper_Seq(C,n) by A9,FINSEQ_3:25;
then Upper_Seq(C,n).1 = Upper_Seq(C,n)/.1 by PARTFUN1:def 6
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by A7,A85,FINSEQ_5:44
.= W-min L~Cage(C,n) by A107,FINSEQ_6:92;
then x = Gij by A21,A109,A110,JORDAN1E:7;
then x in LSeg(Gauge(C,n)*(i,1),Gij) by RLTOPSP1:68;
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 A105,A100,
XBOOLE_0:3;
end;
suppose
A111: x in LSeg(v1/.(len v1),NE);
x in L~Cage(C,n) by A6,A105,A100,XBOOLE_0:def 3;
then x in LSeg(E-max L~Cage(C,n), NE) /\ L~Cage(C,n) by A102,A111,
XBOOLE_0:def 4;
then x in {E-max L~Cage(C,n)} by PSCOMP_1:51;
hence
L~Lower_Seq(C,n) meets L~<*Gauge(C,n)*(i,1),Gij*> by A105,A98,
TARSKI:def 1;
end;
end;
then L~<*Gauge(C,n)*(i,1),Gij*> meets L~Lower_Seq(C,n);
hence thesis by SPPOL_2:21;
end;
suppose
A112: 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;
now
let m be Nat;
assume
A113: m in dom <*Gauge(C,n)*(i,1)*>;
then m in Seg 1 by FINSEQ_1:38;
then m = 1 by FINSEQ_1:2,TARSKI:def 1;
then <*Gauge(C,n)*(i,1)*>.m = Gauge(C,n)*(i,1);
then
A114: <*Gauge(C,n)*(i,1)*>/.m = Gauge(C,n)*(i,1) by A113,PARTFUN1:def 6;
width Gauge(C,n) >= 4 by A12,JORDAN8:10;
then
A115: 1 <= width Gauge(C,n) by XXREAL_0:2;
then Gauge(C,n)*(1,1)`1 <= Gauge(C,n)*(i,1)`1 by A1,A2,SPRECT_3:13;
hence W-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,1)*>/.m)`1 by A12,A114
,A115,JORDAN1A:73;
(Gauge(C,n)*(i,1))`1 <= Gauge(C,n)*(len Gauge(C,n),1)`1 by A1,A2,A115,
SPRECT_3:13;
hence (<*Gauge(C,n)*(i,1)*>/.m)`1 <= E-bound L~Cage(C,n) by A12,A114
,A115,JORDAN1A:71;
thus S-bound L~Cage(C,n) <= (<*Gauge(C,n)*(i,1)*>/.m)`2 by A1,A2,A114,
JORDAN1A:72;
S-bound L~Cage(C,n) = Gauge(C,n)*(i,1)`2 by A1,A2,JORDAN1A:72;
hence (<*Gauge(C,n)*(i,1)*>/.m)`2 <= N-bound L~Cage(C,n) by A114,
SPRECT_1:22;
end;
then
A116: <*Gauge(C,n)*(i,1)*> is_in_the_area_of Cage(C,n) by SPRECT_2:def 1;
<*Gij*> is_in_the_area_of Cage(C,n) by A112,JORDAN1E:17,SPRECT_3:46;
then v1 is_in_the_area_of Cage(C,n) by A112,JORDAN1E:17,SPRECT_3:56;
then
A117: Gv1 is_in_the_area_of Cage(C,n) by A116,SPRECT_2:24;
A118: len Upper_Seq(C,n) in dom Upper_Seq(C,n) by A9,FINSEQ_3:25;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A119: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by
FINSEQ_6:90,SPRECT_2:43;
A120: v1 is non empty by A112,JORDAN1E:3;
then
A121: 0+1 <= len v1 by NAT_1:13;
then 1 in dom v1 by FINSEQ_3:25;
then
A122: v1/.1 = v1.1 by PARTFUN1:def 6
.= Gij by A112,JORDAN3:23;
len v1 in dom v1 by A121,FINSEQ_3:25;
then v1/.(len v1) = v1.(len v1) by PARTFUN1:def 6
.= Upper_Seq(C,n).len Upper_Seq(C,n) by A112,JORDAN1B:4
.= Upper_Seq(C,n)/.len Upper_Seq(C,n) by A118,PARTFUN1:def 6
.= (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 A7,A119,FINSEQ_5:42
.= E-max L~Cage(C,n) by A119,FINSEQ_5:45;
then Gv1/.len Gv1 = E-max L~Cage(C,n) by A120,SPRECT_3:1;
then
A123: (Gv1/.len Gv1)`2 = N-bound L~Cage(C,n) by A112,EUCLID:52;
Gv1/.1 = Gauge(C,n)*(i,1) by FINSEQ_5:15;
then (Gv1/.1)`2 = S-bound L~Cage(C,n) by A1,A2,JORDAN1A:72;
then
A124: Gv1 is_a_v.c._for Cage(C,n) by A117,A123,SPRECT_2:def 3;
A125: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:32;
then (N-max L~Cage(C,n))..Cage(C,n) <= (E-max L~Cage(C,n))..Cage(C,n)
by SPRECT_2:70;
then
A126: (E-max L~Cage(C,n))..Cage(C,n) > 1 by A125,SPRECT_2:69,XXREAL_0:2;
(E-min L~Cage(C,n))..Cage(C,n) <= (S-max L~Cage(C,n))..Cage(C,n)
by A125,SPRECT_2:72;
then (E-max L~Cage(C,n))..Cage(C,n) < (S-max L~Cage(C,n))..Cage(C,n) by
A125,SPRECT_2:71,XXREAL_0:2;
then (E-max L~Cage(C,n))..Cage(C,n) < (S-min L~Cage(C,n))..Cage(C,n) by
A125,SPRECT_2:73,XXREAL_0:2;
then
A127: (E-max L~Cage(C,n))..Cage(C,n) < (W-min L~Cage(C,n))..Cage(C,n )
by A125,SPRECT_2:74,XXREAL_0:2;
then (E-max L~Cage(C,n))..Cage(C,n) < len Cage(C,n) by A125,SPRECT_2:76
,XXREAL_0:2;
then
A128: (E-max L~Cage(C,n))..Cage(C,n)+1 <= len Cage(C,n) by NAT_1:13;
A129: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)) = E-max L~Cage(C,n) by
FINSEQ_5:38;
then
A130: (Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)+1))`1 = E-bound L~Cage
(C,n) by A126,A128,JORDAN1E:20;
1+(E-max L~Cage(C,n))..Cage(C,n)<=0+(W-min L~Cage(C,n))..Cage(C,n)
by A127,NAT_1:13;
then 1+(E-max L~Cage(C,n))..Cage(C,n)-(W-min L~Cage(C,n))..Cage(C,n)<=0
by XREAL_1:20;
then
A131: 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 XREAL_1:6;
A132: len Lower_Seq(C,n) >= 2+1 by JORDAN1E:15;
then
A133: len Lower_Seq(C,n) > 2 by NAT_1:13;
set ci = mid(Upper_Seq(C,n),Index(Gij,Upper_Seq(C,n))+1, len Upper_Seq(C
,n));
rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by A8,SPPOL_2:18,XXREAL_0:2;
then
A134: not Gauge(C,n)*(i,1) in rng Upper_Seq(C,n) by A2,A112,Th44;
not Gauge(C,n)*(i,1) in L~Upper_Seq(C,n) by A2,A112,Th44;
then not Gauge(C,n)*(i,1) in {Gij} by A112,TARSKI:def 1;
then
A135: not Gauge(C,n)*(i,1) in rng <*Gij*> by FINSEQ_1:38;
now
per cases;
suppose
A136: Gij <> Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1);
rng ci c= rng Upper_Seq(C,n) by FINSEQ_6:119;
then not Gauge(C,n)*(i,1) in rng ci by A134;
then not Gauge(C,n)*(i,1) in rng <*Gij*> \/ rng ci by A135,
XBOOLE_0:def 3;
then not Gauge(C,n)*(i,1) in rng(<*Gij*>^ci) by FINSEQ_1:31;
hence not Gauge(C,n)*(i,1) in rng v1 by A136,JORDAN3:def 3;
end;
suppose
Gij = Upper_Seq(C,n).(Index(Gij,Upper_Seq(C,n))+1);
then v1 = ci by JORDAN3:def 3;
then rng v1 c= rng Upper_Seq(C,n) by FINSEQ_6:119;
hence not Gauge(C,n)*(i,1) in rng v1 by A134;
end;
end;
then {Gauge(C,n)*(i,1)} misses rng v1 by ZFMISC_1:50;
then
A137: rng <*Gauge(C,n)*(i,1)*> misses rng v1 by FINSEQ_1:38;
A138: 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+(E-max L~Cage(
C,n))..Cage(C,n);
1+len v1 >= 1+1 by A121,XREAL_1:7;
then
A139: len Gv1 >= 2 by FINSEQ_5:8;
3 <= len Lower_Seq(C,n) by JORDAN1E:15;
then 2 <= len Lower_Seq(C,n) by XXREAL_0:2;
then
A140: 2 in dom Lower_Seq(C,n) by FINSEQ_3:25;
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:53;
then
A141: not E-max L~Cage(C,n) in L~h by A133,JORDAN5B:16;
A142: v1 is being_S-Seq by A112,JORDAN3:34;
(<*Gauge(C,n)*(i,1)*>/.len <*Gauge(C,n)*(i,1)*>)`1 = (<*Gauge(C,n)
*(i,1)*>/.1)`1 by FINSEQ_1:39
.= Gauge(C,n)*(i,1)`1 by FINSEQ_4:16
.= (v1/.1)`1 by A1,A2,A3,A122,GOBOARD5:2;
then
A143: Gv1 is special by A142,GOBOARD2:8;
A144: L~Gv1 = LSeg(Gauge(C,n)*(i,1),v1/.1) \/ L~v1 by A120,SPPOL_2:20;
A145: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
then
A146: (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
A129,A127,SPRECT_5:9;
len Cage(C,n)+0 <= len Cage(C,n)+(E-max L~Cage(C,n))..Cage(C,n) by
XREAL_1:6;
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 A146,XREAL_1:9;
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 XREAL_1:6;
then
A147: 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 A145,FINSEQ_5:50;
A148: len Lower_Seq(C,n) > 1 by A132,XXREAL_0:2;
then
A149: h is non empty by A133,JORDAN1B:2;
A150: len Lower_Seq(C,n) in dom Lower_Seq(C,n) by FINSEQ_5:6;
then h is_in_the_area_of Cage(C,n) by A140,JORDAN1E:18,SPRECT_2:22;
then
A151: Rev h is_in_the_area_of Cage(C,n) by SPRECT_3:51;
A152: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by A129,
FINSEQ_6:90,SPRECT_2:43;
then 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,A140,
FINSEQ_5:52
.= 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 A145,A146,A147,A131,
FINSEQ_6:182
.= Cage(C,n)/.((E-max L~Cage(C,n))..Cage(C,n)+1) by A146,A138,
XREAL_0:def 2;
then (h/.1)`1 = E-bound L~Cage(C,n) by A140,A150,A130,SPRECT_2:8;
then (Rev h/.len h)`1 = E-bound L~Cage(C,n) by A149,FINSEQ_5:65;
then
A153: (Rev h/.len Rev h)`1 = E-bound L~Cage(C,n) by FINSEQ_5:def 3;
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,A152,FINSEQ_5:54
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by FINSEQ_6:def 1
.= W-min L~Cage(C,n) by A145,FINSEQ_6:92;
then (Lower_Seq(C,n)/.len Lower_Seq(C,n))`1 = W-bound L~Cage(C,n) by
EUCLID:52;
then (h/.len h)`1 = W-bound L~Cage(C,n) by A140,A150,SPRECT_2:9;
then (Rev h/.1)`1 = W-bound L~Cage(C,n) by A149,FINSEQ_5:65;
then
A154: Rev h is_a_h.c._for Cage(C,n) by A151,A153,SPRECT_2:def 2;
<*Gauge(C,n)*(i,1)*> is one-to-one by FINSEQ_3:93;
then
A155: Gv1 is one-to-one by A137,A142,FINSEQ_3:91;
A156: L~h c= L~Lower_Seq(C,n) by A11,JORDAN4:35;
h is S-Sequence_in_R2 by A133,A148,JORDAN3:6;
then
A157: Rev h is S-Sequence_in_R2;
then 2 <= len Rev h by TOPREAL1:def 8;
then L~Rev h meets L~Gv1 by A139,A155,A143,A157,A154,A124,SPRECT_2:29;
then L~h meets L~Gv1 by SPPOL_2:22;
then consider x be object such that
A158: x in L~h and
A159: x in L~Gv1 by XBOOLE_0:3;
A160: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
A161: L~v1 c= L~Upper_Seq(C,n) by A112,JORDAN3:42;
now
per cases by A159,A144,XBOOLE_0:def 3;
suppose
x in LSeg(Gauge(C,n)*(i,1),v1/.1);
then x in L~<*Gauge(C,n)*(i,1),Gij*> by A122,SPPOL_2:21;
hence
L~Lower_Seq(C,n) meets L~<*Gauge(C,n)*(i,1),Gij*> by A158,A156,
XBOOLE_0:3;
end;
suppose
A162: x in L~v1;
then x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) by A158,A156,A161,
XBOOLE_0:def 4;
then x in {W-min L~Cage(C,n),E-max L~Cage(C,n)} by JORDAN1E:16;
then
A163: x = W-min L~Cage(C,n) by A158,A141,TARSKI:def 2;
1 in dom Upper_Seq(C,n) by A9,FINSEQ_3:25;
then Upper_Seq(C,n).1 = Upper_Seq(C,n)/.1 by PARTFUN1:def 6
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by A7,A119,FINSEQ_5:44
.= W-min L~Cage(C,n) by A160,FINSEQ_6:92;
then x = Gij by A112,A162,A163,JORDAN1E:7;
then x in LSeg(Gauge(C,n)*(i,1),Gij) by RLTOPSP1:68;
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 A158,A156,
XBOOLE_0:3;
end;
end;
then L~<*Gauge(C,n)*(i,1),Gij*> meets L~Lower_Seq(C,n);
hence thesis by SPPOL_2:21;
end;
suppose
A164: Gij in L~Lower_Seq(C,n);
Gij in LSeg(Gauge(C,n)*(i,1),Gij) by RLTOPSP1:68;
hence thesis by A164,XBOOLE_0:3;
end;
suppose
A165: Gij in L~Upper_Seq(C,n) & Gij = Upper_Seq(C,n).len Upper_Seq(C ,n);
A166: Gij in LSeg(Gauge(C,n)*(i,1),Gij) by RLTOPSP1:68;
A167: rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) & E-max L~Cage(C,n) in rng
Lower_Seq( C,n) by A5,A10,FINSEQ_6:61,SPPOL_2:18,XXREAL_0:2;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A168: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by
FINSEQ_6:90,SPRECT_2:43;
len Upper_Seq(C,n) in dom Upper_Seq(C,n) by A9,FINSEQ_3:25;
then Upper_Seq(C,n).len Upper_Seq(C,n) = Upper_Seq(C,n)/.len Upper_Seq(
C,n) by PARTFUN1:def 6
.= (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 A7,A168,FINSEQ_5:42
.= E-max L~Cage(C,n) by A168,FINSEQ_5:45;
hence thesis by A165,A167,A166,XBOOLE_0:3;
end;
end;
hence thesis;
end;
theorem Th47:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for n be Nat st n > 0 holds First_Point(L~Upper_Seq(C,n),
W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line ((W-bound L~Cage(C,n)+
E-bound L~Cage(C,n))/2)) in rng Upper_Seq(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
assume
A1: n > 0;
set sr = (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2;
set Ebo = E-bound L~Cage(C,n);
set Wbo = W-bound L~Cage(C,n);
set Emax = E-max L~Cage(C,n);
set Wmin = W-min L~Cage(C,n);
set FiP = First_Point(L~Upper_Seq(C,n),Wmin,Emax,Vertical_Line sr);
A2: 1 <= Center Gauge(C,n) by JORDAN1B:11;
A3: Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) & Upper_Seq(C,n)/.len Upper_Seq(C,
n) = E-max L~Cage(C,n) by JORDAN1F:5,7;
then
A4: L~Upper_Seq(C,n) is_an_arc_of Wmin,Emax by TOPREAL1:25;
A5: Wbo < Ebo by SPRECT_1:31;
then Wbo < sr by XREAL_1:226;
then
A6: Wmin`1 <= sr by EUCLID:52;
A7: Center Gauge(C,n) <= len Gauge(C,n) by JORDAN1B:13;
sr < Ebo by A5,XREAL_1:226;
then
A8: sr <= Emax`1 by EUCLID:52;
then
A9: L~Upper_Seq(C,n) meets Vertical_Line(sr) by A4,A6,JORDAN6:49;
L~Upper_Seq(C,n) /\ Vertical_Line(sr) is closed by A4,A6,A8,JORDAN6:49;
then
A10: FiP in L~Upper_Seq(C,n) /\ Vertical_Line sr by A4,A9,JORDAN5C:def 1;
then FiP in L~Upper_Seq(C,n) by XBOOLE_0:def 4;
then consider t be Nat such that
A11: 1 <= t and
A12: t+1 <= len Upper_Seq(C,n) and
A13: FiP in LSeg(Upper_Seq(C,n),t) by SPPOL_2:13;
A14: LSeg(Upper_Seq(C,n),t) = LSeg(Upper_Seq(C,n)/.t,Upper_Seq(C,n)/.(t+1))
by A11,A12,TOPREAL1:def 3;
t < len Upper_Seq(C,n) by A12,NAT_1:13;
then
A15: t in dom Upper_Seq(C,n) by A11,FINSEQ_3:25;
1 <= t+1 by A11,NAT_1:13;
then
A16: t+1 in dom Upper_Seq(C,n) by A12,FINSEQ_3:25;
FiP in Vertical_Line sr by A10,XBOOLE_0:def 4;
then
A17: FiP`1 = sr by JORDAN6:31;
A18: FiP = First_Point (LSeg (Upper_Seq(C,n),t),Upper_Seq(C,n)/.t, Upper_Seq
(C,n)/.(t+1),Vertical_Line sr) by A3,A9,A11,A12,A13,JORDAN5C:19,JORDAN6:30;
now
per cases by SPPOL_1:19;
suppose
A19: LSeg(Upper_Seq(C,n),t) is vertical;
then (Upper_Seq(C,n)/.(t+1))`1 = sr by A13,A14,A17,SPPOL_1:41;
then Upper_Seq(C,n)/.(t+1) in {p where p is Point of TOP-REAL 2: p`1 =
sr};
then
A20: Upper_Seq(C,n)/.(t+1) in Vertical_Line sr by JORDAN6:def 6;
A21: LSeg(Upper_Seq(C,n),t) is closed & LSeg(Upper_Seq(C,n),t)
is_an_arc_of Upper_Seq(C,n)/.t, Upper_Seq(C,n)/.(t+1) by A14,A15,A16,
GOBOARD7:29,TOPREAL1:9;
(Upper_Seq(C,n)/.t)`1 = sr by A13,A14,A17,A19,SPPOL_1:41;
then Upper_Seq(C,n)/.t in {p where p is Point of TOP-REAL 2: p`1 = sr};
then Upper_Seq(C,n)/.t in Vertical_Line sr by JORDAN6:def 6;
then LSeg(Upper_Seq(C,n),t) c= Vertical_Line sr by A14,A20,JORDAN1A:13;
then
First_Point (LSeg(Upper_Seq(C,n),t),Upper_Seq(C,n)/.t, Upper_Seq(C,
n)/.(t+1),Vertical_Line sr) = Upper_Seq(C,n)/.t by A21,JORDAN5C:7;
hence thesis by A18,A15,PARTFUN2:2;
end;
suppose
LSeg(Upper_Seq(C,n),t) is horizontal;
then
A22: (Upper_Seq(C,n)/.t)`2 = (Upper_Seq(C,n)/.(t+1))`2 by A14,SPPOL_1:15;
then
A23: FiP`2 = (Upper_Seq(C,n)/.t)`2 by A13,A14,GOBOARD7:6;
Upper_Seq(C,n) is_sequence_on Gauge(C,n) by Th4;
then consider i1,j1,i2,j2 be Nat such that
A24: [i1,j1] in Indices Gauge(C,n) and
A25: Upper_Seq(C,n)/.t = Gauge(C,n)*(i1,j1) and
A26: [i2,j2] in Indices Gauge(C,n) and
A27: Upper_Seq(C,n)/.(t+1) = Gauge(C,n)*(i2,j2) and
A28: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 =
j2 or i1 = i2 & j1 = j2+1 by A11,A12,JORDAN8:3;
A29: 1 <= i1 by A24,MATRIX_0:32;
A30: 1 <= i2 by A26,MATRIX_0:32;
A31: i1 <= len Gauge(C,n) by A24,MATRIX_0:32;
A32: j1 = j2 by A22,A24,A25,A26,A27,Th6;
A33: i2 <= len Gauge(C,n) by A26,MATRIX_0:32;
A34: 1 <= j1 & j1 <= width Gauge(C,n) by A24,MATRIX_0:32;
then
A35: Gauge(C,n)*(Center Gauge(C,n),j1)`1 = (W-bound C + E-bound C)/2 by A1
,Th35
.= FiP`1 by A17,Th33;
Gauge(C,n)*(Center Gauge(C,n),j1)`2 = Gauge(C,n)*(1,j1)`2 by A2,A7,A34,
GOBOARD5:1
.= FiP`2 by A23,A25,A29,A31,A34,GOBOARD5:1;
then
A36: FiP = Gauge(C,n)*(Center Gauge(C,n),j1) by A35,TOPREAL3:6;
now
per cases by A28,A32;
suppose
A37: i1+1 = i2;
i1 < i1+1 by NAT_1:13;
then
A38: Gauge(C,n)*(i1,j1)`1 <= Gauge(C,n)*(i1+1,j1)`1 by A29,A34,A33,A37,
SPRECT_3:13;
then Gauge(C,n)*(i1,j1)`1 <= FiP`1 by A13,A14,A25,A27,A32,A37,
TOPREAL1:3;
then i1 <= Center Gauge(C,n) by A2,A31,A34,A35,GOBOARD5:3;
then i1 = Center Gauge(C,n) or i1 < Center Gauge(C,n) by XXREAL_0:1;
then
A39: i1 = Center Gauge(C,n) or i1+1 <= Center Gauge(C,n) by NAT_1:13;
FiP`1 <= Gauge(C,n)*(i1+1,j1)`1 by A13,A14,A25,A27,A32,A37,A38,
TOPREAL1:3;
then Center Gauge(C,n) <= i1+1 by A7,A34,A30,A35,A37,GOBOARD5:3;
then i1 = Center Gauge(C,n) or i1+1 = Center Gauge(C,n) by A39,
XXREAL_0:1;
hence thesis by A15,A16,A25,A27,A32,A36,A37,PARTFUN2:2;
end;
suppose
A40: i1 = i2+1;
i2 < i2+1 by NAT_1:13;
then
A41: Gauge(C,n)*(i2,j1)`1 <= Gauge(C,n)*(i2+1,j1)`1 by A31,A34,A30,A40,
SPRECT_3:13;
then Gauge(C,n)*(i2,j1)`1 <= FiP`1 by A13,A14,A25,A27,A32,A40,
TOPREAL1:3;
then i2 <= Center Gauge(C,n) by A2,A34,A33,A35,GOBOARD5:3;
then i2 = Center Gauge(C,n) or i2 < Center Gauge(C,n) by XXREAL_0:1;
then
A42: i2 = Center Gauge(C,n) or i2+1 <= Center Gauge(C,n) by NAT_1:13;
FiP`1 <= Gauge(C,n)*(i2+1,j1)`1 by A13,A14,A25,A27,A32,A40,A41,
TOPREAL1:3;
then Center Gauge(C,n) <= i2+1 by A7,A29,A34,A35,A40,GOBOARD5:3;
then i2 = Center Gauge(C,n) or i2+1 = Center Gauge(C,n) by A42,
XXREAL_0:1;
hence thesis by A15,A16,A25,A27,A32,A36,A40,PARTFUN2:2;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th48:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for n be Nat st n > 0 holds Last_Point(L~Lower_Seq(C,n),
E-max L~Cage(C,n),W-min L~Cage(C,n), Vertical_Line ((W-bound L~Cage(C,n)+
E-bound L~Cage(C,n))/2)) in rng Lower_Seq(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
assume
A1: n > 0;
set sr = (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2;
set Ebo = E-bound L~Cage(C,n);
set Wbo = W-bound L~Cage(C,n);
set Emax = E-max L~Cage(C,n);
set Wmin = W-min L~Cage(C,n);
set LaP = Last_Point(L~Lower_Seq(C,n),Emax,Wmin,Vertical_Line sr);
A2: Lower_Seq(C,n)/.1 = E-max L~Cage(C,n) & Lower_Seq(C,n)/.len Lower_Seq(C,
n) = W-min L~Cage(C,n) by JORDAN1F:6,8;
then
A3: L~Lower_Seq(C,n) is_an_arc_of Emax,Wmin by TOPREAL1:25;
A4: Wbo <= Ebo by SPRECT_1:21;
then Wbo <= sr by JORDAN6:1;
then
A5: Wmin`1 <= sr by EUCLID:52;
sr <= Ebo by A4,JORDAN6:1;
then
A6: sr <= Emax`1 by EUCLID:52;
A7: L~Lower_Seq(C,n) is_an_arc_of Wmin,Emax by A2,JORDAN5B:14,TOPREAL1:25;
then
A8: L~Lower_Seq(C,n) meets Vertical_Line(sr) by A5,A6,JORDAN6:49;
L~Lower_Seq(C,n) /\ Vertical_Line(sr) is closed by A7,A5,A6,JORDAN6:49;
then
A9: LaP in L~Lower_Seq(C,n) /\ Vertical_Line sr by A3,A8,JORDAN5C:def 2;
then LaP in L~Lower_Seq(C,n) by XBOOLE_0:def 4;
then consider t be Nat such that
A10: 1 <= t and
A11: t+1 <= len Lower_Seq(C,n) and
A12: LaP in LSeg(Lower_Seq(C,n),t) by SPPOL_2:13;
A13: LSeg(Lower_Seq(C,n),t) = LSeg(Lower_Seq(C,n)/.t,Lower_Seq(C,n)/.(t+1))
by A10,A11,TOPREAL1:def 3;
1 <= t+1 by A10,NAT_1:13;
then
A14: t+1 in dom Lower_Seq(C,n) by A11,FINSEQ_3:25;
t < len Lower_Seq(C,n) by A11,NAT_1:13;
then
A15: t in dom Lower_Seq(C,n) by A10,FINSEQ_3:25;
LaP in Vertical_Line sr by A9,XBOOLE_0:def 4;
then
A16: LaP`1 = sr by JORDAN6:31;
A17: LaP = Last_Point (LSeg (Lower_Seq(C,n),t),Lower_Seq(C,n)/.t, Lower_Seq(
C,n)/.(t+1),Vertical_Line sr) by A2,A8,A10,A11,A12,JORDAN5C:20,JORDAN6:30;
now
per cases by SPPOL_1:19;
suppose
A18: LSeg(Lower_Seq(C,n),t) is vertical;
then (Lower_Seq(C,n)/.(t+1))`1 = sr by A12,A13,A16,SPPOL_1:41;
then Lower_Seq(C,n)/.(t+1) in {p where p is Point of TOP-REAL 2: p`1 =
sr};
then
A19: Lower_Seq(C,n)/.(t+1) in Vertical_Line sr by JORDAN6:def 6;
A20: LSeg(Lower_Seq(C,n),t) is closed & LSeg(Lower_Seq(C,n),t)
is_an_arc_of Lower_Seq(C,n)/.t, Lower_Seq(C,n)/.(t+1) by A13,A15,A14,
GOBOARD7:29,TOPREAL1:9;
(Lower_Seq(C,n)/.t)`1 = sr by A12,A13,A16,A18,SPPOL_1:41;
then Lower_Seq(C,n)/.t in {p where p is Point of TOP-REAL 2: p`1 = sr};
then Lower_Seq(C,n)/.t in Vertical_Line sr by JORDAN6:def 6;
then LSeg(Lower_Seq(C,n),t) c= Vertical_Line sr by A13,A19,JORDAN1A:13;
then
Last_Point (LSeg(Lower_Seq(C,n),t),Lower_Seq(C,n)/.t, Lower_Seq(C,n
)/.(t+1),Vertical_Line sr) = Lower_Seq(C,n)/.(t+1) by A20,JORDAN5C:7;
hence thesis by A17,A14,PARTFUN2:2;
end;
suppose
LSeg(Lower_Seq(C,n),t) is horizontal;
then
A21: (Lower_Seq(C,n)/.t)`2 = (Lower_Seq(C,n)/.(t+1))`2 by A13,SPPOL_1:15;
then
A22: LaP`2 = (Lower_Seq(C,n)/.t)`2 by A12,A13,GOBOARD7:6;
Lower_Seq(C,n) is_sequence_on Gauge(C,n) by Th5;
then consider i1,j1,i2,j2 be Nat such that
A23: [i1,j1] in Indices Gauge(C,n) and
A24: Lower_Seq(C,n)/.t = Gauge(C,n)*(i1,j1) and
A25: [i2,j2] in Indices Gauge(C,n) and
A26: Lower_Seq(C,n)/.(t+1) = Gauge(C,n)*(i2,j2) and
A27: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 =
j2 or i1 = i2 & j1 = j2+1 by A10,A11,JORDAN8:3;
A28: 1 <= i1 by A23,MATRIX_0:32;
A29: j1 = j2 by A21,A23,A24,A25,A26,Th6;
A30: i2 <= len Gauge(C,n) by A25,MATRIX_0:32;
A31: i1 <= len Gauge(C,n) by A23,MATRIX_0:32;
A32: 1 <= i2 by A25,MATRIX_0:32;
A33: Center Gauge(C,n) <= len Gauge(C,n) by JORDAN1B:13;
A34: 1 <= j1 & j1 <= width Gauge(C,n) by A23,MATRIX_0:32;
then
A35: Gauge(C,n)*(Center Gauge(C,n),j1)`1 = (W-bound C + E-bound C)/2 by A1
,Th35
.= LaP`1 by A16,Th33;
A36: 1 <= Center Gauge(C,n) by JORDAN1B:11;
then Gauge(C,n)*(Center Gauge(C,n),j1)`2 = Gauge(C,n)*(1,j1)`2 by A34,A33
,GOBOARD5:1
.= LaP`2 by A22,A24,A28,A31,A34,GOBOARD5:1;
then
A37: LaP = Gauge(C,n)*(Center Gauge(C,n),j1) by A35,TOPREAL3:6;
now
per cases by A27,A29;
suppose
A38: i1+1 = i2;
i1 < i1+1 by NAT_1:13;
then
A39: Gauge(C,n)*(i1,j1)`1 <= Gauge(C,n)*(i1+1,j1)`1 by A28,A34,A30,A38,
SPRECT_3:13;
then Gauge(C,n)*(i1,j1)`1 <= LaP`1 by A12,A13,A24,A26,A29,A38,
TOPREAL1:3;
then i1 <= Center Gauge(C,n) by A31,A34,A36,A35,GOBOARD5:3;
then i1 = Center Gauge(C,n) or i1 < Center Gauge(C,n) by XXREAL_0:1;
then
A40: i1 = Center Gauge(C,n) or i1+1 <= Center Gauge(C,n) by NAT_1:13;
LaP`1 <= Gauge(C,n)*(i1+1,j1)`1 by A12,A13,A24,A26,A29,A38,A39,
TOPREAL1:3;
then Center Gauge(C,n) <= i1+1 by A34,A32,A33,A35,A38,GOBOARD5:3;
then i1 = Center Gauge(C,n) or i1+1 = Center Gauge(C,n) by A40,
XXREAL_0:1;
hence thesis by A15,A14,A24,A26,A29,A37,A38,PARTFUN2:2;
end;
suppose
A41: i1 = i2+1;
i2 < i2+1 by NAT_1:13;
then
A42: Gauge(C,n)*(i2,j1)`1 <= Gauge(C,n)*(i2+1,j1)`1 by A31,A34,A32,A41,
SPRECT_3:13;
then Gauge(C,n)*(i2,j1)`1 <= LaP`1 by A12,A13,A24,A26,A29,A41,
TOPREAL1:3;
then i2 <= Center Gauge(C,n) by A34,A30,A36,A35,GOBOARD5:3;
then i2 = Center Gauge(C,n) or i2 < Center Gauge(C,n) by XXREAL_0:1;
then
A43: i2 = Center Gauge(C,n) or i2+1 <= Center Gauge(C,n) by NAT_1:13;
LaP`1 <= Gauge(C,n)*(i2+1,j1)`1 by A12,A13,A24,A26,A29,A41,A42,
TOPREAL1:3;
then Center Gauge(C,n) <= i2+1 by A28,A34,A33,A35,A41,GOBOARD5:3;
then i2 = Center Gauge(C,n) or i2+1 = Center Gauge(C,n) by A43,
XXREAL_0:1;
hence thesis by A15,A14,A24,A26,A29,A37,A41,PARTFUN2:2;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th49:
for f be S-Sequence_in_R2 for p be Point of TOP-REAL 2 st p in
rng f holds R_Cut(f,p) = mid(f,1,p..f)
proof
let f be S-Sequence_in_R2;
let p be Point of TOP-REAL 2;
assume
A1: p in rng f;
then consider i be Nat such that
A2: i in dom f and
A3: f.i = p by FINSEQ_2:10;
reconsider i as Nat;
A4: i <= len f by A2,FINSEQ_3:25;
len f >= 2 by TOPREAL1:def 8;
then
A5: rng f c= L~f by SPPOL_2:18;
then
A6: 1 <= Index(p,f) by A1,JORDAN3:8;
A7: Index(p,f) < len f by A1,A5,JORDAN3:8;
A8: 0+1 <= i by A2,FINSEQ_3:25;
then
A9: i-1 >= 0 by XREAL_1:19;
per cases by A8,XXREAL_0:1;
suppose
A10: 1 < i;
1 <= len f by A8,A4,XXREAL_0:2;
then 1 in dom f by FINSEQ_3:25;
then p <> f.1 by A2,A3,A10,FUNCT_1:def 4;
then
A11: R_Cut(f,p) = mid(f,1,Index(p,f))^<*p*> by JORDAN3:def 4;
A12: Index(p,f) + 1 = i by A3,A4,A10,JORDAN3:12;
A13: len mid(f,1,Index(p,f)) = Index(p,f)-'1+1 by A6,A7,FINSEQ_6:186
.= i-'1 by A1,A5,A12,JORDAN3:8,NAT_D:38;
A14: len mid(f,1,i) = i-'1+1 by A8,A4,FINSEQ_6:186
.= i by A8,XREAL_1:235;
then
A15: dom mid(f,1,i) = Seg i by FINSEQ_1:def 3;
A16: now
let j be Nat;
reconsider a=j as Nat;
assume
A17: j in dom mid(f,1,i);
then
A18: 1 <= j by A15,FINSEQ_1:1;
A19: j <= i by A15,A17,FINSEQ_1:1;
now
per cases by A19,XXREAL_0:1;
suppose
j < i;
then
A20: j <= Index(p,f) by A12,NAT_1:13;
then j <= i-'1 by A9,A12,XREAL_0:def 2;
then
A21: j in dom mid(f,1,Index(p,f)) by A13,A18,FINSEQ_3:25;
thus mid(f,1,i).j = f.a by A4,A18,A19,FINSEQ_6:123
.= mid(f,1,Index(p,f)).a by A7,A18,A20,FINSEQ_6:123
.= (mid(f,1,Index(p,f))^<*p*>).j by A21,FINSEQ_1:def 7;
end;
suppose
A22: j = i;
A23: i-'1+1 = i by A8,XREAL_1:235;
thus mid(f,1,i).j = f.a by A4,A18,A19,FINSEQ_6:123
.= (mid(f,1,Index(p,f))^<*p*>).j by A3,A13,A22,A23,FINSEQ_1:42;
end;
end;
hence mid(f,1,i).j = (mid(f,1,Index(p,f))^<*p*>).j;
end;
len (mid(f,1,Index(p,f))^<*p*>) = i-'1+1 by A13,FINSEQ_2:16
.= i by A8,XREAL_1:235;
then mid(f,1,i) = R_Cut(f,p) by A11,A14,A16,FINSEQ_2:9;
hence thesis by A2,A3,FINSEQ_5:11;
end;
suppose
A24: 1 = i;
then
A25: R_Cut(f,p) = <*p*> by A3,JORDAN3:def 4;
A26: p = f/.1 by A2,A3,A24,PARTFUN1:def 6;
then S: p..f = 1 by FINSEQ_6:43;
f/.1 = f.1 by A2,PARTFUN1:def 6,A24;
hence thesis by A2,A24,A25,A26,S,FINSEQ_6:193;
end;
end;
theorem Th50:
for f be S-Sequence_in_R2 for Q be closed Subset of TOP-REAL 2
st L~f meets Q & not f/.1 in Q & First_Point(L~f,f/.1,f/.len f,Q) in rng f
holds L~mid(f,1,First_Point(L~f,f/.1,f/.len f,Q)..f) /\ Q = {First_Point(L~f,f
/.1,f/.len f,Q)}
proof
let f be S-Sequence_in_R2;
let Q be closed Subset of TOP-REAL 2;
assume that
A1: L~f meets Q & not f/.1 in Q and
A2: First_Point(L~f,f/.1,f/.len f,Q) in rng f;
L~R_Cut(f,First_Point(L~f,f/.1,f/.len f,Q)) /\ Q = {First_Point(L~f,f/.1
,f/.len f,Q)} by A1,SPRECT_4:1;
hence thesis by A2,Th49;
end;
theorem Th51:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for n be Nat st n > 0 for k be Nat st 1 <= k &
k < First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n),
Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2)).. Upper_Seq(C,n)
holds (Upper_Seq(C,n)/.k)`1 < (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
assume
A1: n > 0;
set US = Upper_Seq(C,n);
set sr = (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2;
set Ebo = E-bound L~Cage(C,n);
set Wbo = W-bound L~Cage(C,n);
set Emax = E-max L~Cage(C,n);
set Wmin = W-min L~Cage(C,n);
set FiP = First_Point(L~US,Wmin,Emax,Vertical_Line sr);
defpred P[Nat] means 1 <= $1 & $1 < FiP..US implies (US/.$1)`1 < sr;
A2: Wbo < Ebo by SPRECT_1:31;
then
A3: Wbo < sr by XREAL_1:226;
A4: sr < Ebo by A2,XREAL_1:226;
A5: for k be non zero Nat st P[k] holds P[k+1]
proof
set GC1 = Gauge(C,n)*(Center Gauge(C,n),1);
let k be non zero Nat;
assume
A6: 1 <= k & k < FiP..US implies (US/.k)`1 < sr;
4 <= len Gauge(C,n) by JORDAN8:10;
then 1 <= len Gauge(C,n) by XXREAL_0:2;
then
A7: 1 <= width Gauge(C,n) by JORDAN8:def 1;
then
A8: GC1`1 = (W-bound C + E-bound C)/2 by A1,Th35
.= sr by Th33;
A9: k >= 1 by NAT_1:14;
A10: US/.len US = Emax by JORDAN1F:7;
A11: FiP in rng US by A1,Th47;
then
A12: FiP..Upper_Seq(C,n) in dom Upper_Seq(C,n) by FINSEQ_4:20;
then
A13: 1 <= FiP..US by FINSEQ_3:25;
A14: 1 <= Center Gauge(C,n) by JORDAN1B:11;
A15: US/.1 = Wmin by JORDAN1F:5;
reconsider kk=k as Nat;
assume that
A16: 1 <= k+1 and
A17: k+1 < FiP..US;
A18: FiP..US <= len US by A12,FINSEQ_3:25;
then
A19: k+1 <= len US by A17,XXREAL_0:2;
US is_sequence_on Gauge(C,n) by Th4;
then consider i1,j1,i2,j2 be Nat such that
A20: [i1,j1] in Indices Gauge(C,n) and
A21: US/.kk = Gauge(C,n)*(i1,j1) and
A22: [i2,j2] in Indices Gauge(C,n) and
A23: US/.(kk+1) = Gauge(C,n)*(i2,j2) and
A24: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A9,A19,JORDAN8:3;
A25: 1 <= i1 by A20,MATRIX_0:32;
A26: 1 <= j1 & j1 <= width Gauge(C,n) by A20,MATRIX_0:32;
A27: j2 <= width Gauge(C,n) by A22,MATRIX_0:32;
A28: 1 <= i2 & 1 <= j2 by A22,MATRIX_0:32;
A29: i2 <= len Gauge(C,n) by A22,MATRIX_0:32;
A30: i1 <= len Gauge(C,n) by A20,MATRIX_0:32;
A31: Center Gauge(C,n) <= len Gauge(C,n) & i1+1 >= 1 by JORDAN1B:13,NAT_1:11;
now
per cases by A24;
suppose
i1 = i2 & j1+1 = j2;
then (US/.k)`1 = Gauge(C,n)*(i2,1)`1 by A21,A25,A30,A26,GOBOARD5:2
.= (US/.(k+1))`1 by A23,A29,A28,A27,GOBOARD5:2;
hence thesis by A6,A17,NAT_1:13,14;
end;
suppose
A32: i1+1 = i2 & j1 = j2;
A33: now
A34: k+1 >= 1+1 by A9,XREAL_1:7;
len mid(US,1,FiP..US) = FiP..US-'1+1 by A13,A18,FINSEQ_6:186
.= FiP..US by A13,XREAL_1:235;
then
A35: rng mid(US,1,FiP..US) c= L~mid(US,1,FiP..US) by A17,A34,SPPOL_2:18
,XXREAL_0:2;
A36: US/.(FiP..US) = FiP by A11,FINSEQ_5:38;
A37: now
assume US/.1 in Vertical_Line sr;
then Wmin`1 = sr by A15,JORDAN6:31;
hence contradiction by A3,EUCLID:52;
end;
A38: Wmin`1 <= sr & sr <= Emax`1 by A3,A4,EUCLID:52;
A39: Vertical_Line sr is closed & L~US is_an_arc_of Wmin,Emax by A15,A10,
JORDAN6:30,TOPREAL1:25;
First_Point(L~US,US/.1,US/.len US,Vertical_Line sr) in rng US
by A1,A15,A10,Th47;
then
A40: L~mid(US,1,FiP..US) /\ Vertical_Line sr = {FiP} by A15,A10,A39,A38
,A37,Th50,JORDAN6:49;
A41: mid(US,1,FiP..US) = US|(FiP..US) & US|Seg(FiP..US) = US|(FiP..
US) by A13,FINSEQ_1:def 16,FINSEQ_6:116;
assume (US/.(k+1))`1 = sr;
then US/.(k+1) in {p where p is Point of TOP-REAL 2 : p`1 = sr};
then
A42: US/.(k+1) in Vertical_Line sr by JORDAN6:def 6;
A43: k+1 in dom US by A16,A19,FINSEQ_3:25;
k+1 in Seg (FiP..US) by A16,A17,FINSEQ_1:1;
then US/.(k+1) in rng mid(US,1,FiP..US) by A41,A43,PARTFUN2:18;
then US/.(k+1) in {FiP} by A42,A35,A40,XBOOLE_0:def 4;
then US/.(k+1) = FiP by TARSKI:def 1;
hence contradiction by A17,A12,A43,A36,PARTFUN2:10;
end;
i1 < Center Gauge(C,n) by A6,A17,A21,A30,A26,A14,A7,A8,JORDAN1A:18
,NAT_1:13,14;
then i1+1 <= Center Gauge(C,n) by NAT_1:13;
then (US/.(k+1))`1 <= sr by A23,A26,A7,A8,A31,A32,JORDAN1A:18;
hence thesis by A33,XXREAL_0:1;
end;
suppose
i1 = i2+1 & j1 = j2;
then i2 < i1 by NAT_1:13;
then (US/.(k+1))`1 <= (US/.k)`1 by A21,A23,A30,A26,A28,A27,JORDAN1A:18;
hence thesis by A6,A17,NAT_1:13,14,XXREAL_0:2;
end;
suppose
i1 = i2 & j1 = j2+1;
then (US/.k)`1 = Gauge(C,n)*(i2,1)`1 by A21,A25,A30,A26,GOBOARD5:2
.= (US/.(k+1))`1 by A23,A29,A28,A27,GOBOARD5:2;
hence thesis by A6,A17,NAT_1:13,14;
end;
end;
hence thesis;
end;
A44: P[1]
proof
assume that
1 <= 1 and
1 < FiP..US;
US/.1 = Wmin by JORDAN1F:5;
hence thesis by A3,EUCLID:52;
end;
A45: for k being non zero Nat holds P[k] from NAT_1:sch 10(A44, A5);
let k be Nat;
assume 1 <= k & k < First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~
Cage(C,n ), Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))..
Upper_Seq(C,n );
hence thesis by A45;
end;
theorem Th52:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for n be Nat st n > 0 for k be Nat st 1 <= k & k <
First_Point(L~Rev Lower_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n),
Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2)).. Rev Lower_Seq(C,
n) holds (Rev Lower_Seq(C,n)/.k)`1 < (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/
2
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
assume
A1: n > 0;
set LS = Lower_Seq(C,n);
set sr = (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2;
set Ebo = E-bound L~Cage(C,n);
set Wbo = W-bound L~Cage(C,n);
set Emax = E-max L~Cage(C,n);
set Wmin = W-min L~Cage(C,n);
set RLS = Rev LS;
set FiP = First_Point(L~RLS,Wmin,Emax,Vertical_Line sr);
set LaP = Last_Point(L~LS,Emax,Wmin,Vertical_Line sr);
A2: L~RLS = L~LS by SPPOL_2:22;
A3: len RLS = len LS by FINSEQ_5:def 3;
defpred P[Nat] means 1 <= $1 & $1 < FiP..RLS implies (RLS/.$1)`1 < sr;
A4: rng RLS = rng LS by FINSEQ_5:57;
A5: Wbo < Ebo by SPRECT_1:31;
then
A6: Wbo < sr by XREAL_1:226;
A7: sr < Ebo by A5,XREAL_1:226;
A8: for k be non zero Nat st P[k] holds P[k+1]
proof
A9: Wbo <= Ebo by SPRECT_1:21;
then Wbo <= sr by JORDAN6:1;
then
A10: Wmin`1 <= sr by EUCLID:52;
sr <= Ebo by A9,JORDAN6:1;
then
A11: sr <= Emax`1 by EUCLID:52;
A12: RLS/.len RLS = LS/.1 by A3,FINSEQ_5:65
.= Emax by JORDAN1F:6;
set GC1 = Gauge(C,n)*(Center Gauge(C,n),1);
let k be non zero Nat;
assume
A13: 1 <= k & k < FiP..RLS implies (RLS/.k)`1 < sr;
4 <= len Gauge(C,n) by JORDAN8:10;
then 1 <= len Gauge(C,n) by XXREAL_0:2;
then
A14: 1 <= width Gauge(C,n) by JORDAN8:def 1;
then
A15: GC1`1 = (W-bound C + E-bound C)/2 by A1,Th35
.= sr by Th33;
A16: LS/.1 = Emax & LS/.len LS = Wmin by JORDAN1F:6,8;
then
A17: L~LS is_an_arc_of Emax,Wmin by TOPREAL1:25;
A18: 1 <= Center Gauge(C,n) by JORDAN1B:11;
A19: RLS/.1 = LS/.len LS by FINSEQ_5:65
.= Wmin by JORDAN1F:8;
L~LS is_an_arc_of Wmin,Emax by A16,JORDAN5B:14,TOPREAL1:25;
then
L~LS meets Vertical_Line(sr) & L~LS /\ Vertical_Line(sr) is closed by A10
,A11,JORDAN6:49;
then
A20: FiP = LaP by A2,A17,JORDAN5C:18;
then
A21: FiP..RLS in dom RLS by A1,A4,Th48,FINSEQ_4:20;
then
A22: 1 <= FiP..RLS by FINSEQ_3:25;
A23: k >= 1 by NAT_1:14;
reconsider kk=k as Nat;
assume that
A24: 1 <= k+1 and
A25: k+1 < FiP..RLS;
A26: FiP..RLS <= len RLS by A21,FINSEQ_3:25;
then
A27: k+1 <= len RLS by A25,XXREAL_0:2;
LS is_sequence_on Gauge(C,n) by Th5;
then RLS is_sequence_on Gauge(C,n) by JORDAN9:5;
then consider i1,j1,i2,j2 be Nat such that
A28: [i1,j1] in Indices Gauge(C,n) and
A29: RLS/.kk = Gauge(C,n)*(i1,j1) and
A30: [i2,j2] in Indices Gauge(C,n) and
A31: RLS/.(kk+1) = Gauge(C,n)*(i2,j2) and
A32: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A23,A27,JORDAN8:3;
A33: 1 <= i1 by A28,MATRIX_0:32;
A34: 1 <= j1 & j1 <= width Gauge(C,n) by A28,MATRIX_0:32;
A35: i2 <= len Gauge(C,n) by A30,MATRIX_0:32;
A36: i1 <= len Gauge(C,n) by A28,MATRIX_0:32;
A37: j2 <= width Gauge(C,n) by A30,MATRIX_0:32;
A38: 1 <= i2 & 1 <= j2 by A30,MATRIX_0:32;
A39: Center Gauge(C,n) <= len Gauge(C,n) & i1+1 >= 1 by JORDAN1B:13,NAT_1:11;
now
per cases by A32;
suppose
i1 = i2 & j1+1 = j2;
then (RLS/.k)`1 = Gauge(C,n)*(i2,1)`1 by A29,A33,A36,A34,GOBOARD5:2
.= (RLS/.(k+1))`1 by A31,A35,A38,A37,GOBOARD5:2;
hence thesis by A13,A25,NAT_1:13,14;
end;
suppose
A40: i1+1 = i2 & j1 = j2;
A41: now
A42: now
assume RLS/.1 in Vertical_Line sr;
then Wmin`1 = sr by A19,JORDAN6:31;
hence contradiction by A6,EUCLID:52;
end;
assume (RLS/.(k+1))`1 = sr;
then RLS/.(k+1) in {p where p is Point of TOP-REAL 2 : p`1 = sr};
then
A43: RLS/.(k+1) in Vertical_Line sr by JORDAN6:def 6;
A44: sr <= Emax`1 by A7,EUCLID:52;
L~RLS is_an_arc_of Wmin,Emax & Wmin`1 <= sr by A6,A19,A12,EUCLID:52
,TOPREAL1:25;
then
A45: L~RLS meets Vertical_Line sr by A44,JORDAN6:49;
A46: RLS/.(FiP..RLS) = FiP by A1,A4,A20,Th48,FINSEQ_5:38;
A47: k+1 >= 1+1 by A23,XREAL_1:7;
len mid(RLS,1,FiP..RLS) = FiP..RLS-'1+1 by A22,A26,FINSEQ_6:186
.= FiP..RLS by A22,XREAL_1:235;
then
A48: rng mid(RLS,1,FiP..RLS) c= L~mid(RLS,1,FiP..RLS) by A25,A47,
SPPOL_2:18,XXREAL_0:2;
A49: k+1 in dom RLS by A24,A27,FINSEQ_3:25;
Vertical_Line sr is closed & RLS is being_S-Seq by JORDAN6:30;
then
A50: L~mid(RLS,1,FiP..RLS) /\ Vertical_Line sr = {FiP} by A1,A4,A20,A19
,A12,A45,A42,Th48,Th50;
A51: mid(RLS,1,FiP..RLS) = RLS|(FiP..RLS) & RLS|Seg(FiP..RLS) = RLS|
(FiP..RLS) by A22,FINSEQ_1:def 16,FINSEQ_6:116;
k+1 in Seg (FiP..RLS) by A24,A25,FINSEQ_1:1;
then RLS/.(k+1) in rng mid(RLS,1,FiP..RLS) by A51,A49,PARTFUN2:18;
then RLS/.(k+1) in {FiP} by A43,A48,A50,XBOOLE_0:def 4;
then RLS/.(k+1) = FiP by TARSKI:def 1;
hence contradiction by A25,A21,A49,A46,PARTFUN2:10;
end;
i1 < Center Gauge(C,n) by A13,A25,A29,A36,A34,A18,A14,A15,JORDAN1A:18
,NAT_1:13,14;
then i1+1 <= Center Gauge(C,n) by NAT_1:13;
then (RLS/.(k+1))`1 <= sr by A31,A34,A14,A15,A39,A40,JORDAN1A:18;
hence thesis by A41,XXREAL_0:1;
end;
suppose
i1 = i2+1 & j1 = j2;
then i2 < i1 by NAT_1:13;
then (RLS/.(k+1))`1 <= (RLS/.k)`1 by A29,A31,A36,A34,A38,A37,
JORDAN1A:18;
hence thesis by A13,A25,NAT_1:13,14,XXREAL_0:2;
end;
suppose
i1 = i2 & j1 = j2+1;
then (RLS/.k)`1 = Gauge(C,n)*(i2,1)`1 by A29,A33,A36,A34,GOBOARD5:2
.= (RLS/.(k+1))`1 by A31,A35,A38,A37,GOBOARD5:2;
hence thesis by A13,A25,NAT_1:13,14;
end;
end;
hence thesis;
end;
A52: P[1]
proof
assume that
1 <= 1 and
1 < FiP..RLS;
RLS/.1 = LS/.len LS by FINSEQ_5:65
.= Wmin by JORDAN1F:8;
hence thesis by A6,EUCLID:52;
end;
A53: for k being non zero Nat holds P[k] from NAT_1:sch 10(A52, A8);
let k be Nat;
assume 1 <= k & k < First_Point(L~Rev Lower_Seq(C,n),W-min L~Cage(C,n),
E-max L~Cage (C,n),Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))
..Rev Lower_Seq(C,n);
hence thesis by A53;
end;
theorem Th53:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for n be Nat st n > 0 for q be Point of TOP-REAL 2 holds
q in rng mid(Upper_Seq(C,n),2,First_Point(L~Upper_Seq(C,n), W-min L~Cage(C,n),
E-max L~Cage(C,n),Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))
..Upper_Seq(C,n)) implies q`1 <= (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
set Wmin = W-min L~Cage(C,n);
set Emax = E-max L~Cage(C,n);
set Wbo = W-bound L~Cage(C,n);
set Ebo = E-bound L~Cage(C,n);
set sr = (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2;
set US = Upper_Seq(C,n);
set FiP = First_Point(L~US,Wmin,Emax,Vertical_Line sr);
A1: US/.1 = Wmin by JORDAN1F:5;
US/.len US = Emax by JORDAN1F:7;
then
A2: L~US is_an_arc_of Wmin,Emax by A1,TOPREAL1:25;
assume
A3: n > 0;
then
A4: FiP in rng US by Th47;
then
A5: FiP..US in dom US by FINSEQ_4:20;
then
A6: FiP..US <= len US by FINSEQ_3:25;
A7: Wbo < Ebo by SPRECT_1:31;
then
A8: Wbo < sr by XREAL_1:226;
sr < Ebo by A7,XREAL_1:226;
then
A9: sr <= Emax`1 by EUCLID:52;
Wmin`1 <= sr by A8,EUCLID:52;
then
L~US meets Vertical_Line sr & L~US /\ Vertical_Line sr is closed by A2,A9,
JORDAN6:49;
then FiP in L~US /\ Vertical_Line sr by A2,JORDAN5C:def 1;
then FiP in Vertical_Line sr by XBOOLE_0:def 4;
then
A10: FiP`1 = sr by JORDAN6:31;
A11: Wmin in rng US by A1,FINSEQ_6:42;
A12: now
assume FiP..US = 1;
then FiP..US = (US/.1)..US by FINSEQ_6:43
.= Wmin..US by JORDAN1F:5;
then FiP = Wmin by A4,A11,FINSEQ_5:9;
hence contradiction by A8,A10,EUCLID:52;
end;
1 <= FiP..US by A5,FINSEQ_3:25;
then FiP..US > 1 by A12,XXREAL_0:1;
then
A13: 1+1+0 <= FiP..US by NAT_1:13;
then FiP..US-2 >= 0 by XREAL_1:19;
then FiP..US-'2 = FiP..US-2 by XREAL_0:def 2;
then
A14: len mid(US,2,FiP..US) = FiP..US-2+1 by A6,A13,FINSEQ_6:186;
let q be Point of TOP-REAL 2;
assume q in rng mid(US,2,FiP..US);
then consider k be Element of NAT such that
A15: k in dom mid(US,2,FiP..US) and
A16: q = mid(US,2,FiP..US)/.k by PARTFUN2:2;
k+2 >= 1+1 by NAT_1:11;
then
A17: k+2-1 >= 1+1-1 by XREAL_1:9;
len US >= 3 by JORDAN1E:15;
then len US >= 2 by XXREAL_0:2;
then 2 in dom US by FINSEQ_3:25;
then
A18: mid(US,2,FiP..US)/.k = US/.(k+2-'1) by A15,A5,A13,SPRECT_2:3
.= US/.(k+(2-1)) by A17,XREAL_0:def 2;
k <= len mid(US,2,FiP..US) by A15,FINSEQ_3:25;
then k < FiP..US-2+1+1 by A14,NAT_1:13;
then
A19: k+1 <= FiP..US by NAT_1:13;
per cases by A19,XXREAL_0:1;
suppose
k+1 < FiP..US;
hence thesis by A3,A16,A18,Th51,NAT_1:11;
end;
suppose
k+1 = FiP..US;
hence thesis by A16,A4,A10,A18,FINSEQ_5:38;
end;
end;
theorem Th54:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for n be Nat st n > 0 holds First_Point(L~Upper_Seq(C,n),
W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line((W-bound L~Cage(C,n)+E-bound
L~Cage(C,n))/2))`2 > Last_Point(L~Lower_Seq(C,n),E-max L~Cage(C,n),W-min L~Cage
(C,n), Vertical_Line((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))`2
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
set sr = (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2;
set Wmin = W-min L~Cage(C,n);
set Emax = E-max L~Cage(C,n);
set Nbo = N-bound L~Cage(C,n);
set Ebo = E-bound L~Cage(C,n);
set Sbo = S-bound L~Cage(C,n);
set Wbo = W-bound L~Cage(C,n);
set SW = SW-corner L~Cage(C,n);
set FiP = First_Point(L~Upper_Seq(C,n),Wmin,Emax,Vertical_Line sr);
set LaP = Last_Point(L~Lower_Seq(C,n),Emax,Wmin,Vertical_Line sr);
set g = mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n))^<*|[Ebo,FiP`2]|*>;
set h = <*SW*>^((Rev Lower_Seq(C,n))-:LaP)^<*|[sr,Nbo]|*>;
A1: Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by JORDAN1F:5;
A2: Wbo <= Ebo by SPRECT_1:21;
then Wbo <= sr by JORDAN6:1;
then
A3: Wmin`1 <= sr by EUCLID:52;
sr <= Ebo by A2,JORDAN6:1;
then
A4: sr <= Emax`1 by EUCLID:52;
set GCw = Gauge(C,n)*(Center Gauge(C,n),width Gauge(C,n));
A5: 1 <= Center Gauge(C,n) by JORDAN1B:11;
len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
then
A6: GCw`2 = Nbo by A5,JORDAN1A:70,JORDAN1B:13;
A7: SW`2 <= Wmin`2 by PSCOMP_1:30;
A8: |[sr,Nbo]|`2 = Nbo by EUCLID:52;
set RevL = (Rev Lower_Seq(C,n))-:LaP;
A9: <*|[Ebo,FiP`2]|*> is one-to-one & <*|[Ebo,FiP`2]|*> is special by
FINSEQ_3:93;
A10: rng ((Rev Lower_Seq(C,n))-:LaP) c= rng (Rev Lower_Seq(C,n)) by FINSEQ_5:48
;
A11: Lower_Seq(C,n)/.1 = E-max L~Cage(C,n) & Lower_Seq(C,n)/.len Lower_Seq(C
,n) = W-min L~Cage(C,n) by JORDAN1F:6,8;
then
A12: L~Lower_Seq(C,n) is_an_arc_of Emax,Wmin by TOPREAL1:25;
A13: 4 <= len Gauge(C,n) by JORDAN8:10;
then
A14: len Gauge(C,n) >= 3 by XXREAL_0:2;
A15: Wbo < Ebo by SPRECT_1:31;
then
A16: Wbo < sr by XREAL_1:226;
L~Lower_Seq(C,n) is_an_arc_of Wmin,Emax by A11,JORDAN5B:14,TOPREAL1:25;
then
A17: L~Lower_Seq(C,n) meets Vertical_Line(sr) & L~Lower_Seq(C,n) /\
Vertical_Line (sr) is closed by A3,A4,JORDAN6:49;
then
A18: LaP in L~Lower_Seq(C,n) /\ Vertical_Line sr by A12,JORDAN5C:def 2;
then
A19: LaP in L~Lower_Seq(C,n) by XBOOLE_0:def 4;
then LaP in L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n) by XBOOLE_0:def 3;
then
A20: LaP in L~Cage(C,n) by JORDAN1E:13;
assume
A21: n > 0;
then
A22: FiP in rng Upper_Seq(C,n) by Th47;
then
A23: FiP..Upper_Seq(C,n) in dom Upper_Seq(C,n) by FINSEQ_4:20;
then
A24: 1<=FiP..Upper_Seq(C,n) by FINSEQ_3:25;
1 <= len Gauge(C,n) by A13,XXREAL_0:2;
then 1 <= width Gauge(C,n) by JORDAN8:def 1;
then GCw`1 = (W-bound C + E-bound C)/2 by A21,Th35
.= sr by Th33;
then GCw = |[sr,Nbo]| by A6,EUCLID:53;
then not |[sr,Nbo]| in rng Lower_Seq(C,n) by A5,A14,Th43,JORDAN1B:15;
then not |[sr,Nbo]| in rng (Rev Lower_Seq(C,n)) by FINSEQ_5:57;
then
A25: not |[sr,Nbo]| in rng ((Rev Lower_Seq(C,n))-:LaP) by A10;
SW`2 = Sbo by EUCLID:52;
then |[sr,Nbo]| <> SW by A8,SPRECT_1:32;
then not |[sr,Nbo]| in {SW} by TARSKI:def 1;
then not |[sr,Nbo]| in rng <*SW*> by FINSEQ_1:38;
then
not |[sr,Nbo]| in rng <*SW*> \/ rng ((Rev Lower_Seq(C,n))-:LaP) by A25,
XBOOLE_0:def 3;
then not |[sr,Nbo]| in rng (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) by
FINSEQ_1:31;
then rng (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) misses {|[sr,Nbo]|} by
ZFMISC_1:50;
then rng (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) /\ {|[sr,Nbo]|} = {};
then rng (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) /\ rng <*|[sr,Nbo]|*> = {} by
FINSEQ_1:38;
then
A26: rng (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) misses rng <*|[sr,Nbo]| *>;
LaP in rng Lower_Seq(C,n) by A21,Th48;
then
A27: LaP in rng Rev Lower_Seq(C,n) by FINSEQ_5:57;
then
A28: RevL is non empty by FINSEQ_5:47;
A29: len RevL = LaP..Rev Lower_Seq(C,n) by A27,FINSEQ_5:42;
A30: Upper_Seq(C,n)/.len Upper_Seq(C,n) = E-max L~Cage(C,n) by JORDAN1F:7;
then
A31: L~Upper_Seq(C,n) is_an_arc_of Wmin,Emax by A1,TOPREAL1:25;
A32: sr < Ebo by A15,XREAL_1:226;
then
A33: sr <= Emax`1 by EUCLID:52;
Wmin`1 <= sr by A16,EUCLID:52;
then L~Upper_Seq(C,n) meets Vertical_Line(sr) & L~Upper_Seq(C,n) /\
Vertical_Line (sr) is closed by A31,A33,JORDAN6:49;
then
A34: FiP in L~Upper_Seq(C,n) /\ Vertical_Line sr by A31,JORDAN5C:def 1;
then
A35: FiP in L~Upper_Seq(C,n) by XBOOLE_0:def 4;
then FiP in L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n) by XBOOLE_0:def 3;
then
A36: FiP in L~Cage(C,n) by JORDAN1E:13;
now
let m be Nat;
assume m in dom <*|[Ebo,FiP`2]|*>;
then m in Seg 1 by FINSEQ_1:38;
then m = 1 by FINSEQ_1:2,TARSKI:def 1;
then
A37: <*|[Ebo,FiP`2]|*>/.m = |[Ebo,FiP`2]| by FINSEQ_4:16;
then (<*|[Ebo,FiP`2]|*>/.m)`1 = Ebo by EUCLID:52;
hence W-bound L~Cage(C,n) <= (<*|[Ebo,FiP`2]|*>/.m)`1 & (<*|[Ebo,FiP`2]|*>
/.m)`1 <= E-bound L~Cage(C,n) by SPRECT_1:21;
(<*|[Ebo,FiP`2]|*>/.m)`2 = FiP`2 by A37,EUCLID:52;
hence S-bound L~Cage(C,n) <= (<*|[Ebo,FiP`2]|*>/.m)`2 & (<*|[Ebo,FiP`2]|*>
/.m)`2 <= N-bound L~Cage(C,n) by A36,PSCOMP_1:24;
end;
then
A38: <*|[Ebo,FiP`2]|*> is_in_the_area_of Cage(C,n) by SPRECT_2:def 1;
A39: FiP in Vertical_Line sr by A34,XBOOLE_0:def 4;
then
A40: FiP`1 = sr by JORDAN6:31;
now
assume
rng mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) /\ {|[Ebo,FiP`2]|} <> {};
then consider x be object such that
A41: x in rng mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) /\ {|[Ebo,FiP
`2]|} by XBOOLE_0:def 1;
x in rng mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) & x in {|[Ebo,FiP
`2 ]| } by A41,XBOOLE_0:def 4;
then |[Ebo,FiP`2]| in rng mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) by
TARSKI:def 1;
then |[Ebo,FiP`2]|`1 <= sr by A21,Th53;
hence contradiction by A32,EUCLID:52;
end;
then
rng mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) misses {|[Ebo,FiP`2]|};
then
A42: rng mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) misses rng <*|[Ebo,FiP`2
]|*> by FINSEQ_1:38;
A43: FiP..Upper_Seq(C,n)<=len Upper_Seq(C,n) by A23,FINSEQ_3:25;
LaP in Vertical_Line sr by A18,XBOOLE_0:def 4;
then
A44: LaP`1 = sr by JORDAN6:31;
A45: now
assume FiP`2 = LaP`2;
then FiP = LaP by A40,A44,TOPREAL3:6;
then FiP in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) by A35,A19,XBOOLE_0:def 4;
then FiP in {Wmin,Emax} by JORDAN1E:16;
then FiP = Wmin or FiP = Emax by TARSKI:def 2;
hence contradiction by A16,A32,A40,EUCLID:52;
end;
len Upper_Seq(C,n) >= 3 by JORDAN1E:15;
then
A46: len Upper_Seq(C,n) > 2 by XXREAL_0:2;
then
A47: 2 in dom Upper_Seq(C,n) by FINSEQ_3:25;
then
A48: (mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n))/.len mid(Upper_Seq(C,n),2,
FiP..Upper_Seq(C,n)))`2 = (Upper_Seq(C,n)/.(FiP..Upper_Seq(C,n)))`2 by A23,
SPRECT_2:9
.= FiP`2 by A22,FINSEQ_5:38
.= |[Ebo,FiP`2]|`2 by EUCLID:52
.= (<*|[Ebo,FiP`2]|*>/.1)`2 by FINSEQ_4:16;
2 <> FiP..Upper_Seq(C,n)
proof
assume 2 = FiP..Upper_Seq(C,n);
then Upper_Seq(C,n)/.2 = FiP by A22,FINSEQ_5:38;
then FiP`1 = Wbo by Th31;
then Wbo = sr by A39,JORDAN6:31;
hence contradiction by SPRECT_1:31;
end;
then
mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) is being_S-Seq by A46,A24,A43,
JORDAN3:6;
then reconsider g as one-to-one special FinSequence of TOP-REAL 2 by A42,A48
,A9,FINSEQ_3:91,GOBOARD2:8;
mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) is_in_the_area_of Cage(C,n)
by A47,A23,JORDAN1E:17,SPRECT_2:22;
then
A49: g is_in_the_area_of Cage(C,n) by A38,SPRECT_2:24;
A50: (g/.len g)`1 = (<*|[Ebo,FiP`2]|*>/.len <*|[Ebo,FiP`2]|*>)`1 by SPRECT_3:1
.= (<*|[Ebo,FiP`2]|*>/.1)`1 by FINSEQ_1:39
.= (|[Ebo,FiP`2]|)`1 by FINSEQ_4:16
.= E-bound L~Cage(C,n) by EUCLID:52;
A51: 1 <= len mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) by A47,A23,SPRECT_2:5;
then 1 in dom mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n)) by FINSEQ_3:25;
then (g/.1)`1 = (mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n))/.1)`1 by
FINSEQ_4:68
.= (Upper_Seq(C,n)/.2)`1 by A47,A23,SPRECT_2:8
.= W-bound L~Cage(C,n) by Th31;
then
A52: g is_a_h.c._for Cage(C,n) by A49,A50,SPRECT_2:def 2;
assume FiP`2 <= LaP`2;
then
A53: FiP`2 < LaP`2 by A45,XXREAL_0:1;
A54: rng Lower_Seq(C,n) c= rng Cage(C,n) by Th39;
now
per cases;
suppose
A55: SW <> Wmin;
not SW in rng Lower_Seq(C,n)
proof
SW`1 = Wmin`1 by PSCOMP_1:29;
then
A56: SW`2 <> Wmin`2 by A55,TOPREAL3:6;
assume SW in rng Lower_Seq(C,n);
then
A57: SW in rng Cage(C,n) by A54;
len Cage(C,n) > 4 by GOBOARD7:34;
then
A58: rng Cage(C,n) c= L~Cage(C,n) by SPPOL_2:18,XXREAL_0:2;
SW`1 = W-bound L~Cage(C,n) by EUCLID:52;
then SW in W-most L~Cage(C,n) by A57,A58,SPRECT_2:12;
then Wmin`2 <= SW`2 by PSCOMP_1:31;
hence contradiction by A7,A56,XXREAL_0:1;
end;
then not SW in rng (Rev Lower_Seq(C,n)) by FINSEQ_5:57;
then not SW in rng ((Rev Lower_Seq(C,n))-:LaP) by A10;
then {SW} misses rng ((Rev Lower_Seq(C,n))-:LaP) by ZFMISC_1:50;
then {SW} /\ rng ((Rev Lower_Seq(C,n))-:LaP) = {};
then rng <*SW*> /\ rng ((Rev Lower_Seq(C,n))-:LaP) = {} by FINSEQ_1:38;
then
A59: rng <*SW*> misses rng ((Rev Lower_Seq(C,n))-:LaP);
<*SW*> is one-to-one by FINSEQ_3:93;
then
A60: <*SW*>^((Rev Lower_Seq(C,n))-:LaP) is one-to-one by A59,FINSEQ_3:91;
set FiP2 = First_Point(L~Lower_Seq(C,n),Wmin,Emax,Vertical_Line sr);
set midU = mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n));
reconsider RevLS = Rev Lower_Seq(C,n) as special FinSequence of TOP-REAL
2;
(<*SW*>/.len <*SW*>)`1 = (<*SW*>/.1)`1 by FINSEQ_1:39
.= SW`1 by FINSEQ_4:16
.= W-bound L~Cage(C,n) by EUCLID:52
.= (W-min L~Cage(C,n))`1 by EUCLID:52
.= (Lower_Seq(C,n)/.len Lower_Seq(C,n))`1 by JORDAN1F:8
.= ((Rev Lower_Seq(C,n))/.1)`1 by FINSEQ_5:65
.= (((Rev Lower_Seq(C,n))-:LaP)/.1)`1 by A27,FINSEQ_5:44;
then
A61: <*SW*>^(RevLS-:LaP) is special by GOBOARD2:8;
(Rev Lower_Seq(C,n))-:LaP is non empty by A27,FINSEQ_5:47;
then
A62: ((<*SW*>^((Rev Lower_Seq(C,n))-:LaP))/. len (<*SW*>^((Rev
Lower_Seq(C,n))-:LaP)))`1 = (((Rev Lower_Seq(C,n))-:LaP)/.len ((Rev Lower_Seq(C
,n))-:LaP))`1 by SPRECT_3:1
.= (((Rev Lower_Seq(C,n))-:LaP)/.(LaP..Rev Lower_Seq(C,n)))`1 by A27,
FINSEQ_5:42
.= LaP`1 by A27,FINSEQ_5:45
.= |[sr,Nbo]|`1 by A44,EUCLID:52
.= (<*|[sr,Nbo]|*>/.1)`1 by FINSEQ_4:16;
<*|[sr,Nbo]|*> is one-to-one & <*|[sr,Nbo]|*> is special by FINSEQ_3:93;
then reconsider
h as one-to-one special FinSequence of TOP-REAL 2 by A26,A60,A62,A61,
FINSEQ_3:91,GOBOARD2:8;
A63: |[Ebo,FiP`2]|`1 = Ebo by EUCLID:52;
now
let m be Nat;
assume m in dom <*SW*>;
then m in Seg 1 by FINSEQ_1:38;
then m = 1 by FINSEQ_1:2,TARSKI:def 1;
then
A64: <*SW*>/.m = SW by FINSEQ_4:16;
then (<*SW*>/.m)`1 = Wbo by EUCLID:52;
hence W-bound L~Cage(C,n) <= (<*SW*>/.m)`1 & (<*SW*>/.m)`1 <= E-bound
L~Cage(C,n) by SPRECT_1:21;
(<*SW*>/.m)`2 = Sbo by A64,EUCLID:52;
hence S-bound L~Cage(C,n) <= (<*SW*>/.m)`2 & (<*SW*>/.m)`2 <= N-bound
L~Cage(C,n) by SPRECT_1:22;
end;
then
A65: <*SW*> is_in_the_area_of Cage(C,n) by SPRECT_2:def 1;
A66: RevL/.len RevL = RevL/.(LaP..Rev Lower_Seq(C,n)) by A27,FINSEQ_5:42
.= LaP by A27,FINSEQ_5:45;
now
let m be Nat;
A67: W-bound L~Cage(C,n) <= E-bound L~Cage(C,n) by SPRECT_1:21;
assume m in dom <*|[sr,Nbo]|*>;
then m in Seg 1 by FINSEQ_1:38;
then m = 1 by FINSEQ_1:2,TARSKI:def 1;
then
A68: <*|[sr,Nbo]|*>/.m = |[sr,Nbo]| by FINSEQ_4:16;
then (<*|[sr,Nbo]|*>/.m)`1 = sr by EUCLID:52;
hence
W-bound L~Cage(C,n) <= (<*|[sr,Nbo]|*>/.m)`1 & (<*|[sr,Nbo]|*>/.m
)`1 <= E-bound L~Cage(C,n) by A67,JORDAN6:1;
(<*|[sr,Nbo]|*>/.m)`2 = Nbo by A68,EUCLID:52;
hence
S-bound L~Cage(C,n) <= (<*|[sr,Nbo]|*>/.m)`2 & (<*|[sr,Nbo]|*>/.m
)`2 <= N-bound L~Cage(C,n) by SPRECT_1:22;
end;
then
A69: <*|[sr,Nbo]|*> is_in_the_area_of Cage(C,n) by SPRECT_2:def 1;
A70: L~Rev Lower_Seq(C,n) = L~Lower_Seq(C,n) & FiP2 = LaP by A12,A17,
JORDAN5C:18,SPPOL_2:22;
Rev Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:18,SPRECT_3:51
;
then ((Rev Lower_Seq(C,n))-:LaP) is_in_the_area_of Cage(C,n) by A27,
JORDAN1E:1;
then <*SW*>^((Rev Lower_Seq(C,n))-:LaP) is_in_the_area_of Cage(C,n) by
A65,SPRECT_2:24;
then
A71: h is_in_the_area_of Cage(C,n) by A69,SPRECT_2:24;
len (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) = 1 + len ((Rev Lower_Seq
(C,n))-:LaP) by FINSEQ_5:8;
then
A72: len (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) >= 1 by NAT_1:11;
1 in dom h by FINSEQ_5:6;
then h/.1 = h.1 by PARTFUN1:def 6;
then
A73: (h/.1)`2 = ((<*SW*>^((Rev Lower_Seq(C,n))-:LaP))/.1)`2 by A72,
FINSEQ_6:109
.= SW`2 by FINSEQ_5:15
.= S-bound L~Cage(C,n) by EUCLID:52;
A74: len h = len (<*SW*>^((Rev Lower_Seq(C,n))-:LaP)) + 1 by FINSEQ_2:16;
then
A75: 1+1 <= len h by A72,XREAL_1:7;
L~Cage(C,n) = L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n) by JORDAN1E:13;
then
A76: L~Upper_Seq(C,n) c= L~Cage(C,n) by XBOOLE_1:7;
A77: midU/.len midU = Upper_Seq(C,n)/.(FiP..Upper_Seq(C,n)) by A47,A23,
SPRECT_2:9
.= FiP by A22,FINSEQ_5:38;
A78: Wmin in rng Upper_Seq(C,n) by A1,FINSEQ_6:42;
now
assume FiP..Upper_Seq(C,n) = 1;
then FiP..Upper_Seq(C,n) = (Upper_Seq(C,n)/.1)..Upper_Seq(C,n) by
FINSEQ_6:43
.= Wmin..Upper_Seq(C,n) by JORDAN1F:5;
then FiP = Wmin by A22,A78,FINSEQ_5:9;
hence contradiction by A16,A40,EUCLID:52;
end;
then FiP..Upper_Seq(C,n) > 1 by A24,XXREAL_0:1;
then
A79: 1+1+0 <= FiP..Upper_Seq(C,n) by NAT_1:13;
then FiP..Upper_Seq(C,n)-2 >= 0 by XREAL_1:19;
then FiP..Upper_Seq(C,n)-'2 = FiP..Upper_Seq(C,n)-2 by XREAL_0:def 2;
then
A80: len midU = FiP..Upper_Seq(C,n)-2+1 by A43,A79,FINSEQ_6:186
.= FiP..Upper_Seq(C,n)-(2-1);
1 in dom RevL by A28,FINSEQ_5:6;
then
A81: (RevL^<*|[sr,Nbo]|*>)/.1 = RevL/.1 by FINSEQ_4:68
.= (Rev Lower_Seq(C,n))/.1 by A27,FINSEQ_5:44
.= Lower_Seq(C,n)/.len Lower_Seq(C,n) by FINSEQ_5:65
.= Wmin by JORDAN1F:8;
A82: SW`2 <= Wmin`2 by PSCOMP_1:30;
len g = len mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n))+1 by FINSEQ_2:16;
then
A83: 1+1 <= len g by A51,XREAL_1:7;
A84: L~g = L~midU \/ LSeg(midU/.len midU,|[Ebo,FiP`2]|) by A47,A23,SPPOL_2:19
,SPRECT_2:7;
L~Rev Lower_Seq(C,n) = L~RevL \/ L~((Rev Lower_Seq(C,n)):-LaP) by A27,
SPPOL_2:24;
then L~RevL c= L~Rev Lower_Seq(C,n) by XBOOLE_1:7;
then
A85: L~RevL c= L~Lower_Seq(C,n) by SPPOL_2:22;
A86: LaP`2 <= Nbo by A20,PSCOMP_1:24;
A87: |[Ebo,FiP`2]|`2 = FiP`2 by EUCLID:52;
then
A88: LSeg(FiP,|[Ebo,FiP`2]|) is horizontal by SPPOL_1:15;
LaP`1 = |[sr,Nbo]|`1 by A44,EUCLID:52;
then
A89: LSeg(LaP,|[sr,Nbo]|) is vertical by SPPOL_1:16;
A90: L~midU c= L~Upper_Seq(C,n) by A47,A23,SPRECT_3:18;
(h/.len h)`2 = |[sr,Nbo]|`2 by A74,FINSEQ_4:67
.= N-bound L~Cage(C,n) by EUCLID:52;
then h is_a_v.c._for Cage(C,n) by A71,A73,SPRECT_2:def 3;
then L~g meets L~h by A52,A75,A83,SPRECT_2:29;
then consider x be object such that
A91: x in L~g and
A92: x in L~h by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A91;
L~h = L~(<*SW*>^(((Rev Lower_Seq(C,n))-:LaP)^<*|[sr,Nbo]|*>)) by
FINSEQ_1:32
.= LSeg(SW,(RevL^<*|[sr,Nbo]|*>)/.1) \/ L~(RevL^<*|[sr,Nbo]|*>) by
SPPOL_2:20
.= LSeg(SW,(RevL^<*|[sr,Nbo]|*>)/.1) \/ (L~RevL \/ LSeg(RevL/.len
RevL,|[sr,Nbo]|)) by A27,FINSEQ_5:47,SPPOL_2:19;
then
A93: x in LSeg(SW,(RevL^<*|[sr,Nbo]|*>)/.1) or x in L~RevL \/ LSeg(RevL
/.len RevL,|[sr,Nbo]|) by A92,XBOOLE_0:def 3;
A94: SW`1 = Wmin`1 by PSCOMP_1:29;
then
A95: LSeg(SW,Wmin) is vertical by SPPOL_1:16;
now
per cases by A93,A81,A66,XBOOLE_0:def 3;
suppose
A96: x in LSeg(SW,Wmin);
then
A97: x`2 <= Wmin`2 by A82,TOPREAL1:4;
A98: x`1 = SW`1 by A95,A96,SPPOL_1:41;
then
A99: x`1 = Wbo by EUCLID:52;
now
per cases by A91,A84,A77,XBOOLE_0:def 3;
suppose
A100: x in L~midU;
then x in L~Upper_Seq(C,n) by A90;
then x in W-most L~Cage(C,n) by A76,A98,EUCLID:52,SPRECT_2:12;
then x`2 >= Wmin`2 by PSCOMP_1:31;
then x`2 = Wmin`2 by A97,XXREAL_0:1;
then x = Wmin by A94,A98,TOPREAL3:6;
then FiP..Upper_Seq(C,n) = 1 by A46,A1,A24,A43,A100,Th37;
then Wmin = FiP by A1,A22,FINSEQ_5:38;
hence contradiction by A16,A40,EUCLID:52;
end;
suppose
x in LSeg(FiP,|[Ebo,FiP`2]|);
hence contradiction by A16,A32,A40,A63,A99,TOPREAL1:3;
end;
end;
hence contradiction;
end;
suppose
A101: x in L~RevL;
now
per cases by A91,A84,A77,XBOOLE_0:def 3;
suppose
A102: x in L~midU;
then x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) by A90,A85,A101,
XBOOLE_0:def 4;
then
A103: x in {Wmin,Emax} by JORDAN1E:16;
now
per cases by A103,TARSKI:def 2;
suppose
x = Wmin;
then FiP..Upper_Seq(C,n) = 1 by A46,A1,A24,A43,A102,Th37;
then Wmin = FiP by A1,A22,FINSEQ_5:38;
hence contradiction by A16,A40,EUCLID:52;
end;
suppose
x = Emax;
then FiP..Upper_Seq(C,n) = len Upper_Seq(C,n) by A46,A30,A24
,A43,A102,Th38;
then Emax = FiP by A30,A22,FINSEQ_5:38;
hence contradiction by A32,A40,EUCLID:52;
end;
end;
hence contradiction;
end;
suppose
A104: x in LSeg(FiP,|[Ebo,FiP`2]|);
LSeg(FiP,|[Ebo,FiP`2]|) is horizontal by A87,SPPOL_1:15;
then
A105: x`2 = FiP`2 by A104,SPPOL_1:40;
consider i be Nat such that
A106: 1 <= i and
A107: i+1 <= len RevL and
A108: x in LSeg(RevL/.i,RevL/.(i+1)) by A101,SPPOL_2:14;
A109: i < len RevL by A107,NAT_1:13;
then
A110: (Rev Lower_Seq(C,n)/.i)`1 < sr by A21,A29,A70,A106,Th52;
i in Seg (LaP..Rev Lower_Seq(C,n)) by A29,A106,A109,FINSEQ_1:1;
then
A111: RevL/.i = (Rev Lower_Seq(C,n))/.i by A27,FINSEQ_5:43;
i+1 >= 1 by NAT_1:11;
then i+1 in Seg (LaP..Rev Lower_Seq(C,n)) by A29,A107,FINSEQ_1:1;
then
A112: RevL/.(i+1) = (Rev Lower_Seq(C,n))/.(i+1) by A27,FINSEQ_5:43;
A113: FiP`1 <= x`1 by A32,A40,A63,A104,TOPREAL1:3;
now
per cases by A107,XXREAL_0:1;
suppose
A114: i+1 < len RevL;
(RevL/.i)`1 <= (RevL/.(i+1))`1 or (RevL/.(i+1))`1 <= (
RevL/.i) `1;
then
A115: x`1 <= (RevL/.(i+1))`1 or x`1 <= (RevL/.i)`1 by A108,
TOPREAL1:3;
(Rev Lower_Seq(C,n)/.(i+1))`1 < sr by A21,A29,A70,A114,Th52,
NAT_1:11;
hence contradiction by A40,A113,A111,A112,A110,A115,
XXREAL_0:2;
end;
suppose
A116: i+1 = len RevL;
then i+1 <= len Rev Lower_Seq(C,n) by A27,A29,FINSEQ_4:21;
then LSeg(Rev Lower_Seq(C,n)/.i,Rev Lower_Seq(C,n)/.(i+1))
= LSeg(Rev Lower_Seq(C,n),i) by A106,TOPREAL1:def 3;
then LSeg(RevL/.i,RevL/.(i+1)) is vertical or LSeg(RevL/.i,
RevL/.(i+1)) is horizontal by A111,A112,SPPOL_1:19;
hence contradiction by A44,A45,A66,A105,A108,A111,A110,A116,
SPPOL_1:16,40;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
suppose
A117: x in LSeg(LaP,|[sr,Nbo]|);
then
A118: LaP`2 <= x`2 by A8,A86,TOPREAL1:4;
A119: x`1 = LaP`1 by A89,A117,SPPOL_1:41;
now
per cases by A91,A84,A77,XBOOLE_0:def 3;
suppose
x in L~midU;
then consider i be Nat such that
A120: 1 <= i and
A121: i+1 <= len midU and
A122: x in LSeg(midU/.i,midU/.(i+1)) by SPPOL_2:14;
i+2 >= 1+1 by NAT_1:11;
then
A123: i+2-1 >= 1+1-1 by XREAL_1:9;
i < len midU by A121,NAT_1:13;
then i in dom midU by A120,FINSEQ_3:25;
then
A124: midU/.i = Upper_Seq(C,n)/.(i+2-'1) by A47,A23,A79,SPRECT_2:3
.= Upper_Seq(C,n)/.(i+(2-1)) by A123,XREAL_0:def 2;
i+1+2 >= 1+1 by NAT_1:11;
then
A125: i+1+2-1 >= 1+1-1 by XREAL_1:9;
A126: 1 <= i+1 by NAT_1:11;
then i+1 in dom midU by A121,FINSEQ_3:25;
then
A127: midU/.(i+1) = Upper_Seq(C,n)/.(i+1+2-'1) by A47,A23,A79,
SPRECT_2:3
.= Upper_Seq(C,n)/.(i+1+(2-1)) by A125,XREAL_0:def 2;
A128: i+1+1 <= FiP..Upper_Seq(C,n)-1+1 by A80,A121,XREAL_1:7;
then i+1 < FiP..Upper_Seq(C,n) by NAT_1:13;
then
A129: (midU/.i)`1 < sr by A21,A124,Th51,NAT_1:11;
i+1+1 <= len Upper_Seq(C,n) by A43,A128,XXREAL_0:2;
then LSeg(midU/.i,midU/.(i+1)) = LSeg(Upper_Seq(C,n),i+1) by A124
,A126,A127,TOPREAL1:def 3;
then
A130: LSeg(midU/.i,midU/.(i+1)) is vertical or LSeg(midU/.i,midU
/.(i+1)) is horizontal by SPPOL_1:19;
now
per cases by A121,XXREAL_0:1;
suppose
i+1 < len midU;
then i+1+1 <= len midU by NAT_1:13;
then i+1+1+1 <= FiP..Upper_Seq(C,n)-1+1 by A80,XREAL_1:7;
then i+1+1 < FiP..Upper_Seq(C,n) by NAT_1:13;
then
A131: (midU/.(i+1))`1 < sr by A21,A127,Th51,NAT_1:11;
(midU/.i)`1 <= (midU/.(i+1))`1 or (midU/.(i+1))`1 <= (
midU/.i) `1;
hence contradiction by A44,A119,A122,A129,A131,TOPREAL1:3;
end;
suppose
A132: i+1 = len midU;
then (midU/.i)`2 = (midU/.(i+1))`2 by A40,A77,A129,A130,
SPPOL_1:15,16;
hence contradiction by A53,A77,A118,A122,A132,GOBOARD7:6;
end;
end;
hence contradiction;
end;
suppose
x in LSeg(FiP,|[Ebo,FiP`2]|);
hence contradiction by A53,A88,A118,SPPOL_1:40;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
suppose
A133: SW = Wmin;
reconsider RevLS = Rev Lower_Seq(C,n) as special FinSequence of TOP-REAL
2;
set h = ((Rev Lower_Seq(C,n))-:LaP)^<*|[sr,Nbo]|*>;
A134: <*|[sr,Nbo]|*> is one-to-one & RevLS-:LaP is special by FINSEQ_3:93;
rng ((Rev Lower_Seq(C,n))-:LaP) misses {|[sr,Nbo]|} by A25,ZFMISC_1:50;
then rng ((Rev Lower_Seq(C,n))-:LaP) /\ {|[sr,Nbo]|} = {};
then
rng ((Rev Lower_Seq(C,n))-:LaP) /\ rng <*|[sr,Nbo]|*> = {} by FINSEQ_1:38;
then
A135: rng ((Rev Lower_Seq(C,n))-:LaP) misses rng <*|[sr,Nbo]|*>;
(((Rev Lower_Seq(C,n))-:LaP)/.len ((Rev Lower_Seq(C,n))-:LaP))`1 =
(((Rev Lower_Seq(C,n))-:LaP)/.(LaP..Rev Lower_Seq(C,n)))`1 by A27,FINSEQ_5:42
.= LaP`1 by A27,FINSEQ_5:45
.= |[sr,Nbo]|`1 by A44,EUCLID:52
.= (<*|[sr,Nbo]|*>/.1)`1 by FINSEQ_4:16;
then reconsider
h as one-to-one special FinSequence of TOP-REAL 2 by A135,A134,
FINSEQ_3:91,GOBOARD2:8;
now
let m be Nat;
A136: W-bound L~Cage(C,n) <= E-bound L~Cage(C,n) by SPRECT_1:21;
assume m in dom <*|[sr,Nbo]|*>;
then m in Seg 1 by FINSEQ_1:38;
then m = 1 by FINSEQ_1:2,TARSKI:def 1;
then
A137: <*|[sr,Nbo]|*>/.m = |[sr,Nbo]| by FINSEQ_4:16;
then (<*|[sr,Nbo]|*>/.m)`1 = sr by EUCLID:52;
hence
W-bound L~Cage(C,n) <= (<*|[sr,Nbo]|*>/.m)`1 & (<*|[sr,Nbo]|*>/.m
)`1 <= E-bound L~Cage(C,n) by A136,JORDAN6:1;
(<*|[sr,Nbo]|*>/.m)`2 = Nbo by A137,EUCLID:52;
hence
S-bound L~Cage(C,n) <= (<*|[sr,Nbo]|*>/.m)`2 & (<*|[sr,Nbo]|*>/.m
)`2 <= N-bound L~Cage(C,n) by SPRECT_1:22;
end;
then
A138: <*|[sr,Nbo]|*> is_in_the_area_of Cage(C,n) by SPRECT_2:def 1;
Rev Lower_Seq(C,n) is_in_the_area_of Cage(C,n) by JORDAN1E:18,SPRECT_3:51
;
then ((Rev Lower_Seq(C,n))-:LaP) is_in_the_area_of Cage(C,n) by A27,
JORDAN1E:1;
then
A139: h is_in_the_area_of Cage(C,n) by A138,SPRECT_2:24;
A140: len h = len ((Rev Lower_Seq(C,n))-:LaP) + 1 by FINSEQ_2:16;
then
A141: (h/.len h)`2 = |[sr,Nbo]|`2 by FINSEQ_4:67
.= N-bound L~Cage(C,n) by EUCLID:52;
L~Rev Lower_Seq(C,n) = L~RevL \/ L~((Rev Lower_Seq(C,n)):-LaP) by A27,
SPPOL_2:24;
then L~RevL c= L~Rev Lower_Seq(C,n) by XBOOLE_1:7;
then
A142: L~RevL c= L~Lower_Seq(C,n) by SPPOL_2:22;
A143: LaP`2 <= Nbo by A20,PSCOMP_1:24;
LaP..(Rev Lower_Seq(C,n)) >= 0+1 by A28,A29,NAT_1:13;
then
A144: len ((Rev Lower_Seq(C,n))-:LaP) >= 1 by A27,FINSEQ_5:42;
1 in dom h by FINSEQ_5:6;
then h/.1 = h.1 by PARTFUN1:def 6;
then (h/.1)`2 = (((Rev Lower_Seq(C,n))-:LaP)/.1)`2 by A144,FINSEQ_6:109
.= ((Rev Lower_Seq(C,n))/.1)`2 by A27,FINSEQ_5:44
.= (Lower_Seq(C,n)/.len Lower_Seq(C,n))`2 by FINSEQ_5:65
.= Wmin`2 by JORDAN1F:8
.= S-bound L~Cage(C,n) by A133,EUCLID:52;
then
A145: h is_a_v.c._for Cage(C,n) by A139,A141,SPRECT_2:def 3;
set FiP2 = First_Point(L~Lower_Seq(C,n),Wmin,Emax,Vertical_Line sr);
set midU = mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n));
A146: |[Ebo,FiP`2]|`1 = Ebo by EUCLID:52;
A147: L~g = L~midU \/ LSeg(midU/.len midU,|[Ebo,FiP`2]|) by A47,A23,SPPOL_2:19
,SPRECT_2:7;
A148: Wmin in rng Upper_Seq(C,n) by A1,FINSEQ_6:42;
now
assume FiP..Upper_Seq(C,n) = 1;
then FiP..Upper_Seq(C,n) = (Upper_Seq(C,n)/.1)..Upper_Seq(C,n) by
FINSEQ_6:43
.= Wmin..Upper_Seq(C,n) by JORDAN1F:5;
then FiP = Wmin by A22,A148,FINSEQ_5:9;
hence contradiction by A16,A40,EUCLID:52;
end;
then FiP..Upper_Seq(C,n) > 1 by A24,XXREAL_0:1;
then
A149: 1+1+0 <= FiP..Upper_Seq(C,n) by NAT_1:13;
then FiP..Upper_Seq(C,n)-2 >= 0 by XREAL_1:19;
then FiP..Upper_Seq(C,n)-'2 = FiP..Upper_Seq(C,n)-2 by XREAL_0:def 2;
then
A150: len midU = FiP..Upper_Seq(C,n)-2+1 by A43,A149,FINSEQ_6:186
.= FiP..Upper_Seq(C,n)-(2-1);
LaP`1 = |[sr,Nbo]|`1 by A44,EUCLID:52;
then
A151: LSeg(LaP,|[sr,Nbo]|) is vertical by SPPOL_1:16;
len g = len mid(Upper_Seq(C,n),2,FiP..Upper_Seq(C,n))+1 by FINSEQ_2:16;
then
A152: 1+1 <= len g by A51,XREAL_1:7;
A153: RevL/.len RevL = RevL/.(LaP..Rev Lower_Seq(C,n)) by A27,FINSEQ_5:42
.= LaP by A27,FINSEQ_5:45;
1+1 <= len h by A144,A140,XREAL_1:7;
then L~g meets L~h by A52,A145,A152,SPRECT_2:29;
then consider x be object such that
A154: x in L~g and
A155: x in L~h by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A154;
A156: L~h = L~RevL \/ LSeg(RevL/.len RevL,|[sr,Nbo]|) by A27,FINSEQ_5:47
,SPPOL_2:19;
A157: midU/.len midU = Upper_Seq(C,n)/.(FiP..Upper_Seq(C,n)) by A47,A23,
SPRECT_2:9
.= FiP by A22,FINSEQ_5:38;
A158: L~midU c= L~Upper_Seq(C,n) by A47,A23,SPRECT_3:18;
A159: L~Rev Lower_Seq(C,n) = L~Lower_Seq(C,n) & FiP2 = LaP by A12,A17,
JORDAN5C:18,SPPOL_2:22;
A160: |[Ebo,FiP`2]|`2 = FiP`2 by EUCLID:52;
then
A161: LSeg(FiP,|[Ebo,FiP`2]|) is horizontal by SPPOL_1:15;
now
per cases by A155,A156,A153,XBOOLE_0:def 3;
suppose
A162: x in L~RevL;
now
per cases by A154,A147,A157,XBOOLE_0:def 3;
suppose
A163: x in L~midU;
then x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) by A158,A142,A162,
XBOOLE_0:def 4;
then
A164: x in {Wmin,Emax} by JORDAN1E:16;
now
per cases by A164,TARSKI:def 2;
suppose
x = Wmin;
then FiP..Upper_Seq(C,n) = 1 by A46,A1,A24,A43,A163,Th37;
then Wmin = FiP by A1,A22,FINSEQ_5:38;
hence contradiction by A16,A40,EUCLID:52;
end;
suppose
x = Emax;
then FiP..Upper_Seq(C,n) = len Upper_Seq(C,n) by A46,A30,A24
,A43,A163,Th38;
then Emax = FiP by A30,A22,FINSEQ_5:38;
hence contradiction by A32,A40,EUCLID:52;
end;
end;
hence contradiction;
end;
suppose
A165: x in LSeg(FiP,|[Ebo,FiP`2]|);
LSeg(FiP,|[Ebo,FiP`2]|) is horizontal by A160,SPPOL_1:15;
then
A166: x`2 = FiP`2 by A165,SPPOL_1:40;
consider i be Nat such that
A167: 1 <= i and
A168: i+1 <= len RevL and
A169: x in LSeg(RevL/.i,RevL/.(i+1)) by A162,SPPOL_2:14;
A170: i < len RevL by A168,NAT_1:13;
then
A171: (Rev Lower_Seq(C,n)/.i)`1 < sr by A21,A29,A159,A167,Th52;
i in Seg (LaP..Rev Lower_Seq(C,n)) by A29,A167,A170,FINSEQ_1:1;
then
A172: RevL/.i = (Rev Lower_Seq(C,n))/.i by A27,FINSEQ_5:43;
i+1 >= 1 by NAT_1:11;
then i+1 in Seg (LaP..Rev Lower_Seq(C,n)) by A29,A168,FINSEQ_1:1;
then
A173: RevL/.(i+1) = (Rev Lower_Seq(C,n))/.(i+1) by A27,FINSEQ_5:43;
A174: FiP`1 <= x`1 by A32,A40,A146,A165,TOPREAL1:3;
now
per cases by A168,XXREAL_0:1;
suppose
A175: i+1 < len RevL;
(RevL/.i)`1 <= (RevL/.(i+1))`1 or (RevL/.(i+1))`1 <= (
RevL/.i) `1;
then
A176: x`1 <= (RevL/.(i+1))`1 or x`1 <= (RevL/.i)`1 by A169,
TOPREAL1:3;
(Rev Lower_Seq(C,n)/.(i+1))`1 < sr by A21,A29,A159,A175,Th52,
NAT_1:11;
hence contradiction by A40,A174,A172,A173,A171,A176,
XXREAL_0:2;
end;
suppose
A177: i+1 = len RevL;
then i+1 <= len Rev Lower_Seq(C,n) by A27,A29,FINSEQ_4:21;
then LSeg(Rev Lower_Seq(C,n)/.i,Rev Lower_Seq(C,n)/.(i+1))
= LSeg(Rev Lower_Seq(C,n),i) by A167,TOPREAL1:def 3;
then LSeg(RevL/.i,RevL/.(i+1)) is vertical or LSeg(RevL/.i,
RevL/.(i+1)) is horizontal by A172,A173,SPPOL_1:19;
hence contradiction by A44,A45,A153,A166,A169,A172,A171,A177,
SPPOL_1:16,40;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
suppose
A178: x in LSeg(LaP,|[sr,Nbo]|);
then
A179: LaP`2 <= x`2 by A8,A143,TOPREAL1:4;
A180: x`1 = LaP`1 by A151,A178,SPPOL_1:41;
now
per cases by A154,A147,A157,XBOOLE_0:def 3;
suppose
x in L~midU;
then consider i be Nat such that
A181: 1 <= i and
A182: i+1 <= len midU and
A183: x in LSeg(midU/.i,midU/.(i+1)) by SPPOL_2:14;
i+2 >= 1+1 by NAT_1:11;
then
A184: i+2-1 >= 1+1-1 by XREAL_1:9;
i < len midU by A182,NAT_1:13;
then i in dom midU by A181,FINSEQ_3:25;
then
A185: midU/.i = Upper_Seq(C,n)/.(i+2-'1) by A47,A23,A149,SPRECT_2:3
.= Upper_Seq(C,n)/.(i+(2-1)) by A184,XREAL_0:def 2;
i+1+2 >= 1+1 by NAT_1:11;
then
A186: i+1+2-1 >= 1+1-1 by XREAL_1:9;
A187: 1 <= i+1 by NAT_1:11;
then i+1 in dom midU by A182,FINSEQ_3:25;
then
A188: midU/.(i+1) = Upper_Seq(C,n)/.(i+1+2-'1) by A47,A23,A149,
SPRECT_2:3
.= Upper_Seq(C,n)/.(i+1+(2-1)) by A186,XREAL_0:def 2;
A189: i+1+1 <= FiP..Upper_Seq(C,n)-1+1 by A150,A182,XREAL_1:7;
then i+1 < FiP..Upper_Seq(C,n) by NAT_1:13;
then
A190: (midU/.i)`1 < sr by A21,A185,Th51,NAT_1:11;
i+1+1 <= len Upper_Seq(C,n) by A43,A189,XXREAL_0:2;
then LSeg(midU/.i,midU/.(i+1)) = LSeg(Upper_Seq(C,n),i+1) by A185
,A187,A188,TOPREAL1:def 3;
then
A191: LSeg(midU/.i,midU/.(i+1)) is vertical or LSeg(midU/.i,midU
/.(i+1)) is horizontal by SPPOL_1:19;
now
per cases by A182,XXREAL_0:1;
suppose
i+1 < len midU;
then i+1+1 <= len midU by NAT_1:13;
then i+1+1+1 <= FiP..Upper_Seq(C,n)-1+1 by A150,XREAL_1:7;
then i+1+1 < FiP..Upper_Seq(C,n) by NAT_1:13;
then
A192: (midU/.(i+1))`1 < sr by A21,A188,Th51,NAT_1:11;
(midU/.i)`1 <= (midU/.(i+1))`1 or (midU/.(i+1))`1 <= (
midU/.i) `1;
hence contradiction by A44,A180,A183,A190,A192,TOPREAL1:3;
end;
suppose
A193: i+1 = len midU;
then (midU/.i)`2 = (midU/.(i+1))`2 by A40,A157,A190,A191,
SPPOL_1:15,16;
hence contradiction by A53,A157,A179,A183,A193,GOBOARD7:6;
end;
end;
hence contradiction;
end;
suppose
x in LSeg(FiP,|[Ebo,FiP`2]|);
hence contradiction by A53,A161,A179,SPPOL_1:40;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
theorem Th55:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for n be Nat st n > 0 holds L~Upper_Seq(C,n) = Upper_Arc
L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
A1: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A2: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_6:90
,SPRECT_2:43;
A3: 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 Upper_Seq(C,n)/.1 = Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by A2,
FINSEQ_5:44;
then
A4: Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by A1,FINSEQ_6:92;
Upper_Seq(C,n)/.len Upper_Seq(C,n) = (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 A3,A2,FINSEQ_5:42
.= E-max L~Cage(C,n) by A2,FINSEQ_5:45;
then
A5: L~Upper_Seq(C,n) is_an_arc_of W-min L~Cage(C,n),E-max L~Cage(C,n) by A4,
TOPREAL1:25;
assume n > 0;
then
A6: First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n),
Vertical_Line((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))`2 > Last_Point(L~
Lower_Seq(C,n),E-max L~Cage(C,n),W-min L~Cage(C,n), Vertical_Line((W-bound L~
Cage(C,n)+E-bound L~Cage(C,n))/2))`2 by Th54;
A7: 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:53;
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
Lower_Seq(C,n)/.len Lower_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n)
)/. (len Rotate(Cage(C,n),W-min L~Cage(C,n))) by A2,FINSEQ_5:54
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by FINSEQ_6:def 1
.= W-min L~Cage(C,n) by A1,FINSEQ_6:92;
then
A8: L~Lower_Seq(C,n) is_an_arc_of E-max L~Cage(C,n),W-min L~Cage(C,n) by A7,
TOPREAL1:25;
L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) = {W-min L~Cage(C,n),E-max L~Cage(
C,n)} & L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n) = L~Cage(C,n) by JORDAN1E:13,16;
hence thesis by A5,A8,A6,JORDAN6:def 8;
end;
theorem Th56:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for n be Nat st n > 0 holds L~Lower_Seq(C,n) = Lower_Arc
L~Cage(C,n)
proof
let C be compact connected 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:43;
A2: 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:53;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
Lower_Seq(C,n)=Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n) &
E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_6:90
,JORDAN1E:def 2,SPRECT_2:43;
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 FINSEQ_5:54
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by FINSEQ_6:def 1
.= W-min L~Cage(C,n) by A1,FINSEQ_6:92;
then
A3: L~Lower_Seq(C,n) is_an_arc_of E-max L~Cage(C,n),W-min L~Cage(C,n) by A2,
TOPREAL1:25;
assume n > 0;
then
A4: L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) & First_Point(L~Upper_Seq(C,n),
W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line((W-bound L~Cage(C,n)+E-bound
L~Cage(C,n))/2))`2 > Last_Point(L~Lower_Seq(C,n),E-max L~Cage(C,n),W-min L~Cage
(C,n), Vertical_Line((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))`2 by Th54
,Th55;
L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) = {W-min L~Cage(C,n),E-max L~Cage(C
,n)} & L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n) = L~Cage(C,n) by JORDAN1E:13,16;
hence thesis by A3,A4,JORDAN6:def 9;
end;
theorem
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for n be Nat st n > 0 for i,j be Nat st 1 <= i
& i <= len Gauge(C,n) & 1 <= j & j <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~
Cage(C,n) holds LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,j)) meets Lower_Arc L~Cage(
C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
assume n > 0;
then
A1: L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) by Th56;
let i,j be Nat;
assume 1 <= i & i <= len Gauge(C,n) & 1 <= j & j <= width Gauge(C,n) &
Gauge( C,n)*(i,j) in L~Cage(C,n);
hence thesis by A1,Th46;
end;