:: On the components of the complement of a special polygonal curve
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received January 21, 1999
:: Copyright (c) 1999-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, SPPOL_2, RCOMP_1, EUCLID, TOPREAL1, XBOOLE_0,
PARTFUN1, JORDAN3, JORDAN5C, FINSEQ_1, XXREAL_0, ARYTM_3, GROUP_2,
RELAT_1, TARSKI, PRE_TOPC, FUNCT_1, ARYTM_1, RLTOPSP1, ORDINAL4,
SPRECT_2, GOBOARD5, PSCOMP_1, GOBOARD9, SPRECT_1, GOBOARD2, TREES_1,
MATRIX_1, TOPS_1, MCART_1, TOPREAL4, SPPOL_1, FINSEQ_5, FINSEQ_4,
FINSEQ_6, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, REAL_1,
NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, MATRIX_0, STRUCT_0,
PRE_TOPC, TOPS_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL4,
FINSEQ_5, FINSEQ_6, GOBOARD2, SPPOL_1, SPPOL_2, GOBOARD5, GOBOARD9,
JORDAN3, PSCOMP_1, JORDAN5C, SPRECT_1, SPRECT_2, XXREAL_0;
constructors REAL_1, FINSEQ_4, TOPS_1, TOPS_2, COMPTS_1, TOPMETR, TOPREAL4,
GOBOARD2, SPPOL_1, PSCOMP_1, GOBOARD9, JORDAN3, JORDAN5C, SPRECT_1,
SPRECT_2, GOBOARD1, NAT_D, MATRIX_1;
registrations XBOOLE_0, RELSET_1, MEMBERED, FINSEQ_6, STRUCT_0, COMPTS_1,
TOPREAL1, GOBOARD2, SPPOL_2, GOBOARD9, SPRECT_1, SPRECT_3, REVROT_1,
FUNCT_1, EUCLID, ZFMISC_1, XREAL_0, NAT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities PSCOMP_1, RLTOPSP1;
theorems TOPREAL1, JORDAN5C, JORDAN3, FINSEQ_3, SPPOL_2, TOPS_1, SPPOL_1,
TOPREAL3, FINSEQ_5, NAT_1, SPRECT_1, JORDAN5B, SPRECT_2, GOBOARD5,
FINSEQ_4, GOBOARD7, GOBOARD6, GOBOARD9, ZFMISC_1, TOPREAL4, PSCOMP_1,
JORDAN4, FINSEQ_6, FINSEQ_1, TARSKI, EUCLID, SUBSET_1, JORDAN5D,
SPRECT_3, REVROT_1, PARTFUN2, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0,
PARTFUN1, CARD_1, NAT_D, RLTOPSP1, MATRIX_0, RLVECT_1;
begin
reserve i,j,l for Nat;
theorem Th1:
for f being S-Sequence_in_R2, Q being closed Subset of TOP-REAL 2
st L~f meets Q & not f/.1 in Q holds 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) }
proof
let f be S-Sequence_in_R2, Q be closed Subset of TOP-REAL 2 such that
A1: L~f meets Q and
A2: not f/.1 in Q;
set p1 = f/.1, p2 = f/.len f, fp = First_Point(L~f,p1,p2,Q);
A3: L~f /\ Q is closed by TOPS_1:8;
len f >= 1+1 by TOPREAL1:def 8;
then
A4: len f > 1 by NAT_1:13; then
AA: 1 in dom f by FINSEQ_3:25;
L~f is_an_arc_of p1,p2 by TOPREAL1:25;
then
A5: fp in L~f /\ Q by A1,A3,JORDAN5C:def 1;
then
A6: fp in L~f by XBOOLE_0:def 4;
then
A7: 1<=Index(fp,f) by JORDAN3:8;
A8: Index(fp,f)<=len f by A6,JORDAN3:8;
then
A9: Index(fp,f) in dom f by A7,FINSEQ_3:25;
A10: now
assume not L~R_Cut(f,fp) /\ Q c= { fp };
then consider q being object such that
A11: q in L~R_Cut(f,fp) /\ Q and
A12: not q in { fp } by TARSKI:def 3;
reconsider q as Point of TOP-REAL 2 by A11;
A13: q in L~R_Cut(f,fp) by A11,XBOOLE_0:def 4;
A14: L~R_Cut(f,fp) c= L~f by A6,JORDAN3:41;
A15: q <> fp by A12,TARSKI:def 1;
q in Q by A11,XBOOLE_0:def 4;
then
A16: LE fp, q, L~f, p1, p2 by A3,A13,A14,JORDAN5C:15;
per cases;
suppose
A17: fp = f.1;
A18: len<*fp*> = 1 by FINSEQ_1:39;
q in L~<*fp*> by A13,A17,JORDAN3:def 4;
hence contradiction by A18,TOPREAL1:22;
end;
suppose
A19: fp <> f.1;
set m = mid(f,1,Index(fp,f));
A20: Index(fp,f) < len f by A6,JORDAN3:8;
len m = Index(fp,f)-'1+1 by A7,A8,FINSEQ_6:186;
then
A21: m is non empty by CARD_1:27;
A22: fp in LSeg(f,Index(fp,f)) by A6,JORDAN3:9;
q in L~(m^<*fp*>) by A13,A19,JORDAN3:def 4;
then
A23: q in L~m \/ LSeg(m/.len m,fp) by A21,SPPOL_2:19;
now
per cases by A23,XBOOLE_0:def 3;
suppose
A24: q in L~m;
A25: now
assume Index(fp,f) <= 1;
then Index(fp,f) = 1 by A7,XXREAL_0:1;
then len m = 1 by AA,FINSEQ_6:193;
hence contradiction by A24,TOPREAL1:22;
end;
then
A26: LE q, f/.Index(fp,f), L~f, p1, p2 by A8,A24,SPRECT_3:17;
f/.Index(fp,f) in LSeg(f/.Index(fp,f),fp) by RLTOPSP1:68;
then LE f/.Index(fp,f), fp, L~f, p1, p2 by A20,A22,A25,SPRECT_3:23;
then LE q, fp, L~f, p1, p2 by A26,JORDAN5C:13;
hence contradiction by A15,A16,JORDAN5C:12,TOPREAL1:25;
end;
suppose
A27: q in LSeg(m/.len m,fp);
len m in dom m by A21,FINSEQ_5:6;
then m/.len m = m.len m by PARTFUN1:def 6
.= f.Index(fp,f) by A7,A8,FINSEQ_6:188
.= f/.Index(fp,f) by A9,PARTFUN1:def 6;
then LE q, fp, L~f, p1, p2 by A7,A20,A22,A27,SPRECT_3:23;
hence contradiction by A15,A16,JORDAN5C:12,TOPREAL1:25;
end;
end;
hence contradiction;
end;
end;
A28: fp in Q by A5,XBOOLE_0:def 4;
1 in dom f by A4,FINSEQ_3:25;
then fp <> f.1 by A2,A28,PARTFUN1:def 6;
then fp in L~R_Cut(f,fp) by A6,JORDAN5B:20;
then fp in L~R_Cut(f,fp) /\ Q by A28,XBOOLE_0:def 4;
hence thesis by A10,ZFMISC_1:33;
end;
theorem
for f being non empty FinSequence of TOP-REAL 2, p being Point of
TOP-REAL 2 st f is being_S-Seq & p = f/.len f holds L~L_Cut (f,p) = {}
proof
let f be non empty FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: f is being_S-Seq and
A2: p = f/.len f;
len f >= 2 by A1,TOPREAL1:def 8;
then len f >= 1 by XXREAL_0:2;
then len f in dom f by FINSEQ_3:25;
then p = f.len f by A2,PARTFUN1:def 6;
then L_Cut (f,p) = <*p*> by A1,JORDAN5B:17;
then len L_Cut (f,p) = 1 by FINSEQ_1:39;
hence thesis by TOPREAL1:22;
end;
theorem Th3:
for f being S-Sequence_in_R2, p being Point of TOP-REAL 2, j st 1
<=j & j < len f & p in L~mid(f,j,len f) holds LE f/.j, p, L~f, f/.1, f/.len f
proof
let f be S-Sequence_in_R2, p be Point of TOP-REAL 2, j such that
A1: 1 <=j and
A2: j < len f and
A3: p in L~mid(f,j,len f);
consider i such that
A4: 1 <= i and
A5: i+1 <= len mid(f,j,len f) and
A6: p in LSeg(mid(f,j,len f),i) by A3,SPPOL_2:13;
A7: len mid(f,j,len f)=len f-'j+1 by A1,A2,FINSEQ_6:186;
then i <= len f -' j by A5,XREAL_1:6;
then
A8: i + j <= len f by A2,NAT_D:54;
j+i >= i by NAT_1:11;
then
A9: j+i-'1+1 <= len f by A4,A8,XREAL_1:235,XXREAL_0:2;
1+1 <= j+i by A1,A4,XREAL_1:7;
then
A10: 1 <= j+i-'1 by NAT_D:49;
j+1 <= j+i by A4,XREAL_1:6;
then
A11: j <= j+i-'1 by NAT_D:49;
j+i-'1+1 >= j+i-'1 by NAT_1:11;
then len f >= j+i-'1 by A9,XXREAL_0:2;
then
A12: LE f/.j, f/.(j+i-'1), L~f, f/.1, f/.len f by A1,A11,JORDAN5C:24;
i<len f-'j+1 by A5,A7,NAT_1:13;
then p in LSeg(f,j+i-'1) by A1,A2,A4,A6,JORDAN4:19;
then LE f/.(j+i-'1), p, L~f, f/.1, f/.len f by A10,A9,JORDAN5C:25;
hence thesis by A12,JORDAN5C:13;
end;
theorem Th4:
for f being S-Sequence_in_R2, p,q being Point of TOP-REAL 2, j st
1 <=j & j < len f & p in LSeg(f,j) & q in LSeg(p,f/.(j+1)) holds LE p, q, L~f,
f/.1, f/.len f
proof
let f be S-Sequence_in_R2, p,q be Point of TOP-REAL 2, j such that
A1: 1 <=j and
A2: j < len f and
A3: p in LSeg(f,j) and
A4: q in LSeg(p,f/.(j+1));
A5: j+1 <= len f by A2,NAT_1:13;
then
A6: LSeg(f,j) = LSeg(f/.j,f/.(j+1)) by A1,TOPREAL1:def 3;
A7: f/.(j+1) in LSeg(f,j) by A1,A5,TOPREAL1:21;
then
A8: LSeg(p,f/.(j+1)) c= LSeg(f,j) by A3,A6,TOPREAL1:6;
then
A9: q in LSeg(f,j) by A4;
A10: LSeg(f,j) c= L~f by TOPREAL3:19;
per cases;
suppose
p = q;
hence thesis by A3,A10,JORDAN5C:9;
end;
suppose
A11: q <> p;
for i, j being Nat st p in LSeg(f,i) & q in LSeg(f,j) & 1
<= i & i+1 <= len f & 1 <= j & j+1 <= len f holds i <= j & (i = j implies LE p,
q,f/.i,f/.(i+1))
proof
1 <= j+1 by NAT_1:11;
then
A12: j+1 in dom f by A5,FINSEQ_3:25;
let i1, i2 be Nat such that
A13: p in LSeg(f,i1) and
A14: q in LSeg(f,i2) and
1 <= i1 and
A15: i1+1 <= len f and
A16: 1 <= i2 and
i2+1 <= len f;
A17: p in LSeg(f,i1) /\ LSeg(f,j) by A3,A13,XBOOLE_0:def 4;
then
A18: LSeg(f,i1) meets LSeg(f,j) by XBOOLE_0:4;
then
A19: i1 + 1 >= j by TOPREAL1:def 7;
A20: now
A21: j+(1+1) = j+1+1;
assume j + 1 = i1;
then p in {f/.(j+1)} by A1,A15,A17,A21,TOPREAL1:def 6;
then p = f/.(j+1) by TARSKI:def 1;
then q in {p} by A4,RLTOPSP1:70;
hence contradiction by A11,TARSKI:def 1;
end;
A22: now
assume that
A23: i2 + 1 > j and
A24: j+1 > i2;
A25: j <= i2 by A23,NAT_1:13;
i2 <= j by A24,NAT_1:13;
hence i2 = j by A25,XXREAL_0:1;
end;
A26: now
assume that
A27: i1 + 1 > j and
A28: j+1 > i1;
A29: j <= i1 by A27,NAT_1:13;
i1 <= j by A28,NAT_1:13;
hence i1 = j by A29,XXREAL_0:1;
end;
A30: q in LSeg(f,i2) /\ LSeg(f,j) by A4,A8,A14,XBOOLE_0:def 4;
then
A31: LSeg(f,i2) meets LSeg(f,j) by XBOOLE_0:4;
then
A32: j + 1 >= i2 by TOPREAL1:def 7;
A33: j in dom f by A1,A2,FINSEQ_3:25;
A34: now
assume f/.(j+1)=f/.j;
then j = j+1 by A12,A33,PARTFUN2:10;
hence contradiction;
end;
A35: now
A36: i2+(1+1) = i2+1+1;
assume i2+1 = j;
then q in {f/.j} by A5,A16,A30,A36,TOPREAL1:def 6;
then q = f/.j by TARSKI:def 1;
hence contradiction by A3,A4,A6,A7,A11,A34,SPPOL_1:7,TOPREAL1:6;
end;
i2 + 1 >= j by A31,TOPREAL1:def 7;
then i2 + 1 = j or i2 = j or j + 1 = i2 by A22,A32,XXREAL_0:1;
then
A37: i2 >= j by A35,NAT_1:11;
A38: j + 1 >= i1 by A18,TOPREAL1:def 7;
then i1 + 1 = j or i1 = j by A26,A19,A20,XXREAL_0:1;
then i1 <= j by NAT_1:11;
hence i1 <= i2 by A37,XXREAL_0:2;
assume
A39: i1 = i2;
not p in LSeg(q,f/.(j+1)) by A4,A11,SPRECT_3:6;
then not LE q,p,f/.j,f/.(j+1) by JORDAN3:30;
then LT p,q,f/.j,f/.(j+1) by A3,A6,A14,A26,A19,A38,A20,A34,A35,A39,
JORDAN3:28,XXREAL_0:1;
hence thesis by A26,A19,A38,A20,A35,A39,JORDAN3:def 6,XXREAL_0:1;
end;
hence thesis by A3,A9,A10,A11,JORDAN5C:30;
end;
end;
theorem Th5:
for f being S-Sequence_in_R2, Q being closed Subset of TOP-REAL 2
st L~f meets Q & not f/.len f in Q holds L~L_Cut(f,Last_Point(L~f,f/.1,f/.len f
,Q)) /\ Q = { Last_Point(L~f,f/.1,f/.len f,Q) }
proof
let f be S-Sequence_in_R2, Q be closed Subset of TOP-REAL 2 such that
A1: L~f meets Q and
A2: not f/.len f in Q;
set p1 = f/.1, p2 = f/.len f, lp = Last_Point(L~f,p1,p2,Q);
A3: L~f /\ Q is closed by TOPS_1:8;
len f >= 1+1 by TOPREAL1:def 8;
then
A4: len f > 1 by NAT_1:13; then
AA: len f in dom f by FINSEQ_3:25;
L~f is_an_arc_of p1,p2 by TOPREAL1:25;
then
A5: lp in L~f /\ Q by A1,A3,JORDAN5C:def 2;
then
A6: lp in L~f by XBOOLE_0:def 4;
then
A7: 1<=Index(lp,f) by JORDAN3:8;
A8: now
set m = mid(f,Index(lp,f)+1,len f);
assume not L~L_Cut(f,lp) /\ Q c= { lp };
then consider q being object such that
A9: q in L~L_Cut(f,lp) /\ Q and
A10: not q in { lp } by TARSKI:def 3;
reconsider q as Point of TOP-REAL 2 by A9;
A11: q in L~L_Cut(f,lp) by A9,XBOOLE_0:def 4;
A12: L~L_Cut(f,lp) c= L~f by A6,JORDAN3:42;
A13: Index(lp,f) < len f by A6,JORDAN3:8;
then
A14: Index(lp,f)+1 <= len f by NAT_1:13;
A15: 1 <= Index(lp,f)+1 by NAT_1:11;
then len m = len f -' (Index(lp,f)+1)+1 by A14,FINSEQ_6:186;
then
A16: m is non empty by CARD_1:27;
A17: q <> lp by A10,TARSKI:def 1;
q in Q by A9,XBOOLE_0:def 4;
then
A18: LE q, lp, L~f, p1, p2 by A3,A11,A12,JORDAN5C:16;
per cases;
suppose
lp=f.(Index(lp,f)+1);
then
A19: q in L~m by A11,JORDAN3:def 3;
now
assume Index(lp,f)+1 >= len f;
then Index(lp,f)+1 = len f by A14,XXREAL_0:1;
then len m = 1 by AA,FINSEQ_6:193;
hence contradiction by A19,TOPREAL1:22;
end;
then
A20: LE f/.(Index(lp,f)+1), q, L~f, f/.1, f/.len f by A19,Th3,NAT_1:11;
A21: f/.(Index(lp,f)+1) in LSeg(lp,f/.(Index(lp,f)+1)) by RLTOPSP1:68;
lp in LSeg(f,Index(lp,f)) by A6,JORDAN3:9;
then LE lp, f/.(Index(lp,f)+1), L~f, p1, p2 by A7,A13,A21,Th4;
then LE lp, q, L~f, p1, p2 by A20,JORDAN5C:13;
hence contradiction by A17,A18,JORDAN5C:12,TOPREAL1:25;
end;
suppose
A22: lp<>f.(Index(lp,f)+1);
A23: lp in LSeg(f,Index(lp,f)) by A6,JORDAN3:9;
1 <= Index(lp,f)+1 by NAT_1:11;
then
A24: Index(lp,f)+1 in dom f by A14,FINSEQ_3:25;
q in L~(<*lp*>^m) by A11,A22,JORDAN3:def 3;
then
A25: q in L~m \/ LSeg(m/.1,lp) by A16,SPPOL_2:20;
now
per cases by A25,XBOOLE_0:def 3;
suppose
A26: q in L~m;
now
assume Index(lp,f)+1 >= len f;
then Index(lp,f)+1 = len f by A14,XXREAL_0:1;
then len m = 1 by AA,FINSEQ_6:193;
hence contradiction by A26,TOPREAL1:22;
end;
then
A27: LE f/.(Index(lp,f)+1), q, L~f, f/.1, f/.len f by A26,Th3,NAT_1:11;
f/.(Index(lp,f)+1) in LSeg(lp,f/.(Index(lp,f)+1)) by RLTOPSP1:68;
then LE lp, f/.(Index(lp,f)+1), L~f, p1, p2 by A7,A13,A23,Th4;
then LE lp, q, L~f, p1, p2 by A27,JORDAN5C:13;
hence contradiction by A17,A18,JORDAN5C:12,TOPREAL1:25;
end;
suppose
A28: q in LSeg(lp,m/.1);
1 in dom m by A16,FINSEQ_5:6;
then m/.1 = m.1 by PARTFUN1:def 6
.= f.(Index(lp,f)+1) by A4,A14,A15,FINSEQ_6:118
.= f/.(Index(lp,f)+1) by A24,PARTFUN1:def 6;
then LE lp, q, L~f, p1, p2 by A7,A13,A23,A28,Th4;
hence contradiction by A17,A18,JORDAN5C:12,TOPREAL1:25;
end;
end;
hence contradiction;
end;
end;
A29: lp in Q by A5,XBOOLE_0:def 4;
len f in dom f by A4,FINSEQ_3:25;
then lp <> f.len f by A2,A29,PARTFUN1:def 6;
then lp in L~L_Cut(f,lp) by A6,JORDAN5B:19;
then lp in L~L_Cut(f,lp) /\ Q by A29,XBOOLE_0:def 4;
hence thesis by A8,ZFMISC_1:33;
end;
reserve q for Point of TOP-REAL 2;
Lm1: for f being clockwise_oriented non constant standard
special_circular_sequence st f/.1 = N-min L~f holds LeftComp f <> RightComp f
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
set A = N-min L~f;
assume that
A1: f/.1 = A and
A2: LeftComp f = RightComp f;
A3: LeftComp SpStSeq L~f c= LeftComp f by A1,SPRECT_3:41;
consider i such that
A4: 1 <= i and
A5: i < len GoB f and
A6: A = (GoB f)*(i,width GoB f) by SPRECT_3:28;
set w = width GoB f;
A7: len f > 4 by GOBOARD7:34;
A8: 1+1 <= len f by GOBOARD7:34,XXREAL_0:2;
A9: w > 1 by GOBOARD7:33;
then
A10: w-'1+1 = w by XREAL_1:235;
A11: [i,w] in Indices GoB f by A4,A5,A9,MATRIX_0:30;
A12: 1 <= i+1 by NAT_1:11;
A13: i+1 <= len GoB f by A5,NAT_1:13;
then
A14: [i+1,w] in Indices GoB f by A9,A12,MATRIX_0:30;
A15: 1 in dom f by FINSEQ_5:6;
A16: i in dom GoB f by A4,A5,FINSEQ_3:25;
then
A17: f/.(1+1) = (GoB f)*(i+1,w) by A1,A6,SPRECT_3:29;
then
A18: right_cell(f,1) = cell(GoB f,i,w-'1) by A1,A6,A8,A10,A11,A14,GOBOARD5:28;
set z2 = 1/2*((GoB f)*(i,w-'1)+(GoB f)*(i+1,w)), p1 = 1/2*((GoB f)*(i,w)+(
GoB f)*(i+1,w)), p2 = 1/2*((GoB f)*(i,w-'1)+(GoB f)*(i,w));
A19: 1 <= w-'1 by GOBOARD7:33,NAT_D:49;
then
A20: z2 in Int cell(GoB f,i,w-'1) by A4,A10,A13,GOBOARD6:31;
A21: Int right_cell(f,1) c= RightComp f by A8,GOBOARD9:25;
A22: W-bound L~SpStSeq L~f = W-bound L~f by SPRECT_1:58;
A23: S-bound L~SpStSeq L~f = S-bound L~f by SPRECT_1:59;
A24: N-bound L~SpStSeq L~f = N-bound L~f by SPRECT_1:60;
A25: E-bound L~SpStSeq L~f = E-bound L~f by SPRECT_1:61;
A26: 1 < i+1 by A4,NAT_1:13;
A27: 1 <= len GoB f by A4,A5,XXREAL_0:2;
A28: w-'1 < w by A10,XREAL_1:29;
A29: z2 = 1/2*(A+(GoB f)*(i+1,w-'1)) by A4,A6,A10,A13,A19,GOBOARD7:9;
then
A30: z2`1 = 1/2*(A+(GoB f)*(i+1,w-'1))`1 by TOPREAL3:4
.= 1/2*(A`1+(GoB f)*(i+1,w-'1)`1) by TOPREAL3:2
.= 1/2*A`1+1/2*((GoB f)*(i+1,w-'1))`1;
A31: z2`2 = 1/2*(A+(GoB f)*(i+1,w-'1))`2 by A29,TOPREAL3:4
.= 1/2*(A`2+(GoB f)*(i+1,w-'1)`2) by TOPREAL3:2
.= 1/2*(N-bound L~f+(GoB f)*(i+1,w-'1)`2) by EUCLID:52
.= 1/2*N-bound L~f+1/2*((GoB f)*(i+1,w-'1))`2;
A32: 1/2*(W-bound L~f) + 1/2*(W-bound L~f) = (W-bound L~f);
A33: 1/2*(S-bound L~f) + 1/2*(S-bound L~f) = (S-bound L~f);
A34: 1/2*(N-bound L~f) + 1/2*(N-bound L~f) = N-bound L~f;
A35: 1/2*(E-bound L~f) + 1/2*(E-bound L~f) = (E-bound L~f);
N-min L~f in L~f by SPRECT_1:11;
then A`1 >= W-bound L~f by PSCOMP_1:24;
then
A36: 1/2*A`1 >= 1/2*W-bound L~f by XREAL_1:64;
A37: (GoB f)*(1,w-'1)`1 = (GoB f)*(1,1)`1 by A19,A27,A28,GOBOARD5:2;
(GoB f)*(i+1,w-'1)`1 > (GoB f)*(1,w-'1)`1 by A13,A19,A26,A28,GOBOARD5:3;
then (GoB f)*(i+1,w-'1)`1 > W-bound L~f by A37,JORDAN5D:37;
then 1/2*((GoB f)*(i+1,w-'1))`1 > 1/2*W-bound L~f by XREAL_1:68;
then
A38: W-bound L~SpStSeq L~f < z2`1 by A22,A30,A32,A36,XREAL_1:8;
N-max L~f in L~f by SPRECT_1:11;
then (N-max L~f)`1 <= E-bound L~f by PSCOMP_1:24;
then A`1 < E-bound L~f by SPRECT_2:51,XXREAL_0:2;
then
A39: 1/2*A`1 < 1/2*E-bound L~f by XREAL_1:68;
A40: (GoB f)*(len GoB f,w-'1)`1 = (GoB f)*(len GoB f,1)`1 by A19,A27,A28,
GOBOARD5:2;
(GoB f)*(i+1,w-'1)`1 <= (GoB f)*(len GoB f,w-'1)`1 by A12,A13,A19,A28,
SPRECT_3:13;
then (GoB f)*(i+1,w-'1)`1 <= E-bound L~f by A40,JORDAN5D:39;
then 1/2*((GoB f)*(i+1,w-'1))`1 <= 1/2*E-bound L~f by XREAL_1:64;
then
A41: z2`1 < E-bound L~SpStSeq L~f by A25,A30,A35,A39,XREAL_1:8;
A42: 1/2*N-bound L~f > 1/2*S-bound L~f by SPRECT_1:32,XREAL_1:68;
A43: (GoB f)*(i+1,1)`2 = (GoB f)*(1,1)`2 by A9,A12,A13,GOBOARD5:1;
(GoB f)*(i+1,w-'1)`2 >= (GoB f)*(i+1,1)`2 by A12,A13,A19,A28,SPRECT_3:12;
then (GoB f)*(i+1,w-'1)`2 >= S-bound L~f by A43,JORDAN5D:38;
then 1/2*((GoB f)*(i+1,w-'1))`2 >= 1/2*S-bound L~f by XREAL_1:64;
then
A44: S-bound L~SpStSeq L~f < z2`2 by A23,A31,A33,A42,XREAL_1:8;
A45: (GoB f)*(i+1,w)`2 = (GoB f)*(1,width GoB f)`2 by A9,A12,A13,GOBOARD5:1;
(GoB f)*(i+1,w-'1)`2 < (GoB f)*(i+1,w)`2 by A12,A13,A19,A28,GOBOARD5:4;
then (GoB f)*(i+1,w-'1)`2 < N-bound L~f by A45,JORDAN5D:40;
then 1/2*((GoB f)*(i+1,w-'1))`2 < 1/2*N-bound L~f by XREAL_1:68;
then
A46: z2`2 < N-bound L~SpStSeq L~f by A24,A31,A34,XREAL_1:6;
RightComp SpStSeq L~f = {q : W-bound L~SpStSeq L~f < q`1 & q`1 <
E-bound L~SpStSeq L~f & S-bound L~SpStSeq L~f < q`2 & q`2 < N-bound L~SpStSeq
L~f} by SPRECT_3:37;
then
A47: z2 in RightComp SpStSeq L~f by A38,A41,A44,A46;
consider z1 being object such that
A48: z1 in LeftComp SpStSeq L~f by XBOOLE_0:def 1;
LeftComp SpStSeq L~f misses RightComp SpStSeq L~f by SPRECT_1:88;
then
A49: z1 <> z2 by A47,A48,XBOOLE_0:3;
reconsider z1 as Point of TOP-REAL 2 by A48;
consider P being Subset of TOP-REAL 2 such that
A50: P is_S-P_arc_joining z1,z2 and
A51: P c= RightComp f by A2,A3,A18,A20,A21,A48,A49,TOPREAL4:29;
consider Red9 being FinSequence of TOP-REAL 2 such that
A52: Red9 is being_S-Seq and
A53: P = L~Red9 and
A54: z1 = Red9/.1 and
A55: z2 = Red9/.len Red9 by A50,TOPREAL4:def 1;
A56: L~SpStSeq L~f meets L~Red9 by A47,A48,A52,A54,A55,SPRECT_3:33;
A57: 2 in dom f by A8,FINSEQ_3:25;
A58: len f in dom f by FINSEQ_5:6;
A59: len f -' 1 >= 1 by A8,NAT_D:49;
len f -' 1 <= len f by NAT_D:44;
then
A60: len f -' 1 in dom f by A59,FINSEQ_3:25;
1 <= len f by A58,FINSEQ_3:25;
then
A61: len f -' 1 + 1 = len f by XREAL_1:235;
then
A62: len f -' 1 < len f by NAT_1:13;
A63: <*NW-corner L~f*> is_in_the_area_of f by SPRECT_2:26;
A64: w-'1 < width GoB f by A10,NAT_1:13;
then Int cell(GoB f,i,w-'1) misses L~SpStSeq L~f by A4,A5,A19,SPRECT_3:55;
then
A65: not z2 in L~SpStSeq L~f by A20,XBOOLE_0:3;
A66: LSeg(NW-corner L~f,NE-corner L~f) c= L~SpStSeq L~f by SPRECT_3:14;
A67: f/.1 = f/.len f by FINSEQ_6:def 1;
A68: NW-corner L~f in LSeg(NW-corner L~f,NE-corner L~f) by RLTOPSP1:68;
A69: N-min L~f in LSeg(NW-corner L~f,NE-corner L~f) by SPRECT_3:15;
then
A70: LSeg(NW-corner L~f,N-min L~f) c= LSeg(NW-corner L~f,NE-corner L~f ) by A68
,TOPREAL1:6;
A71: LSeg(NW-corner L~f,N-min L~f) is horizontal by A70,SPRECT_1:9;
1 + 2 <= len f by GOBOARD7:34,XXREAL_0:2;
then
A72: LSeg(f,1) /\ LSeg(f,1+1) = {f/.(1+1)} by TOPREAL1:def 6;
len f >= 2 + 1 by GOBOARD7:34,XXREAL_0:2;
then len f -' 1 >= 1 + 1 by NAT_D:49;
then len f -' 1 -' 1 >= 1 by NAT_D:49;
then
A73: len f -' 2 >= 1 by NAT_D:45;
A74: len f -' 2 + 1 = len f -' 1 -' 1 + 1 by NAT_D:45
.= len f -' 1 by A59,XREAL_1:235;
len f -' 2 + 2 = len f by A7,XREAL_1:235,XXREAL_0:2;
then
A75: LSeg(f,len f -' 1) /\ LSeg(f,len f -' 2) = {f/.(len f -' 1)} by A73,A74,
TOPREAL1:def 6;
A76: f/.2 in N-most L~f by A1,SPRECT_2:30;
N-most L~f c= LSeg(NW-corner L~f,NE-corner L~f) by XBOOLE_1:17;
then
A77: LSeg(f/.1, f/.2) c= LSeg(NW-corner L~f,NE-corner L~f) by A1,A69,A76,
TOPREAL1:6;
A78: ((GoB f)*(i,w-'1))`1 = ((GoB f)*(i,1))`1 by A4,A5,A19,A64,GOBOARD5:2
.= A`1 by A4,A5,A6,A9,GOBOARD5:2;
A79: (GoB f)*(i+1,w)`2 = (GoB f)*(1,w)`2 by A9,A12,A13,GOBOARD5:1
.= A`2 by A4,A5,A6,A9,GOBOARD5:1;
then
A80: (f/.2)`2 = N-bound L~f by A17,EUCLID:52;
A81: <*(GoB f)*(i+1,w)*> is_in_the_area_of f by A9,A12,A13,SPRECT_3:49;
<*(GoB f)*(i,w-'1)*> is_in_the_area_of f by A4,A5,A19,A64,SPRECT_3:49;
then <*(GoB f)*(i,w-'1),(GoB f)*(i+1,w)*> is_in_the_area_of f by A81,
SPRECT_3:42;
then <*z2*> is_in_the_area_of f by SPRECT_3:50;
then
A82: <*z2*> is_in_the_area_of SpStSeq L~f by SPRECT_3:53;
A83: (GoB f)*(i,w-'1) = f/.(len f -' 1) by A1,A6,A16,SPRECT_3:29;
then LSeg(A,f/.(len f -' 1)) is vertical by A78,SPPOL_1:16;
then
A84: LSeg(A,f/.(len f -' 1)) /\ LSeg(NW-corner L~f,A) = { A } by A70,SPRECT_1:9
,SPRECT_3:10;
A85: (NW-corner L~f)`2 = A`2 by PSCOMP_1:37;
A86: (NW-corner L~f)`1 <= A`1 by PSCOMP_1:38;
A`1 <= (f/.2)`1 by A76,PSCOMP_1:39;
then A in LSeg(NW-corner L~f,f/.2) by A17,A79,A85,A86,GOBOARD7:8;
then
A87: LSeg(A,f/.2) /\ LSeg(NW-corner L~f,A) = { A } by TOPREAL1:8;
((GoB f)*(i,w))`2 = ((GoB f)*(1,w))`2 by A4,A5,A9,GOBOARD5:1
.= ((GoB f)*(i+1,w))`2 by A9,A12,A13,GOBOARD5:1;
then ((GoB f)*(i,w-'1)+(GoB f)*(i,w))`2 = ((GoB f)*(i,w-'1))`2+((GoB f)*(i+
1,w))`2 by TOPREAL3:2
.= ((GoB f)*(i,w-'1)+(GoB f)*(i+1,w))`2 by TOPREAL3:2;
then p2`2 = 1/2*((GoB f)*(i,w-'1)+(GoB f)*(i+1,w)) `2 by TOPREAL3:4
.= z2`2 by TOPREAL3:4;
then
A88: LSeg(p2,z2) is horizontal by SPPOL_1:15;
A89: f/.(len f -' 1) in LSeg(f/.(len f -' 1), f/.len f) by RLTOPSP1:68;
A90: (GoB f)*(i,w) = f/.len f by A1,A6,FINSEQ_6:def 1;
p2 = 1/2*((GoB f)*(i,w-'1))+(1 - 1/2)*((GoB f)*(i,w)) by RLVECT_1:def 5;
then
A91: p2 in LSeg(f/.(len f -' 1), f/.len f) by A83,A90;
then
A92: LSeg(p2,f/.(len f -' 1)) c= LSeg(f/.(len f -' 1), f/.len f) by A89,
TOPREAL1:6;
LSeg(f/.(len f -' 1), f/.len f) = LSeg(f,len f -' 1) by A59,A61,
TOPREAL1:def 3;
then
A93: LSeg(f/.(len f -' 1), f/.len f) c= L~f by TOPREAL3:19;
then
A94: LSeg(p2,f/.(len f -' 1)) c= L~f by A92,XBOOLE_1:1;
A95: LSeg(p2,f/.(len f -' 1)) c= LSeg(f,len f -' 1) by A59,A61,A92,
TOPREAL1:def 3;
A96: p2`1 = 1/2*((GoB f)*(i,w-'1)+A)`1 by A6,TOPREAL3:4
.= 1/2*(A`1+A`1) by A78,TOPREAL3:2
.= (N-min L~f)`1;
then
A97: LSeg(p2,f/.(len f -' 1)) is vertical by A78,A83,SPPOL_1:16;
A98: p2 in LSeg(p2,f/.(len f -' 1)) by RLTOPSP1:68;
then
A99: p2 in L~f by A94;
A100: now
assume p2 = A;
then f/.(len f -' 1) = f/.len f by A1,A6,A67,A83,SPRECT_3:5;
hence contradiction by A58,A60,A61,GOBOARD7:29;
end;
1 + 1 + 1 <= len f by GOBOARD7:34,XXREAL_0:2;
then
A101: 1 + 1 <= len f -' 1 by NAT_D:49;
then
A102: 1 <= len f -' 1 -' 1 by NAT_D:49;
A103: len f -' 1 -'1 + 1 = len f -' 1 by A101,XREAL_1:235,XXREAL_0:2;
A104: len f -' 1 -' 1 + 2 = len f -' 2 + 2 by NAT_D:45
.= len f by A7,XREAL_1:235,XXREAL_0:2;
A105: for i,j st 1 <= i & i <= j & j < len f -' 1 holds L~mid(f,i,j) misses
LSeg(p2,f/.(len f -' 1))
proof
let l,j such that
A106: 1 <= l and
A107: l <= j and
A108: j < len f -' 1;
assume L~mid(f,l,j) meets LSeg(p2,f/.(len f -' 1));
then L~mid(f,l,j) /\ LSeg(p2,f/.(len f -' 1)) <> {} by XBOOLE_0:def 7;
then consider p being Point of TOP-REAL 2 such that
A109: p in L~mid(f,l,j) /\ LSeg(p2,f/.(len f -' 1)) by SUBSET_1:4;
p in L~mid(f,l,j) by A109,XBOOLE_0:def 4;
then consider ii being Nat such that
A110: 1 <= ii and
A111: ii+1 <= len mid(f,l,j) and
A112: p in LSeg(mid(f,l,j),ii) by SPPOL_2:13;
len f -' 1 > l by A107,A108,XXREAL_0:2;
then len f -' 1 > 1 by A106,XXREAL_0:2;
then
A113: len f -' 1 < len f by NAT_D:51;
then
A114: j < len f by A108,XXREAL_0:2;
then len mid(f,l,j) = j-'l+1 by A106,A107,FINSEQ_6:186;
then
A115: ii<j-'l+1 by A111,NAT_1:13;
set k = ii+l-'1;
A116: p in LSeg(p2,f/.(len f -' 1)) by A109,XBOOLE_0:def 4;
per cases by A107,XXREAL_0:1;
suppose
AB: l = j; then
j in dom f by A106,A114,FINSEQ_3:25;
then len mid(f,l,j) = 1 by AB,FINSEQ_6:193;
then L~mid(f,l,j) = {} by TOPREAL1:22;
hence thesis by A112,SPPOL_2:17;
end;
suppose
A117: l < j;
A118: ii + 1 >= 1 + 1 by A110,XREAL_1:6;
ii + l >= ii + 1 by A106,XREAL_1:6;
then
A119: ii + l >= 1 + 1 by A118,XXREAL_0:2;
then
A120: k >= 1 by NAT_D:49;
A121: ii + l >= 1 by A119,XXREAL_0:2;
A122: now
assume k + 1 >= len f -' 1;
then k >= len f -'1 -' 1 by NAT_D:53;
then
A123: ii + l >= len f -' 1 by A121,NAT_D:56;
ii + l < j -' l + 1 + l by A115,XREAL_1:6;
then ii + l < j -' l + l + 1;
then ii + l < j + 1 by A117,XREAL_1:235;
then len f -' 1 < j + 1 by A123,XXREAL_0:2;
hence contradiction by A108,NAT_1:13;
end;
A124: LSeg(f,1) /\ LSeg(f,len f -' 1) = { f.1 } by JORDAN4:42
.= {f/.1} by A15,PARTFUN1:def 6;
LSeg(mid(f,l,j),ii)=LSeg(f,k) by A106,A114,A110,A115,A117,JORDAN4:19;
then
A125: p in LSeg(f,k) /\ LSeg(f,len f -' 1) by A95,A116,A112,XBOOLE_0:def 4;
then LSeg(f,k) meets LSeg(f,len f -' 1) by XBOOLE_0:4;
then k <= 1 by A113,A122,GOBOARD5:def 4;
then k = 1 by A120,XXREAL_0:1;
then p = f/.1 by A125,A124,TARSKI:def 1;
hence contradiction by A1,A67,A91,A100,A116,SPRECT_3:6;
end;
end;
A126: for j st 1 <= j & j < len f -' 1 holds L~mid(f,j,len f -' 1) /\ LSeg(
p2,f/.(len f -' 1)) = {f/.(len f -' 1)}
proof
let j such that
A127: 1 <= j and
A128: j < len f -' 1;
A129: 1 <= len f -' 1 by A127,A128,XXREAL_0:2;
A130: len f -' 1 -' 1 = len f -' 2 by NAT_D:45;
then
A131: L~mid(f,j,len f -' 1) = LSeg(f,len f -' 2) \/ L~mid(f,j,len f -' 2)
by A127,A128,NAT_D:35,SPRECT_3:20;
j <= len f -' 2 by A128,A130,NAT_D:49;
then LSeg(p2,f/.(len f -' 1)) misses L~mid(f,j,len f -' 2) by A105,A127
,A129,A130,JORDAN5B:1;
hence
L~mid(f,j,len f -' 1) /\ LSeg(p2,f/.(len f -' 1)) = LSeg(f,len f -' 2
) /\ LSeg(p2,f/.(len f -' 1)) by A131,XBOOLE_1:78
.= {f/.(len f -' 1)} by A75,A95,RLTOPSP1:68,ZFMISC_1:124;
end;
A132: LSeg(NW-corner L~f,N-min L~f) misses LSeg(f/.(len f -' 1),p2)
proof
assume LSeg(NW-corner L~f,A) meets LSeg(f/.(len f -' 1),p2);
then LSeg(p2,f/.(len f -' 1)) /\ LSeg(NW-corner L~f,A) <> {} by
XBOOLE_0:def 7;
then consider p being Point of TOP-REAL 2 such that
A133: p in LSeg(p2,f/.(len f -' 1)) /\ LSeg(NW-corner L~f,A) by SUBSET_1:4;
A134: p in LSeg(p2,f/.(len f -' 1)) by A133,XBOOLE_0:def 4;
p in LSeg(NW-corner L~f,A) by A133,XBOOLE_0:def 4;
then p in { A } by A1,A67,A84,A92,A134,XBOOLE_0:def 4;
then p = A by TARSKI:def 1;
hence contradiction by A1,A67,A91,A100,A134,SPRECT_3:6;
end;
A135: p2`2 <> A`2 by A96,A100,TOPREAL3:6;
set G = GoB f;
A136: Int cell(GoB f,i,w-'1) misses L~f by A5,A64,GOBOARD7:12;
L~f /\ (Int cell(G,i,w-'1) \/ { p2 }) = L~f /\ Int cell(G,i,w-'1) \/
L~f /\ { p2 } by XBOOLE_1:23
.= {} \/ L~f /\ { p2 } by A136,XBOOLE_0:def 7
.= L~f /\ { p2 };
then
A137: LSeg(z2,p2) /\ L~f c= L~f /\ { p2 } by A4,A5,A10,A19,A64,GOBOARD6:40
,XBOOLE_1:26;
L~f /\ { p2 } c= { p2 } by XBOOLE_1:17;
then
A138: LSeg(z2,p2) /\ L~f c= { p2 } by A137,XBOOLE_1:1;
A139: for i,j st 1 <= i & i < j & j < len f holds L~mid(f,i,j) misses LSeg(
z2,p2)
proof
len f >= 1 + 1 by GOBOARD7:34,XXREAL_0:2;
then
A140: len f -' 1 >= 1 by NAT_D:49;
let l,j such that
A141: 1 <= l and
A142: l < j and
A143: j < len f;
assume L~mid(f,l,j) meets LSeg(z2,p2);
then L~mid(f,l,j) /\ LSeg(z2,p2) <> {} by XBOOLE_0:def 7;
then consider p being Point of TOP-REAL 2 such that
A144: p in L~mid(f,l,j) /\ LSeg(z2,p2) by SUBSET_1:4;
p in L~mid(f,l,j) by A144,XBOOLE_0:def 4;
then consider ii being Nat such that
A145: 1 <= ii and
A146: ii+1 <= len mid(f,l,j) and
A147: p in LSeg(mid(f,l,j),ii) by SPPOL_2:13;
A148: len mid(f,l,j) = j-'l+1 by A141,A142,A143,FINSEQ_6:186;
then ii<j-'l+1 by A146,NAT_1:13;
then
A149: p in LSeg(f,ii+l-'1) by A141,A142,A143,A145,A147,JORDAN4:19;
set k = ii+l-'1;
A150: ii + 1 >= 1 + 1 by A145,XREAL_1:6;
LSeg(f,k) /\ LSeg(z2,p2) c= L~f /\ LSeg(z2,p2) by TOPREAL3:19,XBOOLE_1:26;
then
A151: LSeg(f,k) /\ LSeg(z2,p2) c= { p2 } by A138,XBOOLE_1:1;
p in LSeg(z2,p2) by A144,XBOOLE_0:def 4;
then p in LSeg(f,ii+l-'1) /\ LSeg(z2,p2) by A149,XBOOLE_0:def 4;
then p = p2 by A151,TARSKI:def 1;
then p2 in LSeg(f,k) /\ LSeg(f/.(len f -' 1), f/.len f) by A91,A149,
XBOOLE_0:def 4;
then
A152: p2 in LSeg(f,k) /\ LSeg(f,len f -' 1) by A61,A140,TOPREAL1:def 3;
then
A153: LSeg(f,k) meets LSeg(f,len f -' 1) by XBOOLE_0:4;
ii + l >= ii + 1 by A141,XREAL_1:6;
then ii + l >= 1 + 1 by A150,XXREAL_0:2;
then
A154: k >= 1 by NAT_D:49;
per cases by A62,A153,GOBOARD5:def 4;
suppose
A155: k <= 1;
A156: LSeg(f,1) /\ LSeg(f,len f -' 1) = {f.1} by JORDAN4:42
.= {f/.1} by A15,PARTFUN1:def 6;
k = 1 by A154,A155,XXREAL_0:1;
hence contradiction by A1,A100,A152,A156,TARSKI:def 1;
end;
suppose
A157: k+1 >= len f -' 1;
ii <= j -' l by A146,A148,XREAL_1:6;
then ii + l <= j by A142,NAT_D:54;
then
A158: ii+l < len f by A143,XXREAL_0:2;
ii+l >= l by NAT_1:11;
then ii+l >= 1 by A141,XXREAL_0:2;
then ii+l-'1 < len f -' 1 by A158,NAT_D:56;
then
A159: ii+l-'1 <= len f -' 1 -' 1 by NAT_D:49;
k >= len f -' 1 -' 1 by A157,NAT_D:53;
then k = len f -' 1 -' 1 by A159,XXREAL_0:1;
then p2 in {f/.(len f -' 1)} by A102,A103,A104,A152,TOPREAL1:def 6;
then p2 = f/.(len f -' 1) by TARSKI:def 1;
hence contradiction by A6,A83,A100,SPRECT_3:5;
end;
end;
A160: <*p2*> is_in_the_area_of f by A94,A98,SPRECT_2:21,SPRECT_3:46;
then
A161: <*p2*> is_in_the_area_of SpStSeq L~f by SPRECT_3:53;
<*p2,z2*> = <*p2*>^<*z2*> by FINSEQ_1:def 9;
then
A162: L~SpStSeq L~f /\ LSeg(p2,z2) c= { p2 } by A65,A82,A161,SPRECT_2:24
,SPRECT_3:47;
((GoB f)*(i,w-'1))`1 = ((GoB f)*(i,1))`1 by A4,A5,A19,GOBOARD5:2,NAT_D:35
.= ((GoB f)*(i,w))`1 by A4,A5,A9,GOBOARD5:2;
then ((GoB f)*(i,w)+(GoB f)*(i+1,w))`1 = ((GoB f)*(i,w-'1))`1+((GoB f)*(i+1
,w))`1 by TOPREAL3:2
.= ((GoB f)*(i,w-'1)+(GoB f)*(i+1,w))`1 by TOPREAL3:2;
then p1`1 = 1/2*((GoB f)*(i,w-'1)+(GoB f)*(i+1,w))`1 by TOPREAL3:4
.= z2`1 by TOPREAL3:4;
then
A163: LSeg(p1,z2) is vertical by SPPOL_1:16;
A164: f/.2 in LSeg(f/.1, f/.(1+1)) by RLTOPSP1:68;
p1 = 1/2*((GoB f)*(i,w))+(1-1/2)*((GoB f)*(i+1,w)) by RLVECT_1:def 5;
then
A165: p1 in LSeg(f/.1, f/.2) by A1,A6,A17;
then
A166: LSeg(p1,f/.2) c= LSeg(f/.1, f/.2) by A164,TOPREAL1:6;
A167: LSeg(f/.1, f/.(1+1)) = LSeg(f,1) by A8,TOPREAL1:def 3;
then
A168: LSeg(f/.1, f/.2) c= L~f by TOPREAL3:19;
then
A169: LSeg(p1,f/.2) c= L~f by A166,XBOOLE_1:1;
A170: p1`2 = 1/2*(A+(GoB f)*(i+1,w))`2 by A6,TOPREAL3:4
.= 1/2*(A`2+A`2) by A79,TOPREAL3:2
.= N-bound L~f by EUCLID:52;
A171: p1 in LSeg(p1,f/.2) by RLTOPSP1:68;
A172: p1 <> A by A1,A6,A15,A17,A57,GOBOARD7:29,SPRECT_3:5;
A173: for i,j st 2 < i & i <= j & j<= len f holds L~mid(f,i,j) misses LSeg(
p1,f/.2)
proof
let l,j such that
A174: 2 < l and
A175: l <= j and
A176: j<= len f;
assume L~mid(f,l,j) meets LSeg(p1,f/.2);
then L~mid(f,l,j) /\ LSeg(p1,f/.2) <> {} by XBOOLE_0:def 7;
then consider p being Point of TOP-REAL 2 such that
A177: p in L~mid(f,l,j) /\ LSeg(p1,f/.2) by SUBSET_1:4;
A178: p in LSeg(p1,f/.2) by A177,XBOOLE_0:def 4;
p in L~mid(f,l,j) by A177,XBOOLE_0:def 4;
then consider ii being Nat such that
A179: 1 <= ii and
A180: ii+1 <= len mid(f,l,j) and
A181: p in LSeg(mid(f,l,j),ii) by SPPOL_2:13;
A182: 1 < l by A174,XXREAL_0:2;
then
A183: len mid(f,l,j) = j-'l+1 by A175,A176,FINSEQ_6:186;
then
A184: ii<j-'l+1 by A180,NAT_1:13;
set k = ii+l-'1;
A185: ii + 2 >= 1 + 2 by A179,XREAL_1:6;
ii + l > ii + 2 by A174,XREAL_1:6;
then ii + l > 1 + 2 by A185,XXREAL_0:2;
then
A186: k > 1+1 by NAT_D:52;
per cases by A175,XXREAL_0:1;
suppose
AB: l = j; then
j in dom f by A176,A182,FINSEQ_3:25;
then len mid(f,l,j) = 1 by AB,FINSEQ_6:193;
then L~mid(f,l,j) = {} by TOPREAL1:22;
hence thesis by A181,SPPOL_2:17;
end;
suppose
A187: l < j;
A188: LSeg(f,1) /\ LSeg(f,len f -' 1) = { f.1 } by JORDAN4:42
.= {f/.1} by A15,PARTFUN1:def 6;
ii <= j -' l by A180,A183,XREAL_1:6;
then ii + l <= j by A175,NAT_D:54;
then ii+l <= len f by A176,XXREAL_0:2;
then
A189: ii+l-'1 <= len f -' 1 by NAT_D:42;
LSeg(mid(f,l,j),ii)=LSeg(f,k) by A176,A182,A179,A184,A187,JORDAN4:19;
then
A190: p in LSeg(f,k) /\ LSeg(f,1) by A166,A167,A178,A181,XBOOLE_0:def 4;
then LSeg(f,k) meets LSeg(f,1) by XBOOLE_0:4;
then k+1 >= len f by A186,GOBOARD5:def 4;
then k >= len f -' 1 by NAT_D:53;
then k = len f -' 1 by A189,XXREAL_0:1;
then p = f/.1 by A190,A188,TARSKI:def 1;
hence contradiction by A1,A165,A172,A178,SPRECT_3:6;
end;
end;
A191: for j st 2 < j & j <= len f holds L~mid(f,2,j) /\ LSeg(p1,f/.2) = {f/. 2}
proof
A192: f/.2 in LSeg(p1,f/.2) by RLTOPSP1:68;
let j such that
A193: 2 < j and
A194: j <= len f;
2+1 <= j by A193,NAT_1:13;
then
A195: LSeg(p1,f/.2) misses L~mid(f,2+1,j) by A173,A194;
L~mid(f,2,j) = LSeg(f,2) \/ L~mid(f,2+1,j) by A193,A194,SPRECT_3:19;
hence L~mid(f,2,j) /\ LSeg(p1,f/.2) = LSeg(f,2) /\ LSeg(p1,f/.2) by A195,
XBOOLE_1:78
.= {f/.2} by A72,A164,A165,A167,A192,TOPREAL1:6,ZFMISC_1:124;
end;
A196: LSeg(p1,f/.2) misses LSeg(NW-corner L~f,A)
proof
assume LSeg(p1,f/.2) meets LSeg(NW-corner L~f,A);
then LSeg(p1,f/.2) /\ LSeg(NW-corner L~f,A) <> {} by XBOOLE_0:def 7;
then consider p being Point of TOP-REAL 2 such that
A197: p in LSeg(p1,f/.2) /\ LSeg(NW-corner L~f,A) by SUBSET_1:4;
A198: p in LSeg(p1,f/.2) by A197,XBOOLE_0:def 4;
p in LSeg(NW-corner L~f,A) by A197,XBOOLE_0:def 4;
then p in { A } by A1,A87,A166,A198,XBOOLE_0:def 4;
then p = A by TARSKI:def 1;
hence contradiction by A1,A165,A172,A198,SPRECT_3:6;
end;
A199: LSeg(NW-corner L~f,N-min L~f) misses LSeg(z2,p1)
proof
assume LSeg(NW-corner L~f,N-min L~f) meets LSeg(z2,p1);
then LSeg(NW-corner L~f,N-min L~f) /\ LSeg(z2,p1) <> {} by XBOOLE_0:def 7;
then consider p being Point of TOP-REAL 2 such that
A200: p in LSeg(NW-corner L~f,N-min L~f) /\ LSeg(z2,p1) by SUBSET_1:4;
A201: p in LSeg(z2,p1) by A200,XBOOLE_0:def 4;
A202: p in LSeg(NW-corner L~f,N-min L~f) by A200,XBOOLE_0:def 4;
LSeg(NW-corner L~f,NE-corner L~f) /\ LSeg(z2,p1) = {p1} by A77,A163,A165,
SPRECT_3:11;
then p in {p1} by A70,A202,A201,XBOOLE_0:def 4;
then p1 in LSeg(NW-corner L~f,N-min L~f) by A202,TARSKI:def 1;
then p1 in LSeg(NW-corner L~f,N-min L~f) /\ L~f
by A169,A171,XBOOLE_0:def 4;
then p1 in { N-min L~f } by PSCOMP_1:43;
hence contradiction by A172,TARSKI:def 1;
end;
A203: for i,j st 1 < i & i < j & j<= len f holds L~mid(f,i,j) misses LSeg(z2
,p1)
proof
A204: len f >= 2 by GOBOARD7:34,XXREAL_0:2;
A205: Int cell(GoB f,i,w-'1) misses L~f by A5,A64,GOBOARD7:12;
A206: L~f /\ { p1 } c= { p1 } by XBOOLE_1:17;
let l,j such that
A207: 1 < l and
A208: l < j and
A209: j<= len f;
assume L~mid(f,l,j) meets LSeg(z2,p1);
then L~mid(f,l,j) /\ LSeg(z2,p1) <> {} by XBOOLE_0:def 7;
then consider p being Point of TOP-REAL 2 such that
A210: p in L~mid(f,l,j) /\ LSeg(z2,p1) by SUBSET_1:4;
p in L~mid(f,l,j) by A210,XBOOLE_0:def 4;
then consider ii being Nat such that
A211: 1 <= ii and
A212: ii+1 <= len mid(f,l,j) and
A213: p in LSeg(mid(f,l,j),ii) by SPPOL_2:13;
A214: len mid(f,l,j) = j-'l+1 by A207,A208,A209,FINSEQ_6:186;
then ii<j-'l+1 by A212,NAT_1:13;
then
A215: p in LSeg(f,ii+l-'1) by A207,A208,A209,A211,A213,JORDAN4:19;
set k = ii+l-'1, G = GoB f;
A216: LSeg(f,k) /\ LSeg(z2,p1) c= L~f /\ LSeg(z2,p1) by TOPREAL3:19,XBOOLE_1:26
;
L~f /\ (Int cell(G,i,w-'1) \/ { p1 }) = L~f /\ Int cell(G,i,w-'1) \/
L~f /\ { p1 } by XBOOLE_1:23
.= {} \/ L~f /\ { p1 } by A205,XBOOLE_0:def 7
.= L~f /\ { p1 };
then LSeg(z2,p1) /\ L~f c= L~f /\ { p1 } by A4,A5,A10,A19,A64,GOBOARD6:41
,XBOOLE_1:26;
then LSeg(z2,p1) /\ L~f c= { p1 } by A206,XBOOLE_1:1;
then
A217: LSeg(f,k) /\ LSeg(z2,p1) c= { p1 } by A216,XBOOLE_1:1;
p in LSeg(z2,p1) by A210,XBOOLE_0:def 4;
then p in LSeg(f,ii+l-'1) /\ LSeg(z2,p1) by A215,XBOOLE_0:def 4;
then p = p1 by A217,TARSKI:def 1;
then p1 in LSeg(f,k) /\ LSeg(f/.1,f/.(1+1)) by A165,A215,XBOOLE_0:def 4;
then
A218: p1 in LSeg(f,k) /\ LSeg(f,1) by A204,TOPREAL1:def 3;
then LSeg(f,k) meets LSeg(f,1) by XBOOLE_0:4;
then
A219: k <= 1+1 or k+1 >= len f by GOBOARD5:def 4;
A220: ii + 1 >= 1 + 1 by A211,XREAL_1:6;
ii + l > ii + 1 by A207,XREAL_1:6;
then ii + l > 1 + 1 by A220,XXREAL_0:2;
then
A221: k > 1 by NAT_D:52;
per cases by A219;
suppose
A222: k <= 2;
k >= 1+1 by A221,NAT_1:13;
then
A223: k = 2 by A222,XXREAL_0:1;
1 + 2 <= len f by GOBOARD7:34,XXREAL_0:2;
then p1 in {f/.(1+1)} by A218,A223,TOPREAL1:def 6;
then p1 = f/.(1+1) by TARSKI:def 1;
hence contradiction by A6,A17,A172,SPRECT_3:5;
end;
suppose
A224: k+1 >= len f;
A225: LSeg(f,1) /\ LSeg(f,len f -' 1) = { f.1 } by JORDAN4:42
.= {f/.1} by A15,PARTFUN1:def 6;
ii <= j -' l by A212,A214,XREAL_1:6;
then ii + l <= j by A208,NAT_D:54;
then ii+l <= len f by A209,XXREAL_0:2;
then
A226: ii+l-'1 <= len f -' 1 by NAT_D:42;
k >= len f -' 1 by A224,NAT_D:53;
then k = len f -' 1 by A226,XXREAL_0:1;
hence contradiction by A1,A172,A218,A225,TARSKI:def 1;
end;
end;
LSeg(f/.1,f/.2) c= L~SpStSeq L~f by A1,SPRECT_3:31;
then
A227: L~SpStSeq L~f /\ LSeg(p1,z2) = { p1 } by A65,A82,A165,SPRECT_3:48;
A228: LSeg(p1,f/.2) is horizontal by A80,A170,SPPOL_1:15;
A229: p1 in LSeg(p1,f/.2) by RLTOPSP1:68;
then
A230: p1 in L~f by A169;
A231: <*p1*> is_in_the_area_of f by A169,A229,SPRECT_2:21,SPRECT_3:46;
A232: L~f misses L~Red9 by A51,A53,SPRECT_3:25,XBOOLE_1:63;
reconsider Red9 as S-Sequence_in_R2 by A52;
len Red9 in dom Red9 by FINSEQ_5:6;
then
A233: z2 in L~Red9 by A55,SPPOL_2:44;
set u1 = Last_Point(L~Red9,Red9/.1,Red9/.len Red9,L~SpStSeq L~f), Red =
L_Cut(Red9,u1), u2 = First_Point(L~Red,Red/.1,Red/.len Red,LSeg(z2,p1)), u3 =
First_Point(L~Red,Red/.1,Red/.len Red,LSeg(z2,p2));
NW-corner L~SpStSeq L~f = NW-corner L~f by SPRECT_1:62;
then
A234: u1 <> NW-corner L~f by A47,A48,A54,A55,SPRECT_3:38;
A235: L~Red9 is_an_arc_of z1,z2 by A54,A55,TOPREAL1:25;
L~Red9 /\ L~SpStSeq L~f is closed by TOPS_1:8;
then
A236: u1 in L~Red9 /\ L~SpStSeq L~f by A54,A55,A56,A235,JORDAN5C:def 2;
then
A237: u1 in L~SpStSeq L~f by XBOOLE_0:def 4;
A238: u1 in L~Red9 by A236,XBOOLE_0:def 4;
A239: now
assume u1 in L~f;
then u1 in L~f /\ L~Red9 by A238,XBOOLE_0:def 4;
hence contradiction by A232,XBOOLE_0:def 7;
end;
len Red9 in dom Red9 by FINSEQ_5:6;
then u1 <> Red9.len Red9 by A55,A65,A237,PARTFUN1:def 6;
then reconsider Red as S-Sequence_in_R2 by A238,JORDAN3:34;
1 in dom Red by FINSEQ_5:6;
then
A240: Red/.1 =Red.1 by PARTFUN1:def 6
.= u1 by A238,JORDAN3:23;
A241: L~SpStSeq L~f /\ L~Red = { u1 } by A55,A56,A65,Th5;
len Red9 in dom Red9 by FINSEQ_5:6;
then z2 = Red9.len Red9 by A55,PARTFUN1:def 6;
then
A242: z2 in L~Red by A65,A233,A237,A238,JORDAN5B:22;
Red is_in_the_area_of SpStSeq L~f by A47,A48,A54,A55,SPRECT_3:54;
then
A243: Red is_in_the_area_of f by SPRECT_3:53;
A244: L~Red c= L~Red9 by A238,JORDAN3:42;
A245: L~f misses L~Red by A232,A238,JORDAN3:42,XBOOLE_1:63;
z2 in LSeg(p1,z2) by RLTOPSP1:68;
then
A246: LSeg(p1,z2) meets L~Red by A242,XBOOLE_0:3;
z2 in LSeg(p2,z2) by RLTOPSP1:68;
then
A247: LSeg(p2,z2) meets L~Red by A242,XBOOLE_0:3;
A248: L~Red /\ LSeg(p1,z2) is closed by TOPS_1:8;
A249: L~Red /\ LSeg(p2,z2) is closed by TOPS_1:8;
L~Red is_an_arc_of Red/.1,Red/.len Red by TOPREAL1:25;
then
A250: u3 in LSeg(p2,z2) /\ L~Red by A247,A249,JORDAN5C:def 1;
then
A251: u3 in L~Red by XBOOLE_0:def 4;
A252: u3 in LSeg(p2,z2) by A250,XBOOLE_0:def 4;
A253: u3 <> p2 by A94,A98,A232,A244,A251,XBOOLE_0:3;
A254: p2 in LSeg(p2,z2) by RLTOPSP1:68;
then
A255: LSeg(p2,u3) c= LSeg(p2,z2) by A252,TOPREAL1:6;
then
A256: LSeg(NW-corner L~f,N-min L~f) misses LSeg(u3,p2) by A71,A88,A135,
SPRECT_3:9,XBOOLE_1:63;
A257: for i,j st 1 <= i & i < j & j < len f holds L~mid(f,i,j) misses LSeg(
u3,p2)
proof
let i,j;
assume that
A258: 1 <= i and
A259: i < j and
A260: j < len f;
L~mid(f,i,j) misses LSeg(z2,p2) by A139,A258,A259,A260;
hence thesis by A252,A254,TOPREAL1:6,XBOOLE_1:63;
end;
A261: now
A262: 1 in dom Red by FINSEQ_5:6;
assume u3 = Red.1;
then u3 in L~SpStSeq L~f by A237,A240,A262,PARTFUN1:def 6;
then u3 in LSeg(p2,z2) /\ L~SpStSeq L~f by A252,XBOOLE_0:def 4;
hence contradiction by A162,A253,TARSKI:def 1;
end;
L~Red is_an_arc_of Red/.1,Red/.len Red by TOPREAL1:25;
then
A263: u2 in LSeg(p1,z2) /\ L~Red by A246,A248,JORDAN5C:def 1;
then
A264: u2 in L~Red by XBOOLE_0:def 4;
A265: u2 in LSeg(p1,z2) by A263,XBOOLE_0:def 4;
A266: u2 <> p1 by A169,A229,A232,A244,A264,XBOOLE_0:3;
A267: p1 in LSeg(p1,z2) by RLTOPSP1:68;
then
A268: LSeg(p1,u2) c= LSeg(p1,z2) by A265,TOPREAL1:6;
A269: LSeg(NW-corner L~f,N-min L~f) misses LSeg(u2,p1) by A199,A265,A267,
TOPREAL1:6,XBOOLE_1:63;
A270: for i,j st 1 < i & i < j & j<= len f holds L~mid(f,i,j) misses LSeg(u2
,p1)
proof
let i,j;
assume that
A271: 1 < i and
A272: i < j and
A273: j<= len f;
L~mid(f,i,j) misses LSeg(z2,p1) by A203,A271,A272,A273;
hence thesis by A265,A267,TOPREAL1:6,XBOOLE_1:63;
end;
A274: now
A275: 1 in dom Red by FINSEQ_5:6;
assume u2 = Red.1;
then u2 in L~SpStSeq L~f by A237,A240,A275,PARTFUN1:def 6;
then u2 in { p1 } by A227,A265,XBOOLE_0:def 4;
hence contradiction by A266,TARSKI:def 1;
end;
reconsider Red2=R_Cut(Red,u3) as S-Sequence_in_R2 by A251,A261,JORDAN3:35;
A276: Red2/.1 = u1 by A240,A251,SPRECT_3:22;
A277: len Red2 in dom Red2 by FINSEQ_5:6;
A278: (Rev Red2)/.1 = Red2/.len Red2 by FINSEQ_5:65
.= Red2.len Red2 by A277,PARTFUN1:def 6
.= u3 by A251,JORDAN3:24;
then
A279: ((Rev Red2)/.1)`2 = p2`2 by A88,A252,SPPOL_1:40;
A280: (Rev Red2)/.1 <> p2 by A94,A98,A232,A244,A251,A278,XBOOLE_0:3;
A281: L~Rev Red2 = L~Red2 by SPPOL_2:22;
A282: u3 in L~Red2 by A251,A261,JORDAN5B:20;
u3 in LSeg(p2,u3) by RLTOPSP1:68;
then
A283: u3 in L~Red2 /\ LSeg(p2,u3) by A282,XBOOLE_0:def 4;
now
assume u1 in LSeg(p2,z2);
then u1 in L~SpStSeq L~f /\ LSeg(p2,z2) by A237,XBOOLE_0:def 4;
hence contradiction by A99,A162,A239,TARSKI:def 1;
end;
then LSeg(p2,z2) /\ L~Red2={ u3 } by A240,A247,Th1;
then LSeg(p2,u3) /\ L~Red2 c={ u3 } by A252,A254,TOPREAL1:6,XBOOLE_1:26;
then LSeg(p2,u3) /\ L~Red2={ u3 } by A283,ZFMISC_1:33;
then reconsider
RB2 = <*p2*>^Rev Red2 as S-Sequence_in_R2 by A278,A279,A280,A281,SPRECT_3:16;
LSeg(p2,f/.(len f -' 1)) misses L~Red by A92,A93,A245,XBOOLE_1:1,63;
then LSeg(p2,f/.(len f -' 1)) misses L~Red2 by A251,JORDAN3:41,XBOOLE_1:63;
then
A284: LSeg(p2,f/.(len f -' 1)) /\ L~Red2 = {} by XBOOLE_0:def 7;
1 in dom Red2 by FINSEQ_5:6;
then u1 in L~Red2 by A276,SPPOL_2:44;
then
A285: u1 in L~SpStSeq L~f /\ L~Red2 by A237,XBOOLE_0:def 4;
L~SpStSeq L~f /\ L~Red2 c= { u1 } by A241,A251,JORDAN3:41,XBOOLE_1:26;
then
A286: L~SpStSeq L~f /\ L~Red2 = { u1 } by A285,ZFMISC_1:33;
reconsider Red1=R_Cut(Red,u2) as S-Sequence_in_R2 by A264,A274,JORDAN3:35;
len Red1 in dom Red1 by FINSEQ_5:6;
then
A287: Red1/.len Red1 = Red1.len Red1 by PARTFUN1:def 6
.= u2 by A264,JORDAN3:24;
A288: Red1/.1 = u1 by A240,A264,SPRECT_3:22;
A289: (Red1/.len Red1)`1 = p1`1 by A163,A265,A287,SPPOL_1:41;
A290: Red1/.len Red1 <> p1 by A169,A229,A232,A244,A264,A287,XBOOLE_0:3;
A291: u2 in L~Red1 by A264,A274,JORDAN5B:20;
u2 in LSeg(p1,u2) by RLTOPSP1:68;
then
A292: u2 in L~Red1 /\ LSeg(p1,u2) by A291,XBOOLE_0:def 4;
now
assume u1 in LSeg(p1,z2);
then u1 in L~SpStSeq L~f /\ LSeg(p1,z2) by A237,XBOOLE_0:def 4;
hence contradiction by A227,A230,A239,TARSKI:def 1;
end;
then LSeg(p1,z2) /\ L~Red1={ u2 } by A240,A246,Th1;
then LSeg(p1,u2) /\ L~Red1 c={ u2 } by A265,A267,TOPREAL1:6,XBOOLE_1:26;
then LSeg(p1,u2) /\ L~Red1={ u2 } by A292,ZFMISC_1:33;
then reconsider RB1 = Red1^<*p1*> as S-Sequence_in_R2 by A287,A289,A290,
SPRECT_2:61;
LSeg(p1,f/.2) misses L~Red by A166,A168,A245,XBOOLE_1:1,63;
then LSeg(p1,f/.2) misses L~Red1 by A264,JORDAN3:41,XBOOLE_1:63;
then
A293: LSeg(p1,f/.2) /\ L~Red1 = {} by XBOOLE_0:def 7;
1 in dom Red1 by FINSEQ_5:6;
then
A294: u1 in L~Red1 by A288,SPPOL_2:44;
then
A295: u1 in L~SpStSeq L~f /\ L~Red1 by A237,XBOOLE_0:def 4;
L~SpStSeq L~f /\ L~Red1 c= { u1 } by A241,A264,JORDAN3:41,XBOOLE_1:26;
then
A296: L~SpStSeq L~f /\ L~Red1 = { u1 } by A295,ZFMISC_1:33;
len Rev Red2 = len Red2 by FINSEQ_5:def 3;
then
A297: RB2/.len RB2 = (Rev Red2)/.len Red2 by SPRECT_3:1
.= u1 by A276,FINSEQ_5:65;
A298: RB2/.1 = p2 by FINSEQ_5:15;
L~Rev Red2 = L~Red2 by SPPOL_2:22;
then
A299: L~RB2 = L~Red2 \/ LSeg(p2,u3) by A278,SPPOL_2:20;
then
A300: LSeg(p2,f/.(len f -' 1)) /\ L~RB2 = {} \/ LSeg(p2,f/.(len f -' 1)) /\
LSeg(u3,p2) by A284,XBOOLE_1:23
.={ p2 } by A88,A97,A255,SPRECT_1:9,SPRECT_3:10;
<*u3*> is_in_the_area_of f by A243,A251,SPRECT_3:46;
then Red2 is_in_the_area_of f by A243,A251,SPRECT_3:52;
then Rev Red2 is_in_the_area_of f by SPRECT_3:51;
then
A301: RB2 is_in_the_area_of f by A160,SPRECT_2:24;
1 in dom Red1 by FINSEQ_5:6;
then
A302: RB1/.1 = u1 by A288,FINSEQ_4:68;
len <*p1*> = 1 by FINSEQ_1:39;
then len RB1 = len Red1 + 1 by FINSEQ_1:22;
then
A303: RB1/.len RB1 = p1 by FINSEQ_4:67;
A304: L~RB1 = L~Red1 \/ LSeg(u2,p1) by A287,SPPOL_2:19;
then
A305: LSeg(p1,f/.2) /\ L~RB1 = {} \/ LSeg(p1,f/.2) /\ LSeg(u2,p1) by A293,
XBOOLE_1:23
.={ p1 } by A163,A228,A268,SPRECT_1:10,SPRECT_3:10;
<*u2*> is_in_the_area_of f by A243,A264,SPRECT_3:46;
then Red1 is_in_the_area_of f by A243,A264,SPRECT_3:52;
then
A306: RB1 is_in_the_area_of f by A231,SPRECT_2:24;
A307: L~Red9 is_an_arc_of z1,z2 by A50,A53,TOPREAL4:2;
L~Red9 /\ L~SpStSeq L~f is closed by TOPS_1:8;
then u1 in L~Red9 /\ L~SpStSeq L~f by A54,A55,A56,A307,JORDAN5C:def 2;
then u1 in L~SpStSeq L~f by XBOOLE_0:def 4;
then u1 in (LSeg(NW-corner L~f,NE-corner L~f) \/ LSeg(NE-corner L~f,
SE-corner L~f)) \/ (LSeg(SE-corner L~f,SW-corner L~f) \/ LSeg(SW-corner L~f,
NW-corner L~f)) by SPRECT_1:41;
then
A308: u1 in LSeg(NW-corner L~f,NE-corner L~f) \/ LSeg(NE-corner L~f,
SE-corner L~f) or u1 in LSeg(SE-corner L~f,SW-corner L~f) \/ LSeg(SW-corner L~f
,NW-corner L~f) by XBOOLE_0:def 3;
A309: N-most L~f c= LSeg(NW-corner L~f,NE-corner L~f) by XBOOLE_1:17;
A310: A in N-most L~f by PSCOMP_1:42;
then LSeg(NW-corner L~f,NE-corner L~f) = LSeg(NW-corner L~f,A) \/ LSeg(A,
NE-corner L~f) by A309,TOPREAL1:5;
then
A311: u1 in LSeg(NW-corner L~f,NE-corner L~f) implies u1 in LSeg(NW-corner
L~f,A) or u1 in LSeg(A,NE-corner L~f) by XBOOLE_0:def 3;
per cases by A308,A311,XBOOLE_0:def 3;
suppose
A312: u1 in LSeg(NW-corner L~f,A);
A313: NW-corner L~f in LSeg(NW-corner L~f,NE-corner L~f) by RLTOPSP1:68;
then LSeg(NW-corner L~f,A) c= LSeg(NW-corner L~f,NE-corner L~f) by A309
,A310,TOPREAL1:6;
then LSeg(NW-corner L~f,u1) c= LSeg(NW-corner L~f,NE-corner L~f) by A312
,A313,TOPREAL1:6;
then LSeg(NW-corner L~f,u1) c= L~SpStSeq L~f by A66,XBOOLE_1:1;
then
A314: LSeg(NW-corner L~f,u1) /\ L~Red1 c= { u1 } by A296,XBOOLE_1:26;
A315: A`2 = N-bound L~f by EUCLID:52;
A316: NW-corner L~f in LSeg(NW-corner L~f,A) by RLTOPSP1:68;
then LSeg(NW-corner L~f,u1) misses LSeg(u2,p1) by A269,A312,TOPREAL1:6
,XBOOLE_1:63;
then
A317: LSeg(NW-corner L~f,u1) /\ LSeg(u2,p1) = {} by XBOOLE_0:def 7;
u1 in LSeg(NW-corner L~f,u1) by RLTOPSP1:68;
then u1 in LSeg(NW-corner L~f,u1) /\ L~Red1 by A294,XBOOLE_0:def 4;
then { u1 } c= LSeg(NW-corner L~f,u1) /\ L~Red1 by ZFMISC_1:31;
then LSeg(NW-corner L~f,u1) /\ L~Red1={ u1 } by A314,XBOOLE_0:def 10;
then
A318: LSeg(NW-corner L~f,u1) /\ L~RB1 = { u1 } \/ {} by A304,A317,XBOOLE_1:23
.= { u1 };
(NW-corner L~f)`2 = N-bound L~f by EUCLID:52;
then u1`2 = (NW-corner L~f)`2 by A312,A315,GOBOARD7:6;
then reconsider
M3 = <*NW-corner L~f*>^RB1 as S-Sequence_in_R2 by A234,A302,A318,
SPRECT_3:16;
A319: L~M3 = LSeg(NW-corner L~f,RB1/.1) \/ L~RB1 by SPPOL_2:20;
set i1 = (S-min L~f)..f, i2 = (E-min L~f)..f;
(N-max L~f)..f > 1 by A1,SPRECT_2:69;
then (N-max L~f)..f >= 1+1 by NAT_1:13;
then 2 <= (E-max L~f)..f by A1,SPRECT_2:70,XXREAL_0:2;
then
A320: 2 < i2 by A1,SPRECT_2:71,XXREAL_0:2;
LSeg(p1,f/.2) misses LSeg(NW-corner L~f,u1) by A196,A312,A316,TOPREAL1:6
,XBOOLE_1:63;
then LSeg(p1,f/.2) /\ LSeg(NW-corner L~f,u1) = {} by XBOOLE_0:def 7;
then
A321: LSeg(p1,f/.2) /\ L~M3 = {} \/ LSeg(p1,f/.2) /\ L~RB1 by A302,A319,
XBOOLE_1:23
.= { p1 } by A305;
A322: L~M3 = LSeg(NW-corner L~f,RB1/.1) \/ L~RB1 by SPPOL_2:20;
(W-min L~f)..f < len f by A1,SPRECT_2:76;
then
A323: i1 < len f by A1,SPRECT_2:74,XXREAL_0:2;
A324: E-min L~f in rng f by SPRECT_2:45;
then
A325: i2 in dom f by FINSEQ_4:20;
then
A326: i2 <= len f by FINSEQ_3:25;
then reconsider M4 = mid(f,2,i2) as S-Sequence_in_R2 by A320,JORDAN4:40;
L~M4 misses L~Red by A57,A245,A325,SPRECT_3:18,XBOOLE_1:63;
then
A327: L~M4 misses L~Red1 by A264,JORDAN3:41,XBOOLE_1:63;
(S-max L~f)..f < i1 by A1,SPRECT_2:73;
then
A328: i2 < i1 by A1,SPRECT_2:72,XXREAL_0:2;
then
A329: 2 < i1 by A320,XXREAL_0:2;
then 1 < i1 by XXREAL_0:2;
then reconsider M1 = mid(f,i1,len f) as S-Sequence_in_R2 by A323,JORDAN4:40
;
A330: L~M1 misses L~M4 by A328,A323,A320,SPRECT_2:47;
A331: L~M1 misses LSeg(p1,f/.2) by A173,A323,A329;
A332: len M1 >= 2 by TOPREAL1:def 8;
A333: M4/.1 = f/.2 by A57,A325,SPRECT_2:8;
L~M4 misses LSeg(u2,p1) by A270,A320,A326;
then
A334: L~RB1 misses L~M4 by A304,A327,XBOOLE_1:70;
A335: LSeg(NW-corner L~f,u1) c= LSeg(NW-corner L~f,A) by A312,A316,TOPREAL1:6;
A336: now
A337: LSeg(NW-corner L~f,A) /\ L~f = {A} by PSCOMP_1:43;
assume L~f meets LSeg(NW-corner L~f,u1);
then consider u being object such that
A338: u in L~f and
A339: u in LSeg(NW-corner L~f,u1) by XBOOLE_0:3;
reconsider u as Point of TOP-REAL 2 by A338;
u in LSeg(NW-corner L~f,A) /\ L~f by A335,A338,A339,XBOOLE_0:def 4;
then u = A by A337,TARSKI:def 1;
hence contradiction by A239,A312,A338,A339,SPRECT_3:6;
end;
then L~M4 misses LSeg(NW-corner L~f,u1) by A57,A325,SPRECT_3:18,XBOOLE_1:63
;
then
A340: L~M3 misses L~M4 by A302,A319,A334,XBOOLE_1:70;
A341: S-min L~f in rng f by SPRECT_2:41;
then
A342: i1 in dom f by FINSEQ_4:20;
then
A343: M1 is_in_the_area_of f by A58,SPRECT_2:23;
A344: (M1/.len M1)`2 = (f/.len f)`2 by A58,A342,SPRECT_2:9
.= (f/.1)`2 by FINSEQ_6:def 1
.= N-bound L~f by A1,EUCLID:52;
(M1/.1)`2 = (f/.i1)`2 by A58,A342,SPRECT_2:8
.= (S-min L~f)`2 by A341,FINSEQ_5:38
.= S-bound L~f by EUCLID:52;
then
A345: M1 is_a_v.c._for f by A343,A344,SPRECT_2:def 3;
A346: <*NW-corner L~f*>^RB1 is_in_the_area_of f by A63,A306,SPRECT_2:24;
1 < i1 by A329,XXREAL_0:2;
then
A347: L~M1 misses LSeg(u2,p1) by A270,A323;
A348: M3/.len M3 = p1 by A303,SPRECT_3:1;
LSeg(p1,f/.2) /\ L~M4 = { f/.2 } by A191,A320,A326;
then reconsider
M2 = M3^M4 as S-Sequence_in_R2 by A80,A170,A348,A333,A340,A321,SPRECT_3:21;
M2 = <*NW-corner L~f*>^(RB1^mid(f,2,i2)) by FINSEQ_1:32;
then
A349: (M2/.1)`1 = (NW-corner L~f)`1 by FINSEQ_5:15
.= W-bound L~f by EUCLID:52;
mid(f,2,i2) is_in_the_area_of f by A57,A325,SPRECT_2:23;
then
A350: M2 is_in_the_area_of f by A346,SPRECT_2:24;
(M2/.len M2)`1 = (mid(f,2,i2)/.len mid(f,2,i2))`1 by SPRECT_3:1
.= (f/.i2)`1 by A57,A325,SPRECT_2:9
.= (E-min L~f)`1 by A324,FINSEQ_5:38
.= E-bound L~f by EUCLID:52;
then
A351: M2 is_a_h.c._for f by A350,A349,SPRECT_2:def 2;
A352: L~M2 = L~M3 \/ LSeg(M3/.len M3,M4/.1) \/ L~M4 by SPPOL_2:23;
len M2 >= 2 by TOPREAL1:def 8;
then L~M1 meets L~M2 by A332,A345,A351,SPRECT_2:29;
then L~M1 meets L~M3 \/ LSeg(M3/.len M3,M4/.1) by A352,A330,XBOOLE_1:70;
then
A353: L~M1 meets L~M3 by A348,A333,A331,XBOOLE_1:70;
L~M1 misses LSeg(NW-corner L~f,u1) by A58,A342,A336,SPRECT_3:18,XBOOLE_1:63
;
then L~M1 meets L~RB1 by A302,A353,A322,XBOOLE_1:70;
then L~M1 meets L~Red1 by A304,A347,XBOOLE_1:70;
then L~M1 meets L~Red by A264,JORDAN3:41,XBOOLE_1:63;
hence contradiction by A58,A245,A342,SPRECT_3:18,XBOOLE_1:63;
end;
suppose that
A354: u1 in LSeg(A,NE-corner L~f) and
A355: N-min L~f = NW-corner L~f;
set i1 = (S-max L~f)..f, i2 = (E-max L~f)..f;
(N-max L~f)..f > 1 by A1,SPRECT_2:69;
then
A356: 1 < i2 by A1,SPRECT_2:70,XXREAL_0:2;
(S-min L~f)..f <= (W-min L~f)..f by A1,SPRECT_2:74;
then (S-max L~f)..f < (W-min L~f)..f by A1,SPRECT_2:73,XXREAL_0:2;
then (S-max L~f)..f + 1 <= (W-min L~f)..f by NAT_1:13;
then (S-max L~f)..f + 1 < len f by A1,SPRECT_2:76,XXREAL_0:2;
then
A357: i1 < len f -' 1 by A61,XREAL_1:6;
(E-max L~f)..f < (E-min L~f)..f by A1,SPRECT_2:71;
then
A358: i2 < i1 by A1,SPRECT_2:72,XXREAL_0:2;
then
A359: 1 < i1 by A356,XXREAL_0:2;
then reconsider M4 = mid(f,i1,len f -' 1) as S-Sequence_in_R2 by A61,A357,
JORDAN4:39;
A360: L~M4 misses LSeg(u3,p2) by A62,A257,A357,A359;
i1 < len f by A357,NAT_D:44;
then
A361: i2 < len f by A358,XXREAL_0:2;
then i2+1 <= len f by NAT_1:13;
then reconsider M2 = mid(f,1,i2) as S-Sequence_in_R2 by A356,JORDAN4:39;
A362: L~M2 misses L~M4 by A62,A358,A357,A356,SPRECT_2:47;
i2 < len f -' 1 by A358,A357,XXREAL_0:2;
then
A363: L~M2 misses LSeg(p2,f/.(len f -' 1)) by A105,A356;
A364: len M2 >= 2 by TOPREAL1:def 8;
A365: L~M2 misses LSeg(u3,p2) by A257,A356,A361;
A366: E-max L~f in rng f by SPRECT_2:46;
then
A367: i2 in dom f by FINSEQ_4:20;
then
A368: (M2/.len M2)`1 = (f/.i2)`1 by A15,SPRECT_2:9
.= (E-max L~f)`1 by A366,FINSEQ_5:38
.= E-bound L~f by EUCLID:52;
A369: S-max L~f in rng f by SPRECT_2:42;
then
A370: i1 in dom f by FINSEQ_4:20;
then L~M4 misses L~Red by A60,A245,SPRECT_3:18,XBOOLE_1:63;
then L~M4 misses L~Red2 by A251,JORDAN3:41,XBOOLE_1:63;
then
A371: L~RB2 misses L~M4 by A299,A360,XBOOLE_1:70;
A372: M2 is_in_the_area_of f by A15,A367,SPRECT_2:23;
(M2/.1)`1 = (f/.1)`1 by A15,A367,SPRECT_2:8
.= W-bound L~f by A1,A355,EUCLID:52;
then
A373: M2 is_a_h.c._for f by A372,A368,SPRECT_2:def 2;
A374: A`2 = N-bound L~f by EUCLID:52;
A375: (NE-corner L~f)`2 = N-bound L~f by EUCLID:52;
A376: M4/.len M4 = f/.(len f -' 1) by A60,A370,SPRECT_2:9;
then LSeg(M4/.len M4,p2) /\ L~M4={ M4/.len M4 } by A126,A357,A359;
then reconsider
M1 = M4^RB2 as S-Sequence_in_R2 by A78,A83,A96,A298,A300,A376,A371,
SPRECT_3:21;
mid(f,i1,len f -' 1) is_in_the_area_of f by A60,A370,SPRECT_2:23;
then
A377: M1 is_in_the_area_of f by A301,SPRECT_2:24;
A378: (M1/.len M1)`2 = (RB2/.len RB2)`2 by SPRECT_3:1
.= N-bound L~f by A297,A354,A375,A374,GOBOARD7:6;
mid(f,i1,len f -' 1) is non empty by A60,A370,SPRECT_2:7;
then 1 in dom mid(f,i1,len f -' 1) by FINSEQ_5:6;
then (M1/.1)`2 = (mid(f,i1,len f -' 1)/.1)`2 by FINSEQ_4:68
.= (f/.i1)`2 by A60,A370,SPRECT_2:8
.= (S-max L~f)`2 by A369,FINSEQ_5:38
.= S-bound L~f by EUCLID:52;
then
A379: M1 is_a_v.c._for f by A377,A378,SPRECT_2:def 3;
A380: L~M1 = L~M4 \/ LSeg(M4/.len M4,p2) \/ L~RB2 by A298,SPPOL_2:23
.= L~M4 \/ (LSeg(M4/.len M4,p2) \/ L~RB2) by XBOOLE_1:4;
len M1 >= 2 by TOPREAL1:def 8;
then L~M1 meets L~M2 by A364,A379,A373,SPRECT_2:29;
then L~M2 meets L~RB2 \/ LSeg(p2,M4/.len M4) by A380,A362,XBOOLE_1:70;
then L~M2 meets L~RB2 by A376,A363,XBOOLE_1:70;
then L~M2 meets L~Red2 by A299,A365,XBOOLE_1:70;
then L~M2 meets L~Red by A251,JORDAN3:41,XBOOLE_1:63;
hence contradiction by A15,A245,A367,SPRECT_3:18,XBOOLE_1:63;
end;
suppose that
A381: u1 in LSeg(A,NE-corner L~f) and
A382: N-min L~f <> NW-corner L~f;
set i1 = (S-min L~f)..f, i2 = (E-max L~f)..f;
A383: (S-min L~f)..f <= (W-min L~f)..f by A1,SPRECT_2:74;
W-max L~f <> N-min L~f by A382,PSCOMP_1:61;
then (S-min L~f)..f < (W-max L~f)..f by A1,A383,SPRECT_2:75,XXREAL_0:2;
then (S-min L~f)..f + 1 <= (W-max L~f)..f by NAT_1:13;
then (S-min L~f)..f + 1 < len f by A1,SPRECT_2:77,XXREAL_0:2;
then
A384: i1 < len f -' 1 by A61,XREAL_1:6;
A385: N-min L~f in LSeg(NW-corner L~f,N-min L~f) by RLTOPSP1:68;
A386: (N-min L~f)`2 = (NW-corner L~f)`2 by PSCOMP_1:37;
(N-max L~f)..f > 1 by A1,SPRECT_2:69;
then
A387: 1 < i2 by A1,SPRECT_2:70,XXREAL_0:2;
(E-max L~f)..f < (E-min L~f)..f by A1,SPRECT_2:71;
then (E-max L~f)..f < (S-max L~f)..f by A1,SPRECT_2:72,XXREAL_0:2;
then
A388: i2 < i1 by A1,SPRECT_2:73,XXREAL_0:2;
then
A389: 1 < i1 by A387,XXREAL_0:2;
then reconsider M4 = mid(f,i1,len f -' 1) as S-Sequence_in_R2 by A61,A384,
JORDAN4:39;
A390: L~M4 misses LSeg(u3,p2) by A62,A257,A384,A389;
i1 < len f by A384,NAT_D:44;
then
A391: i2 < len f by A388,XXREAL_0:2;
then i2+1 <= len f by NAT_1:13;
then reconsider M3 = mid(f,1,i2) as S-Sequence_in_R2 by A387,JORDAN4:39;
A392: L~M3 misses L~M4 by A62,A388,A384,A387,SPRECT_2:47;
i2 < len f -' 1 by A388,A384,XXREAL_0:2;
then
A393: L~M3 misses LSeg(p2,f/.(len f -' 1)) by A105,A387;
A394: L~M3 misses LSeg(u3,p2) by A257,A387,A391;
A395: E-max L~f in rng f by SPRECT_2:46;
then
A396: i2 in dom f by FINSEQ_4:20;
then
A397: M3/.1 = N-min L~f by A1,A15,SPRECT_2:8;
A398: S-min L~f in rng f by SPRECT_2:41;
then
A399: i1 in dom f by FINSEQ_4:20;
then L~M4 misses L~Red by A60,A245,SPRECT_3:18,XBOOLE_1:63;
then L~M4 misses L~Red2 by A251,JORDAN3:41,XBOOLE_1:63;
then
A400: L~RB2 misses L~M4 by A299,A390,XBOOLE_1:70;
A401: M4/.len M4 = f/.(len f -' 1) by A60,A399,SPRECT_2:9;
then LSeg(M4/.len M4,p2) /\ L~M4={ M4/.len M4 } by A126,A384,A389;
then reconsider
M1 = M4^RB2 as S-Sequence_in_R2 by A78,A83,A96,A298,A300,A401,A400,
SPRECT_3:21;
A402: L~M1 = L~M4 \/ LSeg(M4/.len M4,p2) \/ L~RB2 by A298,SPPOL_2:23
.= L~M4 \/ (LSeg(M4/.len M4,p2) \/ L~RB2) by XBOOLE_1:4;
1 in dom M3 by FINSEQ_5:6;
then N-min L~f in L~M3 by A397,SPPOL_2:44;
then N-min L~f in LSeg(NW-corner L~f,N-min L~f) /\ L~M3 by A385,
XBOOLE_0:def 4;
then
A403: {N-min L~f} c= LSeg(NW-corner L~f,N-min L~f) /\ L~M3 by ZFMISC_1:31;
A404: LSeg(NW-corner L~f, N-min L~f) /\ L~f = {N-min L~f} by PSCOMP_1:43;
then LSeg(NW-corner L~f,N-min L~f) /\ L~M3 c= { N-min L~f } by A15,A396,
SPRECT_3:18,XBOOLE_1:26;
then LSeg(NW-corner L~f,N-min L~f) /\ L~M3={ N-min L~f } by A403,
XBOOLE_0:def 10;
then reconsider
M2 = <*NW-corner L~f*>^M3 as S-Sequence_in_R2 by A382,A386,A397,SPRECT_3:16
;
A405: (M2/.1)`1 = (NW-corner L~f)`1 by FINSEQ_5:15
.= W-bound L~f by EUCLID:52;
A406: now
assume LSeg(NW-corner L~f,N-min L~f) meets L~M4;
then
A407: LSeg(NW-corner L~f,N-min L~f) /\ L~M4 <> {} by XBOOLE_0:def 7;
LSeg(NW-corner L~f,N-min L~f) /\ L~M4 c= { N-min L~f } by A60,A399,A404,
SPRECT_3:18,XBOOLE_1:26;
then LSeg(NW-corner L~f,N-min L~f) /\ L~M4 = { N-min L~f } by A407,
ZFMISC_1:33;
then N-min L~f in LSeg(NW-corner L~f,N-min L~f) /\ L~M4 by TARSKI:def 1;
then N-min L~f in L~M4 by XBOOLE_0:def 4;
hence contradiction by A1,A62,A384,A389,SPRECT_3:30;
end;
A408: A`2 = N-bound L~f by EUCLID:52;
A409: (NE-corner L~f)`2 = N-bound L~f by EUCLID:52;
mid(f,1,i2) is_in_the_area_of f by A15,A396,SPRECT_2:23;
then
A410: M2 is_in_the_area_of f by A63,SPRECT_2:24;
(M2/.len M2)`1 = (mid(f,1,i2)/.len mid(f,1,i2))`1 by SPRECT_3:1
.= (f/.i2)`1 by A15,A396,SPRECT_2:9
.= (E-max L~f)`1 by A395,FINSEQ_5:38
.= E-bound L~f by EUCLID:52;
then
A411: M2 is_a_h.c._for f by A410,A405,SPRECT_2:def 2;
A412: L~M2 = LSeg(NW-corner L~f,M3/.1) \/ L~M3 by SPPOL_2:20;
mid(f,i1,len f -' 1) is_in_the_area_of f by A60,A399,SPRECT_2:23;
then
A413: M1 is_in_the_area_of f by A301,SPRECT_2:24;
A414: (M1/.len M1)`2 = u1`2 by A297,SPRECT_3:1
.= N-bound L~f by A381,A409,A408,GOBOARD7:6;
mid(f,i1,len f -' 1) is non empty by A60,A399,SPRECT_2:7;
then 1 in dom mid(f,i1,len f -' 1) by FINSEQ_5:6;
then (M1/.1)`2 = (mid(f,i1,len f -' 1)/.1)`2 by FINSEQ_4:68
.= (f/.i1)`2 by A60,A399,SPRECT_2:8
.= (S-min L~f)`2 by A398,FINSEQ_5:38
.= S-bound L~f by EUCLID:52;
then
A415: M1 is_a_v.c._for f by A413,A414,SPRECT_2:def 3;
A416: len M1 >= 2 by TOPREAL1:def 8;
now
NW-corner L~f in LSeg(NW-corner L~f,NE-corner L~f) by RLTOPSP1:68;
then LSeg(NW-corner L~f,A) c= LSeg(NW-corner L~f,NE-corner L~f) by A309
,A310,TOPREAL1:6;
then LSeg(NW-corner L~f,N-min L~f) c= L~SpStSeq L~f by A66,XBOOLE_1:1;
then
A417: LSeg(NW-corner L~f,N-min L~f) /\ L~Red2 c= { u1 } by A286,XBOOLE_1:26;
assume LSeg(NW-corner L~f,N-min L~f) meets L~Red2;
then LSeg(NW-corner L~f,N-min L~f) /\ L~Red2 <> {} by XBOOLE_0:def 7;
then LSeg(NW-corner L~f,N-min L~f) /\ L~Red2 = { u1} by A417,ZFMISC_1:33;
then u1 in LSeg(NW-corner L~f,N-min L~f) /\ L~Red2 by TARSKI:def 1;
then u1 in LSeg(NW-corner L~f,N-min L~f) by XBOOLE_0:def 4;
then
A418: u1 in LSeg(NW-corner L~f,A) /\ LSeg(A,NE-corner L~f) by A381,
XBOOLE_0:def 4;
LSeg(NW-corner L~f,A) /\ LSeg(A,NE-corner L~f) = {A} by A309,A310,
TOPREAL1:8;
then u1 = A by A418,TARSKI:def 1;
hence contradiction by A239,SPRECT_1:11;
end;
then LSeg(NW-corner L~f,N-min L~f) misses L~RB2 by A256,A299,XBOOLE_1:70;
then LSeg(NW-corner L~f,N-min L~f) misses LSeg(M4/.len M4,p2) \/ L~RB2 by
A132,A401,XBOOLE_1:70;
then
A419: LSeg(NW-corner L~f,N-min L~f) misses L~M1 by A402,A406,XBOOLE_1:70;
len M2 >= 2 by TOPREAL1:def 8;
then
A420: L~M1 meets L~M2 by A416,A415,A411,SPRECT_2:29;
M3/.1 = f/.1 by A15,A396,SPRECT_2:8;
then L~M3 meets L~M1 by A1,A420,A419,A412,XBOOLE_1:70;
then L~M3 meets L~RB2 \/ LSeg(p2,M4/.len M4) by A402,A392,XBOOLE_1:70;
then L~M3 meets L~RB2 by A401,A393,XBOOLE_1:70;
then L~M3 meets L~Red2 by A299,A394,XBOOLE_1:70;
then L~M3 meets L~Red by A251,JORDAN3:41,XBOOLE_1:63;
hence contradiction by A15,A245,A396,SPRECT_3:18,XBOOLE_1:63;
end;
suppose that
A421: u1 in LSeg(NE-corner L~f,SE-corner L~f) and
A422: N-min L~f = W-max L~f;
A423: (RB2/.1)`1 = W-bound L~f by A96,A298,A422,EUCLID:52;
A424: (SE-corner L~f)`1 = E-bound L~f by EUCLID:52;
(NE-corner L~f)`1 = E-bound L~f by EUCLID:52;
then (RB2/.len RB2)`1 = E-bound L~f by A297,A421,A424,GOBOARD7:5;
then
A425: RB2 is_a_h.c._for f by A301,A423,SPRECT_2:def 2;
set i1 = (S-max L~f)..f, i2 = (N-max L~f)..f, i3 = (W-min L~f)..f;
A426: mid(f,i1,i2) = Rev mid(f,i2,i1) by FINSEQ_6:196;
(N-max L~f)..f <= (E-max L~f)..f by A1,SPRECT_2:70;
then (N-max L~f)..f < (E-min L~f)..f by A1,SPRECT_2:71,XXREAL_0:2;
then
A427: i2 < i1 by A1,SPRECT_2:72,XXREAL_0:2;
W-min L~f in rng f by SPRECT_2:43;
then i3 in dom f by FINSEQ_4:20;
then
A428: i3 <= len f by FINSEQ_3:25;
A429: 1 < i2 by A1,SPRECT_2:69;
A430: S-max L~f in rng f by SPRECT_2:42;
then
A431: i1 in dom f by FINSEQ_4:20;
then i1 <= len f by FINSEQ_3:25;
then mid(f,i2,i1) is S-Sequence_in_R2 by A429,A427,JORDAN4:40;
then reconsider M1 = mid(f,i1,i2) as S-Sequence_in_R2 by A426;
A432: len RB2 >= 2 by TOPREAL1:def 8;
(S-max L~f)..f < (S-min L~f)..f by A1,SPRECT_2:73;
then i3 > i1 by A1,SPRECT_2:74,XXREAL_0:2;
then i1 < len f by A428,XXREAL_0:2;
then L~mid(f,i2,i1) misses LSeg(u3,p2) by A257,A429,A427;
then
A433: L~M1 misses LSeg(u3,p2) by A426,SPPOL_2:22;
A434: N-max L~f in rng f by SPRECT_2:40;
then
A435: i2 in dom f by FINSEQ_4:20;
then
A436: (M1/.len M1)`2 = (f/.i2)`2 by A431,SPRECT_2:9
.= (N-max L~f)`2 by A434,FINSEQ_5:38
.= N-bound L~f by EUCLID:52;
A437: M1 is_in_the_area_of f by A431,A435,SPRECT_2:23;
(M1/.1)`2 = (f/.i1)`2 by A431,A435,SPRECT_2:8
.= (S-max L~f)`2 by A430,FINSEQ_5:38
.= S-bound L~f by EUCLID:52;
then
A438: M1 is_a_v.c._for f by A437,A436,SPRECT_2:def 3;
len M1 >= 2 by TOPREAL1:def 8;
then L~M1 meets L~RB2 by A432,A438,A425,SPRECT_2:29;
then L~M1 meets L~Red2 by A299,A433,XBOOLE_1:70;
then L~M1 meets L~Red by A251,JORDAN3:41,XBOOLE_1:63;
hence contradiction by A245,A431,A435,SPRECT_3:18,XBOOLE_1:63;
end;
suppose that
A439: u1 in LSeg(NE-corner L~f,SE-corner L~f) and
A440: N-min L~f <> W-max L~f;
set i1 = (S-max L~f)..f, i2 = (N-max L~f)..f, i3 = (W-min L~f)..f;
(W-max L~f)..f <= len f -' 1 by A1,NAT_D:49,SPRECT_2:77;
then
A441: i3 < len f -' 1 by A1,A440,SPRECT_2:75,XXREAL_0:2;
A442: W-min L~f in rng f by SPRECT_2:43;
then
A443: i3 in dom f by FINSEQ_4:20;
then
A444: 1 <= i3 by FINSEQ_3:25;
then reconsider M3 = mid(f,i3,len f -' 1) as S-Sequence_in_R2 by A61,A441,
JORDAN4:39;
L~M3 misses L~Red by A60,A245,A443,SPRECT_3:18,XBOOLE_1:63;
then
A445: L~M3 misses L~Red2 by A251,JORDAN3:41,XBOOLE_1:63;
L~M3 misses LSeg(u3,p2) by A62,A257,A441,A444;
then
A446: L~RB2 misses L~M3 by A299,A445,XBOOLE_1:70;
A447: M3/.len M3 = f/.(len f -' 1) by A60,A443,SPRECT_2:9;
then LSeg(M3/.len M3,p2) /\ L~M3={ M3/.len M3 } by A126,A441,A444;
then reconsider
M2 = M3^RB2 as S-Sequence_in_R2 by A78,A83,A96,A298,A300,A447,A446,
SPRECT_3:21;
mid(f,i3,len f -' 1) is_in_the_area_of f by A60,A443,SPRECT_2:23;
then
A448: M2 is_in_the_area_of f by A301,SPRECT_2:24;
A449: mid(f,i1,i2) = Rev mid(f,i2,i1) by FINSEQ_6:196;
A450: 1 < i2 by A1,SPRECT_2:69;
(N-max L~f)..f <= (E-max L~f)..f by A1,SPRECT_2:70;
then (N-max L~f)..f < (E-min L~f)..f by A1,SPRECT_2:71,XXREAL_0:2;
then
A451: i2 < i1 by A1,SPRECT_2:72,XXREAL_0:2;
A452: S-max L~f in rng f by SPRECT_2:42;
then
A453: i1 in dom f by FINSEQ_4:20;
then i1 <= len f by FINSEQ_3:25;
then mid(f,i2,i1) is S-Sequence_in_R2 by A450,A451,JORDAN4:40;
then reconsider M1 = mid(f,i1,i2) as S-Sequence_in_R2 by A449;
(S-max L~f)..f < (S-min L~f)..f by A1,SPRECT_2:73;
then
A454: i3 > i1 by A1,SPRECT_2:74,XXREAL_0:2;
then
A455: L~M1 misses L~M3 by A62,A450,A451,A441,SPRECT_2:50;
i3 < len f by A61,A441,NAT_1:13;
then i1 < len f by A454,XXREAL_0:2;
then L~mid(f,i2,i1) misses LSeg(u3,p2) by A257,A450,A451;
then
A456: L~M1 misses LSeg(u3,p2) by A449,SPPOL_2:22;
A457: len M1 >= 2 by TOPREAL1:def 8;
A458: N-max L~f in rng f by SPRECT_2:40;
then
A459: i2 in dom f by FINSEQ_4:20;
then
A460: (M1/.len M1)`2 = (f/.i2)`2 by A453,SPRECT_2:9
.= (N-max L~f)`2 by A458,FINSEQ_5:38
.= N-bound L~f by EUCLID:52;
i1 < len f -' 1 by A454,A441,XXREAL_0:2;
then L~mid(f,i2,i1) misses LSeg(p2,f/.(len f -' 1)) by A105,A450,A451;
then
A461: L~M1 misses LSeg(p2,f/.(len f -' 1)) by A449,SPPOL_2:22;
A462: (SE-corner L~f)`1 = E-bound L~f by EUCLID:52;
A463: (NE-corner L~f)`1 = E-bound L~f by EUCLID:52;
A464: (M2/.len M2)`1 = (RB2/.len RB2)`1 by SPRECT_3:1
.= E-bound L~f by A297,A439,A463,A462,GOBOARD7:5;
mid(f,i3,len f -' 1) is non empty by A60,A443,SPRECT_2:7;
then 1 in dom mid(f,i3,len f -' 1) by FINSEQ_5:6;
then (M2/.1)`1 = (mid(f,i3,len f -' 1)/.1)`1 by FINSEQ_4:68
.= (f/.i3)`1 by A60,A443,SPRECT_2:8
.= (W-min L~f)`1 by A442,FINSEQ_5:38
.= W-bound L~f by EUCLID:52;
then
A465: M2 is_a_h.c._for f by A448,A464,SPRECT_2:def 2;
A466: L~M2 = L~M3 \/ LSeg(M3/.len M3,p2) \/ L~RB2 by A298,SPPOL_2:23
.= L~M3 \/ (LSeg(M3/.len M3,p2) \/ L~RB2) by XBOOLE_1:4;
A467: M1 is_in_the_area_of f by A453,A459,SPRECT_2:23;
(M1/.1)`2 = (f/.i1)`2 by A453,A459,SPRECT_2:8
.= (S-max L~f)`2 by A452,FINSEQ_5:38
.= S-bound L~f by EUCLID:52;
then
A468: M1 is_a_v.c._for f by A467,A460,SPRECT_2:def 3;
len M2 >= 2 by TOPREAL1:def 8;
then L~M1 meets L~M2 by A457,A468,A465,SPRECT_2:29;
then L~M1 meets L~RB2 \/ LSeg(p2,M3/.len M3) by A466,A455,XBOOLE_1:70;
then L~M1 meets L~RB2 by A447,A461,XBOOLE_1:70;
then L~M1 meets L~Red2 by A299,A456,XBOOLE_1:70;
then L~M1 meets L~Red by A251,JORDAN3:41,XBOOLE_1:63;
hence contradiction by A245,A453,A459,SPRECT_3:18,XBOOLE_1:63;
end;
suppose
A469: u1 in LSeg(SE-corner L~f,SW-corner L~f);
A470: (SW-corner L~f)`2 = S-bound L~f by EUCLID:52;
(SE-corner L~f)`2 = S-bound L~f by EUCLID:52;
then (RB1/.1)`2 = S-bound L~f by A302,A469,A470,GOBOARD7:6;
then
A471: RB1 is_a_v.c._for f by A170,A303,A306,SPRECT_2:def 3;
A472: len RB1 >= 2 by TOPREAL1:def 8;
set i1 = (E-min L~f)..f, i2 = (W-min L~f)..f;
A473: mid(f,i2,i1) = Rev mid(f,i1,i2) by FINSEQ_6:196;
(E-min L~f)..f <= (S-max L~f)..f by A1,SPRECT_2:72;
then (E-min L~f)..f < (S-min L~f)..f by A1,SPRECT_2:73,XXREAL_0:2;
then
A474: i1 < i2 by A1,SPRECT_2:74,XXREAL_0:2;
(N-max L~f)..f > 1 by A1,SPRECT_2:69;
then (E-max L~f)..f > 1 by A1,SPRECT_2:70,XXREAL_0:2;
then
A475: 1 < i1 by A1,SPRECT_2:71,XXREAL_0:2;
A476: W-min L~f in rng f by SPRECT_2:43;
then
A477: i2 in dom f by FINSEQ_4:20;
then
A478: i2 <= len f by FINSEQ_3:25;
then mid(f,i1,i2) is S-Sequence_in_R2 by A475,A474,JORDAN4:40;
then reconsider M2 = mid(f,i2,i1) as S-Sequence_in_R2 by A473;
L~mid(f,i1,i2) misses LSeg(u2,p1) by A270,A475,A474,A478;
then
A479: L~M2 misses LSeg(u2,p1) by A473,SPPOL_2:22;
A480: E-min L~f in rng f by SPRECT_2:45;
then
A481: i1 in dom f by FINSEQ_4:20;
then
A482: M2 is_in_the_area_of f by A477,SPRECT_2:23;
A483: (M2/.1)`1 = (f/.i2)`1 by A481,A477,SPRECT_2:8
.= (W-min L~f)`1 by A476,FINSEQ_5:38
.= W-bound L~f by EUCLID:52;
(M2/.len M2)`1 = (f/.i1)`1 by A481,A477,SPRECT_2:9
.= (E-min L~f)`1 by A480,FINSEQ_5:38
.= E-bound L~f by EUCLID:52;
then
A484: M2 is_a_h.c._for f by A482,A483,SPRECT_2:def 2;
len M2 >= 2 by TOPREAL1:def 8;
then L~RB1 meets L~M2 by A472,A471,A484,SPRECT_2:29;
then L~M2 meets L~Red1 by A304,A479,XBOOLE_1:70;
then L~M2 meets L~Red by A264,JORDAN3:41,XBOOLE_1:63;
hence contradiction by A245,A481,A477,SPRECT_3:18,XBOOLE_1:63;
end;
suppose
A485: u1 in LSeg(SW-corner L~f,NW-corner L~f);
A486: (SW-corner L~f)`1 = W-bound L~f by EUCLID:52;
set i1 = (S-min L~f)..f, i3 = (E-min L~f)..f;
A487: (NW-corner L~f)`1 = W-bound L~f by EUCLID:52;
(N-max L~f)..f > 1 by A1,SPRECT_2:69;
then (E-max L~f)..f > 1 by A1,SPRECT_2:70,XXREAL_0:2;
then (E-max L~f)..f >= 1+1 by NAT_1:13;
then
A488: 2 < i3 by A1,SPRECT_2:71,XXREAL_0:2;
A489: E-min L~f in rng f by SPRECT_2:45;
then
A490: i3 in dom f by FINSEQ_4:20;
then
A491: i3 <= len f by FINSEQ_3:25;
then reconsider M3 = mid(f,2,i3) as S-Sequence_in_R2 by A488,JORDAN4:40;
L~M3 misses L~Red by A57,A245,A490,SPRECT_3:18,XBOOLE_1:63;
then
A492: L~M3 misses L~Red1 by A264,JORDAN3:41,XBOOLE_1:63;
L~M3 misses LSeg(u2,p1) by A270,A488,A491;
then
A493: L~RB1 misses L~M3 by A304,A492,XBOOLE_1:70;
A494: M3/.1 = f/.2 by A57,A490,SPRECT_2:8;
then LSeg(p1,M3/.1) /\ L~M3={ M3/.1 } by A191,A488,A491;
then reconsider
M2 = RB1^M3 as S-Sequence_in_R2 by A80,A170,A303,A305,A494,A493,SPRECT_3:21
;
A495: (M2/.len M2)`1 = (mid(f,2,i3)/.len mid(f,2,i3))`1 by SPRECT_3:1
.= (f/.i3)`1 by A57,A490,SPRECT_2:9
.= (E-min L~f)`1 by A489,FINSEQ_5:38
.= E-bound L~f by EUCLID:52;
mid(f,2,i3) is_in_the_area_of f by A57,A490,SPRECT_2:23;
then
A496: M2 is_in_the_area_of f by A306,SPRECT_2:24;
1 in dom RB1 by FINSEQ_5:6;
then (M2/.1)`1 = (RB1/.1)`1 by FINSEQ_4:68
.= W-bound L~f by A302,A485,A487,A486,GOBOARD7:5;
then
A497: M2 is_a_h.c._for f by A496,A495,SPRECT_2:def 2;
A498: L~M2 = L~RB1 \/ LSeg(p1,M3/.1) \/ L~M3 by A303,SPPOL_2:23;
(W-min L~f)..f < len f by A1,SPRECT_2:76;
then
A499: i1 < len f by A1,SPRECT_2:74,XXREAL_0:2;
(E-min L~f)..f <= (S-max L~f)..f by A1,SPRECT_2:72;
then
A500: i3 < i1 by A1,SPRECT_2:73,XXREAL_0:2;
then
A501: 2 < i1 by A488,XXREAL_0:2;
then
A502: 1 < i1 by XXREAL_0:2;
then reconsider M1 = mid(f,i1,len f) as S-Sequence_in_R2 by A499,JORDAN4:40
;
A503: L~M1 misses L~M3 by A500,A499,A488,SPRECT_2:47;
A504: L~M1 misses LSeg(p1,f/.2) by A173,A499,A501;
A505: S-min L~f in rng f by SPRECT_2:41;
then
A506: i1 in dom f by FINSEQ_4:20;
then
A507: M1 is_in_the_area_of f by A58,SPRECT_2:23;
A508: (M1/.len M1)`2 = (f/.len f)`2 by A58,A506,SPRECT_2:9
.= (f/.1)`2 by FINSEQ_6:def 1
.= N-bound L~f by A1,EUCLID:52;
(M1/.1)`2 = (f/.i1)`2 by A58,A506,SPRECT_2:8
.= (S-min L~f)`2 by A505,FINSEQ_5:38
.= S-bound L~f by EUCLID:52;
then
A509: M1 is_a_v.c._for f by A507,A508,SPRECT_2:def 3;
A510: L~M1 misses LSeg(u2,p1) by A270,A499,A502;
A511: len M1 >= 2 by TOPREAL1:def 8;
len M2 >= 2 by TOPREAL1:def 8;
then L~M1 meets L~M2 by A511,A509,A497,SPRECT_2:29;
then L~M1 meets L~RB1 \/ LSeg(p1,M3/.1) by A498,A503,XBOOLE_1:70;
then L~M1 meets L~RB1 by A494,A504,XBOOLE_1:70;
then L~M1 meets L~Red1 by A304,A510,XBOOLE_1:70;
then L~M1 meets L~Red by A264,JORDAN3:41,XBOOLE_1:63;
hence contradiction by A58,A245,A506,SPRECT_3:18,XBOOLE_1:63;
end;
end;
Lm2: for f being non constant standard special_circular_sequence st f/.1 =
N-min L~f holds LeftComp f <> RightComp f
proof
let f be non constant standard special_circular_sequence such that
A1: f/.1 = N-min L~f;
per cases by REVROT_1:38;
suppose
f is clockwise_oriented;
hence thesis by A1,Lm1;
end;
suppose
A2: Rev f is clockwise_oriented;
A3: LeftComp Rev f = RightComp f by GOBOARD9:23;
A4: RightComp Rev f = LeftComp f by GOBOARD9:24;
N-min L~Rev f = N-min L~f by SPPOL_2:22
.= Rev f/.len f by A1,FINSEQ_5:65
.= Rev f/.len Rev f by FINSEQ_5:def 3
.= Rev f/.1 by FINSEQ_6:def 1;
hence thesis by A2,A3,A4,Lm1;
end;
end;
theorem
for f being non constant standard special_circular_sequence holds
LeftComp f <> RightComp f
proof
let f be non constant standard special_circular_sequence;
set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
N-min L~f in rng f by SPRECT_2:39;
then
A2: g/.1 = N-min L~g by A1,FINSEQ_6:92;
A3: RightComp g = RightComp f by REVROT_1:37;
LeftComp g = LeftComp f by REVROT_1:36;
hence thesis by A2,A3,Lm2;
end;