:: The First Part of Jordan's Theorem for Special Polygons
::  by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received July 22, 1996
:: Copyright (c) 1996-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, REAL_1, FUNCT_1, GOBOARD5, TOPREAL1, STRUCT_0,
      EUCLID, RELAT_1, XXREAL_0, FINSEQ_1, GOBOARD2, TREES_1, TOPS_1, TARSKI,
      XBOOLE_0, PRE_TOPC, CONNSP_3, RELAT_2, GOBOARD9, CONNSP_1, ARYTM_3,
      CARD_1, RLTOPSP1, PARTFUN1, MATRIX_1, ZFMISC_1, MCART_1, ARYTM_1,
      RCOMP_1, NAT_1, CONVEX1, CHORD;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, TOPREAL1, ORDINAL1, NUMBERS,
      DOMAIN_1, XCMPLX_0, XREAL_0, STRUCT_0, REAL_1, NAT_1, NAT_D, PRE_TOPC,
      FUNCT_1, PARTFUN1, FINSEQ_1, MATRIX_0, TOPS_1, CONNSP_1, RLVECT_1,
      RLTOPSP1, EUCLID, GOBOARD2, GOBOARD5, GOBOARD9, CONNSP_3, GOBRD10,
      XXREAL_0;
 constructors DOMAIN_1, REAL_1, TOPS_1, CONNSP_1, GOBOARD2, GOBOARD9, CONNSP_3,
      GOBRD10, GOBOARD1, NAT_D, RELSET_1, CONVEX1;
 registrations SUBSET_1, RELSET_1, XXREAL_0, NAT_1, STRUCT_0, PRE_TOPC, EUCLID,
      GOBOARD2, GOBOARD5, GOBRD11, JORDAN1, XREAL_0, ORDINAL1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions TARSKI;
 equalities CONNSP_3, STRUCT_0;
 expansions TARSKI;
 theorems TARSKI, NAT_1, FINSEQ_1, SPPOL_1, GOBOARD7, GOBOARD8, GOBOARD9,
      PRE_TOPC, CONNSP_1, SUBSET_1, EUCLID, CONNSP_3, TOPREAL1, GOBOARD5,
      TOPREAL3, MATRIX_0, GOBRD10, GOBRD11, ZFMISC_1, XBOOLE_0, XBOOLE_1,
      FINSEQ_3, XREAL_1, XXREAL_0, PARTFUN1, XREAL_0, NAT_D, ORDINAL1;
 schemes MATRIX_0;

begin

reserve i,j,k,k1,k2,i1,i2,j1,j2 for Nat,
  r,s for Real,
  x for set,
  f for non constant standard special_circular_sequence;

Lm1: (L~f)` = the carrier of ((TOP-REAL 2)|(L~f)`)
proof
  (L~f)`=[#]((TOP-REAL 2)|(L~f)`) by PRE_TOPC:def 5
    .=the carrier of ((TOP-REAL 2)|(L~f)`);
  hence thesis;
end;

Lm2: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:22;

theorem Th1:
  for i,j st i<=len GoB f & j<=width GoB f holds Int cell(GoB f,i,j )c=(L~f)`
    by GOBOARD7:12,SUBSET_1:23;

theorem Th2:
  for i,j st i<=len GoB f & j<=width GoB f holds Cl Down(Int cell(
  GoB f,i,j),(L~f)`)=cell(GoB f,i,j)/\((L~f)`)
proof
  let i,j;
  reconsider V=Int cell(GoB f,i,j) as Subset of TOP-REAL 2;
  reconsider B=(L~f)` as Subset of TOP-REAL 2;
  assume
A1: i<=len GoB f & j<=width GoB f;
  then Cl Down(V,B) =(Cl V) /\ B by Th1,CONNSP_3:29;
  hence thesis by A1,GOBRD11:35;
end;

theorem Th3:
  for i,j st i<=len GoB f & j<=width GoB f holds Cl Down(Int cell(
GoB f,i,j),(L~f)`) is connected & Down(Int cell(GoB f,i,j),(L~f)`)=Int cell(GoB
  f,i,j)
proof
  let i,j;
  assume
A1: i<=len GoB f & j<=width GoB f;
  then
  Int cell(GoB f,i,j) is convex & Down(Int cell(GoB f,i,j),(L~f)`)=Int
  cell (GoB f,i,j) by Th1,GOBOARD9:17,XBOOLE_1:28;
  then Down(Int cell(GoB f,i,j),(L~f)`) is connected by CONNSP_1:23;
  hence Cl Down(Int cell(GoB f,i,j),(L~f)`) is connected by CONNSP_1:19;
  thus thesis by A1,Th1,XBOOLE_1:28;
end;

Lm3: Cl Down(LeftComp f,(L~f)`) is connected & Down(LeftComp f,(L~f)`)=
LeftComp f & Down(LeftComp f,(L~f)`) is a_component
proof
  LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
  then
A1: ex B1 being Subset of (TOP-REAL 2)|((L~f)`) st B1 = LeftComp f & B1
  is a_component by CONNSP_1:def 6;
A2: the carrier of (TOP-REAL 2)|((L~f)`) =(L~f)` by PRE_TOPC:8;
  then Down(LeftComp f,(L~f)`)=LeftComp f by A1,XBOOLE_1:28;
  then Down(LeftComp f,(L~f)`) is connected by A1,CONNSP_1:def 5;
  hence Cl Down(LeftComp f,(L~f)`) is connected by CONNSP_1:19;
  thus thesis by A1,A2,XBOOLE_1:28;
end;

Lm4: Cl Down(RightComp f,(L~f)`) is connected & Down(RightComp f,(L~f)`)=
RightComp f & Down(RightComp f,(L~f)`) is a_component
proof
  RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
  then
A1: ex B1 being Subset of (TOP-REAL 2)|((L~f)`) st B1 = RightComp f & B1
  is a_component by CONNSP_1:def 6;
A2: the carrier of (TOP-REAL 2)|((L~f)`) =(L~f)` by PRE_TOPC:8;
  then Down(RightComp f,(L~f)`)=RightComp f by A1,XBOOLE_1:28;
  then Down(RightComp f,(L~f)`) is connected by A1,CONNSP_1:def 5;
  hence Cl Down(RightComp f,(L~f)`) is connected by CONNSP_1:19;
  thus thesis by A1,A2,XBOOLE_1:28;
end;

theorem Th4:
  (L~f)`=union {Cl Down(Int cell(GoB f,i,j),(L~f)`): i<=len GoB f &
  j<=width GoB f}
proof
A1: (the carrier of TOP-REAL 2) =union {cell(GoB f,i,j):i<=(len GoB f) & j<=
  (width GoB f)} by GOBRD11:7;
A2: (L~f)`c= union {Cl Down(Int cell(GoB f,i,j),(L~f)`): i<=len GoB f & j<=
  width GoB f}
  proof
    let x be object;
    assume
A3: x in (L~f)`;
    then consider Y being set such that
A4: x in Y & Y in {cell(GoB f,i,j):i<=len GoB f & j<=width GoB f} by A1,
TARSKI:def 4;
    consider i,j such that
A5: Y=cell(GoB f,i,j) and
A6: i<=len GoB f & j<=width GoB f by A4;
    reconsider Y0=Cl Down(Int cell(GoB f,i,j),(L~f)`) as set;
    x in cell(GoB f,i,j)/\((L~f)`) by A3,A4,A5,XBOOLE_0:def 4;
    then
A7: x in Y0 by A6,Th2;
    Y0 in {Cl Down(Int cell(GoB f,i1,j1),(L~f)`): i1<=len GoB f & j1<=
    width GoB f} by A6;
    hence thesis by A7,TARSKI:def 4;
  end;
  union {Cl Down(Int cell(GoB f,i,j),(L~f)`): i<=len GoB f & j<=width GoB
  f} c= (L~f)`
  proof
    let x be object;
    assume x in union {Cl Down(Int cell(GoB f,i,j),(L~f)`): i<=len GoB f & j
    <=width GoB f};
    then consider Y being set such that
A8: x in Y & Y in {Cl Down(Int cell(GoB f,i,j),(L~f)`): i<=len GoB f
    & j<=width GoB f} by TARSKI:def 4;
    consider i,j such that
A9: Y= Cl Down(Int cell(GoB f,i,j),(L~f)`) and
    i<=len GoB f and
    j<=width GoB f by A8;
    Cl Down(Int cell(GoB f,i,j),(L~f)`) c= the carrier of (TOP-REAL 2)|( L~f)`;
    then Y c= (L~f)` by A9,Lm1;
    hence thesis by A8;
  end;
  hence thesis by A2,XBOOLE_0:def 10;
end;

theorem Th5:
  Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`) is
  a_union_of_components of (TOP-REAL 2)|((L~f)`) & Down(LeftComp f,(L~f)`)=
  LeftComp f & Down(RightComp f,(L~f)`)=RightComp f
proof
  LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
  then consider B1 being Subset of (TOP-REAL 2)|((L~f)`) such that
A1: B1 = LeftComp f and
A2: B1 is a_component by CONNSP_1:def 6;
  RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
  then consider B2 being Subset of (TOP-REAL 2)|((L~f)`) such that
A3: B2 = RightComp f and
A4: B2 is a_component by CONNSP_1:def 6;
A5: B2 is Subset of (L~f)` by Lm1;
  then
A6: Down(RightComp f,(L~f)`) is a_component by A3,A4,XBOOLE_1:28;
A7: B1 is Subset of (L~f)` by Lm1;
  then
  Down(LeftComp f,(L~f)`) is a_component by A1,A2,XBOOLE_1:28;
  hence thesis by A1,A7,A3,A5,A6,GOBRD11:3,XBOOLE_1:28;
end;

Lm5: for i1,j1,i2,j2 st i1<=len GoB f & j1<=width GoB f & i2<=len GoB f & j2<=
width GoB f & (i2=i1+1 or i1=i2+1)& j1=j2 holds Int cell(GoB f,i1,j1) c=
LeftComp f \/ RightComp f implies Int cell(GoB f,i2,j2) c= LeftComp f \/
RightComp f
proof
  let i1,j1,i2,j2;
  assume that
A1: i1<=len GoB f and
A2: j1<=width GoB f and
A3: i2<=len GoB f and
A4: j2<=width GoB f and
A5: i2=i1+1 or i1=i2+1 and
A6: j1=j2;
  now
    assume
A7: Int cell(GoB f,i1,j1) c= LeftComp f \/ RightComp f;
    now
      per cases by A5;
      case
A8:     i2=i1+1;
        now
          per cases;
          case
            ex k st 1<=k & k+1 <=len f & j2<>0 & j2<>width GoB f &
            LSeg(f/.k,f/.(k+1))=LSeg((GoB f)*(i1+1,j2),(GoB f)*(i1+1,j2+1));
            then consider k such that
A9:         1<=k & k+1 <=len f and
A10:        j2<>0 and
A11:        j2<>width GoB f and
A12:        LSeg(f/.k,f/.(k+1))=LSeg((GoB f)*(i1+1,j2),(GoB f)*(i1+1, j2+1));
            now
              per cases by A12,SPPOL_1:8;
              case
A13:            f/.k=(GoB f)*(i1+1,j2)& f/.(k+1)= (GoB f)*(i1+1,j2+1);
A14:            Int right_cell(f,k) c= RightComp f & RightComp f c=
                LeftComp f \/ RightComp f by A9,GOBOARD9:25,XBOOLE_1:7;
                j2<width GoB f by A4,A11,XXREAL_0:1;
                then
A15:            j2+1<=width GoB f by NAT_1:13;
                0+1<=i1+1 by XREAL_1:6;
                then
A16:            Indices GoB f=[:dom GoB f,Seg width GoB f:] & i1+1 in dom
                GoB f by A3,A8,FINSEQ_3:25,MATRIX_0:def 4;
                1<=j2+1 by NAT_1:11;
                then j2+1 in Seg width GoB f by A15,FINSEQ_1:1;
                then
A17:            [i1+1,j2+1] in Indices GoB f by A16,ZFMISC_1:87;
                j2>=0+1 by A10,NAT_1:13;
                then j2 in Seg width GoB f by A4,FINSEQ_1:1;
                then [i1+1,j2] in Indices GoB f by A16,ZFMISC_1:87;
                then right_cell(f,k) = cell(GoB f,i1+1,j2) by A9,A13,A17,
GOBOARD5:27;
                hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f by
A14;
              end;
              case
A18:            f/.k=(GoB f)*(i1+1,j2+1)& f/.(k+1)=(GoB f)*(i1+1,j2);
A19:            Int left_cell(f,k) c= LeftComp f & LeftComp f c= LeftComp
                f \/ RightComp f by A9,GOBOARD9:21,XBOOLE_1:7;
                j2<width GoB f by A4,A11,XXREAL_0:1;
                then
A20:            j2+1<=width GoB f by NAT_1:13;
                0+1<=i1+1 by XREAL_1:6;
                then
A21:            Indices GoB f=[:dom GoB f,Seg width GoB f:] & i1+1 in dom
                GoB f by A3,A8,FINSEQ_3:25,MATRIX_0:def 4;
                1<=j2+1 by NAT_1:11;
                then j2+1 in Seg width GoB f by A20,FINSEQ_1:1;
                then
A22:            [i1+1,j2+1] in Indices GoB f by A21,ZFMISC_1:87;
                j2>=0+1 by A10,NAT_1:13;
                then j2 in Seg width GoB f by A4,FINSEQ_1:1;
                then [i1+1,j2] in Indices GoB f by A21,ZFMISC_1:87;
                then left_cell(f,k) = cell(GoB f,i1+1,j2) by A9,A18,A22,
GOBOARD5:30;
                hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f by
A19;
              end;
            end;
            hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f;
          end;
          case
A23:        not ex k st 1<=k & k+1 <=len f & j2<>0 & j2<>width GoB f
            & LSeg(f/.k,f/.(k+1))=LSeg((GoB f)*(i1+1,j2),(GoB f)*(i1+1,j2+1));
            now
              per cases by A23;
              case
A24:            j2=0;
                reconsider p=|[((GoB f)*(i1+1,1))`1,((GoB f)*(i1+1,1))`2-1]|
                as Point of TOP-REAL 2;
A25:            1<width GoB f by GOBOARD7:33;
A26:            1<len GoB f by GOBOARD7:32;
                reconsider P={p} as Subset of TOP-REAL 2;
A27:            p`2<p`2+1 by XREAL_1:29;
A28:            1<=i1+1 by NAT_1:11;
                then ((GoB f)*(i1+1,1))`2=((GoB f)*(1,1))`2 by A3,A8,A25,
GOBOARD5:1;
                then
A29:            p`2=((GoB f)*(1,1))`2-1 by EUCLID:52;
                p in {|[r,s]|:s<=(GoB f)*(1,1)`2}
                proof
                  p=|[p`1,p`2]| by EUCLID:53;
                  hence thesis by A29,A27;
                end;
                then
A30:            p in h_strip(GoB f,j2) by A24,A26,GOBOARD5:7;
                (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
A31:            p in {p} & {p} c= (L~f)` by A29,A27,SUBSET_1:23,TARSKI:def 1;
                then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by
PRE_TOPC:8;
A32:            i1=0 or i1>=0+1 by NAT_1:13;
A33:            now
                  per cases by A3,A8,A32,XXREAL_0:1;
                  case
A34:                i1>=1 & i1+1<len GoB f;
                    then
A35:                i1+1+1<=len GoB f by NAT_1:13;
A36:                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:13;
                      then ((GoB f)*(i1+1,1))`1<=(GoB f)*(i1+1+1,1)`1 by A25
,A28,A35,GOBOARD5:3;
                      hence thesis;
                    end;
                    1<=i1+1 by NAT_1:11;
                    then p in v_strip(GoB f,i1+1) by A25,A34,A36,GOBOARD5:8;
                    then p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A30,
XBOOLE_0:def 4;
                    then
A37:                p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
A38:                p in {|[r,s]|:(GoB f)*(i1,1)`1<=r & r<=(GoB f)*(i1+1, 1)`1}
                    proof
                      i1<i1+1 by NAT_1:13;
                      then ((GoB f)*(i1,1))`1<((GoB f)*(i1+1,1))`1 by A25,A34,
GOBOARD5:3;
                      hence thesis;
                    end;
                    i1<len GoB f by A34,NAT_1:13;
                    then p in v_strip(GoB f,i1) by A25,A34,A38,GOBOARD5:8;
                    then
p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) by A30,XBOOLE_0:def 4;
                    then p in cell(GoB f,i1,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 A31,A37,XBOOLE_0:def 4;
                  end;
                  case
A39:                i1>=1 & i1+1=len GoB f;
A40:                i1<i1+1 by NAT_1:13;
A41:                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 A25,A39,A40,
GOBOARD5:3;
                      hence thesis;
                    end;
                    p in {|[r,s]|:(GoB f)*(i1+1,1)`1<=r};
                    then p in v_strip(GoB f,i1+1) by A25,A39,GOBOARD5:9;
                    then p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A30,
XBOOLE_0:def 4;
                    then
A42:                p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
                    i1<len GoB f by A39,NAT_1:13;
                    then p in v_strip(GoB f,i1) by A25,A39,A41,GOBOARD5:8;
                    then
p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) by A30,XBOOLE_0:def 4;
                    then p in cell(GoB f,i1,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 A31,A42,XBOOLE_0:def 4;
                  end;
                  case
A43:                i1=0 & i1+1<len GoB f;
                    then
A44:                i1+1+1<=len GoB f by NAT_1:13;
                    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:13;
                      then ((GoB f)*(i1+1,1))`1<=(GoB f)*(i1+1+1,1)`1 by A25
,A28,A44,GOBOARD5:3;
                      hence thesis;
                    end;
                    then p in v_strip(GoB f,i1+1) by A25,A43,GOBOARD5:8;
                    then p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A30,
XBOOLE_0:def 4;
                    then
A45:                p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
                    p in {|[r,s]|: r<=(GoB f)*(1,1)`1} by A43;
                    then p in v_strip(GoB f,i1) by A25,A43,GOBOARD5:10;
                    then
p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) by A30,XBOOLE_0:def 4;
                    then p in cell(GoB f,i1,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 A31,A45,XBOOLE_0:def 4;
                  end;
                  case
A46:                i1=0 & i1+1=len GoB f;
                    p in {|[r,s]|:(GoB f)*(i1+1,1)`1<=r};
                    then p in v_strip(GoB f,i1+1) by A25,A46,GOBOARD5:9;
                    then p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A30,
XBOOLE_0:def 4;
                    then
A47:                p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
                    p in {|[r,s]|: r<=(GoB f)*(1,1)`1} by A46;
                    then p in v_strip(GoB f,i1) by A25,A46,GOBOARD5:10;
                    then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) by A30,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i1,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 A31,A47,XBOOLE_0:def 4;
                  end;
                end;
                then p in Cl Down(Int cell(GoB f,i1+1,j2),(L~f) `) by A4,Th2;
                then
A48:            Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`) c= Component_of
                p1 by A3,A4,A8,Th3,GOBRD11:1;
                Down(RightComp f,(L~f)`) is closed by Lm4,CONNSP_1:33;
                then
A49:            Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) is closed by Lm3,CONNSP_1:33;
                then
A50:            Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`) =
                Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
                then
A51:            Cl Down(LeftComp f \/ RightComp f,(L~f)`) =Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A50,A49,PRE_TOPC:20;
A52:            Down(Int cell(GoB f,i1+1,j2),(L~f)`) c= Cl Down(Int cell
(GoB f,i1+1,j2),(L~f) `) & Down(Int cell(GoB f,i1+1,j2),(L~f)`)=Int cell(GoB f,
                i1+1,j2) by A3,A4,A8,Th3,PRE_TOPC:18;
A53:            Down(LeftComp f,(L~f)`)=LeftComp f & Down(RightComp f,(
                L~f)`)=RightComp f by Th5;
                Down(Int cell(GoB f,i1,j2),(L~f)`) c= LeftComp f \/
                RightComp f by A1,A2,A6,A7,Th3;
                then Down(Int cell(GoB f,i1,j2),(L~f)`) c= Down(LeftComp f \/
                RightComp f,(L~f)`) by A53,GOBRD11:4;
                then
A54:            Cl Down(Int cell(GoB f,i1,j2),(L~f)`) c= Cl Down(
                LeftComp f \/ RightComp f,(L~f)`) by PRE_TOPC:19;
                p in Cl Down(Int cell(GoB f,i1,j2),(L~f)`) by A1,A4,A33,Th2;
                then Component_of p1 c= Down(LeftComp f,(L~f)`) \/ Down(
                RightComp f,(L~f)`) by A54,A51,Th5,CONNSP_3:21;
                then Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`) c= Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A48;
                hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f by
A53,A52;
              end;
              case
A55:            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;
A56:            1<width GoB f by GOBOARD7:33;
                reconsider P={p} as Subset of TOP-REAL 2;
A57:            (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;
A58:            1<len GoB f by GOBOARD7:32;
A59:            1<=1+i1 by NAT_1:11;
                then ((GoB f)*(i1+1,width GoB f))`2 =((GoB f)*(1,width GoB f)
                )`2 by A3,A8,A56,GOBOARD5:1;
                then
A60:            p`2=((GoB f)*(1,width GoB f))`2+1 by EUCLID:52;
                then
A61:            ((GoB f)*(1,width GoB f))`2<p`2 by XREAL_1:29;
                p in {|[r,s]|:(GoB f)*(1,width (GoB f))`2<=s}
                proof
                  p=|[p`1,p`2]| by EUCLID:53;
                  hence thesis by A61;
                end;
                then
A62:            p in h_strip(GoB f,j2) by A55,A58,GOBOARD5:6;
                ((GoB f)*(1,width GoB f))`2<((GoB f)*(1,width GoB f))`2+
                1 by XREAL_1:29;
                then
A63:            p in {p} & {p} c= (L~f)` by A60,A57,SUBSET_1:23,TARSKI:def 1;
                then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by
PRE_TOPC:8;
A64:            i1=0 or i1>=0+1 by NAT_1:13;
A65:            now
                  per cases by A3,A8,A64,XXREAL_0:1;
                  case
A66:                i1>=1 & i1+1<len GoB f;
                    then
A67:                i1+1+1<=len GoB f by NAT_1:13;
A68:                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:13;
                      then ((GoB f)*(i1+1,width GoB f))`1 <=(GoB f)*(i1+1+1,
                      width GoB f)`1 by A56,A59,A67,GOBOARD5:3;
                      hence thesis;
                    end;
                    1<=i1+1 by NAT_1:11;
                    then p in v_strip(GoB f,i1+1) by A56,A66,A68,GOBOARD5:8;
                    then p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A62,
XBOOLE_0:def 4;
                    then
A69:                p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
A70:                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:13;
                      then ((GoB f)*(i1,width GoB f))`1 <((GoB f)*(i1+1,width
                      GoB f))`1 by A56,A66,GOBOARD5:3;
                      hence thesis;
                    end;
                    i1<len GoB f by A66,NAT_1:13;
                    then p in v_strip(GoB f,i1) by A56,A66,A70,GOBOARD5:8;
                    then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) by A62,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i1,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 A63,A69,XBOOLE_0:def 4;
                  end;
                  case
A71:                i1>=1 & i1+1=len GoB f;
A72:                i1<i1+1 by NAT_1:13;
A73:                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 A56,A71,A72,GOBOARD5:3;
                      hence thesis;
                    end;
                    p in {|[r,s]|:(GoB f)*(i1+1,width (GoB f))`1<=r};
                    then p in v_strip(GoB f,i1+1) by A56,A71,GOBOARD5:9;
                    then p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A62,
XBOOLE_0:def 4;
                    then
A74:                p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
                    i1<len GoB f by A71,NAT_1:13;
                    then p in v_strip(GoB f,i1) by A56,A71,A73,GOBOARD5:8;
                    then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) by A62,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i1,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 A63,A74,XBOOLE_0:def 4;
                  end;
                  case
A75:                i1=0 & i1+1<len GoB f;
                    then
A76:                i1+1+1<=len GoB f by NAT_1:13;
                    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:13;
                      then ((GoB f)*(i1+1,width (GoB f)))`1 <=(GoB f)*(i1+1+1
                      ,width (GoB f))`1 by A56,A59,A76,GOBOARD5:3;
                      hence thesis;
                    end;
                    then p in v_strip(GoB f,i1+1) by A56,A75,GOBOARD5:8;
                    then p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A62,
XBOOLE_0:def 4;
                    then
A77:                p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
                    p in {|[r,s]|: r<=(GoB f)*(1,width (GoB f))`1} by A75;
                    then p in v_strip(GoB f,i1) by A56,A75,GOBOARD5:10;
                    then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) by A62,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i1,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 A63,A77,XBOOLE_0:def 4;
                  end;
                  case
                    i1=0 & i1+1=len GoB f;
                    hence contradiction by GOBOARD7:32;
                  end;
                end;
                then p in Cl Down(Int cell(GoB f,i1+1,j2),(L~f) `) by A4,Th2;
                then
A78:            Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`) c= Component_of
                p1 by A3,A4,A8,Th3,GOBRD11:1;
                Down(RightComp f,(L~f)`) is closed by Lm4,CONNSP_1:33;
                then
A79:            Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) is closed by Lm3,CONNSP_1:33;
                then
A80:            Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`) =
                Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
                then
A81:            Cl Down(LeftComp f \/ RightComp f,(L~f)`) =Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A80,A79,PRE_TOPC:20;
A82:            Down(Int cell(GoB f,i1+1,j2),(L~f)`) c= Cl Down(Int cell
(GoB f,i1+1,j2),(L~f) `) & Down(Int cell(GoB f,i1+1,j2),(L~f)`)=Int cell(GoB f,
                i1+1,j2) by A3,A4,A8,Th3,PRE_TOPC:18;
A83:            Down(LeftComp f,(L~f)`)=LeftComp f & Down(RightComp f,(
                L~f)`)=RightComp f by Th5;
                Down(Int cell(GoB f,i1,j2),(L~f)`) c= LeftComp f \/
                RightComp f by A1,A2,A6,A7,Th3;
                then Down(Int cell(GoB f,i1,j2),(L~f)`) c= Down(LeftComp f \/
                RightComp f,(L~f)`) by A83,GOBRD11:4;
                then
A84:            Cl Down(Int cell(GoB f,i1,j2),(L~f)`) c= Cl Down(
                LeftComp f \/ RightComp f,(L~f)`) by PRE_TOPC:19;
                p in Cl Down(Int cell(GoB f,i1,j2),(L~f)`) by A1,A4,A65,Th2;
                then Component_of p1 c= Down(LeftComp f,(L~f)`) \/ Down(
                RightComp f,(L~f)`) by A84,A81,Th5,CONNSP_3:21;
                then Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`) c= Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A78;
                hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f by
A83,A82;
              end;
              case
A85:            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
A86:            j2<width GoB f by A4,XXREAL_0:1;
                then
A87:            j2+1<=width GoB f by NAT_1:13;
                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
A88:              1<=k & k+1<=len f;
                  then LSeg(f,k)=LSeg(f/.k,f/.(k+1)) by TOPREAL1:def 3;
                  hence thesis by A85,A88;
                end;
                then
A89:            1 <= i1+1 & i1+1 <= len GoB f & 1 <= j2 & j2+1 <= width
GoB f implies not 1/2*((GoB f)*(i1+1,j2)+(GoB f)*(i1+1,j2+1)) in L~f by
GOBOARD7:39;
                reconsider p=1/2*((GoB f)*(i1+1,j2)+(GoB f)*(i1+1,j2+1)) as
                Point of TOP-REAL 2;
A90:            p`2=1/2*((GoB f)*(i1+1,j2)+(GoB f)*(i1+1,j2+1))`2 by TOPREAL3:4
                  .=1/2*(((GoB f)*(i1+1,j2))`2+((GoB f)*(i1+1,j2+1))`2) by
TOPREAL3:2;
                reconsider P={p} as Subset of TOP-REAL 2;
A91:            1<width GoB f by GOBOARD7:33;
                Down(RightComp f,(L~f)`) is closed by Lm4,CONNSP_1:33;
                then
A92:            Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) is closed by Lm3,CONNSP_1:33;
                then
A93:            Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`) =
                Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
                then
A94:            Cl Down(LeftComp f \/ RightComp f,(L~f)`) =Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A93,A92,PRE_TOPC:20;
A95:            Down(LeftComp f,(L~f)`)=LeftComp f & Down(RightComp f,(
                L~f)`)=RightComp f by Th5;
                Down(Int cell(GoB f,i1,j2),(L~f)`) c= LeftComp f \/
                RightComp f by A1,A2,A6,A7,Th3;
                then Down(Int cell(GoB f,i1,j2),(L~f)`) c= Down(LeftComp f \/
                RightComp f,(L~f)`) by A95,GOBRD11:4;
                then
A96:            Cl Down(Int cell(GoB f,i1,j2),(L~f)`) c= Cl Down(
                LeftComp f \/ RightComp f,(L~f)`) by PRE_TOPC:19;
A97:            Down(Int cell(GoB f,i1+1,j2),(L~f)`) c= Cl Down(Int cell
(GoB f,i1+1,j2),(L~f) `) & Down(Int cell(GoB f,i1+1,j2),(L~f)`)=Int cell(GoB f,
                i1+1,j2) by A3,A4,A8,Th3,PRE_TOPC:18;
A98:            1<=i1+1 by NAT_1:11;
A99:            0+1<=j2 by A85,NAT_1:13;
                then
A100:           1<j2+1 by NAT_1:13;
                (for x being object st x in P holds not x in (L~f))
implies P misses
                L~f by XBOOLE_0:3;
                then
A101:           p in {p} & {p} c= (L~f)` by A3,A8,A99,A86,A89,NAT_1:13
,SUBSET_1:23,TARSKI:def 1;
                then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by
PRE_TOPC:8;
A102:           1<=1+i1 by NAT_1:11;
                p`1=1/2*((GoB f)*(i1+1,j2)+(GoB f)*(i1+1,j2+1))`1 by TOPREAL3:4
                  .=1/2*(((GoB f)*(i1+1,j2))`1+((GoB f)*(i1+1,j2+1))`1) by
TOPREAL3:2;
                then
A103:           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 A90,EUCLID:53;
                j2<j2+1 by NAT_1:13;
                then
A104:           ((GoB f)*(i1+1,j2))`2 <((GoB f)*(i1+1,j2+1))`2 by A3,A8,A99,A87
,A102,GOBOARD5:4;
                then ((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 XREAL_1:8;
                then
A105:           (((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 XREAL_1:74;
                ((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 A104,XREAL_1:8;
                then
A106:           (((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 XREAL_1:74;
                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:53;
                  hence thesis by A90,A106,A105;
                end;
                then
A107:           p in h_strip(GoB f,j2) by A3,A8,A99,A86,A98,GOBOARD5:5;
A108:           i1=0 or i1>=0+1 by NAT_1:13;
A109:           now
                  per cases by A3,A8,A108,XXREAL_0:1;
                  case
A110:               i1>=1 & i1+1<len GoB f;
                    then
A111:               i1+1+1<=len GoB f by NAT_1:13;
A112:               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:13;
                      then
A113:                 ((GoB f)*(i1+1,1))`1<((GoB f)*(i1+1+1,1))`1 by A91,A102
,A111,GOBOARD5:3;
                      ((GoB f)*(i1+1,j2))`1=((GoB f)*(i1+1,1))`1 & ((GoB
f)*(i1+1,j2+1))`1=((GoB f )*(i1+1,1))`1 by A3,A4,A8,A99,A87,A102,A100,
GOBOARD5:2;
                      hence thesis by A103,A113;
                    end;
                    1<=i1+1 by NAT_1:11;
                    then p in v_strip(GoB f,i1+1) by A91,A110,A112,GOBOARD5:8;
                    then p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A107,
XBOOLE_0:def 4;
                    then
A114:               p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
A115:               p in {|[r,s]|:(GoB f)*(i1,1)`1<=r & r<=(GoB f)*(i1+1 ,1)`1}
                    proof
                      i1<i1+1 by NAT_1:13;
                      then
A116:                 ((GoB f)*(i1,1))`1<((GoB f)*(i1+1,1))`1 by A91,A110,
GOBOARD5:3;
                      ((GoB f)*(i1+1,j2))`1=((GoB f)*(i1+1,1))`1 & ((GoB
f)*(i1+1,j2+1))`1=((GoB f )*(i1+1,1))`1 by A3,A4,A8,A99,A87,A102,A100,
GOBOARD5:2;
                      hence thesis by A103,A116;
                    end;
                    i1<len GoB f by A110,NAT_1:13;
                    then p in v_strip(GoB f,i1) by A91,A110,A115,GOBOARD5:8;
                    then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) by A107,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i1,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 A101,A114,XBOOLE_0:def 4;
                  end;
                  case
A117:               i1>=1 & i1+1=len GoB f;
A118:               i1<i1+1 by NAT_1:13;
                    p in {|[r,s]|:(GoB f)*(i1,1)`1<=r & r<=(GoB f)*(i1+1 ,1)`1}
                    proof
A119:                 ((GoB f)*(i1,1))`1<((GoB f)*(i1+1,1))`1 by A91,A117,A118,
GOBOARD5:3;
                      ((GoB f)*(i1+1,j2))`1=((GoB f)*(i1+1,1))`1 & ((GoB
f)*(i1+1,j2+1))`1=((GoB f )*(i1+1,1))`1 by A3,A4,A8,A99,A87,A102,A100,
GOBOARD5:2;
                      hence thesis by A103,A119;
                    end;
                    then p in v_strip(GoB f,i1) by A91,A117,A118,GOBOARD5:8;
                    then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) by A107,
XBOOLE_0:def 4;
                    then
A120:               p in cell(GoB f,i1,j2) by GOBOARD5:def 3;
                    p in {|[r,s]|:(GoB f)*(i1+1,1)`1<=r}
                    proof
                      ((GoB f)*(i1+1,j2))`1=((GoB f)*(i1+1,1))`1 & ((GoB
f)*(i1+1,j2+1))`1=((GoB f )*(i1+1,1))`1 by A3,A4,A8,A99,A87,A102,A100,
GOBOARD5:2;
                      hence thesis by A103;
                    end;
                    then p in v_strip(GoB f,i1+1) by A91,A117,GOBOARD5:9;
                    then p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A107,
XBOOLE_0:def 4;
                    then 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 A101,A120,XBOOLE_0:def 4;
                  end;
                  case
A121:               i1=0 & i1+1<len GoB f;
                    then
A122:               i1+1+1<=len GoB f by NAT_1:13;
                    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:13;
                      then
A123:                 ((GoB f)*(i1+1,1))`1<((GoB f)*(i1+1+1,1))`1 by A91,A102
,A122,GOBOARD5:3;
                      ((GoB f)*(i1+1,j2))`1=((GoB f)*(i1+1,1))`1 & ((GoB
f)*(i1+1,j2+1))`1=((GoB f )*(i1+1,1))`1 by A3,A4,A8,A99,A87,A102,A100,
GOBOARD5:2;
                      hence thesis by A103,A123;
                    end;
                    then p in v_strip(GoB f,i1+1) by A91,A121,GOBOARD5:8;
                    then p in v_strip(GoB f,i1+1)/\ h_strip(GoB f,j2) by A107,
XBOOLE_0:def 4;
                    then
A124:               p in cell(GoB f,i1+1,j2) by GOBOARD5:def 3;
                    p in {|[r,s]|: r<=(GoB f)*(1,1)`1}
                    proof
                      ((GoB f)*(i1+1,j2))`1=((GoB f)*(i1+1,1))`1 & ((GoB
f)*(i1+1,j2+1))`1=((GoB f )*(i1+1,1))`1 by A3,A4,A8,A99,A87,A102,A100,
GOBOARD5:2;
                      hence thesis by A103,A121;
                    end;
                    then p in v_strip(GoB f,i1) by A91,A121,GOBOARD5:10;
                    then p in v_strip(GoB f,i1)/\ h_strip(GoB f,j2) by A107,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i1,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 A101,A124,XBOOLE_0:def 4;
                  end;
                  case
                    i1=0 & i1+1=len GoB f;
                    hence contradiction by GOBOARD7:32;
                  end;
                end;
                then p in Cl Down(Int cell(GoB f,i1+1,j2),(L~f) `) by A4,Th2;
                then
A125:           Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`) c= Component_of
                p1 by A3,A4,A8,Th3,GOBRD11:1;
                p in Cl Down(Int cell(GoB f,i1,j2),(L~f)`) by A1,A4,A109,Th2;
                then Component_of p1 c= Down(LeftComp f,(L~f)`) \/ Down(
                RightComp f,(L~f)`) by A96,A94,Th5,CONNSP_3:21;
                then Cl Down(Int cell(GoB f,i1+1,j2),(L~f)`) c= Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A125;
                hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f by
A95,A97;
              end;
            end;
            hence Int cell(GoB f,i1+1,j2) c= LeftComp f \/ RightComp f;
          end;
        end;
        hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by A8;
      end;
      case
A126:   i1=i2+1;
        then i2<i1 by NAT_1:13;
        then
A127:   i1-'1<i1 by A126,NAT_D:34;
A128:   i2<i2+1 by NAT_1:13;
A129:   1<=i1-'1+1 by NAT_1:11;
A130:   i2+1<i2+1+1 by NAT_1:13;
A131:   1<=i1 & i1-'1=i1-1 by A126,NAT_1:11,XREAL_0:def 2;
A132:   1<=i2+1 by NAT_1:11;
A133:   i1-'1=i2 by A126,NAT_D:34;
        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
A134:       1<=k & k+1 <=len f and
A135:       j2<>0 and
A136:       j2<>width GoB f and
A137:       LSeg(f/.k,f/.(k+1)) =LSeg((GoB f)*(i1-'1+1,j2),(GoB f)*(
            i1-'1+1,j2 +1)) by A133;
            now
              per cases by A137,SPPOL_1:8;
              case
A138:           f/.k=(GoB f)*(i1-'1+1,j2) & f/.(k+1)= (GoB f)*(i1-'1 +1,j2+1);
A139:           Int left_cell(f,k) c= LeftComp f & LeftComp f c=
                LeftComp f \/ RightComp f by A134,GOBOARD9:21,XBOOLE_1:7;
                j2<width GoB f by A4,A136,XXREAL_0:1;
                then
A140:           j2+1<=width GoB f by NAT_1:13;
                i1-'1<len GoB f by A1,A127,XXREAL_0:2;
                then i1-'1+1<=len GoB f by NAT_1:13;
                then
A141:           Indices GoB f=[:dom GoB f,Seg width GoB f:] & i1-'1+1 in
                dom GoB f by A129,FINSEQ_3:25,MATRIX_0:def 4;
                1<=j2+1 by NAT_1:11;
                then j2+1 in Seg width GoB f by A140,FINSEQ_1:1;
                then
A142:           [i1-'1+1,j2+1] in Indices GoB f by A141,ZFMISC_1:87;
                j2>=0+1 by A135,NAT_1:13;
                then j2 in Seg width GoB f by A4,FINSEQ_1:1;
                then [i1-'1+1,j2] in Indices GoB f by A141,ZFMISC_1:87;
                then left_cell(f,k) = cell(GoB f,i1-'1,j2) by A134,A138,A142,
GOBOARD5:27;
                hence Int cell(GoB f,i1-'1,j2) c= LeftComp f \/ RightComp f by
A139;
              end;
              case
A143:           f/.k=(GoB f)*(i1-'1+1,j2+1) & f/.(k+1)= (GoB f)*(i1 -'1+1,j2);
A144:           Int right_cell(f,k) c= RightComp f & RightComp f c=
                LeftComp f \/ RightComp f by A134,GOBOARD9:25,XBOOLE_1:7;
                j2<width GoB f by A4,A136,XXREAL_0:1;
                then
A145:           j2+1<=width GoB f by NAT_1:13;
A146:           Indices GoB f=[:dom GoB f,Seg width GoB f:] & i1-'1+1 in
                dom GoB f by A1,A131,FINSEQ_3:25,MATRIX_0:def 4;
                1<=j2+1 by NAT_1:11;
                then j2+1 in Seg width GoB f by A145,FINSEQ_1:1;
                then
A147:           [i1-'1+1,j2+1] in Indices GoB f by A146,ZFMISC_1:87;
                j2>=0+1 by A135,NAT_1:13;
                then j2 in Seg width GoB f by A4,FINSEQ_1:1;
                then [i1-'1+1,j2] in Indices GoB f by A146,ZFMISC_1:87;
                then
right_cell(f,k) = cell(GoB f,i1-'1,j2) by A134,A143,A147,GOBOARD5:30;
                hence Int cell(GoB f,i1-'1,j2) c= LeftComp f \/ RightComp f by
A144;
              end;
            end;
            hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by A126,
NAT_D:34;
          end;
          case
A148:       not ex k st 1<=k & k+1 <=len f & j2<>0 & j2<>width GoB f
            & LSeg(f/.k,f/.(k+1)) =LSeg((GoB f)*(i2+1,j2),(GoB f)*(i2+1,j2+1));
            now
              per cases by A148;
              case
A149:           j2=0;
                reconsider p=|[((GoB f)*(i2+1,1))`1,((GoB f)*(i2+1,1))`2-1]|
                as Point of TOP-REAL 2;
A150:           1<width GoB f by GOBOARD7:33;
A151:           1<len GoB f by GOBOARD7:32;
                reconsider P={p} as Subset of TOP-REAL 2;
A152:           p`2<p`2+1 by XREAL_1:29;
A153:           1<=i2+1 by NAT_1:11;
                then ((GoB f)*(i2+1,1))`2=((GoB f)*(1,1))`2 by A1,A126,A150,
GOBOARD5:1;
                then
A154:           p`2=((GoB f)*(1,1))`2-1 by EUCLID:52;
                p in {|[r,s]|:s<=(GoB f)*(1,1)`2}
                proof
                  p=|[p`1,p`2]| by EUCLID:53;
                  hence thesis by A154,A152;
                end;
                then
A155:           p in h_strip(GoB f,j2) by A149,A151,GOBOARD5:7;
                (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
A156:           p in {p} & {p} c= (L~f)` by A154,A152,SUBSET_1:23,TARSKI:def 1;
                then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by
PRE_TOPC:8;
A157:           now
                  per cases by A1,A126,XXREAL_0:1;
                  case
A158:               i2+1<len GoB f & i2>0;
                    then
A159:               i2+1+1<=len GoB f by NAT_1:13;
A160:               p in {|[r,s]|:(GoB f)*(i2+1,1)`1<=r & r<=(GoB f)*(i2
                    +1+1,1)`1 }
                    proof
                      i2+1<i2+1+1 by NAT_1:13;
                      then ((GoB f)*(i2+1,1))`1<=(GoB f)*(i2+1+1,1)`1 by A150
,A153,A159,GOBOARD5:3;
                      hence thesis;
                    end;
A161:               0+1<=i2 by A158,NAT_1:13;
A162:               p in {|[r,s]|:(GoB f)*(i2,1)`1<=r & r<=(GoB f)*(i2+1 ,1)`1}
                    proof
                      i2<i2+1 by NAT_1:13;
                      then ((GoB f)*(i2,1))`1<((GoB f)*(i2+1,1))`1 by A1,A126
,A150,A161,GOBOARD5:3;
                      hence thesis;
                    end;
                    i2<len GoB f by A158,NAT_1:13;
                    then p in v_strip(GoB f,i2) by A150,A161,A162,GOBOARD5:8;
                    then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) by A155,
XBOOLE_0:def 4;
                    then
A163:               p in cell(GoB f,i2,j2) by GOBOARD5:def 3;
                    1<=i2+1 by A161,NAT_1:13;
                    then p in v_strip(GoB f,i2+1) by A150,A158,A160,GOBOARD5:8;
                    then p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A155,
XBOOLE_0:def 4;
                    then 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 A156,A163,XBOOLE_0:def 4;
                  end;
                  case
A164:               i2+1<len GoB f & i2=0;
A165:               i2+1<i2+1+1 by NAT_1:13;
A166:               i2+1+1<=len GoB f by A164,NAT_1:13;
                    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 A132,A150,A166
,A165,GOBOARD5:3;
                      hence thesis;
                    end;
                    then p in v_strip(GoB f,i2+1) by A150,A164,GOBOARD5:8;
                    then p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A155,
XBOOLE_0:def 4;
                    then
A167:               p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
                    p in {|[r,s]|: r<=(GoB f)*(i2+1,1)`1};
                    then p in v_strip(GoB f,i2) by A150,A164,GOBOARD5:10;
                    then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) by A155,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,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 A156,A167,XBOOLE_0:def 4;
                  end;
                  case
A168:               i2+1=len GoB f & i2>0;
                    then
A169:               0+1<=i2 by NAT_1:13;
A170:               p in {|[r,s]|:((GoB f)*(i2,1))`1<=r & r<=((GoB f)*(
                    i2+1,1))`1 }
                    proof
                      ((GoB f)*(i2,1))`1<((GoB f)*(i2+1,1))`1 by A128,A150,A168
,A169,GOBOARD5:3;
                      hence thesis;
                    end;
                    p in {|[r,s]|:(GoB f)*(i2+1,1)`1<=r};
                    then p in v_strip(GoB f,i2+1) by A150,A168,GOBOARD5:9;
                    then p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A155,
XBOOLE_0:def 4;
                    then
A171:               p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
                    i2<len GoB f by A168,NAT_1:13;
                    then p in v_strip(GoB f,i2) by A150,A169,A170,GOBOARD5:8;
                    then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) by A155,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,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 A156,A171,XBOOLE_0:def 4;
                  end;
                  case
A172:               i2+1=len GoB f & i2=0;
                    p in {|[r,s]|:(GoB f)*(i2+1,1)`1<=r};
                    then p in v_strip(GoB f,i2+1) by A150,A172,GOBOARD5:9;
                    then p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A155,
XBOOLE_0:def 4;
                    then
A173:               p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
                    p in {|[r,s]|: r<=(GoB f)*(1,1)`1} by A172;
                    then p in v_strip(GoB f,i2) by A150,A172,GOBOARD5:10;
                    then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) by A155,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,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 A156,A173,XBOOLE_0:def 4;
                  end;
                end;
                then p in Cl Down(Int cell(GoB f,i2,j2),(L~f)`) by A3,A4,Th2;
                then
A174:           Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= Component_of p1
                by A3,A4,Th3,GOBRD11:1;
                Down(RightComp f,(L~f)`) is closed by Lm4,CONNSP_1:33;
                then
A175:           Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) is closed by Lm3,CONNSP_1:33;
                then
A176:           Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`) by
PRE_TOPC:22;
A177:           Down(Int cell(GoB f,i2,j2),(L~f)`) c= Cl Down(Int cell(
GoB f,i2,j2),(L~f)`) & Down(Int cell(GoB f,i2,j2),(L~f)`)=Int cell(GoB f,i2,j2)
                by A3,A4,Th3,PRE_TOPC:18;
                Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`) =
                Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
                then
A178:           Cl Down(LeftComp f \/ RightComp f,(L~f)`) =Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A176,A175,PRE_TOPC:20;
A179:           Down(LeftComp f,(L~f)`)=LeftComp f & Down(RightComp f,(
                L~f)`)=RightComp f by Th5;
                Down(Int cell(GoB f,i1,j2),(L~f)`) c= LeftComp f \/
                RightComp f by A1,A2,A6,A7,Th3;
                then Down(Int cell(GoB f,i1,j2),(L~f)`) c= Down(LeftComp f \/
                RightComp f,(L~f)`) by A179,GOBRD11:4;
                then
A180:           Cl Down(Int cell(GoB f,i1,j2),(L~f)`) c= Cl Down(
                LeftComp f \/ RightComp f,(L~f)`) by PRE_TOPC:19;
                p in Cl Down(Int cell(GoB f,i2+1,j2),(L~f) `) by A4,A157,Th2;
                then Component_of p1 c= Down(LeftComp f,(L~f)`) \/ Down(
                RightComp f,(L~f)`) by A126,A180,A178,Th5,CONNSP_3:21;
                then Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= Down(LeftComp f
                ,(L~f)`) \/ Down(RightComp f,(L~f)`) by A174;
                hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by
A179,A177;
              end;
              case
A181:           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;
A182:           1<width GoB f by GOBOARD7:33;
                reconsider P={p} as Subset of TOP-REAL 2;
A183:           (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;
A184:           1<len GoB f by GOBOARD7:32;
A185:           1<=i2+1 by NAT_1:11;
                then ((GoB f)*(i2+1,width GoB f))`2 =((GoB f)*(1,width GoB f)
                )`2 by A1,A126,A182,GOBOARD5:1;
                then
A186:           p`2=((GoB f)*(1,width GoB f))`2+1 by EUCLID:52;
                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 A186,
EUCLID:53,XREAL_1:29;
                  hence thesis;
                end;
                then
A187:           p in h_strip(GoB f,j2) by A181,A184,GOBOARD5:6;
                ((GoB f)*(1,width GoB f))`2<((GoB f)*(1,width GoB f))`2+
                1 by XREAL_1:29;
                then
A188:           p in {p} & {p} c= (L~f)` by A186,A183,SUBSET_1:23,TARSKI:def 1;
                then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by
PRE_TOPC:8;
A189:           now
                  per cases by A1,A126,XXREAL_0:1;
                  case
A190:               i2+1<len GoB f & i2>0;
                    then
A191:               i2+1+1<=len GoB f by NAT_1:13;
A192:               p in {|[r,s]|:(GoB f)*(i2+1,width GoB f)`1<=r & r<=(
                    GoB f)*(i2+1+1,width GoB f)`1}
                    proof
                      i2+1<i2+1+1 by NAT_1:13;
                      then ((GoB f)*(i2+1,width GoB f))`1 <=(GoB f)*(i2+1+1,
                      width GoB f)`1 by A182,A185,A191,GOBOARD5:3;
                      hence thesis;
                    end;
                    1<=i2+1 by NAT_1:11;
                    then p in v_strip(GoB f,i2+1) by A182,A190,A192,GOBOARD5:8;
                    then p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A187,
XBOOLE_0:def 4;
                    then
A193:               p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
A194:               0+1<=i2 by A190,NAT_1:13;
A195:               i2<i2+1 by NAT_1:13;
A196:               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,A126,A182,A194,A195,GOBOARD5:3;
                      hence thesis;
                    end;
                    i2<len GoB f by A190,NAT_1:13;
                    then p in v_strip(GoB f,i2) by A182,A194,A196,GOBOARD5:8;
                    then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) by A187,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,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 A188,A193,XBOOLE_0:def 4;
                  end;
                  case
A197:               i2+1<len GoB f & i2=0;
                    then
A198:               i2+1+1<=len GoB f by NAT_1:13;
                    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 A132,A130,A182,A198,GOBOARD5:3;
                      hence thesis;
                    end;
                    then p in v_strip(GoB f,i2+1) by A182,A197,GOBOARD5:8;
                    then p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A187,
XBOOLE_0:def 4;
                    then
A199:               p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
                    p in {|[r,s]|: r<=(GoB f)*(1,width (GoB f))`1} by A197;
                    then p in v_strip(GoB f,i2) by A182,A197,GOBOARD5:10;
                    then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) by A187,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,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 A188,A199,XBOOLE_0:def 4;
                  end;
                  case
A200:               i2+1=len GoB f & i2>0;
                    then
A201:               0+1<=i2 by NAT_1:13;
A202:               p in {|[r,s]|:(GoB f)*(i2,width (GoB f))`1<=r & r<=(
                    GoB f)*(i2+1,width (GoB f))`1}
                    proof
                      ((GoB f)*(i2,width (GoB f)))`1 <=(GoB f)*(i2+1,
                      width (GoB f))`1 by A128,A182,A200,A201,GOBOARD5:3;
                      hence thesis;
                    end;
                    p in {|[r,s]|: (GoB f)*(len GoB f,width (GoB f))`1<=
                    r} by A200;
                    then p in v_strip(GoB f,i2+1) by A182,A200,GOBOARD5:9;
                    then p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A187,
XBOOLE_0:def 4;
                    then
A203:               p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
                    i2<len GoB f by A200,NAT_1:13;
                    then p in v_strip(GoB f,i2) by A182,A201,A202,GOBOARD5:8;
                    then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) by A187,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,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 A188,A203,XBOOLE_0:def 4;
                  end;
                  case
                    i2+1=len GoB f & i2=0;
                    hence contradiction by GOBOARD7:32;
                  end;
                end;
                then p in Cl Down(Int cell(GoB f,i2,j2),(L~f)`) by A3,A4,Th2;
                then
A204:           Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= Component_of p1
                by A3,A4,Th3,GOBRD11:1;
                Down(RightComp f,(L~f)`) is closed by Lm4,CONNSP_1:33;
                then
A205:           Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) is closed by Lm3,CONNSP_1:33;
                then
A206:           Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`) by
PRE_TOPC:22;
A207:           Down(Int cell(GoB f,i2,j2),(L~f)`) c= Cl Down(Int cell(
GoB f,i2,j2),(L~f)`) & Down(Int cell(GoB f,i2,j2),(L~f)`)=Int cell(GoB f,i2,j2)
                by A3,A4,Th3,PRE_TOPC:18;
                Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`) =
                Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
                then
A208:           Cl Down(LeftComp f \/ RightComp f,(L~f)`) =Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A206,A205,PRE_TOPC:20;
A209:           Down(LeftComp f,(L~f)`)=LeftComp f & Down(RightComp f,(
                L~f)`)=RightComp f by Th5;
                Down(Int cell(GoB f,i1,j2),(L~f)`) c= LeftComp f \/
                RightComp f by A1,A2,A6,A7,Th3;
                then Down(Int cell(GoB f,i1,j2),(L~f)`) c= Down(LeftComp f \/
                RightComp f,(L~f)`) by A209,GOBRD11:4;
                then
A210:           Cl Down(Int cell(GoB f,i1,j2),(L~f)`) c= Cl Down(
                LeftComp f \/ RightComp f,(L~f)`) by PRE_TOPC:19;
                p in Cl Down(Int cell(GoB f,i2+1,j2),(L~f) `) by A4,A189,Th2;
                then Component_of p1 c= Down(LeftComp f,(L~f)`) \/ Down(
                RightComp f,(L~f)`) by A126,A210,A208,Th5,CONNSP_3:21;
                then Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= Down(LeftComp f
                ,(L~f)`) \/ Down(RightComp f,(L~f)`) by A204;
                hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by
A209,A207;
              end;
              case
A211:           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
A212:           j2<width GoB f by A4,XXREAL_0:1;
                then
A213:           j2+1<=width GoB f by NAT_1:13;
                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
A214:             1<=k & k+1<=len f;
                  then LSeg(f,k)=LSeg(f/.k,f/.(k+1)) by TOPREAL1:def 3;
                  hence thesis by A211,A214;
                end;
                then
A215:           1 <= i2+1 & i2+1 <= len GoB f & 1 <= j2 & j2+1 <= width
GoB f implies not 1/2*((GoB f)*(i2+1,j2)+(GoB f)*(i2+1,j2+1)) in L~f by
GOBOARD7:39;
                reconsider p=1/2*((GoB f)*(i2+1,j2)+(GoB f)*(i2+1,j2+1)) as
                Point of TOP-REAL 2;
A216:           p`2=1/2*((GoB f)*(i2+1,j2)+(GoB f)*(i2+1,j2+1))`2 by TOPREAL3:4
                  .=1/2*(((GoB f)*(i2+1,j2))`2+((GoB f)*(i2+1,j2+1))`2) by
TOPREAL3:2;
                reconsider P={p} as Subset of TOP-REAL 2;
A217:           1<width GoB f by GOBOARD7:33;
                Down(RightComp f,(L~f)`) is closed by Lm4,CONNSP_1:33;
                then
A218:           Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) is closed by Lm3,CONNSP_1:33;
                then
A219:           Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`) =
                Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
                then
A220:           Cl Down(LeftComp f \/ RightComp f,(L~f)`) =Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A219,A218,PRE_TOPC:20;
A221:           1<=i2+1 by NAT_1:11;
                p`1=1/2*((GoB f)*(i2+1,j2)+(GoB f)*(i2+1,j2+1))`1 by TOPREAL3:4
                  .=1/2*(((GoB f)*(i2+1,j2))`1+((GoB f)*(i2+1,j2+1))`1) by
TOPREAL3:2;
                then
A222:           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 A216,EUCLID:53;
A223:           Down(Int cell(GoB f,i2,j2),(L~f)`) c= Cl Down(Int cell(
GoB f,i2,j2),(L~f)`) & Down(Int cell(GoB f,i2,j2),(L~f)`)=Int cell(GoB f,i2,j2)
                by A3,A4,Th3,PRE_TOPC:18;
A224:           Down(LeftComp f,(L~f)`)=LeftComp f & Down(RightComp f,(
                L~f)`)=RightComp f by Th5;
                Down(Int cell(GoB f,i1,j2),(L~f)`) c= LeftComp f \/
                RightComp f by A1,A2,A6,A7,Th3;
                then Down(Int cell(GoB f,i1,j2),(L~f)`) c= Down(LeftComp f \/
                RightComp f,(L~f)`) by A224,GOBRD11:4;
                then
A225:           Cl Down(Int cell(GoB f,i1,j2),(L~f)`) c= Cl Down(
                LeftComp f \/ RightComp f,(L~f)`) by PRE_TOPC:19;
A226:           0+1<=j2 by A211,NAT_1:13;
                then
A227:           1<j2+1 by NAT_1:13;
                (for x being object st x in P holds not x in (L~f))
implies P misses
                L~f by XBOOLE_0:3;
                then
A228:           p in {p} & {p} c= (L~f)` by A1,A126,A226,A212,A215,NAT_1:13
,SUBSET_1:23,TARSKI:def 1;
                then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by
PRE_TOPC:8;
A229:           1<=1+i2 by NAT_1:11;
                j2<j2+1 by NAT_1:13;
                then
A230:           ((GoB f)*(i2+1,j2))`2 <((GoB f)*(i2+1,j2+1))`2 by A1,A126,A226
,A213,A229,GOBOARD5:4;
                then ((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 XREAL_1:8;
                then
A231:           (((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 XREAL_1:74;
                ((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 A230,XREAL_1:8;
                then
A232:           (((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 XREAL_1:74;
                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:53;
                  hence thesis by A216,A232,A231;
                end;
                then
A233:           p in h_strip(GoB f,j2) by A1,A126,A226,A212,A221,GOBOARD5:5;
A234:           i2=0 or i2>=0+1 by NAT_1:13;
A235:           now
                  per cases by A1,A126,A234,XXREAL_0:1;
                  case
A236:               i2>=1 & i2+1<len GoB f;
                    then
A237:               i2+1+1<=len GoB f by NAT_1:13;
A238:               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:13;
                      then
A239:                 ((GoB f)*(i2+1,1))`1<((GoB f)*(i2+1+1,1))`1 by A217,A229
,A237,GOBOARD5:3;
                      ((GoB f)*(i2+1,j2))`1=((GoB f)*(i2+1,1))`1 & ((GoB
f)*(i2+1,j2+1))`1=((GoB f )*(i2+1,1))`1 by A1,A4,A126,A226,A213,A229,A227,
GOBOARD5:2;
                      hence thesis by A222,A239;
                    end;
                    1<=i2+1 by NAT_1:11;
                    then p in v_strip(GoB f,i2+1) by A217,A236,A238,GOBOARD5:8;
                    then p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A233,
XBOOLE_0:def 4;
                    then
A240:               p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
A241:               p in {|[r,s]|:(GoB f)*(i2,1)`1<=r & r<=(GoB f)*(i2+1 ,1)`1}
                    proof
                      i2<i2+1 by NAT_1:13;
                      then
A242:                 ((GoB f)*(i2,1))`1<((GoB f)*(i2+1,1))`1 by A217,A236,
GOBOARD5:3;
                      ((GoB f)*(i2+1,j2))`1=((GoB f)*(i2+1,1))`1 & ((GoB
f)*(i2+1,j2+1))`1=((GoB f )*(i2+1,1))`1 by A1,A4,A126,A226,A213,A229,A227,
GOBOARD5:2;
                      hence thesis by A222,A242;
                    end;
                    i2<len GoB f by A236,NAT_1:13;
                    then p in v_strip(GoB f,i2) by A217,A236,A241,GOBOARD5:8;
                    then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) by A233,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,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 A228,A240,XBOOLE_0:def 4;
                  end;
                  case
A243:               i2>=1 & i2+1=len GoB f;
A244:               i2<i2+1 by NAT_1:13;
                    p in {|[r,s]|:(GoB f)*(i2,1)`1<=r & r<=(GoB f)*(i2+1 ,1)`1}
                    proof
A245:                 ((GoB f)*(i2,1))`1<((GoB f)*(i2+1,1))`1 by A217,A243,A244
,GOBOARD5:3;
                      ((GoB f)*(i2+1,j2))`1=((GoB f)*(i2+1,1))`1 & ((GoB
f)*(i2+1,j2+1))`1=((GoB f )*(i2+1,1))`1 by A1,A4,A126,A226,A213,A229,A227,
GOBOARD5:2;
                      hence thesis by A222,A245;
                    end;
                    then p in v_strip(GoB f,i2) by A217,A243,A244,GOBOARD5:8;
                    then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) by A233,
XBOOLE_0:def 4;
                    then
A246:               p in cell(GoB f,i2,j2) by GOBOARD5:def 3;
                    p in {|[r,s]|:(GoB f)*(i2+1,1)`1<=r}
                    proof
                      ((GoB f)*(i2+1,j2))`1=((GoB f)*(i2+1,1))`1 & ((GoB
f)*(i2+1,j2+1))`1=((GoB f )*(i2+1,1))`1 by A1,A4,A126,A226,A213,A229,A227,
GOBOARD5:2;
                      hence thesis by A222;
                    end;
                    then p in v_strip(GoB f,i2+1) by A217,A243,GOBOARD5:9;
                    then p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A233,
XBOOLE_0:def 4;
                    then 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 A228,A246,XBOOLE_0:def 4;
                  end;
                  case
A247:               i2=0 & i2+1<len GoB f;
                    then
A248:               i2+1+1<=len GoB f by NAT_1:13;
                    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:13;
                      then
A249:                 ((GoB f)*(i2+1,1))`1<((GoB f)*(i2+1+1,1))`1 by A217,A229
,A248,GOBOARD5:3;
                      ((GoB f)*(i2+1,j2))`1=((GoB f)*(i2+1,1))`1 & ((GoB
f)*(i2+1,j2+1))`1=((GoB f )*(i2+1,1))`1 by A1,A4,A126,A226,A213,A229,A227,
GOBOARD5:2;
                      hence thesis by A222,A249;
                    end;
                    then p in v_strip(GoB f,i1) by A126,A217,A247,GOBOARD5:8;
                    then p in v_strip(GoB f,i2+1)/\ h_strip(GoB f,j2) by A126
,A233,XBOOLE_0:def 4;
                    then
A250:               p in cell(GoB f,i2+1,j2) by GOBOARD5:def 3;
                    p in {|[r,s]|: r<=(GoB f)*(1,1)`1}
                    proof
                      ((GoB f)*(i2+1,j2))`1=((GoB f)*(i2+1,1))`1 & ((GoB
f)*(i2+1,j2+1))`1=((GoB f )*(i2+1,1))`1 by A1,A4,A126,A226,A213,A229,A227,
GOBOARD5:2;
                      hence thesis by A222,A247;
                    end;
                    then p in v_strip(GoB f,i2) by A217,A247,GOBOARD5:10;
                    then p in v_strip(GoB f,i2)/\ h_strip(GoB f,j2) by A233,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,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 A228,A250,XBOOLE_0:def 4;
                  end;
                  case
                    i2=0 & i2+1=len GoB f;
                    hence contradiction by GOBOARD7:32;
                  end;
                end;
                then p in Cl Down(Int cell(GoB f,i2,j2),(L~f)`) by A3,A4,Th2;
                then
A251:           Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= Component_of p1
                by A3,A4,Th3,GOBRD11:1;
                p in Cl Down(Int cell(GoB f,i1,j2),(L~f)`) by A4,A126,A235,Th2;
                then Component_of p1 c= Down(LeftComp f,(L~f)`) \/ Down(
                RightComp f,(L~f)`) by A225,A220,Th5,CONNSP_3:21;
                then Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= Down(LeftComp f
                ,(L~f)`) \/ Down(RightComp f,(L~f)`) by A251;
                hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by
A224,A223;
              end;
            end;
            hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f;
          end;
        end;
        hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f;
      end;
    end;
    hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f;
  end;
  hence thesis;
end;

Lm6: 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 that
A1: i1<=len GoB f and
A2: j1<=width GoB f and
A3: i2<=len GoB f and
A4: j2<=width GoB f and
A5: j2=j1+1 or j1=j2+1 and
A6: i1=i2;
  now
    assume
A7: Int cell(GoB f,i1,j1) c= LeftComp f \/ RightComp f;
    now
      per cases by A5;
      case
A8:     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
A9:         1<=k & k+1 <=len f and
A10:        i2<>0 and
A11:        i2<>len GoB f and
A12:        LSeg(f/.k,f/.(k+1))=LSeg((GoB f)*(i2,j1+1),(GoB f)*(i2+1, j1+1));
            now
              per cases by A12,SPPOL_1:8;
              case
A13:            f/.k=(GoB f)*(i2,j1+1)& f/.(k+1)= (GoB f)*(i2+1,j1+1);
A14:            Int left_cell(f,k) c= LeftComp f & LeftComp f c= LeftComp
                f \/ RightComp f by A9,GOBOARD9:21,XBOOLE_1:7;
                i2<len GoB f by A3,A11,XXREAL_0:1;
                then
A15:            i2+1<=len GoB f by NAT_1:13;
                0+1<=j1+1 by XREAL_1:6;
                then
A16:            Indices GoB f=[:dom GoB f,Seg width GoB f:] & j1+1 in Seg
                width GoB f by A4,A8,FINSEQ_1:1,MATRIX_0:def 4;
                1<=i2+1 by NAT_1:11;
                then i2+1 in dom GoB f by A15,FINSEQ_3:25;
                then
A17:            [i2+1,j1+1] in Indices GoB f by A16,ZFMISC_1:87;
                i2>=0+1 by A10,NAT_1:13;
                then i2 in dom GoB f by A3,FINSEQ_3:25;
                then [i2,j1+1] in Indices GoB f by A16,ZFMISC_1:87;
                then left_cell(f,k) = cell(GoB f,i2,j1+1) by A9,A13,A17,
GOBOARD5:28;
                hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f by
A14;
              end;
              case
A18:            f/.k=(GoB f)*(i2+1,j1+1)& f/.(k+1)= (GoB f)*(i2,j1+1);
A19:            Int right_cell(f,k) c= RightComp f & RightComp f c=
                LeftComp f \/ RightComp f by A9,GOBOARD9:25,XBOOLE_1:7;
                i2<len GoB f by A3,A11,XXREAL_0:1;
                then
A20:            i2+1<=len GoB f by NAT_1:13;
                0+1<=j1+1 by XREAL_1:6;
                then
A21:            Indices GoB f=[:dom GoB f,Seg width GoB f:] & j1+1 in Seg
                width GoB f by A4,A8,FINSEQ_1:1,MATRIX_0:def 4;
                1<=i2+1 by NAT_1:11;
                then i2+1 in dom GoB f by A20,FINSEQ_3:25;
                then
A22:            [i2+1,j1+1] in Indices GoB f by A21,ZFMISC_1:87;
                i2>=0+1 by A10,NAT_1:13;
                then i2 in dom GoB f by A3,FINSEQ_3:25;
                then [i2,j1+1] in Indices GoB f by A21,ZFMISC_1:87;
                then right_cell(f,k) = cell(GoB f,i2,j1+1) by A9,A18,A22,
GOBOARD5:29;
                hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f by
A19;
              end;
            end;
            hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f;
          end;
          case
A23:        not ex k st 1<=k & k+1 <=len f & i2<>0 & i2<>len GoB f &
            LSeg(f/.k,f/.(k+1))=LSeg((GoB f)*(i2,j1+1),(GoB f)*(i2+1,j1+1));
            now
              per cases by A23;
              case
A24:            i2=0;
                reconsider p=|[((GoB f)*(1,j1+1))`1-1,((GoB f)*(1,j1+1))`2]|
                as Point of TOP-REAL 2;
A25:            1<len GoB f by GOBOARD7:32;
A26:            1<width GoB f by GOBOARD7:33;
                reconsider P={p} as Subset of TOP-REAL 2;
A27:            p`1<p`1+1 by XREAL_1:29;
A28:            1<=1+j1 by NAT_1:11;
                then ((GoB f)*(1,j1+1))`1=((GoB f)*(1,1))`1 by A4,A8,A25,
GOBOARD5:2;
                then
A29:            p`1=((GoB f)*(1,1))`1-1 by EUCLID:52;
                p in {|[s,r]| where s,r is Real:s<=(GoB f)*(1,1)`1}
                proof
                  p=|[p`1,p`2]| by EUCLID:53;
                  hence thesis by A29,A27;
                end;
                then
A30:            p in v_strip(GoB f,i2) by A24,A26,GOBOARD5:10;
                (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
A31:            p in {p} & {p} c= (L~f)` by A29,A27,SUBSET_1:23,TARSKI:def 1;
                then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by
PRE_TOPC:8;
A32:            j1=0 or j1>=0+1 by NAT_1:13;
A33:            now
                  per cases by A4,A8,A32,XXREAL_0:1;
                  case
A34:                j1>=1 & j1+1<width GoB f;
                    then
A35:                j1+1+1<=width GoB f by NAT_1:13;
A36:                p in {|[s,r]| where s,r is Real:
                    (GoB f)*(1,j1+1)`2<=r & r<=(GoB f)*(1,
                    j1+1+1)`2 }
                    proof
                      j1+1<j1+1+1 by NAT_1:13;
                      then ((GoB f)*(1,j1+1))`2<=(GoB f)*(1,j1+1+1)`2 by A25
,A28,A35,GOBOARD5:4;
                      hence thesis;
                    end;
                    1<=j1+1 by NAT_1:11;
                    then p in h_strip(GoB f,j1+1) by A25,A34,A36,GOBOARD5:5;
                    then p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A30,
XBOOLE_0:def 4;
                    then
A37:                p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
A38:                p in {|[s,r]| where s,r is Real:
                    (GoB f)*(1,j1)`2<=r & r<=(GoB f)*(1,j1+ 1)`2}
                    proof
                      j1<j1+1 by NAT_1:13;
                      then ((GoB f)*(1,j1))`2<((GoB f)*(1,j1+1))`2 by A25,A34,
GOBOARD5:4;
                      hence thesis;
                    end;
                    j1<width GoB f by A34,NAT_1:13;
                    then p in h_strip(GoB f,j1) by A25,A34,A38,GOBOARD5:5;
                    then
p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) by A30,XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j1) 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 A31,A37,XBOOLE_0:def 4;
                  end;
                  case
A39:                j1>=1 & j1+1=width GoB f;
A40:                j1<j1+1 by NAT_1:13;
A41:                p in {|[s,r]| where s,r is Real:
                    (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 A25,A39,A40,
GOBOARD5:4;
                      hence thesis;
                    end;
                    p in {|[s,r]|where s,r is Real:(GoB f)*(1,j1+1)`2<=r};
                    then p in h_strip(GoB f,j1+1) by A25,A39,GOBOARD5:6;
                    then p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A30,
XBOOLE_0:def 4;
                    then
A42:                p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
                    j1<width GoB f by A39,NAT_1:13;
                    then p in h_strip(GoB f,j1) by A25,A39,A41,GOBOARD5:5;
                    then
p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) by A30,XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j1) 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 A31,A42,XBOOLE_0:def 4;
                  end;
                  case
A43:                j1=0 & j1+1<width GoB f;
                    then
A44:                j1+1+1<=width GoB f by NAT_1:13;
                    p in {|[s,r]|where s,r is Real:
                    (GoB f)*(1,j1+1)`2<=r & r<=(GoB f)*(1,
                    j1+1+1)`2 }
                    proof
                      j1+1<j1+1+1 by NAT_1:13;
                      then ((GoB f)*(1,j1+1))`2<=(GoB f)*(1,j1+1+1)`2 by A25
,A28,A44,GOBOARD5:4;
                      hence thesis;
                    end;
                    then p in h_strip(GoB f,j1+1) by A25,A43,GOBOARD5:5;
                    then p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A30,
XBOOLE_0:def 4;
                    then
A45:                p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
                    p in {|[s,r]|where s,r is Real: r<=(GoB f)*(1,1)`2} by A43;
                    then p in h_strip(GoB f,j1) by A25,A43,GOBOARD5:7;
                    then
p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) by A30,XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j1) 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 A31,A45,XBOOLE_0:def 4;
                  end;
                  case
A46:                j1=0 & j1+1=width GoB f;
                    p in {|[s,r]|where s,r is Real:(GoB f)*(1,j1+1)`2<=r};
                    then p in h_strip(GoB f,j1+1) by A25,A46,GOBOARD5:6;
                    then p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A30,
XBOOLE_0:def 4;
                    then
A47:                p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
                    p in {|[s,r]|where s,r is Real: r<=(GoB f)*(1,1)`2} by A46;
                    then p in h_strip(GoB f,j1) by A25,A46,GOBOARD5:7;
                    then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) by A30,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j1) 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 A31,A47,XBOOLE_0:def 4;
                  end;
                end;
                then p in Cl Down(Int cell(GoB f,i2,j1+1),(L~f) `) by A3,Th2;
                then
A48:            Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`) c= Component_of
                p1 by A3,A4,A8,Th3,GOBRD11:1;
                Down(RightComp f,(L~f)`) is closed by Lm4,CONNSP_1:33;
                then
A49:            Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) is closed by Lm3,CONNSP_1:33;
                then
A50:            Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`) =
                Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
                then
A51:            Cl Down(LeftComp f \/ RightComp f,(L~f)`) =Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A50,A49,PRE_TOPC:20;
A52:            Down(Int cell(GoB f,i2,j1+1),(L~f)`) c= Cl Down(Int cell
(GoB f,i2,j1+1),(L~f) `) & Down(Int cell(GoB f,i2,j1+1),(L~f)`)=Int cell(GoB f,
                i2,j1+1) by A3,A4,A8,Th3,PRE_TOPC:18;
A53:            Down(LeftComp f,(L~f)`)=LeftComp f & Down(RightComp f,(
                L~f)`)=RightComp f by Th5;
                Down(Int cell(GoB f,i2,j1),(L~f)`) c= LeftComp f \/
                RightComp f by A1,A2,A6,A7,Th3;
                then Down(Int cell(GoB f,i2,j1),(L~f)`) c= Down(LeftComp f \/
                RightComp f,(L~f)`) by A53,GOBRD11:4;
                then
A54:            Cl Down(Int cell(GoB f,i2,j1),(L~f)`) c= Cl Down(
                LeftComp f \/ RightComp f,(L~f)`) by PRE_TOPC:19;
                p in Cl Down(Int cell(GoB f,i2,j1),(L~f)`) by A2,A3,A33,Th2;
                then Component_of p1 c= Down(LeftComp f,(L~f)`) \/ Down(
                RightComp f,(L~f)`) by A54,A51,Th5,CONNSP_3:21;
                then Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`) c= Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A48;
                hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f by
A53,A52;
              end;
              case
A55:            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;
A56:            1<len GoB f by GOBOARD7:32;
                reconsider P={p} as Subset of TOP-REAL 2;
A57:            (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;
A58:            1<width GoB f by GOBOARD7:33;
A59:            1<=1+j1 by NAT_1:11;
                then ((GoB f)*(len GoB f,j1+1))`1 =((GoB f)*(len GoB f,1))`1
                by A4,A8,A56,GOBOARD5:2;
                then
A60:            p`1=((GoB f)*(len GoB f,1))`1+1 by EUCLID:52;
                then
A61:            ((GoB f)*(len GoB f,1))`1<p`1 by XREAL_1:29;
                p in {|[s,r]|where s,r is Real:(GoB f)*(len (GoB f),1)`1<=s}
                proof
                  p=|[p`1,p`2]| by EUCLID:53;
                  hence thesis by A61;
                end;
                then
A62:            p in v_strip(GoB f,i2) by A55,A58,GOBOARD5:9;
                ((GoB f)*(len GoB f,1))`1<((GoB f)*(len GoB f,1))`1+1 by
XREAL_1:29;
                then
A63:            p in {p} & {p} c= (L~f)` by A60,A57,SUBSET_1:23,TARSKI:def 1;
                then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by
PRE_TOPC:8;
A64:            j1=0 or j1>=0+1 by NAT_1:13;
A65:            now
                  per cases by A4,A8,A64,XXREAL_0:1;
                  case
A66:                j1>=1 & j1+1<width GoB f;
                    then
A67:                j1+1+1<=width GoB f by NAT_1:13;
A68:                p in {|[s,r]|where s,r is Real
                    :(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:13;
                      then ((GoB f)*(len GoB f,j1+1))`2 <=(GoB f)*(len GoB f,
                      j1+1+1)`2 by A56,A59,A67,GOBOARD5:4;
                      hence thesis;
                    end;
                    1<=j1+1 by NAT_1:11;
                    then p in h_strip(GoB f,j1+1) by A56,A66,A68,GOBOARD5:5;
                    then p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A62,
XBOOLE_0:def 4;
                    then
A69:                p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
A70:                p in {|[s,r]| where s,r is Real
                    :(GoB f)*(len GoB f,j1)`2<=r & r<=(GoB
                    f)*(len GoB f,j1+1)`2}
                    proof
                      j1<j1+1 by NAT_1:13;
                      then ((GoB f)*(len GoB f,j1))`2 <((GoB f)*(len GoB f,j1
                      +1))`2 by A56,A66,GOBOARD5:4;
                      hence thesis;
                    end;
                    j1<width GoB f by A66,NAT_1:13;
                    then p in h_strip(GoB f,j1) by A56,A66,A70,GOBOARD5:5;
                    then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) by A62,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j1) 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 A63,A69,XBOOLE_0:def 4;
                  end;
                  case
A71:                j1>=1 & j1+1=width GoB f;
A72:                j1<j1+1 by NAT_1:13;
A73:                p in {|[s,r]| where s,r is Real:
                    (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 A56,A71,A72,GOBOARD5:4;
                      hence thesis;
                    end;
                    p in {|[s,r]| where s,r is Real:
                    (GoB f)*(len (GoB f),j1+1)`2<=r};
                    then p in h_strip(GoB f,j1+1) by A56,A71,GOBOARD5:6;
                    then p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A62,
XBOOLE_0:def 4;
                    then
A74:                p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
                    j1<width GoB f by A71,NAT_1:13;
                    then p in h_strip(GoB f,j1) by A56,A71,A73,GOBOARD5:5;
                    then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) by A62,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j1) 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 A63,A74,XBOOLE_0:def 4;
                  end;
                  case
A75:                j1=0 & j1+1<width GoB f;
                    then
A76:                j1+1+1<=width GoB f by NAT_1:13;
                    p in {|[s,r]| where s,r is Real:
                    (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:13;
                      then ((GoB f)*(len (GoB f),j1+1))`2 <=(GoB f)*(len (GoB
                      f),j1+1+1)`2 by A56,A59,A76,GOBOARD5:4;
                      hence thesis;
                    end;
                    then p in h_strip(GoB f,j1+1) by A56,A75,GOBOARD5:5;
                    then p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A62,
XBOOLE_0:def 4;
                    then
A77:                p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
                    p in {|[s,r]| where s,r is Real:
                    r<=(GoB f)*(len (GoB f),1)`2} by A75;
                    then p in h_strip(GoB f,j1) by A56,A75,GOBOARD5:7;
                    then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) by A62,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j1) 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 A63,A77,XBOOLE_0:def 4;
                  end;
                  case
                    j1=0 & j1+1=width GoB f;
                    hence contradiction by GOBOARD7:33;
                  end;
                end;
                then p in Cl Down(Int cell(GoB f,i2,j1+1),(L~f) `) by A3,Th2;
                then
A78:            Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`) c= Component_of
                p1 by A3,A4,A8,Th3,GOBRD11:1;
                Down(RightComp f,(L~f)`) is closed by Lm4,CONNSP_1:33;
                then
A79:            Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) is closed by Lm3,CONNSP_1:33;
                then
A80:            Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`) =
                Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
                then
A81:            Cl Down(LeftComp f \/ RightComp f,(L~f)`) =Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A80,A79,PRE_TOPC:20;
A82:            Down(Int cell(GoB f,i2,j1+1),(L~f)`) c= Cl Down(Int cell
(GoB f,i2,j1+1),(L~f) `) & Down(Int cell(GoB f,i2,j1+1),(L~f)`)=Int cell(GoB f,
                i2,j1+1) by A3,A4,A8,Th3,PRE_TOPC:18;
A83:            Down(LeftComp f,(L~f)`)=LeftComp f & Down(RightComp f,(
                L~f)`)=RightComp f by Th5;
                Down(Int cell(GoB f,i2,j1),(L~f)`) c= LeftComp f \/
                RightComp f by A1,A2,A6,A7,Th3;
                then Down(Int cell(GoB f,i2,j1),(L~f)`) c= Down(LeftComp f \/
                RightComp f,(L~f)`) by A83,GOBRD11:4;
                then
A84:            Cl Down(Int cell(GoB f,i2,j1),(L~f)`) c= Cl Down(
                LeftComp f \/ RightComp f,(L~f)`) by PRE_TOPC:19;
                p in Cl Down(Int cell(GoB f,i2,j1),(L~f)`) by A2,A3,A65,Th2;
                then Component_of p1 c= Down(LeftComp f,(L~f)`) \/ Down(
                RightComp f,(L~f)`) by A84,A81,Th5,CONNSP_3:21;
                then Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`) c= Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A78;
                hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f by
A83,A82;
              end;
              case
A85:            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
A86:            i2<len GoB f by A3,XXREAL_0:1;
                then
A87:            i2+1<=len GoB f by NAT_1:13;
                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
A88:              1<=k & k+1<=len f;
                  then LSeg(f,k)=LSeg(f/.k,f/.(k+1)) by TOPREAL1:def 3;
                  hence thesis by A85,A88;
                end;
                then
A89:            1 <= j1+1 & j1+1 <= width GoB f & 1 <= i2 & i2+1 <= len
GoB f implies not 1/2*((GoB f)*(i2,j1+1)+(GoB f)*(i2+1,j1+1)) in L~f by
GOBOARD7:40;
                reconsider p=1/2*((GoB f)*(i2,j1+1)+(GoB f)*(i2+1,j1+1)) as
                Point of TOP-REAL 2;
A90:            p`1=1/2*((GoB f)*(i2,j1+1)+(GoB f)*(i2+1,j1+1))`1 by TOPREAL3:4
                  .=1/2*(((GoB f)*(i2,j1+1))`1+((GoB f)*(i2+1,j1+1))`1) by
TOPREAL3:2;
                reconsider P={p} as Subset of TOP-REAL 2;
A91:            1<len GoB f by GOBOARD7:32;
                Down(RightComp f,(L~f)`) is closed by Lm4,CONNSP_1:33;
                then
A92:            Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) is closed by Lm3,CONNSP_1:33;
                then
A93:            Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`) =
                Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
                then
A94:            Cl Down(LeftComp f \/ RightComp f,(L~f)`) =Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A93,A92,PRE_TOPC:20;
A95:            Down(LeftComp f,(L~f)`)=LeftComp f & Down(RightComp f,(
                L~f)`)=RightComp f by Th5;
                Down(Int cell(GoB f,i2,j1),(L~f)`) c= LeftComp f \/
                RightComp f by A1,A2,A6,A7,Th3;
                then Down(Int cell(GoB f,i2,j1),(L~f)`) c= Down(LeftComp f \/
                RightComp f,(L~f)`) by A95,GOBRD11:4;
                then
A96:            Cl Down(Int cell(GoB f,i2,j1),(L~f)`) c= Cl Down(
                LeftComp f \/ RightComp f,(L~f)`) by PRE_TOPC:19;
A97:            Down(Int cell(GoB f,i2,j1+1),(L~f)`) c= Cl Down(Int cell
(GoB f,i2,j1+1),(L~f) `) & Down(Int cell(GoB f,i2,j1+1),(L~f)`)=Int cell(GoB f,
                i2,j1+1) by A3,A4,A8,Th3,PRE_TOPC:18;
A98:            1<=j1+1 by NAT_1:11;
A99:            0+1<=i2 by A85,NAT_1:13;
                then
A100:           1<i2+1 by NAT_1:13;
                (for x being object st x in P holds not x in (L~f))
implies P misses
                L~f by XBOOLE_0:3;
                then
A101:           p in {p} & {p} c= (L~f)` by A4,A8,A99,A86,A89,NAT_1:13
,SUBSET_1:23,TARSKI:def 1;
                then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by
PRE_TOPC:8;
A102:           1<=1+j1 by NAT_1:11;
                p`2=1/2*((GoB f)*(i2,j1+1)+(GoB f)*(i2+1,j1+1))`2 by TOPREAL3:4
                  .=1/2*(((GoB f)*(i2,j1+1))`2+((GoB f)*(i2+1,j1+1))`2) by
TOPREAL3:2;
                then
A103:           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 A90,EUCLID:53;
                i2<i2+1 by NAT_1:13;
                then
A104:           ((GoB f)*(i2,j1+1))`1 <((GoB f)*(i2+1,j1+1))`1 by A4,A8,A99,A87
,A102,GOBOARD5:3;
                then ((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 XREAL_1:8;
                then
A105:           (((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 XREAL_1:74;
                ((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 A104,XREAL_1:8;
                then
A106:           (((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 XREAL_1:74;
                p in {|[s,r]| where s,r is Real:
                (GoB f)*(i2,j1+1)`1<=s & s<=(GoB f)*(i2+1,
                j1+1) `1 }
                proof
                  p=|[p`1,p`2]| by EUCLID:53;
                  hence thesis by A90,A106,A105;
                end;
                then
A107:           p in v_strip(GoB f,i2) by A4,A8,A99,A86,A98,GOBOARD5:8;
A108:           j1=0 or j1>=0+1 by NAT_1:13;
A109:           now
                  per cases by A4,A8,A108,XXREAL_0:1;
                  case
A110:               j1>=1 & j1+1<width GoB f;
                    then
A111:               j1+1+1<=width GoB f by NAT_1:13;
A112:               p in {|[s,r]| where s,r is Real:
                    (GoB f)*(1,j1+1)`2<=r & r<=(GoB f)*(1,
                    j1+1+1)`2 }
                    proof
                      j1+1<j1+1+1 by NAT_1:13;
                      then
A113:                 ((GoB f)*(1,j1+1))`2<((GoB f)*(1,j1+1+1))`2 by A91,A102
,A111,GOBOARD5:4;
                      ((GoB f)*(i2,j1+1))`2=((GoB f)*(1,j1+1))`2 & ((GoB
f)*(i2+1,j1+1))`2=((GoB f )*(1,j1+1))`2 by A3,A4,A8,A99,A87,A102,A100,
GOBOARD5:1;
                      hence thesis by A103,A113;
                    end;
                    1<=j1+1 by NAT_1:11;
                    then p in h_strip(GoB f,j1+1) by A91,A110,A112,GOBOARD5:5;
                    then p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A107,
XBOOLE_0:def 4;
                    then
A114:               p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
A115:               p in {|[s,r]| where s,r is Real:
                    (GoB f)*(1,j1)`2<=r & r<=(GoB f)*(1,j1 +1)`2}
                    proof
                      j1<j1+1 by NAT_1:13;
                      then
A116:                 ((GoB f)*(1,j1))`2<((GoB f)*(1,j1+1))`2 by A91,A110,
GOBOARD5:4;
                      ((GoB f)*(i2,j1+1))`2=((GoB f)*(1,j1+1))`2 & ((GoB
f)*(i2+1,j1+1))`2=((GoB f )*(1,j1+1))`2 by A3,A4,A8,A99,A87,A102,A100,
GOBOARD5:1;
                      hence thesis by A103,A116;
                    end;
                    j1<width GoB f by A110,NAT_1:13;
                    then p in h_strip(GoB f,j1) by A91,A110,A115,GOBOARD5:5;
                    then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) by A107,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j1) 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 A101,A114,XBOOLE_0:def 4;
                  end;
                  case
A117:               j1>=1 & j1+1=width GoB f;
A118:               j1<j1+1 by NAT_1:13;
                    p in {|[s,r]| where s,r is Real:
                    (GoB f)*(1,j1)`2<=r & r<=(GoB f)*(1,j1 +1)`2}
                    proof
A119:                 ((GoB f)*(1,j1))`2<((GoB f)*(1,j1+1))`2 by A91,A117,A118,
GOBOARD5:4;
                      ((GoB f)*(i2,j1+1))`2=((GoB f)*(1,j1+1))`2 & ((GoB
f)*(i2+1,j1+1))`2=((GoB f )*(1,j1+1))`2 by A3,A4,A8,A99,A87,A102,A100,
GOBOARD5:1;
                      hence thesis by A103,A119;
                    end;
                    then p in h_strip(GoB f,j1) by A91,A117,A118,GOBOARD5:5;
                    then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) by A107,
XBOOLE_0:def 4;
                    then
A120:               p in cell(GoB f,i2,j1) by GOBOARD5:def 3;
                    p in {|[s,r]| where s,r is Real:(GoB f)*(1,j1+1)`2<=r}
                    proof
                      ((GoB f)*(i2,j1+1))`2=((GoB f)*(1,j1+1))`2 & ((GoB
f)*(i2+1,j1+1))`2=((GoB f )*(1,j1+1))`2 by A3,A4,A8,A99,A87,A102,A100,
GOBOARD5:1;
                      hence thesis by A103;
                    end;
                    then p in h_strip(GoB f,j1+1) by A91,A117,GOBOARD5:6;
                    then p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A107,
XBOOLE_0:def 4;
                    then 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 A101,A120,XBOOLE_0:def 4;
                  end;
                  case
A121:               j1=0 & j1+1<width GoB f;
                    then
A122:               j1+1+1<=width GoB f by NAT_1:13;
                    p in {|[s,r]| where s,r is Real:
                    (GoB f)*(1,j1+1)`2<=r & r<=(GoB f)*(1,
                    j1+1+1)`2 }
                    proof
                      j1+1<j1+1+1 by NAT_1:13;
                      then
A123:                 ((GoB f)*(1,j1+1))`2<((GoB f)*(1,j1+1+1))`2 by A91,A102
,A122,GOBOARD5:4;
                      ((GoB f)*(i2,j1+1))`2=((GoB f)*(1,j1+1))`2 & ((GoB
f)*(i2+1,j1+1))`2=((GoB f )*(1,j1+1))`2 by A3,A4,A8,A99,A87,A102,A100,
GOBOARD5:1;
                      hence thesis by A103,A123;
                    end;
                    then p in h_strip(GoB f,j1+1) by A91,A121,GOBOARD5:5;
                    then p in h_strip(GoB f,j1+1)/\ v_strip(GoB f,i2) by A107,
XBOOLE_0:def 4;
                    then
A124:               p in cell(GoB f,i2,j1+1) by GOBOARD5:def 3;
                    p in {|[s,r]| where s,r is Real: r<=(GoB f)*(1,1)`2}
                    proof
                      ((GoB f)*(i2,j1+1))`2=((GoB f)*(1,j1+1))`2 & ((GoB
f)*(i2+1,j1+1))`2=((GoB f )*(1,j1+1))`2 by A3,A4,A8,A99,A87,A102,A100,
GOBOARD5:1;
                      hence thesis by A103,A121;
                    end;
                    then p in h_strip(GoB f,j1) by A91,A121,GOBOARD5:7;
                    then p in h_strip(GoB f,j1)/\ v_strip(GoB f,i2) by A107,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j1) 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 A101,A124,XBOOLE_0:def 4;
                  end;
                  case
                    j1=0 & j1+1=width GoB f;
                    hence contradiction by GOBOARD7:33;
                  end;
                end;
                then p in Cl Down(Int cell(GoB f,i2,j1+1),(L~f) `) by A3,Th2;
                then
A125:           Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`) c= Component_of
                p1 by A3,A4,A8,Th3,GOBRD11:1;
                p in Cl Down(Int cell(GoB f,i2,j1),(L~f)`) by A2,A3,A109,Th2;
                then Component_of p1 c= Down(LeftComp f,(L~f)`) \/ Down(
                RightComp f,(L~f)`) by A96,A94,Th5,CONNSP_3:21;
                then Cl Down(Int cell(GoB f,i2,j1+1),(L~f)`) c= Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A125;
                hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f by
A95,A97;
              end;
            end;
            hence Int cell(GoB f,i2,j1+1) c= LeftComp f \/ RightComp f;
          end;
        end;
        hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by A8;
      end;
      case
A126:   j1=j2+1;
        then j2<j1 by NAT_1:13;
        then
A127:   j1-'1<j1 by A126,NAT_D:34;
A128:   j2<j2+1 by NAT_1:13;
A129:   1<=j1-'1+1 by NAT_1:11;
A130:   j2+1<j2+1+1 by NAT_1:13;
A131:   1<=j1 & j1-'1=j1-1 by A126,NAT_1:11,XREAL_0:def 2;
A132:   1<=j2+1 by NAT_1:11;
A133:   j1-'1=j2 by A126,NAT_D:34;
        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
A134:       1<=k & k+1 <=len f and
A135:       i2<>0 and
A136:       i2<>len GoB f and
A137:       LSeg(f/.k,f/.(k+1)) =LSeg((GoB f)*(i2,j1-'1+1),(GoB f)*(
            i2+1,j1-'1 +1)) by A133;
            now
              per cases by A137,SPPOL_1:8;
              case
A138:           f/.k=(GoB f)*(i2,j1-'1+1) & f/.(k+1)= (GoB f)*(i2+1, j1-'1+1);
A139:           Int right_cell(f,k) c= RightComp f & RightComp f c=
                LeftComp f \/ RightComp f by A134,GOBOARD9:25,XBOOLE_1:7;
                i2<len GoB f by A3,A136,XXREAL_0:1;
                then
A140:           i2+1<=len GoB f by NAT_1:13;
                j1-'1<width GoB f by A2,A127,XXREAL_0:2;
                then j1-'1+1<=width GoB f by NAT_1:13;
                then
A141:           Indices GoB f=[:dom GoB f,Seg width GoB f:] & j1-'1+1 in
                Seg width GoB f by A129,FINSEQ_1:1,MATRIX_0:def 4;
                1<=i2+1 by NAT_1:11;
                then i2+1 in dom GoB f by A140,FINSEQ_3:25;
                then
A142:           [i2+1,j1-'1+1] in Indices GoB f by A141,ZFMISC_1:87;
                i2>=0+1 by A135,NAT_1:13;
                then i2 in dom GoB f by A3,FINSEQ_3:25;
                then [i2,j1-'1+1] in Indices GoB f by A141,ZFMISC_1:87;
                then
right_cell(f,k) = cell(GoB f,i2,j1-'1) by A134,A138,A142,GOBOARD5:28;
                hence Int cell(GoB f,i2,j1-'1) c= LeftComp f \/ RightComp f by
A139;
              end;
              case
A143:           f/.k=(GoB f)*(i2+1,j1-'1+1) & f/.(k+1)= (GoB f)*(i2, j1-'1+1);
A144:           Int left_cell(f,k) c= LeftComp f & LeftComp f c=
                LeftComp f \/ RightComp f by A134,GOBOARD9:21,XBOOLE_1:7;
                i2<len GoB f by A3,A136,XXREAL_0:1;
                then
A145:           i2+1<=len GoB f by NAT_1:13;
A146:           Indices GoB f=[:dom GoB f,Seg width GoB f:] & j1-'1+1 in
                Seg width GoB f by A2,A131,FINSEQ_1:1,MATRIX_0:def 4;
                1<=i2+1 by NAT_1:11;
                then i2+1 in dom GoB f by A145,FINSEQ_3:25;
                then
A147:           [i2+1,j1-'1+1] in Indices GoB f by A146,ZFMISC_1:87;
                i2>=0+1 by A135,NAT_1:13;
                then i2 in dom GoB f by A3,FINSEQ_3:25;
                then [i2,j1-'1+1] in Indices GoB f by A146,ZFMISC_1:87;
                then left_cell(f,k) = cell(GoB f,i2,j1-'1) by A134,A143,A147,
GOBOARD5:29;
                hence Int cell(GoB f,i2,j1-'1) c= LeftComp f \/ RightComp f by
A144;
              end;
            end;
            hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by A126,
NAT_D:34;
          end;
          case
A148:       not ex k st 1<=k & k+1 <=len f & i2<>0 & i2<>len GoB f &
            LSeg(f/.k,f/.(k+1)) =LSeg((GoB f)*(i2,j2+1),(GoB f)*(i2+1,j2+1));
            now
              per cases by A148;
              case
A149:           i2=0;
                reconsider p=|[((GoB f)*(1,j2+1))`1-1,((GoB f)*(1,j2+1))`2]|
                as Point of TOP-REAL 2;
A150:           1<len GoB f by GOBOARD7:32;
A151:           1<width GoB f by GOBOARD7:33;
                reconsider P={p} as Subset of TOP-REAL 2;
A152:           p`1<p`1+1 by XREAL_1:29;
A153:           1<=j2+1 by NAT_1:11;
                then ((GoB f)*(1,j2+1))`1=((GoB f)*(1,1))`1 by A2,A126,A150,
GOBOARD5:2;
                then
A154:           p`1=((GoB f)*(1,1))`1-1 by EUCLID:52;
                p in {|[s,r]| where s,r is Real:s<=(GoB f)*(1,1)`1}
                proof
                  p=|[p`1,p`2]| by EUCLID:53;
                  hence thesis by A154,A152;
                end;
                then
A155:           p in v_strip(GoB f,i2) by A149,A151,GOBOARD5:10;
                (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
A156:           p in {p} & {p} c= (L~f)` by A154,A152,SUBSET_1:23,TARSKI:def 1;
                then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by
PRE_TOPC:8;
A157:           now
                  per cases by A2,A126,XXREAL_0:1;
                  case
A158:               j2+1<width GoB f & j2>0;
                    then
A159:               j2+1+1<=width GoB f by NAT_1:13;
A160:               p in {|[s,r]| where s,r is Real:
                    (GoB f)*(1,j2+1)`2<=r & r<=(GoB f)*(1,
                    j2+1+1)`2 }
                    proof
                      j2+1<j2+1+1 by NAT_1:13;
                      then ((GoB f)*(1,j2+1))`2<=(GoB f)*(1,j2+1+1)`2 by A150
,A153,A159,GOBOARD5:4;
                      hence thesis;
                    end;
A161:               0+1<=j2 by A158,NAT_1:13;
A162:               p in {|[s,r]| where s,r is Real:
                    (GoB f)*(1,j2)`2<=r & r<=(GoB f)*(1,j2 +1)`2}
                    proof
                      j2<j2+1 by NAT_1:13;
                      then ((GoB f)*(1,j2))`2<((GoB f)*(1,j2+1))`2 by A2,A126
,A150,A161,GOBOARD5:4;
                      hence thesis;
                    end;
                    j2<width GoB f by A158,NAT_1:13;
                    then p in h_strip(GoB f,j2) by A150,A161,A162,GOBOARD5:5;
                    then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) by A155,
XBOOLE_0:def 4;
                    then
A163:               p in cell(GoB f,i2,j2) by GOBOARD5:def 3;
                    1<=j2+1 by A161,NAT_1:13;
                    then p in h_strip(GoB f,j2+1) by A150,A158,A160,GOBOARD5:5;
                    then p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A155,
XBOOLE_0:def 4;
                    then 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 A156,A163,XBOOLE_0:def 4;
                  end;
                  case
A164:               j2+1<width GoB f & j2=0;
A165:               j2+1<j2+1+1 by NAT_1:13;
A166:               j2+1+1<=width GoB f by A164,NAT_1:13;
                    p in {|[s,r]| where s,r is Real:
                    (GoB f)*(1,j2+1)`2<=r & r<=(GoB f)*(1,
                    j2+1+1)`2 }
                    proof
                      (GoB f)*(1,j2+1)`2<(GoB f)*(1,j2+1+1)`2 by A132,A150,A166
,A165,GOBOARD5:4;
                      hence thesis;
                    end;
                    then p in h_strip(GoB f,j2+1) by A150,A164,GOBOARD5:5;
                    then p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A155,
XBOOLE_0:def 4;
                    then
A167:               p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
                    p in {|[s,r]| where s,r is Real: r<=(GoB f)*(1,j2+1)`2};
                    then p in h_strip(GoB f,j2) by A150,A164,GOBOARD5:7;
                    then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) by A155,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j2) 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 A156,A167,XBOOLE_0:def 4;
                  end;
                  case
A168:               j2+1=width GoB f & j2>0;
                    then
A169:               0+1<=j2 by NAT_1:13;
A170:               p in {|[s,r]| where s,r is Real:
                    ((GoB f)*(1,j2))`2<=r & r<=((GoB f)*(1
                    ,j2+1))`2 }
                    proof
                      ((GoB f)*(1,j2))`2<((GoB f)*(1,j2+1))`2 by A128,A150,A168
,A169,GOBOARD5:4;
                      hence thesis;
                    end;
                    p in {|[s,r]| where s,r is Real:(GoB f)*(1,j2+1)`2<=r};
                    then p in h_strip(GoB f,j2+1) by A150,A168,GOBOARD5:6;
                    then p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A155,
XBOOLE_0:def 4;
                    then
A171:               p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
                    j2<width GoB f by A168,NAT_1:13;
                    then p in h_strip(GoB f,j2) by A150,A169,A170,GOBOARD5:5;
                    then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) by A155,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j2) 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 A156,A171,XBOOLE_0:def 4;
                  end;
                  case
A172:               j2+1=width GoB f & j2=0;
                    p in {|[s,r]| where s,r is Real:(GoB f)*(1,j2+1)`2<=r};
                    then p in h_strip(GoB f,j2+1) by A150,A172,GOBOARD5:6;
                    then p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A155,
XBOOLE_0:def 4;
                    then
A173:               p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
                    p in {|[s,r]| where s,r is Real: r<=(GoB f)*(1,1)`2}
                    by A172;
                    then p in h_strip(GoB f,j2) by A150,A172,GOBOARD5:7;
                    then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) by A155,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j2) 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 A156,A173,XBOOLE_0:def 4;
                  end;
                end;
                then p in Cl Down(Int cell(GoB f,i2,j2),(L~f)`) by A3,A4,Th2;
                then
A174:           Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= Component_of p1
                by A3,A4,Th3,GOBRD11:1;
                Down(RightComp f,(L~f)`) is closed by Lm4,CONNSP_1:33;
                then
A175:           Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) is closed by Lm3,CONNSP_1:33;
                then
A176:           Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`) by
PRE_TOPC:22;
A177:           Down(Int cell(GoB f,i2,j2),(L~f)`) c= Cl Down(Int cell(
GoB f,i2,j2),(L~f)`) & Down(Int cell(GoB f,i2,j2),(L~f)`)=Int cell(GoB f,i2,j2)
                by A3,A4,Th3,PRE_TOPC:18;
                Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`) =
                Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
                then
A178:           Cl Down(LeftComp f \/ RightComp f,(L~f)`) =Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A176,A175,PRE_TOPC:20;
A179:           Down(LeftComp f,(L~f)`)=LeftComp f & Down(RightComp f,(
                L~f)`)=RightComp f by Th5;
                Down(Int cell(GoB f,i2,j1),(L~f)`) c= LeftComp f \/
                RightComp f by A1,A2,A6,A7,Th3;
                then Down(Int cell(GoB f,i2,j1),(L~f)`) c= Down(LeftComp f \/
                RightComp f,(L~f)`) by A179,GOBRD11:4;
                then
A180:           Cl Down(Int cell(GoB f,i2,j1),(L~f)`) c= Cl Down(
                LeftComp f \/ RightComp f,(L~f)`) by PRE_TOPC:19;
                p in Cl Down(Int cell(GoB f,i2,j2+1),(L~f) `) by A3,A157,Th2;
                then Component_of p1 c= Down(LeftComp f,(L~f)`) \/ Down(
                RightComp f,(L~f)`) by A126,A180,A178,Th5,CONNSP_3:21;
                then Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= Down(LeftComp f
                ,(L~f)`) \/ Down(RightComp f,(L~f)`) by A174;
                hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by
A179,A177;
              end;
              case
A181:           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;
A182:           1<len GoB f by GOBOARD7:32;
                reconsider P={p} as Subset of TOP-REAL 2;
A183:           (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;
A184:           1<width GoB f by GOBOARD7:33;
                1<=j2+1 by NAT_1:11;
                then ((GoB f)*(len GoB f,j2+1))`1 =((GoB f)*(len GoB f,1))`1
                by A2,A126,A182,GOBOARD5:2;
                then
A185:           p`1=((GoB f)*(len GoB f,1))`1+1 by EUCLID:52;
                then
A186:           ((GoB f)*(len GoB f,1))`1<p`1 by XREAL_1:29;
                p in {|[s,r]| where s,r is Real:(GoB f)*(len (GoB f),1)`1<=s}
                proof
                  p=|[p`1,p`2]| by EUCLID:53;
                  hence thesis by A186;
                end;
                then
A187:           p in v_strip(GoB f,i2) by A181,A184,GOBOARD5:9;
                ((GoB f)*(len GoB f,1))`1<((GoB f)*(len GoB f,1))`1+1 by
XREAL_1:29;
                then
A188:           p in {p} & {p} c= (L~f)` by A185,A183,SUBSET_1:23,TARSKI:def 1;
                then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by
PRE_TOPC:8;
A189:           now
                  per cases by A2,A126,XXREAL_0:1;
                  case
A190:               j2+1<width GoB f & j2>0;
                    then
A191:               j2+1+1<=width GoB f by NAT_1:13;
A192:               p in {|[s,r]|where s,r is Real
                    :(GoB f)*(len GoB f,j2+1)`2<=r & r<=(
                    GoB f)*(len GoB f,j2+1+1)`2}
                    proof
                      j2+1<j2+1+1 by NAT_1:13;
                      then ((GoB f)*(len GoB f,j2+1))`2 <=(GoB f)*(len GoB f,
                      j2+1+1)`2 by A132,A182,A191,GOBOARD5:4;
                      hence thesis;
                    end;
                    1<=j2+1 by NAT_1:11;
                    then p in h_strip(GoB f,j2+1) by A182,A190,A192,GOBOARD5:5;
                    then p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A187,
XBOOLE_0:def 4;
                    then
A193:               p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
A194:               0+1<=j2 by A190,NAT_1:13;
A195:               j2<j2+1 by NAT_1:13;
A196:               p in {|[s,r]| where s,r is Real:
                    (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 A2,A126,A182,A194,A195,GOBOARD5:4;
                      hence thesis;
                    end;
                    j2<width GoB f by A190,NAT_1:13;
                    then p in h_strip(GoB f,j2) by A182,A194,A196,GOBOARD5:5;
                    then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) by A187,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j2) 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 A188,A193,XBOOLE_0:def 4;
                  end;
                  case
A197:               j2+1<width GoB f & j2=0;
                    then
A198:               j2+1+1<=width GoB f by NAT_1:13;
                    p in {|[s,r]| where s,r is Real:
                    (GoB f)*(len (GoB f),j2+1)`2<=r & r<=(
                    GoB f)*(len (GoB f),j2+1+1)`2}
                    proof
                      (GoB f)*(len (GoB f),j2+1)`2 <(GoB f)*(len (GoB f)
                      ,j2+1+1)`2 by A132,A130,A182,A198,GOBOARD5:4;
                      hence thesis;
                    end;
                    then p in h_strip(GoB f,j2+1) by A182,A197,GOBOARD5:5;
                    then p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A187,
XBOOLE_0:def 4;
                    then
A199:               p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
                    p in {|[s,r]| where s,r is Real:
                    r<=(GoB f)*(len (GoB f),1)`2} by A197;
                    then p in h_strip(GoB f,j2) by A182,A197,GOBOARD5:7;
                    then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) by A187,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j2) 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 A188,A199,XBOOLE_0:def 4;
                  end;
                  case
A200:               j2+1=width GoB f & j2>0;
                    then
A201:               0+1<=j2 & j2<width GoB f by NAT_1:13;
                    p in {|[s,r]| where s,r is Real:
                    (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 A182,A200,A201,GOBOARD5:4;
                      hence thesis;
                    end;
                    then p in h_strip(GoB f,j2) by A182,A201,GOBOARD5:5;
                    then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) by A187,
XBOOLE_0:def 4;
                    then
A202:               p in cell(GoB f,i2,j2) by GOBOARD5:def 3;
                    p in {|[s,r]| where s,r is Real:
                    (GoB f)*(len GoB f,width GoB f)`2<=r}
                    by A200;
                    then p in h_strip(GoB f,j2+1) by A182,A200,GOBOARD5:6;
                    then p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A187,
XBOOLE_0:def 4;
                    then 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 A188,A202,XBOOLE_0:def 4;
                  end;
                  case
                    j2+1=width GoB f & j2=0;
                    hence contradiction by GOBOARD7:33;
                  end;
                end;
                then p in Cl Down(Int cell(GoB f,i2,j2),(L~f)`) by A3,A4,Th2;
                then
A203:           Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= Component_of p1
                by A3,A4,Th3,GOBRD11:1;
                Down(RightComp f,(L~f)`) is closed by Lm4,CONNSP_1:33;
                then
A204:           Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) is closed by Lm3,CONNSP_1:33;
                then
A205:           Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`) by
PRE_TOPC:22;
A206:           Down(Int cell(GoB f,i2,j2),(L~f)`) c= Cl Down(Int cell(
GoB f,i2,j2),(L~f)`) & Down(Int cell(GoB f,i2,j2),(L~f)`)=Int cell(GoB f,i2,j2)
                by A3,A4,Th3,PRE_TOPC:18;
                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,A204,PRE_TOPC:20;
A208:           Down(LeftComp f,(L~f)`)=LeftComp f & Down(RightComp f,(
                L~f)`)=RightComp f by Th5;
                Down(Int cell(GoB f,i2,j1),(L~f)`) c= LeftComp f \/
                RightComp f by A1,A2,A6,A7,Th3;
                then Down(Int cell(GoB f,i2,j1),(L~f)`) c= Down(LeftComp f \/
                RightComp f,(L~f)`) by A208,GOBRD11:4;
                then
A209:           Cl Down(Int cell(GoB f,i2,j1),(L~f)`) c= Cl Down(
                LeftComp f \/ RightComp f,(L~f)`) by PRE_TOPC:19;
                p in Cl Down(Int cell(GoB f,i2,j2+1),(L~f) `) by A3,A189,Th2;
                then Component_of p1 c= Down(LeftComp f,(L~f)`) \/ Down(
                RightComp f,(L~f)`) by A126,A209,A207,Th5,CONNSP_3:21;
                then Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= Down(LeftComp f
                ,(L~f)`) \/ Down(RightComp f,(L~f)`) by A203;
                hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by
A208,A206;
              end;
              case
A210:           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
A211:           i2<len GoB f by A3,XXREAL_0:1;
                then
A212:           i2+1<=len GoB f by NAT_1:13;
                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
A213:             1<=k & k+1<=len f;
                  then LSeg(f,k)=LSeg(f/.k,f/.(k+1)) by TOPREAL1:def 3;
                  hence thesis by A210,A213;
                end;
                then
A214:           1 <= j2+1 & j2+1 <= width GoB f & 1 <= i2 & i2+1 <= len
GoB f implies not 1/2*((GoB f)*(i2,j2+1)+(GoB f)*(i2+1,j2+1)) in L~f by
GOBOARD7:40;
                reconsider p=1/2*((GoB f)*(i2,j2+1)+(GoB f)*(i2+1,j2+1)) as
                Point of TOP-REAL 2;
A215:           p`1=1/2*((GoB f)*(i2,j2+1)+(GoB f)*(i2+1,j2+1))`1 by TOPREAL3:4
                  .=1/2*(((GoB f)*(i2,j2+1))`1+((GoB f)*(i2+1,j2+1))`1) by
TOPREAL3:2;
                reconsider P={p} as Subset of TOP-REAL 2;
A216:           1<len GoB f by GOBOARD7:32;
                Down(RightComp f,(L~f)`) is closed by Lm4,CONNSP_1:33;
                then
A217:           Cl Down(RightComp f,(L~f)`)=Down(RightComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) is closed by Lm3,CONNSP_1:33;
                then
A218:           Cl Down(LeftComp f,(L~f)`)=Down(LeftComp f,(L~f)`) by
PRE_TOPC:22;
                Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`) =
                Down((LeftComp f) \/ (RightComp f),(L~f)`) by GOBRD11:4;
                then
A219:           Cl Down(LeftComp f \/ RightComp f,(L~f)`) =Down(LeftComp
                f,(L~f)`) \/ Down(RightComp f,(L~f)`) by A218,A217,PRE_TOPC:20;
A220:           1<=j2+1 by NAT_1:11;
A221:           Down(Int cell(GoB f,i2,j2),(L~f)`) c= Cl Down(Int cell(
GoB f,i2,j2),(L~f)`) & Down(Int cell(GoB f,i2,j2),(L~f)`)=Int cell(GoB f,i2,j2)
                by A3,A4,Th3,PRE_TOPC:18;
A222:           Down(LeftComp f,(L~f)`)=LeftComp f & Down(RightComp f,(
                L~f)`)=RightComp f by Th5;
                Down(Int cell(GoB f,i2,j1),(L~f)`) c= LeftComp f \/
                RightComp f by A1,A2,A6,A7,Th3;
                then Down(Int cell(GoB f,i2,j1),(L~f)`) c= Down(LeftComp f \/
                RightComp f,(L~f)`) by A222,GOBRD11:4;
                then
A223:           Cl Down(Int cell(GoB f,i2,j1),(L~f)`) c= Cl Down(
                LeftComp f \/ RightComp f,(L~f)`) by PRE_TOPC:19;
A224:           0+1<=i2 by A210,NAT_1:13;
                then
A225:           1<i2+1 by NAT_1:13;
                (for x being object st x in P holds not x in (L~f))
implies P misses
                L~f by XBOOLE_0:3;
                then
A226:           p in {p} & {p} c= (L~f)` by A2,A126,A224,A211,A214,NAT_1:13
,SUBSET_1:23,TARSKI:def 1;
                then reconsider p1=p as Point of (TOP-REAL 2)|((L~f)`) by
PRE_TOPC:8;
A227:           1<=1+j2 by NAT_1:11;
                i2<i2+1 by NAT_1:13;
                then
A228:           ((GoB f)*(i2,j2+1))`1 <((GoB f)*(i2+1,j2+1))`1 by A2,A126,A224
,A212,A220,GOBOARD5:3;
                then ((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 XREAL_1:8;
                then
A229:           (((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 XREAL_1:74;
                ((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 A228,XREAL_1:8;
                then
A230:           (((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 XREAL_1:74;
                p in {|[s,r]| where s,r is Real:
                (GoB f)*(i2,j2+1)`1<=s & s<=(GoB f)*(i2+1,
                j2+1) `1 }
                proof
                  p=|[p`1,p`2]| by EUCLID:53;
                  hence thesis by A215,A230,A229;
                end;
                then
A231:           p in v_strip(GoB f,i2) by A2,A126,A224,A211,A227,GOBOARD5:8;
                p`2=1/2*((GoB f)*(i2,j2+1)+(GoB f)*(i2+1,j2+1))`2 by TOPREAL3:4
                  .=1/2*(((GoB f)*(i2,j2+1))`2+((GoB f)*(i2+1,j2+1))`2) by
TOPREAL3:2;
                then
A232:           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 A215,EUCLID:53;
A233:           j2=0 or j2>=0+1 by NAT_1:13;
A234:           now
                  per cases by A2,A126,A233,XXREAL_0:1;
                  case
A235:               j2>=1 & j2+1<width GoB f;
                    then
A236:               j2+1+1<=width GoB f by NAT_1:13;
                    p in {|[s,r]| where s,r is Real:
                    (GoB f)*(1,j2+1)`2<=r & r<=(GoB f)*(1,
                    j2+1+1)`2 }
                    proof
                      j2+1<j2+1+1 by NAT_1:13;
                      then
A237:                 ((GoB f)*(1,j2+1))`2<((GoB f)*(1,j2+1+1))`2 by A216,A220
,A236,GOBOARD5:4;
                      ((GoB f)*(i2,j2+1))`2=((GoB f)*(1,j2+1))`2 & ((GoB
f)*(i2+1,j2+1))`2=((GoB f )*(1,j2+1))`2 by A2,A3,A126,A224,A212,A220,A225,
GOBOARD5:1;
                      hence thesis by A232,A237;
                    end;
                    then p in h_strip(GoB f,j2+1) by A216,A227,A235,GOBOARD5:5;
                    then p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A231,
XBOOLE_0:def 4;
                    then
A238:               p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
A239:               p in {|[s,r]| where s,r is Real:
                    (GoB f)*(1,j2)`2<=r & r<=(GoB f)*(1,j2 +1)`2}
                    proof
                      j2<j2+1 by NAT_1:13;
                      then
A240:                 ((GoB f)*(1,j2))`2<((GoB f)*(1,j2+1))`2 by A216,A235,
GOBOARD5:4;
                      ((GoB f)*(i2,j2+1))`2=((GoB f)*(1,j2+1))`2 & ((GoB
f)*(i2+1,j2+1))`2=((GoB f )*(1,j2+1))`2 by A2,A3,A126,A224,A212,A220,A225,
GOBOARD5:1;
                      hence thesis by A232,A240;
                    end;
                    j2<width GoB f by A235,NAT_1:13;
                    then p in h_strip(GoB f,j2) by A216,A235,A239,GOBOARD5:5;
                    then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) by A231,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j2) 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 A226,A238,XBOOLE_0:def 4;
                  end;
                  case
A241:               j2>=1 & j2+1=width GoB f;
A242:               j2<j2+1 by NAT_1:13;
                    p in {|[s,r]| where s,r is Real:
                    (GoB f)*(1,j2)`2<=r & r<=(GoB f)*(1,j2 +1)`2}
                    proof
A243:                 ((GoB f)*(1,j2))`2<((GoB f)*(1,j2+1))`2 by A216,A241,A242
,GOBOARD5:4;
                      ((GoB f)*(i2,j2+1))`2=((GoB f)*(1,j2+1))`2 & ((GoB
f)*(i2+1,j2+1))`2=((GoB f )*(1,j2+1))`2 by A2,A3,A126,A224,A212,A220,A225,
GOBOARD5:1;
                      hence thesis by A232,A243;
                    end;
                    then p in h_strip(GoB f,j2) by A216,A241,A242,GOBOARD5:5;
                    then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) by A231,
XBOOLE_0:def 4;
                    then
A244:               p in cell(GoB f,i2,j2) by GOBOARD5:def 3;
                    p in {|[s,r]| where s,r is Real:(GoB f)*(1,j2+1)`2<=r}
                    proof
                      ((GoB f)*(i2,j2+1))`2=((GoB f)*(1,j2+1))`2 & ((GoB
f)*(i2+1,j2+1))`2=((GoB f )*(1,j2+1))`2 by A2,A3,A126,A224,A212,A220,A225,
GOBOARD5:1;
                      hence thesis by A232;
                    end;
                    then p in h_strip(GoB f,j2+1) by A216,A241,GOBOARD5:6;
                    then p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A231,
XBOOLE_0:def 4;
                    then 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 A226,A244,XBOOLE_0:def 4;
                  end;
                  case
A245:               j2=0 & j2+1<width GoB f;
                    then
A246:               j2+1+1<=width GoB f by NAT_1:13;
                    p in {|[s,r]| where s,r is Real:
                    (GoB f)*(1,j2+1)`2<=r & r<=(GoB f)*(1,
                    j2+1+1)`2 }
                    proof
                      j2+1<j2+1+1 by NAT_1:13;
                      then
A247:                 ((GoB f)*(1,j2+1))`2<((GoB f)*(1,j2+1+1))`2 by A216,A220
,A246,GOBOARD5:4;
                      ((GoB f)*(i2,j2+1))`2=((GoB f)*(1,j2+1))`2 & ((GoB
f)*(i2+1,j2+1))`2=((GoB f )*(1,j2+1))`2 by A2,A3,A126,A224,A212,A220,A225,
GOBOARD5:1;
                      hence thesis by A232,A247;
                    end;
                    then p in h_strip(GoB f,j1) by A126,A216,A245,GOBOARD5:5;
                    then p in h_strip(GoB f,j2+1)/\ v_strip(GoB f,i2) by A126
,A231,XBOOLE_0:def 4;
                    then
A248:               p in cell(GoB f,i2,j2+1) by GOBOARD5:def 3;
                    p in {|[s,r]| where s,r is Real: r<=(GoB f)*(1,1)`2}
                    proof
                      ((GoB f)*(i2,j2+1))`2=((GoB f)*(1,j2+1))`2 & ((GoB
f)*(i2+1,j2+1))`2=((GoB f )*(1,j2+1))`2 by A2,A3,A126,A224,A212,A220,A225,
GOBOARD5:1;
                      hence thesis by A232,A245;
                    end;
                    then p in h_strip(GoB f,j2) by A216,A245,GOBOARD5:7;
                    then p in h_strip(GoB f,j2)/\ v_strip(GoB f,i2) by A231,
XBOOLE_0:def 4;
                    then p in cell(GoB f,i2,j2) 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 A226,A248,XBOOLE_0:def 4;
                  end;
                  case
                    j2=0 & j2+1=width GoB f;
                    hence contradiction by GOBOARD7:33;
                  end;
                end;
                then p in Cl Down(Int cell(GoB f,i2,j2),(L~f)`) by A3,A4,Th2;
                then
A249:           Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= Component_of p1
                by A3,A4,Th3,GOBRD11:1;
                p in Cl Down(Int cell(GoB f,i2,j1),(L~f)`) by A3,A126,A234,Th2;
                then Component_of p1 c= Down(LeftComp f,(L~f)`) \/ Down(
                RightComp f,(L~f)`) by A223,A219,Th5,CONNSP_3:21;
                then Cl Down(Int cell(GoB f,i2,j2),(L~f)`) c= Down(LeftComp f
                ,(L~f)`) \/ Down(RightComp f,(L~f)`) by A249;
                hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by
A222,A221;
              end;
            end;
            hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f;
          end;
        end;
        hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f;
      end;
    end;
    hence Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f;
  end;
  hence thesis;
end;

theorem Th6:
  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_adjacent 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 that
A1: i1<=len GoB f & j1<=width GoB f and
A2: i2<=len GoB f and
A3: j2<=width GoB f and
A4: i1,j1,i2,j2 are_adjacent;
A5: i1,i2 are_adjacent & j1=j2 or i1=i2 & j1,j2 are_adjacent by A4,
GOBRD10:def 2;
  now
    per cases by A5,GOBRD10:def 1;
    case
      (i2=i1+1 or i1=i2+1)& j1=j2;
      hence thesis by A1,A2,Lm5;
    end;
    case
      i1=i2 &(j2=j1+1 or j1=j2+1);
      hence thesis by A1,A3,Lm6;
    end;
  end;
  hence thesis;
end;

theorem Th7:
  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,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
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;
  consider i1 such that
A4: i1 in dom F1 and
A5: Int cell(GoB f,F1/.i1,F2/.i1) c=LeftComp f \/ RightComp f by A2;
  reconsider kw1=F1/.i1,kw2=F2/.i1 as Element of NAT;
  reconsider k1=kw1+1,k2=kw2+1 as Element of NAT;
  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,PARTFUN1:def 6;
A7: F1/.i1=F1.i1 by A4,PARTFUN1:def 6;
  then kw1<=len GoB f by A3,A4,A6;
  then
A8: k1 <=len GoB f +1 by XREAL_1:6;
  kw2<=width GoB f by A3,A4,A7,A6;
  then
A9: k2<=width GoB f +1 by XREAL_1:6;
A10: k1-'1=F1/.i1 & k2-'1=F2/.i1 by NAT_D:34;
  set n=len GoB f, m=width GoB f;
  defpred P[Nat,Nat,set] means $3 = Int cell(GoB f,$1-'1,$2-'1);
  reconsider F=LeftComp f \/ RightComp f as Subset of REAL 2 by EUCLID:22;
A11: for i,j being Nat st [i,j] in [:Seg ((len (GoB f))+1), Seg ((width (GoB
  f))+1):] ex x being Subset of REAL 2 st P[i,j,x] by Lm2;
  ex Mm being (Matrix of (len (GoB f))+1, (width (GoB f))+1,(bool (REAL 2
  ) )) st for i,j being Nat st [i,j] in Indices Mm holds P[i,j,Mm*(i,j)] from
  MATRIX_0:sch 2(A11);
  then consider
  Mm being (Matrix of (len (GoB f))+1, (width (GoB f))+1,(bool (REAL
  2))) such that
A12: for i,j being Nat st [i,j] in Indices Mm holds Mm*(i,j) = Int cell(
  GoB f,i-'1,j-'1);
A13: len Mm=len GoB f +1 by MATRIX_0:def 2;
  then
A14: dom Mm=Seg (len (GoB f) +1) by FINSEQ_1:def 3;
A15: Seg (width (GoB f) +1)=Seg width Mm by A13,MATRIX_0:20;
A16: width (GoB f) +1=width Mm by A13,MATRIX_0:20;
A17: for i1,j1,i2,j2 being Element of NAT
   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_adjacent holds Mm*(i1,j1)c=LeftComp f \/ RightComp f iff Mm*(i2,j2)c=
  LeftComp f \/ RightComp f
  proof
    let i1,j1,i2,j2 be Element of NAT;
    assume that
A18: i1 in Seg (len GoB f +1) and
A19: i2 in Seg (len GoB f +1) and
A20: j1 in Seg (width GoB f +1) and
A21: j2 in Seg (width GoB f +1) and
A22: i1,j1,i2,j2 are_adjacent;
A23: 1<=i2 by A19,FINSEQ_1:1;
    then 0<=i2-1 by XREAL_1:48;
    then
A24: i2-'1=i2-1 by XREAL_0:def 2;
    [i2,j2] in [:dom Mm,Seg width Mm:] by A14,A15,A19,A21,ZFMISC_1:87;
    then [i2,j2] in Indices Mm by MATRIX_0:def 4;
    then
A25: Mm*(i2,j2)=Int cell(GoB f,i2-'1,j2-'1) by A12;
    reconsider ii1=i1-'1,ii2=i2-'1,jj1=j1-'1,jj2=j2-'1 as Element of NAT;
A26: 1<=i1 by A18,FINSEQ_1:1;
    then 0<=i1-1 by XREAL_1:48;
    then
A27: i1-'1=i1-1 by XREAL_0:def 2;
    [i1,j1] in [:dom Mm,Seg width Mm:] by A14,A16,A18,A20,ZFMISC_1:87;
    then [i1,j1] in Indices Mm by MATRIX_0:def 4;
    then
A28: Mm*(i1,j1)=Int cell(GoB f,i1-'1,j1-'1) by A12;
A29: 1<=j2 by A21,FINSEQ_1:1;
    then 0<=j2-1 by XREAL_1:48;
    then
A30: j2-'1=j2-1 by XREAL_0:def 2;
    i2<=len GoB f +1 by A19,FINSEQ_1:1;
    then
A31: i2-'1<=len GoB f +1-1 by A24,XREAL_1:9;
A32: 1<=j1 by A20,FINSEQ_1:1;
    then 0<=j1-1 by XREAL_1:48;
    then
A33: j1-'1=j1-1 by XREAL_0:def 2;
    j2<=width GoB f +1 by A21,FINSEQ_1:1;
    then
A34: j2-'1<=width GoB f +1-1 by A30,XREAL_1:9;
    j1<=width GoB f +1 by A20,FINSEQ_1:1;
    then
A35: j1-'1<=width GoB f +1-1 by A33,XREAL_1:9;
    i1<=len GoB f +1 by A18,FINSEQ_1:1;
    then
A36: i1-'1<=len GoB f +1-1 by A27,XREAL_1:9;
    ii1,jj1,ii2,jj2 are_adjacent by A22,A26,A23,A32,A29,GOBRD10:4;
    hence thesis by A36,A31,A35,A34,A28,A25,Th6;
  end;
  0+1<=k2 by NAT_1:13;
  then
A37: k2 in Seg(m +1) by A9,FINSEQ_1:1;
  0+1<=k1 by NAT_1:13;
  then
A38: k1 in Seg(n +1) by A8,FINSEQ_1:1;
  then [k1,k2] in [:dom Mm,Seg width Mm:] by A37,A14,A15,ZFMISC_1:87;
  then [k1,k2] in Indices Mm by MATRIX_0:def 4;
  then Mm*(k1,k2) c=LeftComp f \/ RightComp f by A5,A12,A10;
  then
A39: for i,j being Element of NAT
   st i in Seg(n +1) & j in Seg(m +1) holds Mm*(i,j)c=F
    by A38,A37,A17,GOBRD10:8;
  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
A40: i in dom F1;
    reconsider kx1=F1/.i,kx2=F2/.i as Element of NAT;
    reconsider kk1=kx1+1,kk2=kx2+1 as Element of NAT;
    dom F1=Seg len F1 by FINSEQ_1:def 3;
    then dom F1=dom F2 by A1,FINSEQ_1:def 3;
    then
A41: F2/.i=F2.i by A40,PARTFUN1:def 6;
A42: F1/.i=F1.i by A40,PARTFUN1:def 6;
    then kx1<=len GoB f by A3,A40,A41;
    then
A43: kk1<=len GoB f +1 by XREAL_1:6;
    kx2 <=width GoB f by A3,A40,A42,A41;
    then
A44: kk2 <=width GoB f +1 by XREAL_1:6;
    0+1<=kk2 by NAT_1:13;
    then
A45: kk2 in Seg (width GoB f +1) by A44,FINSEQ_1:1;
    0+1<=kk1 by NAT_1:13;
    then
A46: kk1 in Seg (len GoB f +1) by A43,FINSEQ_1:1;
A47: len Mm=len GoB f +1 by MATRIX_0:def 2;
    dom Mm=Seg (len (GoB f) +1) & Seg (width (GoB f) +1)=Seg width Mm
     by A47,FINSEQ_1:def 3,MATRIX_0:20;
    then [kk1,kk2] in [:dom Mm,Seg width Mm:] by A46,A45,ZFMISC_1:87;
    then
A48: [kk1,kk2] in Indices Mm by MATRIX_0:def 4;
A49: kk1-'1=F1/.i & kk2-'1=F2/.i by NAT_D:34;
    Mm*(kk1,kk2)c=LeftComp f \/ RightComp f by A39,A46,A45;
    hence thesis by A12,A49,A48;
  end;
end;

theorem Th8:
  ex i,j st i<=len GoB f & j<=width GoB f & Int cell(GoB f,i,j) c=
  LeftComp f \/ RightComp f
proof
  1+1<=len f by GOBOARD7:34,XXREAL_0:2;
  then
A1: (ex i,j st i <= len GoB f & j <= width GoB f & cell(GoB f,i,j) =
  left_cell( f,1) )& Int left_cell(f,1) c= LeftComp f by GOBOARD9:11,21;
  LeftComp f c= LeftComp f \/ RightComp f by XBOOLE_1:7;
  hence thesis by A1,XBOOLE_1:1;
end;

theorem Th9:
  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;
  set n=len GoB f, m=width GoB f;
  consider i2,j2 such that
A1: i2<=n & j2<=m and
A2: Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f by Th8;
A3: i in NAT & j in NAT & i2 in NAT & j2 in NAT &
    n in NAT & m in NAT by ORDINAL1:def 12;
  assume i<=len GoB f & j<=width GoB f;
  then consider fs1,fs2 being FinSequence of NAT such that
A4: for k,k1,k2 being Element of NAT
   st k in dom fs1 & k1=fs1.k & k2=fs2.k holds k1 <= n & k2 <= m and
A5: fs1.1=i and
A6: fs1.(len fs1)=i2 and
A7: fs2.1=j and
A8: fs2.(len fs2)=j2 and
A9: len fs1=len fs2 and
A10: len fs1=(i-'i2)+(i2-'i)+(j-'j2)+(j2-'j)+1 and
  for k being Element of NAT
  st 1<=k & k<len fs1 holds fs1/.k,fs2/.k,fs1/.(k+1),fs2/.(k+1)
  are_adjacent by A1,GOBRD10:7,A3;
A11: for k,k1,k2 being Nat
   st k in dom fs1 & k1=fs1.k & k2=fs2.k holds k1 <= n & k2 <= m
   proof let k,k1,k2 be Nat;
     k in NAT & k1 in NAT & k2 in NAT by ORDINAL1:def 12;
    hence thesis by A4;
   end;
A12: 1<=1+((i-'i2)+(i2-'i)+(j-'j2)+(j2-'j)) by NAT_1:12;
  then
A13: 1 in dom fs1 by A10,FINSEQ_3:25;
  then
A14: fs1/.1=i by A5,PARTFUN1:def 6;
A15: 1<=1+((i-'i2)+(i2-'i)+(j-'j2)+(j2-'j)) by NAT_1:12;
  then len fs2 in dom fs2 by A9,A10,FINSEQ_3:25;
  then
A16: j2=fs2/.len fs1 by A8,A9,PARTFUN1:def 6;
  1 in dom fs2 by A9,A10,A12,FINSEQ_3:25;
  then
A17: fs2/.1=j by A7,PARTFUN1:def 6;
A18: len fs1 in dom fs1 by A10,A15,FINSEQ_3:25;
  then i2= fs1/.len fs1 by A6,PARTFUN1:def 6;
  hence thesis by A2,A9,A18,A16,A13,A14,A17,Th7,A11;
end;

::$N Jordan Curve Theorem for special polygons
theorem
  (L~f)`=LeftComp f \/ RightComp f
proof
  LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
  then consider B1 being Subset of (TOP-REAL 2)|(L~f)` such that
A1: B1 = LeftComp f and
  B1 is a_component by CONNSP_1:def 6;
  B1 c= the carrier of (TOP-REAL 2)|(L~f)`;
  then
A2: LeftComp f c= (L~f)` by A1,Lm1;
  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
    RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
    then consider B2 being Subset of (TOP-REAL 2)|(L~f)` such that
A3: B2 = RightComp f and
A4: B2 is a_component by CONNSP_1:def 6;
    Cl B2= (Cl RightComp f)/\([#]((TOP-REAL 2)|(L~f)`)) by A3,PRE_TOPC:17;
    then
A5: Cl B2= (Cl RightComp f)/\((L~f)`) by PRE_TOPC:def 5;
    reconsider B2 as Subset of (TOP-REAL 2)|(L~f)`;
    B2 is closed by A4,CONNSP_1:33;
    then
A6: (Cl RightComp f)/\((L~f)`)=RightComp f by A3,A5,PRE_TOPC:22;
    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
A7: B1 = LeftComp f and
A8: B1 is a_component by CONNSP_1:def 6;
    Cl B1= (Cl LeftComp f)/\([#]((TOP-REAL 2)|(L~f)`)) by A7,PRE_TOPC:17;
    then
A9: Cl B1= (Cl LeftComp f)/\((L~f)`) by PRE_TOPC:def 5;
    reconsider B1 as Subset of (TOP-REAL 2)|(L~f)`;
    B1 is closed by A8,CONNSP_1:33;
    then
A10: (Cl (LeftComp f) \/ Cl (RightComp f))/\((L~f)`) = (Cl LeftComp f)/\((
L~f)`) \/ (Cl RightComp f)/\((L~f)`) & (Cl LeftComp f)/\((L~f)`)=LeftComp f by
A7,A9,PRE_TOPC:22,XBOOLE_1:23;
    reconsider Q=(L~f)` as Subset of TOP-REAL 2;
    let x be object;
A11: Cl (LeftComp f \/ RightComp f)= Cl (LeftComp f) \/ Cl(RightComp f) by
PRE_TOPC:20;
    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
A12: 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
A13: y=Cl Down(Int cell(GoB f,i,j),(L~f)`) and
A14: i<=len GoB f & j<=width GoB f by A12;
    Cl (Int cell(GoB f,i,j)) c= Cl (LeftComp f \/ RightComp f) by A14,Th9,
PRE_TOPC:19;
    then
A15: (Cl (Int cell(GoB f,i,j)))/\((L~f)`) c= (Cl (LeftComp f) \/ Cl (
    RightComp f))/\((L~f)`) by A11,XBOOLE_1:26;
    reconsider P=Int cell(GoB f,i,j) as Subset of TOP-REAL 2;
    Cl Down(P,Q) =(Cl (P))/\(Q) by A14,Th1,CONNSP_3:29;
    hence thesis by A12,A13,A15,A10,A6;
  end;
  then
A16: (L~f)`c=LeftComp f \/ RightComp f by Th4;
  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
A17: B1 = RightComp f and
  B1 is a_component by CONNSP_1:def 6;
  B1 c= the carrier of (TOP-REAL 2)|(L~f)`;
  then B1 c= (L~f)` by Lm1;
  then LeftComp f \/ RightComp f c= (L~f)` by A2,A17,XBOOLE_1:8;
  hence thesis by A16,XBOOLE_0:def 10;
end;