The Mizar article:

Special Polygons

by
Czeslaw Bylinski, and
Yatsuka Nakamura

Received January 30, 1995

Copyright (c) 1995 Association of Mizar Users

MML identifier: SPPOL_2
[ MML identifier index ]


environ

 vocabulary EUCLID, FINSEQ_1, PRE_TOPC, ARYTM, MCART_1, TOPREAL1, FINSEQ_5,
      RELAT_1, FINSEQ_4, BOOLE, RFINSEQ, ARYTM_1, TARSKI, FUNCT_1, REALSET1,
      TOPREAL4, RCOMP_1, COMPTS_1, BORSUK_1, TOPS_2, ORDINAL2, SUBSET_1,
      SPPOL_2;
 notation TARSKI, XBOOLE_0, ORDINAL1, XREAL_0, STRUCT_0, REAL_1, NAT_1,
      FUNCT_1, FINSEQ_1, REALSET1, FINSEQ_4, RFINSEQ, PRE_TOPC, COMPTS_1,
      TOPS_2, EUCLID, BORSUK_1, TOPREAL1, TOPREAL4, FINSEQ_5;
 constructors TOPMETR, REAL_1, NAT_1, REALSET1, RFINSEQ, COMPTS_1, TOPS_2,
      TOPREAL1, TOPREAL4, FINSEQ_4, FINSEQ_5, INT_1, MEMBERED, XBOOLE_0;
 clusters PRE_TOPC, FINSEQ_5, RELSET_1, STRUCT_0, EUCLID, XREAL_0, FINSEQ_1,
      INT_1, TOPREAL1, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, TOPREAL1, TOPREAL4, XBOOLE_0;
 theorems TARSKI, AXIOMS, ENUMSET1, ZFMISC_1, REAL_1, NAT_1, RLVECT_1,
      SQUARE_1, REAL_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, TOPS_2, HEINE,
      TOPMETR, COMPTS_1, RFINSEQ, EUCLID, TOPREAL1, TOPREAL3, TOPREAL4,
      GOBOARD1, GOBOARD2, SPPOL_1, FINSEQ_5, RELAT_1, GROUP_5, PARTFUN2, INT_1,
      XBOOLE_0, XBOOLE_1, XCMPLX_1;
 schemes FINSEQ_2, COMPLSP1;

begin :: Segments in TOP-REAL 2

reserve P for Subset of TOP-REAL 2,
        f,f1,f2,g for FinSequence of TOP-REAL 2,
        p,p1,p2,q,q1,q2 for Point of TOP-REAL 2,
        r1,r2,r1',r2' for Real,
        i,j,k,n for Nat;

theorem Th1:
  for r1, r2, r1', r2' being real number st
   |[ r1,r2 ]| = |[ r1',r2' ]| holds r1 = r1' & r2 = r2'
 proof
  let r1, r2, r1', r2' be real number;
    |[r1,r2]|`1=r1 & |[r1,r2]|`2=r2 & |[r1',r2']|`1=r1' & |[r1',r2']|`2=r2'
    by EUCLID:56;
  hence thesis;
 end;

theorem Th2:
   i+j = len f implies LSeg(f,i) = LSeg(Rev f,j)
 proof assume
A1: i+j = len f;
  per cases;
   suppose that
A2:  1 <= i and
A3:  i + 1 <= len f;
A4:  i in dom f by A2,A3,GOBOARD2:3;
A5:  i+1 in dom f by A2,A3,GOBOARD2:3;
A6: i+(j+1) = len f + 1 by A1,XCMPLX_1:1;
   then j+1 in dom Rev f by A4,FINSEQ_5:62;
then A7:  j+1 <= len Rev f by FINSEQ_3:27;
A8: i+1+j = len f + 1 by A1,XCMPLX_1:1;
   then j in dom Rev f by A5,FINSEQ_5:62;
then A9:  1 <= j by FINSEQ_3:27;
  thus LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A2,A3,TOPREAL1:def 5
                .= LSeg((Rev f)/.(j+1),f/.(i+1)) by A4,A6,FINSEQ_5:69
                .= LSeg((Rev f)/.j,(Rev f)/.(j+1)) by A5,A8,FINSEQ_5:69
                .= LSeg(Rev f,j) by A7,A9,TOPREAL1:def 5;
   suppose
A10:   not 1 <= i;
    then i = 0 by RLVECT_1:98;
    then not j+1 <= len f by A1,NAT_1:38;
    then not j+1 <= len Rev f by FINSEQ_5:def 3;
    then LSeg(f,i) = {} & LSeg(Rev f,j) = {} by A10,TOPREAL1:def 5;
    hence thesis;
   suppose
A11:   not i+1 <= len f;
    then j < 1 by A1,AXIOMS:24;
    then LSeg(f,i) = {} & LSeg(Rev f,j) = {} by A11,TOPREAL1:def 5;
    hence thesis;
 end;

theorem Th3:
   i+1 <= len(f|n) implies LSeg(f|n,i) = LSeg(f,i)
 proof assume
A1:  i+1 <= len(f|n);
  per cases;
  suppose i <> 0;
then A2:  1 <= i by RLVECT_1:99;
then A3:  i in dom(f|n) by A1,GOBOARD2:3;
A4:  i+1 in dom(f|n) by A1,A2,GOBOARD2:3;
     len(f|n) <= len f by FINSEQ_5:18;
then A5: i+1 <= len f by A1,AXIOMS:22;
   thus LSeg(f|n,i) = LSeg((f|n)/.i,(f|n)/.(i+1)) by A1,A2,TOPREAL1:def 5
                   .= LSeg(f/.i,(f|n)/.(i+1)) by A3,TOPREAL1:1
                   .= LSeg(f/.i,f/.(i+1)) by A4,TOPREAL1:1
                   .= LSeg(f,i) by A2,A5,TOPREAL1:def 5;
  suppose
A6: i = 0;
   hence LSeg(f|n,i) = {} by TOPREAL1:def 5
                    .= LSeg(f,i) by A6,TOPREAL1:def 5;
 end;

theorem Th4:
   n <= len f & 1 <= i implies LSeg(f/^n,i) = LSeg(f,n+i)
 proof assume that
A1: n <= len f and
A2: 1 <= i;
 per cases;
 suppose
A3: i+1 <= len f - n;
     1<=i+1 by NAT_1:29;
   then 1 <= len f - n by A3,AXIOMS:22;
then A4: 1+n <= len f by REAL_1:84;
     n <= 1+n by NAT_1:29;
   then n <= len f by A4,AXIOMS:22;
then A5: len(f/^n) = len f - n by RFINSEQ:def 2;
then A6: i in dom(f/^n) by A2,A3,GOBOARD2:3;
A7: i+1 in dom(f/^n) by A2,A3,A5,GOBOARD2:3;
      i <= i+n by NAT_1:29;
then A8: 1 <= i+n by A2,AXIOMS:22;
    i+1+n <= len f by A3,REAL_1:84;
then A9: i+n+1 <= len f by XCMPLX_1:1;
   thus LSeg(f/^n,i)
      = LSeg((f/^n)/.i,(f/^n)/.(i+1)) by A2,A3,A5,TOPREAL1:def 5
     .= LSeg(f/.(i+n),(f/^n)/.(i+1)) by A6,FINSEQ_5:30
     .= LSeg(f/.(i+n),f/.(i+1+n)) by A7,FINSEQ_5:30
     .= LSeg(f/.(i+n),f/.(i+n+1)) by XCMPLX_1:1
     .= LSeg(f,n+i) by A8,A9,TOPREAL1:def 5;
 suppose
A10: i+1 > len f - n;
  then n+(i+1) > len f by REAL_1:84;
then A11: n+i+1 > len f by XCMPLX_1:1;
    i+1 > len(f/^n) by A1,A10,RFINSEQ:def 2;
  hence LSeg(f/^n,i) = {} by TOPREAL1:def 5
                    .= LSeg(f,n+i) by A11,TOPREAL1:def 5;
 end;

theorem Th5:
   1 <= i & i+1 <= len f - n implies LSeg(f/^n,i) = LSeg(f,n+i)
 proof assume
A1: 1 <= i;
  assume i+1 <= len f - n;
then A2: i+1+n <= len f by REAL_1:84;
    n <= i+1+n by NAT_1:29;
  then n <= len f by A2,AXIOMS:22;
  hence thesis by A1,Th4;
 end;

theorem Th6:
   i+1 <= len f implies LSeg(f^g,i) = LSeg(f,i)
 proof assume
A1: i+1 <= len f;
  per cases;
  suppose i <> 0;
then A2: 1 <= i by RLVECT_1:99;
then A3: i in dom f by A1,GOBOARD2:3;
A4: i+1 in dom f by A1,A2,GOBOARD2:3;
     len(f^g) = len f + len g by FINSEQ_1:35;
   then len(f^g) >= len f by NAT_1:29;
then A5: i+1 <= len(f^g) by A1,AXIOMS:22;
   thus LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A1,A2,TOPREAL1:def 5
                 .= LSeg((f^g)/.i,f/.(i+1)) by A3,GROUP_5:95
                 .= LSeg((f^g)/.i,(f^g)/.(i+1)) by A4,GROUP_5:95
                 .= LSeg(f^g,i) by A2,A5,TOPREAL1:def 5;
  suppose
A6:  i = 0;
   hence LSeg(f^g,i) = {} by TOPREAL1:def 5
                    .= LSeg(f,i) by A6,TOPREAL1:def 5;
 end;

theorem Th7:
   1 <= i implies LSeg(f^g,len f + i) = LSeg(g,i)
 proof assume
A1: 1 <= i;
  per cases;
  suppose
A2: i+1 <= len g;
then A3: i in dom g by A1,GOBOARD2:3;
A4: i+1 in dom g by A1,A2,GOBOARD2:3;
     i <= len f+i by NAT_1:29;
then A5: 1 <= len f+i by A1,AXIOMS:22;
A6: len f +(i+1) = len f+i+1 by XCMPLX_1:1;
   then len f +i+1 <= len f + len g by A2,AXIOMS:24;
then A7: len f+i+1 <= len(f^g) by FINSEQ_1:35;
   thus LSeg(g,i) = LSeg(g/.i,g/.(i+1)) by A1,A2,TOPREAL1:def 5
                 .= LSeg((f^g)/.(len f+i),g/.(i+1)) by A3,GROUP_5:96
                 .= LSeg((f^g)/.(len f+i),
(f^g)/.(len f + (i+1))) by A4,GROUP_5:96
                 .= LSeg(f^g,len f + i) by A5,A6,A7,TOPREAL1:def 5;
  suppose
A8:  i+1 > len g;
  then len f + (i + 1) > len f + len g by REAL_1:53;
  then len f + (i + 1) > len(f^g) by FINSEQ_1:35;
  then len f + i + 1 > len(f^g) by XCMPLX_1:1;
  hence LSeg(f^g,len f + i) = {} by TOPREAL1:def 5
                           .= LSeg(g,i) by A8,TOPREAL1:def 5;
 end;

theorem Th8:
  f is non empty & g is non empty
   implies LSeg(f^g,len f) = LSeg(f/.len f,g/.1)
 proof assume that
A1:  f is non empty and
A2:  g is non empty;
A3:  len f in dom f by A1,FINSEQ_5:6;
A4:  1 in dom g by A2,FINSEQ_5:6;
A5:  1 <= len f by A3,FINSEQ_3:27;
     1 <= len g by A4,FINSEQ_3:27;
   then len f + 1 <= len f + len g by AXIOMS:24;
   then len f + 1 <= len(f^g) by FINSEQ_1:35;
   hence LSeg(f^g,len f)
       = LSeg((f^g)/.(len f),(f^g)/.(len f+1)) by A5,TOPREAL1:def 5
      .= LSeg(f/.len f,(f^g)/.(len f+1)) by A3,GROUP_5:95
      .= LSeg(f/.len f,g/.1) by A4,GROUP_5:96;
 end;

theorem Th9:
   i+1 <= len(f-:p) implies LSeg(f-:p,i) = LSeg(f,i)
 proof f-:p = f|(p..f) by FINSEQ_5:def 1;
  hence thesis by Th3;
 end;

theorem Th10:
   p in rng f implies LSeg(f:-p,i+1) = LSeg(f,i+p..f)
 proof assume
A1: p in rng f;
A2: 1 <= i+1 by NAT_1:29;
A3: i+(1+1) = i+1+1 by XCMPLX_1:1;
A4: len (f:-p) = len f - p..f + 1 by A1,FINSEQ_5:53;
  per cases;
  suppose
A5: i+2 <= len(f:-p);
then A6: i+1 in dom(f:-p) by A2,A3,GOBOARD2:3;
A7: i+1+1 in dom(f:-p) by A2,A3,A5,GOBOARD2:3;
     1 <= p..f by A1,FINSEQ_4:31;
   then i+1 <= i+p..f by AXIOMS:24;
then A8: 1 <= i+p..f by A2,AXIOMS:22;
     i+1 <= len f - p..f by A3,A4,A5,REAL_1:53;
   then i+1+p..f <= len f by REAL_1:84;
then A9: i+p..f+1 <= len f by XCMPLX_1:1;
    thus LSeg(f:-p,i+1)
       = LSeg((f:-p)/.(i+1),(f:-p)/.(i+1+1)) by A2,A3,A5,TOPREAL1:def 5
      .= LSeg(f/.(i+p..f),(f:-p)/.(i+1+1)) by A1,A6,FINSEQ_5:55
      .= LSeg(f/.(i+p..f),f/.(i+1+p..f)) by A1,A7,FINSEQ_5:55
      .= LSeg(f/.(i+p..f),f/.(i+p..f+1)) by XCMPLX_1:1
      .= LSeg(f,i+p..f) by A8,A9,TOPREAL1:def 5;
  suppose
A10: i+2 > len(f:-p);
   then i+1 > len f - p..f by A3,A4,AXIOMS:24;
   then p..f+(i+1) > len f by REAL_1:84;
   then i+p..f+1 > len f by XCMPLX_1:1;
   hence LSeg(f,i+p..f) = {} by TOPREAL1:def 5
                       .= LSeg(f:-p,i+1) by A3,A10,TOPREAL1:def 5;
 end;

theorem Th11:
   L~<*>(the carrier of TOP-REAL 2) = {}
 proof len(<*>(the carrier of TOP-REAL 2)) = 0 by FINSEQ_1:32;
  hence thesis by TOPREAL1:28;
 end;

theorem Th12:
   L~<*p*> = {}
 proof len <*p*> = 1 by FINSEQ_1:56;
  hence thesis by TOPREAL1:28;
 end;

theorem Th13:
   p in L~f implies ex i st 1 <= i & i+1 <= len f & p in LSeg(f,i)
 proof assume
A1:  p in L~f;
  set X = { LSeg(f,i) : 1 <= i & i+1 <= len f};
    L~f = union X by TOPREAL1:def 6;
  then consider Y being set such that
A2:  p in Y and
A3:  Y in X by A1,TARSKI:def 4;
    ex i st Y = LSeg(f,i) & 1 <= i & i+1 <= len f by A3;
  hence thesis by A2;
 end;

theorem Th14:
   p in L~f implies ex i st 1 <= i & i+1 <= len f & p in LSeg(f/.i,f/.(i+1))
 proof assume p in L~f;
  then consider i such that
A1:  1 <= i & i+1 <= len f and
A2:  p in LSeg(f,i) by Th13;
  take i;
  thus 1 <= i & i+1 <= len f by A1;
  thus thesis by A1,A2,TOPREAL1:def 5;
 end;

theorem Th15:
   1 <= i & i+1 <= len f & p in LSeg(f/.i,f/.(i+1)) implies p in L~f
 proof assume that
A1:  1 <= i and
A2:  i+1 <= len f and
A3:  p in LSeg(f/.i,f/.(i+1));
  set X = { LSeg(f,j) : 1 <= j & j+1 <= len f };
A4:  LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A1,A2,TOPREAL1:def 5;
    LSeg(f,i) in X by A1,A2;
  then p in union X by A3,A4,TARSKI:def 4;
  hence p in L~f by TOPREAL1:def 6;
 end;

theorem
     1 <= i & i+1 <= len f implies LSeg(f/.i,f/.(i+1)) c= L~f
 proof assume 1 <= i & i+1 <= len f;
  then LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by TOPREAL1:def 5;
  hence thesis by TOPREAL3:26;
 end;

theorem
     p in LSeg(f,i) implies p in L~f
 proof LSeg(f,i) c= L~f by TOPREAL3:26; hence thesis; end;

theorem Th18:
   len f >= 2 implies rng f c= L~f
 proof assume
A1: len f >= 2;
  let x be set;
  assume x in rng f;
  then consider i such that
A2: i in dom f and
A3: f/.i = x by PARTFUN2:4;
A4: 1 <= i by A2,FINSEQ_3:27;
A5: i <= len f by A2,FINSEQ_3:27;
A6: f/.i in LSeg(f/.i,f/.(i+1)) by TOPREAL1:6;
  per cases;
   suppose
A7:  i = len f;
    then i <>0 by A1;
    then consider j such that
A8:  j+1 = i by NAT_1:22;
A9:  f/.(j+1) in LSeg(f/.j,f/.(j+1)) by TOPREAL1:6;
      1+1 <= j+1 by A1,A7,A8;
    then 1 <= j by REAL_1:53;
    hence x in L~f by A3,A7,A8,A9,Th15;
   suppose i <> len f;
    then i < len f by A5,REAL_1:def 5;
    then i+1 <= len f by NAT_1:38;
    hence x in L~f by A3,A4,A6,Th15;
 end;

theorem Th19:
   f is non empty implies L~(f^<*p*>) = L~f \/ LSeg(f/.len f,p)
 proof assume that
A1:  f is non empty;
   set fp = f^<*p*>;
A2: len fp = len f + 1 by FINSEQ_2:19;
    1 <= len f + 1 & len f + 1 <= len fp by FINSEQ_2:19,NAT_1:29;
then A3: len f + 1 in dom fp by FINSEQ_3:27;
A4: len f in dom f by A1,FINSEQ_5:6;
then A5: fp/.len f = f/.len f by GROUP_5:95;
A6: fp/.(len f + 1) = p by TOPREAL4:1;
A7: fp|(len f + 1) = fp by A2,TOPREAL1:2;
  A8: dom f c= dom(fp) by FINSEQ_1:39;
    fp|len f = f by FINSEQ_5:26;
  hence thesis by A3,A4,A5,A6,A7,A8,TOPREAL3:45;
 end;

theorem Th20:
   f is non empty implies L~(<*p*>^f) = LSeg(p,f/.1) \/ L~f
 proof assume that
A1:  f is non empty;
    set q = f/.1;
A2:  len f <> 0 by A1,FINSEQ_1:25;
A3:  len <*p*> = 1 by FINSEQ_1:56;
then A4:  len (<*p*>^f) = 1 + len f by FINSEQ_1:35;
   hereby
    let x be set;
     assume
A5:    x in L~(<*p*>^f);
     then reconsider r = x as Point of TOP-REAL 2;
     consider i such that
A6:    1 <= i and
A7:    i+1 <= len (<*p*>^f) and
A8:    r in LSeg((<*p*>^f)/.i,(<*p*>^f)/.(i+1)) by A5,Th14;
        now
       per cases by A6,REAL_1:def 5;
       case
A9:      i = 1;
then A10:      p = (<*p*>^f)/.i by FINSEQ_5:16;
          i in dom f by A1,A9,FINSEQ_5:6;
        hence r in LSeg(p,q) by A3,A8,A9,A10,GROUP_5:96;
       case
A11:      i > 1;
        then i <> 0;
        then consider j such that
A12:      i = j + 1 by NAT_1:22;
A13:      1 <= j by A11,A12,NAT_1:38;
A14:      j+1 <= len f by A4,A7,A12,REAL_1:53;
        then j in dom f by A13,GOBOARD2:3;
then A15:      (<*p*>^f)/.i = f/.j by A3,A12,GROUP_5:96;
          j+1 in dom f by A13,A14,GOBOARD2:3;
        then (<*p*>^f)/.(i+1) = f/.(j+1) by A3,A12,GROUP_5:96;
        hence r in L~f by A8,A13,A14,A15,Th15;
      end;
     hence x in LSeg(p,q) \/ L~f by XBOOLE_0:def 2;
    end;
   let x be set;
   assume
A16:   x in LSeg(p,q) \/ L~f;
    then reconsider r = x as Point of TOP-REAL 2;
   per cases by A16,XBOOLE_0:def 2;
   suppose
A17:  r in LSeg(p,q);
    set i = 1;
    i <= len f by A2,RLVECT_1:99;
then A18:  i+1 <= len(<*p*>^f) by A4,AXIOMS:24;
A19:  p = (<*p*>^f)/.i by FINSEQ_5:16;
      i in dom f by A1,FINSEQ_5:6;
    then q = (<*p*>^f)/.(i+1) by A3,GROUP_5:96;
    hence x in L~(<*p*>^f) by A17,A18,A19,Th15;
   suppose r in L~f;
    then consider j such that
A20:  1 <= j and
A21:  j+1 <= len f and
A22:  r in LSeg(f/.j,f/.(j+1)) by Th14;
    set i = j + 1;
    A23:  1 <= i by NAT_1:37;
A24:  i+1 <= len (<*p*>^f) by A4,A21,AXIOMS:24;
     j in dom f by A20,A21,GOBOARD2:3;
then A25:  (<*p*>^f)/.i = f/.j by A3,GROUP_5:96;
     j+1 in dom f by A20,A21,GOBOARD2:3;
   then (<*p*>^f)/.(i+1) = f/.(j+1) by A3,GROUP_5:96;
   hence x in L~(<*p*>^f) by A22,A23,A24,A25,Th15;
 end;

theorem Th21:
   L~<*p,q*> = LSeg(p,q)
 proof set f = <*p*>;
A1:  len f = 1 by FINSEQ_1:56;
  thus L~<*p,q*> = L~(f^<*q*>) by FINSEQ_1:def 9
                .= L~f \/ LSeg(f/.len f,q) by Th19
                .= L~f \/ LSeg(p,q) by A1,FINSEQ_4:25
                .= {} \/ LSeg(p,q) by A1,TOPREAL1:28
                .= LSeg(p,q);
 end;

theorem Th22:
   L~f = L~(Rev f)
 proof
  defpred P[FinSequence of TOP-REAL 2] means L~$1 = L~(Rev $1);
A1: P[<*>(the carrier of TOP-REAL 2)];
A2: for f,p st P[f] holds P[f^<*p*>]
  proof let f,p such that
A3: P[f];
   per cases;
   suppose
A4:  f is empty;
    hence L~(f^<*p*>) = L~<*p*> by FINSEQ_1:47
                 .= L~(Rev <*p*>) by FINSEQ_5:63
                 .= L~(Rev(f^<*p*>)) by A4,FINSEQ_1:47;
   suppose
A5:  f is non empty;
then A6:  len f <> 0 by FINSEQ_1:25;
    set q = f/.len f;
A7:   len f = len Rev f by FINSEQ_5:def 3;
    set q' = (Rev f)/.1;
A8:  q = q' by A5,FINSEQ_5:68;
A9:  Rev f is non empty by A6,A7,FINSEQ_1:25;
    thus L~(f^<*p*>) = LSeg(p,q') \/ L~(Rev f) by A3,A5,A8,Th19
                .= L~(<*p*>^(Rev f)) by A9,Th20
                .= L~(Rev(f^<*p*>)) by FINSEQ_5:66;
  end;
    for f holds P[f] from IndSeqD(A1,A2);
  hence thesis;
 end;

theorem Th23:
   f1 is non empty & f2 is non empty implies
    L~(f1^f2) = L~f1 \/ LSeg(f1/.len f1,f2/.1) \/ L~f2
 proof set p = f1/.len f1, q = f2/.1;
  assume
A1:  f1 is non empty;
  assume f2 is non empty;
then A2: f2 = <*q*>^(f2/^1) by FINSEQ_5:32;
  defpred P[FinSequence of TOP-REAL 2] means
    L~(f1^<*q*>^$1) = L~f1 \/ LSeg(p,q) \/ L~(<*q*>^$1);
A3: P[<*>(the carrier of TOP-REAL 2)]
  proof set O = <*>(the carrier of TOP-REAL 2);
   thus L~(f1^<*q*>^O) = L~(f1^<*q*>) by FINSEQ_1:47
                      .= L~f1 \/ LSeg(p,q) \/ {} by A1,Th19
                      .= L~f1 \/ LSeg(p,q) \/ L~<*q*> by Th12
                      .= L~f1 \/ LSeg(p,q) \/ L~(<*q*>^O) by FINSEQ_1:47;
  end;
A4: for f for o being Point of TOP-REAL 2 st P[f] holds P[f^<*o*>]
  proof let f; let o be Point of TOP-REAL 2 such that
A5: P[f];
A6:  f1^<*q*> is non empty by FINSEQ_1:48;
   per cases;
   suppose f is empty;
then A7:  (f^<*o*>) = <*o*> by FINSEQ_1:47;
       len(f1^<*q*>) = len f1 + 1 by FINSEQ_2:19;
  then (f1^<*q*>)/.len(f1^<*q*>) = q by TOPREAL4:1;
    hence L~(f1^<*q*>^(f^<*o*>)) = L~(f1^<*q*>) \/ LSeg(q,o) by A6,A7,Th19
       .= L~f1 \/ LSeg(p,q) \/ LSeg(q,o) by A1,Th19
       .= L~f1 \/ LSeg(p,q) \/ L~<*q,o*> by Th21
       .= L~f1 \/ LSeg(p,q) \/ L~(<*q*>^(f^<*o*>)) by A7,FINSEQ_1:def 9;
   suppose
A8:   f is non empty;
    set g = f1^<*q*>^f, h = <*q*>^f;
A9:  g is non empty by A6,FINSEQ_1:48;
A10:  h is non empty by FINSEQ_1:48;
     len f <> 0 by A8,FINSEQ_1:25;
   then consider f' being FinSequence of TOP-REAL 2, d being Point of TOP-REAL
2
    such that
A11:   f = f'^<*d*> by FINSEQ_2:22;
A12:  g = f1^<*q*>^f'^<*d*> & h = <*q*>^f'^<*d*> by A11,FINSEQ_1:45;
   then len g = len(f1^<*q*>^f')+1 & len h = len(<*q*>^f')+1 by FINSEQ_2:19;
   then g/.len g = d & h/.len h = d by A12,TOPREAL4:1;
then A13:  L~h \/ LSeg(g/.len g,o)
       = L~(h^<*o*>) by A10,Th19
      .= L~(<*q*>^(f^<*o*>)) by FINSEQ_1:45;
    thus L~(f1^<*q*>^(f^<*o*>))
       = L~(g^<*o*>) by FINSEQ_1:45
      .= L~g \/ LSeg(g/.len g,o) by A9,Th19
      .= L~f1 \/ LSeg(p,q) \/ L~(<*q*>^(f^<*o*>)) by A5,A13,XBOOLE_1:4;
  end;
    for f holds P[f] from IndSeqD(A3,A4);
  then L~(f1^<*q*>^(f2/^1)) = L~f1 \/ LSeg(p,q) \/ L~(<*q*>^(f2/^1));
  hence L~(f1^f2) = L~f1 \/ LSeg(f1/.len f1,f2/.1) \/ L~f2 by A2,FINSEQ_1:45;
 end;

 Lm1:
   L~(f|n) c= L~f
 proof
      now per cases;
     suppose
A1:     n = 0;
         f|0 is empty;
       hence thesis by A1,Th11,XBOOLE_1:2;
     suppose
A2:    n <> 0;
        now per cases;
       suppose
A3:      n < len f;
        then len(f|n) = n by TOPREAL1:3;
then A4:      f|n is non empty by A2,FINSEQ_1:25;
          len(f/^n) = len f - n by A3,RFINSEQ:def 2;
        then len(f/^n) <> 0 by A3,XCMPLX_1:15;
then A5:      f/^n is non empty by FINSEQ_1:25;
          (f|n)^(f/^n) = f by RFINSEQ:21;
        then L~f = L~(f|n) \/ LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n)
                  by A4,A5,Th23
                .= L~(f|n) \/ (LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n))
                  by XBOOLE_1:4;
        hence thesis by XBOOLE_1:7;
       suppose n >= len f;
         hence thesis by TOPREAL1:2;
      end;
      hence thesis;
    end;
    hence thesis;
 end;

canceled;

theorem Th25:
   q in rng f implies L~f = L~(f-:q) \/ L~(f:-q)
 proof assume
A1: q in rng f;
 set n = q..f;
 A2: n <> 0 by A1,FINSEQ_4:31;
A3: n <= len f by A1,FINSEQ_4:31;
 per cases by A3,REAL_1:def 5;
 suppose
A4:  n < len f;
then A5:  len(f|n) = n by TOPREAL1:3;
then A6:  f|n is non empty by A2,FINSEQ_1:25;
       f|n = f-:q by FINSEQ_5:def 1;
then A7:  (f|n)/.len(f|n) = q by A1,A5,FINSEQ_5:48;
    len(f/^n) = len f - n by A4,RFINSEQ:def 2;
  then len(f/^n) <> 0 by A4,XCMPLX_1:15;
then A8:  f/^n is non empty by FINSEQ_1:25;
    (f|n)^(f/^n) = f by RFINSEQ:21;
  hence L~f = L~(f|n) \/ LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n)
              by A6,A8,Th23
          .= L~(f|n) \/ (LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n))
              by XBOOLE_1:4
          .= L~(f|n) \/ L~(<*(f|n)/.len(f|n)*>^(f/^n)) by A8,Th20
          .= L~(f|n) \/ L~(f:-q) by A7,FINSEQ_5:def 2
          .= L~(f-:q) \/ L~(f:-q) by FINSEQ_5:def 1;
 suppose
A9:  n = len f;
then A10:  L~f = L~(f|n) by TOPREAL1:2
        .= L~(f-:q) by FINSEQ_5:def 1;
    len(f/^n) = len f - n by A9,RFINSEQ:def 2
           .= 0 by A9,XCMPLX_1:14;
then A11:  f/^n is empty by FINSEQ_1:25;
    f:-q = <*q*>^(f/^n) by FINSEQ_5:def 2
      .= <*q*> by A11,FINSEQ_1:47;
  then L~(f:-q) is empty by Th12;
  hence thesis by A10;
 end;

theorem Th26:
   p in LSeg(f,n) implies L~f = L~Ins(f,n,p)
 proof assume
A1: p in LSeg(f,n);
  set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n;
A2: g1 is non empty by FINSEQ_1:48;
A3: g1/.len g1 = g1/.(len f1 + 1) by FINSEQ_2:19
                .= p by TOPREAL4:1;
A4: 1 <= n & n+1 <= len f by A1,TOPREAL1:def 5;
    n <= n+1 by NAT_1:29;
then A5: n <= len f by A4,AXIOMS:22;
then A6: len f1 = n by TOPREAL1:3;
then A7: n in dom f1 by A4,FINSEQ_3:27;
A8: f1 is non empty by A4,A6,FINSEQ_3:27,RELAT_1:60;
     1 <= len f - n by A4,REAL_1:84;
   then 1 <= len f2 by A5,RFINSEQ:def 2;
then A9: 1 in dom f2 by FINSEQ_3:27;
A10: LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A4,TOPREAL1:def 5
             .= LSeg(f1/.len f1,f/.(n+1)) by A6,A7,TOPREAL1:1
             .= LSeg(f1/.len f1,f2/.1) by A9,FINSEQ_5:30;
  thus L~Ins(f,n,p) = L~(g1^f2) by FINSEQ_5:def 4
    .= L~g1 \/ LSeg(g1/.len g1,f2/.1) \/ L~f2 by A2,A9,Th23,RELAT_1:60
    .= L~f1 \/ LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1) \/ L~f2
      by A7,Th19,RELAT_1:60
    .= L~f1 \/ (LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1)) \/ L~f2
      by XBOOLE_1:4
    .= L~f1 \/ LSeg(f1/.len f1,f2/.1) \/ L~f2 by A1,A3,A10,TOPREAL1:11
    .= L~(f1^f2) by A8,A9,Th23,RELAT_1:60
    .= L~f by RFINSEQ:21;
 end;

begin

definition
 cluster being_S-Seq FinSequence of TOP-REAL 2;
  existence
 proof set p = |[ 0,0 ]|, q = |[ 1,1 ]|;
   p`1 = 0 & p`2 = 0 & q`1 = 1 & q`2 = 1 by EUCLID:56;
  then <* p,|[p`1,q`2]|,q *> is_S-Seq by TOPREAL3:41;
  hence thesis;
 end;
 cluster being_S-Seq ->
     one-to-one unfolded s.n.c. special non trivial FinSequence of TOP-REAL 2;
  coherence
 proof let f;
  assume
A1: f is being_S-Seq;
   then len f >= 2 by TOPREAL1:def 10;
   hence thesis by A1,SPPOL_1:2,TOPREAL1:def 10;
 end;
 cluster one-to-one unfolded s.n.c. special non trivial ->
     being_S-Seq FinSequence of TOP-REAL 2;
  coherence
 proof let f;
  assume
A2:  f is one-to-one unfolded s.n.c. special;
   assume f is non trivial;
   then len f >= 2 by SPPOL_1:2;
   hence thesis by A2,TOPREAL1:def 10;
 end;
 cluster being_S-Seq -> non empty FinSequence of TOP-REAL 2;
  coherence
 proof let f;
  assume f is being_S-Seq;
  then len f <> 0 by TOPREAL1:def 10;
  hence thesis by FINSEQ_1:25;
 end;
end;

definition
 cluster
  one-to-one unfolded s.n.c. special non trivial FinSequence of TOP-REAL 2;
   existence
 proof consider f being being_S-Seq FinSequence of TOP-REAL 2;
    f is one-to-one unfolded s.n.c. special non trivial;
  hence thesis;
 end;
end;

theorem Th27:
   len f <= 2 implies f is unfolded
 proof assume
A1: len f <= 2;
  let i such that
A2: 1 <= i;
  assume i+2 <= len f;
  then i+2 <= 2 by A1,AXIOMS:22;
  then i <= 2-2 by REAL_1:84;
  hence LSeg(f,i) /\ LSeg(f,i+1) = {f/.(i+1)} by A2,AXIOMS:22;
 end;

Lm2: <*p,q*> is unfolded
 proof len <*p,q*> = 2 by FINSEQ_1:61; hence thesis by Th27; end;

Lm3:
   f is unfolded implies f|n is unfolded
 proof assume
A1:  f is unfolded;
  set h = f|n;
  let i such that
A2:  1 <= i and
A3:  i + 2 <= len h;
A4:  i+1+1 = i+(1+1) by XCMPLX_1:1;
     len h <= len f by FINSEQ_5:18;
then A5:  i+2 <= len f by A3,AXIOMS:22;
A6:  i+1 in dom h by A2,A3,GOBOARD2:4;
    i+1 <= i+2 by AXIOMS:24;
  then i+1 <= len h by A3,AXIOMS:22;
  hence LSeg(h,i) /\ LSeg(h,i+1) = LSeg(f,i) /\ LSeg(h,i+1) by Th3
                               .= LSeg(f,i) /\ LSeg(f,i+1) by A3,A4,Th3
                               .= {f/.(i+1)} by A1,A2,A5,TOPREAL1:def 8
                               .= {h/.(i+1)} by A6,TOPREAL1:1;
 end;

Lm4:
   f is unfolded implies f/^n is unfolded
 proof assume
A1: f is unfolded;
 per cases;
 suppose
A2: n <= len f;
  set h = f/^n;
  let i such that
A3:  1 <= i and
A4:  i + 2 <= len h;
   A5:  1 <= i+1 by NAT_1:29;
A6:  i+1+1 = i+(1+1) by XCMPLX_1:1;
A7:  len h = len f - n by A2,RFINSEQ:def 2;
     then n+(i+2) <= len f by A4,REAL_1:84;
then A8:  n+i+2 <= len f by XCMPLX_1:1;
A9:  i+1 in dom h by A3,A4,GOBOARD2:4;
     i <= n+i by NAT_1:29;
then A10: 1 <= n+i by A3,AXIOMS:22;
    i+1 <= i+2 by AXIOMS:24;
  then i+1 <= len h by A4,AXIOMS:22;
  hence LSeg(h,i) /\ LSeg(h,i+1)
      = LSeg(f,n+i) /\ LSeg(h,i+1) by A3,A7,Th5
     .= LSeg(f,n+i) /\ LSeg(f,n+(i+1)) by A4,A5,A6,A7,Th5
     .= LSeg(f,n+i) /\ LSeg(f,n+i+1) by XCMPLX_1:1
     .= {f/.(n+i+1)} by A1,A8,A10,TOPREAL1:def 8
     .= {f/.(n+(i+1))} by XCMPLX_1:1
     .= {h/.(i+1)} by A9,FINSEQ_5:30;
 suppose n > len f;
  then f/^n = <*>(the carrier of TOP-REAL 2) by RFINSEQ:def 2;
  then len(f/^n) = 0 by FINSEQ_1:25;
  hence thesis by Th27;
 end;

definition let f be unfolded FinSequence of TOP-REAL 2, n;
 cluster f|n -> unfolded;
  coherence by Lm3;
 cluster f/^n -> unfolded;
  coherence by Lm4;
end;

theorem Th28:
   p in rng f & f is unfolded implies f:-p is unfolded
 proof assume p in rng f;
  then ex i st i+1 = p..f & f:-p = f/^i by FINSEQ_5:52;
  hence thesis by Lm4;
 end;

Lm5:
   f is unfolded implies f-:p is unfolded
 proof
    f-:p = f|(p..f) by FINSEQ_5:def 1;
  hence thesis by Lm3;
 end;

definition let f be unfolded FinSequence of TOP-REAL 2, p;
 cluster f-:p -> unfolded;
  coherence by Lm5;
end;

theorem Th29:
   f is unfolded implies Rev f is unfolded
 proof assume
A1: f is unfolded;
  let i such that
A2: 1 <= i and
A3: i + 2 <= len Rev f;
A4: len Rev f = len f by FINSEQ_5:def 3;
    i <= i+2 by NAT_1:29;
  then i <= len f by A3,A4,AXIOMS:22;
  then reconsider j = len f - i as Nat by INT_1:18;
A5: j+i = len f by XCMPLX_1:27;
    i+1 <= i+1+1 by NAT_1:29;
  then i+1 <= i+(1+1) by XCMPLX_1:1;
  then i+1 <= len f by A3,A4,AXIOMS:22;
  then reconsider j' = len f - (i+1) as Nat by INT_1:18;
A6: j'+1 = len f - i - 1 + 1 by XCMPLX_1:36
        .= j by XCMPLX_1:27;
A7: j'+(i+1) = len f by XCMPLX_1:27;
A8: j + (i+1) = len f + 1 by A5,XCMPLX_1:1;
A9: dom f = Seg len f by FINSEQ_1:def 3;
    i+(1+1) = i+1+1 by XCMPLX_1:1;
then A10: 1 <= j' by A3,A4,REAL_1:84;
     i in dom f by A2,A3,A4,GOBOARD2:4;
   then j + 1 in dom f by A9,FINSEQ_5:2;
   then j' + (1+1) in dom f by A6,XCMPLX_1:1;
then A11: j'+2 <= len f by FINSEQ_3:27;
     i+1 in dom f by A2,A3,A4,GOBOARD2:4;
   then A12: j'+1 in dom f by A9,FINSEQ_5:2;
  thus LSeg(Rev f,i) /\ LSeg(Rev f,i+1)
     = LSeg(f,j) /\ LSeg(Rev f,i+1) by A5,Th2
    .= LSeg(f,j'+1) /\ LSeg(f,j') by A6,A7,Th2
    .= {f/.(j'+1)} by A1,A10,A11,TOPREAL1:def 8
    .= {(Rev f)/.(i+1)} by A6,A8,A12,FINSEQ_5:69;
 end;

theorem Th30:
  g is unfolded & LSeg(p,g/.1) /\ LSeg(g,1) = {g/.1}
   implies <*p*>^g is unfolded
 proof set f = <*p*>;
A1: len f = 1 by FINSEQ_1:56;
  assume that
A2: g is unfolded and
A3: LSeg(p,g/.1) /\ LSeg(g,1) = {g/.1};
A4: f/.1 = p by FINSEQ_4:25;
  let i such that
A5: 1 <= i and
A6: i + 2 <= len(f^g);
A7: len(f^g) = len f + len g by FINSEQ_1:35;
A8:   i+(1+1) = i+1+1 by XCMPLX_1:1;
    per cases;
     suppose
A9:    i = len f;
       now
      assume A10: len g = 0;
        i <= i+1 by NAT_1:29;
      then i < i+(1+1) by A8,NAT_1:38;
      hence contradiction by A1,A5,A6,A7,A10,AXIOMS:22;
     end;
     then 1 <= len g by RLVECT_1:99;
then A11:    1 in dom g by FINSEQ_3:27;
then A12:     LSeg(f^g,i) = LSeg(f/.len f,g/.1) by A9,Th8,RELAT_1:60;
        LSeg(f^g,i+1) = LSeg(g,1) by A9,Th7;
       hence thesis by A1,A3,A4,A9,A11,A12,GROUP_5:96;
     suppose i <> len f;
then A13:    i > len f by A1,A5,REAL_1:def 5;
      reconsider j = i - len f as Nat by A1,A5,INT_1:18;
A14:    len f + j = i by XCMPLX_1:27;
then A15:    len f + (j+1) = i+1 by XCMPLX_1:1;
        len f + 1 <= i by A13,NAT_1:38;
then A16:    1 <= j by REAL_1:84;
        i+2-len f <= len g by A6,A7,REAL_1:86;
then A17:   j+(1+1) <= len g by XCMPLX_1:29;
then A18:    j+1+1 <= len g by XCMPLX_1:1;
        j+1 <= j+1+1 by NAT_1:29;
then A19:    j+1 <= len g by A18,AXIOMS:22;
      A20:    1 <= j+1 by NAT_1:29;
A21:    j+1 in dom g by A16,A19,GOBOARD2:3;
      thus LSeg(f^g,i) /\ LSeg(f^g,i+1)
         = LSeg(g,j) /\ LSeg(f^g,i+1) by A14,A16,Th7
        .= LSeg(g,j) /\ LSeg(g,j+1) by A15,A20,Th7
        .= {g/.(j+1)} by A2,A16,A17,TOPREAL1:def 8
        .= {(f^g)/.(i+1)} by A15,A21,GROUP_5:96;
 end;

theorem Th31:
  f is unfolded & k+1 = len f & LSeg(f,k) /\
 LSeg(f/.len f,p) = {f/.len f}
   implies f^<*p*> is unfolded
 proof set g = <*p*>;
  assume that
A1: f is unfolded and
A2: k+1 = len f & LSeg(f,k) /\ LSeg(f/.len f,p) = {f/.len f};
A3: len g = 1 by FINSEQ_1:56;
A4: g/.1 = p by FINSEQ_4:25;
  let i such that
A5: 1 <= i and
A6: i + 2 <= len(f^g);
A7: len(f^g) = len f + len g by FINSEQ_1:35;
A8:   i+(1+1) = i+1+1 by XCMPLX_1:1;
  per cases;
   suppose
A9:  i+2 <= len f;
then A10:  i+1 in dom f by A5,GOBOARD2:4;
      i+1 <= i+1+1 by NAT_1:29;
    then i+1 <= len f by A8,A9,AXIOMS:22;
    hence LSeg(f^g,i) /\ LSeg(f^g,i+1)
        = LSeg(f,i) /\ LSeg(f^g,i+1) by Th6
       .= LSeg(f,i) /\ LSeg(f,i+1) by A8,A9,Th6
       .= {f/.(i+1)} by A1,A5,A9,TOPREAL1:def 8
       .= {(f^g)/.(i+1)} by A10,GROUP_5:95;
   suppose
A11: i + 2 > len f;
A12: i+1 <= len f by A3,A6,A7,A8,REAL_1:53;
then A13: f is non empty by A5,GOBOARD2:3,RELAT_1:60;
     len f <= i+1 by A8,A11,NAT_1:38;
then A14:  i+1 = len f by A12,AXIOMS:21;
   then k = i by A2,XCMPLX_1:2;
then A15: LSeg(f^g,i) = LSeg(f,k) by A12,Th6;
A16: LSeg(f^g,i+1) = LSeg(f/.len f,g/.1) by A13,A14,Th8;
     len f in dom f by A13,FINSEQ_5:6;
   hence thesis by A2,A4,A14,A15,A16,GROUP_5:95;
 end;

theorem Th32:
  f is unfolded & g is unfolded &
    k+1 = len f & LSeg(f,k) /\ LSeg(f/.len f,g/.1) = {f/.len f} &
    LSeg(f/.len f,g/.1) /\ LSeg(g,1) = {g/.1}
   implies f^g is unfolded
 proof assume that
A1: f is unfolded and
A2: g is unfolded and
A3: k+1 = len f & LSeg(f,k) /\ LSeg(f/.len f,g/.1) = {f/.len f} and
A4: LSeg(f/.len f,g/.1) /\ LSeg(g,1) = {g/.1};
  let i such that
A5: 1 <= i and
A6: i + 2 <= len(f^g);
A7: len(f^g) = len f + len g by FINSEQ_1:35;
  per cases;
   suppose
A8:  i+2 <= len f;
then A9:  i+1 in dom f by A5,GOBOARD2:4;
A10:  i+(1+1) = i+1+1 by XCMPLX_1:1;
      i+1 <= i+1+1 by NAT_1:29;
    then i+1 <= len f by A8,A10,AXIOMS:22;
    hence LSeg(f^g,i) /\ LSeg(f^g,i+1)
        = LSeg(f,i) /\ LSeg(f^g,i+1) by Th6
       .= LSeg(f,i) /\ LSeg(f,i+1) by A8,A10,Th6
       .= {f/.(i+1)} by A1,A5,A8,TOPREAL1:def 8
       .= {(f^g)/.(i+1)} by A9,GROUP_5:95;
   suppose
A11:   i + 2 > len f;
A12:   i+(1+1) = i+1+1 by XCMPLX_1:1;
      now per cases;
     suppose
A13:    i <= len f;
then A14:    f is non empty by A5,FINSEQ_3:27,RELAT_1:60;
       len g <> 0 by A6,A7,A11;
     then 1 <= len g by RLVECT_1:99;
then A15:    1 in dom g by FINSEQ_3:27;
        now per cases;
       suppose
A16:       i = len f;
then A17:      LSeg(f^g,i) = LSeg(f/.len f,g/.1) by A14,A15,Th8,RELAT_1:60;
        LSeg(f^g,i+1) = LSeg(g,1) by A16,Th7;
        hence thesis by A4,A15,A16,A17,GROUP_5:96;
       suppose i <> len f;
         then i < len f by A13,REAL_1:def 5;
then A18:        i+1 <= len f by NAT_1:38;
           len f <= i+1 by A11,A12,NAT_1:38;
then A19:        i+1 = len f by A18,AXIOMS:21;
         then k = i by A3,XCMPLX_1:2;
then A20:      LSeg(f^g,i) = LSeg(f,k) by A18,Th6;
A21:      LSeg(f^g,i+1) = LSeg(f/.len f,g/.1) by A14,A15,A19,Th8,RELAT_1:60;
         len f in dom f by A14,FINSEQ_5:6;
       hence thesis by A3,A19,A20,A21,GROUP_5:95;
      end;
      hence thesis;
     suppose
A22:    i > len f;
      then reconsider j = i - len f as Nat by INT_1:18;
A23:    len f + j = i by XCMPLX_1:27;
then A24:    len f + (j+1) = i+1 by XCMPLX_1:1;
        len f + 1 <= i by A22,NAT_1:38;
then A25:    1 <= j by REAL_1:84;
        i+2-len f <= len g by A6,A7,REAL_1:86;
then A26:   j+(1+1) <= len g by XCMPLX_1:29;
then A27:    j+1+1 <= len g by XCMPLX_1:1;
        j+1 <= j+1+1 by NAT_1:29;
then A28:    j+1 <= len g by A27,AXIOMS:22;
      A29:    1 <= j+1 by NAT_1:29;
A30:    j+1 in dom g by A25,A28,GOBOARD2:3;
      thus LSeg(f^g,i) /\ LSeg(f^g,i+1)
         = LSeg(g,j) /\ LSeg(f^g,i+1) by A23,A25,Th7
        .= LSeg(g,j) /\ LSeg(g,j+1) by A24,A29,Th7
        .= {g/.(j+1)} by A2,A25,A26,TOPREAL1:def 8
        .= {(f^g)/.(i+1)} by A24,A30,GROUP_5:96;
    end;
    hence thesis;
 end;

theorem Th33:
   f is unfolded & p in LSeg(f,n) implies Ins(f,n,p) is unfolded
 proof assume that
A1: f is unfolded and
A2: p in LSeg(f,n);
  set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n;
A3: g1/.len g1 = g1/.(len f1 + 1) by FINSEQ_2:19
                .= p by TOPREAL4:1;
A4: 1 <= n & n+1 <= len f by A2,TOPREAL1:def 5;
    n <= n+1 by NAT_1:29;
then A5: n <= len f by A4,AXIOMS:22;
then A6: len f1 = n by TOPREAL1:3;
then A7: n in dom f1 by A4,FINSEQ_3:27;
     1 <= len f - n by A4,REAL_1:84;
then A8: 1 <= len f2 by A5,RFINSEQ:def 2;
then A9: 1 in dom f2 by FINSEQ_3:27;
A10: LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A4,TOPREAL1:def 5;
A11: f/.n = f1/.len f1 by A6,A7,TOPREAL1:1;
A12: f/.(n+1) = f2/.1 by A9,FINSEQ_5:30;
then A13: LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1)
     = LSeg(f1/.len f1,f2/.1) by A2,A3,A10,A11,TOPREAL1:11;
A14: now len f1 <> 0 by A2,A6,TOPREAL1:def 5;
     then consider k such that
A15:    k+1 = len f1 by NAT_1:22;
A16:    k+(1+1) <= len f by A4,A6,A15,XCMPLX_1:1;
A17:    f1 is unfolded by A1,Lm3;
     per cases;
     suppose k <> 0;
then A18:    1 <= k by RLVECT_1:98;
        LSeg(f1,k) = LSeg(f,k) by A15,Th3;
then A19:    LSeg(f1,k) /\
 LSeg(f,n) = {f/.n} by A1,A6,A15,A16,A18,TOPREAL1:def 8;
        now let x be set;
       hereby assume x in LSeg(f1,k) /\ LSeg(f1/.len f1,p);
then A20:     x in LSeg(f1,k) & x in LSeg(f1/.len f1,p) by XBOOLE_0:def 3;
        then x in LSeg(f,n) by A10,A11,A12,A13,XBOOLE_0:def 2;
        then x in LSeg(f1,k) /\ LSeg(f,n) by A20,XBOOLE_0:def 3;
        hence x = f/.n by A19,TARSKI:def 1;
       end;
       assume
A21:     x = f/.n;
       then x in LSeg(f1,k) /\ LSeg(f,n) by A19,TARSKI:def 1;
then A22:     x in LSeg(f1,k) by XBOOLE_0:def 3;
         x in LSeg(f1/.len f1,p) by A11,A21,TOPREAL1:6;
       hence x in LSeg(f1,k) /\ LSeg(f1/.len f1,p) by A22,XBOOLE_0:def 3;
      end;
      then LSeg(f1,k) /\ LSeg(f1/.len f1,p) = {f1/.len f1} by A11,TARSKI:def 1
;
      hence g1 is unfolded by A15,A17,Th31;
     suppose k = 0;
      then len g1 = 1+1 by A15,FINSEQ_2:19;
      hence g1 is unfolded by Th27;
    end;
A23:  n+1 = len g1 by A6,FINSEQ_2:19;
      f1/.len f1 = g1/.n by A6,A7,GROUP_5:95;
    then LSeg(g1,n) = LSeg(f1/.len f1,g1/.len g1)
     by A4,A23,TOPREAL1:def 5;
then A24:  LSeg(g1,n) /\ LSeg(g1/.len g1,f2/.1) = {g1/.len g1}
      by A2,A3,A10,A11,A12,TOPREAL1:14;
     now per cases;
    suppose len f2 = 1;
     then f2 = <*f2/.1*> by FINSEQ_5:15;
     hence g1^f2 is unfolded by A14,A23,A24,Th31;
    suppose len f2 <> 1;
     then len f2 > 1 by A8,REAL_1:def 5;
then A25:    1+1 <= len f2 by NAT_1:38;
     then LSeg(f2,1) = LSeg(f2/.1,f2/.(1+1)) by TOPREAL1:def 5;
then A26:    f2/.1 in LSeg(f2,1) by TOPREAL1:6;
A27:    1+1 <= len f - n by A5,A25,RFINSEQ:def 2;
     then n+(1+1) <= len f by REAL_1:84;
then A28:     {f/.(n+1)} = LSeg(f,n) /\ LSeg(f,n+1) by A1,A4,TOPREAL1:def 8
                    .= LSeg(f,n) /\ LSeg(f2,1) by A27,Th5;

        now let x be set;
       hereby assume x in LSeg(g1/.len g1,f2/.1) /\ LSeg(f2,1);
then A29:      x in LSeg(g1/.len g1,f2/.1) & x in LSeg(f2,1) by XBOOLE_0:def 3;
        then x in LSeg(f,n) by A10,A11,A12,A13,XBOOLE_0:def 2;
        then x in LSeg(f,n) /\ LSeg(f2,1) by A29,XBOOLE_0:def 3;
        hence x = f2/.1 by A12,A28,TARSKI:def 1;
       end;
       assume
A30:     x = f2/.1;
       then x in LSeg(g1/.len g1,f2/.1) by TOPREAL1:6;
       hence x in LSeg(g1/.len g1,f2/.1) /\ LSeg(f2,1)
        by A26,A30,XBOOLE_0:def 3;
      end;
then A31:  LSeg(g1/.len g1,f2/.1) /\ LSeg(f2,1) = {f2/.1} by TARSKI:def 1;
       f2 is unfolded by A1,Lm4;
     hence g1^f2 is unfolded by A14,A23,A24,A31,Th32;
   end;
  hence thesis by FINSEQ_5:def 4;
 end;

theorem Th34:
   len f <= 2 implies f is s.n.c.
 proof assume
A1: len f <= 2;
  let i,j such that
A2: i+1 < j;
     now
    assume that
A3:  1 <= i and
A4:  i+1 <= len f and
A5:  1 <= j and
A6:  j+1 <= len f;
      i+1 <= 1+1 & j+1 <= 1+1 by A1,A4,A6,AXIOMS:22;
    then i <= 1 & j <= 1 by REAL_1:53;
    then i = 1 & j = 1 by A3,A5,AXIOMS:21;
    hence contradiction by A2;
   end;
  then LSeg(f,i) = {} or LSeg(f,j) = {} by TOPREAL1:def 5;
  hence LSeg(f,i) /\ LSeg(f,j) = {};
 end;

Lm6:
  <*p,q*> is s.n.c.
 proof len <*p,q*> = 2 by FINSEQ_1:61; hence thesis by Th34; end;

Lm7:
   f is s.n.c. implies f|n is s.n.c.
 proof assume
A1: f is s.n.c.;
  let i,j such that
A2:  i+1 < j;
  per cases;
  suppose
A3: i = 0 or j+1 > len(f|n);
     now per cases by A3;
    case i = 0;
     hence LSeg(f|n,i) = {} by TOPREAL1:def 5;
    case j+1 > len(f|n);
     hence LSeg(f|n,j) = {} by TOPREAL1:def 5;
   end; then LSeg(f|n,i) /\ LSeg(f|n,j) = {};
   hence LSeg(f|n,i) misses LSeg(f|n,j) by XBOOLE_0:def 7;
  suppose that i <> 0 and
A4: j+1 <= len(f|n);
A5: LSeg(f,i) misses LSeg(f,j) by A1,A2,TOPREAL1:def 9;
     j <= j+1 by NAT_1:29;
   then i+1 < j+1 by A2,AXIOMS:22;
   then i+1 <= len(f|n) by A4,AXIOMS:22;
   then LSeg(f|n,i) /\ LSeg(f|n,j)
       = LSeg(f,i) /\ LSeg(f|n,j) by Th3
      .= LSeg(f,i) /\ LSeg(f,j) by A4,Th3
      .= {} by A5,XBOOLE_0:def 7;
   hence LSeg(f|n,i) misses LSeg(f|n,j) by XBOOLE_0:def 7;
 end;

Lm8:
   f is s.n.c. implies f/^n is s.n.c.
 proof assume
A1: f is s.n.c.;
 per cases;
 suppose
A2: n <= len f;
  let i,j such that
A3: i+1 < j;
    now per cases;
  suppose
A4: i = 0 or j+1 > len(f/^n);
     now per cases by A4;
    case i = 0;
     hence LSeg(f/^n,i) = {} by TOPREAL1:def 5;
    case j+1 > len(f/^n);
     hence LSeg(f/^n,j) = {} by TOPREAL1:def 5;
   end; then LSeg(f/^n,i) /\ LSeg(f/^n,j) = {};
   hence thesis by XBOOLE_0:def 7;
  suppose that
A5: i <> 0 and
A6: j+1 <= len(f/^n);
A7: len(f/^n) = len f - n by A2,RFINSEQ:def 2;
A8: 1 <= i by A5,RLVECT_1:99;
     i <= j by A3,NAT_1:38;
then A9: 1 <= j by A8,AXIOMS:22;
     n+(i+1) < n+j by A3,REAL_1:53;
then n+i+1 < n+j by XCMPLX_1:1;
then A10: LSeg(f,n+i) misses LSeg(f,n+j) by A1,TOPREAL1:def 9;
     j <= j+1 by NAT_1:29;
   then i+1 < j+1 by A3,AXIOMS:22;
   then i+1 <= len(f/^n) by A6,AXIOMS:22;
   then LSeg(f/^n,i) /\ LSeg(f/^n,j)
       = LSeg(f,n+i) /\ LSeg(f/^n,j) by A7,A8,Th5
      .= LSeg(f,n+i) /\ LSeg(f,n+j) by A6,A7,A9,Th5
      .= {} by A10,XBOOLE_0:def 7;
   hence thesis by XBOOLE_0:def 7;
  end;
  hence thesis;
 suppose n > len f;
  then f/^n = <*>(the carrier of TOP-REAL 2) by RFINSEQ:def 2;
  then len(f/^n) = 0 by FINSEQ_1:25;
  hence thesis by Th34;
 end;

definition let f be s.n.c. FinSequence of TOP-REAL 2, n;
  cluster f|n -> s.n.c.;
   coherence by Lm7;
  cluster f/^n -> s.n.c.;
   coherence by Lm8;
end;

Lm9:
   f is s.n.c. implies f-:p is s.n.c.
 proof f-:p = f|(p..f) by FINSEQ_5:def 1;
  hence thesis by Lm7;
 end;

definition let f be s.n.c. FinSequence of TOP-REAL 2, p;
  cluster f-:p -> s.n.c.;
   coherence by Lm9;
end;

theorem Th35:
  p in rng f & f is s.n.c. implies f:-p is s.n.c.
 proof assume p in rng f;
  then ex i st i+1 = p..f & f:-p = f/^i by FINSEQ_5:52;
  hence thesis by Lm8;
 end;

theorem Th36:
   f is s.n.c. implies Rev f is s.n.c.
 proof assume
A1: f is s.n.c.;
  let i,j such that
A2:  i+1 < j;
  per cases;
  suppose
A3: i = 0 or j+1 > len(Rev f);
     now per cases by A3;
    case i = 0;
     hence LSeg(Rev f,i) = {} by TOPREAL1:def 5;
    case j+1 > len(Rev f);
     hence LSeg(Rev f,j) = {} by TOPREAL1:def 5;
   end;
   then LSeg(Rev f,i) /\ LSeg(Rev f,j) = {};
   hence thesis by XBOOLE_0:def 7;
  suppose that
   i <> 0 and
A4: j+1 <= len(Rev f);
A5: len Rev f = len f by FINSEQ_5:def 3;
     j <= j+1 by NAT_1:29;
then A6: j <= len f by A4,A5,AXIOMS:22;
   then reconsider j' = len f - j as Nat by INT_1:18;
     i <= i+1 by NAT_1:29;
   then i < j by A2,AXIOMS:22;
   then i <= len f by A6,AXIOMS:22;
   then reconsider i' = len f - i as Nat by INT_1:18;
A7: j'+j = len f by XCMPLX_1:27;
     len f - (i+1) > j' by A2,REAL_2:105;
   then i' - 1 > j' by XCMPLX_1:36;
   then i' - 1 + 1 > j'+1 by REAL_1:53;
then j'+1 < i' by XCMPLX_1:27;
then A8: LSeg(f,i') misses LSeg(f,j') by A1,TOPREAL1:def 9;
     i'+i = len f by XCMPLX_1:27;
   hence LSeg(Rev f,i) /\ LSeg(Rev f,j)
       = LSeg(f,i') /\ LSeg(Rev f,j) by Th2
      .= LSeg(f,i') /\ LSeg(f,j') by A7,Th2
      .= {} by A8,XBOOLE_0:def 7;
 end;

theorem Th37:
  f is s.n.c. & g is s.n.c. & L~f misses L~g &
 (for i st 1<=i & i+2 <= len f holds LSeg(f,i) misses LSeg(f/.len f,g/.1)) &
 (for i st 2<=i & i+1 <= len g holds LSeg(g,i) misses LSeg(f/.len f,g/.1))
   implies f^g is s.n.c.
 proof assume that
A1: f is s.n.c. and
A2: g is s.n.c. and
A3: L~f /\ L~g = {} and
A4: for i st 1<=i & i+2<=
len f holds LSeg(f,i) misses LSeg(f/.len f,g/.1) and
A5: for i st 2<=i & i+1 <= len g
      holds LSeg(g,i) misses LSeg(f/.len f,g/.1);
  let i,j such that
A6: i+1 < j;
  per cases;
  suppose
A7: i = 0 or j+1 > len(f^g);
     now per cases by A7;
    case i = 0;
     hence LSeg(f^g,i) = {} by TOPREAL1:def 5;
    case j+1 > len(f^g);
     hence LSeg(f^g,j) = {} by TOPREAL1:def 5;
   end;
   then LSeg(f^g,i) /\ LSeg(f^g,j) = {};
   hence thesis by XBOOLE_0:def 7;
  suppose that
A8: i <> 0 and
A9: j+1 <= len(f^g);
A10: len(f^g) = len f + len g by FINSEQ_1:35;
A11:  1 <= i by A8,RLVECT_1:99;
      i <= i+1 by NAT_1:29;
then A12:  i < j by A6,AXIOMS:22;
     now per cases;
    suppose
A13:   j+1 <= len f;
       j <= j+1 by NAT_1:29;
     then i < j+1 by A12,AXIOMS:22;
     then i < len f by A13,AXIOMS:22;
     then i+1 <= len f by NAT_1:38;
then A14:   LSeg(f^g,i) = LSeg(f,i) by Th6;
       LSeg(f^g,j) = LSeg(f,j) by A13,Th6;
     hence thesis by A1,A6,A14,TOPREAL1:def 9;
    suppose
     j+1 > len f;
then A15:  len f <= j by NAT_1:38;
     then reconsider j' = j - len f as Nat by INT_1:18;
A16:   len f + j' = j by XCMPLX_1:27;
       j+1-len f <= len g by A9,A10,REAL_1:86;
then A17:   j'+1 <= len g by XCMPLX_1:29;
       now per cases;
      suppose
A18:     i <= len f;
       then A19:     f is non empty by A11,FINSEQ_3:27,RELAT_1:60;
         now per cases;
        suppose
A20:       i = len f;
         then len f +1+1 <= j by A6,NAT_1:38;
         then len f +(1+1) <= j by XCMPLX_1:1;
then A21:       1+1 <= j' by REAL_1:84;
then A22:       1 <= j' by AXIOMS:22;
then A23:       LSeg(f^g,j) = LSeg(g,j') by A16,Th7;
           g is non empty by A17,A22,GOBOARD2:3,RELAT_1:60;
         then LSeg(f^g,i) = LSeg(f/.len f,g/.1) by A19,A20,Th8;
         hence thesis by A5,A17,A21,A23;
        suppose i <> len f;
       then i < len f by A18,REAL_1:def 5;
         then i+1 <= len f by NAT_1:38;
then A24:       LSeg(f^g,i) = LSeg(f,i) by Th6;
           now per cases;
          suppose
A25:         j = len f;
           then i+1+1 <= len f by A6,NAT_1:38;
then A26:          i+(1+1) <= len f by XCMPLX_1:1;
             1 <= len g by A9,A10,A25,REAL_1:53;
           then g is non empty by FINSEQ_3:27,RELAT_1:60;
           then LSeg(f^g,j) = LSeg(f/.len f,g/.1) by A19,A25,Th8;
           hence thesis by A4,A11,A24,A26;
          suppose j <> len f;
           then len f < j by A15,REAL_1:def 5;
           then len f+1 <= j by NAT_1:38;
           then 1 <= j' by REAL_1:84;
           then LSeg(f^g,len f+j') = LSeg(g,j') by Th7;
then A27:         LSeg(f^g,j) c= L~g by A16,TOPREAL3:26;
             LSeg(f^g,i) c= L~f by A24,TOPREAL3:26;
           then LSeg(f^g,i) /\ LSeg(f^g,j) c= L~f /\ L~g by A27,XBOOLE_1:27;
           then LSeg(f^g,i) /\ LSeg(f^g,j) = {} by A3,XBOOLE_1:3;
           hence thesis by XBOOLE_0:def 7;
         end;
         hence thesis;
       end;
      hence thesis;
      suppose
A28:     i > len f;
       then reconsider i' = i - len f as Nat by INT_1:18;
A29:     len f + i' = i by XCMPLX_1:27;
         len f + 1 <= i by A28,NAT_1:38;
     then 1 <= i' by REAL_1:84;
then A30:     LSeg(f^g,len f+i') = LSeg(g,i') by Th7;
         i+1-len f < j' by A6,REAL_1:54;
then A31:     i'+1 < j' by XCMPLX_1:29;
         j <> len f by A6,A28,NAT_1:38;
       then len f < j by A15,REAL_1:def 5;
       then len f+1 <= j by NAT_1:38;
       then 1 <= j' by REAL_1:84;
       then LSeg(f^g,len f+j') = LSeg(g,j') by Th7;
       hence thesis by A2,A16,A29,A30,A31,TOPREAL1:def 9;
     end;
     hence thesis;
   end;
   hence thesis;
 end;

theorem Th38:
   f is unfolded s.n.c. & p in LSeg(f,n) & not p in rng f
    implies Ins(f,n,p) is s.n.c.
 proof assume that
A1: f is unfolded and
A2: f is s.n.c. and
A3: p in LSeg(f,n) and
A4: not p in rng f;
  let i,j such that
A5: i+1 < j;
  set fp = Ins(f,n,p);
  per cases;
  suppose
A6: i = 0 or j+1 > len fp;
     now per cases by A6;
    case i = 0;
     hence LSeg(fp,i) = {} by TOPREAL1:def 5;
    case j+1 > len fp;
     hence LSeg(fp,j) = {} by TOPREAL1:def 5;
   end; then LSeg(fp,i) /\ LSeg(fp,j) = {};
   hence thesis by XBOOLE_0:def 7;
  suppose that
A7: i <> 0 and
A8: j+1 <= len fp;
   set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n;
A9: fp = g1^f2 by FINSEQ_5:def 4;
A10: 1 <= i by A7,RLVECT_1:99;
     i <= i+1 by NAT_1:29;
then A11: i < j by A5,AXIOMS:22;
A12: len fp = len f + 1 by FINSEQ_5:72;
A13: len g1 = len f1 + 1 by FINSEQ_2:19;
then A14: g1/.len g1 = p by TOPREAL4:1;
A15: 1 <= n & n+1 <= len f by A3,TOPREAL1:def 5;
A16: n <= n+1 by NAT_1:29;
then A17: n <= len f by A15,AXIOMS:22;
then A18: len f1 = n by TOPREAL1:3;
     i+1+1 <= j by A5,NAT_1:38;
   then i+1+1+1 <= j+1 by AXIOMS:24;
   then i+1+1+1 <= len f + 1 by A8,A12,AXIOMS:22;
then A19: i+1+1 <= len f by REAL_1:53;
     i+1 <= i+1+1 by NAT_1:29;
then A20: i+1 <= len f by A19,AXIOMS:22;
     now per cases;
    suppose
A21:   j+1 <= n;
then A22:   j+1 <= len g1 by A13,A16,A18,AXIOMS:22;
       j <= j+1 by NAT_1:29;
     then i < j+1 by A11,AXIOMS:22;
     then i < n by A21,AXIOMS:22;
then A23:    i+1 <= n by NAT_1:38;
     then i+1 <= len g1 by A13,A16,A18,AXIOMS:22;
then A24:   LSeg(fp,i) = LSeg(g1,i) by A9,Th6
                .= LSeg(f1,i) by A18,A23,Th6
                .= LSeg(f,i) by A18,A23,Th3;
       LSeg(fp,j) = LSeg(g1,j) by A9,A22,Th6
                    .= LSeg(f1,j) by A18,A21,Th6
                    .= LSeg(f,j) by A18,A21,Th3;
     hence thesis by A2,A5,A24,TOPREAL1:def 9;
    suppose
     j+1 > n;
     then A25:   n <= j by NAT_1:38;
       now per cases;
      suppose
A26:     i <= n+1;
A27:     LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A15,TOPREAL1:def 5;
A28:     n in dom f1 by A15,A18,FINSEQ_3:27;
then A29:    f/.n = f1/.len f1 by A18,TOPREAL1:1;
        1 <= len f - n by A15,REAL_1:84;
      then 1 <= len f2 by A17,RFINSEQ:def 2;
    then 1 in dom f2 by FINSEQ_3:27;
then A30:    f/.(n+1) = f2/.1 by FINSEQ_5:30;
then A31:    LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1)
         = LSeg(f1/.len f1,f2/.1) by A3,A14,A27,A29,TOPREAL1:11;
A32:    f1/.len f1 = g1/.len f1 by A18,A28,GROUP_5:95;
A33:    LSeg(fp,n) = LSeg(g1,n) by A9,A13,A18,Th6
                 .= LSeg(f1/.len f1,p)
                   by A13,A14,A15,A18,A32,TOPREAL1:def 5;
A34:    fp/.(n+1+1) = f/.(n+1) by A15,FINSEQ_5:77;
A35:    1 <= n+1 by NAT_1:29;
A36:    n+1+1 <= len fp by A12,A15,AXIOMS:24;
        g1 is non empty by FINSEQ_1:48;
      then len g1 in dom g1 by FINSEQ_5:6;
     then fp/.(n+1) = g1/.len g1 by A9,A13,A18,GROUP_5:95;
then A37:     LSeg(fp,n+1) = LSeg(p,f2/.1)
         by A14,A30,A34,A35,A36,TOPREAL1:def 5;
A38:     LSeg(f1/.len f1,p) /\ LSeg(p,f2/.1) = {p}
         by A3,A27,A29,A30,TOPREAL1:14;
A39:     LSeg(fp,n) c= LSeg(f,n) by A27,A29,A30,A31,A33,XBOOLE_1:7;
A40:     LSeg(fp,n+1) c= LSeg(f,n) by A14,A27,A29,A30,A31,A37,XBOOLE_1:7;
         now per cases by REAL_1:def 5;
        suppose
         i < n;
then A41:      i+1 <= n by NAT_1:38;
         then i+1 <= len g1 by A13,A16,A18,AXIOMS:22;
then A42:       LSeg(fp,i) = LSeg(g1,i) by A9,Th6
                    .= LSeg(f1,i) by A18,A41,Th6
                    .= LSeg(f,i) by A18,A41,Th3;
           now per cases;
          suppose
A43:         j = n;
then A44:         LSeg(f,i) misses LSeg(f,n) by A2,A5,TOPREAL1:def 9;
             LSeg(fp,i) /\ LSeg(fp,j) c= LSeg(f,i) /\ LSeg(f,n)
            by A39,A42,A43,XBOOLE_1:26;
           then LSeg(fp,i) /\ LSeg(fp,j) c= {}
             by A44,XBOOLE_0:def 7;
           then LSeg(fp,i) /\ LSeg(fp,j) = {} by XBOOLE_1:3;
           hence thesis by XBOOLE_0:def 7;
          suppose j <> n;
         then n < j by A25,REAL_1:def 5;
then A45:         n+1 <= j by NAT_1:38;
             now per cases;
            suppose
A46:           j = n+1;
               now per cases;
              suppose
A47:             i+1 = n;
               then i+1 <= len g1 by A13,A18,NAT_1:29;
then A48:             LSeg(fp,i) = LSeg(g1,i) by A9,Th6
                          .= LSeg(f1,i) by A18,A47,Th6
                          .= LSeg(f,i) by A18,A47,Th3;
                 i+(1+1) <= len f by A19,XCMPLX_1:1;
then A49:               LSeg(fp,i) /\ LSeg(f,n) = {f/.n}
                by A1,A10,A47,A48,TOPREAL1:def 8;
               assume not thesis;
               then consider x being set such that
A50:             x in LSeg(fp,i) /\ LSeg(fp,j) by XBOOLE_0:4;
A51:             n in dom f by A15,GOBOARD2:3;
A52:             x in LSeg(fp,i) by A50,XBOOLE_0:def 3;
A53:             x in LSeg(fp,j) by A50,XBOOLE_0:def 3;
               then x in LSeg(f,n) by A14,A27,A29,A30,A31,A37,A46,XBOOLE_0:def
2;
               then x in {f/.n} by A49,A52,XBOOLE_0:def 3;
then A54:             x = f/.n by TARSKI:def 1;
               then x in LSeg(fp,n) by A29,A33,TOPREAL1:6;
               then x in LSeg(fp,n) /\ LSeg(fp,n+1) by A46,A53,XBOOLE_0:def 3;
               then p = f/.n by A33,A37,A38,A54,TARSKI:def 1;
               hence contradiction by A4,A51,PARTFUN2:4;
              suppose i+1 <> n;
             then i+1 < n by A41,REAL_1:def 5;
then A55:         LSeg(f,i) misses LSeg(f,n) by A2,TOPREAL1:def 9;
                 LSeg(fp,i) /\ LSeg(fp,j) c= LSeg(f,i) /\ LSeg(f,n)
                by A40,A42,A46,XBOOLE_1:26;
               then LSeg(fp,i) /\ LSeg(fp,j) c= {}
                 by A55,XBOOLE_0:def 7;
               then LSeg(fp,i) /\ LSeg(fp,j) = {} by XBOOLE_1:3;
               hence thesis by XBOOLE_0:def 7;
             end;
             hence thesis;
            suppose j <> n+1;
then A56:           n+1 < j by A45,REAL_1:def 5;
then A57:           n+1+1 <= j by NAT_1:38;
               1 < j by A10,A11,AXIOMS:22;
             then reconsider j' = j - 1 as Nat by INT_1:18;
             reconsider nj = j-(n+1) as Nat by A45,INT_1:18;
A58:           j = nj+(n+1) by XCMPLX_1:27;
A59:           1 <= nj by A57,REAL_1:84;
A60:           n+nj = n+j-(n+1) by XCMPLX_1:29
                  .= n+j-n-1 by XCMPLX_1:36
                  .= j' by XCMPLX_1:26;
               i+1+1 <= n+1 by A41,AXIOMS:24;
             then i+1+1 < j by A56,AXIOMS:22;
then A61:          i+1 < j' by REAL_1:86;
               LSeg(fp,j) = LSeg(f2,nj) by A9,A13,A18,A58,A59,Th7
                       .= LSeg(f,j') by A17,A59,A60,Th4;
             hence thesis by A2,A42,A61,TOPREAL1:def 9;
           end;
          hence thesis;
         end;
         hence thesis;
        suppose
A62:       i = n;
then A63:       n+1+1 <= j by A5,NAT_1:38;
           1 < j by A10,A11,AXIOMS:22;
         then reconsider j' = j - 1 as Nat by INT_1:18;
         reconsider nj = j-(n+1) as Nat by A5,A62,INT_1:18;
A64:       j = nj+(n+1) by XCMPLX_1:27;
A65:       1 <= nj by A63,REAL_1:84;
A66:       n+nj = n+j-(n+1) by XCMPLX_1:29
              .= n+j-n-1 by XCMPLX_1:36
              .= j' by XCMPLX_1:26;
A67:       LSeg(fp,j) = LSeg(f2,nj) by A9,A13,A18,A64,A65,Th7
                    .= LSeg(f,j') by A17,A65,A66,Th4;
           now per cases;
          suppose j <> n+1+1;
then n+1+1 < j by A63,REAL_1:def 5;
then i+1 < j' by A62,REAL_1:86;
then A68:        LSeg(f,i) misses LSeg(f,j') by A2,TOPREAL1:def 9;
             LSeg(fp,i) /\ LSeg(fp,j) c= LSeg(f,i) /\ LSeg(f,j')
              by A39,A62,A67,XBOOLE_1:26;
           then LSeg(fp,i) /\ LSeg(fp,j) c= {} by A68,XBOOLE_0:def 7;
           then LSeg(fp,i) /\ LSeg(fp,j) = {} by XBOOLE_1:3;
           hence thesis by XBOOLE_0:def 7;
          suppose
A69:         j = n+1+1;
then A70:         j' = n+1 by XCMPLX_1:26;
             j <= len f by A8,A12,REAL_1:53;
           then n+(1+1) <= len f by A69,XCMPLX_1:1;
then A71:         LSeg(f,n) /\ LSeg(f,j') = {f/.j'} by A1,A15,A70,TOPREAL1:def
8;
           assume not thesis;
           then consider x being set such that
A72:         x in LSeg(fp,i) /\ LSeg(fp,j) by XBOOLE_0:4;
A73:         n+1 in dom f by A15,GOBOARD2:3;
A74:         x in LSeg(fp,j) by A72,XBOOLE_0:def 3;
A75:         x in LSeg(fp,i) by A72,XBOOLE_0:def 3;
           then x in LSeg(f,n)
             by A27,A29,A30,A31,A33,A62,XBOOLE_0:def 2;
           then x in {f/.(n+1)} by A67,A70,A71,A74,XBOOLE_0:def 3;
then A76:         x = f/.(n+1) by TARSKI:def 1;
           then x in LSeg(fp,n+1) by A30,A37,TOPREAL1:6;
           then x in LSeg(fp,n) /\ LSeg(fp,n+1) by A62,A75,XBOOLE_0:def 3;
           then p = f/.(n+1) by A33,A37,A38,A76,TARSKI:def 1;
           hence contradiction by A4,A73,PARTFUN2:4;
         end;
         hence thesis;
        suppose i>n;
         then i>=n+1 by NAT_1:38;
then A77:       i = n+1 by A26,AXIOMS:21;
           1 < j by A10,A11,AXIOMS:22;
         then reconsider j' = j - 1 as Nat by INT_1:18;
           n+1 <= n+1+1 by NAT_1:29;
         then n+1 < j by A5,A77,AXIOMS:22;
         then reconsider nj = j-(n+1) as Nat by INT_1:18;
A78:       j = nj+(n+1) by XCMPLX_1:27;
A79:       1 <= nj by A5,A77,REAL_1:84;
A80:       n+nj = n+j-(n+1) by XCMPLX_1:29
              .= n+j-n-1 by XCMPLX_1:36
              .= j' by XCMPLX_1:26;
A81:       LSeg(fp,j) = LSeg(f2,nj) by A9,A13,A18,A78,A79,Th7
                    .= LSeg(f,j') by A17,A79,A80,Th4;
         n+1 < j' by A5,A77,REAL_1:86;
then A82:      LSeg(f,n) misses LSeg(f,j') by A2,TOPREAL1:def 9;
           LSeg(fp,n+1) c= LSeg(f,n) by A14,A27,A29,A30,A31,A37,XBOOLE_1:7;
         then LSeg(fp,n+1) /\ LSeg(fp,j) c= LSeg(f,n) /\ LSeg(f,j')
            by A81,XBOOLE_1:26;
         then LSeg(fp,n+1) /\ LSeg(fp,j) c= {} by A82,XBOOLE_0:def 7;
         then LSeg(fp,n+1) /\ LSeg(fp,j) = {} by XBOOLE_1:3;
         hence thesis by A77,XBOOLE_0:def 7;
       end;
       hence thesis;
      suppose A83: i > n+1;
then A84:     n+1+1 <= i by NAT_1:38;
       reconsider ni = i - (n+1) as Nat by A83,INT_1:18;
A85:     i = ni+(n+1) by XCMPLX_1:27;
       reconsider i' = i - 1 as Nat by A10,INT_1:18;
A86:     1 <= ni by A84,REAL_1:84;
         len f <= len f+1 by NAT_1:29;
       then i+1 <= len f+1 by A20,AXIOMS:22;
       then i+1-(n+1) <= len f+1- (n+1) by REAL_1:49;
       then i+1-(n+1) <= len f+1-1-n by XCMPLX_1:36;
       then i+1-(n+1) <= len f - n by XCMPLX_1:26;
then A87:     ni+1 <= len f - n by XCMPLX_1:29;
A88:     n+ni = n+i-(n+1) by XCMPLX_1:29
            .= n+i-n-1 by XCMPLX_1:36
            .= i' by XCMPLX_1:26;
A89:     LSeg(fp,i) = LSeg(f2,ni) by A9,A13,A18,A85,A86,Th7
                  .= LSeg(f,i') by A86,A87,A88,Th5;
         1 < j by A10,A11,AXIOMS:22;
       then reconsider j' = j - 1 as Nat by INT_1:18;
A90:      n+1 < j by A11,A83,AXIOMS:22;
       then reconsider nj = j-(n+1) as Nat by INT_1:18;
A91:     j = nj+(n+1) by XCMPLX_1:27;
         n+1+1 <= j by A90,NAT_1:38;
then A92:     1 <= nj by REAL_1:84;
A93:     n+nj = n+j-(n+1) by XCMPLX_1:29
            .= n+j-n-1 by XCMPLX_1:36
            .= j' by XCMPLX_1:26;
         i+1-1 < j' by A5,REAL_1:54;
then A94:    i'+1 < j' by XCMPLX_1:29;
         LSeg(fp,j) = LSeg(f2,nj) by A9,A13,A18,A91,A92,Th7
                 .= LSeg(f,j') by A17,A92,A93,Th4;
       hence thesis by A2,A89,A94,TOPREAL1:def 9;
     end;
     hence thesis;
   end;
   hence thesis;
 end;

Lm10:
   <*>(the carrier of TOP-REAL 2) is special
 proof set f = <*>(the carrier of TOP-REAL 2);
  let i such that
A1:  1 <= i and
A2:  i+1 <= len f;
    i <= i+1 by NAT_1:29;
  then i <= len f by A2,AXIOMS:22;
  then i <= 0 by FINSEQ_1:25;
  hence thesis by A1,AXIOMS:22;
 end;

definition
 cluster <*>(the carrier of TOP-REAL 2) -> special;
  coherence by Lm10;
end;

theorem Th39:
   <*p*> is special
 proof set f = <*p*>;
  let i such that
A1:  1 <= i and
A2:  i+1 <= len f;
    len f = 0+1 by FINSEQ_1:56;
  then i <= 0 by A2,REAL_1:53;
  hence thesis by A1,AXIOMS:22;
 end;

theorem Th40:
   p`1 = q`1 or p`2 = q`2 implies <*p,q*> is special
 proof assume
A1: p`1 = q`1 or p`2 = q`2;
  set f = <*p,q*>;
A2: len f = 1+1 by FINSEQ_1:61;
  let i such that
A3: 1 <= i and
A4: i+1 <= len f;
    i <= 1 by A2,A4,REAL_1:53;
  then i = 1 by A3,AXIOMS:21;
  then f/.i = p & f/.(i+1) = q by FINSEQ_4:26;
  hence thesis by A1;
 end;

Lm11:
   f is special implies f|n is special
 proof assume
A1: f is special;
  let i such that
A2: 1 <= i and
A3: i+1 <= len(f|n);
    i in dom(f|n) by A2,A3,GOBOARD2:3;
then A4: (f|n)/.i = f/.i by TOPREAL1:1;
    i+1 in dom(f|n) by A2,A3,GOBOARD2:3;
then A5: (f|n)/.(i+1) = f/.(i+1) by TOPREAL1:1;
    len(f|n) <= len f by FINSEQ_5:18;
  then i+1 <= len f by A3,AXIOMS:22;
  hence thesis by A1,A2,A4,A5,TOPREAL1:def 7;
 end;

Lm12:
   f is special implies f/^n is special
 proof assume
A1: f is special;
 per cases;
 suppose
A2: n <= len f;
  let i such that
A3: 1 <= i and
A4: i+1 <= len(f/^n);
A5: len(f/^n) = len f - n by A2,RFINSEQ:def 2;
    i in dom(f/^n) by A3,A4,GOBOARD2:3;
then A6:  (f/^n)/.i = f/.(n+i) by FINSEQ_5:30;
    i+1 in dom(f/^n) by A3,A4,GOBOARD2:3;
then A7:  (f/^n)/.(i+1) = f/.(n+(i+1)) by FINSEQ_5:30
                .= f/.(n+i+1) by XCMPLX_1:1;
    i <= n+i by NAT_1:29;
then A8: 1 <= n+i by A3,AXIOMS:22;
    n+(i+1) <= len f by A4,A5,REAL_1:84;
  then n+i+1 <= len f by XCMPLX_1:1;
  hence thesis by A1,A6,A7,A8,TOPREAL1:def 7;
 suppose n > len f;
  then f/^n = <*>(the carrier of TOP-REAL 2) by RFINSEQ:def 2;
  hence thesis;
 end;

definition let f be special FinSequence of TOP-REAL 2, n;
 cluster f|n -> special;
  coherence by Lm11;
 cluster f/^n -> special;
  coherence by Lm12;
end;

theorem Th41:
   p in rng f & f is special implies f:-p is special
 proof assume p in rng f;
  then ex i st i+1 = p..f & f:-p = f/^i by FINSEQ_5:52;
  hence thesis by Lm12;
 end;

Lm13:
   f is special implies f-:p is special
 proof f-:p = f|(p..f) by FINSEQ_5:def 1;
  hence thesis by Lm11;
 end;

definition let f be special FinSequence of TOP-REAL 2, p;
 cluster f-:p -> special;
  coherence by Lm13;
end;

theorem Th42:
   f is special implies Rev f is special
 proof assume
A1: f is special;
  let i such that
A2: 1 <= i and
A3: i+1 <= len(Rev f);
A4: len Rev f = len f by FINSEQ_5:def 3;
    i <= i+1 by NAT_1:29;
 then i <= len f by A3,A4,AXIOMS:22;
  then reconsider j = len f - i as Nat by INT_1:18;
    j <= len f - 1 by A2,REAL_2:106;
  then j+1 <= len f - 1 + 1 by AXIOMS:24;
then A5: j+1 <= len f by XCMPLX_1:27;
    i+1-i <= j by A3,A4,REAL_1:49;
then A6: 1 <= j by XCMPLX_1:26;
A7: i+j = len f by XCMPLX_1:27;
then A8: i+(j+1) = len f + 1 by XCMPLX_1:1;
    j+1 in dom f by A5,A6,GOBOARD2:3;
then A9: (Rev f)/.i = f/.(j+1) by A8,FINSEQ_5:69;
A10: 1+i+j = len f + 1 by A7,XCMPLX_1:1;
    j in dom f by A5,A6,GOBOARD2:3;
  then (Rev f)/.(i+1) = f/.j by A10,FINSEQ_5:69;
  hence thesis by A1,A5,A6,A9,TOPREAL1:def 7;
 end;

 Lm14:
   f is special & g is special &
     ((f/.len f)`1 = (g/.1)`1 or (f/.len f)`2 = (g/.1)`2)
    implies f^g is special
 proof assume that
A1:  f is special and
A2:  g is special and
A3:  (f/.len f)`1 = (g/.1)`1 or (f/.len f)`2 = (g/.1)`2;
  let i such that
A4:  1 <= i and
A5:  i+1 <= len(f^g);
A6:  len(f^g) = len f + len g by FINSEQ_1:35;
  per cases by REAL_1:def 5;
   suppose i < len f;
then A7:  i+1 <= len f by NAT_1:38;
    then i in dom f by A4,GOBOARD2:3;
then A8:  (f^g)/.i=f/.i by GROUP_5:95;
      i+1 in dom f by A4,A7,GOBOARD2:3;
    then (f^g)/.(i+1)=f/.(i+1) by GROUP_5:95;
    hence thesis by A1,A4,A7,A8,TOPREAL1:def 7;
   suppose
A9:  i = len f;
    then i in dom f by A4,FINSEQ_3:27;
then A10:  (f^g)/.i = f/.i by GROUP_5:95;
      1 <= len g by A5,A6,A9,REAL_1:53;
    then 1 in dom g by FINSEQ_3:27;
    hence thesis by A3,A9,A10,GROUP_5:96;
   suppose
A11:  i > len f;
    then reconsider j = i - len f as Nat by INT_1:18;
A12:  len f + j = i by XCMPLX_1:27;
then A13:  len f + (j+1) = i+1 by XCMPLX_1:1;
      len f + 1 <= i by A11,NAT_1:38;
then A14:  1 <= j by REAL_1:84;
      i+1-len f <= len g by A5,A6,REAL_1:86;
then A15:  j+1 <= len g by XCMPLX_1:29;
    then j in dom g by A14,GOBOARD2:3;
then A16:  (f^g)/.i= g/.j by A12,GROUP_5:96;
      j+1 in dom g by A14,A15,GOBOARD2:3;
    then (f^g)/.(i+1)= g/.(j+1) by A13,GROUP_5:96;
    hence thesis by A2,A14,A15,A16,TOPREAL1:def 7;
 end;

canceled;

theorem Th44:
   f is special & p in LSeg(f,n) implies Ins(f,n,p) is special
 proof assume that
A1: f is special and
A2: p in LSeg(f,n);
  set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n;
A3: g1/.len g1 = g1/.(len f1 + 1) by FINSEQ_2:19
                .= p by TOPREAL4:1;
A4: 1 <= n & n+1 <= len f by A2,TOPREAL1:def 5;
    n <= n+1 by NAT_1:29;
then A5: n <= len f by A4,AXIOMS:22;
then A6: len f1 = n by TOPREAL1:3;
then A7: n in dom f1 by A4,FINSEQ_3:27;
     1 <= len f - n by A4,REAL_1:84;
   then 1 <= len f2 by A5,RFINSEQ:def 2;
then A8: 1 in dom f2 by FINSEQ_3:27;
A9: LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A4,TOPREAL1:def 5;
A10: f/.n = f1/.len f1 by A6,A7,TOPREAL1:1;
A11: f/.(n+1) = f2/.1 by A8,FINSEQ_5:30;
A12: f1 is special by A1,Lm11;
  set p1 = f1/.len f1, p2 = f2/.1;
A13:  p1`1 = p2`1 or p1`2 = p2`2 by A1,A4,A10,A11,TOPREAL1:def 7;
A14:  p1 = |[p1`1, p1`2]| by EUCLID:57;
A15:  p2 = |[p2`1, p2`2]| by EUCLID:57;
    <*p*>/.1 = p by FINSEQ_4:25;
then A16: p1`1 = (<*p*>/.1)`1 or p1`2 = (<*p*>/.1)`2
     by A2,A9,A10,A11,A13,A14,A15,TOPREAL3:17,18;
     <*p*> is special by Th39;
then A17:  g1 is special by A12,A16,Lm14;
   set q1 = g1/.len g1;
A18: q1`1 = p2`1 or q1`2 = p2`2
     by A2,A3,A9,A10,A11,A13,A14,A15,TOPREAL3:17,18;
     f2 is special by A1,Lm12;
   then g1^f2 is special by A17,A18,Lm14;
  hence thesis by FINSEQ_5:def 4;
 end;

theorem Th45:
   q in rng f & 1<>q..f & q..f<>len f & f is unfolded s.n.c.
    implies L~(f-:q) /\ L~(f:-q) = {q}
 proof assume that
A1: q in rng f and
A2: 1 <> q..f and
A3: q..f <> len f and
A4: f is unfolded and
A5: f is s.n.c.;
A6: len(f-:q) = q..f by A1,FINSEQ_5:45;
       f-:q is non empty by A1,FINSEQ_5:50;
then A7: len(f-:q) in dom(f-:q) by FINSEQ_5:6;
A8: (f-:q)/.(q..f) = q by A1,FINSEQ_5:48;
A9:  1 in dom(f:-q) by FINSEQ_5:6;
A10: (f:-q)/.1 = q by FINSEQ_5:56;
A11: len(f:-q) = len f - q..f + 1 by A1,FINSEQ_5:53;
  thus L~(f-:q) /\ L~(f:-q) c= {q}
   proof let x be set;
    assume
A12:  x in L~(f-:q) /\ L~(f:-q);
    then reconsider p = x as Point of TOP-REAL 2;
      p in L~(f-:q) by A12,XBOOLE_0:def 3;
    then consider i such that
A13:  1 <= i and
A14:  i+1 <= len(f-:q) and
A15:  p in LSeg((f-:q),i) by Th13;
      p in L~(f:-q) by A12,XBOOLE_0:def 3;
    then consider j such that
A16:  1 <= j and
    j+1 <= len(f:-q) and
A17:  p in LSeg((f:-q),j) by Th13;
A18:  LSeg(f-:q,i) = LSeg(f,i) by A14,Th9;
      j <> 0 by A16;
    then consider j' being Nat such that
A19:  j=j'+1 by NAT_1:22;
A20:  LSeg(f:-q,j) = LSeg(f,j'+q..f) by A1,A19,Th10;
    per cases;
    suppose that
A21:   i+1 = len(f-:q) and
A22:   j' = 0;
       q..f <= len f by A1,FINSEQ_4:31;
     then q..f < len f by A3,REAL_1:def 5;
     then i+1+1 <= len f by A6,A21,NAT_1:38;
     then i+(1+1) <= len f by XCMPLX_1:1;
     then LSeg((f-:q),i) /\ LSeg(f:-q,j)
        = {f/.(q..f)} by A4,A6,A13,A18,A20,A21,A22,TOPREAL1:def 8
       .= {q} by A1,FINSEQ_5:41;
     hence x in {q} by A15,A17,XBOOLE_0:def 3;
    suppose that
A23:    i+1 = len(f-:q) and
A24:    j' <> 0;
       1 <= j' by A24,RLVECT_1:99;
     then i+1+1 <= j'+q..f by A6,A23,REAL_1:55;
     then i+1 < j'+q..f by NAT_1:38;
     then LSeg((f-:q),i) misses LSeg(f:-q,j) by A5,A18,A20,TOPREAL1:def 9;
     then LSeg((f-:q),i) /\ LSeg(f:-q,j) = {} by XBOOLE_0:def 7;
     hence thesis by A15,A17,XBOOLE_0:def 3;
    suppose i+1 <> len(f-:q);
then A25:   i+1 < q..f by A6,A14,REAL_1:def 5;
       q..f <= j'+q..f by NAT_1:29;
     then i+1 < j'+q..f by A25,AXIOMS:22;
     then LSeg((f-:q),i) misses LSeg(f:-q,j) by A5,A18,A20,TOPREAL1:def 9;
     then LSeg((f-:q),i) /\ LSeg(f:-q,j) = {} by XBOOLE_0:def 7;
     hence thesis by A15,A17,XBOOLE_0:def 3;
   end;
A26: q in rng(f-:q) by A6,A7,A8,PARTFUN2:4;
    1 <= q..f by A1,FINSEQ_4:31;
  then 1 < q..f by A2,REAL_1:def 5;
  then 1+1 <= q..f by NAT_1:38;
  then A27: rng(f-:q) c= L~(f-:q) by A6,Th18;
A28: q in rng(f:-q) by A9,A10,PARTFUN2:4;
    q..f <= len f by A1,FINSEQ_4:31;
  then q..f < len f by A3,REAL_1:def 5;
  then q..f+1 <= len f by NAT_1:38;
  then 1 <= len f - q..f by REAL_1:84;
  then 1+1<=len(f:-q) by A11,AXIOMS:24;
  then rng(f:-q) c= L~(f:-q) by Th18;
  then q in L~(f-:q) /\ L~(f:-q) by A26,A27,A28,XBOOLE_0:def 3;
  hence {q} c= L~(f-:q) /\ L~(f:-q) by ZFMISC_1:37;
 end;

theorem Th46:
   p <> q & (p`1 = q`1 or p`2 = q`2) implies <*p,q*> is being_S-Seq
 proof assume that
A1: p <> q and
A2: p`1 = q`1 or p`2 = q`2;
  set f = <*p,q*>;
  thus f is one-to-one by A1,FINSEQ_3:103;
  thus len f >= 2 by FINSEQ_1:61;
  thus thesis by A2,Lm2,Lm6,Th40;
 end;

definition
 mode S-Sequence_in_R2 is being_S-Seq FinSequence of TOP-REAL 2;
end;

theorem Th47:
   for f being S-Sequence_in_R2 holds Rev f is being_S-Seq
 proof let f be S-Sequence_in_R2;
  set g = Rev f;
  thus g is one-to-one;
    len g = len f by FINSEQ_5:def 3;
  hence len g >= 2 by TOPREAL1:def 10;
  thus thesis by Th29,Th36,Th42;
 end;

theorem
     for f being S-Sequence_in_R2 st i in dom f holds f/.i in L~f
 proof let f be S-Sequence_in_R2;
    len f >= 2 by TOPREAL1:def 10;
  hence thesis by GOBOARD1:16;
 end;

theorem
     p <> q & (p`1 = q`1 or p`2 = q`2) implies LSeg(p,q) is being_S-P_arc
 proof assume
A1: p <> q & (p`1 = q`1 or p`2 = q`2);
  take f = <*p,q*>;
  thus f is_S-Seq by A1,Th46;
  thus L~f = LSeg(p,q) by Th21;
 end;

Lm15: p in rng f implies L~(f-:p) c= L~f
 proof assume p in rng f;
  then L~f = L~(f-:p) \/ L~(f:-p) by Th25;
  hence thesis by XBOOLE_1:7;
 end;

Lm16: p in rng f implies L~(f:-p) c= L~f
 proof assume p in rng f;
  then L~f = L~(f-:p) \/ L~(f:-p) by Th25;
  hence thesis by XBOOLE_1:7;
 end;

theorem Th50:
   for f being S-Sequence_in_R2 st p in rng f & p..f <> 1
    holds f-:p is being_S-Seq
 proof let f be S-Sequence_in_R2 such that
A1:  p in rng f and
A2:  p..f <> 1;
  thus f-:p is one-to-one;
    1 <= p..f by A1,FINSEQ_4:31;
  then 1 < p..f by A2,REAL_1:def 5;
  then 1+1 <= p..f by NAT_1:38;
  hence len(f-:p) >= 2 by A1,FINSEQ_5:45;
  thus thesis;
 end;

theorem
     for f being S-Sequence_in_R2 st p in rng f & p..f <> len f
    holds f:-p is being_S-Seq
 proof let f be S-Sequence_in_R2 such that
A1:  p in rng f and
A2:  p..f <> len f;
  thus f:-p is one-to-one by A1,FINSEQ_5:59;
  hereby assume
A3: len(f:-p) < 2;
     p..f <= len f by A1,FINSEQ_4:31;
   then p..f < len f by A2,REAL_1:def 5;
   then 1 + p..f <= len f by NAT_1:38;
then A4:  len f - p..f >= 1 by REAL_1:84;
     len f - p..f + 1 < 1 + 1 by A1,A3,FINSEQ_5:53;
   hence contradiction by A4,AXIOMS:24;
  end;
  thus thesis by A1,Th28,Th35,Th41;
 end;

theorem Th52:
   for f being S-Sequence_in_R2 st p in LSeg(f,i) & not p in rng f
    holds Ins(f,i,p) is being_S-Seq
 proof let f be S-Sequence_in_R2 such that
A1: p in LSeg(f,i) and
A2: not p in rng f;
  set g = Ins(f,i,p);
  thus g is one-to-one by A2,FINSEQ_5:79;
A3: len f >= 2 by TOPREAL1:def 10;
     len g = len f + 1 by FINSEQ_5:72;
   then len g >= len f by NAT_1:29;
  hence len g >= 2 by A3,AXIOMS:22;
  thus g is unfolded by A1,Th33;
  thus g is s.n.c. by A1,A2,Th38;
  thus g is special by A1,Th44;
 end;

begin :: Special Polygons in TOP-REAL 2

definition
 cluster being_S-P_arc Subset of TOP-REAL 2;
  existence
 proof set p = |[ 0,0 ]|, q = |[ 1,1 ]|, f = <* p,|[p`1,q`2]|,q *>;
    0 <> 1 & p`1 = 0 & p`2 = 0 & q`1 = 1 & q`2 = 1 by EUCLID:56;
  then f is_S-Seq by TOPREAL3:41;
  then L~f is_S-P_arc by TOPREAL1:def 11;
  hence thesis;
 end;
end;

theorem
     P is_S-P_arc_joining p1,p2 implies P is_S-P_arc_joining p2,p1
 proof given f such that
A1:  f is_S-Seq and
A2:  P = L~f and
A3:  p1=f/.1 & p2 = f/.len f;
  take g = Rev f;
  thus g is_S-Seq & P = L~g by A1,A2,Th22,Th47;
    len f <> 0 by A1,TOPREAL1:def 10;
  then f is non empty & len g = len f by FINSEQ_1:25,FINSEQ_5:def 3;
  hence thesis by A3,FINSEQ_5:68;
 end;

definition let p1,p2; let P be Subset of TOP-REAL 2;
 pred p1,p2 split P means
:Def1: p1 <> p2 &
  ex f1,f2 being S-Sequence_in_R2 st
   p1 = f1/.1 & p1 = f2/.1 & p2 = f1/.len f1 & p2 = f2/.len f2 &
   L~f1 /\ L~f2 = {p1,p2} & P = L~f1 \/ L~f2;
end;

theorem Th54:
   p1,p2 split P implies p2,p1 split P
 proof
  assume
A1:  p1 <> p2;
  given f1,f2 being S-Sequence_in_R2 such that
A2:  p1 = f1/.1 & p1 = f2/.1 and
A3:  p2 = f1/.len f1 & p2 = f2/.len f2 and
A4:  L~f1 /\ L~f2 = {p1,p2} and
A5:  P = L~f1 \/ L~f2;
  thus p2 <> p1 by A1;
  reconsider g1 = Rev f1, g2 = Rev f2 as S-Sequence_in_R2 by Th47;
  take g1, g2;
    len g1 = len f1 & len g2 = len f2 by FINSEQ_5:def 3;
  hence p2 = g1/.1 & p2 = g2/.1 &
  p1 = g1/.len g1 & p1 = g2/.len g2 by A2,A3,FINSEQ_5:68;
    L~g1 = L~f1 & L~g2 = L~f2 by Th22;
  hence thesis by A4,A5;
 end;

Lm17:
 for f1,f2 being S-Sequence_in_R2 st
   p1 = f1/.1 & p1 = f2/.1 & p2 = f1/.len f1 & p2 = f2/.len f2 &
   L~f1 /\ L~f2 = {p1,p2} & P = L~f1 \/ L~f2 & q <> p1 & q in rng f1
  ex g1,g2 being S-Sequence_in_R2 st
   p1 = g1/.1 & p1 = g2/.1 & q = g1/.len g1 & q = g2/.len g2 &
   L~g1 /\ L~g2 = {p1,q} & P = L~g1 \/ L~g2
 proof let f1,f2 be S-Sequence_in_R2 such that
A1:  p1 = f1/.1 and
A2:  p1 = f2/.1 and
A3:  p2 = f1/.len f1 and
A4:  p2 = f2/.len f2 and
A5:  L~f1 /\ L~f2 = {p1,p2} and
A6:  P = L~f1 \/ L~f2 and
A7:  q <> p1 and
A8:  q in rng f1;
A9:  len f2 in dom f2 by FINSEQ_5:6;
A10:   now assume 1 = q..f1;
       then f1.1 = q & 1 in dom f1 by A8,FINSEQ_4:29,30;
       hence contradiction by A1,A7,FINSEQ_4:def 4;
      end;
      then reconsider g1 = f1-:q as S-Sequence_in_R2 by A8,Th50;
      set f1' = Rev(f1:-q);
      1 in dom f2 by FINSEQ_5:6;
    then 1 <= len f2 by FINSEQ_3:27;
      then reconsider l = len f2 - 1 as Nat by INT_1:18;
      set f2' = f2|l;
      set g2 = f2'^f1';
      set Z = rng f2' /\ rng f1';
A11:    l < len f2 by SQUARE_1:29;
then A12:    len f2' = l by TOPREAL1:3;
     reconsider f1q = f1:-q as one-to-one FinSequence of TOP-REAL 2 by A8,
FINSEQ_5:59;
A13:     1 in dom f1 by FINSEQ_5:6;
        now assume
A14:      p1 in rng(f1:-q);
       set l = p1..(f1:-q);
A15:      l in dom(f1:-q) by A14,FINSEQ_4:30;
         (f1:-q).l = p1 by A14,FINSEQ_4:29;
then A16:      (f1:-q)/.l = p1 by A15,FINSEQ_4:def 4;
         l <> 0 by A14,FINSEQ_4:31;
       then consider j such that
A17:      l = j+1 by NAT_1:22;
A18:      (f1:-q)/.l = f1/.(j+q..f1) by A8,A15,A17,FINSEQ_5:55;
         j+q..f1 in dom f1 by A8,A15,A17,FINSEQ_5:54;
       then j+q..f1 = 1 by A1,A13,A16,A18,PARTFUN2:17;
       then 1 <= q..f1 & q..f1 <= 1 by A8,FINSEQ_4:31,NAT_1:29;
       hence contradiction by A10,AXIOMS:21;
      end;
      then not p1 in rng f1' by FINSEQ_5:60;
then A19:     not p1 in Z by XBOOLE_0:def 3;
A20:    p2..f2 = len f2 by A4,A9,FINSEQ_5:44;
     now assume
A21:      p2 in rng f2';
       then p2..f2' = p2..f2 by FINSEQ_5:43;
       hence contradiction by A11,A12,A20,A21,FINSEQ_4:31;
      end;
      then not p2 in Z by XBOOLE_0:def 3;
then A22:    Z <> {p1} & Z <> {p2} & Z <> {p1,p2} by A19,TARSKI:def 1,def 2;
        rng f1' = rng(f1:-q) by FINSEQ_5:60;
      then rng f2' c= rng f2 & rng f1' c= rng f1
        by A8,FINSEQ_5:21,58;
then A23:    Z c= rng f2 /\ rng f1 by XBOOLE_1:27;
        len f1 >= 2 & len f2 >= 2 by TOPREAL1:def 10;
    then rng f1 c= L~f1 & rng f2 c= L~f2 by Th18;
      then rng f2 /\ rng f1 c= L~f1 /\ L~f2 by XBOOLE_1:27;
      then Z c= {p1,p2} by A5,A23,XBOOLE_1:1;
      then Z = {} by A22,ZFMISC_1:42;
then A24:     rng f2' misses rng f1' by XBOOLE_0:def 7;
       Rev f1q is one-to-one;
then A25:   g2 is one-to-one by A24,FINSEQ_3:98;
A26:     1 <= q..f1 by A8,FINSEQ_4:31;
        len(f1:-q) <> 0 by FINSEQ_1:25;
      then len(f1:-q) >= 1 by RLVECT_1:99;
then A27:    len f1' >= 1 by FINSEQ_5:def 3;
then A28:    len f1' in dom f1' by FINSEQ_3:27;
        len f2 >= 2 by TOPREAL1:def 10;
      then A29: len f2 - 1 >= 1+1-1 by REAL_1:49;
then A30:     len f2' >= 1 by A11,TOPREAL1:3;
        len f2' + len f1' >= 1+1 by A12,A27,A29,REAL_1:55;
then A31:     len g2 >= 2 by FINSEQ_1:35;
A32:     1 in dom f2' by A12,A29,FINSEQ_3:27;
A33:     f2' is non empty by A30,FINSEQ_3:27,RELAT_1:60;
       f1:-q is unfolded by A8,Th28;
then A34:     f1' is unfolded by Th29;
A35:     l+1 = len f2 by XCMPLX_1:27;
A36:     l in dom f2' by A12,A29,FINSEQ_3:27;
then A37:     f2'/.len f2' = f2/.l by A12,TOPREAL1:1;
A38:     f1'/.1 = (f1:-q)/.len(f1:-q) by FINSEQ_5:68
                .= f2/.len f2 by A3,A4,A8,FINSEQ_5:57;
      dom f2 = Seg len f2 & dom f2' = Seg len f2' by FINSEQ_1:def 3;
then A39:     len f2' in dom f2 by A12,A35,A36,FINSEQ_2:9;
A40:  now assume p1 in L~f1';
then A41:       p1 in L~(f1:-q) by Th22;
        then consider i such that
A42:      1 <= i and
        i+1 <= len(f1:-q) and
A43:      p1 in LSeg(f1:-q,i) by Th13;
A44:      1 + 1 <= len f1 by TOPREAL1:def 10;
         p1 in LSeg(f1/.1,f1/.(1+1)) by A1,TOPREAL1:6;
then A45:      p1 in LSeg(f1,1) by A44,TOPREAL1:def 5;
         i <> 0 by A42;
       then consider j such that
A46:      i = j+1 by NAT_1:22;
A47:      LSeg(f1:-q,i) = LSeg(f1,j+q..f1) by A8,A46,Th10;
      then p1 in LSeg(f1,1) /\ LSeg(f1,j+q..f1) by A43,A45,XBOOLE_0:def 3;
then A48:       LSeg(f1,1) meets LSeg(f1,j+q..f1) by XBOOLE_0:4;
A49:      1 < q..f1 by A10,A26,REAL_1:def 5;
       per cases;
        suppose
A50:       j = 0;
A51:       1+1 <= q..f1 by A49,NAT_1:38;
           now per cases by A51,REAL_1:def 5;
          suppose
A52:         q..f1 = 2;
         A53: q..f1 <= len f1 by A8,FINSEQ_4:31;
             now per cases by A52,A53,REAL_1:def 5;
           suppose len f1 = 2;
            then len(f1:-q) = len f1 - len f1 + 1 by A8,A52,FINSEQ_5:53;
            then len(f1:-q) = 0+1 by XCMPLX_1:14;
            hence contradiction by A41,TOPREAL1:28;
           suppose len f1 > 2;
            then 1+2 <= len f1 by NAT_1:38;
            then LSeg(f1,1) /\ LSeg(f1,1+1) = {f1/.(1+1)} by TOPREAL1:def 8;
            then p1 in {f1/.2} by A43,A45,A47,A50,A52,XBOOLE_0:def 3;
then A54:           p1 = f1/.2 by TARSKI:def 1;
              1 <> 2 & 2 in dom f1 by A8,A52,FINSEQ_4:30;
            hence contradiction by A1,A13,A54,PARTFUN2:17;
           end;
           hence contradiction;
          suppose q..f1 > 2;
           then 1+1 < j+q..f1 by A50;
           hence contradiction by A48,TOPREAL1:def 9;
         end;
         hence contradiction;
        suppose j <> 0;
         then 1 <= j by RLVECT_1:99;
         then 1+1 < j+q..f1 by A49,REAL_1:67;
         hence contradiction by A48,TOPREAL1:def 9;
      end;
A55:   LSeg(f2'/.len f2',f1'/.1) = LSeg(f2,l)
       by A29,A35,A37,A38,TOPREAL1:def 5;
A56:  now assume len f1' <> 1;
      then 1 < len f1' by A27,REAL_1:def 5;
then A57:    1+1 <= len f1' by NAT_1:38;
        now let x be set;
       hereby
        assume
A58:      x in LSeg(f2'/.len f2',f1'/.1) /\ LSeg(f1',1);
A59:      LSeg(f2'/.len f2',f1'/.1) c=L~f2 by A55,TOPREAL3:26;
        reconsider m = len f1'-2 as Nat by A57,INT_1:18;
       m+1+1 = m+(1+1) by XCMPLX_1:1;
      then m+1+1 = len f1' by XCMPLX_1:27
              .= len(f1:-q) by FINSEQ_5:def 3;
        then LSeg(f1',1) = LSeg(f1:-q,m+1) by Th2
                        .= LSeg(f1,m+q..f1) by A8,Th10;
        then LSeg(f1',1) c= L~f1 by TOPREAL3:26;
        then A60: LSeg(f2'/.len f2',f1'/.1) /\ LSeg(f1',1) c= {p1,p2}
          by A5,A59,XBOOLE_1:27;
          LSeg(f1',1) c= L~f1' by TOPREAL3:26;
        then not p1 in LSeg(f1',1) by A40;
        then not p1 in LSeg(f2'/.len f2',f1'/.1) /\ LSeg(f1',1)
         by XBOOLE_0:def 3;
        hence x = f1'/.1 by A4,A38,A58,A60,TARSKI:def 2;
       end;
       assume
A61:     x = f1'/.1;
       then x in LSeg(f1'/.1,f1'/.(1+1)) by TOPREAL1:6;
then A62:     x in LSeg(f1',1) by A57,TOPREAL1:def 5;
         x in LSeg(f2'/.len f2',f1'/.1) by A61,TOPREAL1:6;
       hence x in LSeg(f2'/.len f2',f1'/.1) /\ LSeg(f1',1)
        by A62,XBOOLE_0:def 3;
      end;
      hence LSeg(f2'/.len f2',f1'/.1) /\ LSeg(f1',1) = {f1'/.1}
       by TARSKI:def 1;
     end;
A63:  now
      per cases;
      suppose len f2' = 1 & len f1' = 1;
       then len g2 = 1+1 by FINSEQ_1:35;
       hence g2 is unfolded by Th27;
      suppose that
A64:     len f2' <> 1 and
A65:     len f1' = 1;
A66:     len f2' > 1 by A12,A29,A64,REAL_1:def 5;
         len f2' <> 0 by A30;
       then consider k such that
A67:     k+1 = len f2' by NAT_1:22;
A68:     1 <= k by A66,A67,NAT_1:38;
         l+1 <= len f2 by A11,NAT_1:38;
then A69:     k+(1+1) <= len f2 by A12,A67,XCMPLX_1:1;
         LSeg(f2',k) = LSeg(f2,k) by A67,Th3;
then A70:     LSeg(f2',k) /\ LSeg(f2'/.len f2',f1'/.1) = {f2'/.len f2'}
         by A12,A37,A55,A67,A68,A69,TOPREAL1:def 8;
         f1' = <*f1'/.1*> by A65,FINSEQ_5:15;
       hence g2 is unfolded by A67,A70,Th31;
      suppose that
A71:      len f2' = 1 and
A72:      len f1' <> 1;
        f2' = <*f2'/.len f2'*> by A71,FINSEQ_5:15;
       hence g2 is unfolded by A34,A56,A72,Th30;
      suppose that
A73:     len f2' <> 1 and
A74:     len f1' <> 1;
A75:     len f2' > 1 by A12,A29,A73,REAL_1:def 5;
         len f2' <> 0 by A30;
       then consider k such that
A76:     k+1 = len f2' by NAT_1:22;
A77:     1 <= k by A75,A76,NAT_1:38;
         l+1 <= len f2 by A11,NAT_1:38;
then A78:     k+(1+1) <= len f2 by A12,A76,XCMPLX_1:1;
         LSeg(f2',k) = LSeg(f2,k) by A76,Th3;
     then LSeg(f2',k) /\ LSeg(f2'/.len f2',f1'/.1) = {f2'/.len f2'}
         by A12,A37,A55,A76,A77,A78,TOPREAL1:def 8;
       hence g2 is unfolded by A34,A56,A74,A76,Th32;
     end;
      f1:-q is s.n.c. by A8,Th35;
then A79:    f1' is s.n.c. by Th36;
        L~(f1:-q) c= L~f1 by A8,Lm16;
then A80:    L~f1' c= L~f1 by Th22;
        L~f2' c= L~f2 by Lm1;
      then L~f2' /\ L~f1' c= {p1,p2} by A5,A80,XBOOLE_1:27;
then A81:     L~f2' /\ L~f1' = {} or
         L~f2' /\ L~f1' = {p1} or L~f2' /\ L~f1' = {p2} or
         L~f2' /\ L~f1' = {p1,p2} by ZFMISC_1:42;
A82:   now let i such that
       1<=i and
A83:     i+2<=len f2';
         i+(1+1) <= len f2' by A83;
       then i+1+1 <= len f2' by XCMPLX_1:1;
then A84:     i+1 < len f2' by NAT_1:38;
       then LSeg(f2',i) = LSeg(f2,i) by Th3;
       hence LSeg(f2',i) misses LSeg(f2'/.len f2',f1'/.1)
        by A12,A55,A84,TOPREAL1:def 9;
      end;
A85:   now let i such that
A86:     2<=i and
A87:     i+1 <= len f1';
         LSeg(f1',i) c= L~f1' by TOPREAL3:26;
       then A88: not p1 in LSeg(f1',i) by A40;
A89:     LSeg(f2'/.len f2',f1'/.1) c=L~f2 by A55,TOPREAL3:26;
       reconsider m = len f1'-(i+1) as Nat by A87,INT_1:18;
       m+1+i = m+(i+1) by XCMPLX_1:1;
      then m+1+i = len f1' by XCMPLX_1:27
              .= len(f1:-q) by FINSEQ_5:def 3;
then A90:      LSeg(f1',i) = LSeg(f1:-q,m+1) by Th2
                    .= LSeg(f1,m+q..f1) by A8,Th10;
A91:     now
A92:       len f1 >= 1+1 by TOPREAL1:def 10;
         then len f1 >= 1 by AXIOMS:22;
         then reconsider k = len f1 - 1 as Nat by INT_1:18;
A93:       k+1 = len f1 by XCMPLX_1:27;
then A94:       1 <= k by A92,REAL_1:53;
           p2 in LSeg(f1/.k,f1/.len f1) by A3,TOPREAL1:6;
then A95:       p2 in LSeg(f1,k) by A93,A94,TOPREAL1:def 5;
A96:       len f1' = len(f1:-q) by FINSEQ_5:def 3;
A97:       len f1 - i
            = len f1 - q..f1 + q..f1 - i by XCMPLX_1:27
           .= len f1 - q..f1 + 1 - 1 + q..f1 - i by XCMPLX_1:26
           .= len f1' - 1 + q..f1 - i by A8,A96,FINSEQ_5:53
           .= len f1' - 1 - i + q..f1 by XCMPLX_1:29
           .= m + q..f1 by XCMPLX_1:36;
         per cases;
         suppose i = 1+1;
then A98:        m + q..f1 + 1 = len f1 - 1 - 1 + 1 by A97,XCMPLX_1:36
                        .= k by XCMPLX_1:27;
A99:        1 <= q..f1 by A8,FINSEQ_4:31;
            q..f1 <= m+q..f1 by NAT_1:29;
then A100:        1 <= m + q..f1 by A99,AXIOMS:22;
            m+q..f1+(1+1) = len f1 by A93,A98,XCMPLX_1:1;
then A101:        LSeg(f1,m + q..f1) /\ LSeg(f1,k) = {f1/.k}
            by A98,A100,TOPREAL1:def 8;
A102:        1 <= k by A92,REAL_1:84;
             k <= len f1 by A93,NAT_1:29;
then A103:        k in dom f1 by A102,FINSEQ_3:27;
A104:        len f1 in dom f1 by FINSEQ_5:6;
            p2 in LSeg(f1/.k,f1/.(k+1)) by A3,A93,TOPREAL1:6;
then A105:        p2 in LSeg(f1,k) by A93,A102,TOPREAL1:def 5;
          assume p2 in LSeg(f1',i);
          then p2 in {f1/.k} by A90,A101,A105,XBOOLE_0:def 3;
          then f1/.len f1 = f1/.k by A3,TARSKI:def 1;
          then len f1 - k = len f1 - len f1 by A103,A104,PARTFUN2:17
                          .= 0 by XCMPLX_1:14;
          then 0 = len f1 - len f1 + 1 by XCMPLX_1:37
                .= 0 + 1 by XCMPLX_1:14;
          hence contradiction;
         suppose i <> 2;
          then 2 < i by A86,REAL_1:def 5;
          then 2+1 <= i by NAT_1:38;
          then len f1 - i <= len f1 - (1+2) by REAL_2:106;
          then len f1 - i <= len f1 - 1 - 2 by XCMPLX_1:36;
then A106:         len f1 - i + (1+1) <= k by REAL_1:84;
            len f1 - i + (1+1) = m + q..f1 + 1 + 1 by A97,XCMPLX_1:1;
          then m+q..f1 +1 < k by A106,NAT_1:38;
          then LSeg(f1,k) misses LSeg(f1,m+q..f1) by TOPREAL1:def 9;
          then LSeg(f1,k) /\ LSeg(f1,m+q..f1) = {} by XBOOLE_0:def 7;
          hence not p2 in LSeg(f1',i) by A90,A95,XBOOLE_0:def 3;
        end;
         LSeg(f1',i) c= L~f1 by A90,TOPREAL3:26;
then A107:     LSeg(f2'/.len f2',f1'/.1) /\ LSeg(f1',i) c= {p1,p2}
         by A5,A89,XBOOLE_1:27;
         now given x being set such that
A108:      x in LSeg(f2'/.len f2',f1'/.1) /\ LSeg(f1',i);
          x = p1 or x = p2 by A107,A108,TARSKI:def 2;
        hence contradiction by A88,A91,A108,XBOOLE_0:def 3;
       end;
       then LSeg(f1',i) /\
 LSeg(f2'/.len f2',f1'/.1) = {} by XBOOLE_0:def 1;
       hence LSeg(f1',i) misses
 LSeg(f2'/.len f2',f1'/.1) by XBOOLE_0:def 7;
      end;
        now assume p2 in L~f2';
        then consider i such that
A109:      1 <= i and
A110:      i+1 <= len(f2') and
A111:      p2 in LSeg(f2',i) by Th13;
A112:      LSeg(f2',i) = LSeg(f2,i) by A110,Th3;
          p2 in LSeg(f2/.len f2',p2) by TOPREAL1:6;
        then p2 in LSeg(f2,len f2') by A4,A12,A29,A35,TOPREAL1:def 5;
then A113:      p2 in LSeg(f2,i) /\ LSeg(f2,len f2') by A111,A112,XBOOLE_0:def
3
;
then A114:      LSeg(f2,i) meets LSeg(f2,len f2') by XBOOLE_0:4;
A115:      len f2 <> len f2' by A11,TOPREAL1:3;
       per cases;
       suppose
A116:       i+1 = len(f2');
        then i + (1+1) = len f2 by A12,A35,XCMPLX_1:1;
        then LSeg(f2,i) /\ LSeg(f2,len f2') = {f2/.len f2'}
           by A109,A116,TOPREAL1:def 8;
        then p2 = f2/.len f2' by A113,TARSKI:def 1;
        hence contradiction by A4,A9,A39,A115,PARTFUN2:17;
       suppose i+1 <> len(f2');
        then i+1 < len(f2') by A110,REAL_1:def 5;
        hence contradiction by A114,TOPREAL1:def 9;
      end;
      then not p1 in L~f2' /\ L~f1' & not p2 in L~f2' /\ L~f1'
       by A40,XBOOLE_0:def 3;
      then L~f2' misses L~f1' by A81,TARSKI:def 1,def 2,XBOOLE_0:def 7;
   then A117: f2'^f1' is s.n.c. by A79,A82,A85,Th37;
        f1:-q is special by A8,Th41;
then A118:    f1' is special by Th42;
        (f2'/.len f2')`1 = (f1'/.1)`1 or (f2'/.len f2')`2 = (f1'/.1)`2
       by A29,A35,A37,A38,TOPREAL1:def 7;
      then g2 is special by A118,Lm14;
      then reconsider g2 as S-Sequence_in_R2 by A25,A31,A63,A117,TOPREAL1:def
10;
      take g1,g2;
      thus
A119:     p1 = g1/.1 by A1,A8,FINSEQ_5:47;
A120:     1 in dom g2 by FINSEQ_5:6;
      hence
A121:     g2/.1 = g2.1 by FINSEQ_4:def 4
               .= f2'.1 by A32,FINSEQ_1:def 7
               .= f2'/.1 by A32,FINSEQ_4:def 4
               .= p1 by A2,A32,TOPREAL1:1;
      thus
A122:       q = g1/.(q..f1) by A8,FINSEQ_5:48
           .= g1/.len g1 by A8,FINSEQ_5:45;
A123:    1 in dom(f1:-q) by FINSEQ_5:6;
A124:    len g2 in dom g2 by FINSEQ_5:6;
      hence
A125:      g2/.len g2 = g2.(len g2) by FINSEQ_4:def 4
                     .= g2.(len f2' + len f1') by FINSEQ_1:35
                     .= f1'.(len f1') by A28,FINSEQ_1:def 7
                     .= f1'.(len (f1:-q)) by FINSEQ_5:def 3
                     .= (f1:-q).1 by FINSEQ_5:65
                     .= (f1:-q)/.1 by A123,FINSEQ_4:def 4
                     .= q by FINSEQ_5:56;
        len g1 >= 2 & len g2 >= 2 by TOPREAL1:def 10;
then A126:    rng g1 c= L~g1 & rng g2 c= L~g2 by Th18;
A127:    len g1 in dom g1 by FINSEQ_5:6;
A128:   1 in dom g1 by FINSEQ_5:6;
A129:   L~f2 \/ L~f1' = L~(f2'^<*p2*>) \/ L~f1' by A4,A35,FINSEQ_5:24
                   .= L~f2' \/ LSeg(f2'/.len f2',f1'/.1) \/ L~f1'
                       by A4,A32,A38,Th19,RELAT_1:60
                   .= L~g2 by A28,A33,Th23,RELAT_1:60;
      thus {p1,q} = L~g1 /\ L~g2
       proof
        hereby let x be set;
         assume A130: x in {p1,q};
         per cases by A130,TARSKI:def 2;
          suppose
A131:        x = p1;
           p1 in rng g1 & p1 in rng g2
          by A119,A120,A121,A128,PARTFUN2:4;
         hence x in L~g1 /\ L~g2 by A126,A131,XBOOLE_0:def 3;
          suppose
A132:        x = q;
           q in rng g1 & q in rng g2 by A122,A124,A125,A127,PARTFUN2:4;
         hence x in L~g1 /\ L~g2 by A126,A132,XBOOLE_0:def 3;
        end;
A133:     L~g1 /\ L~g2 = L~g1 /\ L~f2 \/ L~g1 /\ L~f1' by A129,XBOOLE_1:23;
A134:    len g1 = q..f1 by A8,FINSEQ_5:45;
A135:    q..f1 in dom f1 by A8,FINSEQ_4:30;
A136:    len f1 in dom f1 by FINSEQ_5:6;
A137:    q = f1.(q..f1) by A8,FINSEQ_4:29
         .= f1/.(q..f1) by A135,FINSEQ_4:def 4;
       per cases;
        suppose
A138:       q <> p2;
           now assume p2 in L~g1;
           then consider i such that
A139:         1 <= i and
A140:         i+1 <= len g1 and
A141:         p2 in LSeg(g1,i) by Th13;
A142:        p2 in LSeg(f1,i) by A140,A141,Th9;
A143:         q..f1 <= len f1 by A8,FINSEQ_4:31;
           then 1 <= len f1 by A26,AXIOMS:22;
           then reconsider j = len f1 - 1 as Nat by INT_1:18;
A144:         j+1 = len f1 by XCMPLX_1:27;
           1 < q..f1 by A10,A26,REAL_1:def 5;
           then 1 < len f1 by A143,AXIOMS:22;
then A145:         1 <= j by A144,NAT_1:38;
             p2 in LSeg(f1/.j,f1/.(j+1)) by A3,A144,TOPREAL1:6;
then A146:          p2 in LSeg(f1,j) by A144,A145,TOPREAL1:def 5;
             q..f1 < len f1 by A3,A137,A138,A143,REAL_1:def 5;
then A147:         q..f1 <= j by A144,NAT_1:38;
then A148:         i+1 <= j by A134,A140,AXIOMS:22;
           per cases;
           suppose
A149:           i+1 = j;
             then i+(1+1) = j+1 by XCMPLX_1:1;
             then LSeg(f1,i) /\ LSeg(f1,i+1) = {f1/.(i+1)}
              by A139,A144,TOPREAL1:def 8;
             then p2 in {f1/.(i+1)} by A142,A146,A149,XBOOLE_0:def 3;
             then p2 = f1/.(i+1) by TARSKI:def 1;
             hence contradiction by A134,A137,A138,A140,A147,A149,AXIOMS:21;
           suppose i+1 <> j;
            then i+1 < j by A148,REAL_1:def 5;
            then LSeg(f1,i) misses LSeg(f1,j) by TOPREAL1:def 9;
            then LSeg(f1,i) /\ LSeg(f1,j) = {} by XBOOLE_0:def 7;
            hence contradiction by A142,A146,XBOOLE_0:def 3;
         end;
then A150:       not p2 in L~g1 /\ L~f2 by XBOOLE_0:def 3;
A151:       L~g1 /\ L~f1' = L~g1 /\ L~(f1:-q) by Th22
                      .= {q} by A3,A8,A10,A137,A138,Th45;
           L~g1 c= L~f1 by A8,Lm15;
         then L~g1 /\ L~f2 c= {p1,p2} by A5,XBOOLE_1:26;
         then L~g1 /\ L~f2 = {} or L~g1 /\ L~f2 = {p1} or
              L~g1 /\ L~f2 = {p2} or L~g1 /\ L~f2 = {p1,p2} by ZFMISC_1:42;
         then L~g1 /\
 L~f2 c= {p1} by A150,TARSKI:def 1,def 2,ZFMISC_1:39;
         then L~g1 /\ L~g2 c= {p1} \/ {q} by A133,A151,XBOOLE_1:9;
         hence L~g1 /\ L~g2 c= {p1,q} by ENUMSET1:41;
        suppose
A152:        q = p2;
          p2..f1 = len f1 by A3,A136,FINSEQ_5:44;
then A153:        len(f1:-q) = len f1 - len f1 + 1 by A8,A152,FINSEQ_5:53
                     .= 0+1 by XCMPLX_1:14;
A154:        L~g1 /\ L~f1' = L~g1 /\ L~(f1:-q) by Th22
                       .= L~g1 /\ {} by A153,TOPREAL1:28
                       .= {};
           L~g1 c= L~f1 by A8,Lm15;
         hence L~g1 /\ L~g2 c= {p1,q} by A5,A133,A152,A154,XBOOLE_1:26;
       end;
      thus P = L~(f1-:q) \/ L~(f1:-q) \/ L~f2 by A6,A8,Th25
            .= L~g1 \/ (L~f2 \/ L~(f1:-q)) by XBOOLE_1:4
            .= L~g1 \/ L~g2 by A129,Th22;
 end;

theorem Th55:
   p1,p2 split P & q in P & q <> p1 implies p1,q split P
 proof assume p1 <> p2;
  given f1,f2 being S-Sequence_in_R2 such that
A1: p1 = f1/.1 and
A2: p1 = f2/.1 and
A3: p2 = f1/.len f1 and
A4: p2 = f2/.len f2 and
A5: L~f1 /\ L~f2 = {p1,p2} and
A6: P = L~f1 \/ L~f2;
  assume
A7: q in P;
  assume
A8: q <> p1;
  hence p1 <> q;
  per cases by A6,A7,XBOOLE_0:def 2;
   suppose
A9:  q in L~f1;
      now per cases;
     suppose q in rng f1;
      hence thesis by A1,A2,A3,A4,A5,A6,A8,Lm17;
     suppose
A10:    not q in rng f1;
      consider i such that
A11:    1 <= i and
A12:    i+1 <= len f1 and
A13:    q in LSeg(f1,i) by A9,Th13;
      reconsider f1' = Ins(f1,i,q) as S-Sequence_in_R2 by A10,A13,Th52;
A14:    q in rng f1' by FINSEQ_5:74;
A15:   p1 = f1'/.1 by A1,A11,FINSEQ_5:78;
        len f1' = len f1 + 1 by FINSEQ_5:72;
then A16:   p2 = f1'/.len f1' by A3,A12,FINSEQ_5:77;
       L~f1' = L~f1 by A13,Th26;
     hence thesis by A2,A4,A5,A6,A8,A14,A15,A16,Lm17;
    end;
    hence thesis;
   suppose
A17:   q in L~f2;
      now per cases;
     suppose q in rng f2;
      hence thesis by A1,A2,A3,A4,A5,A6,A8,Lm17;
     suppose
A18:    not q in rng f2;
      consider i such that
A19:    1 <= i and
A20:    i+1 <= len f2 and
A21:    q in LSeg(f2,i) by A17,Th13;
      reconsider f2' = Ins(f2,i,q) as S-Sequence_in_R2 by A18,A21,Th52;
A22:    q in rng f2' by FINSEQ_5:74;
A23:   p1 = f2'/.1 by A2,A19,FINSEQ_5:78;
        len f2' = len f2 + 1 by FINSEQ_5:72;
then A24:   p2 = f2'/.len f2' by A4,A20,FINSEQ_5:77;
       L~f2' = L~f2 by A21,Th26;
     hence thesis by A1,A3,A5,A6,A8,A22,A23,A24,Lm17;
    end;
   hence thesis;
 end;

theorem Th56:
   p1,p2 split P & q in P & q <> p2 implies q,p2 split P
 proof assume that
A1:  p1,p2 split P and
A2:  q in P & q <> p2;
    p2,p1 split P by A1,Th54;
  then p2,q split P by A2,Th55;
  hence thesis by Th54;
 end;

theorem Th57:
   p1,p2 split P & q1 in P & q2 in P & q1 <> q2 implies q1,q2 split P
 proof assume that
A1:  p1,p2 split P and
A2:  q1 in P and
A3:  q2 in P and
A4:  q1 <> q2;
A5:  p2,p1 split P by A1,Th54;
  per cases;
   suppose p1 = q1;
    hence thesis by A1,A3,A4,Th55;
   suppose p1 = q2;
    hence thesis by A2,A4,A5,Th56;
   suppose p1 <> q1;
    then p1,q1 split P by A1,A2,Th55;
    then q2,q1 split P by A3,A4,Th56;
    hence thesis by Th54;
   suppose p2 <> q1;
    then q1,p2 split P by A1,A2,Th56;
    hence thesis by A3,A4,Th55;
 end;

definition let P be Subset of TOP-REAL 2;
 redefine attr P is being_special_polygon means
:Def2: ex p1,p2 st p1,p2 split P;
  compatibility
 proof
  thus P is being_special_polygon
    implies ex p1,p2 st p1,p2 split P
  proof given p1,p2 being Point of TOP-REAL 2,
              P1,P2 being Subset of TOP-REAL 2 such that
A1:  p1 <> p2 and p1 in P & p2 in P and
A2:  P1 is_S-P_arc_joining p1,p2 and
A3:  P2 is_S-P_arc_joining p1,p2 and
A4:  P1 /\ P2 = {p1,p2} & P = P1 \/ P2;
   take p1,p2;
   thus p1 <> p2 by A1;
   consider f1 such that
A5:  f1 is_S-Seq and
A6:  P1 = L~f1 & p1=f1/.1 & p2=f1/.len f1 by A2,TOPREAL4:def 1;
   consider f2 such that
A7:  f2 is_S-Seq and
A8:  P2 = L~f2 & p1=f2/.1 & p2=f2/.len f2 by A3,TOPREAL4:def 1;
   reconsider f1,f2 as S-Sequence_in_R2 by A5,A7;
   take f1,f2;
   thus p1 = f1/.1 & p1 = f2/.1 & p2 = f1/.len f1 & p2 = f2/.len f2 &
    L~f1 /\ L~f2 = {p1,p2} & P = L~f1 \/ L~f2 by A4,A6,A8;
  end;
  given p1,p2 such that
A9: p1,p2 split P;
  consider f1,f2 being S-Sequence_in_R2 such that
A10: p1 = f1/.1 & p1 = f2/.1 & p2 = f1/.len f1 & p2 = f2/.len f2 and
A11: L~f1 /\ L~f2 = {p1,p2} & P = L~f1 \/ L~f2 by A9,Def1;
  take p1,p2, P1=L~f1, P2=L~f2;
  thus p1 <> p2 by A9,Def1;
A12: {p1,p2} c= P by A11,XBOOLE_1:29;
    p1 in {p1,p2} & p2 in {p1,p2} by TARSKI:def 2;
  hence p1 in P & p2 in P by A12;
  thus ex f st f is_S-Seq & P1 = L~f & p1=f/.1 & p2=f/.len f by A10;
  thus ex f st f is_S-Seq & P2 = L~f & p1=f/.1 & p2=f/.len f by A10;
  thus thesis by A11;
 end;
  synonym P is special_polygonal;
end;

Lm18:
 for P being Subset of TOP-REAL 2 holds
 P is_special_polygon implies ex p1,p2 st p1 <> p2 & p1 in P & p2 in P
 proof let P be Subset of TOP-REAL 2;
  assume P is_special_polygon;
  then ex p1,p2 being Point of TOP-REAL 2,
    P1,P2 being Subset of TOP-REAL 2
     st p1 <> p2 & p1 in P & p2 in P &
   P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 &
    P1 /\ P2 = {p1,p2} & P = P1 \/ P2 by TOPREAL4:def 2;
  hence thesis;
 end;

definition let r1,r2,r1',r2';
 func [.r1,r2,r1',r2'.] -> Subset of TOP-REAL 2 equals
:Def3:
    { p: p`1 = r1 & p`2 <= r2' & p`2 >= r1' or
             p`1 <= r2 & p`1 >= r1 & p`2 = r2' or
             p`1 <= r2 & p`1 >= r1 & p`2 = r1' or
             p`1 = r2 & p`2 <= r2' & p`2 >= r1'};
  coherence
 proof
   defpred X[Element of TOP-REAL 2] means
        $1`1 = r1 & $1`2 <= r2' & $1`2 >= r1' or
        $1`1 <= r2 & $1`1 >= r1 & $1`2 = r2' or
        $1`1 <= r2 & $1`1 >= r1 & $1`2 = r1' or
        $1`1 = r2 & $1`2 <= r2' & $1`2 >= r1';
 deffunc U(Element of TOP-REAL 2) = $1;
   set P = { U(p): X[p] };
      P is Subset of TOP-REAL 2 from SubsetFD;
   hence thesis;
 end;
end;

theorem Th58:
   r1<r2 & r1'<r2' implies
     [.r1,r2,r1',r2'.] =
       ( LSeg(|[r1,r1']|,|[r1,r2']|) \/ LSeg(|[r1,r2']|,|[r2,r2']|) ) \/
       ( LSeg(|[r2,r2']|,|[r2,r1']|) \/ LSeg(|[r2,r1']|,|[r1,r1']|) )
 proof assume that
A1: r1<r2 and
A2: r1'<r2';
  set P = { p: p`1 = r1 & p`2 <= r2' & p`2 >= r1' or
               p`1 <= r2 & p`1 >= r1 & p`2 = r2' or
               p`1 <= r2 & p`1 >= r1 & p`2 = r1' or
               p`1 = r2 & p`2 <= r2' & p`2 >= r1'};
  set P1 = { p: p`1 = r1 & r1'<= p`2 & p`2 <= r2'};
  set P2 = { p: p`2 = r2'& r1 <= p`1 & p`1 <= r2 };
  set P3 = { p: p`1 = r2 & r1'<= p`2 & p`2 <= r2'};
  set P4 = { p: p`2 = r1'& r1 <= p`1 & p`1 <= r2 };
  set p1 = |[r1,r1']|, p2 = |[r1,r2']| , p3 = |[r2,r2']|, p4 = |[r2,r1']|;
    P = P1 \/ P2 \/ (P3 \/ P4)
   proof
    hereby let x be set;
     assume x in P;
     then consider p such that
A3:    x = p and
A4:    p`1 = r1 & p`2 <= r2' & p`2 >= r1' or
       p`1 <= r2 & p`1 >= r1 & p`2 = r2' or
       p`1 <= r2 & p`1 >= r1 & p`2 = r1' or
       p`1 = r2 & p`2 <= r2' & p`2 >= r1';
       x in P1 or x in P2 or x in P3 or x in P4 by A3,A4;
     then x in P1 \/ P2 or x in P3 \/ P4 by XBOOLE_0:def 2;
     hence x in P1 \/ P2 \/ (P3 \/ P4) by XBOOLE_0:def 2;
    end;
    let x be set;
    assume x in P1 \/ P2 \/ (P3 \/ P4);
    then A5: x in P1 \/ P2 or x in P3 \/ P4 by XBOOLE_0:def 2;
    per cases by A5,XBOOLE_0:def 2;
     suppose x in P1;
      then ex p st x = p & p`1 = r1 & r1'<= p`2 & p`2 <= r2';
      hence x in P;
     suppose x in P2;
      then ex p st x = p & p`2 = r2'& r1 <= p`1 & p`1 <= r2;
      hence x in P;
     suppose x in P3;
      then ex p st x = p & p`1 = r2 & r1'<= p`2 & p`2 <= r2';
      hence x in P;
     suppose x in P4;
      then ex p st x = p & p`2 = r1'& r1 <= p`1 & p`1 <= r2;
      hence x in P;
   end;
  hence [.r1,r2,r1',r2'.]
      = P1 \/ P2 \/ (P3 \/ P4) by Def3
     .= LSeg(p1,p2) \/ P2 \/ (P3 \/ P4) by A2,TOPREAL3:15
     .= LSeg(p1,p2) \/ LSeg(p2,p3) \/ (P3 \/ P4) by A1,TOPREAL3:16
     .= LSeg(p1,p2) \/ LSeg(p2,p3) \/ (LSeg(p3,p4) \/ P4) by A2,TOPREAL3:15
     .= LSeg(p1,p2) \/ LSeg(p2,p3) \/ (LSeg(p3,p4) \/ LSeg(p4,p1)) by A1,
TOPREAL3:16;
 end;

theorem Th59:
   r1<r2 & r1'<r2' implies [.r1,r2,r1',r2'.] is special_polygonal
 proof assume that
A1: r1<r2 and
A2: r1'<r2';
  set p1 = |[r1,r1']|, p2 = |[r1,r2']| , p3 = |[r2,r2']|, p4 = |[r2,r1']|;
  take p1,p3;
  thus p1 <> p3 by A1,Th1;
A3: p1`1 = r1 & p1`2 = r1' & p2`1 = r1 & p2`2 = r2' &
    p3`1 = r2 & p3`2 = r2' & p4`1 = r2 & p4`2 = r1' by EUCLID:56;
  set f1 = <* p1,p2,p3 *>, f2 = <* p1,p4,p3 *>;
  A4: len f1 = 3 & len f2 = 3 by FINSEQ_1:62;
  reconsider f1,f2 as S-Sequence_in_R2 by A1,A2,A3,TOPREAL3:41,42;
  take f1,f2;
  thus p1 = f1/.1 & p1 = f2/.1 & p3 = f1/.len f1 & p3 = f2/.len f2
   by A4,FINSEQ_4:27;
A5:  L~f1 = LSeg(p1,p2) \/ LSeg(p2,p3) by TOPREAL3:23;
A6:  L~f2 = LSeg(p3,p4) \/ LSeg(p4,p1) by TOPREAL3:23;
  hence L~f1 /\ L~f2
     = ((LSeg(p1,p2) \/ LSeg(p2,p3)) /\ LSeg(p3,p4)) \/
        ((LSeg(p1,p2) \/ LSeg(p2,p3)) /\ LSeg(p4,p1)) by A5,XBOOLE_1:23
    .= ((LSeg(p2,p1) \/ LSeg(p3,p2)) /\ LSeg(p4,p3)) \/
 {p1} by A2,A3,TOPREAL3:34
    .= {p3} \/ {p1} by A1,A3,TOPREAL3:35
    .= {p1,p3} by ENUMSET1:41;
  thus L~f1 \/ L~f2 = [.r1,r2,r1',r2'.] by A1,A2,A5,A6,Th58;
 end;

theorem Th60:
   R^2-unit_square = [.0,1,0,1.] by Def3,TOPREAL1:def 3;

definition
 cluster special_polygonal Subset of TOP-REAL 2;
 existence
  proof
   take A = [.0,1,0,1.];
   thus A is special_polygonal by Th59;
  end;
end;

theorem Th61:
  R^2-unit_square is special_polygonal by Th59,Th60;

definition
 cluster special_polygonal Subset of TOP-REAL 2;
  existence by Th61;
 cluster special_polygonal -> non empty Subset of TOP-REAL 2;
  coherence
 proof let P be Subset of TOP-REAL 2;
  assume P is special_polygonal;
  then ex p1,p2 st p1 <> p2 & p1 in P & p2 in P by Lm18;
  hence P is non empty;
 end;
 cluster special_polygonal ->
    non trivial Subset of TOP-REAL 2;
  coherence
 proof let P be Subset of TOP-REAL 2;
  assume P is special_polygonal;
  then ex p1,p2 st p1 <> p2 & p1 in P & p2 in P by Lm18;
  hence P is non trivial by SPPOL_1:4;
 end;
end;

definition
 mode Special_polygon_in_R2 is special_polygonal Subset of TOP-REAL 2;
end;

theorem Th62:
   P is being_S-P_arc implies P is compact
 proof assume P is being_S-P_arc;
  then reconsider P as being_S-P_arc Subset of TOP-REAL 2;
  consider f being map of I[01], (TOP-REAL 2)|P such that
A1:  f is_homeomorphism by TOPREAL1:36;
A2:  f is continuous by A1,TOPS_2:def 5;
A3:  I[01] is compact by HEINE:11,TOPMETR:27;
    rng f = [#]((TOP-REAL 2)|P) by A1,TOPS_2:def 5;
  then (TOP-REAL 2)|P is compact by A2,A3,COMPTS_1:23;
  hence thesis by COMPTS_1:12;
 end;

theorem
     for G being Special_polygon_in_R2 holds G is compact
 proof let G be Special_polygon_in_R2;
  consider p,q being Point of TOP-REAL 2,
     P1,P2 being Subset of TOP-REAL 2 such that
         p<>q & p in G & q in G and
A1: P1 is_S-P_arc_joining p,q & P2 is_S-P_arc_joining p,q and
    P1 /\ P2 = {p,q} and
A2: G = P1 \/ P2 by TOPREAL4:def 2;
  reconsider P1,P2 as Subset of TOP-REAL 2;
    P1 is_S-P_arc & P2 is_S-P_arc by A1,TOPREAL4:2;
  then P1 is compact & P2 is compact by Th62;
  hence thesis by A2,COMPTS_1:19;
 end;

theorem Th64:
  P is special_polygonal implies
   for p1,p2 st p1 <> p2 & p1 in P & p2 in P holds p1,p2 split P
 proof assume P is special_polygonal;
  then ex q1,q2 st q1,q2 split P by Def2;
  hence thesis by Th57;
 end;

theorem
    P is special_polygonal implies
   for p1,p2 st p1 <> p2 & p1 in P & p2 in P
    ex P1,P2 being Subset of TOP-REAL 2
     st P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 &
     P1 /\ P2 = {p1,p2} & P = P1 \/ P2
 proof
  assume
A1:  P is special_polygonal;
  let p1,p2;
  assume p1 <> p2 & p1 in P & p2 in P;
  then p1,p2 split P by A1,Th64;
  then consider f1,f2 being S-Sequence_in_R2 such that
A2:  p1 = f1/.1 and
A3:  p1 = f2/.1 and
A4:  p2 = f1/.len f1 and
A5:  p2 = f2/.len f2 and
A6:  L~f1 /\ L~f2 = {p1,p2} & P = L~f1 \/ L~f2 by Def1;
  take P1 = L~f1, P2 = L~f2;
  thus P1 is_S-P_arc_joining p1,p2 by A2,A4,TOPREAL4:def 1;
  thus P2 is_S-P_arc_joining p1,p2 by A3,A5,TOPREAL4:def 1;
  thus P1 /\ P2 = {p1,p2} & P = P1 \/ P2 by A6;
 end;




Back to top