Copyright (c) 1996 Association of Mizar Users
environ
vocabulary PRE_TOPC, SEQM_3, GOBOARD5, ARYTM_3, EUCLID, MCART_1, RELAT_1,
SUBSET_1, TOPREAL1, FINSEQ_1, GOBOARD2, TREES_1, TOPS_1, BOOLE, CONNSP_3,
RELAT_2, GOBOARD9, CONNSP_1, TARSKI, MATRIX_1, ARYTM_1, GOBRD10, FUNCT_1,
FINSEQ_4;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, TOPREAL1, GOBOARD1, NUMBERS,
XREAL_0, STRUCT_0, REAL_1, NAT_1, BINARITH, PRE_TOPC, FUNCT_1, FINSEQ_1,
FINSEQ_4, MATRIX_1, TOPS_1, CONNSP_1, EUCLID, GOBOARD2, GOBOARD5,
GOBOARD9, CONNSP_3, GOBRD10;
constructors REAL_1, BINARITH, TOPS_1, CONNSP_1, GOBOARD2, GOBOARD9, CONNSP_3,
GOBRD10, FINSEQ_4, MEMBERED;
clusters SUBSET_1, GOBOARD5, RELSET_1, PRE_TOPC, GOBOARD2, EUCLID, XREAL_0,
GOBRD11, NAT_1, MEMBERED;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
theorems TARSKI, NAT_1, FINSEQ_1, REAL_1, AXIOMS, SPPOL_1, FINSEQ_4, GOBOARD7,
GOBOARD8, GOBOARD9, PRE_TOPC, CONNSP_1, SUBSET_1, EUCLID, CONNSP_3,
TOPREAL1, GOBOARD5, SQUARE_1, TOPREAL3, MATRIX_1, BINARITH, GOBRD10,
GOBRD11, ZFMISC_1, XBOOLE_0, XBOOLE_1, JORDAN1, FINSEQ_3, XCMPLX_1;
schemes MATRIX_1;
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: for r holds 1/2*(r+r)=r
proof let r; 1/2*(r+r)=(r+r)/2 by XCMPLX_1:100;
hence thesis by XCMPLX_1:65;
end;
Lm2: (L~f)` = the carrier of ((TOP-REAL 2)|(L~f)`)
proof
(L~f)`=[#]((TOP-REAL 2)|(L~f)`) by PRE_TOPC:def 10
.=the carrier of ((TOP-REAL 2)|(L~f)`) by PRE_TOPC:12;
hence thesis;
end;
Lm3: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:25;
canceled;
theorem Th2: for i,j st i<=len GoB f & j<=width GoB f
holds Int cell(GoB f,i,j)c=(L~f)`
proof let i,j;assume i<=len GoB f & j<=width GoB f;
then Int cell(GoB f,i,j) misses (L~f) by GOBOARD7:14;
hence thesis by SUBSET_1:43;
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)`)=cell(GoB f,i,j)/\((L~f)`)
proof let i,j;assume A1:i<=len GoB f & j<=width GoB f;
reconsider V=Int cell(GoB f,i,j) as Subset of TOP-REAL 2;
reconsider B=(L~f)` as Subset of TOP-REAL 2;
V c= B by A1,Th2;
then Cl Down(V,B) =(Cl V) /\ B by CONNSP_3:30;
hence thesis by A1,GOBRD11:35;
end;
theorem
Th4: 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 A2:Int cell(GoB f,i,j) is connected by GOBOARD9:21;
A3: Int cell(GoB f,i,j) c= (L~f)` by A1,Th2;
then Down(Int cell(GoB f,i,j),(L~f)`)=Int cell(GoB f,i,j) by CONNSP_3:28;
then Down(Int cell(GoB f,i,j),(L~f)`) is connected by A2,CONNSP_1:24;
hence Cl Down(Int cell(GoB f,i,j),(L~f)`) is connected
by CONNSP_1:20;
thus thesis by A3,CONNSP_3:28;
end;
Lm4:Cl Down(LeftComp f,(L~f)`) is connected
& Down(LeftComp f,(L~f)`)=LeftComp f
& Down(LeftComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~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 & B1 is_a_component_of (TOP-REAL 2)|((L~f)`)
by CONNSP_1:def 6;
A2: the carrier of (TOP-REAL 2)|((L~f)`) =(L~f)` by JORDAN1:1;
then Down(LeftComp f,(L~f)`)=LeftComp f by A1,CONNSP_3: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:20;
thus thesis by A1,A2,CONNSP_3:28;
end;
Lm5:Cl Down(RightComp f,(L~f)`) is connected
& Down(RightComp f,(L~f)`)=RightComp f
& Down(RightComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
proof
RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
then consider B1 being Subset of (TOP-REAL 2)|((L~f)`) such that
A1:B1 = RightComp f & B1 is_a_component_of (TOP-REAL 2)|((L~f)`)
by CONNSP_1:def 6;
A2: the carrier of (TOP-REAL 2)|((L~f)`) =(L~f)` by JORDAN1:1;
then Down(RightComp f,(L~f)`)=RightComp f by A1,CONNSP_3: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:20;
thus thesis by A1,A2,CONNSP_3:28;
end;
theorem
Th5: (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;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) & (i<=len GoB f & j<=width GoB f) by A4;
A6: x in cell(GoB f,i,j)/\((L~f)`) by A3,A4,A5,XBOOLE_0:def 3;
reconsider Y0=Cl Down(Int cell(GoB f,i,j),(L~f)`) as set;
x in Y0 & Y0 in {Cl Down(Int cell(GoB f,i1,j1),(L~f)`):
i1<=len GoB f & j1<=width GoB f} by A5,A6,Th3;
hence x in union {Cl Down(Int cell(GoB f,i1,j1),(L~f)`):
i1<=len GoB f & j1<=width GoB f} by 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;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
A7: 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
A8: Y= Cl Down(Int cell(GoB f,i,j),(L~f)`) &
(i<=len GoB f & j<=width GoB f) by A7;
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 A8,Lm2;
hence x in (L~f)` by A7;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Th6: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
& B1 is_a_component_of ((TOP-REAL 2)|((L~f)`)) by CONNSP_1:def 6;
A2: B1 is Subset of (L~f)` by Lm2;
then A3:Down(LeftComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by A1,CONNSP_3:28;
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 A4:B2 = RightComp f
& B2 is_a_component_of ((TOP-REAL 2)|((L~f)`)) by CONNSP_1:def 6;
A5: B2 is Subset of (L~f)` by Lm2;
then Down(RightComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by A4,CONNSP_3:28;
hence thesis by A1,A2,A3,A4,A5,CONNSP_3:28,GOBRD11:3;
end;
Lm6: 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
A1: 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);
now assume A2:Int cell(GoB f,i1,j1) c= LeftComp f \/ RightComp f;
now per cases by A1;
case A3: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 A4: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 A4,SPPOL_1:25;
case A5:f/.k=(GoB f)*(i1+1,j2)& f/.(k+1)= (GoB f)*(i1+1,j2+1);
A6:Indices GoB f=[:dom GoB f,Seg width GoB f:] by MATRIX_1:def 5;
0<=i1 by NAT_1:18;
then 0+1<=i1+1 by AXIOMS:24;
then A7:i1+1 in dom GoB f by A1,A3,FINSEQ_3:27;
j2>0 by A4,NAT_1:19; then j2>=0+1 by NAT_1:38;
then j2 in Seg width GoB f by A1,FINSEQ_1:3;
then A8:[i1+1,j2] in Indices GoB f by A6,A7,ZFMISC_1:106;
j2<width GoB f by A1,A4,REAL_1:def 5;
then A9:j2+1<=width GoB f by NAT_1:38;
1<=j2+1 by NAT_1:29;
then j2+1 in Seg width GoB f by A9,FINSEQ_1:3;
then [i1+1,j2+1] in Indices GoB f by A6,A7,ZFMISC_1:106;
then A10:right_cell(f,k) = cell(GoB f,i1+1,j2)
by A4,A5,A8,GOBOARD5:28;
A11: Int right_cell(f,k) c= RightComp f by A4,GOBOARD9:28;
RightComp f c= LeftComp f \/ RightComp f by XBOOLE_1:7;
hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f
by A10,A11,XBOOLE_1:1;
case A12:f/.k=(GoB f)*(i1+1,j2+1)& f/.(k+1)=(GoB f)*(i1+1,j2);
A13:Indices GoB f=[:dom GoB f,Seg width GoB f:] by MATRIX_1:def 5;
0<=i1 by NAT_1:18;
then 0+1<=i1+1 by AXIOMS:24;
then A14:i1+1 in dom GoB f by A1,A3,FINSEQ_3:27;
j2>0 by A4,NAT_1:19; then j2>=0+1 by NAT_1:38;
then j2 in Seg width GoB f by A1,FINSEQ_1:3;
then A15:[i1+1,j2] in Indices GoB f by A13,A14,ZFMISC_1:106;
j2<width GoB f by A1,A4,REAL_1:def 5;
then A16:j2+1<=width GoB f by NAT_1:38;
1<=j2+1 by NAT_1:29;
then j2+1 in Seg width GoB f by A16,FINSEQ_1:3;
then [i1+1,j2+1] in Indices GoB f by A13,A14,ZFMISC_1:106;
then A17:left_cell(f,k) = cell(GoB f,i1+1,j2) by A4,A12,A15,GOBOARD5:31
;
A18: Int left_cell(f,k) c= LeftComp f by A4,GOBOARD9:24;
LeftComp f c= LeftComp f \/ RightComp f by XBOOLE_1:7;
hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f
by A17,A18,XBOOLE_1:1;
end;
hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f;
case A19: 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 A19;
case A20:j2=0;
reconsider p=|[((GoB f)*(i1+1,1))`1,((GoB f)*(i1+1,1))`2-1]| as
Point of TOP-REAL 2;
A21:1<width GoB f by GOBOARD7:35;
A22:1<len GoB f by GOBOARD7:34;
A23:1<=i1+1 by NAT_1:29;
then ((GoB f)*(i1+1,1))`2=((GoB f)*(1,1))`2 by A1,A3,A21,GOBOARD5:2
;
then A24:p`2=((GoB f)*(1,1))`2-1 by EUCLID:56;
p`2<p`2+1 by REAL_1:69;
then A25:p`2< ((GoB f)*(1,1))`2 by A24,XCMPLX_1:27;
A26:p in {p} by TARSKI:def 1;
reconsider P={p} as Subset of TOP-REAL 2;
(for q being Point of TOP-REAL 2
st q in P holds q`2<((GoB f)*(1,1))`2) implies
P misses L~f by GOBOARD8:23;
then A27: {p} c= (L~f)` by A25,SUBSET_1:43,TARSKI:def 1;
then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by A26,
JORDAN1:1;
p in {|[r,s]|:s<=(GoB f)*(1,1)`2}
proof
p=|[p`1,p`2]| by EUCLID:57;
hence thesis by A25;
end;
then A28:p in h_strip(GoB f,j2) by A20,A22,GOBOARD5:8;
0<=i1 by NAT_1:18;
then A29: i1=0 or i1>=0+1 by NAT_1:38;
now per cases by A1,A3,A29,REAL_1:def 5;
case A30:i1>=1 & i1+1<len GoB f;
then A31:1<=i1+1 & i1+1<len GoB f by NAT_1:29;
A32:1<=i1 & i1<len GoB f by A30,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i1,1)`1<=r & r<=(GoB f)*(i1+1,1)`1}
proof i1<i1+1 by NAT_1:38;
then ((GoB f)*(i1,1))`1<((GoB f)*(i1+1,1))`1 by A21,A30,GOBOARD5:
4;
hence thesis;
end;
then A33:p in v_strip(GoB f,i1) by A21,A32,GOBOARD5:9;
A34:i1+1+1<=len GoB f by A30,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i1+1,1)`1<=r & r<=(GoB f)*(i1+1+1,1)`1}
proof i1+1<i1+1+1 by NAT_1:38;
then ((GoB f)*(i1+1,1)`1<=((GoB f)*(i1+1,1))`1
& ((GoB f)*(i1+1,1))`1<=(GoB f)*(i1+1+1,1)`1)
by A21,A23,A34,GOBOARD5:4;
hence thesis;
end;
then p in v_strip(GoB f,i1+1) by A21,A31,GOBOARD5:9;
then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A28,A33,XBOOLE_0:
def 3
;
then p in cell(GoB f,i1,j2) &
p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i1+1,j2)/\((L~f)`) &
p in cell(GoB f,i1,j2)/\((L~f)`) by A26,A27,XBOOLE_0:def 3;
case A35:i1>=1 & i1+1=len GoB f;
A36: i1<i1+1 by NAT_1:38;
A37:1<=i1 & i1<len GoB f by A35,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i1,1)`1<=r & r<=(GoB f)*(i1+1,1)`1}
proof
((GoB f)*(i1,1))`1<((GoB f)*(i1+1,1))`1 by A21,A35,A36,GOBOARD5
:4;
hence thesis;
end;
then A38:p in v_strip(GoB f,i1) by A21,A37,GOBOARD5:9;
p in {|[r,s]|:(GoB f)*(i1+1,1)`1<=r};
then p in v_strip(GoB f,i1+1) by A21,A35,GOBOARD5:10;
then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A28,A38,XBOOLE_0:
def 3
;
then p in cell(GoB f,i1,j2) &
p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i1+1,j2)/\((L~f)`) &
p in cell(GoB f,i1,j2)/\((L~f)`) by A26,A27,XBOOLE_0:def 3;
case A39:i1=0 & i1+1<len GoB f;
then p in {|[r,s]|: r<=(GoB f)*(1,1)`1};
then A40:p in v_strip(GoB f,i1) by A21,A39,GOBOARD5:11;
A41:i1+1+1<=len GoB f by A39,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i1+1,1)`1<=r & r<=(GoB f)*(i1+1+1,1)`1}
proof i1+1<i1+1+1 by NAT_1:38;
then ((GoB f)*(i1+1,1)`1<=((GoB f)*(i1+1,1))`1
& ((GoB f)*(i1+1,1))`1<=(GoB f)*(i1+1+1,1)`1) by A21,A23,A41,
GOBOARD5:4;
hence thesis;
end;
then p in v_strip(GoB f,i1+1) by A21,A39,GOBOARD5:9;
then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A28,A40,XBOOLE_0:
def 3
;
then p in cell(GoB f,i1,j2) &
p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i1+1,j2)/\((L~f)`) &
p in cell(GoB f,i1,j2)/\((L~f)`) by A26,A27,XBOOLE_0:def 3;
case A42:i1=0 & i1+1=len GoB f;
then p in {|[r,s]|: r<=(GoB f)*(1,1)`1};
then A43:p in v_strip(GoB f,i1) by A21,A42,GOBOARD5:11;
p in {|[r,s]|:(GoB f)*(i1+1,1)`1<=r};
then p in v_strip(GoB f,i1+1) by A21,A42,GOBOARD5:10;
then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A28,A43,XBOOLE_0:
def 3
;
then p in cell(GoB f,i1,j2) &
p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i1+1,j2)/\((L~f)`) &
p in cell(GoB f,i1,j2)/\((L~f)`) by A26,A27,XBOOLE_0:def 3;
end;
then A44:p in Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`)
& p in Cl Down(Int cell(GoB f,i1,j2),(L~f)`) by A1,Th3;
A45:Down(LeftComp f,(L~f)`)=LeftComp f &
Down(RightComp f,(L~f)`)=RightComp f by Th6;
Down(Int cell(GoB f,i1,j2),(L~f)`)
c= LeftComp f \/ RightComp f by A1,A2,Th4;
then Down(Int cell(GoB f,i1,j2),(L~f)`)
c= Down(LeftComp f \/ RightComp f,(L~f)`)
by A45,GOBRD11:4;
then A46:Cl Down(Int cell(GoB f,i1,j2),(L~f)`)
c= Cl Down(LeftComp f \/ RightComp f,(L~f)`)
by PRE_TOPC:49;
A47:Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`) is connected
by A1,A3,Th4;
Down(LeftComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm4;
then Down(LeftComp f,(L~f)`) is closed by CONNSP_1:35;
then A48:Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`)
by PRE_TOPC:52;
Down(RightComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm5;
then Down(RightComp f,(L~f)`) is closed by CONNSP_1:35;
then A49:Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`)
by PRE_TOPC:52;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
=Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
then A50:Cl Down(LeftComp f \/ RightComp f,(L~f)`)
=Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A48,A49,PRE_TOPC:50;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
is a_union_of_components of (TOP-REAL 2)|((L~f)`) by Th6;
then A51:skl p1 c= Down(LeftComp f,(L~f)`)
\/ Down(RightComp f,(L~f)`) by A44,A46,A50,CONNSP_3:21;
Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`) c= skl p1
by A44,A47,GOBRD11:1;
then A52: Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`)
c= Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A51,XBOOLE_1:1;
A53:Down(Int cell(GoB f,i1+1,j2),(L~f)`)
c= Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`)
by PRE_TOPC:48;
Down(Int cell(GoB f,i1+1,j2),(L~f)`)=Int cell(GoB f,i1+1,j2)
by A1,A3,Th4;
hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f
by A45,A52,A53,XBOOLE_1:1;
case A54:j2=width GoB f;
reconsider p=|[((GoB f)*(i1+1,width GoB f))`1,
((GoB f)*(i1+1,width GoB f))`2+1]| as Point of TOP-REAL 2;
A55:1<width GoB f by GOBOARD7:35;
A56:1<len GoB f by GOBOARD7:34;
A57: 1<=1+i1 by NAT_1:29;
then ((GoB f)*(i1+1,width GoB f))`2
=((GoB f)*(1,width GoB f))`2 by A1,A3,A55,GOBOARD5:2;
then A58:p`2=((GoB f)*(1,width GoB f))`2+1 by EUCLID:56;
A59: ((GoB f)*(1,width GoB f))`2<((GoB f)*(1,width GoB f))`2+1
by REAL_1:69;
A60:((GoB f)*(1,width GoB f))`2<p`2 by A58,REAL_1:69;
A61:p in {p} by TARSKI:def 1;
reconsider P={p} as Subset of TOP-REAL 2;
(for q being Point of TOP-REAL 2
st q in P holds ((GoB f)*(1,width GoB f)`2)<q`2) implies
P misses L~f by GOBOARD8:24;
then A62: {p} c= (L~f)` by A58,A59,SUBSET_1:43,TARSKI:def 1;
then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by A61,
JORDAN1:1;
p in {|[r,s]|:(GoB f)*(1,width (GoB f))`2<=s}
proof
p=|[p`1,p`2]| by EUCLID:57;
hence thesis by A60;
end;
then A63:p in h_strip(GoB f,j2) by A54,A56,GOBOARD5:7;
0<=i1 by NAT_1:18;
then A64: i1=0 or i1>=0+1 by NAT_1:38;
now per cases by A1,A3,A64,REAL_1:def 5;
case A65:i1>=1 & i1+1<len GoB f;
then A66:1<=i1+1 & i1+1<len GoB f by NAT_1:29;
A67:1<=i1 & i1<len GoB f by A65,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i1,width GoB f)`1<=r &
r<=(GoB f)*(i1+1,width GoB f)`1}
proof i1<i1+1 by NAT_1:38;
then ((GoB f)*(i1,width GoB f))`1
<((GoB f)*(i1+1,width GoB f))`1 by A55,A65,GOBOARD5:4;
hence thesis;
end;
then A68:p in v_strip(GoB f,i1) by A55,A67,GOBOARD5:9;
A69:i1+1+1<=len GoB f by A65,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i1+1,width GoB f)`1<=r
& r<=(GoB f)*(i1+1+1,width GoB f)`1}
proof i1+1<i1+1+1 by NAT_1:38;
then ((GoB f)*(i1+1,width GoB f)`1
<=((GoB f)*(i1+1,width GoB f))`1
& ((GoB f)*(i1+1,width GoB f))`1
<=(GoB f)*(i1+1+1,width GoB f)`1) by A55,A57,A69,GOBOARD5:4;
hence thesis;
end;
then p in v_strip(GoB f,i1+1) by A55,A66,GOBOARD5:9;
then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A63,A68,XBOOLE_0:
def 3
;
then p in cell(GoB f,i1,j2) &
p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i1+1,j2)/\((L~f)`) &
p in cell(GoB f,i1,j2)/\((L~f)`) by A61,A62,XBOOLE_0:def 3;
case A70:i1>=1 & i1+1=len GoB f;
A71: i1<i1+1 by NAT_1:38;
A72:1<=i1 & i1<len GoB f by A70,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i1,width (GoB f))`1<=r
& r<=(GoB f)*(i1+1,width (GoB f))`1}
proof
((GoB f)*(i1,width GoB f))`1
<((GoB f)*(i1+1,width (GoB f)))`1 by A55,A70,A71,
GOBOARD5:4;
hence thesis;
end;
then A73:p in v_strip(GoB f,i1) by A55,A72,GOBOARD5:9;
p in {|[r,s]|:(GoB f)*(i1+1,width (GoB f))`1<=r};
then p in v_strip(GoB f,i1+1) by A55,A70,GOBOARD5:10;
then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A63,A73,XBOOLE_0:
def 3
;
then p in cell(GoB f,i1,j2) &
p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i1+1,j2)/\((L~f)`) &
p in cell(GoB f,i1,j2)/\((L~f)`) by A61,A62,XBOOLE_0:def 3;
case A74:i1=0 & i1+1<len GoB f;
then p in {|[r,s]|: r<=(GoB f)*(1,width (GoB f))`1};
then A75:p in v_strip(GoB f,i1) by A55,A74,GOBOARD5:11;
A76:i1+1+1<=len GoB f by A74,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i1+1,width (GoB f))`1<=r
& r<=(GoB f)*(i1+1+1,width (GoB f))`1}
proof i1+1<i1+1+1 by NAT_1:38;
then ((GoB f)*(i1+1,width (GoB f))`1
<=((GoB f)*(i1+1,width (GoB f)))`1
& ((GoB f)*(i1+1,width (GoB f)))`1
<=(GoB f)*(i1+1+1,width (GoB f))`1) by A55,A57,A76,GOBOARD5:
4;
hence thesis;
end;
then p in v_strip(GoB f,i1+1) by A55,A74,GOBOARD5:9;
then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A63,A75,XBOOLE_0:
def 3
;
then p in cell(GoB f,i1,j2) &
p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i1+1,j2)/\((L~f)`) &
p in cell(GoB f,i1,j2)/\((L~f)`) by A61,A62,XBOOLE_0:def 3;
case i1=0 & i1+1=len GoB f;
hence contradiction by GOBOARD7:34;
end;
then A77:p in Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`)
& p in Cl Down(Int cell(GoB f,i1,j2),(L~f)`) by A1,Th3;
A78:Down(LeftComp f,(L~f)`)=LeftComp f &
Down(RightComp f,(L~f)`)=RightComp f by Th6;
Down(Int cell(GoB f,i1,j2),(L~f)`)
c= LeftComp f \/ RightComp f by A1,A2,Th4;
then Down(Int cell(GoB f,i1,j2),(L~f)`)
c= Down(LeftComp f \/ RightComp f,(L~f)`)
by A78,GOBRD11:4;
then A79:Cl Down(Int cell(GoB f,i1,j2),(L~f)`)
c= Cl Down(LeftComp f \/ RightComp f,(L~f)`)
by PRE_TOPC:49;
A80:Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`) is connected
by A1,A3,Th4;
Down(LeftComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm4;
then Down(LeftComp f,(L~f)`) is closed by CONNSP_1:35;
then A81:Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`)
by PRE_TOPC:52;
Down(RightComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm5;
then Down(RightComp f,(L~f)`) is closed by CONNSP_1:35;
then A82:Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`)
by PRE_TOPC:52;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
=Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
then A83:Cl Down(LeftComp f \/ RightComp f,(L~f)`)
=Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A81,A82,PRE_TOPC:50;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
is a_union_of_components of (TOP-REAL 2)|((L~f)`) by Th6;
then A84:skl p1 c= Down(LeftComp f,(L~f)`)
\/ Down(RightComp f,(L~f)`) by A77,A79,A83,CONNSP_3:21;
Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`) c= skl p1
by A77,A80,GOBRD11:1;
then A85: Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`)
c= Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A84,XBOOLE_1:1;
A86:Down(Int cell(GoB f,i1+1,j2),(L~f)`)
c= Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`)
by PRE_TOPC:48;
Down(Int cell(GoB f,i1+1,j2),(L~f)`)=Int cell(GoB f,i1+1,j2)
by A1,A3,Th4;
hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f
by A78,A85,A86,XBOOLE_1:1;
case A87:j2<>0 & 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 0<j2 by NAT_1:19; then A88: 0+1<=j2 by NAT_1:38;
A89:j2<width GoB f by A1,A87,REAL_1:def 5;
then A90:j2+1<=width GoB f by NAT_1:38;
for k st 1<=k & k+1<=len f holds
LSeg((GoB f)*(i1+1,j2),(GoB f)*(i1+1,j2+1))<>LSeg(f,k)
proof let k;assume A91:1<=k & k+1<=len f;
then LSeg(f,k)=LSeg(f/.k,f/.(k+1)) by TOPREAL1:def 5;
hence LSeg((GoB f)*(i1+1,j2),(GoB f)*(i1+1,j2+1))<>LSeg(f,k)
by A87,A91;
end;
then A92: 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:41;
reconsider p=1/2*((GoB f)*(i1+1,j2)+(GoB f)*(i1+1,j2+1)) as
Point of TOP-REAL 2;
A93:p`1=1/2*((GoB f)*(i1+1,j2)+(GoB f)*(i1+1,j2+1))`1 by TOPREAL3:9
.=1/2*(((GoB f)*(i1+1,j2))`1+((GoB f)*(i1+1,j2+1))`1) by
TOPREAL3:7;
A94:p`2=1/2*((GoB f)*(i1+1,j2)+(GoB f)*(i1+1,j2+1))`2 by TOPREAL3:9
.=1/2*(((GoB f)*(i1+1,j2))`2+((GoB f)*(i1+1,j2+1))`2) by
TOPREAL3:7;
then A95:p=|[1/2*(((GoB f)*(i1+1,j2))`1+((GoB f)*(i1+1,j2+1))`1),
1/2*(((GoB f)*(i1+1,j2))`2+((GoB f)*(i1+1,j2+1))`2)]|
by A93,EUCLID:57;
A96:1<width GoB f by GOBOARD7:35;
A97: 1<=1+i1 by NAT_1:29;
A98:j2<j2+1 by NAT_1:38;
A99: 1<j2+1 by A88,NAT_1:38;
A100:((GoB f)*(i1+1,j2))`2 <((GoB f)*(i1+1,j2+1))`2
by A1,A3,A88,A90,A97,A98,GOBOARD5:5;
then A101:((GoB f)*(i1+1,j2))`2+((GoB f)*(i1+1,j2))`2
<((GoB f)*(i1+1,j2))`2+((GoB f)*(i1+1,j2+1))`2
by REAL_1:67;
A102:((GoB f)*(i1+1,j2))`2+((GoB f)*(i1+1,j2+1))`2
<((GoB f)*(i1+1,j2+1))`2+((GoB f)*(i1+1,j2+1))`2
by A100,REAL_1:67;
(((GoB f)*(i1+1,j2))`2+((GoB f)*(i1+1,j2))`2)/2
<(((GoB f)*(i1+1,j2))`2+((GoB f)*(i1+1,j2+1))`2)/2
by A101,REAL_1:73;
then A103:((GoB f)*(i1+1,j2))`2
<(((GoB f)*(i1+1,j2))`2+((GoB f)*(i1+1,j2+1))`2)/2
by XCMPLX_1:65;
(((GoB f)*(i1+1,j2))`2+((GoB f)*(i1+1,j2+1))`2)/2
<(((GoB f)*(i1+1,j2+1))`2+((GoB f)*(i1+1,j2+1))`2)/2
by A102,REAL_1:73;
then A104:((GoB f)*(i1+1,j2+1))`2
>(((GoB f)*(i1+1,j2))`2+((GoB f)*(i1+1,j2+1))`2)/2
by XCMPLX_1:65;
A105:((GoB f)*(i1+1,j2))`2<p`2 by A94,A103,XCMPLX_1:100;
A106:p`2< ((GoB f)*(i1+1,j2+1))`2 by A94,A104,XCMPLX_1:100;
A107:p in {p} by TARSKI:def 1;
reconsider P={p} as Subset of TOP-REAL 2;
(for x st x in P holds not x in (L~f)) implies
P misses L~f by XBOOLE_0:3;
then A108: {p} c= (L~f)` by A1,A3,A88,A89,A92,NAT_1:29,38,SUBSET_1:
43,TARSKI:def 1;
then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by A107,
JORDAN1:1;
A109:1<=i1+1 & i1+1<=len GoB f by A1,A3,NAT_1:29;
p in {|[r,s]|:(GoB f)*(i1+1,j2)`2<=s & s<=(GoB f)*(i1+1,j2+1)`2}
proof
p=|[p`1,p`2]| by EUCLID:57;
hence thesis by A105,A106;
end;
then A110:p in h_strip(GoB f,j2) by A88,A89,A109,GOBOARD5:6;
0<=i1 by NAT_1:18;
then A111: i1=0 or i1>=0+1 by NAT_1:38;
now per cases by A1,A3,A111,REAL_1:def 5;
case A112:i1>=1 & i1+1<len GoB f;
then A113:1<=i1+1 & i1+1<len GoB f by NAT_1:29;
A114:1<=i1 & i1<len GoB f by A112,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i1,1)`1<=r & r<=(GoB f)*(i1+1,1)`1}
proof A115: i1<i1+1 by NAT_1:38;
A116:((GoB f)*(i1+1,j2))`1=((GoB f)*(i1+1,1))`1
by A1,A3,A88,A97,GOBOARD5:3;
A117:((GoB f)*(i1+1,j2+1))`1=((GoB f)*(i1+1,1))`1
by A1,A3,A90,A97,A99,GOBOARD5:3;
A118:((GoB f)*(i1,1))`1<((GoB f)*(i1+1,1))`1
by A96,A112,A115,GOBOARD5:4;
1/2*(((GoB f)*(i1+1,j2))`1+((GoB f)*(i1+1,j2+1))`1)
=((GoB f)*(i1+1,1))`1 by A116,A117,Lm1;
hence thesis by A95,A118;
end;
then A119:p in v_strip(GoB f,i1) by A96,A114,GOBOARD5:9;
A120:i1+1+1<=len GoB f by A112,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i1+1,1)`1<=r & r<=(GoB f)*(i1+1+1,1)`1}
proof A121: i1+1<i1+1+1 by NAT_1:38;
A122:((GoB f)*(i1+1,j2))`1=((GoB f)*(i1+1,1))`1
by A1,A3,A88,A97,GOBOARD5:3;
A123:((GoB f)*(i1+1,j2+1))`1=((GoB f)*(i1+1,1))`1
by A1,A3,A90,A97,A99,GOBOARD5:3;
A124:((GoB f)*(i1+1,1))`1<((GoB f)*(i1+1+1,1))`1
by A96,A97,A120,A121,GOBOARD5:4;
1/2*(((GoB f)*(i1+1,j2))`1+((GoB f)*(i1+1,j2+1))`1)
=((GoB f)*(i1+1,1))`1 by A122,A123,Lm1;
hence thesis by A95,A124;
end;
then p in v_strip(GoB f,i1+1) by A96,A113,GOBOARD5:9;
then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A110,A119,XBOOLE_0
:def 3
;
then p in cell(GoB f,i1,j2) &
p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i1+1,j2)/\((L~f)`) &
p in cell(GoB f,i1,j2)/\((L~f)`) by A107,A108,XBOOLE_0:def 3;
case A125:i1>=1 & i1+1=len GoB f;
A126: i1<i1+1 by NAT_1:38;
p in {|[r,s]|:(GoB f)*(i1,1)`1<=r & r<=(GoB f)*(i1+1,1)`1}
proof
A127:((GoB f)*(i1+1,j2))`1=((GoB f)*(i1+1,1))`1
by A1,A3,A88,A97,GOBOARD5:3;
A128:((GoB f)*(i1+1,j2+1))`1=((GoB f)*(i1+1,1))`1
by A1,A3,A90,A97,A99,GOBOARD5:3;
A129:((GoB f)*(i1,1))`1<((GoB f)*(i1+1,1))`1
by A96,A125,A126,GOBOARD5:4;
1/2*(((GoB f)*(i1+1,j2))`1+((GoB f)*(i1+1,j2+1))`1)
=((GoB f)*(i1+1,1))`1 by A127,A128,Lm1;
hence thesis by A95,A129;
end;
then A130:p in v_strip(GoB f,i1) by A96,A125,A126,GOBOARD5:9;
p in {|[r,s]|:(GoB f)*(i1+1,1)`1<=r}
proof
A131:((GoB f)*(i1+1,j2))`1=((GoB f)*(i1+1,1))`1
by A1,A3,A88,A97,GOBOARD5:3;
((GoB f)*(i1+1,j2+1))`1=((GoB f)*(i1+1,1))`1
by A1,A3,A90,A97,A99,GOBOARD5:3;
then (GoB f)*(i1+1,1)`1
<=1/2*(((GoB f)*(i1+1,j2))`1+((GoB f)*(i1+1,j2+1))`1) by
A131,Lm1;
hence thesis by A95;
end;
then p in v_strip(GoB f,i1+1) by A96,A125,GOBOARD5:10;
then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A110,A130,XBOOLE_0
:def 3
;
then p in cell(GoB f,i1,j2) &
p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i1+1,j2)/\((L~f)`) &
p in cell(GoB f,i1,j2)/\((L~f)`) by A107,A108,XBOOLE_0:def 3;
case A132:i1=0 & i1+1<len GoB f;
p in {|[r,s]|: r<=(GoB f)*(1,1)`1}
proof
A133:((GoB f)*(i1+1,j2))`1=((GoB f)*(i1+1,1))`1
by A1,A3,A88,A97,GOBOARD5:3;
((GoB f)*(i1+1,j2+1))`1=((GoB f)*(i1+1,1))`1
by A1,A3,A90,A97,A99,GOBOARD5:3;
then 1/2*(((GoB f)*(i1+1,j2))`1+((GoB f)*(i1+1,j2+1))`1)
<=((GoB f)*(1,1))`1 by A132,A133,Lm1;
hence thesis by A95;
end;
then A134:p in v_strip(GoB f,i1) by A96,A132,GOBOARD5:11;
A135:i1+1+1<=len GoB f by A132,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i1+1,1)`1<=r & r<=(GoB f)*(i1+1+1,1)`1}
proof A136: i1+1<i1+1+1 by NAT_1:38;
A137:((GoB f)*(i1+1,j2))`1=((GoB f)*(i1+1,1))`1
by A1,A3,A88,A97,GOBOARD5:3;
A138:((GoB f)*(i1+1,j2+1))`1=((GoB f)*(i1+1,1))`1
by A1,A3,A90,A97,A99,GOBOARD5:3;
A139:((GoB f)*(i1+1,1))`1<((GoB f)*(i1+1+1,1))`1
by A96,A97,A135,A136,GOBOARD5:4;
1/2*(((GoB f)*(i1+1,j2))`1+((GoB f)*(i1+1,j2+1))`1)
=((GoB f)*(i1+1,1))`1 by A137,A138,Lm1;
hence thesis by A95,A139;
end;
then p in v_strip(GoB f,i1+1) by A96,A132,GOBOARD5:9;
then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A110,A134,XBOOLE_0
:def 3
;
then p in cell(GoB f,i1,j2) &
p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i1+1,j2)/\((L~f)`) &
p in cell(GoB f,i1,j2)/\((L~f)`) by A107,A108,XBOOLE_0:def 3;
case i1=0 & i1+1=len GoB f;
hence contradiction by GOBOARD7:34;
end;
then A140:p in Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`)
& p in Cl Down(Int cell(GoB f,i1,j2),(L~f)`) by A1,Th3;
A141:Down(LeftComp f,(L~f)`)=LeftComp f &
Down(RightComp f,(L~f)`)=RightComp f by Th6;
Down(Int cell(GoB f,i1,j2),(L~f)`)
c= LeftComp f \/ RightComp f by A1,A2,Th4;
then Down(Int cell(GoB f,i1,j2),(L~f)`)
c= Down(LeftComp f \/ RightComp f,(L~f)`)
by A141,GOBRD11:4;
then A142:Cl Down(Int cell(GoB f,i1,j2),(L~f)`)
c= Cl Down(LeftComp f \/ RightComp f,(L~f)`)
by PRE_TOPC:49;
A143:Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`) is connected
by A1,A3,Th4;
Down(LeftComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm4;
then Down(LeftComp f,(L~f)`) is closed by CONNSP_1:35;
then A144:Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`)
by PRE_TOPC:52;
Down(RightComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm5;
then Down(RightComp f,(L~f)`) is closed by CONNSP_1:35;
then A145:Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`)
by PRE_TOPC:52;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
=Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
then A146:Cl Down(LeftComp f \/ RightComp f,(L~f)`)
=Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A144,A145,PRE_TOPC:50;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
is a_union_of_components of (TOP-REAL 2)|((L~f)`) by Th6;
then A147:skl p1 c= Down(LeftComp f,(L~f)`)
\/ Down(RightComp f,(L~f)`) by A140,A142,A146,CONNSP_3:21;
Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`) c= skl p1
by A140,A143,GOBRD11:1;
then A148: Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`)
c= Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A147,XBOOLE_1:1;
A149:Down(Int cell(GoB f,i1+1,j2),(L~f)`)
c= Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`)
by PRE_TOPC:48;
Down(Int cell(GoB f,i1+1,j2),(L~f)`)=Int cell(GoB f,i1+1,j2)
by A1,A3,Th4;
hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f
by A141,A148,A149,XBOOLE_1:1;
end;
hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f;
end;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by A3;
case A150: i1=i2+1;
then A151:i1-'1=i2 by BINARITH:39;
A152:i2<i2+1 by NAT_1:38;
A153:i2<i1 by A150,NAT_1:38;
A154:1<=i2+1 by NAT_1:29;
A155:1<=i1 by A150,NAT_1:29;
A156:i2+1<i2+1+1 by NAT_1:38;
i1-1=i2 by A150,XCMPLX_1:26;
then i1-1>=0 by NAT_1:18;
then i1-'1=i1-1 by BINARITH:def 3;
then A157:i1=i1-'1+1 by XCMPLX_1:27;
A158:1<=i1-'1+1 by NAT_1:29;
A159:i1-'1<i1 by A150,A153,BINARITH:39;
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)*(i2+1,j2),(GoB f)*(i2+1,j2+1));
then consider k such that A160:1<=k & k+1 <=len f
& j2<>0 & j2<>width GoB f &
LSeg(f/.k,f/.(k+1))
=LSeg((GoB f)*(i1-'1+1,j2),(GoB f)*(i1-'1+1,j2+1))
by A151;
now per cases by A160,SPPOL_1:25;
case A161:f/.k=(GoB f)*(i1-'1+1,j2)
& f/.(k+1)= (GoB f)*(i1-'1+1,j2+1);
A162:Indices GoB f=[:dom GoB f,Seg width GoB f:] by MATRIX_1:def 5;
i1-'1<len GoB f by A1,A159,AXIOMS:22;
then i1-'1+1<=len GoB f by NAT_1:38;
then A163:i1-'1+1 in dom GoB f by A158,FINSEQ_3:27;
j2>0 by A160,NAT_1:19; then j2>=0+1 by NAT_1:38;
then j2 in Seg width GoB f by A1,FINSEQ_1:3;
then A164:[i1-'1+1,j2] in Indices GoB f by A162,A163,ZFMISC_1:106;
j2<width GoB f by A1,A160,REAL_1:def 5;
then A165:j2+1<=width GoB f by NAT_1:38;
1<=j2+1 by NAT_1:29;
then j2+1 in Seg width GoB f by A165,FINSEQ_1:3;
then [i1-'1+1,j2+1] in Indices GoB f by A162,A163,ZFMISC_1:106;
then A166:left_cell(f,k) = cell(GoB f,i1-'1,j2)
by A160,A161,A164,GOBOARD5:28;
A167: Int left_cell(f,k) c= LeftComp f by A160,GOBOARD9:24;
LeftComp f c= LeftComp f \/ RightComp f by XBOOLE_1:7;
hence Int cell(GoB f,i1-'1,j2) c= LeftComp f \/ RightComp f
by A166,A167,XBOOLE_1:1;
case A168:f/.k=(GoB f)*(i1-'1+1,j2+1)
& f/.(k+1)= (GoB f)*(i1-'1+1,j2);
A169:Indices GoB f=[:dom GoB f,Seg width GoB f:] by MATRIX_1:def 5;
A170:i1-'1+1 in dom GoB f by A1,A155,A157,FINSEQ_3:27;
j2>0 by A160,NAT_1:19; then j2>=0+1 by NAT_1:38;
then j2 in Seg width GoB f by A1,FINSEQ_1:3;
then A171:[i1-'1+1,j2] in Indices GoB f by A169,A170,ZFMISC_1:106;
j2<width GoB f by A1,A160,REAL_1:def 5;
then A172:j2+1<=width GoB f by NAT_1:38;
1<=j2+1 by NAT_1:29;
then j2+1 in Seg width GoB f by A172,FINSEQ_1:3;
then [i1-'1+1,j2+1] in Indices GoB f by A169,A170,ZFMISC_1:106;
then A173:right_cell(f,k) = cell(GoB f,i1-'1,j2)
by A160,A168,A171,GOBOARD5:31;
A174: Int right_cell(f,k) c= RightComp f by A160,GOBOARD9:28;
RightComp f c= LeftComp f \/ RightComp f by XBOOLE_1:7;
hence Int cell(GoB f,i1-'1,j2) c= LeftComp f \/ RightComp f
by A173,A174,XBOOLE_1:1;
end;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f
by A150,BINARITH:39;
case A175: 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 A175;
case A176:j2=0;
reconsider p=|[((GoB f)*(i2+1,1))`1,((GoB f)*(i2+1,1))`2-1]| as
Point of TOP-REAL 2;
A177:1<width GoB f by GOBOARD7:35;
A178:1<len GoB f by GOBOARD7:34;
A179:1<=i2+1 by NAT_1:29;
then ((GoB f)*(i2+1,1))`2=((GoB f)*(1,1))`2 by A1,A150,A177,
GOBOARD5:2;
then A180:p`2=((GoB f)*(1,1))`2-1 by EUCLID:56;
p`2<p`2+1 by REAL_1:69;
then A181:p`2< ((GoB f)*(1,1))`2 by A180,XCMPLX_1:27;
A182:p in {p} by TARSKI:def 1;
reconsider P={p} as Subset of TOP-REAL 2;
(for q being Point of TOP-REAL 2
st q in P holds q`2<((GoB f)*(1,1))`2) implies
P misses L~f by GOBOARD8:23;
then A183: {p} c= (L~f)` by A181,SUBSET_1:43,TARSKI:def 1;
then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by A182,
JORDAN1:1;
p in {|[r,s]|:s<=(GoB f)*(1,1)`2}
proof
p=|[p`1,p`2]| by EUCLID:57;
hence thesis by A181;
end;
then A184:p in h_strip(GoB f,j2) by A176,A178,GOBOARD5:8;
now per cases by A1,A150,NAT_1:18,REAL_1:def 5;
case A185:i2+1<len GoB f & i2>0; then A186: 0+1<=i2 by NAT_1:38;
then A187:1<=i2+1 & i2+1<len GoB f by A185,NAT_1:38;
A188:1<=i2 & i2<len GoB f by A185,A186,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i2,1)`1<=r & r<=(GoB f)*(i2+1,1)`1}
proof i2<i2+1 by NAT_1:38;
then ((GoB f)*(i2,1))`1<((GoB f)*(i2+1,1))`1 by A1,A150,A177,A186
,GOBOARD5:4;
hence thesis;
end;
then A189:p in v_strip(GoB f,i2) by A177,A188,GOBOARD5:9;
A190:i2+1+1<=len GoB f by A185,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i2+1,1)`1<=r & r<=(GoB f)*(i2+1+1,1)`1}
proof i2+1<i2+1+1 by NAT_1:38;
then ((GoB f)*(i2+1,1)`1<=((GoB f)*(i2+1,1))`1
& ((GoB f)*(i2+1,1))`1<=(GoB f)*(i2+1+1,1)`1)
by A177,A179,A190,GOBOARD5:4;
hence thesis;
end;
then p in v_strip(GoB f,i2+1) by A177,A187,GOBOARD5:9;
then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A184,A189,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i2+1,j2)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A182,A183,XBOOLE_0:def 3;
case A191:i2+1<len GoB f & i2=0;
then A192:i2+1+1<=len GoB f by NAT_1:38;
A193: i2+1<i2+1+1 by NAT_1:38;
p in {|[r,s]|: r<=(GoB f)*(i2+1,1)`1};
then A194:p in v_strip(GoB f,i2) by A177,A191,GOBOARD5:11;
p in {|[r,s]|:(GoB f)*(i2+1,1)`1<=r & r<=(GoB f)*(i2+1+1,1)`1}
proof
(GoB f)*(i2+1,1)`1<(GoB f)*(i2+1+1,1)`1 by A154,A177,A192,
A193,GOBOARD5:4;
hence thesis;
end;
then p in v_strip(GoB f,i2+1) by A177,A191,GOBOARD5:9;
then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A184,A194,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i2+1,j2)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A182,A183,XBOOLE_0:def 3;
case A195:i2+1=len GoB f & i2>0; then A196: 0+1<=i2 by NAT_1:38;
then A197:1<=i2 & i2<len GoB f by A195,NAT_1:38;
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 A152,A177,A195,A196,
GOBOARD5:4;
hence thesis;
end;
then A198:p in v_strip(GoB f,i2) by A177,A197,GOBOARD5:9;
p in {|[r,s]|:(GoB f)*(i2+1,1)`1<=r};
then p in v_strip(GoB f,i2+1) by A177,A195,GOBOARD5:10;
then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A184,A198,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i2+1,j2)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A182,A183,XBOOLE_0:def 3;
case A199:i2+1=len GoB f & i2=0;
then p in {|[r,s]|: r<=(GoB f)*(1,1)`1};
then A200:p in v_strip(GoB f,i2) by A177,A199,GOBOARD5:11;
p in {|[r,s]|:(GoB f)*(i2+1,1)`1<=r};
then p in v_strip(GoB f,i2+1) by A177,A199,GOBOARD5:10;
then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A184,A200,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i2+1,j2)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A182,A183,XBOOLE_0:def 3;
end;
then A201:p in Cl Down(Int cell(GoB f,i2+1,j2),(L~f)`)
& p in Cl Down(Int cell(GoB f,i2,j2),(L~f)`) by A1,Th3;
A202:Down(LeftComp f,(L~f)`)=LeftComp f &
Down(RightComp f,(L~f)`)=RightComp f by Th6;
Down(Int cell(GoB f,i1,j2),(L~f)`)
c= LeftComp f \/ RightComp f by A1,A2,Th4;
then Down(Int cell(GoB f,i1,j2),(L~f)`)
c= Down(LeftComp f \/ RightComp f,(L~f)`)
by A202,GOBRD11:4;
then A203:Cl Down(Int cell(GoB f,i1,j2),(L~f)`)
c= Cl Down(LeftComp f \/ RightComp f,(L~f)`)
by PRE_TOPC:49;
A204:Cl Down(Int cell(GoB f,i2,j2),(L~f)`) is connected
by A1,Th4;
Down(LeftComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm4;
then Down(LeftComp f,(L~f)`) is closed by CONNSP_1:35;
then A205:Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`)
by PRE_TOPC:52;
Down(RightComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm5;
then Down(RightComp f,(L~f)`) is closed by CONNSP_1:35;
then A206:Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`)
by PRE_TOPC:52;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
=Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
then A207:Cl Down(LeftComp f \/ RightComp f,(L~f)`)
=Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A205,A206,PRE_TOPC:50;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
is a_union_of_components of (TOP-REAL 2)|((L~f)`) by Th6;
then A208:skl p1 c= Down(LeftComp f,(L~f)`)
\/ Down(RightComp f,(L~f)`) by A150,A201,A203,A207,CONNSP_3:21
;
Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= skl p1
by A201,A204,GOBRD11:1;
then A209: Cl Down(Int cell(GoB f,i2,j2),(L~f)`)
c= Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A208,XBOOLE_1:1;
A210:Down(Int cell(GoB f,i2,j2),(L~f)`)
c= Cl Down(Int cell(GoB f,i2,j2),(L~f)`)
by PRE_TOPC:48;
Down(Int cell(GoB f,i2,j2),(L~f)`)=Int cell(GoB f,i2,j2)
by A1,Th4;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f
by A202,A209,A210,XBOOLE_1:1;
case A211:j2=width GoB f;
reconsider p=|[((GoB f)*(i2+1,width GoB f))`1,
((GoB f)*(i2+1,width GoB f))`2+1]| as Point of TOP-REAL 2;
A212:1<width GoB f by GOBOARD7:35;
A213:1<len GoB f by GOBOARD7:34;
A214:1<=i2+1 by NAT_1:29;
then ((GoB f)*(i2+1,width GoB f))`2
=((GoB f)*(1,width GoB f))`2 by A1,A150,A212,GOBOARD5:2
;
then A215:p`2=((GoB f)*(1,width GoB f))`2+1 by EUCLID:56;
A216: ((GoB f)*(1,width GoB f))`2<((GoB f)*(1,width GoB f))`2+1
by REAL_1:69;
A217:p in {p} by TARSKI:def 1;
reconsider P={p} as Subset of TOP-REAL 2;
(for q being Point of TOP-REAL 2
st q in P holds ((GoB f)*(1,width GoB f)`2)<q`2) implies
P misses L~f by GOBOARD8:24;
then A218: {p} c= (L~f)` by A215,A216,SUBSET_1:43,TARSKI:def 1;
then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by A217,
JORDAN1:1;
p in {|[r,s]|:(GoB f)*(1,width (GoB f))`2<=s}
proof
p=|[p`1,p`2]| & ((GoB f)*(1,width GoB f)`2<=p`2) by A215,
EUCLID:57,REAL_1:69;
hence thesis;
end;
then A219:p in h_strip(GoB f,j2) by A211,A213,GOBOARD5:7;
now per cases by A1,A150,NAT_1:18,REAL_1:def 5;
case A220:i2+1<len GoB f & i2>0;
then A221:i2+1+1<=len GoB f by NAT_1:38;
A222:0+1<=i2 by A220,NAT_1:38;
A223:i2<i2+1 by NAT_1:38;
A224:1<=i2+1 & i2+1<len GoB f by A220,NAT_1:29;
A225:1<=i2 & i2<len GoB f by A220,A222,NAT_1:38;
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 A1,A150,A212,A222,A223,
GOBOARD5:4;
hence thesis;
end;
then A226:p in v_strip(GoB f,i2) by A212,A225,GOBOARD5:9;
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+1<i2+1+1 by NAT_1:38;
then ((GoB f)*(i2+1,width GoB f)`1
<=((GoB f)*(i2+1,width GoB f))`1
& ((GoB f)*(i2+1,width GoB f))`1
<=(GoB f)*(i2+1+1,width GoB f)`1) by A212,A214,A221,GOBOARD5
:4;
hence thesis;
end;
then p in v_strip(GoB f,i2+1) by A212,A224,GOBOARD5:9;
then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A219,A226,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i2+1,j2)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A217,A218,XBOOLE_0:def 3;
case A227:i2+1<len GoB f & i2=0;
then A228:i2+1+1<=len GoB f by NAT_1:38;
p in {|[r,s]|: r<=(GoB f)*(1,width (GoB f))`1} by A227;
then A229:p in v_strip(GoB f,i2) by A212,A227,GOBOARD5:11;
p in {|[r,s]|:(GoB f)*(i2+1,width (GoB f))`1<=r &
r<=(GoB f)*(i2+1+1,width (GoB f))`1}
proof
(GoB f)*(i2+1,width (GoB f))`1
<(GoB f)*(i2+1+1,width (GoB f))`1 by A154,A156,A212,A228,
GOBOARD5:4;
hence thesis;
end;
then p in v_strip(GoB f,i2+1) by A212,A227,GOBOARD5:9;
then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A219,A229,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i2+1,j2)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A217,A218,XBOOLE_0:def 3;
case A230:i2+1=len GoB f & i2>0;
then A231: 0+1<=i2 by NAT_1:38;
then A232:1<=i2 & i2<len GoB f by A230,NAT_1:38;
p in {|[r,s]|: (GoB f)*(len GoB f,width (GoB f))`1<=r}
by A230;
then A233:p in v_strip(GoB f,i2+1) by A212,A230,GOBOARD5:10;
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+1,width (GoB f))`1
<=((GoB f)*(i2+1,width (GoB f)))`1
& ((GoB f)*(i2,width (GoB f)))`1
<=(GoB f)*(i2+1,width (GoB f))`1)
by A152,A212,A230,A231,GOBOARD5:4;
hence thesis;
end;
then p in v_strip(GoB f,i2) by A212,A232,GOBOARD5:9;
then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A219,A233,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i2+1,j2)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A217,A218,XBOOLE_0:def 3;
case i2+1=len GoB f & i2=0;
hence contradiction by GOBOARD7:34;
end;
then A234:p in Cl Down(Int cell(GoB f,i2+1,j2),(L~f)`)
& p in Cl Down(Int cell(GoB f,i2,j2),(L~f)`) by A1,Th3;
A235:Down(LeftComp f,(L~f)`)=LeftComp f &
Down(RightComp f,(L~f)`)=RightComp f by Th6;
Down(Int cell(GoB f,i1,j2),(L~f)`)
c= LeftComp f \/ RightComp f by A1,A2,Th4;
then Down(Int cell(GoB f,i1,j2),(L~f)`)
c= Down(LeftComp f \/ RightComp f,(L~f)`)
by A235,GOBRD11:4;
then A236:Cl Down(Int cell(GoB f,i1,j2),(L~f)`)
c= Cl Down(LeftComp f \/ RightComp f,(L~f)`)
by PRE_TOPC:49;
A237:Cl Down(Int cell(GoB f,i2,j2),(L~f)`) is connected
by A1,Th4;
Down(LeftComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm4;
then Down(LeftComp f,(L~f)`) is closed by CONNSP_1:35;
then A238:Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`)
by PRE_TOPC:52;
Down(RightComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm5;
then Down(RightComp f,(L~f)`) is closed by CONNSP_1:35;
then A239:Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`)
by PRE_TOPC:52;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
=Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
then A240:Cl Down(LeftComp f \/ RightComp f,(L~f)`)
=Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A238,A239,PRE_TOPC:50;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
is a_union_of_components of (TOP-REAL 2)|((L~f)`) by Th6;
then A241:skl p1 c= Down(LeftComp f,(L~f)`)
\/ Down(RightComp f,(L~f)`) by A150,A234,A236,A240,CONNSP_3:21
;
Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= skl p1
by A234,A237,GOBRD11:1;
then A242: Cl Down(Int cell(GoB f,i2,j2),(L~f)`)
c= Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A241,XBOOLE_1:1;
A243:Down(Int cell(GoB f,i2,j2),(L~f)`)
c= Cl Down(Int cell(GoB f,i2,j2),(L~f)`)
by PRE_TOPC:48;
Down(Int cell(GoB f,i2,j2),(L~f)`)=Int cell(GoB f,i2,j2)
by A1,Th4;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f
by A235,A242,A243,XBOOLE_1:1;
case A244:j2<>0 & 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 0<j2 by NAT_1:19; then A245: 0+1<=j2 by NAT_1:38;
A246:j2<width GoB f by A1,A244,REAL_1:def 5;
then A247:j2+1<=width GoB f by NAT_1:38;
for k st 1<=k & k+1<=len f holds
LSeg((GoB f)*(i2+1,j2),(GoB f)*(i2+1,j2+1))<>LSeg(f,k)
proof let k;assume A248:1<=k & k+1<=len f;
then LSeg(f,k)=LSeg(f/.k,f/.(k+1)) by TOPREAL1:def 5;
hence LSeg((GoB f)*(i2+1,j2),(GoB f)*(i2+1,j2+1))<>LSeg(f,k)
by A244,A248;
end;
then A249: 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:41;
reconsider p=1/2*((GoB f)*(i2+1,j2)+(GoB f)*(i2+1,j2+1)) as
Point of TOP-REAL 2;
A250:p`1=1/2*((GoB f)*(i2+1,j2)+(GoB f)*(i2+1,j2+1))`1 by TOPREAL3:
9
.=1/2*(((GoB f)*(i2+1,j2))`1+((GoB f)*(i2+1,j2+1))`1) by
TOPREAL3:7;
A251:p`2=1/2*((GoB f)*(i2+1,j2)+(GoB f)*(i2+1,j2+1))`2 by TOPREAL3:
9
.=1/2*(((GoB f)*(i2+1,j2))`2+((GoB f)*(i2+1,j2+1))`2) by
TOPREAL3:7;
then A252:p=|[1/2*(((GoB f)*(i2+1,j2))`1+((GoB f)*(i2+1,j2+1))`1),
1/2*(((GoB f)*(i2+1,j2))`2+((GoB f)*(i2+1,j2+1))`2)]|
by A250,EUCLID:57;
A253:1<width GoB f by GOBOARD7:35;
A254: 1<=1+i2 by NAT_1:29;
A255:j2<j2+1 by NAT_1:38;
A256: 1<j2+1 by A245,NAT_1:38;
A257:((GoB f)*(i2+1,j2))`2 <((GoB f)*(i2+1,j2+1))`2
by A1,A150,A245,A247,A254,A255,GOBOARD5:5;
then A258:((GoB f)*(i2+1,j2))`2+((GoB f)*(i2+1,j2))`2
<((GoB f)*(i2+1,j2))`2+((GoB f)*(i2+1,j2+1))`2 by REAL_1:67;
A259:((GoB f)*(i2+1,j2))`2+((GoB f)*(i2+1,j2+1))`2
<((GoB f)*(i2+1,j2+1))`2+((GoB f)*(i2+1,j2+1))`2
by A257,REAL_1:67;
(((GoB f)*(i2+1,j2))`2+((GoB f)*(i2+1,j2))`2)/2
<(((GoB f)*(i2+1,j2))`2+((GoB f)*(i2+1,j2+1))`2)/2
by A258,REAL_1:73;
then A260:((GoB f)*(i2+1,j2))`2
<(((GoB f)*(i2+1,j2))`2+((GoB f)*(i2+1,j2+1))`2)/2
by XCMPLX_1:65;
(((GoB f)*(i2+1,j2))`2+((GoB f)*(i2+1,j2+1))`2)/2
<(((GoB f)*(i2+1,j2+1))`2+((GoB f)*(i2+1,j2+1))`2)/2
by A259,REAL_1:73;
then A261:((GoB f)*(i2+1,j2+1))`2
>(((GoB f)*(i2+1,j2))`2+((GoB f)*(i2+1,j2+1))`2)/2
by XCMPLX_1:65;
A262:((GoB f)*(i2+1,j2))`2<p`2 by A251,A260,XCMPLX_1:100;
A263:p`2< ((GoB f)*(i2+1,j2+1))`2 by A251,A261,XCMPLX_1:100;
A264:p in {p} by TARSKI:def 1;
reconsider P={p} as Subset of TOP-REAL 2;
(for x st x in P holds not x in (L~f)) implies
P misses L~f by XBOOLE_0:3;
then A265: {p} c= (L~f)` by A1,A150,A245,A246,A249,NAT_1:29,38,
SUBSET_1:43,TARSKI:def 1;
then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by A264,
JORDAN1:1;
A266:1<=i2+1 & i2+1<=len GoB f by A1,A150,NAT_1:29;
p in {|[r,s]|:(GoB f)*(i2+1,j2)`2<=s & s<=(GoB f)*(i2+1,j2+1)`2}
proof
p=|[p`1,p`2]| by EUCLID:57;
hence thesis by A262,A263;
end;
then A267:p in h_strip(GoB f,j2) by A245,A246,A266,GOBOARD5:6;
0<=i2 by NAT_1:18;
then A268: i2=0 or i2>=0+1 by NAT_1:38;
now per cases by A1,A150,A268,REAL_1:def 5;
case A269:i2>=1 & i2+1<len GoB f;
then A270:1<=i2+1 & i2+1<len GoB f by NAT_1:29;
A271:1<=i2 & i2<len GoB f by A269,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i2,1)`1<=r & r<=(GoB f)*(i2+1,1)`1}
proof A272: i2<i2+1 by NAT_1:38;
A273:((GoB f)*(i2+1,j2))`1=((GoB f)*(i2+1,1))`1
by A1,A150,A245,A254,GOBOARD5:3;
A274:((GoB f)*(i2+1,j2+1))`1=((GoB f)*(i2+1,1))`1
by A1,A150,A247,A254,A256,GOBOARD5:3;
A275:((GoB f)*(i2,1))`1<((GoB f)*(i2+1,1))`1
by A253,A269,A272,GOBOARD5:4;
1/2*(((GoB f)*(i2+1,j2))`1+((GoB f)*(i2+1,j2+1))`1)
=((GoB f)*(i2+1,1))`1 by A273,A274,Lm1;
hence thesis by A252,A275;
end;
then A276:p in v_strip(GoB f,i2) by A253,A271,GOBOARD5:9;
A277:i2+1+1<=len GoB f by A269,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i2+1,1)`1<=r & r<=(GoB f)*(i2+1+1,1)`1}
proof A278: i2+1<i2+1+1 by NAT_1:38;
A279:((GoB f)*(i2+1,j2))`1=((GoB f)*(i2+1,1))`1
by A1,A150,A245,A254,GOBOARD5:3;
A280:((GoB f)*(i2+1,j2+1))`1=((GoB f)*(i2+1,1))`1
by A1,A150,A247,A254,A256,GOBOARD5:3;
A281:((GoB f)*(i2+1,1))`1<((GoB f)*(i2+1+1,1))`1
by A253,A254,A277,A278,GOBOARD5:4;
1/2*(((GoB f)*(i2+1,j2))`1+((GoB f)*(i2+1,j2+1))`1)
=((GoB f)*(i2+1,1))`1 by A279,A280,Lm1;
hence thesis by A252,A281;
end;
then p in v_strip(GoB f,i2+1) by A253,A270,GOBOARD5:9;
then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A267,A276,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i2+1,j2)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A264,A265,XBOOLE_0:def 3;
case A282:i2>=1 & i2+1=len GoB f;
A283: i2<i2+1 by NAT_1:38;
p in {|[r,s]|:(GoB f)*(i2,1)`1<=r & r<=(GoB f)*(i2+1,1)`1}
proof
A284:((GoB f)*(i2+1,j2))`1=((GoB f)*(i2+1,1))`1
by A1,A150,A245,A254,GOBOARD5:3;
A285:((GoB f)*(i2+1,j2+1))`1=((GoB f)*(i2+1,1))`1
by A1,A150,A247,A254,A256,GOBOARD5:3;
A286:((GoB f)*(i2,1))`1<((GoB f)*(i2+1,1))`1
by A253,A282,A283,GOBOARD5:4;
1/2*(((GoB f)*(i2+1,j2))`1+((GoB f)*(i2+1,j2+1))`1)
=((GoB f)*(i2+1,1))`1 by A284,A285,Lm1;
hence thesis by A252,A286;
end;
then A287:p in v_strip(GoB f,i2) by A253,A282,A283,GOBOARD5:9;
p in {|[r,s]|:(GoB f)*(i2+1,1)`1<=r}
proof
A288:((GoB f)*(i2+1,j2))`1=((GoB f)*(i2+1,1))`1
by A1,A150,A245,A254,GOBOARD5:3;
((GoB f)*(i2+1,j2+1))`1=((GoB f)*(i2+1,1))`1
by A1,A150,A247,A254,A256,GOBOARD5:3;
then (GoB f)*(i2+1,1)`1
<=1/2*(((GoB f)*(i2+1,j2))`1+((GoB f)*(i2+1,j2+1))`1) by
A288,Lm1;
hence thesis by A252;
end;
then p in v_strip(GoB f,i2+1) by A253,A282,GOBOARD5:10;
then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A267,A287,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i2+1,j2)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A264,A265,XBOOLE_0:def 3;
case A289:i2=0 & i2+1<len GoB f;
p in {|[r,s]|: r<=(GoB f)*(1,1)`1}
proof
A290:((GoB f)*(i2+1,j2))`1=((GoB f)*(i2+1,1))`1
by A1,A150,A245,A254,GOBOARD5:3;
((GoB f)*(i2+1,j2+1))`1=((GoB f)*(i2+1,1))`1
by A1,A150,A247,A254,A256,GOBOARD5:3;
then 1/2*(((GoB f)*(i2+1,j2))`1+((GoB f)*(i2+1,j2+1))`1)
<=((GoB f)*(1,1))`1 by A289,A290,Lm1;
hence thesis by A252;
end;
then A291:p in v_strip(GoB f,i2) by A253,A289,GOBOARD5:11;
A292:i2+1+1<=len GoB f by A289,NAT_1:38;
p in {|[r,s]|:(GoB f)*(i2+1,1)`1<=r & r<=(GoB f)*(i2+1+1,1)`1}
proof A293: i2+1<i2+1+1 by NAT_1:38;
A294:((GoB f)*(i2+1,j2))`1=((GoB f)*(i2+1,1))`1
by A1,A150,A245,A254,GOBOARD5:3;
A295:((GoB f)*(i2+1,j2+1))`1=((GoB f)*(i2+1,1))`1
by A1,A150,A247,A254,A256,GOBOARD5:3;
A296:((GoB f)*(i2+1,1))`1<((GoB f)*(i2+1+1,1))`1
by A253,A254,A292,A293,GOBOARD5:4;
1/2*(((GoB f)*(i2+1,j2))`1+((GoB f)*(i2+1,j2+1))`1)
=((GoB f)*(i2+1,1))`1 by A294,A295,Lm1;
hence thesis by A252,A296;
end;
then p in v_strip(GoB f,i1) by A150,A253,A289,GOBOARD5:9;
then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) &
p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A150,A267,A291,
XBOOLE_0:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
hence p in cell(GoB f,i2+1,j2)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A264,A265,XBOOLE_0:def 3;
case i2=0 & i2+1=len GoB f;
hence contradiction by GOBOARD7:34;
end;
then A297:p in Cl Down(Int cell(GoB f,i1,j2),(L~f)`)
& p in Cl Down(Int cell(GoB f,i2,j2),(L~f)`)
by A1,A150,Th3;
A298:Down(LeftComp f,(L~f)`)=LeftComp f &
Down(RightComp f,(L~f)`)=RightComp f by Th6;
Down(Int cell(GoB f,i1,j2),(L~f)`)
c= LeftComp f \/ RightComp f by A1,A2,Th4;
then Down(Int cell(GoB f,i1,j2),(L~f)`)
c= Down(LeftComp f \/ RightComp f,(L~f)`)
by A298,GOBRD11:4;
then A299:Cl Down(Int cell(GoB f,i1,j2),(L~f)`)
c= Cl Down(LeftComp f \/ RightComp f,(L~f)`)
by PRE_TOPC:49;
A300:Cl Down(Int cell(GoB f,i2,j2),(L~f)`) is connected
by A1,Th4;
Down(LeftComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm4;
then Down(LeftComp f,(L~f)`) is closed by CONNSP_1:35;
then A301:Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`)
by PRE_TOPC:52;
Down(RightComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm5;
then Down(RightComp f,(L~f)`) is closed by CONNSP_1:35;
then A302:Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`)
by PRE_TOPC:52;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
=Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
then A303:Cl Down(LeftComp f \/ RightComp f,(L~f)`)
=Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A301,A302,PRE_TOPC:50;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
is a_union_of_components of (TOP-REAL 2)|((L~f)`) by Th6;
then A304:skl p1 c= Down(LeftComp f,(L~f)`)
\/ Down(RightComp f,(L~f)`) by A297,A299,A303,CONNSP_3:21;
Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= skl p1
by A297,A300,GOBRD11:1;
then A305: Cl Down(Int cell(GoB f,i2,j2),(L~f)`)
c= Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A304,XBOOLE_1:1;
A306:Down(Int cell(GoB f,i2,j2),(L~f)`)
c= Cl Down(Int cell(GoB f,i2,j2),(L~f)`)
by PRE_TOPC:48;
Down(Int cell(GoB f,i2,j2),(L~f)`)=Int cell(GoB f,i2,j2)
by A1,Th4;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f
by A298,A305,A306,XBOOLE_1:1;
end;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f;
end;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f;
end;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f;
end;
hence Int cell(GoB f,i1,j1) c= LeftComp f \/ RightComp f
implies Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f;
end;
Lm7: for i1,j1,i2,j2 st i1<=len GoB f & j1<=width GoB f
& i2<=len GoB f & j2<=width GoB f & (j2=j1+1 or j1=j2+1)&(i1=i2)
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
A1: i1<=len GoB f & j1<=width GoB f
& i2<=len GoB f & j2<=width GoB f & (j2=j1+1 or j1=j2+1)&(i1=i2);
now assume A2:Int cell(GoB f,i1,j1) c= LeftComp f \/ RightComp f;
now per cases by A1;
case A3:j2=j1+1;
now per cases;
case 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));
then consider k such that A4: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 A4,SPPOL_1:25;
case A5:f/.k=(GoB f)*(i2,j1+1)& f/.(k+1)= (GoB f)*(i2+1,j1+1);
A6:Indices GoB f=[:dom GoB f,Seg width GoB f:] by MATRIX_1:def 5;
0<=j1 by NAT_1:18;
then 0+1<=j1+1 by AXIOMS:24;
then A7:j1+1 in Seg width GoB f by A1,A3,FINSEQ_1:3;
i2>0 by A4,NAT_1:19; then i2>=0+1 by NAT_1:38;
then i2 in dom GoB f by A1,FINSEQ_3:27;
then A8:[i2,j1+1] in Indices GoB f by A6,A7,ZFMISC_1:106;
i2<len GoB f by A1,A4,REAL_1:def 5;
then A9:i2+1<=len GoB f by NAT_1:38;
1<=i2+1 by NAT_1:29;
then i2+1 in dom GoB f by A9,FINSEQ_3:27;
then [i2+1,j1+1] in Indices GoB f by A6,A7,ZFMISC_1:106;
then A10:left_cell(f,k) = cell(GoB f,i2,j1+1)
by A4,A5,A8,GOBOARD5:29;
A11: Int left_cell(f,k) c= LeftComp f by A4,GOBOARD9:24;
LeftComp f c= LeftComp f \/ RightComp f by XBOOLE_1:7;
hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f
by A10,A11,XBOOLE_1:1;
case A12:f/.k=(GoB f)*(i2+1,j1+1)& f/.(k+1)= (GoB f)*(i2,j1+1);
A13:Indices GoB f=[:dom GoB f,Seg width GoB f:] by MATRIX_1:def 5;
0<=j1 by NAT_1:18;
then 0+1<=j1+1 by AXIOMS:24;
then A14:j1+1 in Seg width GoB f by A1,A3,FINSEQ_1:3;
i2>0 by A4,NAT_1:19; then i2>=0+1 by NAT_1:38;
then i2 in dom GoB f by A1,FINSEQ_3:27;
then A15:[i2,j1+1] in Indices GoB f by A13,A14,ZFMISC_1:106;
i2<len GoB f by A1,A4,REAL_1:def 5;
then A16:i2+1<=len GoB f by NAT_1:38;
1<=i2+1 by NAT_1:29;
then i2+1 in dom GoB f by A16,FINSEQ_3:27;
then [i2+1,j1+1] in Indices GoB f by A13,A14,ZFMISC_1:106;
then A17:right_cell(f,k) = cell(GoB f,i2,j1+1)
by A4,A12,A15,GOBOARD5:30;
A18: Int right_cell(f,k) c= RightComp f by A4,GOBOARD9:28;
RightComp f c= LeftComp f \/ RightComp f by XBOOLE_1:7;
hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f
by A17,A18,XBOOLE_1:1;
end;
hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f;
case A19: 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 A19;
case A20:i2=0;
reconsider p=|[((GoB f)*(1,j1+1))`1-1,((GoB f)*(1,j1+1))`2]| as
Point of TOP-REAL 2;
A21:1<len GoB f by GOBOARD7:34;
A22:1<width GoB f by GOBOARD7:35;
A23: 1<=1+j1 by NAT_1:29;
then ((GoB f)*(1,j1+1))`1=((GoB f)*(1,1))`1 by A1,A3,A21,GOBOARD5:3
;
then A24:p`1=((GoB f)*(1,1))`1-1 by EUCLID:56;
p`1<p`1+1 by REAL_1:69;
then A25:p`1< ((GoB f)*(1,1))`1 by A24,XCMPLX_1:27;
A26:p in {p} by TARSKI:def 1;
reconsider P={p} as Subset of TOP-REAL 2;
(for q being Point of TOP-REAL 2
st q in P holds q`1<((GoB f)*(1,1))`1) implies
P misses L~f by GOBOARD8:21;
then A27: {p} c= (L~f)` by A25,SUBSET_1:43,TARSKI:def 1;
then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by A26,
JORDAN1:1;
p in {|[s,r]|:s<=(GoB f)*(1,1)`1}
proof
p=|[p`1,p`2]| by EUCLID:57;
hence thesis by A25;
end;
then A28:p in v_strip(GoB f,i2) by A20,A22,GOBOARD5:11;
0<=j1 by NAT_1:18;
then A29: j1=0 or j1>=0+1 by NAT_1:38;
now per cases by A1,A3,A29,REAL_1:def 5;
case A30:j1>=1 & j1+1<width GoB f;
then A31:1<=j1+1 & j1+1<width GoB f by NAT_1:29;
A32:1<=j1 & j1<width GoB f by A30,NAT_1:38;
p in {|[s,r]|:(GoB f)*(1,j1)`2<=r & r<=(GoB f)*(1,j1+1)`2}
proof j1<j1+1 by NAT_1:38;
then ((GoB f)*(1,j1))`2<((GoB f)*(1,j1+1))`2 by A21,A30,GOBOARD5:
5;
hence thesis;
end;
then A33:p in h_strip(GoB f,j1) by A21,A32,GOBOARD5:6;
A34:j1+1+1<=width GoB f by A30,NAT_1:38;
p in {|[s,r]|:(GoB f)*(1,j1+1)`2<=r & r<=(GoB f)*(1,j1+1+1)`2}
proof j1+1<j1+1+1 by NAT_1:38;
then ((GoB f)*(1,j1+1)`2<=((GoB f)*(1,j1+1))`2
& ((GoB f)*(1,j1+1))`2<=(GoB f)*(1,j1+1+1)`2)
by A21,A23,A34,GOBOARD5:5;
hence thesis;
end;
then p in h_strip(GoB f,j1+1) by A21,A31,GOBOARD5:6;
then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A28,A33,XBOOLE_0:
def 3
;
then p in cell(GoB f,i2,j1) &
p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j1+1)/\((L~f)`) &
p in cell(GoB f,i2,j1)/\((L~f)`) by A26,A27,XBOOLE_0:def 3;
case A35:j1>=1 & j1+1=width GoB f;
A36: j1<j1+1 by NAT_1:38;
A37:1<=j1 & j1<width GoB f by A35,NAT_1:38;
p in {|[s,r]|:(GoB f)*(1,j1)`2<=r & r<=(GoB f)*(1,j1+1)`2}
proof
((GoB f)*(1,j1))`2<((GoB f)*(1,j1+1))`2 by A21,A35,A36,GOBOARD5
:5;
hence thesis;
end;
then A38:p in h_strip(GoB f,j1) by A21,A37,GOBOARD5:6;
p in {|[s,r]|:(GoB f)*(1,j1+1)`2<=r};
then p in h_strip(GoB f,j1+1) by A21,A35,GOBOARD5:7;
then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A28,A38,XBOOLE_0:
def 3
;
then p in cell(GoB f,i2,j1) &
p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j1+1)/\((L~f)`) &
p in cell(GoB f,i2,j1)/\((L~f)`) by A26,A27,XBOOLE_0:def 3;
case A39:j1=0 & j1+1<width GoB f;
then p in {|[s,r]|: r<=(GoB f)*(1,1)`2};
then A40:p in h_strip(GoB f,j1) by A21,A39,GOBOARD5:8;
A41:j1+1+1<=width GoB f by A39,NAT_1:38;
p in {|[s,r]|:(GoB f)*(1,j1+1)`2<=r & r<=(GoB f)*(1,j1+1+1)`2}
proof j1+1<j1+1+1 by NAT_1:38;
then ((GoB f)*(1,j1+1)`2<=((GoB f)*(1,j1+1))`2
& ((GoB f)*(1,j1+1))`2<=(GoB f)*(1,j1+1+1)`2) by A21,A23,A41,
GOBOARD5:5;
hence thesis;
end;
then p in h_strip(GoB f,j1+1) by A21,A39,GOBOARD5:6;
then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A28,A40,XBOOLE_0:
def 3
;
then p in cell(GoB f,i2,j1) &
p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j1+1)/\((L~f)`) &
p in cell(GoB f,i2,j1)/\((L~f)`) by A26,A27,XBOOLE_0:def 3;
case A42:j1=0 & j1+1=width GoB f;
then p in {|[s,r]|: r<=(GoB f)*(1,1)`2};
then A43:p in h_strip(GoB f,j1) by A21,A42,GOBOARD5:8;
p in {|[s,r]|:(GoB f)*(1,j1+1)`2<=r};
then p in h_strip(GoB f,j1+1) by A21,A42,GOBOARD5:7;
then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A28,A43,XBOOLE_0:
def 3
;
then p in cell(GoB f,i2,j1) &
p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j1+1)/\((L~f)`) &
p in cell(GoB f,i2,j1)/\((L~f)`) by A26,A27,XBOOLE_0:def 3;
end;
then A44:p in Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`)
& p in Cl Down(Int cell(GoB f,i2,j1),(L~f)`) by A1,Th3;
A45:Down(LeftComp f,(L~f)`)=LeftComp f &
Down(RightComp f,(L~f)`)=RightComp f by Th6;
Down(Int cell(GoB f,i2,j1),(L~f)`)
c= LeftComp f \/ RightComp f by A1,A2,Th4;
then Down(Int cell(GoB f,i2,j1),(L~f)`)
c= Down(LeftComp f \/ RightComp f,(L~f)`)
by A45,GOBRD11:4;
then A46:Cl Down(Int cell(GoB f,i2,j1),(L~f)`)
c= Cl Down(LeftComp f \/ RightComp f,(L~f)`)
by PRE_TOPC:49;
A47:Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`) is connected
by A1,A3,Th4;
Down(LeftComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm4;
then Down(LeftComp f,(L~f)`) is closed by CONNSP_1:35;
then A48:Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`)
by PRE_TOPC:52;
Down(RightComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm5;
then Down(RightComp f,(L~f)`) is closed by CONNSP_1:35;
then A49:Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`)
by PRE_TOPC:52;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
=Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
then A50:Cl Down(LeftComp f \/ RightComp f,(L~f)`)
=Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A48,A49,PRE_TOPC:50;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
is a_union_of_components of (TOP-REAL 2)|((L~f)`) by Th6;
then A51:skl p1 c= Down(LeftComp f,(L~f)`)
\/ Down(RightComp f,(L~f)`) by A44,A46,A50,CONNSP_3:21;
Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`) c= skl p1
by A44,A47,GOBRD11:1;
then A52: Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`)
c= Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A51,XBOOLE_1:1;
A53:Down(Int cell(GoB f,i2,j1+1),(L~f)`)
c= Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`)
by PRE_TOPC:48;
Down(Int cell(GoB f,i2,j1+1),(L~f)`)=Int cell(GoB f,i2,j1+1)
by A1,A3,Th4;
hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f
by A45,A52,A53,XBOOLE_1:1;
case A54:i2=len GoB f;
reconsider p=|[((GoB f)*(len GoB f,j1+1))`1+1,
((GoB f)*(len GoB f,j1+1))`2]| as Point of TOP-REAL 2;
A55:1<len GoB f by GOBOARD7:34;
A56:1<width GoB f by GOBOARD7:35;
A57: 1<=1+j1 by NAT_1:29;
then ((GoB f)*(len GoB f,j1+1))`1
=((GoB f)*(len GoB f,1))`1 by A1,A3,A55,GOBOARD5:3;
then A58:p`1=((GoB f)*(len GoB f,1))`1+1 by EUCLID:56;
A59: ((GoB f)*(len GoB f,1))`1<((GoB f)*(len GoB f,1))`1+1
by REAL_1:69;
A60:((GoB f)*(len GoB f,1))`1<p`1 by A58,REAL_1:69;
A61:p in {p} by TARSKI:def 1;
reconsider P={p} as Subset of TOP-REAL 2;
(for q being Point of TOP-REAL 2
st q in P holds ((GoB f)*(len GoB f,1)`1)<q`1) implies
P misses L~f by GOBOARD8:22;
then A62: {p} c= (L~f)` by A58,A59,SUBSET_1:43,TARSKI:def 1;
then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by A61,
JORDAN1:1;
p in {|[s,r]|:(GoB f)*(len (GoB f),1)`1<=s}
proof
p=|[p`1,p`2]| by EUCLID:57;
hence thesis by A60;
end;
then A63:p in v_strip(GoB f,i2) by A54,A56,GOBOARD5:10;
0<=j1 by NAT_1:18;
then A64: j1=0 or j1>=0+1 by NAT_1:38;
now per cases by A1,A3,A64,REAL_1:def 5;
case A65:j1>=1 & j1+1<width GoB f;
then A66:1<=j1+1 & j1+1<width GoB f by NAT_1:29;
A67:1<=j1 & j1<width GoB f by A65,NAT_1:38;
p in {|[s,r]|:(GoB f)*(len GoB f,j1)`2<=r &
r<=(GoB f)*(len GoB f,j1+1)`2}
proof j1<j1+1 by NAT_1:38;
then ((GoB f)*(len GoB f,j1))`2
<((GoB f)*(len GoB f,j1+1))`2 by A55,A65,GOBOARD5:5;
hence thesis;
end;
then A68:p in h_strip(GoB f,j1) by A55,A67,GOBOARD5:6;
A69:j1+1+1<=width GoB f by A65,NAT_1:38;
p in {|[s,r]|:(GoB f)*(len GoB f,j1+1)`2<=r
& r<=(GoB f)*(len GoB f,j1+1+1)`2}
proof j1+1<j1+1+1 by NAT_1:38;
then ((GoB f)*(len GoB f,j1+1)`2
<=((GoB f)*(len GoB f,j1+1))`2
& ((GoB f)*(len GoB f,j1+1))`2
<=(GoB f)*(len GoB f,j1+1+1)`2) by A55,A57,A69,GOBOARD5:5;
hence thesis;
end;
then p in h_strip(GoB f,j1+1) by A55,A66,GOBOARD5:6;
then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A63,A68,XBOOLE_0:
def 3
;
then p in cell(GoB f,i2,j1) &
p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j1+1)/\((L~f)`) &
p in cell(GoB f,i2,j1)/\((L~f)`) by A61,A62,XBOOLE_0:def 3;
case A70:j1>=1 & j1+1=width GoB f;
A71: j1<j1+1 by NAT_1:38;
A72:1<=j1 & j1<width GoB f by A70,NAT_1:38;
p in {|[s,r]|:(GoB f)*(len (GoB f),j1)`2<=r
& r<=(GoB f)*(len (GoB f),j1+1)`2}
proof
((GoB f)*(len GoB f,j1))`2
<((GoB f)*(len (GoB f),j1+1))`2 by A55,A70,A71,
GOBOARD5:5;
hence thesis;
end;
then A73:p in h_strip(GoB f,j1) by A55,A72,GOBOARD5:6;
p in {|[s,r]|:(GoB f)*(len (GoB f),j1+1)`2<=r};
then p in h_strip(GoB f,j1+1) by A55,A70,GOBOARD5:7;
then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A63,A73,XBOOLE_0:
def 3
;
then p in cell(GoB f,i2,j1) &
p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j1+1)/\((L~f)`) &
p in cell(GoB f,i2,j1)/\((L~f)`) by A61,A62,XBOOLE_0:def 3;
case A74:j1=0 & j1+1<width GoB f;
then p in {|[s,r]|: r<=(GoB f)*(len (GoB f),1)`2};
then A75:p in h_strip(GoB f,j1) by A55,A74,GOBOARD5:8;
A76:j1+1+1<=width GoB f by A74,NAT_1:38;
p in {|[s,r]|:(GoB f)*(len (GoB f),j1+1)`2<=r
& r<=(GoB f)*(len (GoB f),j1+1+1)`2}
proof
j1+1<j1+1+1 by NAT_1:38;
then ((GoB f)*(len (GoB f),j1+1)`2
<=((GoB f)*(len (GoB f),j1+1))`2
& ((GoB f)*(len (GoB f),j1+1))`2
<=(GoB f)*(len (GoB f),j1+1+1)`2) by A55,A57,A76,GOBOARD5:5;
hence thesis;
end;
then p in h_strip(GoB f,j1+1) by A55,A74,GOBOARD5:6;
then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A63,A75,XBOOLE_0:
def 3
;
then p in cell(GoB f,i2,j1) &
p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j1+1)/\((L~f)`) &
p in cell(GoB f,i2,j1)/\((L~f)`) by A61,A62,XBOOLE_0:def 3;
case j1=0 & j1+1=width GoB f;
hence contradiction by GOBOARD7:35;
end;
then A77:p in Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`)
& p in Cl Down(Int cell(GoB f,i2,j1),(L~f)`) by A1,Th3;
A78:Down(LeftComp f,(L~f)`)=LeftComp f &
Down(RightComp f,(L~f)`)=RightComp f by Th6;
Down(Int cell(GoB f,i2,j1),(L~f)`)
c= LeftComp f \/ RightComp f by A1,A2,Th4;
then Down(Int cell(GoB f,i2,j1),(L~f)`)
c= Down(LeftComp f \/ RightComp f,(L~f)`)
by A78,GOBRD11:4;
then A79:Cl Down(Int cell(GoB f,i2,j1),(L~f)`)
c= Cl Down(LeftComp f \/ RightComp f,(L~f)`)
by PRE_TOPC:49;
A80:Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`) is connected
by A1,A3,Th4;
Down(LeftComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm4;
then Down(LeftComp f,(L~f)`) is closed by CONNSP_1:35;
then A81:Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`)
by PRE_TOPC:52;
Down(RightComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm5;
then Down(RightComp f,(L~f)`) is closed by CONNSP_1:35;
then A82:Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`)
by PRE_TOPC:52;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
=Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
then A83:Cl Down(LeftComp f \/ RightComp f,(L~f)`)
=Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A81,A82,PRE_TOPC:50;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
is a_union_of_components of (TOP-REAL 2)|((L~f)`) by Th6;
then A84:skl p1 c= Down(LeftComp f,(L~f)`)
\/ Down(RightComp f,(L~f)`) by A77,A79,A83,CONNSP_3:21;
Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`) c= skl p1
by A77,A80,GOBRD11:1;
then A85: Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`)
c= Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A84,XBOOLE_1:1;
A86:Down(Int cell(GoB f,i2,j1+1),(L~f)`)
c= Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`)
by PRE_TOPC:48;
Down(Int cell(GoB f,i2,j1+1),(L~f)`)=Int cell(GoB f,i2,j1+1)
by A1,A3,Th4;
hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f
by A78,A85,A86,XBOOLE_1:1;
case A87:i2<>0 & 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 0<i2 by NAT_1:19; then A88: 0+1<=i2 by NAT_1:38;
A89:i2<len GoB f by A1,A87,REAL_1:def 5;
then A90:i2+1<=len GoB f by NAT_1:38;
for k st 1<=k & k+1<=len f holds
LSeg((GoB f)*(i2,j1+1),(GoB f)*(i2+1,j1+1))<>LSeg(f,k)
proof let k;assume A91:1<=k & k+1<=len f;
then LSeg(f,k)=LSeg(f/.k,f/.(k+1)) by TOPREAL1:def 5;
hence LSeg((GoB f)*(i2,j1+1),(GoB f)*(i2+1,j1+1))<>LSeg(f,k)
by A87,A91;
end;
then A92: 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:42;
reconsider p=1/2*((GoB f)*(i2,j1+1)+(GoB f)*(i2+1,j1+1)) as
Point of TOP-REAL 2;
A93:p`2=1/2*((GoB f)*(i2,j1+1)+(GoB f)*(i2+1,j1+1))`2 by TOPREAL3:9
.=1/2*(((GoB f)*(i2,j1+1))`2+((GoB f)*(i2+1,j1+1))`2) by
TOPREAL3:7;
A94:p`1=1/2*((GoB f)*(i2,j1+1)+(GoB f)*(i2+1,j1+1))`1 by TOPREAL3:9
.=1/2*(((GoB f)*(i2,j1+1))`1+((GoB f)*(i2+1,j1+1))`1) by
TOPREAL3:7;
then A95:p=|[1/2*(((GoB f)*(i2,j1+1))`1+((GoB f)*(i2+1,j1+1))`1),
1/2*(((GoB f)*(i2,j1+1))`2+((GoB f)*(i2+1,j1+1))`2)]|
by A93,EUCLID:57;
A96:1<len GoB f by GOBOARD7:34;
A97: 1<=1+j1 by NAT_1:29;
A98:i2<i2+1 by NAT_1:38;
A99: 1<i2+1 by A88,NAT_1:38;
A100:((GoB f)*(i2,j1+1))`1 <((GoB f)*(i2+1,j1+1))`1
by A1,A3,A88,A90,A97,A98,GOBOARD5:4;
then A101:((GoB f)*(i2,j1+1))`1+((GoB f)*(i2,j1+1))`1
<((GoB f)*(i2,j1+1))`1+((GoB f)*(i2+1,j1+1))`1
by REAL_1:67;
A102:((GoB f)*(i2,j1+1))`1+((GoB f)*(i2+1,j1+1))`1
<((GoB f)*(i2+1,j1+1))`1+((GoB f)*(i2+1,j1+1))`1
by A100,REAL_1:67;
(((GoB f)*(i2,j1+1))`1+((GoB f)*(i2,j1+1))`1)/2
<(((GoB f)*(i2,j1+1))`1+((GoB f)*(i2+1,j1+1))`1)/2
by A101,REAL_1:73;
then A103:((GoB f)*(i2,j1+1))`1
<(((GoB f)*(i2,j1+1))`1+((GoB f)*(i2+1,j1+1))`1)/2
by XCMPLX_1:65;
(((GoB f)*(i2,j1+1))`1+((GoB f)*(i2+1,j1+1))`1)/2
<(((GoB f)*(i2+1,j1+1))`1+((GoB f)*(i2+1,j1+1))`1)/2
by A102,REAL_1:73;
then A104:((GoB f)*(i2+1,j1+1))`1
>(((GoB f)*(i2,j1+1))`1+((GoB f)*(i2+1,j1+1))`1)/2
by XCMPLX_1:65;
A105:p in {p} by TARSKI:def 1;
reconsider P={p} as Subset of TOP-REAL 2;
(for x st x in P holds not x in (L~f)) implies
P misses L~f by XBOOLE_0:3;
then A106: {p} c= (L~f)` by A1,A3,A88,A89,A92,NAT_1:29,38,SUBSET_1:
43,TARSKI:def 1;
then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by A105,
JORDAN1:1;
A107:1<=j1+1 & j1+1<=width GoB f by A1,A3,NAT_1:29;
p in {|[s,r]|:(GoB f)*(i2,j1+1)`1<=s & s<=(GoB f)*(i2+1,j1+1)`1}
proof
p=|[p`1,p`2]| & ((GoB f)*(i2,j1+1)`1<=p`1
& p`1<=(GoB f)*(i2+1,j1+1)`1) by A94,A103,A104,EUCLID:57,
XCMPLX_1:100;
hence thesis;
end;
then A108:p in v_strip(GoB f,i2) by A88,A89,A107,GOBOARD5:9;
0<=j1 by NAT_1:18;
then A109: j1=0 or j1>=0+1 by NAT_1:38;
now per cases by A1,A3,A109,REAL_1:def 5;
case A110:j1>=1 & j1+1<width GoB f;
then A111:1<=j1+1 & j1+1<width GoB f by NAT_1:29;
A112:1<=j1 & j1<width GoB f by A110,NAT_1:38;
p in {|[s,r]|:(GoB f)*(1,j1)`2<=r & r<=(GoB f)*(1,j1+1)`2}
proof A113: j1<j1+1 by NAT_1:38;
A114:((GoB f)*(i2,j1+1))`2=((GoB f)*(1,j1+1))`2
by A1,A3,A88,A97,GOBOARD5:2;
A115:((GoB f)*(i2+1,j1+1))`2=((GoB f)*(1,j1+1))`2
by A1,A3,A90,A97,A99,GOBOARD5:2;
A116:((GoB f)*(1,j1))`2<((GoB f)*(1,j1+1))`2
by A96,A110,A113,GOBOARD5:5;
1/2*(((GoB f)*(i2,j1+1))`2+((GoB f)*(i2+1,j1+1))`2)
=((GoB f)*(1,j1+1))`2 by A114,A115,Lm1;
hence thesis by A95,A116;
end;
then A117:p in h_strip(GoB f,j1) by A96,A112,GOBOARD5:6;
A118:j1+1+1<=width GoB f by A110,NAT_1:38;
p in {|[s,r]|:(GoB f)*(1,j1+1)`2<=r & r<=(GoB f)*(1,j1+1+1)`2}
proof
A119: j1+1<j1+1+1 by NAT_1:38;
A120:((GoB f)*(i2,j1+1))`2=((GoB f)*(1,j1+1))`2
by A1,A3,A88,A97,GOBOARD5:2;
A121:((GoB f)*(i2+1,j1+1))`2=((GoB f)*(1,j1+1))`2
by A1,A3,A90,A97,A99,GOBOARD5:2;
A122:((GoB f)*(1,j1+1))`2<((GoB f)*(1,j1+1+1))`2
by A96,A97,A118,A119,GOBOARD5:5;
1/2*(((GoB f)*(i2,j1+1))`2+((GoB f)*(i2+1,j1+1))`2)
=((GoB f)*(1,j1+1))`2 by A120,A121,Lm1;
hence thesis by A95,A122;
end;
then p in h_strip(GoB f,j1+1) by A96,A111,GOBOARD5:6;
then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A108,A117,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j1) &
p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j1+1)/\((L~f)`) &
p in cell(GoB f,i2,j1)/\((L~f)`) by A105,A106,XBOOLE_0:def 3;
case A123:j1>=1 & j1+1=width GoB f;
A124: j1<j1+1 by NAT_1:38;
p in {|[s,r]|:(GoB f)*(1,j1)`2<=r & r<=(GoB f)*(1,j1+1)`2}
proof
A125:((GoB f)*(i2,j1+1))`2=((GoB f)*(1,j1+1))`2
by A1,A3,A88,A97,GOBOARD5:2;
A126:((GoB f)*(i2+1,j1+1))`2=((GoB f)*(1,j1+1))`2
by A1,A3,A90,A97,A99,GOBOARD5:2;
A127:((GoB f)*(1,j1))`2<((GoB f)*(1,j1+1))`2
by A96,A123,A124,GOBOARD5:5;
1/2*(((GoB f)*(i2,j1+1))`2+((GoB f)*(i2+1,j1+1))`2)
=((GoB f)*(1,j1+1))`2 by A125,A126,Lm1;
hence thesis by A95,A127;
end;
then A128:p in h_strip(GoB f,j1) by A96,A123,A124,GOBOARD5:6;
p in {|[s,r]|:(GoB f)*(1,j1+1)`2<=r}
proof
A129:((GoB f)*(i2,j1+1))`2=((GoB f)*(1,j1+1))`2
by A1,A3,A88,A97,GOBOARD5:2;
((GoB f)*(i2+1,j1+1))`2=((GoB f)*(1,j1+1))`2
by A1,A3,A90,A97,A99,GOBOARD5:2;
then (GoB f)*(1,j1+1)`2
<=1/2*(((GoB f)*(i2,j1+1))`2+((GoB f)*(i2+1,j1+1))`2) by
A129,Lm1;
hence thesis by A95;
end;
then p in h_strip(GoB f,j1+1) by A96,A123,GOBOARD5:7;
then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A108,A128,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j1) &
p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j1+1)/\((L~f)`) &
p in cell(GoB f,i2,j1)/\((L~f)`) by A105,A106,XBOOLE_0:def 3;
case A130:j1=0 & j1+1<width GoB f;
p in {|[s,r]|: r<=(GoB f)*(1,1)`2}
proof
A131:((GoB f)*(i2,j1+1))`2=((GoB f)*(1,j1+1))`2
by A1,A3,A88,A97,GOBOARD5:2;
((GoB f)*(i2+1,j1+1))`2=((GoB f)*(1,j1+1))`2
by A1,A3,A90,A97,A99,GOBOARD5:2;
then 1/2*(((GoB f)*(i2,j1+1))`2+((GoB f)*(i2+1,j1+1))`2)
<=((GoB f)*(1,1))`2 by A130,A131,Lm1;
hence thesis by A95;
end;
then A132:p in h_strip(GoB f,j1) by A96,A130,GOBOARD5:8;
A133:j1+1+1<=width GoB f by A130,NAT_1:38;
p in {|[s,r]|:(GoB f)*(1,j1+1)`2<=r & r<=(GoB f)*(1,j1+1+1)`2}
proof A134: j1+1<j1+1+1 by NAT_1:38;
A135:((GoB f)*(i2,j1+1))`2=((GoB f)*(1,j1+1))`2
by A1,A3,A88,A97,GOBOARD5:2;
A136:((GoB f)*(i2+1,j1+1))`2=((GoB f)*(1,j1+1))`2
by A1,A3,A90,A97,A99,GOBOARD5:2;
A137:((GoB f)*(1,j1+1))`2<((GoB f)*(1,j1+1+1))`2
by A96,A97,A133,A134,GOBOARD5:5;
1/2*(((GoB f)*(i2,j1+1))`2+((GoB f)*(i2+1,j1+1))`2)
=((GoB f)*(1,j1+1))`2 by A135,A136,Lm1;
hence thesis by A95,A137;
end;
then p in h_strip(GoB f,j1+1) by A96,A130,GOBOARD5:6;
then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A108,A132,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j1) &
p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j1+1)/\((L~f)`) &
p in cell(GoB f,i2,j1)/\((L~f)`) by A105,A106,XBOOLE_0:def 3;
case j1=0 & j1+1=width GoB f;
hence contradiction by GOBOARD7:35;
end;
then A138:p in Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`)
& p in Cl Down(Int cell(GoB f,i2,j1),(L~f)`) by A1,Th3;
A139:Down(LeftComp f,(L~f)`)=LeftComp f &
Down(RightComp f,(L~f)`)=RightComp f by Th6;
Down(Int cell(GoB f,i2,j1),(L~f)`)
c= LeftComp f \/ RightComp f by A1,A2,Th4;
then Down(Int cell(GoB f,i2,j1),(L~f)`)
c= Down(LeftComp f \/ RightComp f,(L~f)`)
by A139,GOBRD11:4;
then A140:Cl Down(Int cell(GoB f,i2,j1),(L~f)`)
c= Cl Down(LeftComp f \/ RightComp f,(L~f)`)
by PRE_TOPC:49;
A141:Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`) is connected
by A1,A3,Th4;
Down(LeftComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm4;
then Down(LeftComp f,(L~f)`) is closed by CONNSP_1:35;
then A142:Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`)
by PRE_TOPC:52;
Down(RightComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm5;
then Down(RightComp f,(L~f)`) is closed by CONNSP_1:35;
then A143:Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`)
by PRE_TOPC:52;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
=Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
then A144:Cl Down(LeftComp f \/ RightComp f,(L~f)`)
=Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A142,A143,PRE_TOPC:50;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
is a_union_of_components of (TOP-REAL 2)|((L~f)`) by Th6;
then A145:skl p1 c= Down(LeftComp f,(L~f)`)
\/ Down(RightComp f,(L~f)`) by A138,A140,A144,CONNSP_3:21;
Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`) c= skl p1
by A138,A141,GOBRD11:1;
then A146: Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`)
c= Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A145,XBOOLE_1:1;
A147:Down(Int cell(GoB f,i2,j1+1),(L~f)`)
c= Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`)
by PRE_TOPC:48;
Down(Int cell(GoB f,i2,j1+1),(L~f)`)=Int cell(GoB f,i2,j1+1)
by A1,A3,Th4;
hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f
by A139,A146,A147,XBOOLE_1:1;
end;
hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f;
end;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by A3;
case A148: j1=j2+1;
then A149:j1-'1=j2 by BINARITH:39;
A150:j2<j2+1 by NAT_1:38;
A151:j2<j1 by A148,NAT_1:38;
A152:1<=j2+1 by NAT_1:29;
A153:1<=j1 by A148,NAT_1:29;
A154:j2+1<j2+1+1 by NAT_1:38;
j1-1=j2 by A148,XCMPLX_1:26;
then j1-1>=0 by NAT_1:18;
then j1-'1=j1-1 by BINARITH:def 3;
then A155:j1=j1-'1+1 by XCMPLX_1:27;
A156:1<=j1-'1+1 by NAT_1:29;
A157:j1-'1<j1 by A148,A151,BINARITH:39;
now per cases;
case 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));
then consider k such that A158:1<=k & k+1 <=len f
& i2<>0 & i2<>len GoB f &
LSeg(f/.k,f/.(k+1))
=LSeg((GoB f)*(i2,j1-'1+1),(GoB f)*(i2+1,j1-'1+1))
by A149;
now per cases by A158,SPPOL_1:25;
case A159:f/.k=(GoB f)*(i2,j1-'1+1)
& f/.(k+1)= (GoB f)*(i2+1,j1-'1+1);
A160:Indices GoB f=[:dom GoB f,Seg width GoB f:] by MATRIX_1:def 5;
j1-'1<width GoB f by A1,A157,AXIOMS:22;
then j1-'1+1<=width GoB f by NAT_1:38;
then A161:j1-'1+1 in Seg width GoB f by A156,FINSEQ_1:3;
i2>0 by A158,NAT_1:19; then i2>=0+1 by NAT_1:38;
then i2 in dom GoB f by A1,FINSEQ_3:27;
then A162:[i2,j1-'1+1] in Indices GoB f by A160,A161,ZFMISC_1:106;
i2<len GoB f by A1,A158,REAL_1:def 5;
then A163:i2+1<=len GoB f by NAT_1:38;
1<=i2+1 by NAT_1:29;
then i2+1 in dom GoB f by A163,FINSEQ_3:27;
then [i2+1,j1-'1+1] in Indices GoB f by A160,A161,ZFMISC_1:106;
then A164:right_cell(f,k) = cell(GoB f,i2,j1-'1)
by A158,A159,A162,GOBOARD5:29;
A165: Int right_cell(f,k) c= RightComp f by A158,GOBOARD9:28;
RightComp f c= LeftComp f \/ RightComp f by XBOOLE_1:7;
hence Int cell(GoB f,i2,j1-'1) c= LeftComp f \/ RightComp f
by A164,A165,XBOOLE_1:1;
case A166:f/.k=(GoB f)*(i2+1,j1-'1+1)
& f/.(k+1)= (GoB f)*(i2,j1-'1+1);
A167:Indices GoB f=[:dom GoB f,Seg width GoB f:] by MATRIX_1:def 5;
A168:j1-'1+1 in Seg width GoB f by A1,A153,A155,FINSEQ_1:3;
i2>0 by A158,NAT_1:19; then i2>=0+1 by NAT_1:38;
then i2 in dom GoB f by A1,FINSEQ_3:27;
then A169:[i2,j1-'1+1] in Indices GoB f by A167,A168,ZFMISC_1:106;
i2<len GoB f by A1,A158,REAL_1:def 5;
then A170:i2+1<=len GoB f by NAT_1:38;
1<=i2+1 by NAT_1:29;
then i2+1 in dom GoB f by A170,FINSEQ_3:27;
then [i2+1,j1-'1+1] in Indices GoB f by A167,A168,ZFMISC_1:106;
then A171:left_cell(f,k) = cell(GoB f,i2,j1-'1)
by A158,A166,A169,GOBOARD5:30;
A172: Int left_cell(f,k) c= LeftComp f by A158,GOBOARD9:24;
LeftComp f c= LeftComp f \/ RightComp f by XBOOLE_1:7;
hence Int cell(GoB f,i2,j1-'1) c= LeftComp f \/ RightComp f
by A171,A172,XBOOLE_1:1;
end;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f
by A148,BINARITH:39;
case A173: 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 A173;
case A174:i2=0;
reconsider p=|[((GoB f)*(1,j2+1))`1-1,((GoB f)*(1,j2+1))`2]| as
Point of TOP-REAL 2;
A175:1<len GoB f by GOBOARD7:34;
A176:1<width GoB f by GOBOARD7:35;
A177:1<=j2+1 by NAT_1:29;
then ((GoB f)*(1,j2+1))`1=((GoB f)*(1,1))`1 by A1,A148,A175,
GOBOARD5:3;
then A178:p`1=((GoB f)*(1,1))`1-1 by EUCLID:56;
p`1<p`1+1 by REAL_1:69;
then A179:p`1< ((GoB f)*(1,1))`1 by A178,XCMPLX_1:27;
A180:p in {p} by TARSKI:def 1;
reconsider P={p} as Subset of TOP-REAL 2;
(for q being Point of TOP-REAL 2
st q in P holds q`1<((GoB f)*(1,1))`1) implies
P misses L~f by GOBOARD8:21;
then A181: {p} c= (L~f)` by A179,SUBSET_1:43,TARSKI:def 1;
then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by A180,
JORDAN1:1;
p in {|[s,r]|:s<=(GoB f)*(1,1)`1}
proof
p=|[p`1,p`2]| by EUCLID:57;
hence thesis by A179;
end;
then A182:p in v_strip(GoB f,i2) by A174,A176,GOBOARD5:11;
now per cases by A1,A148,NAT_1:18,REAL_1:def 5;
case A183:j2+1<width GoB f & j2>0; then A184: 0+1<=j2 by NAT_1:38;
then A185:1<=j2+1 & j2+1<width GoB f by A183,NAT_1:38;
A186:1<=j2 & j2<width GoB f by A183,A184,NAT_1:38;
p in {|[s,r]|:(GoB f)*(1,j2)`2<=r & r<=(GoB f)*(1,j2+1)`2}
proof j2<j2+1 by NAT_1:38;
then ((GoB f)*(1,j2))`2<((GoB f)*(1,j2+1))`2 by A1,A148,A175,A184
,GOBOARD5:5;
hence thesis;
end;
then A187:p in h_strip(GoB f,j2) by A175,A186,GOBOARD5:6;
A188:j2+1+1<=width GoB f by A183,NAT_1:38;
p in {|[s,r]|:(GoB f)*(1,j2+1)`2<=r & r<=(GoB f)*(1,j2+1+1)`2}
proof j2+1<j2+1+1 by NAT_1:38;
then ((GoB f)*(1,j2+1)`2<=((GoB f)*(1,j2+1))`2
& ((GoB f)*(1,j2+1))`2<=(GoB f)*(1,j2+1+1)`2)
by A175,A177,A188,GOBOARD5:5;
hence thesis;
end;
then p in h_strip(GoB f,j2+1) by A175,A185,GOBOARD5:6;
then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A182,A187,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j2+1)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A180,A181,XBOOLE_0:def 3;
case A189:j2+1<width GoB f & j2=0;
then A190:j2+1+1<=width GoB f by NAT_1:38;
A191: j2+1<j2+1+1 by NAT_1:38;
p in {|[s,r]|: r<=(GoB f)*(1,j2+1)`2};
then A192:p in h_strip(GoB f,j2) by A175,A189,GOBOARD5:8;
p in {|[s,r]|:(GoB f)*(1,j2+1)`2<=r & r<=(GoB f)*(1,j2+1+1)`2}
proof
(GoB f)*(1,j2+1)`2<(GoB f)*(1,j2+1+1)`2 by A152,A175,A190,
A191,GOBOARD5:5;
hence thesis;
end;
then p in h_strip(GoB f,j2+1) by A175,A189,GOBOARD5:6;
then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A182,A192,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j2+1)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A180,A181,XBOOLE_0:def 3;
case A193:j2+1=width GoB f & j2>0; then A194: 0+1<=j2 by NAT_1:38;
then A195:1<=j2 & j2<width GoB f by A193,NAT_1:38;
p in {|[s,r]|:((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 A150,A175,A193,A194,
GOBOARD5:5;
hence thesis;
end;
then A196:p in h_strip(GoB f,j2) by A175,A195,GOBOARD5:6;
p in {|[s,r]|:(GoB f)*(1,j2+1)`2<=r};
then p in h_strip(GoB f,j2+1) by A175,A193,GOBOARD5:7;
then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A182,A196,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j2+1)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A180,A181,XBOOLE_0:def 3;
case A197:j2+1=width GoB f & j2=0;
then p in {|[s,r]|: r<=(GoB f)*(1,1)`2};
then A198:p in h_strip(GoB f,j2) by A175,A197,GOBOARD5:8;
p in {|[s,r]|:(GoB f)*(1,j2+1)`2<=r};
then p in h_strip(GoB f,j2+1) by A175,A197,GOBOARD5:7;
then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A182,A198,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j2+1)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A180,A181,XBOOLE_0:def 3;
end;
then A199:p in Cl Down(Int cell(GoB f,i2,j2+1),(L~f)`)
& p in Cl Down(Int cell(GoB f,i2,j2),(L~f)`) by A1,Th3;
A200:Down(LeftComp f,(L~f)`)=LeftComp f &
Down(RightComp f,(L~f)`)=RightComp f by Th6;
Down(Int cell(GoB f,i2,j1),(L~f)`)
c= LeftComp f \/ RightComp f by A1,A2,Th4;
then Down(Int cell(GoB f,i2,j1),(L~f)`)
c= Down(LeftComp f \/ RightComp f,(L~f)`) by A200,GOBRD11:4;
then A201:Cl Down(Int cell(GoB f,i2,j1),(L~f)`)
c= Cl Down(LeftComp f \/ RightComp f,(L~f)`)
by PRE_TOPC:49;
A202:Cl Down(Int cell(GoB f,i2,j2),(L~f)`) is connected
by A1,Th4;
Down(LeftComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm4;
then Down(LeftComp f,(L~f)`) is closed by CONNSP_1:35;
then A203:Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`)
by PRE_TOPC:52;
Down(RightComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm5;
then Down(RightComp f,(L~f)`) is closed by CONNSP_1:35;
then A204:Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`)
by PRE_TOPC:52;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
=Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
then A205:Cl Down(LeftComp f \/ RightComp f,(L~f)`)
=Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A203,A204,PRE_TOPC:50;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
is a_union_of_components of (TOP-REAL 2)|((L~f)`) by Th6;
then A206:skl p1 c= Down(LeftComp f,(L~f)`)
\/ Down(RightComp f,(L~f)`) by A148,A199,A201,A205,CONNSP_3:21
;
Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= skl p1
by A199,A202,GOBRD11:1;
then A207: Cl Down(Int cell(GoB f,i2,j2),(L~f)`)
c= Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A206,XBOOLE_1:1;
A208:Down(Int cell(GoB f,i2,j2),(L~f)`)
c= Cl Down(Int cell(GoB f,i2,j2),(L~f)`)
by PRE_TOPC:48;
Down(Int cell(GoB f,i2,j2),(L~f)`)=Int cell(GoB f,i2,j2)
by A1,Th4;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f
by A200,A207,A208,XBOOLE_1:1;
case A209:i2=len GoB f;
reconsider p=|[((GoB f)*(len GoB f,j2+1))`1+1,
((GoB f)*(len GoB f,j2+1))`2]| as Point of TOP-REAL 2;
A210:1<len GoB f by GOBOARD7:34;
A211:1<width GoB f by GOBOARD7:35;
1<=j2+1 by NAT_1:29;
then ((GoB f)*(len GoB f,j2+1))`1
=((GoB f)*(len GoB f,1))`1 by A1,A148,A210,GOBOARD5:3;
then A212:p`1=((GoB f)*(len GoB f,1))`1+1 by EUCLID:56;
A213: ((GoB f)*(len GoB f,1))`1<((GoB f)*(len GoB f,1))`1+1
by REAL_1:69;
A214:((GoB f)*(len GoB f,1))`1<p`1 by A212,REAL_1:69;
A215:p in {p} by TARSKI:def 1;
reconsider P={p} as Subset of TOP-REAL 2;
(for q being Point of TOP-REAL 2
st q in P holds ((GoB f)*(len GoB f,1)`1)<q`1) implies
P misses L~f by GOBOARD8:22;
then A216: {p} c= (L~f)` by A212,A213,SUBSET_1:43,TARSKI:def 1;
then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by A215,
JORDAN1:1;
p in {|[s,r]|:(GoB f)*(len (GoB f),1)`1<=s}
proof
p=|[p`1,p`2]| by EUCLID:57;
hence thesis by A214;
end;
then A217:p in v_strip(GoB f,i2) by A209,A211,GOBOARD5:10;
now per cases by A1,A148,NAT_1:18,REAL_1:def 5;
case A218:j2+1<width GoB f & j2>0;
then A219:j2+1+1<=width GoB f by NAT_1:38;
A220:0+1<=j2 by A218,NAT_1:38;
A221:j2<j2+1 by NAT_1:38;
A222:1<=j2+1 & j2+1<width GoB f by A218,NAT_1:29;
A223:1<=j2 & j2<width GoB f by A218,A220,NAT_1:38;
p in {|[s,r]|:(GoB f)*(len GoB f,j2)`2<=r &
r<=(GoB f)*(len GoB f,j2+1)`2}
proof
((GoB f)*(len GoB f,j2))`2
<((GoB f)*(len GoB f,j2+1))`2 by A1,A148,A210,A220,A221,
GOBOARD5:5;
hence thesis;
end;
then A224:p in h_strip(GoB f,j2) by A210,A223,GOBOARD5:6;
p in {|[s,r]|:(GoB f)*(len GoB f,j2+1)`2<=r
& r<=(GoB f)*(len GoB f,j2+1+1)`2}
proof
j2+1<j2+1+1 by NAT_1:38;
then ((GoB f)*(len GoB f,j2+1)`2
<=((GoB f)*(len GoB f,j2+1))`2
& ((GoB f)*(len GoB f,j2+1))`2
<=(GoB f)*(len GoB f,j2+1+1)`2) by A152,A210,A219,GOBOARD5:5
;
hence thesis;
end;
then p in h_strip(GoB f,j2+1) by A210,A222,GOBOARD5:6;
then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A217,A224,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j2+1)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A215,A216,XBOOLE_0:def 3;
case A225:j2+1<width GoB f & j2=0;
then A226:j2+1+1<=width GoB f by NAT_1:38;
p in {|[s,r]|: r<=(GoB f)*(len (GoB f),1)`2} by A225;
then A227:p in h_strip(GoB f,j2) by A210,A225,GOBOARD5:8;
p in {|[s,r]|:(GoB f)*(len (GoB f),j2+1)`2<=r &
r<=(GoB f)*(len (GoB f),j2+1+1)`2}
proof
(GoB f)*(len (GoB f),j2+1)`2
<(GoB f)*(len (GoB f),j2+1+1)`2 by A152,A154,A210,A226,GOBOARD5
:5;
hence thesis;
end;
then p in h_strip(GoB f,j2+1) by A210,A225,GOBOARD5:6;
then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A217,A227,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j2+1)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A215,A216,XBOOLE_0:def 3;
case A228:j2+1=width GoB f & j2>0;
then 0+1<=j2 by NAT_1:38;
then A229:1<=j2 & j2<width GoB f by A228,NAT_1:38;
p in {|[s,r]|: (GoB f)*(len GoB f,width GoB f)`2<=r} by A228;
then A230:p in h_strip(GoB f,j2+1) by A210,A228,GOBOARD5:7;
p in {|[s,r]|:(GoB f)*(len (GoB f),j2)`2<=r
& r<=(GoB f)*(len (GoB f),j2+1)`2}
proof
((GoB f)*(len (GoB f),j2+1)`2
<=((GoB f)*(len (GoB f),j2+1))`2
& ((GoB f)*(len (GoB f),j2))`2
<=(GoB f)*(len (GoB f),j2+1)`2) by A210,A228,A229,GOBOARD5:5
;
hence thesis;
end;
then p in h_strip(GoB f,j2) by A210,A229,GOBOARD5:6;
then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A217,A230,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j2+1)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A215,A216,XBOOLE_0:def 3;
case j2+1=width GoB f & j2=0;
hence contradiction by GOBOARD7:35;
end;
then A231:p in Cl Down(Int cell(GoB f,i2,j2+1),(L~f)`)
& p in Cl Down(Int cell(GoB f,i2,j2),(L~f)`) by A1,Th3;
A232:Down(LeftComp f,(L~f)`)=LeftComp f &
Down(RightComp f,(L~f)`)=RightComp f by Th6;
Down(Int cell(GoB f,i2,j1),(L~f)`)
c= LeftComp f \/ RightComp f by A1,A2,Th4;
then Down(Int cell(GoB f,i2,j1),(L~f)`)
c= Down(LeftComp f \/ RightComp f,(L~f)`)
by A232,GOBRD11:4;
then A233:Cl Down(Int cell(GoB f,i2,j1),(L~f)`)
c= Cl Down(LeftComp f \/ RightComp f,(L~f)`)
by PRE_TOPC:49;
A234:Cl Down(Int cell(GoB f,i2,j2),(L~f)`) is connected
by A1,Th4;
Down(LeftComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm4;
then Down(LeftComp f,(L~f)`) is closed by CONNSP_1:35;
then A235:Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`)
by PRE_TOPC:52;
Down(RightComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm5;
then Down(RightComp f,(L~f)`) is closed by CONNSP_1:35;
then A236:Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`)
by PRE_TOPC:52;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
=Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
then A237:Cl Down(LeftComp f \/ RightComp f,(L~f)`)
=Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A235,A236,PRE_TOPC:50;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
is a_union_of_components of (TOP-REAL 2)|((L~f)`) by Th6;
then A238:skl p1 c= Down(LeftComp f,(L~f)`)
\/ Down(RightComp f,(L~f)`) by A148,A231,A233,A237,CONNSP_3:21
;
Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= skl p1
by A231,A234,GOBRD11:1;
then A239: Cl Down(Int cell(GoB f,i2,j2),(L~f)`)
c= Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A238,XBOOLE_1:1;
A240:Down(Int cell(GoB f,i2,j2),(L~f)`)
c= Cl Down(Int cell(GoB f,i2,j2),(L~f)`)
by PRE_TOPC:48;
Down(Int cell(GoB f,i2,j2),(L~f)`)=Int cell(GoB f,i2,j2)
by A1,Th4;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f
by A232,A239,A240,XBOOLE_1:1;
case A241:i2<>0 & 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 0<i2 by NAT_1:19; then A242: 0+1<=i2 by NAT_1:38;
A243:i2<len GoB f by A1,A241,REAL_1:def 5;
then A244:i2+1<=len GoB f by NAT_1:38;
for k st 1<=k & k+1<=len f holds
LSeg((GoB f)*(i2,j2+1),(GoB f)*(i2+1,j2+1))<>LSeg(f,k)
proof let k;assume A245:1<=k & k+1<=len f;
then LSeg(f,k)=LSeg(f/.k,f/.(k+1)) by TOPREAL1:def 5;
hence LSeg((GoB f)*(i2,j2+1),(GoB f)*(i2+1,j2+1))<>LSeg(f,k)
by A241,A245;
end;
then A246: 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:42;
reconsider p=1/2*((GoB f)*(i2,j2+1)+(GoB f)*(i2+1,j2+1)) as
Point of TOP-REAL 2;
A247:p`2=1/2*((GoB f)*(i2,j2+1)+(GoB f)*(i2+1,j2+1))`2 by TOPREAL3:
9
.=1/2*(((GoB f)*(i2,j2+1))`2+((GoB f)*(i2+1,j2+1))`2) by
TOPREAL3:7;
A248:p`1=1/2*((GoB f)*(i2,j2+1)+(GoB f)*(i2+1,j2+1))`1 by TOPREAL3:
9
.=1/2*(((GoB f)*(i2,j2+1))`1+((GoB f)*(i2+1,j2+1))`1) by
TOPREAL3:7;
then A249:p=|[1/2*(((GoB f)*(i2,j2+1))`1+((GoB f)*(i2+1,j2+1))`1),
1/2*(((GoB f)*(i2,j2+1))`2+((GoB f)*(i2+1,j2+1))`2)]|
by A247,EUCLID:57;
A250:1<len GoB f by GOBOARD7:34;
A251: 1<=1+j2 by NAT_1:29;
A252:1<=j2+1 by NAT_1:29;
A253:i2<i2+1 by NAT_1:38;
A254: 1<i2+1 by A242,NAT_1:38;
A255:((GoB f)*(i2,j2+1))`1 <((GoB f)*(i2+1,j2+1))`1
by A1,A148,A242,A244,A252,A253,GOBOARD5:4;
then A256:((GoB f)*(i2,j2+1))`1+((GoB f)*(i2,j2+1))`1
<((GoB f)*(i2,j2+1))`1+((GoB f)*(i2+1,j2+1))`1
by REAL_1:67;
A257:((GoB f)*(i2,j2+1))`1+((GoB f)*(i2+1,j2+1))`1
<((GoB f)*(i2+1,j2+1))`1+((GoB f)*(i2+1,j2+1))`1
by A255,REAL_1:67;
(((GoB f)*(i2,j2+1))`1+((GoB f)*(i2,j2+1))`1)/2
<(((GoB f)*(i2,j2+1))`1+((GoB f)*(i2+1,j2+1))`1)/2
by A256,REAL_1:73;
then A258:((GoB f)*(i2,j2+1))`1
<(((GoB f)*(i2,j2+1))`1+((GoB f)*(i2+1,j2+1))`1)/2
by XCMPLX_1:65;
(((GoB f)*(i2,j2+1))`1+((GoB f)*(i2+1,j2+1))`1)/2
<(((GoB f)*(i2+1,j2+1))`1+((GoB f)*(i2+1,j2+1))`1)/2
by A257,REAL_1:73;
then A259:((GoB f)*(i2+1,j2+1))`1
>(((GoB f)*(i2,j2+1))`1+((GoB f)*(i2+1,j2+1))`1)/2
by XCMPLX_1:65;
A260:((GoB f)*(i2,j2+1))`1<p`1 by A248,A258,XCMPLX_1:100;
A261:p`1< ((GoB f)*(i2+1,j2+1))`1 by A248,A259,XCMPLX_1:100;
A262:p in {p} by TARSKI:def 1;
reconsider P={p} as Subset of TOP-REAL 2;
(for x st x in P holds not x in (L~f)) implies
P misses L~f by XBOOLE_0:3;
then A263: {p} c= (L~f)` by A1,A148,A242,A243,A246,NAT_1:29,38,
SUBSET_1:43,TARSKI:def 1;
then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by A262,
JORDAN1:1;
p in {|[s,r]|:(GoB f)*(i2,j2+1)`1<=s & s<=(GoB f)*(i2+1,j2+1)`1}
proof
p=|[p`1,p`2]| by EUCLID:57;
hence thesis by A260,A261;
end;
then A264:p in v_strip(GoB f,i2) by A1,A148,A242,A243,A251,
GOBOARD5:9;
0<=j2 by NAT_1:18;
then A265: j2=0 or j2>=0+1 by NAT_1:38;
now per cases by A1,A148,A265,REAL_1:def 5;
case A266:j2>=1 & j2+1<width GoB f;
then A267:1<=j2 & j2<width GoB f by NAT_1:38;
p in {|[s,r]|:(GoB f)*(1,j2)`2<=r & r<=(GoB f)*(1,j2+1)`2}
proof
A268: j2<j2+1 by NAT_1:38;
A269:((GoB f)*(i2,j2+1))`2=((GoB f)*(1,j2+1))`2
by A1,A148,A242,A252,GOBOARD5:2;
A270:((GoB f)*(i2+1,j2+1))`2=((GoB f)*(1,j2+1))`2
by A1,A148,A244,A252,A254,GOBOARD5:2;
A271:((GoB f)*(1,j2))`2<((GoB f)*(1,j2+1))`2
by A250,A266,A268,GOBOARD5:5;
1/2*(((GoB f)*(i2,j2+1))`2+((GoB f)*(i2+1,j2+1))`2)
=((GoB f)*(1,j2+1))`2 by A269,A270,Lm1;
hence thesis by A249,A271;
end;
then A272:p in h_strip(GoB f,j2) by A250,A267,GOBOARD5:6;
A273:j2+1+1<=width GoB f by A266,NAT_1:38;
p in {|[s,r]|:(GoB f)*(1,j2+1)`2<=r & r<=(GoB f)*(1,j2+1+1)`2}
proof
A274: j2+1<j2+1+1 by NAT_1:38;
A275:((GoB f)*(i2,j2+1))`2=((GoB f)*(1,j2+1))`2
by A1,A148,A242,A252,GOBOARD5:2;
A276:((GoB f)*(i2+1,j2+1))`2=((GoB f)*(1,j2+1))`2
by A1,A148,A244,A252,A254,GOBOARD5:2;
A277:((GoB f)*(1,j2+1))`2<((GoB f)*(1,j2+1+1))`2
by A250,A252,A273,A274,GOBOARD5:5;
1/2*(((GoB f)*(i2,j2+1))`2+((GoB f)*(i2+1,j2+1))`2)
=((GoB f)*(1,j2+1))`2 by A275,A276,Lm1;
hence thesis by A249,A277;
end;
then p in h_strip(GoB f,j2+1) by A250,A251,A266,GOBOARD5:6;
then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A264,A272,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j2+1)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A262,A263,XBOOLE_0:def 3;
case A278:j2>=1 & j2+1=width GoB f;
A279: j2<j2+1 by NAT_1:38;
p in {|[s,r]|:(GoB f)*(1,j2)`2<=r & r<=(GoB f)*(1,j2+1)`2}
proof
A280:((GoB f)*(i2,j2+1))`2=((GoB f)*(1,j2+1))`2
by A1,A148,A242,A252,GOBOARD5:2;
A281:((GoB f)*(i2+1,j2+1))`2=((GoB f)*(1,j2+1))`2
by A1,A148,A244,A252,A254,GOBOARD5:2;
A282:((GoB f)*(1,j2))`2<((GoB f)*(1,j2+1))`2
by A250,A278,A279,GOBOARD5:5;
1/2*(((GoB f)*(i2,j2+1))`2+((GoB f)*(i2+1,j2+1))`2)
=((GoB f)*(1,j2+1))`2 by A280,A281,Lm1;
hence thesis by A249,A282;
end;
then A283:p in h_strip(GoB f,j2) by A250,A278,A279,GOBOARD5:6;
p in {|[s,r]|:(GoB f)*(1,j2+1)`2<=r}
proof
A284:((GoB f)*(i2,j2+1))`2=((GoB f)*(1,j2+1))`2
by A1,A148,A242,A252,GOBOARD5:2;
((GoB f)*(i2+1,j2+1))`2=((GoB f)*(1,j2+1))`2
by A1,A148,A244,A252,A254,GOBOARD5:2;
then 1/2*(((GoB f)*(i2,j2+1))`2+((GoB f)*(i2+1,j2+1))`2)
=((GoB f)*(1,j2+1))`2 by A284,Lm1;
hence thesis by A249;
end;
then p in h_strip(GoB f,j2+1) by A250,A278,GOBOARD5:7;
then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A264,A283,XBOOLE_0
:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j2+1)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A262,A263,XBOOLE_0:def 3;
case A285:j2=0 & j2+1<width GoB f;
p in {|[s,r]|: r<=(GoB f)*(1,1)`2}
proof
A286:((GoB f)*(i2,j2+1))`2=((GoB f)*(1,j2+1))`2
by A1,A148,A242,A252,GOBOARD5:2;
((GoB f)*(i2+1,j2+1))`2=((GoB f)*(1,j2+1))`2
by A1,A148,A244,A252,A254,GOBOARD5:2;
then 1/2*(((GoB f)*(i2,j2+1))`2+((GoB f)*(i2+1,j2+1))`2)
<=((GoB f)*(1,1))`2 by A285,A286,Lm1;
hence thesis by A249;
end;
then A287:p in h_strip(GoB f,j2) by A250,A285,GOBOARD5:8;
A288:j2+1+1<=width GoB f by A285,NAT_1:38;
p in {|[s,r]|:(GoB f)*(1,j2+1)`2<=r & r<=(GoB f)*(1,j2+1+1)`2}
proof
A289: j2+1<j2+1+1 by NAT_1:38;
A290:((GoB f)*(i2,j2+1))`2=((GoB f)*(1,j2+1))`2
by A1,A148,A242,A252,GOBOARD5:2;
A291:((GoB f)*(i2+1,j2+1))`2=((GoB f)*(1,j2+1))`2
by A1,A148,A244,A252,A254,GOBOARD5:2;
A292:((GoB f)*(1,j2+1))`2<((GoB f)*(1,j2+1+1))`2
by A250,A252,A288,A289,GOBOARD5:5;
1/2*(((GoB f)*(i2,j2+1))`2+((GoB f)*(i2+1,j2+1))`2)
=((GoB f)*(1,j2+1))`2 by A290,A291,Lm1;
hence thesis by A249,A292;
end;
then p in h_strip(GoB f,j1) by A148,A250,A285,GOBOARD5:6;
then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) &
p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A148,A264,A287,
XBOOLE_0:def 3
;
then p in cell(GoB f,i2,j2) &
p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
hence p in cell(GoB f,i2,j2+1)/\((L~f)`) &
p in cell(GoB f,i2,j2)/\((L~f)`) by A262,A263,XBOOLE_0:def 3;
case j2=0 & j2+1=width GoB f;
hence contradiction by GOBOARD7:35;
end;
then A293:p in Cl Down(Int cell(GoB f,i2,j1),(L~f)`)
& p in Cl Down(Int cell(GoB f,i2,j2),(L~f)`)
by A1,A148,Th3;
A294:Down(LeftComp f,(L~f)`)=LeftComp f &
Down(RightComp f,(L~f)`)=RightComp f by Th6;
Down(Int cell(GoB f,i2,j1),(L~f)`)
c= LeftComp f \/ RightComp f by A1,A2,Th4;
then Down(Int cell(GoB f,i2,j1),(L~f)`)
c= Down(LeftComp f \/ RightComp f,(L~f)`)
by A294,GOBRD11:4;
then A295:Cl Down(Int cell(GoB f,i2,j1),(L~f)`)
c= Cl Down(LeftComp f \/ RightComp f,(L~f)`)
by PRE_TOPC:49;
A296:Cl Down(Int cell(GoB f,i2,j2),(L~f)`) is connected
by A1,Th4;
Down(LeftComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm4;
then Down(LeftComp f,(L~f)`) is closed by CONNSP_1:35;
then A297:Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`)
by PRE_TOPC:52;
Down(RightComp f,(L~f)`) is_a_component_of (TOP-REAL 2)|((L~f)`)
by Lm5;
then Down(RightComp f,(L~f)`) is closed by CONNSP_1:35;
then A298:Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`)
by PRE_TOPC:52;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
=Down((LeftComp f) \/ (RightComp f),(L~f)`)
by GOBRD11:4;
then A299:Cl Down(LeftComp f \/ RightComp f,(L~f)`)
=Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A297,A298,PRE_TOPC:50;
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
is a_union_of_components of (TOP-REAL 2)|((L~f)`) by Th6;
then A300:skl p1 c= Down(LeftComp f,(L~f)`)
\/ Down(RightComp f,(L~f)`) by A293,A295,A299,CONNSP_3:21;
Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= skl p1
by A293,A296,GOBRD11:1;
then A301: Cl Down(Int cell(GoB f,i2,j2),(L~f)`)
c= Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
by A300,XBOOLE_1:1;
A302:Down(Int cell(GoB f,i2,j2),(L~f)`)
c= Cl Down(Int cell(GoB f,i2,j2),(L~f)`)
by PRE_TOPC:48;
Down(Int cell(GoB f,i2,j2),(L~f)`)=Int cell(GoB f,i2,j2)
by A1,Th4;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f
by A294,A301,A302,XBOOLE_1:1;
end;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f;
end;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f;
end;
hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f;
end;
hence Int cell(GoB f,i1,j1) c= LeftComp f \/ RightComp f
implies Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f;
end;
theorem
Th7: for i1,j1,i2,j2 st i1<=len GoB f & j1<=width GoB f
& i2<=len GoB f & j2<=width GoB f & i1,j1,i2,j2 are_adjacent2
holds Int cell(GoB f,i1,j1) c= LeftComp f \/ RightComp f
iff Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f
proof let i1,j1,i2,j2;assume
A1: i1<=len GoB f & j1<=width GoB f
& i2<=len GoB f & j2<=width GoB f & i1,j1,i2,j2 are_adjacent2;
then A2: i1,i2 are_adjacent1 & j1=j2 or i1=i2 & j1,j2 are_adjacent1
by GOBRD10:def 2;
now per cases by A2,GOBRD10:def 1;
case (i2=i1+1 or i1=i2+1)& j1=j2;
hence thesis by A1,Lm6;
case (i1=i2)&(j2=j1+1 or j1=j2+1);
hence thesis by A1,Lm7;
end;
hence thesis;
end;
theorem
Th8: for F1,F2 being FinSequence of NAT st len F1=len F2 &
(ex i st i in dom F1 & Int cell(GoB f,F1/.i,F2/.i)
c=LeftComp f \/ RightComp f)&
(for i st 1<=i & i<len F1 holds
F1/.i,F2/.i,F1/.(i+1),F2/.(i+1) are_adjacent2)&
(for i,k1,k2 st i in dom F1 & k1=F1.i & k2=F2.i holds
k1<=len GoB f & k2<=width GoB f)
holds (for i st i in dom F1 holds
Int cell(GoB f,F1/.i,F2/.i)c=LeftComp f \/ RightComp f)
proof let F1,F2 be FinSequence of NAT;
assume that A1:len F1=len F2 and
A2:(ex i st i in dom F1 & Int cell(GoB f,F1/.i,F2/.i)
c=LeftComp f \/ RightComp f)and
(for i st 1<=i & i<len F1 holds
F1/.i,F2/.i,F1/.(i+1),F2/.(i+1) are_adjacent2)and
A3:(for i,k1,k2 st i in dom F1 & k1=F1.i & k2=F2.i holds
k1<=len GoB f & k2<=width GoB f);
reconsider F=LeftComp f \/ RightComp f as Subset of REAL 2 by EUCLID:25;
consider i1 such that A4: i1 in dom F1 &
Int cell(GoB f,F1/.i1,F2/.i1)
c=LeftComp f \/ RightComp f by A2;
reconsider kw1=F1/.i1,kw2=F2/.i1 as Nat;
reconsider k1=kw1+1,k2=kw2+1 as Nat;
A5:F1/.i1=F1.i1 by A4,FINSEQ_4:def 4;
dom F1=Seg len F1 by FINSEQ_1:def 3;
then dom F1=dom F2 by A1,FINSEQ_1:def 3;
then A6:F2/.i1=F2.i1 by A4,FINSEQ_4:def 4;
defpred P[Nat,Nat,set] means $3 = Int cell(GoB f,$1-'1,$2-'1);
A7:for i,j st [i,j] in [:Seg ((len (GoB f))+1),
Seg ((width (GoB f))+1):]
for x1,x2 being Element of (bool (REAL 2)) st P[i,j,x1] & P[i,j,x2]
holds x1 = x2;
A8: for i,j st [i,j] in [:Seg ((len (GoB f))+1),
Seg ((width (GoB f))+1):]
ex x being Element of bool (REAL 2) st P[i,j,x] by Lm3;
ex Mm being (Matrix of (len (GoB f))+1, (width (GoB f))+1,(bool (REAL 2)
)) st for i,j st [i,j] in Indices Mm holds P[i,j,Mm*(i,j)]
from MatrixEx(A7,A8);
then consider
Mm being (Matrix of (len (GoB f))+1, (width (GoB f))+1,(bool (REAL 2)))
such that
A9: for i,j st [i,j] in Indices Mm holds
Mm*(i,j) = Int cell(GoB f,i-'1,j-'1);
kw1<=len GoB f & kw2<=width GoB f by A3,A4,A5,A6;
then A10:k1 <=len GoB f +1 & k2<=width GoB f +1 by AXIOMS:24;
0<k1 & 0<k2 by NAT_1:19;
then 0+1<=k1 & 0+1<=k2 by NAT_1:38;
then A11:k1 in Seg (len GoB f +1)&
k2 in Seg (width GoB f +1) by A10,FINSEQ_1:3;
A12:len Mm=len GoB f +1 by MATRIX_1:def 3;
then A13:dom Mm=Seg (len (GoB f) +1) by FINSEQ_1:def 3;
A14:Mm is Matrix of len Mm,width (GoB f) +1,bool (REAL 2) by MATRIX_1:def
3;
A15: 0<len GoB f +1 by NAT_1:19;
A16: 0<len Mm by A12,NAT_1:19;
A17: width (GoB f) +1=width Mm by A12,A15,MATRIX_1:20;
A18: Seg (width (GoB f) +1)=Seg width Mm by A14,A16,MATRIX_1:20;
A19:k1-'1=F1/.i1 & k2-'1=F2/.i1 by BINARITH:39;
[k1,k2] in [:dom Mm,Seg width Mm:] by A11,A13,A18,ZFMISC_1:106;
then [k1,k2] in Indices Mm by MATRIX_1:def 5;
then A20: Mm*(k1,k2) c=LeftComp f \/ RightComp f by A4,A9,A19;
for i1,j1,i2,j2 st i1 in Seg (len GoB f +1) & i2 in Seg (len GoB f +1)
& j1 in Seg (width GoB f +1) & j2 in Seg (width GoB f +1)
& i1,j1,i2,j2 are_adjacent2 holds
Mm*(i1,j1)c=LeftComp f \/ RightComp f
iff Mm*(i2,j2)c=LeftComp f \/ RightComp f
proof let i1,j1,i2,j2;
assume A21:i1 in Seg (len GoB f +1) & i2 in Seg (len GoB f +1)
& j1 in Seg (width GoB f +1) & j2 in Seg (width GoB f +1)
& i1,j1,i2,j2 are_adjacent2;
reconsider ii1=i1-'1,ii2=i2-'1,jj1=j1-'1,jj2=j2-'1 as Nat;
A22:1<=i1 & i1<=len GoB f +1 by A21,FINSEQ_1:3;
A23:1<=i2 & i2<=len GoB f +1 by A21,FINSEQ_1:3;
A24:1<=j1 & j1<=width GoB f +1 by A21,FINSEQ_1:3;
A25:1<=j2 & j2<=width GoB f +1 by A21,FINSEQ_1:3;
0<=i1-1 by A22,SQUARE_1:12;
then i1-'1=i1-1 by BINARITH:def 3;
then i1-'1<=len GoB f +1-1 by A22,REAL_1:49;
then A26: ii1<=len GoB f by XCMPLX_1:26;
0<=i2-1 by A23,SQUARE_1:12;
then i2-'1=i2-1 by BINARITH:def 3;
then i2-'1<=len GoB f +1-1 by A23,REAL_1:49;
then A27: ii2<=len GoB f by XCMPLX_1:26;
0<=j1-1 by A24,SQUARE_1:12;
then j1-'1=j1-1 by BINARITH:def 3;
then j1-'1<=width GoB f +1-1 by A24,REAL_1:49;
then A28: jj1<=width GoB f by XCMPLX_1:26;
0<=j2-1 by A25,SQUARE_1:12;
then j2-'1=j2-1 by BINARITH:def 3;
then j2-'1<=width GoB f +1-1 by A25,REAL_1:49;
then A29: jj2<=width GoB f by XCMPLX_1:26;
A30: ii1,jj1,ii2,jj2 are_adjacent2 by A21,A22,A23,A24,A25,GOBRD10:4;
[i1,j1] in [:dom Mm,Seg width Mm:] by A13,A17,A21,ZFMISC_1:106;
then [i1,j1] in Indices Mm by MATRIX_1:def 5;
then A31:Mm*(i1,j1)=Int cell(GoB f,i1-'1,j1-'1) by A9;
[i2,j2] in [:dom Mm,Seg width Mm:] by A13,A18,A21,ZFMISC_1:106;
then [i2,j2] in Indices Mm by MATRIX_1:def 5;
then Mm*(i2,j2)=Int cell(GoB f,i2-'1,j2-'1) by A9;
hence Mm*(i1,j1)c=LeftComp f \/ RightComp f
iff Mm*(i2,j2)c=LeftComp f \/ RightComp f
by A26,A27,A28,A29,A30,A31,Th7;
end;
then A32:for i,j st i in Seg (len GoB f +1) & j in Seg (width GoB f +1)
holds Mm*(i,j)c=F by A11,A20,GOBRD10:9;
thus for i st i in dom F1 holds
Int cell(GoB f,F1/.i,F2/.i)c=LeftComp f \/ RightComp f
proof let i;assume A33:i in dom F1;
reconsider kx1=F1/.i,kx2=F2/.i as Nat;
reconsider kk1=kx1+1,kk2=kx2+1 as Nat;
A34:F1/.i=F1.i by A33,FINSEQ_4:def 4;
dom F1=Seg len F1 by FINSEQ_1:def 3;
then dom F1=dom F2 by A1,FINSEQ_1:def 3;
then F2/.i=F2.i by A33,FINSEQ_4:def 4;
then kx1<=len GoB f & kx2 <=width GoB f by A3,A33,A34;
then A35:kk1<=len GoB f +1 & kk2 <=width GoB f +1 by AXIOMS:24;
0<kk1 & 0<kk2 by NAT_1:19;
then 0+1<=kk1 & 0+1<=kk2 by NAT_1:38;
then A36:kk1 in Seg (len GoB f +1)&
kk2 in Seg (width GoB f +1) by A35,FINSEQ_1:3;
then A37: Mm*(kk1,kk2)c=LeftComp f \/ RightComp f by A32;
A38:len Mm=len GoB f +1 by MATRIX_1:def 3;
then A39:dom Mm=Seg (len (GoB f) +1) by FINSEQ_1:def 3;
A40:Mm is Matrix of len Mm,width (GoB f) +1,bool (REAL 2) by MATRIX_1:def
3;
0<len Mm by A38,NAT_1:19;
then A41: Seg (width (GoB f) +1)=Seg width Mm by A40,MATRIX_1:20;
A42:kk1-'1=F1/.i & kk2-'1=F2/.i by BINARITH:39;
[kk1,kk2] in [:dom Mm,Seg width Mm:] by A36,A39,A41,ZFMISC_1:106;
then [kk1,kk2] in Indices Mm by MATRIX_1:def 5;
hence Int cell(GoB f,F1/.i,F2/.i)c=LeftComp f \/ RightComp f by A9,A37,A42;
end;
end;
theorem
Th9: ex i,j st i<=len GoB f & j<=width GoB f &
Int cell(GoB f,i,j) c= LeftComp f \/ RightComp f
proof len f>4 by GOBOARD7:36;
then A1:1<=1 & 1+1<=len f by AXIOMS:22;
then consider i,j such that A2:i <= len GoB f & j <= width GoB f
& cell(GoB f,i,j) = left_cell(f,1) by GOBOARD9:14;
A3: Int left_cell(f,1) c= LeftComp f by A1,GOBOARD9:24;
LeftComp f c= LeftComp f \/ RightComp f by XBOOLE_1:7;
then Int cell(GoB f,i,j) c= LeftComp f \/ RightComp f by A2,A3,XBOOLE_1:1;
hence thesis by A2;
end;
theorem
Th10: for i,j st i<=len GoB f & j<=width GoB f holds
Int cell(GoB f,i,j) c= LeftComp f \/ RightComp f
proof let i,j;assume A1:i<=len GoB f & j<=width GoB f;
consider i2,j2 such that A2: i2<=len GoB f & j2<=width GoB f &
Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by Th9;
reconsider n=(len GoB f), m=(width GoB f) as Nat;
consider fs1,fs2 being FinSequence of NAT such that
A3: (for k,k1,k2 st k in dom fs1 & k1=fs1.k & k2=fs2.k
holds k1 <= n & k2 <= m)&
fs1.1=i & fs1.(len fs1)=i2 &
fs2.1=j & fs2.(len fs2)=j2 & len fs1=len fs2 &
len fs1=(i-'i2)+(i2-'i)+(j-'j2)+(j2-'j)+1 &
for k st 1<=k & k<len fs1 holds
fs1/.k,fs2/.k,fs1/.(k+1),fs2/.(k+1) are_adjacent2 by A1,A2,GOBRD10:8;
A4: 1<=1+((i-'i2)+(i2-'i)+(j-'j2)+(j2-'j)) by NAT_1:37;
then A5:len fs1 in dom fs1 by A3,FINSEQ_3:27;
len fs2 in dom fs2 by A3,A4,FINSEQ_3:27;
then A6: i2= fs1/.len fs1 & j2=fs2/.len fs1 by A3,A5,FINSEQ_4:def 4;
1<=1+((i-'i2)+(i2-'i)+(j-'j2)+(j2-'j)) by NAT_1:37;
then A7:1 in dom fs1 & 1 in dom fs2 by A3,FINSEQ_3:27;
then fs1/.1=i & fs2/.1=j by A3,FINSEQ_4:def 4;
hence thesis by A2,A3,A5,A6,A7,Th8;
end;
theorem
(L~f)`=LeftComp f \/ RightComp f
proof
union {Cl Down(Int cell(GoB f,i,j),(L~f)`):
i<=len GoB f & j<=width GoB f} c= LeftComp f \/ RightComp f
proof let x;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
A1: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 A2:y=Cl Down(Int cell(GoB f,i,j),(L~f)`) &
i<=len GoB f & j<=width GoB f by A1;
A3:Int cell(GoB f,i,j)c= LeftComp f \/ RightComp f by A2,Th10;
reconsider P=Int cell(GoB f,i,j) as Subset of TOP-REAL 2;
reconsider Q=(L~f)` as Subset of TOP-REAL 2;
P c=(L~f)` by A2,Th2;
then A4:Cl Down(P,Q) =(Cl (P))/\(Q) by CONNSP_3:30;
A5:Cl (Int cell(GoB f,i,j)) c= Cl (LeftComp f \/ RightComp f)
by A3,PRE_TOPC:49;
Cl (LeftComp f \/ RightComp f)= Cl (LeftComp f) \/ Cl(RightComp f)
by PRE_TOPC:50;
then A6:(Cl (Int cell(GoB f,i,j)))/\((L~f)`)
c= (Cl (LeftComp f) \/ Cl (RightComp f))/\((L~f)`)
by A5,XBOOLE_1:26;
A7:(Cl (LeftComp f) \/ Cl (RightComp f))/\((L~f)`)
= (Cl LeftComp f)/\((L~f)`) \/ (Cl RightComp f)/\((L~f)`) by XBOOLE_1:23;
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
A8: B1 = LeftComp f
& B1 is_a_component_of ((TOP-REAL 2)|(L~f)`) by CONNSP_1:def 6;
Cl B1= (Cl LeftComp f)/\([#]((TOP-REAL 2)|(L~f)`))
by A8,PRE_TOPC:47;
then A9:Cl B1= (Cl LeftComp f)/\((L~f)`) by PRE_TOPC:def 10;
reconsider B1 as Subset of (TOP-REAL 2)|(L~f)`;
B1 is closed by A8,CONNSP_1:35;
then A10:(Cl LeftComp f)/\((L~f)`)=LeftComp f by A8,A9,PRE_TOPC:52;
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
A11: B2 = RightComp f
& B2 is_a_component_of ((TOP-REAL 2)|(L~f)`) by CONNSP_1:def 6;
Cl B2= (Cl RightComp f)/\([#]((TOP-REAL 2)|(L~f)`))
by A11,PRE_TOPC:47;
then A12:Cl B2= (Cl RightComp f)/\((L~f)`) by PRE_TOPC:def 10;
reconsider B2 as Subset of (TOP-REAL 2)|(L~f)`;
B2 is closed by A11,CONNSP_1:35;
then (Cl RightComp f)/\((L~f)`)=RightComp f by A11,A12,PRE_TOPC:52;
hence x in (LeftComp f) \/ (RightComp f) by A1,A2,A4,A6,A7,A10;
end;
then A13:(L~f)`c=LeftComp f \/ RightComp f by Th5;
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
A14: B1 = LeftComp f & B1 is_a_component_of (TOP-REAL 2)|(L~f)`
by CONNSP_1:def 6;
B1 c= the carrier of (TOP-REAL 2)|(L~f)`;
then A15:LeftComp f c= (L~f)` by A14,Lm2;
RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
then consider B1 being Subset of (TOP-REAL 2)|(L~f)` such that
A16: B1 = RightComp f & B1 is_a_component_of (TOP-REAL 2)|(L~f)`
by CONNSP_1:def 6;
B1 c= the carrier of (TOP-REAL 2)|(L~f)`;
then B1 c= (L~f)` by Lm2;
then LeftComp f \/ RightComp f c= (L~f)` by A15,A16,XBOOLE_1:8;
hence thesis by A13,XBOOLE_0:def 10;
end;