:: The First Part of Jordan's Theorem for Special Polygons
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received July 22, 1996
:: Copyright (c) 1996-2021 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, REAL_1, FUNCT_1, GOBOARD5, TOPREAL1, STRUCT_0,
EUCLID, RELAT_1, XXREAL_0, FINSEQ_1, GOBOARD2, TREES_1, TOPS_1, TARSKI,
XBOOLE_0, PRE_TOPC, CONNSP_3, RELAT_2, GOBOARD9, CONNSP_1, ARYTM_3,
CARD_1, RLTOPSP1, PARTFUN1, MATRIX_1, ZFMISC_1, MCART_1, ARYTM_1,
RCOMP_1, NAT_1, CONVEX1, CHORD;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, TOPREAL1, ORDINAL1, NUMBERS,
DOMAIN_1, XCMPLX_0, XREAL_0, STRUCT_0, REAL_1, NAT_1, NAT_D, PRE_TOPC,
FUNCT_1, PARTFUN1, FINSEQ_1, MATRIX_0, TOPS_1, CONNSP_1, RLVECT_1,
RLTOPSP1, EUCLID, GOBOARD2, GOBOARD5, GOBOARD9, CONNSP_3, GOBRD10,
XXREAL_0;
constructors DOMAIN_1, REAL_1, TOPS_1, CONNSP_1, GOBOARD2, GOBOARD9, CONNSP_3,
GOBRD10, GOBOARD1, NAT_D, RELSET_1, CONVEX1;
registrations SUBSET_1, RELSET_1, XXREAL_0, NAT_1, STRUCT_0, PRE_TOPC, EUCLID,
GOBOARD2, GOBOARD5, GOBRD11, JORDAN1, XREAL_0, ORDINAL1;
requirements NUMERALS, REAL, SUBSET, ARITHM;
definitions TARSKI;
equalities CONNSP_3, STRUCT_0;
expansions TARSKI;
theorems TARSKI, NAT_1, FINSEQ_1, SPPOL_1, GOBOARD7, GOBOARD8, GOBOARD9,
PRE_TOPC, CONNSP_1, SUBSET_1, EUCLID, CONNSP_3, TOPREAL1, GOBOARD5,
TOPREAL3, MATRIX_0, GOBRD10, GOBRD11, ZFMISC_1, XBOOLE_0, XBOOLE_1,
FINSEQ_3, XREAL_1, XXREAL_0, PARTFUN1, XREAL_0, NAT_D, ORDINAL1;
schemes MATRIX_0;
begin
reserve i,j,k,k1,k2,i1,i2,j1,j2 for Nat,
r,s for Real,
x for set,
f for non constant standard special_circular_sequence;
Lm1: (L~f)` = the carrier of ((TOP-REAL 2)|(L~f)`)
proof
(L~f)`=[#]((TOP-REAL 2)|(L~f)`) by PRE_TOPC:def 5
.=the carrier of ((TOP-REAL 2)|(L~f)`);
hence thesis;
end;
Lm2: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:22;
theorem Th1:
for i,j st i<=len GoB f & j<=width GoB f holds Int cell(GoB f,i,j )c=(L~f)`
by GOBOARD7:12,SUBSET_1:23;
theorem Th2:
for i,j st i<=len GoB f & j<=width GoB f holds Cl Down(Int cell(
GoB f,i,j),(L~f)`)=cell(GoB f,i,j)/\((L~f)`)
proof
let i,j;
reconsider V=Int cell(GoB f,i,j) as Subset of TOP-REAL 2;
reconsider B=(L~f)` as Subset of TOP-REAL 2;
assume
A1: i<=len GoB f & j<=width GoB f;
then Cl Down(V,B) =(Cl V) /\ B by Th1,CONNSP_3:29;
hence thesis by A1,GOBRD11:35;
end;
theorem Th3:
for i,j st i<=len GoB f & j<=width GoB f holds Cl Down(Int cell(
GoB f,i,j),(L~f)`) is connected & Down(Int cell(GoB f,i,j),(L~f)`)=Int cell(GoB
f,i,j)
proof
let i,j;
assume
A1: i<=len GoB f & j<=width GoB f;
then
Int cell(GoB f,i,j) is convex & Down(Int cell(GoB f,i,j),(L~f)`)=Int
cell (GoB f,i,j) by Th1,GOBOARD9:17,XBOOLE_1:28;
then Down(Int cell(GoB f,i,j),(L~f)`) is connected by CONNSP_1:23;
hence Cl Down(Int cell(GoB f,i,j),(L~f)`) is connected by CONNSP_1:19;
thus thesis by A1,Th1,XBOOLE_1:28;
end;
Lm3: Cl Down(LeftComp f,(L~f)`) is connected & Down(LeftComp f,(L~f)`)=
LeftComp f & Down(LeftComp f,(L~f)`) is a_component
proof
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
then
A1: ex B1 being Subset of (TOP-REAL 2)|((L~f)`) st B1 = LeftComp f & B1
is a_component by CONNSP_1:def 6;
A2: the carrier of (TOP-REAL 2)|((L~f)`) =(L~f)` by PRE_TOPC:8;
then Down(LeftComp f,(L~f)`)=LeftComp f by A1,XBOOLE_1:28;
then Down(LeftComp f,(L~f)`) is connected by A1,CONNSP_1:def 5;
hence Cl Down(LeftComp f,(L~f)`) is connected by CONNSP_1:19;
thus thesis by A1,A2,XBOOLE_1:28;
end;
Lm4: Cl Down(RightComp f,(L~f)`) is connected & Down(RightComp f,(L~f)`)=
RightComp f & Down(RightComp f,(L~f)`) is a_component
proof
RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
then
A1: ex B1 being Subset of (TOP-REAL 2)|((L~f)`) st B1 = RightComp f & B1
is a_component by CONNSP_1:def 6;
A2: the carrier of (TOP-REAL 2)|((L~f)`) =(L~f)` by PRE_TOPC:8;
then Down(RightComp f,(L~f)`)=RightComp f by A1,XBOOLE_1:28;
then Down(RightComp f,(L~f)`) is connected by A1,CONNSP_1:def 5;
hence Cl Down(RightComp f,(L~f)`) is connected by CONNSP_1:19;
thus thesis by A1,A2,XBOOLE_1:28;
end;
theorem Th4:
(L~f)`=union {Cl Down(Int cell(GoB f,i,j),(L~f)`): i<=len GoB f &
j<=width GoB f}
proof
A1: (the carrier of TOP-REAL 2) =union {cell(GoB f,i,j):i<=(len GoB f) & j<=
(width GoB f)} by GOBRD11:7;
A2: (L~f)`c= union {Cl Down(Int cell(GoB f,i,j),(L~f)`): i<=len GoB f & j<=
width GoB f}
proof
let x be object;
assume
A3: x in (L~f)`;
then consider Y being set such that
A4: x in Y & Y in {cell(GoB f,i,j):i<=len GoB f & j<=width GoB f} by A1,
TARSKI:def 4;
consider i,j such that
A5: Y=cell(GoB f,i,j) and
A6: i<=len GoB f & j<=width GoB f by A4;
reconsider Y0=Cl Down(Int cell(GoB f,i,j),(L~f)`) as set;
x in cell(GoB f,i,j)/\((L~f)`) by A3,A4,A5,XBOOLE_0:def 4;
then
A7: x in Y0 by A6,Th2;
Y0 in {Cl Down(Int cell(GoB f,i1,j1),(L~f)`): i1<=len GoB f & j1<=
width GoB f} by A6;
hence thesis by A7,TARSKI:def 4;
end;
union {Cl Down(Int cell(GoB f,i,j),(L~f)`): i<=len GoB f & j<=width GoB
f} c= (L~f)`
proof
let x be object;
assume x in union {Cl Down(Int cell(GoB f,i,j),(L~f)`): i<=len GoB f & j
<=width GoB f};
then consider Y being set such that
A8: x in Y & Y in {Cl Down(Int cell(GoB f,i,j),(L~f)`): i<=len GoB f
& j<=width GoB f} by TARSKI:def 4;
consider i,j such that
A9: Y= Cl Down(Int cell(GoB f,i,j),(L~f)`) and
i<=len GoB f and
j<=width GoB f by A8;
Cl Down(Int cell(GoB f,i,j),(L~f)`) c= the carrier of (TOP-REAL 2)|( L~f)`;
then Y c= (L~f)` by A9,Lm1;
hence thesis by A8;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Th5:
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`) is
a_union_of_components of (TOP-REAL 2)|((L~f)`) & Down(LeftComp f,(L~f)`)=
LeftComp f & Down(RightComp f,(L~f)`)=RightComp f
proof
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
then consider B1 being Subset of (TOP-REAL 2)|((L~f)`) such that
A1: B1 = LeftComp f and
A2: B1 is a_component by CONNSP_1:def 6;
RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
then consider B2 being Subset of (TOP-REAL 2)|((L~f)`) such that
A3: B2 = RightComp f and
A4: B2 is a_component by CONNSP_1:def 6;
A5: B2 is Subset of (L~f)` by Lm1;
then
A6: Down(RightComp f,(L~f)`) is a_component by A3,A4,XBOOLE_1:28;
A7: B1 is Subset of (L~f)` by Lm1;
then
Down(LeftComp f,(L~f)`) is a_component by A1,A2,XBOOLE_1:28;
hence thesis by A1,A7,A3,A5,A6,GOBRD11:3,XBOOLE_1:28;
end;
Lm5: for i1,j1,i2,j2 st i1<=len GoB f & j1<=width GoB f & i2<=len GoB f & j2<=
width GoB f & (i2=i1+1 or i1=i2+1)& j1=j2 holds Int cell(GoB f,i1,j1) c=
LeftComp f \/ RightComp f implies Int cell(GoB f,i2,j2) c= LeftComp f \/
RightComp f
proof
let i1,j1,i2,j2;
assume that
A1: i1<=len GoB f and
A2: j1<=width GoB f and
A3: i2<=len GoB f and
A4: j2<=width GoB f and
A5: i2=i1+1 or i1=i2+1 and
A6: j1=j2;
now
assume
A7: Int cell(GoB f,i1,j1) c= LeftComp f \/ RightComp f;
now
per cases by A5;
case
A8: i2=i1+1;
now
per cases;
case
ex k st 1<=k & k+1 <=len f & j2<>0 & j2<>width GoB f &
LSeg(f/.k,f/.(k+1))=LSeg((GoB f)*(i1+1,j2),(GoB f)*(i1+1,j2+1));
then consider k such that
A9: 1<=k & k+1 <=len f and
A10: j2<>0 and
A11: j2<>width GoB f and
A12: LSeg(f/.k,f/.(k+1))=LSeg((GoB f)*(i1+1,j2),(GoB f)*(i1+1, j2+1));
now
per cases by A12,SPPOL_1:8;
case
A13: f/.k=(GoB f)*(i1+1,j2)& f/.(k+1)= (GoB f)*(i1+1,j2+1);
A14: Int right_cell(f,k) c= RightComp f & RightComp f c=
LeftComp f \/ RightComp f by A9,GOBOARD9:25,XBOOLE_1:7;
j2=0+1 by A10,NAT_1:13;
then j2 in Seg width GoB f by A4,FINSEQ_1:1;
then [i1+1,j2] in Indices GoB f by A16,ZFMISC_1:87;
then right_cell(f,k) = cell(GoB f,i1+1,j2) by A9,A13,A17,
GOBOARD5:27;
hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f by
A14;
end;
case
A18: f/.k=(GoB f)*(i1+1,j2+1)& f/.(k+1)=(GoB f)*(i1+1,j2);
A19: Int left_cell(f,k) c= LeftComp f & LeftComp f c= LeftComp
f \/ RightComp f by A9,GOBOARD9:21,XBOOLE_1:7;
j2=0+1 by A10,NAT_1:13;
then j2 in Seg width GoB f by A4,FINSEQ_1:1;
then [i1+1,j2] in Indices GoB f by A21,ZFMISC_1:87;
then left_cell(f,k) = cell(GoB f,i1+1,j2) by A9,A18,A22,
GOBOARD5:30;
hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f by
A19;
end;
end;
hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f;
end;
case
A23: not ex k st 1<=k & k+1 <=len f & j2<>0 & j2<>width GoB f
& LSeg(f/.k,f/.(k+1))=LSeg((GoB f)*(i1+1,j2),(GoB f)*(i1+1,j2+1));
now
per cases by A23;
case
A24: j2=0;
reconsider p=|[((GoB f)*(i1+1,1))`1,((GoB f)*(i1+1,1))`2-1]|
as Point of TOP-REAL 2;
A25: 1=0+1 by NAT_1:13;
A33: now
per cases by A3,A8,A32,XXREAL_0:1;
case
A34: i1>=1 & i1+1=1 & i1+1=len GoB f;
A40: i1=0+1 by NAT_1:13;
A65: now
per cases by A3,A8,A64,XXREAL_0:1;
case
A66: i1>=1 & i1+1=1 & i1+1=len GoB f;
A72: i10 & j2<>width GoB f & not ex k st 1<=k & k+1 <=
len f & LSeg(f/.k,f/.(k+1)) =LSeg((GoB f)*(i1+1,j2),(GoB f)*(i1+1,j2+1));
then
A86: j2LSeg(f,k)
proof
let k;
assume
A88: 1<=k & k+1<=len f;
then LSeg(f,k)=LSeg(f/.k,f/.(k+1)) by TOPREAL1:def 3;
hence thesis by A85,A88;
end;
then
A89: 1 <= i1+1 & i1+1 <= len GoB f & 1 <= j2 & j2+1 <= width
GoB f implies not 1/2*((GoB f)*(i1+1,j2)+(GoB f)*(i1+1,j2+1)) in L~f by
GOBOARD7:39;
reconsider p=1/2*((GoB f)*(i1+1,j2)+(GoB f)*(i1+1,j2+1)) as
Point of TOP-REAL 2;
A90: p`2=1/2*((GoB f)*(i1+1,j2)+(GoB f)*(i1+1,j2+1))`2 by TOPREAL3:4
.=1/2*(((GoB f)*(i1+1,j2))`2+((GoB f)*(i1+1,j2+1))`2) by
TOPREAL3:2;
reconsider P={p} as Subset of TOP-REAL 2;
A91: 1=0+1 by NAT_1:13;
A109: now
per cases by A3,A8,A108,XXREAL_0:1;
case
A110: i1>=1 & i1+1=1 & i1+1=len GoB f;
A118: i10 & j2<>width GoB f &
LSeg(f/.k,f/.(k+1)) =LSeg((GoB f)*(i2+1,j2),(GoB f)*(i2+1,j2+1));
then consider k such that
A134: 1<=k & k+1 <=len f and
A135: j2<>0 and
A136: j2<>width GoB f and
A137: LSeg(f/.k,f/.(k+1)) =LSeg((GoB f)*(i1-'1+1,j2),(GoB f)*(
i1-'1+1,j2 +1)) by A133;
now
per cases by A137,SPPOL_1:8;
case
A138: f/.k=(GoB f)*(i1-'1+1,j2) & f/.(k+1)= (GoB f)*(i1-'1 +1,j2+1);
A139: Int left_cell(f,k) c= LeftComp f & LeftComp f c=
LeftComp f \/ RightComp f by A134,GOBOARD9:21,XBOOLE_1:7;
j2=0+1 by A135,NAT_1:13;
then j2 in Seg width GoB f by A4,FINSEQ_1:1;
then [i1-'1+1,j2] in Indices GoB f by A141,ZFMISC_1:87;
then left_cell(f,k) = cell(GoB f,i1-'1,j2) by A134,A138,A142,
GOBOARD5:27;
hence Int cell(GoB f,i1-'1,j2) c= LeftComp f \/ RightComp f by
A139;
end;
case
A143: f/.k=(GoB f)*(i1-'1+1,j2+1) & f/.(k+1)= (GoB f)*(i1 -'1+1,j2);
A144: Int right_cell(f,k) c= RightComp f & RightComp f c=
LeftComp f \/ RightComp f by A134,GOBOARD9:25,XBOOLE_1:7;
j2=0+1 by A135,NAT_1:13;
then j2 in Seg width GoB f by A4,FINSEQ_1:1;
then [i1-'1+1,j2] in Indices GoB f by A146,ZFMISC_1:87;
then
right_cell(f,k) = cell(GoB f,i1-'1,j2) by A134,A143,A147,GOBOARD5:30;
hence Int cell(GoB f,i1-'1,j2) c= LeftComp f \/ RightComp f by
A144;
end;
end;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by A126,
NAT_D:34;
end;
case
A148: not ex k st 1<=k & k+1 <=len f & j2<>0 & j2<>width GoB f
& LSeg(f/.k,f/.(k+1)) =LSeg((GoB f)*(i2+1,j2),(GoB f)*(i2+1,j2+1));
now
per cases by A148;
case
A149: j2=0;
reconsider p=|[((GoB f)*(i2+1,1))`1,((GoB f)*(i2+1,1))`2-1]|
as Point of TOP-REAL 2;
A150: 10;
then
A159: i2+1+1<=len GoB f by NAT_1:13;
A160: p in {|[r,s]|:(GoB f)*(i2+1,1)`1<=r & r<=(GoB f)*(i2
+1+1,1)`1 }
proof
i2+10;
then
A169: 0+1<=i2 by NAT_1:13;
A170: p in {|[r,s]|:((GoB f)*(i2,1))`1<=r & r<=((GoB f)*(
i2+1,1))`1 }
proof
((GoB f)*(i2,1))`1<((GoB f)*(i2+1,1))`1 by A128,A150,A168
,A169,GOBOARD5:3;
hence thesis;
end;
p in {|[r,s]|:(GoB f)*(i2+1,1)`1<=r};
then p in v_strip(GoB f,i2+1) by A150,A168,GOBOARD5:9;
then p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A155,
XBOOLE_0:def 4;
then
A171: p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
i20;
then
A191: i2+1+1<=len GoB f by NAT_1:13;
A192: p in {|[r,s]|:(GoB f)*(i2+1,width GoB f)`1<=r & r<=(
GoB f)*(i2+1+1,width GoB f)`1}
proof
i2+10;
then
A201: 0+1<=i2 by NAT_1:13;
A202: p in {|[r,s]|:(GoB f)*(i2,width (GoB f))`1<=r & r<=(
GoB f)*(i2+1,width (GoB f))`1}
proof
((GoB f)*(i2,width (GoB f)))`1 <=(GoB f)*(i2+1,
width (GoB f))`1 by A128,A182,A200,A201,GOBOARD5:3;
hence thesis;
end;
p in {|[r,s]|: (GoB f)*(len GoB f,width (GoB f))`1<=
r} by A200;
then p in v_strip(GoB f,i2+1) by A182,A200,GOBOARD5:9;
then p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A187,
XBOOLE_0:def 4;
then
A203: p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
i20 & j2<>width GoB f & not ex k st 1<=k & k+1 <=
len f & LSeg(f/.k,f/.(k+1)) =LSeg((GoB f)*(i2+1,j2),(GoB f)*(i2+1,j2+1));
then
A212: j2LSeg(f,k)
proof
let k;
assume
A214: 1<=k & k+1<=len f;
then LSeg(f,k)=LSeg(f/.k,f/.(k+1)) by TOPREAL1:def 3;
hence thesis by A211,A214;
end;
then
A215: 1 <= i2+1 & i2+1 <= len GoB f & 1 <= j2 & j2+1 <= width
GoB f implies not 1/2*((GoB f)*(i2+1,j2)+(GoB f)*(i2+1,j2+1)) in L~f by
GOBOARD7:39;
reconsider p=1/2*((GoB f)*(i2+1,j2)+(GoB f)*(i2+1,j2+1)) as
Point of TOP-REAL 2;
A216: p`2=1/2*((GoB f)*(i2+1,j2)+(GoB f)*(i2+1,j2+1))`2 by TOPREAL3:4
.=1/2*(((GoB f)*(i2+1,j2))`2+((GoB f)*(i2+1,j2+1))`2) by
TOPREAL3:2;
reconsider P={p} as Subset of TOP-REAL 2;
A217: 1=0+1 by NAT_1:13;
A235: now
per cases by A1,A126,A234,XXREAL_0:1;
case
A236: i2>=1 & i2+1=1 & i2+1=len GoB f;
A244: i20 & i2<>len GoB f & LSeg
(f/.k,f/.(k+1))=LSeg((GoB f)*(i2,j1+1),(GoB f)*(i2+1,j1+1));
then consider k such that
A9: 1<=k & k+1 <=len f and
A10: i2<>0 and
A11: i2<>len GoB f and
A12: LSeg(f/.k,f/.(k+1))=LSeg((GoB f)*(i2,j1+1),(GoB f)*(i2+1, j1+1));
now
per cases by A12,SPPOL_1:8;
case
A13: f/.k=(GoB f)*(i2,j1+1)& f/.(k+1)= (GoB f)*(i2+1,j1+1);
A14: Int left_cell(f,k) c= LeftComp f & LeftComp f c= LeftComp
f \/ RightComp f by A9,GOBOARD9:21,XBOOLE_1:7;
i2=0+1 by A10,NAT_1:13;
then i2 in dom GoB f by A3,FINSEQ_3:25;
then [i2,j1+1] in Indices GoB f by A16,ZFMISC_1:87;
then left_cell(f,k) = cell(GoB f,i2,j1+1) by A9,A13,A17,
GOBOARD5:28;
hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f by
A14;
end;
case
A18: f/.k=(GoB f)*(i2+1,j1+1)& f/.(k+1)= (GoB f)*(i2,j1+1);
A19: Int right_cell(f,k) c= RightComp f & RightComp f c=
LeftComp f \/ RightComp f by A9,GOBOARD9:25,XBOOLE_1:7;
i2=0+1 by A10,NAT_1:13;
then i2 in dom GoB f by A3,FINSEQ_3:25;
then [i2,j1+1] in Indices GoB f by A21,ZFMISC_1:87;
then right_cell(f,k) = cell(GoB f,i2,j1+1) by A9,A18,A22,
GOBOARD5:29;
hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f by
A19;
end;
end;
hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f;
end;
case
A23: not ex k st 1<=k & k+1 <=len f & i2<>0 & i2<>len GoB f &
LSeg(f/.k,f/.(k+1))=LSeg((GoB f)*(i2,j1+1),(GoB f)*(i2+1,j1+1));
now
per cases by A23;
case
A24: i2=0;
reconsider p=|[((GoB f)*(1,j1+1))`1-1,((GoB f)*(1,j1+1))`2]|
as Point of TOP-REAL 2;
A25: 1=0+1 by NAT_1:13;
A33: now
per cases by A4,A8,A32,XXREAL_0:1;
case
A34: j1>=1 & j1+1=1 & j1+1=width GoB f;
A40: j1=0+1 by NAT_1:13;
A65: now
per cases by A4,A8,A64,XXREAL_0:1;
case
A66: j1>=1 & j1+1=1 & j1+1=width GoB f;
A72: j10 & i2<>len GoB f & not ex k st 1<=k & k+1 <=len
f & LSeg(f/.k,f/.(k+1)) =LSeg((GoB f)*(i2,j1+1),(GoB f)*(i2+1,j1+1));
then
A86: i2LSeg(f,k)
proof
let k;
assume
A88: 1<=k & k+1<=len f;
then LSeg(f,k)=LSeg(f/.k,f/.(k+1)) by TOPREAL1:def 3;
hence thesis by A85,A88;
end;
then
A89: 1 <= j1+1 & j1+1 <= width GoB f & 1 <= i2 & i2+1 <= len
GoB f implies not 1/2*((GoB f)*(i2,j1+1)+(GoB f)*(i2+1,j1+1)) in L~f by
GOBOARD7:40;
reconsider p=1/2*((GoB f)*(i2,j1+1)+(GoB f)*(i2+1,j1+1)) as
Point of TOP-REAL 2;
A90: p`1=1/2*((GoB f)*(i2,j1+1)+(GoB f)*(i2+1,j1+1))`1 by TOPREAL3:4
.=1/2*(((GoB f)*(i2,j1+1))`1+((GoB f)*(i2+1,j1+1))`1) by
TOPREAL3:2;
reconsider P={p} as Subset of TOP-REAL 2;
A91: 1=0+1 by NAT_1:13;
A109: now
per cases by A4,A8,A108,XXREAL_0:1;
case
A110: j1>=1 & j1+1=1 & j1+1=width GoB f;
A118: j10 & i2<>len GoB f &
LSeg(f/.k,f/.(k+1)) =LSeg((GoB f)*(i2,j2+1),(GoB f)*(i2+1,j2+1));
then consider k such that
A134: 1<=k & k+1 <=len f and
A135: i2<>0 and
A136: i2<>len GoB f and
A137: LSeg(f/.k,f/.(k+1)) =LSeg((GoB f)*(i2,j1-'1+1),(GoB f)*(
i2+1,j1-'1 +1)) by A133;
now
per cases by A137,SPPOL_1:8;
case
A138: f/.k=(GoB f)*(i2,j1-'1+1) & f/.(k+1)= (GoB f)*(i2+1, j1-'1+1);
A139: Int right_cell(f,k) c= RightComp f & RightComp f c=
LeftComp f \/ RightComp f by A134,GOBOARD9:25,XBOOLE_1:7;
i2=0+1 by A135,NAT_1:13;
then i2 in dom GoB f by A3,FINSEQ_3:25;
then [i2,j1-'1+1] in Indices GoB f by A141,ZFMISC_1:87;
then
right_cell(f,k) = cell(GoB f,i2,j1-'1) by A134,A138,A142,GOBOARD5:28;
hence Int cell(GoB f,i2,j1-'1) c= LeftComp f \/ RightComp f by
A139;
end;
case
A143: f/.k=(GoB f)*(i2+1,j1-'1+1) & f/.(k+1)= (GoB f)*(i2, j1-'1+1);
A144: Int left_cell(f,k) c= LeftComp f & LeftComp f c=
LeftComp f \/ RightComp f by A134,GOBOARD9:21,XBOOLE_1:7;
i2=0+1 by A135,NAT_1:13;
then i2 in dom GoB f by A3,FINSEQ_3:25;
then [i2,j1-'1+1] in Indices GoB f by A146,ZFMISC_1:87;
then left_cell(f,k) = cell(GoB f,i2,j1-'1) by A134,A143,A147,
GOBOARD5:29;
hence Int cell(GoB f,i2,j1-'1) c= LeftComp f \/ RightComp f by
A144;
end;
end;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by A126,
NAT_D:34;
end;
case
A148: not ex k st 1<=k & k+1 <=len f & i2<>0 & i2<>len GoB f &
LSeg(f/.k,f/.(k+1)) =LSeg((GoB f)*(i2,j2+1),(GoB f)*(i2+1,j2+1));
now
per cases by A148;
case
A149: i2=0;
reconsider p=|[((GoB f)*(1,j2+1))`1-1,((GoB f)*(1,j2+1))`2]|
as Point of TOP-REAL 2;
A150: 10;
then
A159: j2+1+1<=width GoB f by NAT_1:13;
A160: p in {|[s,r]| where s,r is Real:
(GoB f)*(1,j2+1)`2<=r & r<=(GoB f)*(1,
j2+1+1)`2 }
proof
j2+10;
then
A169: 0+1<=j2 by NAT_1:13;
A170: p in {|[s,r]| where s,r is Real:
((GoB f)*(1,j2))`2<=r & r<=((GoB f)*(1
,j2+1))`2 }
proof
((GoB f)*(1,j2))`2<((GoB f)*(1,j2+1))`2 by A128,A150,A168
,A169,GOBOARD5:4;
hence thesis;
end;
p in {|[s,r]| where s,r is Real:(GoB f)*(1,j2+1)`2<=r};
then p in h_strip(GoB f,j2+1) by A150,A168,GOBOARD5:6;
then p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A155,
XBOOLE_0:def 4;
then
A171: p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
j20;
then
A191: j2+1+1<=width GoB f by NAT_1:13;
A192: p in {|[s,r]|where s,r is Real
:(GoB f)*(len GoB f,j2+1)`2<=r & r<=(
GoB f)*(len GoB f,j2+1+1)`2}
proof
j2+10;
then
A201: 0+1<=j2 & j20 & i2<>len GoB f & not ex k st 1<=k & k+1 <=len
f & LSeg(f/.k,f/.(k+1)) =LSeg((GoB f)*(i2,j2+1),(GoB f)*(i2+1,j2+1));
then
A211: i2LSeg(f,k)
proof
let k;
assume
A213: 1<=k & k+1<=len f;
then LSeg(f,k)=LSeg(f/.k,f/.(k+1)) by TOPREAL1:def 3;
hence thesis by A210,A213;
end;
then
A214: 1 <= j2+1 & j2+1 <= width GoB f & 1 <= i2 & i2+1 <= len
GoB f implies not 1/2*((GoB f)*(i2,j2+1)+(GoB f)*(i2+1,j2+1)) in L~f by
GOBOARD7:40;
reconsider p=1/2*((GoB f)*(i2,j2+1)+(GoB f)*(i2+1,j2+1)) as
Point of TOP-REAL 2;
A215: p`1=1/2*((GoB f)*(i2,j2+1)+(GoB f)*(i2+1,j2+1))`1 by TOPREAL3:4
.=1/2*(((GoB f)*(i2,j2+1))`1+((GoB f)*(i2+1,j2+1))`1) by
TOPREAL3:2;
reconsider P={p} as Subset of TOP-REAL 2;
A216: 1=0+1 by NAT_1:13;
A234: now
per cases by A2,A126,A233,XXREAL_0:1;
case
A235: j2>=1 & j2+1=1 & j2+1=width GoB f;
A242: j2