The Mizar article:

Some Properties of Special Polygonal Curves

by
Andrzej Trybulec, and
Yatsuka Nakamura

Received October 22, 1998

Copyright (c) 1998 Association of Mizar Users

MML identifier: SPRECT_3
[ MML identifier index ]


environ

 vocabulary BOOLE, ARYTM_1, FINSEQ_1, MATRIX_1, MATRIX_2, PRE_TOPC, EUCLID,
      ARYTM_3, TOPREAL1, METRIC_1, RELAT_2, JORDAN1, CONNSP_1, PCOMPS_1,
      SPPOL_1, MCART_1, GOBOARD1, TREES_1, PSCOMP_1, SPRECT_1, COMPTS_1,
      JORDAN3, RELAT_1, SPPOL_2, FUNCT_1, TARSKI, RFINSEQ, GROUP_2, SEQM_3,
      GOBOARD5, GOBOARD9, SUBSET_1, TOPREAL4, JORDAN5D, GOBOARD2, SPRECT_2,
      ABSVALUE, CARD_1, ORDINAL2, TOPS_1, JORDAN5C, FINSEQ_5, FINSEQ_4, ARYTM;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, XREAL_0,
      REAL_1, NAT_1, ABSVALUE, BINARITH, CARD_1, RFINSEQ, FUNCT_1, FINSEQ_1,
      FINSEQ_4, FINSEQ_5, MATRIX_1, MATRIX_2, STRUCT_0, METRIC_1, PRE_TOPC,
      TOPS_1, COMPTS_1, CONNSP_1, PCOMPS_1, EUCLID, TOPREAL1, TOPREAL4,
      JORDAN1, PSCOMP_1, GOBOARD1, GOBOARD2, SPPOL_1, SPPOL_2, GOBOARD5,
      GOBOARD9, JORDAN3, JORDAN5C, JORDAN5D, SPRECT_1, SPRECT_2;
 constructors SPRECT_2, PSCOMP_1, REALSET1, SPRECT_1, SPPOL_1, COMPTS_1,
      REAL_1, GOBOARD2, BINARITH, JORDAN3, TOPREAL2, TOPREAL4, GOBOARD9,
      CONNSP_1, TOPS_1, JORDAN1, JORDAN5C, TOPS_2, MATRIX_2, ENUMSET1,
      JORDAN5D, ABSVALUE, RFINSEQ, FINSEQ_4, TOPMETR, MEMBERED;
 clusters STRUCT_0, RELSET_1, SPRECT_1, SPRECT_2, EUCLID, SPPOL_2, GOBOARD2,
      XREAL_0, FINSEQ_5, ARYTM_3, MEMBERED, ZFMISC_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, SPRECT_2, JORDAN1, TOPREAL4, GOBOARD1, XBOOLE_0;
 theorems FINSEQ_4, TARSKI, FINSEQ_3, FINSEQ_1, SPRECT_2, GOBOARD7, PSCOMP_1,
      SPRECT_1, TOPREAL3, AXIOMS, REAL_1, REAL_2, SPPOL_2, NAT_1, SPPOL_1,
      EUCLID, ZFMISC_1, TOPREAL1, GOBOARD5, JORDAN5D, FINSEQ_5, AMI_5,
      FINSEQ_6, JORDAN4, JORDAN3, TOPREAL5, TOPS_1, GOBRD11, GOBOARD9, TOPMETR,
      GOBOARD6, JORDAN1, CONNSP_1, SUBSET_1, GOBRD12, JORDAN5C, JORDAN6,
      CQC_THE1, MATRIX_2, SCMFSA_7, GOBOARD1, ENUMSET1, CARD_2, GOBOARD2,
      SQUARE_1, BINARITH, NAT_2, ABSVALUE, GOBOARD8, RLVECT_1, PARTFUN2,
      FUNCT_1, XBOOLE_0, XBOOLE_1, XREAL_0, XCMPLX_1, FINSEQ_2;
 schemes DOMAIN_1;

begin :: Preliminaries

 reserve i,j,k,n,m for Nat;

canceled;

theorem
   for A,B,C,p being set st A c= B & B /\ C = {p} & p in A
  holds A /\ C = {p}
proof
 let A,B,C,p be set such that
A1: A c= B;
 assume
A2: B /\ C = {p};
  then p in B /\ C by TARSKI:def 1;
then A3: p in C by XBOOLE_0:def 3;
 assume p in A;
then A4: p in A /\ C by A3,XBOOLE_0:def 3;
    A /\ C c= { p } by A1,A2,XBOOLE_1:26;
 hence A /\ C = {p} by A4,ZFMISC_1:39;
end;

theorem Th3:
 for q,r,s,t being Real st t >= 0 & t <= 1 &
  s = (1-t)*q + t*r & q <= s & r < s
  holds t = 0
proof let q,r,s,t be Real such that
A1: t >= 0 and
A2: t <= 1 and
A3: s = (1-t)*q + t*r and
A4: q <= s and
A5: r < s;
A6: 1*s = ((1-t) + t)*s by XCMPLX_1:27
    .= (1-t)*s + t*s by XCMPLX_1:8;
 assume t <> 0;
  then A7: t*r < t*s by A1,A5,REAL_1:70;
    1-t >= 0 by A2,SQUARE_1:12;
  then (1-t)*q <= (1-t)*s by A4,AXIOMS:25;
 hence contradiction by A3,A6,A7,REAL_1:67;
end;

theorem Th4:
 for q,r,s,t being Real st t >= 0 & t <= 1 &
  s = (1-t)*q + t*r & q >= s & r > s
  holds t = 0
proof let q,r,s,t be Real such that
A1: t >= 0 and
A2: t <= 1 and
A3: s = (1-t)*q + t*r and
A4: q >= s and
A5: r > s;
A6: 1*s = ((1-t) + t)*s by XCMPLX_1:27
      .= (1-t)*s + t*s by XCMPLX_1:8;
 assume t <> 0;
  then A7: t*r > t*s by A1,A5,REAL_1:70;
    1-t >= 0 by A2,SQUARE_1:12;
  then (1-t)*q >= (1-t)*s by A4,AXIOMS:25;
 hence contradiction by A3,A6,A7,REAL_1:67;
end;

theorem Th5:
 i-'k <= j implies i <= j + k
proof assume
A1: i-'k <= j;
 per cases;
 suppose
A2: i >= k;
    i-'k +k <= j + k by A1,AXIOMS:24;
 hence i <= j + k by A2,AMI_5:4;
 suppose
A3: i <= k;
    k <= j + k by NAT_1:29;
 hence i <= j + k by A3,AXIOMS:22;
end;

theorem Th6:
 i <= j + k implies i-'k <= j
proof assume i <= j + k;
  then i -' k <= j + k -' k by JORDAN3:5;
 hence i-'k <= j by BINARITH:39;
end;

theorem Th7:
 i <= j -' k & k <= j implies i + k <= j
proof assume that
A1: i <= j -' k and
A2: j >= k;
    i + k <= j -' k + k by A1,AXIOMS:24;
 hence i + k <= j by A2,AMI_5:4;
end;

theorem
   j + k <= i implies k <= i -' j
proof assume
A1: j + k <= i;
 per cases by A1,AXIOMS:21;
 suppose j + k = i;
 hence k <= i -' j by BINARITH:39;
 suppose j + k < i;
 hence k <= i -' j by Th5;
end;

theorem
   k <= i & i < j implies i -' k < j -' k
proof assume that
A1: k <= i and
A2: i < j;
A3: k <= j by A1,A2,AXIOMS:22;
    i -' k + k = i by A1,AMI_5:4;
  then i -' k + k < j -' k + k by A2,A3,AMI_5:4;
 hence i -' k < j -' k by AXIOMS:24;
end;

theorem
   i < j & k < j implies i -' k < j -' k
proof assume that
A1: i < j and
A2: k < j;
 per cases;
 suppose k <= i;
then A3: i -' k = i - k by SCMFSA_7:3;
    j -' k = j - k by A2,SCMFSA_7:3;
 hence thesis by A1,A3,REAL_1:54;
 suppose k > i;
  then i - k < 0 by REAL_2:105;
  then A4: i -' k = 0 by BINARITH:def 3;
    j -' k <> 0 by A2,JORDAN4:1;
 hence thesis by A4,NAT_1:19;
end;

theorem
   for D being non empty set
 for f being non empty FinSequence of D, g being FinSequence of D
 holds (g^f)/.len(g^f) = f/.len f
proof
 let D be non empty set,
     f be non empty FinSequence of D, g be FinSequence of D;
A1: len(g^f) = len g + len f by FINSEQ_1:35;
    len f <> 0 by FINSEQ_1:25;
  then len f >= 1 by RLVECT_1:99;
 hence thesis by A1,GOBOARD2:5;
end;

theorem Th12:
 for a,b,c,d being set holds
  Indices (a,b)][(c,d) = {[1,1],[1,2],[2,1],[2,2]}
proof let a,b,c,d be set;
 thus Indices (a,b)][(c,d) = [:Seg 2,Seg 2:] by MATRIX_2:3
          .= [:{1},Seg 2:] \/ [:{2},Seg 2:] by FINSEQ_1:4,ZFMISC_1:132
          .= [:{1},Seg 2:] \/ {[2,1], [2,2]} by FINSEQ_1:4,ZFMISC_1:36
          .= { [1,1], [1,2]} \/ {[2,1], [2,2]} by FINSEQ_1:4,ZFMISC_1:36
          .= {[1,1],[1,2],[2,1],[2,2]} by ENUMSET1:45;
end;

begin :: Euclidean Space

theorem Th13:
 for p,q being Point of TOP-REAL n, r being Real
   st 0 < r & p = (1-r)*p+r*q
  holds p = q
proof
 let p,q be Point of TOP-REAL n, r be Real such that
A1: 0 < r and
A2: p = (1-r)*p+r*q;
A3: (1-r)*p+r*p = ((1-r)+r)*p by EUCLID:37
        .= 1*p by XCMPLX_1:27
        .= p by EUCLID:33;
    r*p = r*p + 0.REAL n by EUCLID:31
     .= r*p + ((1-r)*p + -(1-r)*p) by EUCLID:40
     .= r*q + (1-r)*p + -(1-r)*p by A2,A3,EUCLID:30
     .= r*q + ((1-r)*p + -(1-r)*p) by EUCLID:30
     .= r*q + 0.REAL n by EUCLID:40
     .= r*q by EUCLID:31;
 hence p = q by A1,EUCLID:38;
end;

theorem Th14:
 for p,q being Point of TOP-REAL n, r being Real
   st r < 1 & p = (1-r)*q+r*p
  holds p = q
proof let p,q be Point of TOP-REAL n, r be Real such that
A1: r < 1 and
A2: p = (1-r)*q+r*p;
   set s = 1 -r;
      r + 0 < 1 by A1;
then A3: 0 < 1 - r by REAL_1:86;
     p = (1-s)*p+s*q by A2,XCMPLX_1:18;
 hence p = q by A3,Th13;
end;

theorem
   for p,q being Point of TOP-REAL n st p = 1/2*(p+q)
  holds p = q
proof let p,q be Point of TOP-REAL n;
  assume p = 1/2*(p+q);
  then p = (1 - 1/2)*p + 1/2*q by EUCLID:36;
 hence p = q by Th13;
end;

theorem Th16:
 for p,q,r being Point of TOP-REAL n st
  q in LSeg(p,r) & r in LSeg(p,q) holds q = r
proof let p,q,r be Point of TOP-REAL n;
 assume q in LSeg(p,r);
  then consider r1 being Real such that
A1: 0<=r1 and
A2: r1<=1 and
A3: q = (1-r1)*p+r1*r by SPPOL_1:21;
 assume r in LSeg(p,q);
  then consider r2 being Real such that
A4: 0<=r2 and
A5: r2<=1 and
A6: r = (1-r2)*p+r2*q by SPPOL_1:21;
A7:  (1-r1)+r1*(1-r2) = (1-r1)+(r1*1-r1*r2) by XCMPLX_1:40
           .= (1-r1)+r1-r1*r2 by XCMPLX_1:29
           .= 1 - r1*r2 by XCMPLX_1:27;
A8:  (1-r2)+r2*(1-r1) = (1-r2)+(r2*1-r2*r1) by XCMPLX_1:40
           .= (1-r2)+r2-r2*r1 by XCMPLX_1:29
           .= 1 - r2*r1 by XCMPLX_1:27;
A9:  q = (1-r1)*p+(r1*((1-r2)*p)+r1*(r2*q)) by A3,A6,EUCLID:36
       .= (1-r1)*p+r1*((1-r2)*p)+r1*(r2*q) by EUCLID:30
       .= (1-r1)*p+r1*(1-r2)*p+r1*(r2*q) by EUCLID:34
       .= (1 - r1*r2)*p+r1*(r2*q) by A7,EUCLID:37
       .= (1 - r1*r2)*p+r1*r2*q by EUCLID:34;
A10:  r = (1-r2)*p+(r2*((1-r1)*p)+r2*(r1*r)) by A3,A6,EUCLID:36
       .= (1-r2)*p+r2*((1-r1)*p)+r2*(r1*r) by EUCLID:30
       .= (1-r2)*p+r2*(1-r1)*p+r2*(r1*r) by EUCLID:34
       .= (1 - r2*r1)*p+r2*(r1*r) by A8,EUCLID:37
       .= (1 - r2*r1)*p+r2*r1*r by EUCLID:34;
A11: r1*r2 <= 1 by A1,A2,A4,A5,REAL_2:140;
  per cases by A11,REAL_1:def 5;
  suppose
A12:   r1*r2 = 1;
   then 1 <= r1 or 1 <= r2 by A1,A4,REAL_2:139;
   then 1*r1 = 1 or 1*r2 = 1 by A2,A5,AXIOMS:21;
  hence q = 0 * p+r by A3,A12,EUCLID:33
         .= 0.REAL n+r by EUCLID:33
         .= r by EUCLID:31;
  suppose
A13: r1*r2 < 1;
  hence q = p by A9,Th14
     .= r by A10,A13,Th14;
end;

begin :: Euclidean Plane

theorem Th17:
 for A being non empty Subset of TOP-REAL 2,
     p being Element of Euclid 2, r being Real st A = Ball(p,r)
 holds A is connected
proof
 let A be non empty Subset of TOP-REAL 2,
     p be Element of Euclid 2, r be Real such that
A1: A = Ball(p,r);
    A is convex
   proof let w1,w2 be Point of TOP-REAL 2;
    assume w1 in A & w2 in A;
    hence LSeg(w1,w2) c= A by A1,TOPREAL3:28;
   end;
 hence A is connected by JORDAN1:9;
end;

theorem Th18:
 for A, B being Subset of TOP-REAL 2 st
  A is open & B is_a_component_of A
 holds B is open
proof let A, B be Subset of TOP-REAL 2 such that
A1: A is open and
A2: B is_a_component_of A;
A3: B c= A by A2,SPRECT_1:7;
A4: TOP-REAL 2 = TopSpaceMetr (Euclid 2) by EUCLID:def 8;
   reconsider C = B, D = A
    as Subset of TopSpaceMetr Euclid 2 by EUCLID:def 8;
    for p being Point of Euclid 2 st p in C
   ex r being real number st r>0 & Ball(p,r) c= C
  proof let p be Point of Euclid 2; assume
A5:  p in C;
    then consider r being real number such that
A6:  r > 0 and
A7:  Ball(p,r) c= D by A1,A3,A4,TOPMETR:22;
   reconsider r as Real by XREAL_0:def 1;
   take r;
   thus r>0 by A6;
      the carrier of TopSpaceMetr Euclid 2 = the carrier of Euclid 2
       by TOPMETR:16;
    then reconsider E = Ball(p,r) as Subset of TOP-REAL 2 by A4;
A8: p in E by A6,GOBOARD6:4;
then A9: B meets E by A5,XBOOLE_0:3;
      E is connected by A8,Th17;
   hence Ball(p,r) c= C by A2,A7,A9,GOBOARD9:6;
  end;
 hence B is open by A4,TOPMETR:22;
end;

theorem Th19:
 for p,q,r being Point of TOP-REAL 2
  st LSeg(p,q) is horizontal & r in LSeg(p,q)
 holds p`2 = r`2
proof let p,q,r be Point of TOP-REAL 2;
 assume LSeg(p,q) is horizontal;
then A1: p`2 = q`2 by SPPOL_1:36;
 assume r in LSeg(p,q);
  then consider t being Real such that
     0 <= t & t <= 1 and
A2: r = (1-t)*p+t*q by SPPOL_1:21;
 thus p`2 = 1*p`2
        .= (1-t+t)*p`2 by XCMPLX_1:27
        .= (1-t)*p`2+t*p`2 by XCMPLX_1:8
        .= ((1-t)*p)`2+t*q`2 by A1,TOPREAL3:9
        .= ((1-t)*p)`2+(t*q)`2 by TOPREAL3:9
        .= r`2 by A2,TOPREAL3:7;
end;

theorem Th20:
 for p,q,r being Point of TOP-REAL 2
  st LSeg(p,q) is vertical & r in LSeg(p,q)
 holds p`1 = r`1
proof let p,q,r be Point of TOP-REAL 2;
 assume LSeg(p,q) is vertical;
then A1: p`1 = q`1 by SPPOL_1:37;
 assume r in LSeg(p,q);
  then consider t being Real such that
     0 <= t & t <= 1 and
A2: r = (1-t)*p+t*q by SPPOL_1:21;
 thus p`1 = 1*p`1
        .= (1-t+t)*p`1 by XCMPLX_1:27
        .= (1-t)*p`1+t*p`1 by XCMPLX_1:8
        .= ((1-t)*p)`1+t*q`1 by A1,TOPREAL3:9
        .= ((1-t)*p)`1+(t*q)`1 by TOPREAL3:9
        .= r`1 by A2,TOPREAL3:7;
end;

theorem
   for p,q,r,s being Point of TOP-REAL 2
  st LSeg(p,q) is horizontal & LSeg(r,s) is horizontal &
   LSeg(p,q) meets LSeg(r,s)
 holds p`2= r`2
proof
 let p,q,r,s be Point of TOP-REAL 2 such that
A1: LSeg(p,q) is horizontal and
A2: LSeg(r,s) is horizontal;
 assume LSeg(p,q) meets LSeg(r,s);
  then LSeg(p,q) /\ LSeg(r,s) <> {} by XBOOLE_0:def 7;
  then consider x being Point of TOP-REAL 2 such that
A3: x in LSeg(p,q) /\ LSeg(r,s) by SUBSET_1:10;
A4: x in LSeg(r,s) by A3,XBOOLE_0:def 3;
     x in LSeg(p,q) by A3,XBOOLE_0:def 3;
 hence p`2 = x`2 by A1,Th19
        .= r`2 by A2,A4,Th19;
end;

theorem
   for p,q,r being Point of TOP-REAL 2
  st LSeg(p,q) is vertical & LSeg(q,r) is horizontal
 holds LSeg(p,q) /\ LSeg(q,r) = {q}
proof let p,q,r be Point of TOP-REAL 2 such that
A1: LSeg(p,q) is vertical and
A2: LSeg(q,r) is horizontal;
    for x being set holds x in LSeg(p,q) /\ LSeg(q,r) iff x = q
   proof let x be set;
    thus x in LSeg(p,q) /\ LSeg(q,r) implies x = q
     proof assume
A3:     x in LSeg(p,q) /\ LSeg(q,r);
       then reconsider x as Point of TOP-REAL 2;
         x in LSeg(p,q) & x in LSeg(q,r) by A3,XBOOLE_0:def 3;
       then x`1 = q`1 & x`2 = q`2 by A1,A2,Th19,Th20;
      hence thesis by TOPREAL3:11;
     end;
    assume x = q;
     then x in LSeg(p,q) & x in LSeg(q,r) by TOPREAL1:6;
    hence thesis by XBOOLE_0:def 3;
   end;
 hence LSeg(p,q) /\ LSeg(q,r) = {q} by TARSKI:def 1;
end;

theorem
   for p,q,r,s being Point of TOP-REAL 2
  st LSeg(p,q) is horizontal & LSeg(s,r) is vertical & r in LSeg(p,q)
 holds LSeg(p,q) /\ LSeg(s,r) = {r}
proof let p,q,r,s be Point of TOP-REAL 2 such that
A1: LSeg(p,q) is horizontal and
A2: LSeg(s,r) is vertical and
A3: r in LSeg(p,q);
    for x being set holds x in LSeg(p,q) /\ LSeg(s,r) iff x = r
   proof let x be set;
    thus x in LSeg(p,q) /\ LSeg(s,r) implies x = r
     proof assume
A4:     x in LSeg(p,q) /\ LSeg(s,r);
       then reconsider x as Point of TOP-REAL 2;
A5:     p`2 = r`2 by A1,A3,Th19;
         x in LSeg(p,q) & x in LSeg(s,r) by A4,XBOOLE_0:def 3;
       then x`2 = p`2 & x`1 = r`1 by A1,A2,Th19,Th20;
      hence thesis by A5,TOPREAL3:11;
     end;
    assume x = r;
     then x in LSeg(p,q) & x in LSeg(s,r) by A3,TOPREAL1:6;
    hence thesis by XBOOLE_0:def 3;
   end;
 hence LSeg(p,q) /\ LSeg(s,r) = {r} by TARSKI:def 1;
end;

begin :: Main

reserve p,q for Point of TOP-REAL 2;
reserve G for Go-board;

theorem
   1 <= j & j <= k & k <= width G & 1 <= i & i <= len G
 implies G*(i,j)`2 <= G*(i,k)`2
proof
 assume
A1: 1 <= j & j <= k & k <= width G & 1 <= i & i <= len G;
 per cases by A1,REAL_1:def 5;
 suppose j < k;
 hence G*(i,j)`2 <= G*(i,k)`2 by A1,GOBOARD5:5;
 suppose j = k;
 hence thesis;
end;

theorem
   1 <= j & j <= width G & 1 <= i & i <= k & k <= len G
 implies G*(i,j)`1 <= G*(k,j)`1
proof assume
A1: 1 <= j & j <= width G & 1 <= i & i <= k & k <= len G;
 per cases by A1,REAL_1:def 5;
 suppose i < k;
 hence G*(i,j)`1 <= G*(k,j)`1 by A1,GOBOARD5:4;
 suppose i = k;
 hence thesis;
end;

reserve C for Subset of TOP-REAL 2;

theorem Th26:
 LSeg(NW-corner C,NE-corner C) c= L~SpStSeq C
proof
A1: LSeg(NW-corner C,NE-corner C) c=
  LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C) by XBOOLE_1:7;
   LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C) c=
  (LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C)) \/
  (LSeg(SE-corner C,SW-corner C) \/ LSeg(SW-corner C,NW-corner C)) by XBOOLE_1:
7;
 then LSeg(NW-corner C,NE-corner C) c=
  (LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C)) \/
  (LSeg(SE-corner C,SW-corner C) \/ LSeg(SW-corner C,NW-corner C))
     by A1,XBOOLE_1:1;
 hence thesis by SPRECT_1:43;
end;

theorem Th27:
 N-most C c= LSeg(NW-corner C,NE-corner C)
proof
    N-most C = LSeg(NW-corner C, NE-corner C) /\ C by PSCOMP_1:def 39;
 hence N-most C c= LSeg(NW-corner C,NE-corner C) by XBOOLE_1:17;
end;

theorem Th28:
 for C being non empty compact Subset of TOP-REAL 2
  holds N-min C in LSeg(NW-corner C,NE-corner C)
proof let C be non empty compact Subset of TOP-REAL 2;
A1: N-min C in N-most C by PSCOMP_1:101;
     N-most C c= LSeg(NW-corner C,NE-corner C) by Th27;
 hence N-min C in LSeg(NW-corner C,NE-corner C) by A1;
end;

theorem
   LSeg(NW-corner C,NE-corner C) is horizontal
proof
    (NW-corner C)`2 = N-bound C by PSCOMP_1:75
         .= (NE-corner C)`2 by PSCOMP_1:77;
 hence LSeg(NW-corner C,NE-corner C) is horizontal by SPPOL_1:36;
end;

canceled;

theorem :: JORDAN3:76
  for g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st
  g/.1 <> p & ((g/.1)`1 = p`1 or (g/.1)`2 = p`2) &
    g is_S-Seq & LSeg(p,g/.1) /\ L~g={ g/.1 }
 holds <*p*>^g is_S-Seq
proof let g be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2 such that
A1: g/.1 <> p and
A2: (g/.1)`1 = p`1 or (g/.1)`2 = p`2 and
A3: g is_S-Seq and
A4: LSeg(p,g/.1) /\ L~g={ g/.1 };
  set f = <*p,g/.1*>;
  reconsider g' = g as S-Sequence_in_R2 by A3;
A5: 1 in dom g' by FINSEQ_5:6;
A6: len f = 1+1 by FINSEQ_1:61;
then A7: len f -' 1 = 1 by BINARITH:39;
A8: f.len f = g/.1 by A6,FINSEQ_1:61
        .= g.1 by A5,FINSEQ_4:def 4;
A9: f is_S-Seq by A1,A2,SPPOL_2:46;
A10:  L~f /\ L~g ={ g/.1 } by A4,SPPOL_2:21
        .={g.1} by A5,FINSEQ_4:def 4;
    mid(f,1,len f-'1) = <*f/.1*> by A6,A7,JORDAN4:27
       .= <*p*> by FINSEQ_4:26;
 hence <*p*>^g is_S-Seq by A3,A8,A9,A10,JORDAN3:80;
end;

canceled;

theorem
   for f being S-Sequence_in_R2, p being Point of TOP-REAL 2 st
   1 <j & j <= len f & p in L~mid(f,1,j)
  holds LE p, f/.j, L~f, f/.1, f/.len f
proof
 let f be S-Sequence_in_R2, p be Point of TOP-REAL 2 such that
A1: 1 <j & j <= len f and
A2: p in L~mid(f,1,j);
A3: L~f is_an_arc_of f/.1,f/.len f by TOPREAL1:31;
  consider i such that
A4: 1 <= i & i+1 <= len mid(f,1,j) and
A5: p in LSeg(mid(f,1,j),i) by A2,SPPOL_2:13;
A6: j -' 1 + 1 = j by A1,AMI_5:4;
then A7: i+1 <= j by A1,A4,JORDAN4:20;
A8: i = i + 1 -' 1 by BINARITH:39;
     i < j-'1+1 by A6,A7,NAT_1:38;
then A9:  LSeg(mid(f,1,j),i) = LSeg(f,i+1-'1) by A1,A4,JORDAN4:31;
    i+1 <= len f by A1,A7,AXIOMS:22;
  then A10:  LE p, f/.(i+1), L~f, f/.1, f/.len f by A4,A5,A8,A9,JORDAN5C:26;
     1 <= i+1 by NAT_1:29;
  then LE f/.(i+1), f/.j, L~f, f/.1, f/.len f by A1,A7,JORDAN5C:24;
 hence LE p, f/.j, L~f, f/.1, f/.len f by A3,A10,JORDAN5C:13;
end;

theorem :: JORDAN4:47
  for h being FinSequence of TOP-REAL 2 st
 i in dom h & j in dom h holds L~mid(h,i,j) c= L~h
proof let h be FinSequence of TOP-REAL 2;
 assume i in dom h & j in dom h;
  then 1 <= i & i <= len h & 1 <= j & j <= len h by FINSEQ_3:27;
 hence thesis by JORDAN4:47;
end;

theorem
   1 <= i & i < j implies
  for f being FinSequence of TOP-REAL 2 st j <= len f holds
   L~mid(f,i,j) = LSeg(f,i) \/ L~mid(f,i+1,j)
proof assume that
A1: 1 <= i and
A2: i < j;
 let f be FinSequence of TOP-REAL 2 such that
A3: j <= len f;
A4: 1 <= i+1 by NAT_1:29;
A5: i+1 <= j by A2,NAT_1:38;
   set A = { LSeg(f,k): i <= k & k < j},
       B = { LSeg(f,k): i+1 <= k & k < j};
A6:  A = B \/ {LSeg(f,i)}
   proof
    thus A c= B \/ {LSeg(f,i)}
     proof let e be set;
      assume e in A;
       then consider k such that
A7:     e = LSeg(f,k) and
A8:     i <= k and
A9:     k < j;
         i = k or i < k by A8,AXIOMS:21;
       then i = k or i+1 <= k by NAT_1:38;
       then e in B or e in {LSeg(f,i)} by A7,A9,TARSKI:def 1;
      hence e in B \/ {LSeg(f,i)} by XBOOLE_0:def 2;
     end;
    let e be set;
    assume
A10:    e in B \/ {LSeg(f,i)};
     per cases by A10,XBOOLE_0:def 2;
     suppose e in B;
       then consider k such that
A11:     e = LSeg(f,k) and
A12:     i+1 <= k and
A13:     k < j;
       i < k by A12,NAT_1:38;
    hence e in A by A11,A13;
     suppose e in {LSeg(f,i)};
      then e = LSeg(f,i) by TARSKI:def 1;
    hence e in A by A2;
   end;
 thus L~mid(f,i,j) = union A by A1,A2,A3,SPRECT_2:18
     .= union B \/ union{LSeg(f,i)} by A6,ZFMISC_1:96
     .= union B \/ LSeg(f,i) by ZFMISC_1:31
     .= LSeg(f,i) \/ L~mid(f,i+1,j) by A3,A4,A5,SPRECT_2:18;
end;

theorem
    for f being FinSequence of TOP-REAL 2 st 1 <= i holds
    i < j & j <= len f implies
   L~mid(f,i,j) = L~mid(f,i,j -' 1) \/ LSeg(f,j -' 1)
proof
 let f be FinSequence of TOP-REAL 2 such that
A1: 1 <= i and
A2: i < j and
A3: j <= len f;
A4: i <= j -' 1 by A2,JORDAN3:12;
      j -' 1 <= j by GOBOARD9:2;
then A5: j -' 1 <= len f by A3,AXIOMS:22;
   set A = { LSeg(f,k): i <= k & k < j},
       B = { LSeg(f,k): i <= k & k < j -' 1};
A6:  A = B \/ {LSeg(f,j -' 1)}
   proof
    thus A c= B \/ {LSeg(f,j -' 1)}
     proof let e be set;
      assume e in A;
       then consider k such that
A7:     e = LSeg(f,k) and
A8:     i <= k and
A9:     k < j;
         k <= j -' 1 by A9,JORDAN3:12;
       then j -' 1 = k or k < j -' 1 by AXIOMS:21;
       then e in B or e in {LSeg(f,j -' 1)} by A7,A8,TARSKI:def 1;
      hence e in B \/ {LSeg(f,j -' 1)} by XBOOLE_0:def 2;
     end;
    let e be set;
    assume
A10:    e in B \/ {LSeg(f,j -' 1)};
A11:  j -' 1 <= j by GOBOARD9:2;
     per cases by A10,XBOOLE_0:def 2;
     suppose e in B;
       then consider k such that
A12:     e = LSeg(f,k) and
A13:     i <= k and
A14:     k < j -' 1;
       k < j by A11,A14,AXIOMS:22;
    hence e in A by A12,A13;
     suppose e in {LSeg(f,j -' 1)};
      then A15:    e = LSeg(f,j -' 1) by TARSKI:def 1;
       1 <= j & 1 <= j -' 1 by A1,A2,A4,AXIOMS:22;
     then j-' 1 < j by JORDAN3:14;
    hence e in A by A4,A15;
   end;
 thus L~mid(f,i,j) = union A by A1,A2,A3,SPRECT_2:18
     .= union B \/ union{LSeg(f,j -' 1)} by A6,ZFMISC_1:96
     .= union B \/ LSeg(f,j -' 1) by ZFMISC_1:31
     .= L~mid(f,i,j -' 1) \/ LSeg(f,j -' 1) by A1,A4,A5,SPRECT_2:18;
end;

canceled;

theorem
  for f, g being FinSequence of TOP-REAL 2 st f is_S-Seq & g is_S-Seq &
  ((f/.len f)`1 = (g/.1)`1 or (f/.len f)`2 = (g/.1)`2) &
   L~f misses L~g &
   LSeg(f/.len f,g/.1) /\ L~f={ f/.len f } &
   LSeg(f/.len f,g/.1) /\ L~g={ g/.1 }
 holds f^g is_S-Seq
proof let f,g be FinSequence of TOP-REAL 2 such that
A1: f is_S-Seq and
A2: g is_S-Seq and
A3: (f/.len f)`1 = (g/.1)`1 or (f/.len f)`2 = (g/.1)`2 and
A4: L~f misses L~g and
A5: LSeg(f/.len f,g/.1) /\ L~f={ f/.len f } and
A6: LSeg(f/.len f,g/.1) /\ L~g={ g/.1 };
   set h = <*f/.len f*>^g;
A7: len f >= 2 by A1,TOPREAL1:def 10;
A8: len g >= 2 by A2,TOPREAL1:def 10;
      1 <= len f by A7,AXIOMS:22;
then A9: len f in dom f by FINSEQ_3:27;
A10: len g >= 1 by A8,AXIOMS:22;
then A11: 1 in dom g by FINSEQ_3:27;
A12: len h = len<*f/.len f*>+len g by FINSEQ_1:35
       .= len g + 1 by FINSEQ_1:56;
then A13: len h >= 1+1 by A10,AXIOMS:24;
      len g <> 0 by A2,TOPREAL1:def 10;
then A14: g is non empty by FINSEQ_1:25;
A15: f.len f = f/.len f by A9,FINSEQ_4:def 4
       .=h.1 by FINSEQ_1:58;
   f/.len f in L~f & g/.1 in L~g by A7,A8,A9,A11,GOBOARD1:16;
 then f/.len f <> g/.1 by A4,XBOOLE_0:3;
then A16: h is_S-Seq by A2,A3,A6,SPRECT_2:64;
A17: L~f /\ L~h = L~f /\ (LSeg(f/.len f,g/.1) \/ L~g) by A14,SPPOL_2:20
         .= L~f /\ LSeg(f/.len f,g/.1) \/ L~f /\ L~g by XBOOLE_1:23
         .= L~f /\ LSeg(f/.len f,g/.1) \/ {} by A4,XBOOLE_0:def 7
         .={h.1} by A5,A9,A15,FINSEQ_4:def 4;
    mid(h,2,len h) = (h/^(1+1-'1))|(len h-'2+1) by A13,JORDAN3:def 1
        .= (h/^1)|(len h-'2+1) by BINARITH:39
        .= g|(len h-'2+1) by FINSEQ_6:49
        .= g|(len h-'1-'1+1) by JORDAN3:8
        .= g|(len g-'1+1) by A12,BINARITH:39
        .= g|len g by A10,AMI_5:4
        .= g by TOPREAL1:2;
 hence f^g is_S-Seq by A1,A15,A16,A17,JORDAN3:73;
end;

theorem
   for f being S-Sequence_in_R2, p being Point of TOP-REAL 2 st p in L~f
holds (R_Cut(f,p))/.1 = f/.1
proof let f be S-Sequence_in_R2, p be Point of TOP-REAL 2;
  set i = Index(p,f);
 assume
A1: p in L~f;
 then A2: 1 <= i & i <= len f by JORDAN3:41;
A3: 1 in dom f by FINSEQ_5:6;
    p = f.1 or p <> f.1;
  then len R_Cut(f,p) = Index(p,f) or len R_Cut(f,p) = Index(p,f) + 1
               by A1,JORDAN3:60;
  then 1 <= len R_Cut(f,p) by A1,JORDAN3:41,NAT_1:29;
 hence (R_Cut(f,p))/.1 = R_Cut(f,p).1 by FINSEQ_4:24
      .= f.1 by A1,A2,JORDAN3:59
      .= f/.1 by A3,FINSEQ_4:def 4;
end;

theorem
   for f being S-Sequence_in_R2, p,q being Point of TOP-REAL 2 st
   1 <=j & j < len f & p in LSeg(f,j) & q in LSeg(f/.j,p)
  holds LE q, p, L~f, f/.1, f/.len f
proof let f be S-Sequence_in_R2, p,q be Point of TOP-REAL 2 such that
A1: 1 <=j & j < len f and
A2: p in LSeg(f,j) and
A3: q in LSeg(f/.j,p);
A4: L~f is_an_arc_of f/.1, f/.len f by TOPREAL1:31;
A5: j+1 <= len f by A1,NAT_1:38;
then A6: LSeg(f,j) = LSeg(f/.j,f/.(j+1)) by A1,TOPREAL1:def 5;
      f/.j in LSeg(f,j) by A1,A5,TOPREAL1:27;
    then A7:   LSeg(f/.j,p) c= LSeg(f,j) by A2,A6,TOPREAL1:12;
then A8: q in LSeg(f,j) by A3;
A9: LSeg(f,j) c= L~f by TOPREAL3:26;
  per cases;
  suppose p = q;
   hence thesis by A2,A4,A9,JORDAN5C:9;
  suppose
A10: q <> p;
   for i, j being Nat st q in LSeg(f,i) & p in LSeg(f,j)
  & 1 <= i & i+1 <= len f
  & 1 <= j & j+1 <= len f holds
       i <= j & (i = j implies LE q,p,f/.i,f/.(i+1))
  proof let i1, i2 be Nat such that
A11: q in LSeg(f,i1) and
A12: p in LSeg(f,i2) and
A13: 1 <= i1 & i1+1 <= len f and
A14: 1 <= i2 & i2+1 <= len f;
A15: now assume i2 + 1 > j & j+1 > i2;
      then i2 <= j & j <= i2 by NAT_1:38;
     hence i2 = j by AXIOMS:21;
    end;
A16: p in LSeg(f,i2) /\ LSeg(f,j) by A2,A12,XBOOLE_0:def 3;
    then LSeg(f,i2) meets LSeg(f,j) by XBOOLE_0:4;
    then i2 + 1 >= j & j + 1 >= i2 by TOPREAL1:def 9;
    then A17:   i2 + 1 = j or i2 = j or j + 1 = i2 by A15,AXIOMS:21;
A18: now assume
A19:   i2 + 1 = j;
        i2+(1+1) = i2+1+1 by XCMPLX_1:1;
      then i2+2 <= len f by A1,A19,NAT_1:38;
      then p in {f/.j} by A14,A16,A19,TOPREAL1:def 8;
      then p = f/.j by TARSKI:def 1;
      then q in {p} by A3,TOPREAL1:7;
     hence contradiction by A10,TARSKI:def 1;
    end;
then A20: i2 >= j by A17,NAT_1:29;
A21: now assume i1 + 1 > j & j+1 > i1;
      then i1 <= j & j <= i1 by NAT_1:38;
     hence i1 = j by AXIOMS:21;
    end;
A22: q in LSeg(f,i1) /\ LSeg(f,j) by A3,A7,A11,XBOOLE_0:def 3;
    then LSeg(f,i1) meets LSeg(f,j) by XBOOLE_0:4;
then A23: i1 + 1 >= j & j + 1 >= i1 by TOPREAL1:def 9;
then A24: i1 + 1 = j or i1 = j or j + 1 = i1 by A21,AXIOMS:21;
      1 <= j+1 by NAT_1:29;
then A25: j+1 in dom f by A5,FINSEQ_3:27;
A26: j in dom f by A1,FINSEQ_3:27;
A27:now assume f/.(j+1)=f/.j;
      then j = j+1 by A25,A26,PARTFUN2:17;
     hence contradiction by REAL_1:69;
    end;
A28: now assume
A29:   i1 = j + 1;
        j+(1+1) = j+1+1 by XCMPLX_1:1;
      then q in {f/.(j+1)} by A1,A13,A22,A29,TOPREAL1:def 8;
      then q = f/.(j+1) by TARSKI:def 1;
     hence contradiction by A3,A6,A7,A10,A27,SPPOL_1:24;
    end;
    then i1 <= j by A24,NAT_1:29;
    hence i1 <= i2 by A20,AXIOMS:22;
    assume
A30:   i1 = i2;
       not p in LSeg(f/.j,q) by A3,A10,Th16;
     then not LE p,q,f/.j,f/.(j+1) by JORDAN3:65;
     then LT q,p,f/.j,f/.(j+1)
       by A2,A6,A11,A18,A21,A23,A27,A28,A30,AXIOMS:21,JORDAN3:63;
    hence LE q,p,f/.i1,f/.(i1+1)
     by A18,A21,A23,A28,A30,AXIOMS:21,JORDAN3:def 7;
  end;
 hence LE q, p, L~f, f/.1, f/.len f by A2,A8,A9,A10,JORDAN5C:30;
end;

begin :: Special circular

theorem Th41:
 for f being non constant standard special_circular_sequence holds
  LeftComp f is open & RightComp f is open
proof
 let f be non constant standard special_circular_sequence;
    L~f is closed by SPPOL_1:49;
then A1:  (L~f)` is open by TOPS_1:29;
     LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
   then LeftComp f is_a_component_of (L~f)`;
 hence LeftComp f is open by A1,Th18;
     RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
   then RightComp f is_a_component_of (L~f)`;
 hence RightComp f is open by A1,Th18;
end;

definition let f be non constant standard special_circular_sequence;
 cluster L~f -> non vertical non horizontal;
 coherence
proof
    W-bound L~f <> E-bound L~f by TOPREAL5:23;
 hence L~f is non vertical by SPRECT_1:17;
    S-bound L~f <> N-bound L~f by TOPREAL5:22;
 hence L~f is non horizontal by SPRECT_1:18;
end;
 cluster LeftComp f -> being_Region;
 coherence
proof
 thus LeftComp f is open by Th41;
    LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
  then consider A being Subset of (TOP-REAL 2)|(L~f)` such that
A1:  A = LeftComp f and
A2:  A is_a_component_of (TOP-REAL 2)|(L~f)` by CONNSP_1:def 6;
    A is connected by A2,CONNSP_1:def 5;
 hence LeftComp f is connected by A1,CONNSP_1:24;
end;
 cluster RightComp f -> being_Region;
 coherence
proof
 thus RightComp f is open by Th41;
    RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
  then consider A being Subset of (TOP-REAL 2)|(L~f)` such that
A3:  A = RightComp f and
A4:  A is_a_component_of (TOP-REAL 2)|(L~f)` by CONNSP_1:def 6;
    A is connected by A4,CONNSP_1:def 5;
 hence RightComp f is connected by A3,CONNSP_1:24;
end;
end;

theorem Th42:
 for f being non constant standard special_circular_sequence
  holds RightComp f misses L~f
proof
 let f be non constant standard special_circular_sequence;
    (L~f)` =LeftComp f \/ RightComp f by GOBRD12:11;
  then RightComp f c= (L~f)` by XBOOLE_1:7;
 hence RightComp f misses L~f by SUBSET_1:43;
end;

theorem Th43:
 for f being non constant standard special_circular_sequence
  holds LeftComp f misses L~f
proof
 let f be non constant standard special_circular_sequence;
    (L~f)` =LeftComp f \/ RightComp f by GOBRD12:11;
  then LeftComp f c= (L~f)` by XBOOLE_1:7;
 hence LeftComp f misses L~f by SUBSET_1:43;
end;

theorem Th44:
 for f being non constant standard special_circular_sequence
  holds i_w_n f < i_e_n f
 proof let f be non constant standard special_circular_sequence;
   set G = GoB f;
A1: width G > 1 by GOBOARD7:35;
A2: i_w_n f <= len G by JORDAN5D:47;
A3: G*(i_w_n f,width G) = N-min L~f by JORDAN5D:def 7;
A4: 1 <= i_e_n f by JORDAN5D:47;
A5: G*(i_e_n f,width G) = N-max L~f by JORDAN5D:def 8;
A6:  (N-min L~f)`1 < (N-max L~f)`1 by SPRECT_2:55;
    then A7:    i_w_n f <> i_e_n f by A5,JORDAN5D:def 7;
  assume i_w_n f >= i_e_n f;
   then i_w_n f > i_e_n f by A7,AXIOMS:21;
  hence contradiction by A1,A2,A3,A4,A5,A6,GOBOARD5:4;
 end;

theorem Th45:
 for f being non constant standard special_circular_sequence
 ex i st 1 <= i & i < len GoB f & N-min L~f = (GoB f)*(i,width GoB f)
proof let f be non constant standard special_circular_sequence;
 take i = i_w_n f;
 thus 1 <= i by JORDAN5D:47;
A1:   i_e_n f <= len GoB f by JORDAN5D:47;
      i < i_e_n f by Th44;
 hence i < len GoB f by A1,AXIOMS:22;
 thus N-min L~f = (GoB f)*(i,width GoB f) by JORDAN5D:def 7;
end;

theorem Th46:
 for f being clockwise_oriented
      (non constant standard special_circular_sequence)
  st i in dom GoB f & f/.1 = (GoB f)*(i,width GoB f) &
     f/.1 = N-min L~f
  holds f/.2 = (GoB f)*(i+1,width GoB f)
       & f/.(len f -' 1) = (GoB f)*(i,width GoB f -' 1)
proof
 let f be clockwise_oriented (non constant standard special_circular_sequence)
  such that
A1: i in dom GoB f and
A2: f/.1 = (GoB f)*(i,width GoB f) and
A3: f/.1 = N-min L~f;
A4: f/.2 in N-most L~f by A3,SPRECT_2:34;
A5: 1 <= width GoB f by GOBRD11:34;
A6: 4 < len f by GOBOARD7:36;
   then A7:  1+1 <= len f by AXIOMS:22;
   then A8:   1+1 in dom f by FINSEQ_3:27;
   then consider i1,j1 being Nat such that
A9: [i1,j1] in Indices GoB f and
A10: f/.2 = (GoB f)*(i1,j1) by GOBOARD2:25;
A11: 1 <= len f by A6,AXIOMS:22;
then A12: 1 in dom f by FINSEQ_3:27;
A13: 1 <= i & i <= len GoB f by A1,FINSEQ_3:27;
then A14: [i,width GoB f] in Indices GoB f by A5,GOBOARD7:10;
A15: 1 <= j1 & j1 <= width GoB f by A9,GOBOARD5:1;
A16: 1 <= i1 & i1 <= len GoB f by A9,GOBOARD5:1;
     now assume
A17:  j1 < width GoB f;
A18:    (GoB f)*(i1,width GoB f)`2 = (GoB f)*(1,width GoB f)`2
                  by A5,A16,GOBOARD5:2
            .= N-bound L~f by JORDAN5D:42;
       (f/.2)`2 = (N-min L~f)`2 by A4,PSCOMP_1:98
             .= N-bound L~f by PSCOMP_1:94;
    hence contradiction by A10,A15,A16,A17,A18,GOBOARD5:5;
   end;
then A19: j1 = width GoB f by A15,AXIOMS:21;
A20:  abs(i-i1)+0 = abs(i-i1)+abs(0) by ABSVALUE:7
        .=abs(i-i1)+abs(width GoB f-width GoB f) by XCMPLX_1:14
        .= 1 by A2,A8,A9,A10,A12,A14,A19,GOBOARD5:13;
     now assume i > i1;
     then (f/.2)`1 < (N-min L~f)`1 by A2,A3,A10,A13,A15,A16,A19,GOBOARD5:4;
    hence contradiction by A4,PSCOMP_1:98;
   end;
  hence
A21: f/.2 = (GoB f)*(i+1,width GoB f) by A10,A19,A20,GOBOARD1:1;
A22: f/.len f = f/.1 by FINSEQ_6:def 1;
A23: len f -' 1 + 1 = len f by A11,AMI_5:4;
A24:  1 <= len f -' 1 & len f -' 1 <= len f by A7,JORDAN3:7,12;
   then A25: len f -' 1 in dom f by FINSEQ_3:27;
   then consider i2,j2 being Nat such that
A26: [i2,j2] in Indices GoB f and
A27: f/.(len f -' 1) = (GoB f)*(i2,j2) by GOBOARD2:25;
A28: 1 <= i2 & i2 <= len GoB f by A26,GOBOARD5:1;
A29: 1 <= j2 & j2 <= width GoB f by A26,GOBOARD5:1;
     len f in dom f by A11,FINSEQ_3:27;
   then A30:   abs(i2-i)+abs(j2-width GoB f) = 1
        by A2,A14,A22,A23,A25,A26,A27,GOBOARD5:13;
  per cases by A30,GOBOARD1:2;
  suppose that
A31: abs(i2-i)=1 and
A32: j2=width GoB f;
A33: (f/.(len f -' 1))`2 = ((GoB f)*(1,width GoB f))`2 by A5,A27,A28,A32,
GOBOARD5:2
         .= (N-min L~f)`2 by A2,A3,A5,A13,GOBOARD5:2
         .= N-bound L~f by PSCOMP_1:94;
      f/.(len f -' 1) in L~f by A7,A25,GOBOARD1:16;
then A34: f/.(len f -' 1) in N-most L~f by A33,SPRECT_2:14;
     now per cases by A31,GOBOARD1:1;
    suppose i > i2;
     then (f/.(len f -' 1))`1 < (N-min L~f)`1
          by A2,A3,A5,A13,A27,A28,A32,GOBOARD5:4;
    hence contradiction by A34,PSCOMP_1:98;
    suppose i+1 = i2;
     then 2 >= len f -' 1 by A21,A24,A27,A32,GOBOARD7:39;
     then 2+1 >= len f by Th5;
    hence contradiction by A6,AXIOMS:22;
   end;
  hence thesis;
  suppose that
A35: abs(j2-width GoB f)=1 and
A36: i2=i;
     j2 < width GoB f & width GoB f = j2+1 by A29,A35,GOBOARD1:1;
  hence f/.(len f -' 1) = (GoB f)*(i,width GoB f -' 1) by A27,A36,BINARITH:39;
end;

theorem
   for f being non constant standard special_circular_sequence
  st 1 <= i & i < j & j <= len f & f/.1 in L~mid(f,i,j)
 holds i = 1 or j = len f
proof
 let f be non constant standard special_circular_sequence such that
A1: 1 <= i and
A2: i < j and
A3: j <= len f;
 assume f/.1 in L~mid(f,i,j);
  then consider n such that
A4: 1 <= n & n+1 <= len mid(f,i,j) and
A5: f/.1 in LSeg(mid(f,i,j),n) by SPPOL_2:13;
 assume that
A6: i <> 1 and
A7: j <> len f;
    n < len mid(f,i,j) by A4,NAT_1:38;
  then A8: n<j-'i+1 by A1,A2,A3,JORDAN4:20;
  then A9: LSeg(mid(f,i,j),n)=LSeg(f,n+i-'1) by A1,A2,A3,A4,JORDAN4:31;
A10:  len f > 4 by GOBOARD7:36;
  then 1+1 <= len f by AXIOMS:22;
  then f/.1 in LSeg(f,1) by TOPREAL1:27;
  then A11: f/.1 in LSeg(f,1) /\ LSeg(f,n+i-'1) by A5,A9,XBOOLE_0:def 3;
then A12: LSeg(f,1) meets LSeg(f,n+i-'1) by XBOOLE_0:4;
 per cases by A12,GOBOARD5:def 4;
 suppose 1+1 >= n+i-'1;
  then A13: n+i <= 2+1 by Th5;
     n+i >= i+1 by A4,AXIOMS:24;
   then i+1 <= 2+1 by A13,AXIOMS:22;
   then A14:  i <= 2 by REAL_1:53;
     i > 1 by A1,A6,AXIOMS:21;
   then i >= 1+1 by NAT_1:38;
   then A15:  i = 2 by A14,AXIOMS:21;
   then n <= 1 by A13,REAL_1:53;
   then n = 1 by A4,AXIOMS:21;
   then A16:   n+i-'1 = 2 by A15,BINARITH:39;
     1+2 <= len f by A10,AXIOMS:22;
   then LSeg(f,1) /\ LSeg(f,1+1) = {f/.(1+1)} by TOPREAL1:def 8;
   then A17:  f/.1 = f/.2 by A11,A16,TARSKI:def 1;
    2 < len f by A10,AXIOMS:22;
 hence contradiction by A17,GOBOARD7:38;
 suppose
A18: n+i-'1+1 >= len f;
    n <= n+i by NAT_1:29;
  then 1 <= n+i by A4,AXIOMS:22;
then A19: len f <= n+i by A18,AMI_5:4;
A20: j < len f by A3,A7,AXIOMS:21;
     j-'i+1+i = j-'i+i+1 by XCMPLX_1:1
        .= j+1 by A2,AMI_5:4;
   then n+i < j+1 by A8,REAL_1:53;
   then n+i <= j by NAT_1:38;
 hence contradiction by A19,A20,AXIOMS:22;
end;

theorem
   for f being
  clockwise_oriented (non constant standard special_circular_sequence)
  st f/.1 = N-min L~f
 holds LSeg(f/.1,f/.2) c= L~SpStSeq L~f
proof
 let f be clockwise_oriented (non constant standard special_circular_sequence);
 assume
A1: f/.1 = N-min L~f;
then A2: f/.1 in LSeg(NW-corner L~f,NE-corner L~f) by Th28;
A3: f/.2 in N-most L~f by A1,SPRECT_2:34;
    N-most L~f c= LSeg(NW-corner L~f,NE-corner L~f) by Th27;
  then A4: LSeg(f/.1,f/.2) c= LSeg(NW-corner L~f,NE-corner L~f)
             by A2,A3,TOPREAL1:12;
    LSeg(NW-corner L~f,NE-corner L~f) c= L~SpStSeq L~f by Th26;
 hence LSeg(f/.1,f/.2) c= L~SpStSeq L~f by A4,XBOOLE_1:1;
end;

begin :: Rectangular

theorem Th49:
 for f being rectangular FinSequence of TOP-REAL 2,
     p being Point of TOP-REAL 2 st p in L~f
  holds p`1 = W-bound L~f or p`1 = E-bound L~f or
        p`2 = S-bound L~f or p`2 = N-bound L~f
proof
 let f be rectangular FinSequence of TOP-REAL 2,
     p be Point of TOP-REAL 2 such that
A1:   p in L~f;
  consider D being non vertical non horizontal non empty compact
                      Subset of TOP-REAL 2
           such that
A2:  f = SpStSeq D by SPRECT_1:def 2;
     L~f = (LSeg(NW-corner D,NE-corner D) \/ LSeg(NE-corner D,SE-corner D)) \/
         (LSeg(SE-corner D,SW-corner D) \/ LSeg(SW-corner D,NW-corner D))
          by A2,SPRECT_1:43;
   then A3:  p in LSeg(NW-corner D,NE-corner D) \/ LSeg(NE-corner D,SE-corner D
) or
     p in LSeg(SE-corner D,SW-corner D) \/ LSeg(SW-corner D,NW-corner D)
              by A1,XBOOLE_0:def 2;
 per cases by A3,XBOOLE_0:def 2;
 suppose
A4: p in LSeg(NW-corner D,NE-corner D);
    N-bound L~SpStSeq D = N-bound D by SPRECT_1:68;
  then (NW-corner D)`2 = N-bound L~f & (NE-corner D)`2 = N-bound L~f
        by A2,PSCOMP_1:75,77;
 hence thesis by A4,GOBOARD7:6;
 suppose
A5: p in LSeg(NE-corner D,SE-corner D);
    E-bound L~SpStSeq D = E-bound D by SPRECT_1:69;
  then (NE-corner D)`1 = E-bound L~f & (SE-corner D)`1 = E-bound L~f
        by A2,PSCOMP_1:76,78;
 hence thesis by A5,GOBOARD7:5;
 suppose
A6: p in LSeg(SE-corner D,SW-corner D);
    S-bound L~SpStSeq D = S-bound D by SPRECT_1:67;
  then (SE-corner D)`2 = S-bound L~f & (SW-corner D)`2 = S-bound L~f
        by A2,PSCOMP_1:73,79;
 hence thesis by A6,GOBOARD7:6;
 suppose
A7: p in LSeg(SW-corner D,NW-corner D);
    W-bound L~SpStSeq D = W-bound D by SPRECT_1:66;
  then (SW-corner D)`1 = W-bound L~f & (NW-corner D)`1 = W-bound L~f
        by A2,PSCOMP_1:72,74;
 hence thesis by A7,GOBOARD7:5;
end;

definition
 cluster rectangular special_circular_sequence;
 existence
proof
  consider C being non empty compact non vertical non horizontal
      Subset of TOP-REAL2;
    SpStSeq C is special_circular_sequence;
 hence thesis;
end;
end;

theorem Th50:
 for f being rectangular special_circular_sequence,
     g being S-Sequence_in_R2
  st g/.1 in LeftComp f & g/.len g in RightComp f
 holds L~f meets L~g
proof
 let f be rectangular special_circular_sequence,
     g be S-Sequence_in_R2 such that
A1: g/.1 in LeftComp f and
A2: g/.len g in RightComp f;
 assume L~f misses L~g;
  then L~g c= (L~f)` by SUBSET_1:43;
  then A3: L~g c= LeftComp f \/ RightComp f by GOBRD12:11;
A4: LeftComp f is open & RightComp f is open by Th41;
A5: len g >= 2 by TOPREAL1:def 10;
   then g/.1 in L~g by JORDAN3:34;
   then g/.1 in LeftComp f /\ L~g by A1,XBOOLE_0:def 3;
then A6:LeftComp f meets L~g by XBOOLE_0:4;
     g/.len g in L~g by A5,JORDAN3:34;
   then g/.len g in RightComp f /\ L~g by A2,XBOOLE_0:def 3;
then A7:RightComp f meets L~g by XBOOLE_0:4;
     LeftComp f misses RightComp f by SPRECT_1:96;
   then A8: L~g is not connected by A3,A4,A6,A7,TOPREAL5:4;
    L~g is_an_arc_of g/.1,g/.len g by TOPREAL1:31;
 hence contradiction by A8,JORDAN6:11;
end;

theorem Th51:
 for f being rectangular special_circular_sequence
  holds SpStSeq L~f = f
proof let f be rectangular special_circular_sequence;
A1: SpStSeq L~f = <*NW-corner L~f,NE-corner L~f,SE-corner L~f*>^
      <*SW-corner L~f,NW-corner L~f*> by SPRECT_1:def 1;
   set C = L~f, g = SpStSeq C;
   consider D being non vertical non horizontal non empty compact
       Subset of TOP-REAL 2 such that
A2:   f = SpStSeq D by SPRECT_1:def 2;
A3: 5 = len f by SPRECT_1:90;
A4: len g = len<*NW-corner L~f,NE-corner L~f,SE-corner L~f*>
             +len<*SW-corner L~f,NW-corner L~f*> by A1,FINSEQ_1:35
        .= 3+len<*SW-corner L~f,NW-corner L~f*> by FINSEQ_1:62
        .= 3+2 by FINSEQ_1:61;
   then A5: dom f = dom g by A3,FINSEQ_3:31;
    for i st i in dom f holds f/.i = g/.i
   proof let i;
    assume i in dom f;
then A6:    0 <> i & i <= len f by FINSEQ_3:27;
A7:  f/.1 = W-max C by SPRECT_1:91
          .= NW-corner D by A2,SPRECT_1:83
          .= NW-corner C by A2,SPRECT_1:70
          .= g/.1 by SPRECT_1:37;
    per cases by A3,A6,CQC_THE1:6;
    suppose i = 1;
    hence thesis by A7;
    suppose
A8:   i = 2;
    hence f/.i = E-max C by SPRECT_1:92
          .= NE-corner D by A2,SPRECT_1:87
          .= NE-corner C by A2,SPRECT_1:71
          .= g/.i by A8,SPRECT_1:38;
    suppose
A9:   i = 3;
    hence f/.i = E-min C by SPRECT_1:93
          .= SE-corner D by A2,SPRECT_1:86
          .= SE-corner C by A2,SPRECT_1:73
          .= g/.i by A9,SPRECT_1:39;
    suppose
A10:   i = 4;
    hence f/.i = W-min C by SPRECT_1:94
          .= SW-corner D by A2,SPRECT_1:82
          .= SW-corner C by A2,SPRECT_1:72
          .= g/.i by A10,SPRECT_1:40;
    suppose
A11:   i = 5;
    hence f/.i = f/.1 by A3,FINSEQ_6:def 1
          .= g/.i by A4,A7,A11,FINSEQ_6:def 1;
   end;
 hence f = g by A5,FINSEQ_5:13;
end;

theorem Th52:
 for f being rectangular special_circular_sequence holds
  L~f = { p where p is Point of TOP-REAL 2:
           p`1 = W-bound L~f & p`2 <= N-bound L~f & p`2 >= S-bound L~f or
           p`1 <= E-bound L~f & p`1 >= W-bound L~f & p`2 = N-bound L~f or
           p`1 <= E-bound L~f & p`1 >= W-bound L~f & p`2 = S-bound L~f or
           p`1 = E-bound L~f & p`2 <= N-bound L~f & p`2 >= S-bound L~f}
proof let f be rectangular special_circular_sequence;
  set C = L~f,
      E = { p : p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C},
      S = { p : p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C},
      N = { p : p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C},
      W = { p : p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C};
A1: C = L~SpStSeq C by Th51;
A2: LSeg(SE-corner C, NE-corner C) = E by SPRECT_1:25;
A3: LSeg(SW-corner C, SE-corner C) = S by SPRECT_1:26;
A4: LSeg(NW-corner C, NE-corner C) = N by SPRECT_1:27;
A5: LSeg(SW-corner C, NW-corner C) = W by SPRECT_1:28;
 thus
    C c= { p where p is Point of TOP-REAL 2:
           p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C or
           p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C or
           p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C or
           p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C}
  proof let x be set;
   assume
A6:  x in C;
    then reconsider q=x as Point of TOP-REAL 2;
      q in (LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C)) \/
        (LSeg(SE-corner C,SW-corner C) \/ LSeg(SW-corner C,NW-corner C))
           by A1,A6,SPRECT_1:43;
    then q in (LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C))
or
    q in (LSeg(SE-corner C,SW-corner C) \/ LSeg(SW-corner C,NW-corner C))
           by XBOOLE_0:def 2;
    then q in LSeg(NW-corner C,NE-corner C) or q in LSeg(NE-corner C,SE-corner
C) or
    q in LSeg(SE-corner C,SW-corner C) or q in LSeg(SW-corner C,NW-corner C)
           by XBOOLE_0:def 2;
    then (ex p st x = p & p`1 = E-bound C & p`2 <= N-bound C & p`2 >=
 S-bound C)
      or (ex p st x = p & p`1 <= E-bound C & p`1 >=
 W-bound C & p`2 = S-bound C)
      or (ex p st x = p & p`1 <= E-bound C & p`1 >=
 W-bound C & p`2 = N-bound C)
      or (ex p st x = p & p`1 = W-bound C & p`2 <= N-bound C & p`2 >=
 S-bound C)
           by A2,A3,A4,A5;
   hence x in { p where p is Point of TOP-REAL 2:
           p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C or
           p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C or
           p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C or
           p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C};
  end;
 let x be set;
 assume x in { p where p is Point of TOP-REAL 2:
           p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C or
           p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C or
           p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C or
           p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C};
  then ex p st x = p &
          (p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C or
           p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C or
           p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C or
           p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C);
    then x in LSeg(NW-corner C,NE-corner C) or x in LSeg(NE-corner C,SE-corner
C) or
    x in LSeg(SE-corner C,SW-corner C) or x in LSeg(SW-corner C,NW-corner C)
           by A2,A3,A4,A5;
    then x in (LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C))
or
    x in (LSeg(SE-corner C,SW-corner C) \/ LSeg(SW-corner C,NW-corner C))
           by XBOOLE_0:def 2;
    then x in (LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C))
\/
        (LSeg(SE-corner C,SW-corner C) \/ LSeg(SW-corner C,NW-corner C))
           by XBOOLE_0:def 2;
 hence x in C by A1,SPRECT_1:43;
end;

theorem Th53:
 for f being rectangular special_circular_sequence holds
  GoB f = (f/.4,f/.1)][(f/.3,f/.2)
proof let f be rectangular special_circular_sequence;
  set G = (f/.4,f/.1)][(f/.3,f/.2),
      v1 = Incr X_axis f, v2 = Incr Y_axis f;
A1: f/.1 = N-min L~f & f/.1 = W-max L~f by SPRECT_1:91;
A2: f/.2 = N-max L~f & f/.2 = E-max L~f by SPRECT_1:92;
A3: f/.3 = S-max L~f & f/.3 = E-min L~f by SPRECT_1:93;
A4: f/.4 = S-min L~f & f/.4 = W-min L~f by SPRECT_1:94;
A5: len f = 5 by SPRECT_1:90;
   set g = <*(f/.1)`1,(f/.2)`1*>,
       h = <*(f/.1)`1,(f/.2)`1*>^<*(f/.3)`1,(f/.4)`1,(f/.5)`1*>;
A6: len g = 2 by FINSEQ_1:61;
A7: len<*(f/.3)`1,(f/.4)`1,(f/.5)`1*> = 3 by FINSEQ_1:62;
A8: len h = len <*(f/.1)`1,(f/.2)`1*> + len<*(f/.3)`1,(f/.4)`1,(f/.5)`1*>
                by FINSEQ_1:35
        .= len <*(f/.1)`1,(f/.2)`1*> + 3 by FINSEQ_1:62
        .= 2 + 3 by FINSEQ_1:61
        .= len f by SPRECT_1:90;
      for n st n in dom h holds h.n = (f/.n)`1
     proof let n;
      assume n in dom h;
       then 1 <= n & n <= 5 by A5,A8,FINSEQ_3:27;
       then A9:     1 <= n & (n=0 or n=1 or n=2 or n=3 or n=4 or n=5) by
CQC_THE1:6;
      per cases by A9;
      suppose
A10:     n=1;
       then n in dom g by A6,FINSEQ_3:27;
      hence h.n = <*(f/.1)`1,(f/.2)`1*>.1 by A10,FINSEQ_1:def 7
         .= (f/.n)`1 by A10,FINSEQ_1:61;
      suppose
A11:      n=2;
       then n in dom g by A6,FINSEQ_3:27;
      hence h.n = <*(f/.1)`1,(f/.2)`1*>.2 by A11,FINSEQ_1:def 7
         .= (f/.n)`1 by A11,FINSEQ_1:61;
      suppose
A12:      n=3;
      hence h.n = h.(2+1)
         .= <*(f/.3)`1,(f/.4)`1,(f/.5)`1*>.1 by A6,A7,SCMFSA_7:10
         .= (f/.n)`1 by A12,FINSEQ_1:62;
      suppose
A13:      n=4;
      hence h.n = h.(2+2)
         .= <*(f/.3)`1,(f/.4)`1,(f/.5)`1*>.2 by A6,A7,SCMFSA_7:10
         .= (f/.n)`1 by A13,FINSEQ_1:62;
      suppose
A14:      n=5;
      hence h.n = h.(2+3)
         .= <*(f/.3)`1,(f/.4)`1,(f/.5)`1*>.3 by A6,A7,SCMFSA_7:10
         .= (f/.n)`1 by A14,FINSEQ_1:62;
     end;
   then A15: X_axis f = h by A8,GOBOARD1:def 3;
A16: dom g = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
A17: {(f/.3)`1,(f/.4)`1,(f/.5)`1} c= { (f/.1)`1,(f/.2)`1 }
    proof let x be set;
     assume
A18:     x in {(f/.3)`1,(f/.4)`1,(f/.5)`1};
     per cases by A18,ENUMSET1:13;
     suppose x = (f/.3)`1;
       then x = (f/.2)`1 by A2,A3,PSCOMP_1:105;
      hence thesis by TARSKI:def 2;
     suppose x = (f/.4)`1;
       then x = (f/.1)`1 by A1,A4,PSCOMP_1:85;
      hence thesis by TARSKI:def 2;
     suppose x = (f/.5)`1;
       then x = (f/.1)`1 by A5,FINSEQ_6:def 1;
      hence thesis by TARSKI:def 2;
    end;
A19: rng g = { (f/.1)`1,(f/.2)`1 } by FINSEQ_2:147;
then A20: rng g = rng<*(f/.1)`1,(f/.2)`1*> \/ {(f/.3)`1,(f/.4)`1,(f/.5)`1}
                                 by A17,XBOOLE_1:12
         .= rng<*(f/.1)`1,(f/.2)`1*> \/ rng<*(f/.3)`1,(f/.4)`1,(f/.5)`1*>
                                 by FINSEQ_2:148
         .= rng X_axis f by A15,FINSEQ_1:44;
A21: (f/.1)`1 < (f/.2)`1 by A1,A2,SPRECT_2:55;
A22: len g = 2 by FINSEQ_1:61
   .= Card rng X_axis f by A19,A20,A21,CARD_2:76;
     g is increasing
    proof let n,m such that
A23:   n in dom g and
A24:   m in dom g and
A25:   n<m;
A26:   g.1 = (f/.1)`1 & g.2 = (f/.2)`1 by FINSEQ_1:61;
        (n = 1 or n = 2) & (m = 1 or m = 2) by A16,A23,A24,TARSKI:def 2;
     hence g.n < g.m by A1,A2,A25,A26,SPRECT_2:55;
    end;
then A27: v1 = <*(f/.1)`1,(f/.2)`1*> by A20,A22,GOBOARD2:def 2;
   set g = <*(f/.4)`2,(f/.5)`2*>,
       h = <*(f/.1)`2,(f/.2)`2,(f/.3)`2*>^<*(f/.4)`2,(f/.5)`2*>;
A28: len g = 2 by FINSEQ_1:61;
A29: len<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> = 3 by FINSEQ_1:62;
A30: len h = len <*(f/.1)`2,(f/.2)`2,(f/.3)`2*> + len<*(f/.4)`2,(f/.5)`2*>
                by FINSEQ_1:35
        .= len <*(f/.4)`2,(f/.5)`2*> + 3 by FINSEQ_1:62
        .= 2 + 3 by FINSEQ_1:61
        .= len f by SPRECT_1:90;
      for n st n in dom h holds h.n = (f/.n)`2
     proof let n;
      assume n in dom h;
       then 1 <= n & n <= 5 by A5,A30,FINSEQ_3:27;
       then A31:     1 <= n & (n=0 or n=1 or n=2 or n=3 or n=4 or n=5) by
CQC_THE1:6;
      per cases by A31;
      suppose
A32:     n=1;
       then n in dom<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> by A29,FINSEQ_3:27;
      hence h.n = <*(f/.1)`2,(f/.2)`2,(f/.3)`2*>.1 by A32,FINSEQ_1:def 7
         .= (f/.n)`2 by A32,FINSEQ_1:62;
      suppose
A33:      n=2;
       then n in dom<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> by A29,FINSEQ_3:27;
      hence h.n = <*(f/.1)`2,(f/.2)`2,(f/.3)`2*>.2 by A33,FINSEQ_1:def 7
         .= (f/.n)`2 by A33,FINSEQ_1:62;
      suppose
A34:      n=3;
       then n in dom<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> by A29,FINSEQ_3:27;
      hence h.n = <*(f/.1)`2,(f/.2)`2,(f/.3)`2*>.3 by A34,FINSEQ_1:def 7
         .= (f/.n)`2 by A34,FINSEQ_1:62;
      suppose
A35:      n=4;
      hence h.n = h.(3+1)
         .= <*(f/.4)`2,(f/.5)`2*>.1 by A28,A29,SCMFSA_7:10
         .= (f/.n)`2 by A35,FINSEQ_1:61;
      suppose
A36:      n=5;
      hence h.n = h.(2+3)
         .= <*(f/.4)`2,(f/.5)`2*>.2 by A28,A29,SCMFSA_7:10
         .= (f/.n)`2 by A36,FINSEQ_1:61;
     end;
   then A37: Y_axis f = h by A30,GOBOARD1:def 4;
A38: dom g = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
A39: f/.1 = f/.5 by A5,FINSEQ_6:def 1;
A40: {(f/.1)`2,(f/.2)`2,(f/.3)`2} c= { (f/.4)`2,(f/.5)`2 }
    proof let x be set;
     assume
A41:     x in {(f/.1)`2,(f/.2)`2,(f/.3)`2};
     per cases by A41,ENUMSET1:13;
     suppose x = (f/.1)`2;
      hence thesis by A39,TARSKI:def 2;
     suppose x = (f/.2)`2;
       then x = (f/.1)`2 by A1,A2,PSCOMP_1:95;
      hence thesis by A39,TARSKI:def 2;
     suppose x = (f/.3)`2;
       then x = (f/.4)`2 by A3,A4,PSCOMP_1:115;
      hence thesis by TARSKI:def 2;
    end;
A42: rng g = { (f/.4)`2,(f/.5)`2 } by FINSEQ_2:147;
then A43: rng g = {(f/.1)`2,(f/.2)`2,(f/.3)`2} \/ {(f/.4)`2,(f/.5)`2}
    by A40,XBOOLE_1:12
         .= rng<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> \/ {(f/.4)`2,(f/.5)`2}
                                 by FINSEQ_2:148
         .= rng<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> \/ rng<*(f/.4)`2,(f/.5)`2*>
                                 by FINSEQ_2:147
         .= rng Y_axis f by A37,FINSEQ_1:44;
A44: (f/.4)`2 < (f/.5)`2 by A1,A4,A39,SPRECT_2:61;
A45: len g = 2 by FINSEQ_1:61
   .= Card rng Y_axis f by A42,A43,A44,CARD_2:76;
     g is increasing
    proof let n,m such that
A46:   n in dom g and
A47:   m in dom g and
A48:   n<m;
A49:   g.1 = (f/.4)`2 & g.2 = (f/.5)`2 by FINSEQ_1:61;
        (n = 1 or n = 2) & (m = 1 or m = 2) by A38,A46,A47,TARSKI:def 2;
     hence g.n < g.m by A1,A4,A39,A48,A49,SPRECT_2:61;
    end;
then A50: v2 = <*(f/.4)`2,(f/.1)`2*> by A39,A43,A45,GOBOARD2:def 2;
A51: len G = 2 by MATRIX_2:3 .= len v1 by A27,FINSEQ_1:61;
A52: width G = 2 by MATRIX_2:3 .= len v2 by A50,FINSEQ_1:61;
A53: v1.1 = (f/.1)`1 by A27,FINSEQ_1:61;
A54: v1.2 = (f/.2)`1 by A27,FINSEQ_1:61;
A55: v2.1 = (f/.4)`2 by A50,FINSEQ_1:61;
A56: v2.2 = (f/.1)`2 by A50,FINSEQ_1:61;
A57:  (f/.1)`1 = (f/.4)`1 by A1,A4,PSCOMP_1:85;
A58:  (f/.3)`1 = (f/.2)`1 by A2,A3,PSCOMP_1:105;
A59:  (f/.3)`2 = (f/.4)`2 by A3,A4,PSCOMP_1:115;
A60:  (f/.2)`2 = (f/.1)`2 by A1,A2,PSCOMP_1:95;
    for n,m st [n,m] in Indices G holds G*(n,m) = |[v1.n,v2.m]|
   proof let n,m;
    assume [n,m] in Indices G;
then A61:  [n,m]in { [1,1], [1,2],[2,1], [2,2]} by Th12;
    per cases by A61,ENUMSET1:18;
    suppose [n,m] = [1,1];
then A62:   n = 1 & m = 1 by ZFMISC_1:33;
    hence G*(n,m) = f/.4 by MATRIX_2:6
             .= |[v1.n,v2.m]| by A53,A55,A57,A62,EUCLID:57;
    suppose [n,m] = [1,2];
then A63:   n = 1 & m = 2 by ZFMISC_1:33;
    hence G*(n,m) = f/.1 by MATRIX_2:6
             .= |[v1.n,v2.m]| by A53,A56,A63,EUCLID:57;
    suppose [n,m] = [2,1];
then A64:   n = 2 & m = 1 by ZFMISC_1:33;
    hence G*(n,m) = f/.3 by MATRIX_2:6
             .= |[v1.n,v2.m]| by A54,A55,A58,A59,A64,EUCLID:57;
    suppose [n,m] = [2,2];
then A65:   n = 2 & m = 2 by ZFMISC_1:33;
    hence G*(n,m) = f/.2 by MATRIX_2:6
             .= |[v1.n,v2.m]| by A54,A56,A60,A65,EUCLID:57;
   end;
  then GoB(v1,v2) = G by A51,A52,GOBOARD2:def 1;
 hence thesis by GOBOARD2:def 3;
end;

theorem Th54:
 for f being rectangular special_circular_sequence holds
   LeftComp f = {p : not(W-bound L~f <= p`1 & p`1 <= E-bound L~f
                  & S-bound L~f <= p`2 & p`2 <= N-bound L~f)} &
   RightComp f = {q : W-bound L~f < q`1 & q`1 < E-bound L~f
                   & S-bound L~f < q`2 & q`2 < N-bound L~f}
proof let f be rectangular special_circular_sequence;
 defpred U[Element of TOP-REAL 2] means
     not(W-bound L~f <= $1`1 & $1`1 <= E-bound L~f
             & S-bound L~f <= $1`2 & $1`2 <= N-bound L~f);
 defpred V[Element of TOP-REAL 2] means
     W-bound L~f < $1`1 & $1`1 < E-bound L~f
                   & S-bound L~f < $1`2 & $1`2 < N-bound L~f;
 defpred W[Element of TOP-REAL 2] means
     $1`1 = W-bound L~f & $1`2 <= N-bound L~f & $1`2 >= S-bound L~f or
     $1`1 <= E-bound L~f & $1`1 >= W-bound L~f & $1`2 = N-bound L~f or
     $1`1 <= E-bound L~f & $1`1 >= W-bound L~f & $1`2 = S-bound L~f or
     $1`1 = E-bound L~f & $1`2 <= N-bound L~f & $1`2 >= S-bound L~f;
  set LC = {p : U[p] }, RC = {q : V[q] }, Lf = {p : W[p] };
A1: L~f = Lf by Th52;
A2: W-bound L~f < E-bound L~f by SPRECT_1:33;
A3: S-bound L~f < N-bound L~f by SPRECT_1:34;
A4: LC is Subset of TOP-REAL 2 from SubsetD;
A5: RC is Subset of TOP-REAL 2 from SubsetD;
    Lf is Subset of TOP-REAL 2 from SubsetD;
  then reconsider Lc'=LC,Rc'=RC,Lf as Subset of TOP-REAL 2
      by A4,A5;
  reconsider Lc', Rc' as Subset of TOP-REAL 2;
  reconsider Lf as Subset of TOP-REAL 2;
  reconsider Lc=Lc', Rc=Rc' as Subset of (TOP-REAL 2)|Lf`
   by A2,A3,JORDAN1:44,46;
  reconsider Lc, Rc as Subset of (TOP-REAL 2)|Lf`;
A6: LeftComp f is_a_component_of (L~f)` & RightComp f is_a_component_of (L~f)`
        by GOBOARD9:def 1,def 2;
    Rc = Rc';
  then Lc is_a_component_of (TOP-REAL 2)|Lf` by A2,A3,JORDAN1:41;
  then A7: Lc' is_a_component_of Lf` by CONNSP_1:def 6;
     len f > 4 by GOBOARD7:36;
then A8: 1+1 <= len f by AXIOMS:22;
      1 < width GoB f by GOBOARD7:35;
then A9: 1+1 <= width GoB f by NAT_1:38;
     1 <= len GoB f by GOBOARD7:34;
then A10: [1,1+1] in Indices GoB f by A9,GOBOARD7:10;
A11: GoB f = (f/.4,f/.1)][(f/.3,f/.2) by Th53;
then A12: f/.1 = (GoB f)*(1,1+1) by MATRIX_2:6;
A13:  1+1 = len GoB f by A11,MATRIX_2:3;
then A14: [1+1,1+1] in Indices GoB f by A9,GOBOARD7:10;
A15: 1+1 = width GoB f by A11,MATRIX_2:3;
A16: f/.(1+1) = (GoB f)*(1+1,1+1) by A11,MATRIX_2:6;
  then A17: left_cell(f,1) = cell(GoB f,1,1+1)by A8,A10,A12,A14,GOBOARD5:29;
  set p = 1/2*((GoB f)*(1,width GoB f)+(GoB f)*(1+1,width GoB f))+|[0,1]|,
      q = 1/2*((GoB f)*(1,width GoB f)+(GoB f)*(1+1,width GoB f));
A18: p in Int cell(GoB f,1,1+1) by A13,A15,GOBOARD6:35;
A19: Int cell(GoB f,1,1+1) c= LeftComp f by A17,GOBOARD9:def 1;
A20: p`2 = q`2+|[0,1]|`2 by TOPREAL3:7
     .= q`2+1 by EUCLID:56;
    q`2 = (1/2*((GoB f)*(1,width GoB f)+f/.2))`2 by A11,A15,MATRIX_2:6
     .= (1/2*(f/.1+f/.2))`2 by A11,A15,MATRIX_2:6
     .= 1/2*(f/.1+f/.2)`2 by TOPREAL3:9
     .= 1/2*((f/.1)`2+(f/.2)`2) by TOPREAL3:7
     .= 1/2*((N-min L~f)`2+(f/.2)`2) by SPRECT_1:91
     .= 1/2*((N-min L~f)`2+(N-max L~f)`2) by SPRECT_1:92
     .= 1/2*(N-bound L~f+(N-max L~f)`2) by PSCOMP_1:94
     .= 1/2*(N-bound L~f+N-bound L~f) by PSCOMP_1:94
     .= 1/2*(2*N-bound L~f) by XCMPLX_1:11
     .= N-bound L~f by XCMPLX_1:108;
  then p`2 > 0 + N-bound L~f by A20,REAL_1:67;
  then p in LC;
  then LC meets LeftComp f by A18,A19,XBOOLE_0:3;
 hence LeftComp f = LC by A1,A6,A7,GOBOARD9:3;
    Lc = Lc';
  then Rc is_a_component_of (TOP-REAL 2)|Lf` by A2,A3,JORDAN1:41;
  then A21: Rc' is_a_component_of Lf` by CONNSP_1:def 6;
A22: right_cell(f,1) = cell(GoB f,1,1) by A8,A10,A12,A14,A16,GOBOARD5:29;
  set p = 1/2*((GoB f)*(1,1)+(GoB f)*(2,2));
A23: p in Int cell(GoB f,1,1) by A13,A15,GOBOARD6:34;
A24: Int cell(GoB f,1,1) c= RightComp f by A22,GOBOARD9:def 2;
A25: p = 1/2*((GoB f)*(1,1)+f/.2) by A11,MATRIX_2:6
     .= 1/2*(f/.4+f/.2) by A11,MATRIX_2:6;
A26: 1/2*(W-bound L~f) + 1/2*(W-bound L~f)
        = 1/2*((W-bound L~f)+(W-bound L~f)) by XCMPLX_1:8
       .= 1/2*(2*(W-bound L~f)) by XCMPLX_1:11
       .= (W-bound L~f) by XCMPLX_1:108;
A27: 1/2*(S-bound L~f) + 1/2*(S-bound L~f)
        = 1/2*((S-bound L~f)+(S-bound L~f)) by XCMPLX_1:8
       .= 1/2*(2*(S-bound L~f)) by XCMPLX_1:11
       .= (S-bound L~f) by XCMPLX_1:108;
A28: 1/2*(N-bound L~f) + 1/2*(N-bound L~f)
        = 1/2*((N-bound L~f)+(N-bound L~f)) by XCMPLX_1:8
       .= 1/2*(2*(N-bound L~f)) by XCMPLX_1:11
       .= (N-bound L~f) by XCMPLX_1:108;
A29: 1/2*(E-bound L~f) + 1/2*(E-bound L~f)
        = 1/2*((E-bound L~f)+(E-bound L~f)) by XCMPLX_1:8
       .= 1/2*(2*(E-bound L~f)) by XCMPLX_1:11
       .= (E-bound L~f) by XCMPLX_1:108;
A30: p`1 = 1/2*(f/.4+f/.2)`1 by A25,TOPREAL3:9
        .= 1/2*((f/.4)`1+(f/.2)`1) by TOPREAL3:7
        .= 1/2*(f/.4)`1+ 1/2*(f/.2)`1 by XCMPLX_1:8;
A31: p`2 = 1/2*(f/.4+f/.2)`2 by A25,TOPREAL3:9
        .= 1/2*((f/.4)`2+(f/.2)`2) by TOPREAL3:7
        .= 1/2*(f/.4)`2+ 1/2*(f/.2)`2 by XCMPLX_1:8;
A32: (f/.4)`1 = (W-min L~f)`1 by SPRECT_1:94
         .= W-bound L~f by PSCOMP_1:84;
A33: (f/.2)`1 = (E-max L~f)`1 by SPRECT_1:92
        .= E-bound L~f by PSCOMP_1:104;
A34: (f/.4)`2 = (S-min L~f)`2 by SPRECT_1:94
         .= S-bound L~f by PSCOMP_1:114;
A35: (f/.2)`2 = (N-max L~f)`2 by SPRECT_1:92
         .= N-bound L~f by PSCOMP_1:94;
     (f/.2)`1 > W-bound L~f by A33,SPRECT_1:33;
   then 1/2*(f/.2)`1 > 1/2*W-bound L~f by REAL_1:70;
   then A36: W-bound L~f < p`1 by A26,A30,A32,REAL_1:53;
     (f/.4)`1 < E-bound L~f by A32,SPRECT_1:33;
   then 1/2*(f/.4)`1 < 1/2*E-bound L~f by REAL_1:70;
   then A37: p`1 < E-bound L~f by A29,A30,A33,REAL_1:53;
     (f/.2)`2 > S-bound L~f by A35,SPRECT_1:34;
   then 1/2*(f/.2)`2 > 1/2*S-bound L~f by REAL_1:70;
   then A38: S-bound L~f < p`2 by A27,A31,A34,REAL_1:53;
    (f/.4)`2 < N-bound L~f by A34,SPRECT_1:34;
  then 1/2*(f/.4)`2 < 1/2*N-bound L~f by REAL_1:70;
  then p`2 < N-bound L~f by A28,A31,A35,REAL_1:53;
  then p in RC by A36,A37,A38;
  then RC meets RightComp f by A23,A24,XBOOLE_0:3;
 hence RightComp f = RC by A1,A6,A21,GOBOARD9:3;
end;

definition
 cluster clockwise_oriented (rectangular special_circular_sequence);
 existence
proof
  consider C being non empty compact non vertical non horizontal
      Subset of TOP-REAL2;
    SpStSeq C is clockwise_oriented;
 hence thesis;
end;
end;

definition
 cluster -> clockwise_oriented (rectangular special_circular_sequence);
 coherence
proof let f be rectangular special_circular_sequence;
  consider D being non vertical non horizontal non empty compact
      Subset of TOP-REAL 2 such that
A1: f = SpStSeq D by SPRECT_1:def 2;
 thus thesis by A1;
end;
end;

theorem
   for f being rectangular special_circular_sequence,
     g being S-Sequence_in_R2
   st g/.1 in LeftComp f & g/.len g in RightComp f
 holds Last_Point(L~g,g/.1,g/.len g,L~f) <> NW-corner L~f
proof
 let f be rectangular special_circular_sequence,
     g be S-Sequence_in_R2 such that
A1: g/.1 in LeftComp f and
A2: g/.len g in RightComp f;
A3: L~f meets L~g by A1,A2,Th50;
A4: L~f is closed by SPPOL_1:49;
      L~f is closed & L~g is closed by SPPOL_1:49;
then A5: L~f /\ L~g is closed by TOPS_1:35;
A6: L~g is_an_arc_of g/.1, g/.len g by TOPREAL1:31;
  set nw = NW-corner L~f, inw = Index(nw,g);
 assume
A7: Last_Point(L~g,g/.1,g/.len g,L~f) = NW-corner L~f;
  then A8:  nw in L~g /\ L~f by A3,A5,A6,JORDAN5C:def 2;
  then A9:  nw in L~g by XBOOLE_0:def 3;
A10: L~f misses RightComp f by Th42;
A11: nw in L~f by A8,XBOOLE_0:def 3;
A12: len g in dom g by FINSEQ_5:6;
   then g.len g = g/.len g by FINSEQ_4:def 4;
then A13: nw <> g.len g by A2,A10,A11,XBOOLE_0:3;
     A14: inw < len g by A9,JORDAN3:41;
  then A15: 1 <= inw & inw+1 <= len g by A9,JORDAN3:41,NAT_1:38;
A16: nw in LSeg(g,inw) by A9,JORDAN3:42;

A17: 1 <= inw+1 by NAT_1:29;
then A18: inw+1 in dom g by A15,FINSEQ_3:27;
A19: now
   assume nw <> g.(inw+1);
then A20: nw <> g/.(inw+1) by A18,FINSEQ_4:def 4;
A21: len g >= 1 by A15,A17,AXIOMS:22;
   per cases;
  suppose
A22: g/.(inw+1) in L~f;
   then inw+1 <> len g by A2,A10,XBOOLE_0:3;
   then inw+1 < len g by A15,AXIOMS:21;
   then A23: inw+1+1 <= len g by NAT_1:38;
   then g/.(inw+1) in LSeg(g,inw+1) by A17,TOPREAL1:27;
   then inw >= inw+1 by A3,A4,A7,A15,A16,A17,A20,A22,A23,JORDAN5C:28;
 hence contradiction by REAL_1:69;
 suppose not g/.(inw+1) in L~f;
  then g/.(inw+1) in (L~f)` by SUBSET_1:50;
  then A24: g/.(inw+1) in LeftComp f \/ RightComp f by GOBRD12:11;
A25: now
A26: RightComp f = {q : W-bound L~f < q`1 & q`1 < E-bound L~f
                   & S-bound L~f < q`2 & q`2 < N-bound L~f} by Th54;
   assume g/.(inw+1) in RightComp f;
then A27:     ex q st g/.(inw+1) = q &
                 W-bound L~f < q`1 & q`1 < E-bound L~f &
                 S-bound L~f < q`2 & q`2 < N-bound L~f by A26;
A28:   LSeg(g,inw) = LSeg(g/.inw,g/.(inw+1)) by A15,TOPREAL1:def 5;
      LSeg(g,inw) is vertical or LSeg(g,inw) is horizontal by SPPOL_1:41;
    then (g/.(inw+1))`1 = nw`1 or (g/.(inw+1))`2 = nw`2 by A16,A28,Th19,Th20;
   hence contradiction by A27,PSCOMP_1:74,75;
  end;
then A29: g/.(inw+1) in LeftComp f by A24,XBOOLE_0:def 2;
A30: inw+1<len g by A2,A15,A25,AXIOMS:21;
  reconsider m = mid(g,inw+1,len g) as S-Sequence_in_R2
           by A2,A15,A17,A21,A25,JORDAN3:39;
A31: m/.1 in LeftComp f by A12,A18,A29,SPRECT_2:12;
    m/.len m in RightComp f by A2,A12,A18,SPRECT_2:13;
  then L~f meets L~m by A31,Th50;
  then consider q being set such that
A32: q in L~f and
A33: q in L~m by XBOOLE_0:3;
  reconsider q as Point of TOP-REAL 2 by A33;
  consider i such that
A34: 1 <= i & i+1 <= len m and
A35: q in LSeg(m,i) by A33,SPPOL_2:13;
A36: len m = len g-'(inw+1)+1 by A15,A17,JORDAN4:20;
    i < len m by A34,NAT_1:38;
  then A37: LSeg(m,i)=LSeg(g,i+(inw+1)-'1) by A17,A30,A34,A36,JORDAN4:31;
  set j = i+(inw+1)-'1;
A38: j = i+inw+1-'1 by XCMPLX_1:1
   .= i+inw by BINARITH:39;
    inw >= 0 by NAT_1:18;
  then A39: 0+1 <= j by A34,A38,REAL_1:55;
    len m = len g -' inw by A14,A36,NAT_2:9;
  then len m + inw = len g by A14,AMI_5:4;
  then i+1 + inw <= len g by A34,AXIOMS:24;
then A40: j + 1 <= len g by A38,XCMPLX_1:1;
A41: j >= inw+1 by A34,A38,AXIOMS:24;
   now assume nw = q;
then A42: nw in LSeg(g,inw) /\ LSeg(g,j) by A16,A35,A37,XBOOLE_0:def 3;
then A43: LSeg(g,inw) meets LSeg(g,j) by XBOOLE_0:4;
   per cases by A41,AXIOMS:21;
   suppose
A44:  inw+1 = j;
      inw+1+1 <= len g by A30,NAT_1:38;
    then inw + (1+1) <= len g by XCMPLX_1:1;
    then LSeg(g,inw) /\ LSeg(g,inw+1) = {g/.(inw+1)} by A15,TOPREAL1:def 8;
   hence contradiction by A20,A42,A44,TARSKI:def 1;
   suppose inw+1 < j;
   hence contradiction by A43,TOPREAL1:def 9;
  end;
  then inw >= j by A3,A4,A7,A15,A16,A32,A35,A37,A39,A40,JORDAN5C:28;
  then inw >= inw+1 by A41,AXIOMS:22;
 hence contradiction by REAL_1:69;
 end;
 then A45: inw+1 < len g by A13,A15,AXIOMS:21;
 then A46: inw+1+1 <= len g by NAT_1:38;
A47: 1 <= inw+1+1 by NAT_1:29;
 then A48: inw+1+1 in dom g by A46,FINSEQ_3:27;
   g/.(inw+1) in LSeg(g,inw+1) by A17,A46,TOPREAL1:27;
 then A49: nw in LSeg(g,inw+1) by A18,A19,FINSEQ_4:def 4;
   inw+1 < inw+1+1 by NAT_1:38;
 then A50:  nw <> g.(inw+1+1) by A18,A19,A48,FUNCT_1:def 8;
then A51: nw <> g/.(inw+1+1) by A48,FINSEQ_4:def 4;
A52: len g >= 1 by A46,A47,AXIOMS:22;
   per cases;
  suppose
A53: g/.(inw+1+1) in L~f;
   then inw+1+1 <> len g by A2,A10,XBOOLE_0:3;
   then inw+1+1 < len g by A46,AXIOMS:21;
   then A54: inw+1+1+1 <= len g by NAT_1:38;
   then A55:   g/.(inw+1+1) in LSeg(g,inw+1+1) by A47,TOPREAL1:27;
    nw <> g/.(inw+1+1) by A48,A50,FINSEQ_4:def 4;
  then inw+1 >= inw+1+1 by A3,A4,A7,A17,A46,A47,A49,A53,A54,A55,JORDAN5C:28;
 hence contradiction by REAL_1:69;
 suppose not g/.(inw+1+1) in L~f;
  then g/.(inw+1+1) in (L~f)` by SUBSET_1:50;
  then A56: g/.(inw+1+1) in LeftComp f \/ RightComp f by GOBRD12:11;
A57: now
A58: RightComp f = {q : W-bound L~f < q`1 & q`1 < E-bound L~f
                   & S-bound L~f < q`2 & q`2 < N-bound L~f} by Th54;
   assume g/.(inw+1+1) in RightComp f;
then A59:     ex q st g/.(inw+1+1) = q &
                 W-bound L~f < q`1 & q`1 < E-bound L~f &
                 S-bound L~f < q`2 & q`2 < N-bound L~f by A58;
A60:   LSeg(g,inw+1) = LSeg(g/.(inw+1),g/.(inw+1+1))
      by A17,A46,TOPREAL1:def 5;
       LSeg(g,inw+1) is vertical or LSeg(g,inw+1) is horizontal by SPPOL_1:41;
     then (g/.(inw+1+1))`1 = nw`1 or (g/.(inw+1+1))`2 = nw`2
       by A49,A60,Th19,Th20;
   hence contradiction by A59,PSCOMP_1:74,75;
  end;
then A61: g/.(inw+1+1) in LeftComp f by A56,XBOOLE_0:def 2;
A62: inw+1+1<len g by A2,A46,A57,AXIOMS:21;
  reconsider m = mid(g,inw+1+1,len g) as S-Sequence_in_R2
           by A2,A46,A47,A52,A57,JORDAN3:39;
A63: m/.1 in LeftComp f by A12,A48,A61,SPRECT_2:12;
    m/.len m in RightComp f by A2,A12,A48,SPRECT_2:13;
  then L~f meets L~m by A63,Th50;
  then consider q being set such that
A64: q in L~f and
A65: q in L~m by XBOOLE_0:3;
  reconsider q as Point of TOP-REAL 2 by A65;
  consider i such that
A66: 1 <= i & i+1 <= len m and
A67: q in LSeg(m,i) by A65,SPPOL_2:13;
A68: len m = len g-'(inw+1+1)+1 by A46,A47,JORDAN4:20;
    i < len m by A66,NAT_1:38;
  then A69: LSeg(m,i)=LSeg(g,i+(inw+1+1)-'1) by A47,A62,A66,A68,JORDAN4:31;
  set j = i+(inw+1+1)-'1;
A70: j = i+(inw+1)+1-'1 by XCMPLX_1:1
       .= i+inw+1+1-'1 by XCMPLX_1:1
       .= i+inw+1 by BINARITH:39;
then A71: 0+1 <= j by NAT_1:29;
    len m = len g -' (inw+1) by A45,A68,NAT_2:9;
  then len m + (inw+1) = len g by A15,AMI_5:4;
  then i+ 1 + (inw +1) <= len g by A66,AXIOMS:24;
  then i+ 1 + inw +1 <= len g by XCMPLX_1:1;
then A72: j + 1 <= len g by A70,XCMPLX_1:1;
     j = i+(inw+1) by A70,XCMPLX_1:1;
   then A73: j >= inw+1+1 by A66,AXIOMS:24;
    now assume nw = q;
then A74: nw in LSeg(g,inw+1) /\ LSeg(g,j) by A49,A67,A69,XBOOLE_0:def 3;
then A75: LSeg(g,inw+1) meets LSeg(g,j) by XBOOLE_0:4;
   per cases by A73,AXIOMS:21;
   suppose
A76:  inw+1+1 = j;
      inw+1+1+1 <= len g by A62,NAT_1:38;
    then inw+1 + (1+1) <= len g by XCMPLX_1:1;
    then LSeg(g,inw+1) /\ LSeg(g,inw+1+1) = {g/.(inw+1+1)}
                 by A17,TOPREAL1:def 8;
   hence contradiction by A51,A74,A76,TARSKI:def 1;
   suppose inw+1+1 < j;
   hence contradiction by A75,TOPREAL1:def 9;
  end;
  then inw+1 >= j by A3,A4,A7,A17,A46,A49,A64,A67,A69,A71,A72,JORDAN5C:28;
  then inw+1 >= inw+1+1 by A73,AXIOMS:22;
 hence contradiction by REAL_1:69;
end;

theorem
   for f being rectangular special_circular_sequence,
     g being S-Sequence_in_R2
   st g/.1 in LeftComp f & g/.len g in RightComp f
 holds Last_Point(L~g,g/.1,g/.len g,L~f) <> SE-corner L~f
proof
 let f be rectangular special_circular_sequence,
     g be S-Sequence_in_R2 such that
A1: g/.1 in LeftComp f and
A2: g/.len g in RightComp f;
A3: L~f meets L~g by A1,A2,Th50;
A4: L~f is closed by SPPOL_1:49;
      L~f is closed & L~g is closed by SPPOL_1:49;
then A5: L~f /\ L~g is closed by TOPS_1:35;
A6: L~g is_an_arc_of g/.1, g/.len g by TOPREAL1:31;
  set se = SE-corner L~f, ise = Index(se,g);
 assume
A7: Last_Point(L~g,g/.1,g/.len g,L~f) = SE-corner L~f;
then A8:  se in L~g /\ L~f by A3,A5,A6,JORDAN5C:def 2;
then A9:  se in L~g by XBOOLE_0:def 3;
A10: L~f misses RightComp f by Th42;
A11: se in L~f by A8,XBOOLE_0:def 3;
A12: len g in dom g by FINSEQ_5:6;
   then g.len g = g/.len g by FINSEQ_4:def 4;
then A13: se <> g.len g by A2,A10,A11,XBOOLE_0:3;
     A14: ise < len g by A9,JORDAN3:41;
then A15: 1 <= ise & ise+1 <= len g by A9,JORDAN3:41,NAT_1:38;
A16: se in LSeg(g,ise) by A9,JORDAN3:42;
A17: 1 <= ise+1 by NAT_1:29;
then A18: ise+1 in dom g by A15,FINSEQ_3:27;
A19: now
   assume se <> g.(ise+1);
then A20: se <> g/.(ise+1) by A18,FINSEQ_4:def 4;
A21: len g >= 1 by A15,A17,AXIOMS:22;
   per cases;
  suppose
A22: g/.(ise+1) in L~f;
   then ise+1 <> len g by A2,A10,XBOOLE_0:3;
   then ise+1 < len g by A15,AXIOMS:21;
   then A23: ise+1+1 <= len g by NAT_1:38;
   then g/.(ise+1) in LSeg(g,ise+1) by A17,TOPREAL1:27;
   then ise >= ise+1 by A3,A4,A7,A15,A16,A17,A20,A22,A23,JORDAN5C:28;
 hence contradiction by REAL_1:69;
 suppose not g/.(ise+1) in L~f;
  then g/.(ise+1) in (L~f)` by SUBSET_1:50;
  then A24: g/.(ise+1) in LeftComp f \/ RightComp f by GOBRD12:11;
A25: now
A26: RightComp f = {q : W-bound L~f < q`1 & q`1 < E-bound L~f
                   & S-bound L~f < q`2 & q`2 < N-bound L~f} by Th54;
   assume g/.(ise+1) in RightComp f;
then A27:     ex q st g/.(ise+1) = q &
                 W-bound L~f < q`1 & q`1 < E-bound L~f &
                 S-bound L~f < q`2 & q`2 < N-bound L~f by A26;
A28:   LSeg(g,ise) = LSeg(g/.ise,g/.(ise+1)) by A15,TOPREAL1:def 5;
     LSeg(g,ise) is vertical or LSeg(g,ise) is horizontal by SPPOL_1:41;
   then (g/.(ise+1))`1 = se`1 or (g/.(ise+1))`2 = se`2 by A16,A28,Th19,Th20;
   hence contradiction by A27,PSCOMP_1:78,79;
  end;
then A29: g/.(ise+1) in LeftComp f by A24,XBOOLE_0:def 2;
A30: ise+1<len g by A2,A15,A25,AXIOMS:21;
  reconsider m = mid(g,ise+1,len g) as S-Sequence_in_R2
           by A2,A15,A17,A21,A25,JORDAN3:39;
A31: m/.1 in LeftComp f by A12,A18,A29,SPRECT_2:12;
    m/.len m in RightComp f by A2,A12,A18,SPRECT_2:13;
  then L~f meets L~m by A31,Th50;
  then consider q being set such that
A32: q in L~f and
A33: q in L~m by XBOOLE_0:3;
  reconsider q as Point of TOP-REAL 2 by A33;
  consider i such that
A34: 1 <= i & i+1 <= len m and
A35: q in LSeg(m,i) by A33,SPPOL_2:13;
A36: len m = len g-'(ise+1)+1 by A15,A17,JORDAN4:20;
    i < len m by A34,NAT_1:38;
  then A37: LSeg(m,i)=LSeg(g,i+(ise+1)-'1) by A17,A30,A34,A36,JORDAN4:31;
  set j = i+(ise+1)-'1;
A38: j = i+ise+1-'1 by XCMPLX_1:1
   .= i+ise by BINARITH:39;
    ise >= 0 by NAT_1:18;
  then A39: 0+1 <= j by A34,A38,REAL_1:55;
    len m = len g -' ise by A14,A36,NAT_2:9;
  then len m + ise = len g by A14,AMI_5:4;
  then i+1 + ise <= len g by A34,AXIOMS:24;
then A40: j + 1 <= len g by A38,XCMPLX_1:1;
A41: j >= ise+1 by A34,A38,AXIOMS:24;
   now assume se = q;
then A42: se in LSeg(g,ise) /\ LSeg(g,j) by A16,A35,A37,XBOOLE_0:def 3;
then A43: LSeg(g,ise) meets LSeg(g,j) by XBOOLE_0:4;
   per cases by A41,AXIOMS:21;
   suppose
A44:  ise+1 = j;
      ise+1+1 <= len g by A30,NAT_1:38;
    then ise + (1+1) <= len g by XCMPLX_1:1;
    then LSeg(g,ise) /\ LSeg(g,ise+1) = {g/.(ise+1)} by A15,TOPREAL1:def 8;
   hence contradiction by A20,A42,A44,TARSKI:def 1;
   suppose ise+1 < j;
   hence contradiction by A43,TOPREAL1:def 9;
  end;
  then ise >= j by A3,A4,A7,A15,A16,A32,A35,A37,A39,A40,JORDAN5C:28;
  then ise >= ise+1 by A41,AXIOMS:22;
 hence contradiction by REAL_1:69;
 end;
 then A45: ise+1 < len g by A13,A15,AXIOMS:21;
 then A46: ise+1+1 <= len g by NAT_1:38;
A47: 1 <= ise+1+1 by NAT_1:29;
 then A48: ise+1+1 in dom g by A46,FINSEQ_3:27;
   g/.(ise+1) in LSeg(g,ise+1) by A17,A46,TOPREAL1:27;
 then A49: se in LSeg(g,ise+1) by A18,A19,FINSEQ_4:def 4;
   ise+1 < ise+1+1 by NAT_1:38;
 then A50:  se <> g.(ise+1+1) by A18,A19,A48,FUNCT_1:def 8;
then A51: se <> g/.(ise+1+1) by A48,FINSEQ_4:def 4;
A52: len g >= 1 by A46,A47,AXIOMS:22;
   per cases;
  suppose
A53: g/.(ise+1+1) in L~f;
   then ise+1+1 <> len g by A2,A10,XBOOLE_0:3;
   then ise+1+1 < len g by A46,AXIOMS:21;
   then A54: ise+1+1+1 <= len g by NAT_1:38;
   then A55:   g/.(ise+1+1) in LSeg(g,ise+1+1) by A47,TOPREAL1:27;
    se <> g/.(ise+1+1) by A48,A50,FINSEQ_4:def 4;
  then ise+1 >= ise+1+1 by A3,A4,A7,A17,A46,A47,A49,A53,A54,A55,JORDAN5C:28;
 hence contradiction by REAL_1:69;
 suppose not g/.(ise+1+1) in L~f;
  then g/.(ise+1+1) in (L~f)` by SUBSET_1:50;
  then A56: g/.(ise+1+1) in LeftComp f \/ RightComp f by GOBRD12:11;
A57: now
A58: RightComp f = {q : W-bound L~f < q`1 & q`1 < E-bound L~f
                   & S-bound L~f < q`2 & q`2 < N-bound L~f} by Th54;
   assume g/.(ise+1+1) in RightComp f;
then A59:     ex q st g/.(ise+1+1) = q &
                 W-bound L~f < q`1 & q`1 < E-bound L~f &
                 S-bound L~f < q`2 & q`2 < N-bound L~f by A58;
A60:   LSeg(g,ise+1) = LSeg(g/.(ise+1),g/.(ise+1+1))
     by A17,A46,TOPREAL1:def 5;
       LSeg(g,ise+1) is vertical or LSeg(g,ise+1) is horizontal by SPPOL_1:41;
     then (g/.(ise+1+1))`1 = se`1 or (g/.(ise+1+1))`2 = se`2
     by A49,A60,Th19,Th20;
   hence contradiction by A59,PSCOMP_1:78,79;
  end;
then A61: g/.(ise+1+1) in LeftComp f by A56,XBOOLE_0:def 2;
A62: ise+1+1<len g by A2,A46,A57,AXIOMS:21;
  reconsider m = mid(g,ise+1+1,len g) as S-Sequence_in_R2
           by A2,A46,A47,A52,A57,JORDAN3:39;
A63: m/.1 in LeftComp f by A12,A48,A61,SPRECT_2:12;
    m/.len m in RightComp f by A2,A12,A48,SPRECT_2:13;
  then L~f meets L~m by A63,Th50;
  then consider q being set such that
A64: q in L~f and
A65: q in L~m by XBOOLE_0:3;
  reconsider q as Point of TOP-REAL 2 by A65;
  consider i such that
A66: 1 <= i & i+1 <= len m and
A67: q in LSeg(m,i) by A65,SPPOL_2:13;
A68: len m = len g-'(ise+1+1)+1 by A46,A47,JORDAN4:20;
    i < len m by A66,NAT_1:38;
  then A69: LSeg(m,i)=LSeg(g,i+(ise+1+1)-'1) by A47,A62,A66,A68,JORDAN4:31;
  set j = i+(ise+1+1)-'1;
A70: j = i+(ise+1)+1-'1 by XCMPLX_1:1
       .= i+ise+1+1-'1 by XCMPLX_1:1
       .= i+ise+1 by BINARITH:39;
then A71: 0+1 <= j by NAT_1:29;
    len m = len g -' (ise+1) by A45,A68,NAT_2:9;
  then len m + (ise+1) = len g by A15,AMI_5:4;
  then i+ 1 + (ise +1) <= len g by A66,AXIOMS:24;
  then i+ 1 + ise +1 <= len g by XCMPLX_1:1;
then A72: j + 1 <= len g by A70,XCMPLX_1:1;
     j = i+(ise+1) by A70,XCMPLX_1:1;
   then A73: j >= ise+1+1 by A66,AXIOMS:24;
    now assume se = q;
then A74: se in LSeg(g,ise+1) /\ LSeg(g,j) by A49,A67,A69,XBOOLE_0:def 3;
then A75: LSeg(g,ise+1) meets LSeg(g,j) by XBOOLE_0:4;
   per cases by A73,AXIOMS:21;
   suppose
A76:  ise+1+1 = j;
      ise+1+1+1 <= len g by A62,NAT_1:38;
    then ise+1 + (1+1) <= len g by XCMPLX_1:1;
    then LSeg(g,ise+1) /\ LSeg(g,ise+1+1) = {g/.(ise+1+1)}
                 by A17,TOPREAL1:def 8;
   hence contradiction by A51,A74,A76,TARSKI:def 1;
   suppose ise+1+1 < j;
   hence contradiction by A75,TOPREAL1:def 9;
  end;
  then ise+1 >= j by A3,A4,A7,A17,A46,A49,A64,A67,A69,A71,A72,JORDAN5C:28;
  then ise+1 >= ise+1+1 by A73,AXIOMS:22;
 hence contradiction by REAL_1:69;
end;

theorem Th57:
 for f being rectangular special_circular_sequence,
     p being Point of TOP-REAL 2 st
   W-bound L~f > p`1 or p`1 > E-bound L~f or
   S-bound L~f > p`2 or p`2 > N-bound L~f
 holds p in LeftComp f
proof
 let f be rectangular special_circular_sequence,
     p be Point of TOP-REAL 2;
     LeftComp f = {q : not(W-bound L~f <= q`1 & q`1 <= E-bound L~f
                  & S-bound L~f <= q`2 & q`2 <= N-bound L~f)} by Th54;
 hence thesis;
end;

theorem
   for f being
   clockwise_oriented (non constant standard special_circular_sequence)
  st f/.1 = N-min L~f
 holds LeftComp SpStSeq L~f c= LeftComp f
proof
 let f be clockwise_oriented (non constant standard special_circular_sequence)
 such that
A1: f/.1 = N-min L~f;
A2: LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
     LeftComp SpStSeq L~f is_a_component_of (L~SpStSeq L~f)` by GOBOARD9:def 1;
   then consider B1 being Subset of (TOP-REAL 2)|(L~SpStSeq L~f)`
   such that
A3: B1 = LeftComp SpStSeq L~f and
A4: B1 is_a_component_of (TOP-REAL 2)|(L~SpStSeq L~f)` by CONNSP_1:def 6;
     B1 is connected by A4,CONNSP_1:def 5;
then A5: LeftComp SpStSeq L~f is connected by A3,CONNSP_1:24;
   consider i such that
A6: 1 <= i & i < len GoB f and
A7: N-min L~f = (GoB f)*(i,width GoB f) by Th45;
A8: i in dom GoB f by A6,FINSEQ_3:27;
   then A9:  f/.2 = (GoB f)*(i+1,width GoB f) by A1,A7,Th46;
A10: width GoB f >= 1 by GOBRD11:34;
then A11: width GoB f -' 1 + 1 = width GoB f by AMI_5:4;
     len f > 4 by GOBOARD7:36;
then A12: 1+1 <= len f by AXIOMS:22;
A13: [i,width GoB f] in Indices GoB f by A6,A10,GOBOARD7:10;
A14: 1 <= i+1 & i+1 <= len GoB f by A6,NAT_1:38;
  then [i+1,width GoB f] in Indices GoB f by A10,GOBOARD7:10;
  then A15: left_cell(f,1) = cell(GoB f,i,width GoB f) by A1,A7,A9,A11,A12,A13,
GOBOARD5:29;
  set a = 1/2*((GoB f)*(i,width GoB f)+(GoB f)*(i+1,width GoB f))+|[0,1]|,
      q = 1/2*((GoB f)*(i,width GoB f)+(GoB f)*(i+1,width GoB f));
A16: a in Int cell(GoB f,i,width GoB f) by A6,A14,GOBOARD6:35;
A17: Int cell(GoB f,i,width GoB f) c= LeftComp f by A15,GOBOARD9:def 1;
A18: a`2 = q`2+|[0,1]|`2 by TOPREAL3:7
     .= q`2+1 by EUCLID:56;
A19: N-bound L~SpStSeq L~f = N-bound L~f by SPRECT_1:68;
A20: (f/.2)`2 = ((GoB f)*(1,width GoB f))`2 by A9,A10,A14,GOBOARD5:2
         .= (N-min L~f)`2 by A6,A7,A10,GOBOARD5:2
         .= N-bound L~f by PSCOMP_1:94;
A21: LeftComp SpStSeq L~f =
      {p : not(W-bound L~SpStSeq L~f <= p`1 & p`1 <= E-bound L~SpStSeq L~f
           & S-bound L~SpStSeq L~f <= p`2 & p`2 <= N-bound L~SpStSeq L~f)}
               by Th54;
    q`2 = (1/2*((GoB f)*(i,width GoB f)+f/.2))`2 by A1,A7,A8,Th46
     .= 1/2*(f/.1+f/.2)`2 by A1,A7,TOPREAL3:9
     .= 1/2*((f/.1)`2+(f/.2)`2) by TOPREAL3:7
     .= 1/2*(N-bound L~f+N-bound L~f) by A1,A20,PSCOMP_1:94
     .= 1/2*(2*N-bound L~f) by XCMPLX_1:11
     .= N-bound L~f by XCMPLX_1:108;
  then a`2 > 0 + N-bound L~f by A18,REAL_1:67;
  then a`2 > N-bound L~SpStSeq L~f by SPRECT_1:68;
  then a in LeftComp SpStSeq L~f by A21;
   then A22: LeftComp f meets LeftComp SpStSeq L~f by A16,A17,XBOOLE_0:3;
  defpred X[Element of TOP-REAL 2] means $1`2 < S-bound L~f;
  reconsider P1 = { p: X[p] }
     as Subset of TOP-REAL 2 from SubsetD;
  defpred X[Element of TOP-REAL 2] means $1`2 > N-bound L~f;
  reconsider P2 = { p: X[p] }
     as Subset of TOP-REAL 2 from SubsetD;
  defpred X[Element of TOP-REAL 2] means $1`1 > E-bound L~f;
  reconsider P3 = { p: X[p] }
     as Subset of TOP-REAL 2 from SubsetD;
  defpred X[Element of TOP-REAL 2] means $1`1 < W-bound L~f;
  reconsider P4 = { p: X[p] }
     as Subset of TOP-REAL 2 from SubsetD;
A23: W-bound L~SpStSeq L~f = W-bound L~f by SPRECT_1:66;
A24: S-bound L~SpStSeq L~f = S-bound L~f by SPRECT_1:67;
A25: E-bound L~SpStSeq L~f = E-bound L~f by SPRECT_1:69;
A26: LeftComp SpStSeq L~f = P1 \/ P2 \/ (P3 \/ P4)
   proof
     thus LeftComp SpStSeq L~f c= P1 \/ P2 \/ (P3 \/ P4)
      proof let x be set;
       assume x in LeftComp SpStSeq L~f;
        then x in { p : not(W-bound L~f <= p`1 & p`1 <= E-bound L~f
                  & S-bound L~f <= p`2 & p`2 <= N-bound L~f)}
                         by A19,A23,A24,A25,Th54;
        then ex p st p = x & not(W-bound L~f <= p`1 & p`1 <= E-bound L~f
                  & S-bound L~f <= p`2 & p`2 <= N-bound L~f);
        then x in P1 or x in P2 or x in P3 or x in P4;
        then x in P1 \/ P2 or x in P3 \/ P4 by XBOOLE_0:def 2;
       hence thesis by XBOOLE_0:def 2;
      end;
    let x be set;
    assume x in P1 \/ P2 \/ (P3 \/ P4);
     then A27:   x in P1 \/ P2 or x in P3 \/ P4 by XBOOLE_0:def 2;
    per cases by A27,XBOOLE_0:def 2;
    suppose x in P1;
     then ex p st x = p & p`2 < S-bound L~f;
    hence x in LeftComp SpStSeq L~f by A24,Th57;
    suppose x in P2;
     then ex p st x = p & p`2 > N-bound L~f;
    hence x in LeftComp SpStSeq L~f by A19,Th57;
    suppose x in P3;
     then ex p st x = p & p`1 > E-bound L~f;
    hence x in LeftComp SpStSeq L~f by A25,Th57;
    suppose x in P4;
     then ex p st x = p & p`1 < W-bound L~f;
    hence x in LeftComp SpStSeq L~f by A23,Th57;
   end;
     for p st p in P1 holds p`2 < (GoB f)*(1,1)`2
    proof let p;
     assume p in P1;
      then ex q st p = q & q`2 < S-bound L~f;
     hence p`2 < (GoB f)*(1,1)`2 by JORDAN5D:40;
    end;
then A28: P1 misses L~f by GOBOARD8:23;
      for p st p in P2 holds p`2 > (GoB f)*(1, width GoB f)`2
    proof let p;
     assume p in P2;
      then ex q st p = q & q`2 > N-bound L~f;
     hence p`2 > (GoB f)*(1,width GoB f)`2 by JORDAN5D:42;
    end;
    then P2 misses L~f by GOBOARD8:24;
then A29: P1 \/ P2 misses L~f by A28,XBOOLE_1:70;
      for p st p in P3 holds p`1 > (GoB f)*(len GoB f,1)`1
     proof let p;
      assume p in P3;
       then ex q st p = q & q`1 > E-bound L~f;
      hence p`1 > (GoB f)*(len GoB f,1)`1 by JORDAN5D:41;
     end;
then A30: P3 misses L~f by GOBOARD8:22;
    for p st p in P4 holds p`1 < (GoB f)*(1,1)`1
     proof let p;
      assume p in P4;
       then ex q st p = q & q`1 < W-bound L~f;
      hence p`1 < (GoB f)*(1,1)`1 by JORDAN5D:39;
     end;
  then P4 misses L~f by GOBOARD8:21;
  then P3 \/ P4 misses L~f by A30,XBOOLE_1:70;
  then LeftComp SpStSeq L~f misses L~f by A26,A29,XBOOLE_1:70;
  then LeftComp SpStSeq L~f c= (L~f)` by SUBSET_1:43;
 hence LeftComp SpStSeq L~f c= LeftComp f by A2,A5,A22,GOBOARD9:6;
end;

begin :: In the area

theorem Th59:
 for f being FinSequence of TOP-REAL 2,
     p,q being Point of TOP-REAL 2 holds <*p,q*> is_in_the_area_of f
  iff <*p*> is_in_the_area_of f &
        <*q*> is_in_the_area_of f
proof let f be FinSequence of TOP-REAL 2,
          p,q be Point of TOP-REAL 2;
 thus <*p,q*> is_in_the_area_of f
      implies <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f
  proof assume
A1:  <*p,q*> is_in_the_area_of f;
      dom<*p,q*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
    then 1 in dom<*p,q*> & <*p,q*>/.1 = p & 2 in
 dom<*p,q*> & <*p,q*>/.2 = q by FINSEQ_4:26,TARSKI:def 2;
    then A2:  W-bound L~f <= p`1 & p`1 <= E-bound L~f &
    S-bound L~f <= p`2 & p`2 <= N-bound L~f &
    W-bound L~f <= q`1 & q`1 <= E-bound L~f &
    S-bound L~f <= q`2 & q`2 <= N-bound L~f by A1,SPRECT_2:def 1;
   thus <*p*> is_in_the_area_of f
    proof let i;
     assume i in dom<*p*>;
      then i in {1} by FINSEQ_1:4,55;
      then i = 1 by TARSKI:def 1;
     hence thesis by A2,FINSEQ_4:25;
    end;
   let i;
   assume i in dom<*q*>;
    then i in {1} by FINSEQ_1:4,55;
    then i = 1 by TARSKI:def 1;
   hence thesis by A2,FINSEQ_4:25;
  end;
 assume
A3:  <*p*> is_in_the_area_of f;
     dom<*p*> = {1} by FINSEQ_1:4,55;
   then 1 in dom<*p*> & <*p*>/.1 = p by FINSEQ_4:25,TARSKI:def 1;
  then A4: W-bound L~f <= p`1 & p`1 <= E-bound L~f &
    S-bound L~f <= p`2 & p`2 <= N-bound L~f by A3,SPRECT_2:def 1;
 assume
A5: <*q*> is_in_the_area_of f;
     dom<*q*> = {1} by FINSEQ_1:4,55;
   then 1 in dom<*q*> & <*q*>/.1 = q by FINSEQ_4:25,TARSKI:def 1;
  then A6: W-bound L~f <= q`1 & q`1 <= E-bound L~f &
    S-bound L~f <= q`2 & q`2 <= N-bound L~f by A5,SPRECT_2:def 1;
 let i;
 assume i in dom<*p,q*>;
  then i in {1,2} by FINSEQ_1:4,FINSEQ_3:29;
  then i =1 or i =2 by TARSKI:def 2;
 hence thesis by A4,A6,FINSEQ_4:26;
end;

theorem Th60:
 for f being rectangular FinSequence of TOP-REAL 2,
     p being Point of TOP-REAL 2
  st <*p*> is_in_the_area_of f &
     (p`1 = W-bound L~f or p`1 = E-bound L~f or
      p`2 = S-bound L~f or p`2 = N-bound L~f)
  holds p in L~f
proof let f be rectangular FinSequence of TOP-REAL 2,
          p be Point of TOP-REAL 2;
 assume
A1: <*p*> is_in_the_area_of f;
     dom<*p*> = {1} by FINSEQ_1:4,55;
   then 1 in dom<*p*> & <*p*>/.1 = p by FINSEQ_4:25,TARSKI:def 1;
  then A2: W-bound L~f <= p`1 & p`1 <= E-bound L~f &
    S-bound L~f <= p`2 & p`2 <= N-bound L~f by A1,SPRECT_2:def 1;
  consider D being non vertical non horizontal non empty compact
                      Subset of TOP-REAL 2
           such that
A3:  f = SpStSeq D by SPRECT_1:def 2;
A4: L~f = (LSeg(NW-corner D,NE-corner D) \/ LSeg(NE-corner D,SE-corner D)) \/
         (LSeg(SE-corner D,SW-corner D) \/ LSeg(SW-corner D,NW-corner D))
          by A3,SPRECT_1:43;
A5: W-bound L~SpStSeq D = W-bound D by SPRECT_1:66;
A6: S-bound L~SpStSeq D = S-bound D by SPRECT_1:67;
A7: N-bound L~SpStSeq D = N-bound D by SPRECT_1:68;
A8: E-bound L~SpStSeq D = E-bound D by SPRECT_1:69;
  assume
A9: p`1 = W-bound L~f or p`1 = E-bound L~f or
    p`2 = S-bound L~f or p`2 = N-bound L~f;
  per cases by A9;
  suppose
A10:  p`1 = W-bound L~f;
A11: (SW-corner D)`1 = W-bound D & (NW-corner D)`1 = W-bound D
                  by PSCOMP_1:72,74;
     (SW-corner D)`2 = S-bound D & (NW-corner D)`2 = N-bound D
       by PSCOMP_1:73,75;
   then p in
 LSeg(SW-corner D,NW-corner D) by A2,A3,A5,A6,A7,A10,A11,GOBOARD7:8;
   then p in LSeg(SE-corner D,SW-corner D) \/ LSeg(SW-corner D,NW-corner D)
       by XBOOLE_0:def 2;
 hence p in L~f by A4,XBOOLE_0:def 2;
  suppose
A12:  p`1 = E-bound L~f;
A13: (NE-corner D)`1 = E-bound D & (SE-corner D)`1 = E-bound D
            by PSCOMP_1:76,78;
     (NE-corner D)`2 = N-bound D & (SE-corner D)`2 = S-bound D
            by PSCOMP_1:77,79;
   then p in
 LSeg(NE-corner D,SE-corner D) by A2,A3,A6,A7,A8,A12,A13,GOBOARD7:8;
   then p in LSeg(NW-corner D,NE-corner D) \/ LSeg(NE-corner D,SE-corner D)
       by XBOOLE_0:def 2;
 hence p in L~f by A4,XBOOLE_0:def 2;
  suppose
A14:  p`2 = S-bound L~f;
A15: (SE-corner D)`1 = E-bound D & (SW-corner D)`1 = W-bound D
      by PSCOMP_1:72,78;
     (SE-corner D)`2 = S-bound D & (SW-corner D)`2 = S-bound D
               by PSCOMP_1:73,79;
   then p in
 LSeg(SE-corner D,SW-corner D) by A2,A3,A5,A6,A8,A14,A15,GOBOARD7:9;
   then p in LSeg(SE-corner D,SW-corner D) \/ LSeg(SW-corner D,NW-corner D)
       by XBOOLE_0:def 2;
 hence p in L~f by A4,XBOOLE_0:def 2;
  suppose
A16:  p`2 = N-bound L~f;
A17: (NW-corner D)`1 = W-bound D & (NE-corner D)`1 = E-bound D
          by PSCOMP_1:74,76;
     (NW-corner D)`2 = N-bound D & (NE-corner D)`2 = N-bound D
                   by PSCOMP_1:75,77;
   then p in
 LSeg(NW-corner D,NE-corner D) by A2,A3,A5,A7,A8,A16,A17,GOBOARD7:9;
   then p in LSeg(NW-corner D,NE-corner D) \/ LSeg(NE-corner D,SE-corner D)
       by XBOOLE_0:def 2;
 hence p in L~f by A4,XBOOLE_0:def 2;
end;

theorem Th61:
 for f being FinSequence of TOP-REAL 2,
    p,q being Point of TOP-REAL 2, r being Real
 st 0<=r & r <= 1 & <*p,q*> is_in_the_area_of f
 holds <*(1-r)*p+r*q*> is_in_the_area_of f
proof
 let f be FinSequence of TOP-REAL 2,
     p,q be Point of TOP-REAL 2, r be Real such that
A1: 0 <= r and
A2: r <= 1 and
A3: <*p,q*> is_in_the_area_of f;
      dom<*p,q*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
    then 1 in dom<*p,q*> & <*p,q*>/.1 = p & 2 in
 dom<*p,q*> & <*p,q*>/.2 = q by FINSEQ_4:26,TARSKI:def 2;
    then A4:  W-bound L~f <= p`1 & p`1 <= E-bound L~f &
    S-bound L~f <= p`2 & p`2 <= N-bound L~f &
    W-bound L~f <= q`1 & q`1 <= E-bound L~f &
    S-bound L~f <= q`2 & q`2 <= N-bound L~f by A3,SPRECT_2:def 1;
 let n;
 assume
A5: n in dom <*(1-r)*p+r*q*>;
     dom <*(1-r)*p+r*q*> = {1} by FINSEQ_1:4,55;
  then A6: n = 1 by A5,TARSKI:def 1;
A7: ((1-r)*p+r*q)`1 = ((1-r)*p)`1+(r*q)`1 by TOPREAL3:7
        .= (1-r)*p`1+(r*q)`1 by TOPREAL3:9
        .= (1-r)*p`1+r*q`1 by TOPREAL3:9;
A8: (1-r)*W-bound L~f+r*W-bound L~f = ((1-r)+r)*W-bound L~f by XCMPLX_1:8
        .= 1*W-bound L~f by XCMPLX_1:27;
A9: r*W-bound L~f <= r*q`1 by A1,A4,AXIOMS:25;
A10: 1-r >= 0 by A2,SQUARE_1:12;
   then (1-r)*W-bound L~f <= (1-r)*p`1 by A4,AXIOMS:25;
   then W-bound L~f <= (1-r)*p`1+r*q`1 by A8,A9,REAL_1:55;
 hence W-bound L~f <= (<*(1-r)*p+r*q*>/.n)`1 by A6,A7,FINSEQ_4:25;
A11: (1-r)*E-bound L~f+r*E-bound L~f = ((1-r)+r)*E-bound L~f by XCMPLX_1:8
        .= 1*E-bound L~f by XCMPLX_1:27;
A12:  r*q`1<= r*E-bound L~f by A1,A4,AXIOMS:25;
     (1-r)*p`1 <= (1-r)*E-bound L~f by A4,A10,AXIOMS:25;
   then (1-r)*p`1+r*q`1 <= E-bound L~f by A11,A12,REAL_1:55;
 hence (<*(1-r)*p+r*q*>/.n)`1 <= E-bound L~f by A6,A7,FINSEQ_4:25;
A13: ((1-r)*p+r*q)`2 = ((1-r)*p)`2+(r*q)`2 by TOPREAL3:7
        .= (1-r)*p`2+(r*q)`2 by TOPREAL3:9
        .= (1-r)*p`2+r*q`2 by TOPREAL3:9;
A14: (1-r)*S-bound L~f+r*S-bound L~f = ((1-r)+r)*S-bound L~f by XCMPLX_1:8
        .= 1*S-bound L~f by XCMPLX_1:27;
A15: r*S-bound L~f <= r*q`2 by A1,A4,AXIOMS:25;
     (1-r)*S-bound L~f <= (1-r)*p`2 by A4,A10,AXIOMS:25;
   then S-bound L~f <= (1-r)*p`2+r*q`2 by A14,A15,REAL_1:55;
 hence S-bound L~f <= (<*(1-r)*p+r*q*>/.n)`2 by A6,A13,FINSEQ_4:25;
A16: (1-r)*N-bound L~f+r*N-bound L~f = ((1-r)+r)*N-bound L~f by XCMPLX_1:8
        .= 1*N-bound L~f by XCMPLX_1:27;
A17:  r*q`2<= r*N-bound L~f by A1,A4,AXIOMS:25;
     (1-r)*p`2 <= (1-r)*N-bound L~f by A4,A10,AXIOMS:25;
   then (1-r)*p`2+r*q`2 <= N-bound L~f by A16,A17,REAL_1:55;
 hence (<*(1-r)*p+r*q*>/.n)`2 <= N-bound L~f by A6,A13,FINSEQ_4:25;
end;

theorem Th62:
 for f, g being FinSequence of TOP-REAL 2
  st g is_in_the_area_of f & i in dom g
 holds <*g/.i*> is_in_the_area_of f
proof
 let f, g be FinSequence of TOP-REAL 2 such that
A1: g is_in_the_area_of f and
A2:  i in dom g;
 let n;
 assume
A3: n in dom <*g/.i*>;
     dom <*g/.i*> = {1} by FINSEQ_1:4,55;
   then n = 1 by A3,TARSKI:def 1;
   then <*g/.i*>/.n = g/.i by FINSEQ_4:25;
 hence thesis by A1,A2,SPRECT_2:def 1;
end;

theorem Th63:
 for f, g being FinSequence of TOP-REAL 2,
     p being Point of TOP-REAL 2
  st g is_in_the_area_of f & p in L~g
 holds <*p*> is_in_the_area_of f
proof
 let f, g be FinSequence of TOP-REAL 2,
     p be Point of TOP-REAL 2 such that
A1: g is_in_the_area_of f;
 assume p in L~g;
  then consider i such that
A2: 1 <= i and
A3: i+1 <= len g and
A4: p in LSeg(g/.i,g/.(i+1)) by SPPOL_2:14;
    i <= i+1 by NAT_1:29;
  then i <= len g by A3,AXIOMS:22;
  then i in dom g by A2,FINSEQ_3:27;
  then A5: <*g/.i*> is_in_the_area_of f by A1,Th62;
    1 <= i+1 by NAT_1:29;
  then i+1 in dom g by A3,FINSEQ_3:27;
  then <*g/.(i+1)*> is_in_the_area_of f by A1,Th62;
  then A6: <*g/.i,g/.(i+1)*> is_in_the_area_of f by A5,Th59;
    ex r being Real st
    0<=r & r<=1 & p = (1-r)*g/.i+r*g/.(i+1) by A4,SPPOL_1:21;
 hence thesis by A6,Th61;
end;

theorem Th64:
 for f being rectangular FinSequence of TOP-REAL 2,
     p,q being Point of TOP-REAL 2
  st not q in L~f & <*p,q*> is_in_the_area_of f
 holds LSeg(p,q) /\ L~f c= {p}
proof
 let f be rectangular FinSequence of TOP-REAL 2,
     p,q be Point of TOP-REAL 2 such that
A1: not q in L~f;
 assume
A2: <*p,q*> is_in_the_area_of f;
   then <*q*> is_in_the_area_of f by Th59;
   then A3:  q`1 <> W-bound L~f & q`1 <> E-bound L~f &
      q`2 <> S-bound L~f & q`2 <> N-bound L~f by A1,Th60;
A4: dom <*p,q*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
  then A5: 1 in dom <*p,q*> by TARSKI:def 2;
A6: <*p,q*>/.1 = p by FINSEQ_4:26;
then A7: W-bound L~f <= p`1 & p`1 <= E-bound L~f by A2,A5,SPRECT_2:def 1;
A8: S-bound L~f <= p`2 & p`2 <= N-bound L~f by A2,A5,A6,SPRECT_2:def 1;
A9: 2 in dom <*p,q*> by A4,TARSKI:def 2;
A10: <*p,q*>/.2 = q by FINSEQ_4:26;
 then W-bound L~f <= q`1 & q`1 <= E-bound L~f by A2,A9,SPRECT_2:def 1;
 then A11: W-bound L~f < q`1 & q`1 < E-bound L~f by A3,REAL_1:def 5;
   S-bound L~f <= q`2 & q`2 <= N-bound L~f by A2,A9,A10,SPRECT_2:def 1;
 then A12: S-bound L~f < q`2 & q`2 < N-bound L~f by A3,REAL_1:def 5;
 let x be set;
 assume
A13: x in LSeg(p,q) /\ L~f;
  then A14: x in LSeg(p,q) by XBOOLE_0:def 3;
  reconsider p' = x as Point of TOP-REAL 2 by A13;
  consider r being Real such that
A15: 0<=r and
A16: r<=1 and
A17: p' = (1-r)*p+r*q by A14,SPPOL_1:21;
A18: p'`1 = ((1-r)*p)`1+(r*q)`1 by A17,TOPREAL3:7
       .= (1-r)*p`1+(r*q)`1 by TOPREAL3:9
       .= (1-r)*p`1+r*q`1 by TOPREAL3:9;
A19: p'`2 = ((1-r)*p)`2+(r*q)`2 by A17,TOPREAL3:7
       .= (1-r)*p`2+(r*q)`2 by TOPREAL3:9
       .= (1-r)*p`2+r*q`2 by TOPREAL3:9;
A20: p' in L~f by A13,XBOOLE_0:def 3;
 per cases by A20,Th49;
 suppose p'`1 = W-bound L~f;
  then r = 0 by A7,A11,A15,A16,A18,Th4;
  then p' = 1*p+0.REAL 2 by A17,EUCLID:33
   .= 1*p by EUCLID:31
   .= p by EUCLID:33;
 hence x in {p} by ZFMISC_1:37;
 suppose p'`1 = E-bound L~f;
  then r = 0 by A7,A11,A15,A16,A18,Th3;
  then p' = 1*p+0.REAL 2 by A17,EUCLID:33
   .= 1*p by EUCLID:31
   .= p by EUCLID:33;
 hence x in {p} by ZFMISC_1:37;
 suppose p'`2 = S-bound L~f;
  then r = 0 by A8,A12,A15,A16,A19,Th4;
  then p' = 1*p+0.REAL 2 by A17,EUCLID:33
   .= 1*p by EUCLID:31
   .= p by EUCLID:33;
 hence x in {p} by ZFMISC_1:37;
 suppose p'`2 = N-bound L~f;
  then r = 0 by A8,A12,A15,A16,A19,Th3;
  then p' = 1*p+0.REAL 2 by A17,EUCLID:33
   .= 1*p by EUCLID:31
   .= p by EUCLID:33;
 hence x in {p} by ZFMISC_1:37;
end;

theorem
   for f being rectangular FinSequence of TOP-REAL 2,
     p,q being Point of TOP-REAL 2
  st p in L~f & not q in L~f & <*q*> is_in_the_area_of f
 holds LSeg(p,q) /\ L~f = {p}
proof
 let f be rectangular FinSequence of TOP-REAL 2,
     p,q be Point of TOP-REAL 2 such that
A1: p in L~f and
A2: not q in L~f and
A3: <*q*> is_in_the_area_of f;
     f is_in_the_area_of f by SPRECT_2:25;
then A4: <*p*> is_in_the_area_of f by A1,Th63;
     <*p,q*> = <*p*>^<*q*> by FINSEQ_1:def 9;
   then <*p,q*> is_in_the_area_of f by A3,A4,SPRECT_2:28;
 hence LSeg(p,q) /\ L~f c= {p} by A2,Th64;
    p in LSeg(p,q) by TOPREAL1:6;
  then p in LSeg(p,q) /\ L~f by A1,XBOOLE_0:def 3;
 hence {p} c= LSeg(p,q) /\ L~f by ZFMISC_1:37;
end;

theorem Th66:
 for f being non constant standard special_circular_sequence
   st 1 <= i & i <= len GoB f & 1 <= j & j <= width GoB f
 holds <*(GoB f)*(i,j)*> is_in_the_area_of f
proof
 let f be non constant standard special_circular_sequence such that
A1: 1 <= i & i <= len GoB f & 1 <= j & j <= width GoB f;
   set p = (GoB f)*(i,j);
  let n;
  assume n in dom<*(GoB f)*(i,j)*>;
   then n in {1} by FINSEQ_1:4,55;
   then n = 1 by TARSKI:def 1;
   then A2:  <*p*>/.n = p by FINSEQ_4:25;
   set G = GoB f;
A3: 1 <= len G by A1,AXIOMS:22;
A4: 1 <= width G by A1,AXIOMS:22;
A5: W-bound L~f = G*(1,1)`1 by JORDAN5D:39
              .= G*(1,j)`1 by A1,A3,GOBOARD5:3;
A6: i = 1 or i > 1 by A1,REAL_1:def 5;
A7: S-bound L~f = (G)*(1,1)`2 by JORDAN5D:40
              .= (G)*(i,1)`2 by A1,A4,GOBOARD5:2;
A8: j = 1 or j > 1 by A1,REAL_1:def 5;
A9: E-bound L~f = (G)*(len G,1)`1 by JORDAN5D:41
              .= (G)*(len G,j)`1 by A1,A3,GOBOARD5:3;
A10: i = len G or i < len G by A1,REAL_1:def 5;
A11: N-bound L~f = (G)*(1,width G)`2 by JORDAN5D:42
              .= (G)*(i,width G)`2 by A1,A4,GOBOARD5:2;
     j = width G or j < width G by A1,REAL_1:def 5;
  hence thesis by A2,A5,A6,A7,A8,A9,A10,A11,GOBOARD5:4,5;
end;

theorem
   for g being FinSequence of TOP-REAL 2,
     p,q being Point of TOP-REAL 2
  st <*p,q*> is_in_the_area_of g
  holds <*1/2*(p+q)*> is_in_the_area_of g
proof
 let g be FinSequence of TOP-REAL 2,
     p,q be Point of TOP-REAL 2;
    1/2*(p+q) = (1 - 1/2)*p + 1/2*q by EUCLID:36;
 hence thesis by Th61;
end;

theorem
   for f, g being FinSequence of TOP-REAL 2 st g is_in_the_area_of f
   holds Rev g is_in_the_area_of f
proof
 let f, g be FinSequence of TOP-REAL 2 such that
A1: g is_in_the_area_of f;
A2: Rev Rev g = g by FINSEQ_6:29;
A3: len Rev g = len g by FINSEQ_5:def 3;
 let n such that
A4: n in dom Rev g;
  set i = len g + 1 -' n;
A5: n <= len g by A3,A4,FINSEQ_3:27;
    len g <= len g + 1 by NAT_1:29;
  then n <= len g + 1 by A5,AXIOMS:22;
  then n + i = len g + 1 by AMI_5:4;
  then A6: (Rev g)/.n = g/.i by A2,A3,A4,FINSEQ_5:69;
A7: i = len g -' n + 1 by A5,JORDAN4:3;
then A8: 1 <= i by NAT_1:29;
A9: i = len g - n + 1 by A5,A7,SCMFSA_7:3
   .= len g - (n-1) by XCMPLX_1:37;
    n >= 1 by A4,FINSEQ_3:27;
  then n-1 >= 0 by SQUARE_1:12;
  then i <= len g - 0 by A9,REAL_1:92;
  then i in dom g by A8,FINSEQ_3:27;
 hence W-bound L~f <= ((Rev g)/.n)`1 & ((Rev g)/.n)`1 <= E-bound L~f &
   S-bound L~f <= ((Rev g)/.n)`2 & ((Rev g)/.n)`2 <= N-bound L~f
          by A1,A6,SPRECT_2:def 1;
end;

theorem
   for f, g being FinSequence of TOP-REAL 2,
     p being Point of TOP-REAL 2
   st g is_in_the_area_of f & <*p*> is_in_the_area_of f &
     g is_S-Seq & p in L~g
   holds R_Cut(g,p) is_in_the_area_of f
proof
 let f, g be FinSequence of TOP-REAL 2,
     p be Point of TOP-REAL 2 such that
A1: g is_in_the_area_of f and
A2: <*p*> is_in_the_area_of f and
A3:  g is_S-Seq;
      2 <= len g by A3,TOPREAL1:def 10;
    then A4:  1 <= len g by AXIOMS:22;
then A5: 1 in dom g by FINSEQ_3:27;
    assume p in L~g;
    then 1<=Index(p,g) & Index(p,g) < len g by JORDAN3:41;
then A6: Index(p,g) in dom g by FINSEQ_3:27;
 per cases;
 suppose p<>g.1;
  then A7: R_Cut(g,p) = mid(g,1,Index(p,g))^<*p*> by JORDAN3:def 5;
    mid(g,1,Index(p,g)) is_in_the_area_of f by A1,A5,A6,SPRECT_2:26;
 hence R_Cut(g,p) is_in_the_area_of f by A2,A7,SPRECT_2:28;
 suppose p=g.1;
  then R_Cut(g,p) = <*g.1*> by JORDAN3:def 5
            .= <*g/.1*> by A5,FINSEQ_4:def 4
            .= mid(g,1,1) by A4,JORDAN4:27;
 hence R_Cut(g,p) is_in_the_area_of f by A1,A5,SPRECT_2:26;
end;

theorem
   for f being non constant standard special_circular_sequence,
     g being FinSequence of TOP-REAL2
   holds g is_in_the_area_of f iff g is_in_the_area_of SpStSeq L~f
proof
 let f be non constant standard special_circular_sequence,
     g be FinSequence of TOP-REAL2;
A1: W-bound L~SpStSeq L~f = W-bound L~f &
   S-bound L~SpStSeq L~f = S-bound L~f &
   N-bound L~SpStSeq L~f = N-bound L~f &
   E-bound L~SpStSeq L~f = E-bound L~f by SPRECT_1:66,67,68,69;
 thus g is_in_the_area_of f implies g is_in_the_area_of SpStSeq L~f
  proof assume
A2: g is_in_the_area_of f;
   let n; thus thesis by A1,A2,SPRECT_2:def 1;
  end;
 assume
A3: g is_in_the_area_of SpStSeq L~f;
   let n; thus thesis by A1,A3,SPRECT_2:def 1;
end;

theorem
   for f being rectangular special_circular_sequence,
     g being S-Sequence_in_R2
   st g/.1 in LeftComp f & g/.len g in RightComp f
 holds L_Cut(g,Last_Point(L~g,g/.1,g/.len g,L~f)) is_in_the_area_of f
proof
 let f be rectangular special_circular_sequence,
     g be S-Sequence_in_R2 such that
A1: g/.1 in LeftComp f and
A2: g/.len g in RightComp f;
  set lp = Last_Point(L~g,g/.1,g/.len g,L~f),
      ilp = Index(lp,g),
      h = L_Cut(g,lp);
A3: L~f misses LeftComp f by Th43;
A4: L~g meets L~f by A1,A2,Th50;
A5: L~g is closed & L~f is closed by SPPOL_1:49;
then A6: L~g /\ L~f is closed by TOPS_1:35;
      L~g is_an_arc_of g/.1,g/.len g by TOPREAL1:31;
    then A7: lp in L~g /\ L~f by A4,A6,JORDAN5C:def 2;
then A8: lp in L~f by XBOOLE_0:def 3;
A9:   lp in L~g by A7,XBOOLE_0:def 3;
A10: len g in dom g by FINSEQ_5:6;
     1 in dom g by FINSEQ_5:6;
then A11: len g >= 1 by FINSEQ_3:27;
A12: lp in LSeg(g,ilp) by A9,JORDAN3:42;
 given n such that
A13: n in dom h and
A14: W-bound L~f > (h/.n)`1 or (h/.n)`1 > E-bound L~f or
   S-bound L~f > (h/.n)`2 or (h/.n)`2 > N-bound L~f;
    LeftComp f = {p : not(W-bound L~f <= p`1 & p`1 <= E-bound L~f
                  & S-bound L~f <= p`2 & p`2 <= N-bound L~f)} by Th54;
  then A15: h/.n in LeftComp f by A14;
A16: 1 <= n & n <= len h by A13,FINSEQ_3:27;
  then A17: n = n -'1 +1 by AMI_5:4;
A18: len<*lp*> = 1 by FINSEQ_1:56;
A19: ilp < len g by A9,JORDAN3:41;
    then A20: ilp+1<=len g by NAT_1:38;
A21: 1<=ilp+1 by NAT_1:29;
    then A22:   len mid(g,ilp+1,len g)=len g-'(ilp+1)+1 by A20,JORDAN4:20
            .= len g -' ilp by A19,NAT_2:9;
    then A23:  ilp + len mid(g,ilp+1,len g) + 1 = len g + 1 by A19,AMI_5:4;
A24: ilp+1 in dom g by A20,A21,FINSEQ_3:27;
A25: n+ilp <= len h + ilp by A16,AXIOMS:24;
A26: LeftComp f misses RightComp f by SPRECT_1:96;
A27: 1 <= ilp by A9,JORDAN3:41;

    now
   assume
A28:   n = 1;
   per cases;
   suppose lp <> g.(ilp+1);
    then h = <*lp*>^mid(g,ilp+1,len g) by JORDAN3:def 4;
    then h/.n = lp by A28,FINSEQ_5:16;
   hence contradiction by A3,A8,A15,XBOOLE_0:3;
   suppose
A29:  lp = g.(ilp+1);
    then h = mid(g,ilp+1,len g) by JORDAN3:def 4;
    then h/.n = g/.(1+(ilp+1)-'1) by A10,A13,A20,A24,A28,SPRECT_2:7
           .= g/.(ilp+1) by BINARITH:39
           .= lp by A24,A29,FINSEQ_4:def 4;
   hence contradiction by A3,A8,A15,XBOOLE_0:3;
  end;
  then A30: n > 1 by A16,AXIOMS:21;
  then A31: 1+1 < ilp+n by A27,REAL_1:67;
  then A32: 1 <= ilp+n-'1 by JORDAN3:12;
A33: ilp+n-'1 = ilp+(n-'1) by A16,JORDAN4:3;
A34: 1 <= n-'1 by A17,A30,NAT_1:38;
   now assume
A35:  lp <> g.(ilp+1);
  then A36: h = <*lp*>^mid(g,ilp+1,len g) by JORDAN3:def 4;
then A37: len h = 1 + len mid(g,ilp+1,len g) by A18,FINSEQ_1:35;
    then len h -' 1 = len mid(g,ilp+1,len g) by BINARITH:39;
    then A38:  n-'1 <= len mid(g,ilp+1,len g) by A16,JORDAN3:5;
then A39: h/.n = (mid(g,ilp+1,len g))/.(n-'1) by A17,A18,A34,A36,GOBOARD2:5;
A40:  ilp + len h = len g + 1 by A23,A37,XCMPLX_1:1;
     n-'1 in dom mid(g,ilp+1,len g) by A34,A38,FINSEQ_3:27;
   then A41: h/.n = g/.(n-'1+(ilp+1)-'1) by A10,A20,A24,A39,SPRECT_2:7
          .= g/.(n+ilp-'1) by A17,XCMPLX_1:1;
A42: ilp+n-'1 <= len g by A25,A40,Th6;
A43: ilp+n-'1<>len g by A2,A15,A26,A41,XBOOLE_0:3;
  then reconsider m = mid(g,ilp+n-'1,len g) as S-Sequence_in_R2
             by A11,A32,A42,JORDAN3:39;
A44: ilp+n-'1 in dom g by A32,A42,FINSEQ_3:27;
then A45: m/.1 in LeftComp f by A10,A15,A41,SPRECT_2:12;
    m/.len m in RightComp f by A2,A10,A44,SPRECT_2:13;
  then L~f meets L~m by A45,Th50;
  then consider q being set such that
A46: q in L~f and
A47: q in L~m by XBOOLE_0:3;
  reconsider q as Point of TOP-REAL 2 by A47;
  consider i such that
A48: 1 <= i & i+1 <= len m and
A49: q in LSeg(m,i) by A47,SPPOL_2:13;
A50: len m = len g-'(ilp+n-'1)+1 by A32,A42,JORDAN4:20;
A51:  i < len m by A48,NAT_1:38;
      ilp+n-'1<len g by A42,A43,AXIOMS:21;
  then A52: LSeg(m,i)=LSeg(g,i+(ilp+n-'1)-'1) by A32,A48,A50,A51,JORDAN4:31;
  set j = i+(ilp+n-'1)-'1;
      j = i-'1+(ilp+n-'1) by A48,JORDAN4:3;
  then A53: j >= ilp+n-'1 by NAT_1:29;
     ilp+1 <= ilp+n-'1 by A33,A34,AXIOMS:24;
   then A54: ilp +1 <= j by A53,AXIOMS:22;
A55: lp <> g/.(ilp+1) by A24,A35,FINSEQ_4:def 4;
A56: 1 <= j by A21,A54,AXIOMS:22;
      i <= len g-'(ilp+n-'1) by A48,A50,REAL_1:53;
    then A57:  i+(ilp+n-'1) <= len g by A42,Th7;
      i <= i+(ilp+n-'1) by NAT_1:29;
    then 1 <= i+(ilp+n-'1) by A48,AXIOMS:22;
then A58: j + 1 <= len g by A57,AMI_5:4;
    now assume lp = q;
then A59: lp in LSeg(g,ilp) /\ LSeg(g,j) by A12,A49,A52,XBOOLE_0:def 3;
then A60: LSeg(g,ilp) meets LSeg(g,j) by XBOOLE_0:4;
   per cases by A54,AXIOMS:21;
   suppose
A61:  ilp+1 = j;
    then ilp + (1+1) <= len g by A58,XCMPLX_1:1;
    then LSeg(g,ilp) /\ LSeg(g,ilp+1) = {g/.(ilp+1)} by A27,TOPREAL1:def 8;
   hence contradiction by A55,A59,A61,TARSKI:def 1;
   suppose ilp+1 < j;
   hence contradiction by A60,TOPREAL1:def 9;
  end;
  then ilp >= j by A4,A5,A12,A20,A27,A46,A49,A52,A56,A58,JORDAN5C:28;
  then ilp >= ilp+1 by A54,AXIOMS:22;
 hence contradiction by REAL_1:69;
 end;
  then A62: h = mid(g,ilp+1,len g) by JORDAN3:def 4;
then A63:  ilp + len h = len g by A19,A22,AMI_5:4;
A64: 1 <= ilp+n by A31,AXIOMS:22;
    then ilp+n -' 1 + 1 = ilp+n by AMI_5:4;
   then A65: ilp+n-'1 < len g by A25,A63,NAT_1:38;
  set m = mid(g,ilp+n,len g);
    m = g/^(ilp+n-'1) by A25,A63,JORDAN3:26;
  then A66: m/.len m in RightComp f by A2,A65,JORDAN4:18;
A67: h/.n = g/.(n+(ilp+1)-'1) by A10,A13,A20,A24,A62,SPRECT_2:7
       .= g/.(n+ilp+1-'1) by XCMPLX_1:1
       .= g/.(ilp+n) by BINARITH:39;
  then A68: ilp+n <> len g by A2,A15,A26,XBOOLE_0:3;
  then reconsider m as S-Sequence_in_R2 by A11,A25,A63,A64,JORDAN3:39;
  ilp+n in dom g by A25,A63,A64,FINSEQ_3:27;
then m/.1 in LeftComp f by A10,A15,A67,SPRECT_2:12;
  then L~f meets L~m by A66,Th50;
  then consider q being set such that
A69: q in L~f and
A70: q in L~m by XBOOLE_0:3;
  reconsider q as Point of TOP-REAL 2 by A70;
  consider i such that
A71: 1 <= i & i+1 <= len m and
A72: q in LSeg(m,i) by A70,SPPOL_2:13;
A73:  ilp+n < len g by A25,A63,A68,AXIOMS:21;
    len m = len g -' (ilp+n) + 1 by A11,A25,A63,A64,JORDAN3:27;
  then A74: i < len g -'(ilp+n) +1 by A71,NAT_1:38;
  then A75: LSeg(m,i) = LSeg(g,i+(ilp+n)-'1) by A64,A71,A73,JORDAN4:31;
  set j = i+(ilp+n)-'1;
A76: j = i-'1+(ilp+n) by A71,JORDAN4:3;
  then A77: j >= ilp+n by NAT_1:29;
    ilp+1 < ilp+n by A30,REAL_1:53;
  then A78: j > ilp+1 by A77,AXIOMS:22;
A79:  now assume lp = q;
    then lp in LSeg(g,ilp) /\ LSeg(g,j) by A12,A72,A75,XBOOLE_0:def 3;
    then LSeg(g,ilp) meets LSeg(g,j) by XBOOLE_0:4;
   hence contradiction by A78,TOPREAL1:def 9;
  end;
    i-'1 < len g-'(ilp+n) by A71,A74,Th7;
  then i-'1+(ilp+n) < len g by Th6;
  then A80: j + 1 <= len g by A76,NAT_1:38;
  1 <= j by A64,A77,AXIOMS:22;
  then ilp >= j by A4,A5,A12,A20,A27,A69,A72,A75,A79,A80,JORDAN5C:28;
  then ilp >= ilp+1 by A78,AXIOMS:22;
 hence contradiction by REAL_1:69;
end;

theorem
   for f being non constant standard special_circular_sequence
     st 1 <= i & i < len GoB f & 1 <= j & j < width GoB f
  holds Int cell(GoB f,i,j) misses L~SpStSeq L~f
proof
 let f be non constant standard special_circular_sequence
  such that
A1: 1 <= i & i < len GoB f and
A2: 1 <= j & j < width GoB f;
  set G = GoB f;
A3: Int cell(G,i,j) = { |[r,s]| where r,s is Real:
       G*(i,1)`1 < r & r < G*(i+1,1)`1 &
                G*(1,j)`2 < s & s < G*(1,j+1)`2 } by A1,A2,GOBOARD6:29;
 assume Int cell(GoB f,i,j) meets L~SpStSeq L~f;
  then consider x being set such that
A4: x in Int cell(GoB f,i,j) and
A5: x in L~SpStSeq L~f by XBOOLE_0:3;
  consider r,s being Real such that
A6: x = |[r,s]| and
A7: G*(i,1)`1 < r & r < G*(i+1,1)`1 and
A8:  G*(1,j)`2 < s & s < G*(1,j+1)`2 by A3,A4;
A9:   1 <= width GoB f by GOBRD11:34;
then A10: <*(GoB f)*(i,1)*> is_in_the_area_of f by A1,Th66;
A11:   1 <= len GoB f by GOBRD11:34;
then A12: <*(GoB f)*(1,j)*> is_in_the_area_of f by A2,Th66;
        1 <= i+1 & i+1 <= len GoB f by A1,NAT_1:38;
then A13: <*(GoB f)*(i+1,1)*> is_in_the_area_of f by A9,Th66;
        1 <= j+1 & j+1 <= width GoB f by A2,NAT_1:38;
then A14: <*(GoB f)*(1,j+1)*> is_in_the_area_of f by A11,Th66;
    L~SpStSeq L~f = { p:
      p`1 = W-bound L~SpStSeq L~f &
      p`2 <= N-bound L~SpStSeq L~f & p`2 >= S-bound L~SpStSeq L~f or
      p`1 <= E-bound L~SpStSeq L~f & p`1 >= W-bound L~SpStSeq L~f &
      p`2 = N-bound L~SpStSeq L~f or
      p`1 <= E-bound L~SpStSeq L~f & p`1 >= W-bound L~SpStSeq L~f &
      p`2 = S-bound L~SpStSeq L~f or
      p`1 = E-bound L~SpStSeq L~f &
      p`2 <= N-bound L~SpStSeq L~f & p`2 >= S-bound L~SpStSeq L~f}
       by Th52;
   then consider p such that
A15:   p = x and
A16:   p`1 = W-bound L~SpStSeq L~f &
      p`2 <= N-bound L~SpStSeq L~f & p`2 >= S-bound L~SpStSeq L~f or
      p`1 <= E-bound L~SpStSeq L~f & p`1 >= W-bound L~SpStSeq L~f &
      p`2 = N-bound L~SpStSeq L~f or
      p`1 <= E-bound L~SpStSeq L~f & p`1 >= W-bound L~SpStSeq L~f &
      p`2 = S-bound L~SpStSeq L~f or
      p`1 = E-bound L~SpStSeq L~f &
      p`2 <= N-bound L~SpStSeq L~f & p`2 >= S-bound L~SpStSeq L~f by A5;
A17: p`1 = r by A6,A15,EUCLID:56;
A18: p`2 = s by A6,A15,EUCLID:56;
A19: W-bound L~SpStSeq L~f = W-bound L~f &
   S-bound L~SpStSeq L~f = S-bound L~f &
   N-bound L~SpStSeq L~f = N-bound L~f &
   E-bound L~SpStSeq L~f = E-bound L~f by SPRECT_1:66,67,68,69;
  per cases by A16;
  suppose
A20: p`1 = W-bound L~SpStSeq L~f;
A21:  <*G*(i,1)*>/.1 = G*(i,1) by FINSEQ_4:25;
      1 in dom<*G*(i,1)*> by FINSEQ_5:6;
   hence contradiction by A7,A10,A17,A19,A20,A21,SPRECT_2:def 1;
  suppose
A22: p`2 = N-bound L~SpStSeq L~f;
A23:  <*G*(1,j+1)*>/.1 = G*(1,j+1) by FINSEQ_4:25;
      1 in dom<*G*(1,j+1)*> by FINSEQ_5:6;
   hence contradiction by A8,A14,A18,A19,A22,A23,SPRECT_2:def 1;
  suppose that
A24: p`2 = S-bound L~SpStSeq L~f;
A25:  <*G*(1,j)*>/.1 = G*(1,j) by FINSEQ_4:25;
      1 in dom<*G*(1,j)*> by FINSEQ_5:6;
   hence contradiction by A8,A12,A18,A19,A24,A25,SPRECT_2:def 1;
  suppose that
A26: p`1 = E-bound L~SpStSeq L~f;
A27:  <*G*(i+1,1)*>/.1 = G*(i+1,1) by FINSEQ_4:25;
      1 in dom<*G*(i+1,1)*> by FINSEQ_5:6;
   hence contradiction by A7,A13,A17,A19,A26,A27,SPRECT_2:def 1;
end;

theorem
   for f, g being FinSequence of TOP-REAL 2,
     p being Point of TOP-REAL 2
   st g is_in_the_area_of f & <*p*> is_in_the_area_of f &
     g is_S-Seq & p in L~g
   holds L_Cut(g,p) is_in_the_area_of f
proof
 let f, g be FinSequence of TOP-REAL 2,
     p be Point of TOP-REAL 2 such that
A1: g is_in_the_area_of f and
A2: <*p*> is_in_the_area_of f and
A3:  g is_S-Seq;
    2 <= len g by A3,TOPREAL1:def 10;
  then 1 <= len g by AXIOMS:22;
  then A4: len g in dom g by FINSEQ_3:27;
 assume p in L~g;
  then Index(p,g) < len g by JORDAN3:41;
  then A5:   Index(p,g)+1 <= len g by NAT_1:38;
      1<=Index(p,g)+1 by NAT_1:29;
    then A6: Index(p,g)+1 in dom g by A5,FINSEQ_3:27;
 per cases;
 suppose p<>g.(Index(p,g)+1);
  then A7: L_Cut(g,p) = <*p*>^mid(g,Index(p,g)+1,len g) by JORDAN3:def 4;
    mid(g,Index(p,g)+1,len g) is_in_the_area_of f by A1,A4,A6,SPRECT_2:26;
 hence L_Cut(g,p) is_in_the_area_of f by A2,A7,SPRECT_2:28;
 suppose p=g.(Index(p,g)+1);
  then L_Cut(g,p) = mid(g,Index(p,g)+1,len g) by JORDAN3:def 4;
 hence L_Cut(g,p) is_in_the_area_of f by A1,A4,A6,SPRECT_2:26;
end;


Back to top