The Mizar article:

On the Order on a Special Polygon

by
Andrzej Trybulec, and
Yatsuka Nakamura

Received November 30, 1997

Copyright (c) 1997 Association of Mizar Users

MML identifier: SPRECT_2
[ MML identifier index ]


environ

 vocabulary BOOLE, TARSKI, FINSEQ_1, RELAT_1, JORDAN3, ARYTM_1, FINSEQ_4,
      FUNCT_1, COMPTS_1, EUCLID, PRE_TOPC, MCART_1, PSCOMP_1, TOPREAL1,
      GOBOARD1, REALSET1, GOBOARD4, FINSEQ_6, SEQM_3, GOBOARD5, FUNCT_5,
      SUBSET_1, ORDINAL2, SPPOL_1, SPRECT_1, SPPOL_2, FINSEQ_5, TOPREAL2,
      SPRECT_2, ARYTM;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1,
      FUNCT_1, FUNCT_2, FINSEQ_1, STRUCT_0, FINSEQ_4, FINSEQ_5, REALSET1,
      FINSEQ_6, NAT_1, BINARITH, PRE_TOPC, COMPTS_1, EUCLID, TOPREAL1,
      TOPREAL2, GOBOARD1, GOBOARD4, SPPOL_1, SPPOL_2, GOBOARD5, JORDAN3,
      PSCOMP_1, SPRECT_1;
 constructors PSCOMP_1, GOBOARD5, JORDAN3, GOBOARD4, BINARITH, REALSET1,
      SPPOL_1, FINSEQ_5, REAL_1, SEQM_3, TOPREAL4, SPRECT_1, TOPREAL2,
      COMPTS_1, FINSEQ_4, GOBOARD1;
 clusters STRUCT_0, EUCLID, RELSET_1, GOBOARD5, SPPOL_2, GOBOARD2, GOBOARD4,
      PSCOMP_1, SPRECT_1, XREAL_0, FINSEQ_1, ARYTM_3, MEMBERED;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, GOBOARD4, TOPREAL1, XBOOLE_0;
 theorems FINSEQ_6, FINSEQ_4, FINSEQ_5, REAL_1, GOBOARD4, GOBOARD1, PSCOMP_1,
      FINSEQ_3, JORDAN3, AXIOMS, REAL_2, NAT_1, SPPOL_1, CQC_THE1, TOPREAL4,
      FINSEQ_1, GROUP_5, JORDAN4, ZFMISC_1, SPPOL_2, TOPREAL3, TARSKI, FUNCT_1,
      TOPREAL1, GOBOARD2, AMI_5, BINARITH, GOBOARD7, PARTFUN2, GOBOARD5,
      EUCLID, TOPREAL2, FUNCT_2, PRE_TOPC, RELAT_1, SPRECT_1, TOPREAL5,
      SCMFSA_7, XBOOLE_0, XBOOLE_1, SQUARE_1, XCMPLX_1;

begin :: Preliminaries

theorem Th1:
 for A,B,C,p being set st A /\ B c= {p} & p in C & C misses B
  holds A \/ C misses B
proof let A,B,C,p be set such that
A1: A /\ B c= {p} and
A2: p in C and
A3: C misses B;
    {p} c= C by A2,ZFMISC_1:37;
  then A /\ B c= C by A1,XBOOLE_1:1;
  then A /\ B /\ B c= C /\ B by XBOOLE_1:27;
  then A4: A /\ (B /\ B) c= C /\ B by XBOOLE_1:16;
     (A \/ C) /\ B = A /\ B \/ C /\ B by XBOOLE_1:23
           .= C /\ B by A4,XBOOLE_1:12
           .= {} by A3,XBOOLE_0:def 7;
 hence A \/ C misses B by XBOOLE_0:def 7;
end;

theorem Th2:
 for A,B,C,p being set st A /\ C = {p} & p in B & B c= C
  holds A /\ B = {p}
proof let A,B,C,p be set such that
A1: A /\ C = {p} and
A2: p in B and
A3: B c= C;
A4: {p} c= B by A2,ZFMISC_1:37;
 thus A /\ B = A /\ (C /\ B) by A3,XBOOLE_1:28
      .= {p} /\ B by A1,XBOOLE_1:16
      .= {p} by A4,XBOOLE_1:28;
end;

canceled;

theorem Th4:
 for A,B being set
  st for x,y being set st x in A & y in B holds x misses y
 holds union A misses union B
proof let A,B be set such that
A1: for x,y being set st x in A & y in B holds x misses y;
     for y being set st y in B holds union A misses y
    proof let y be set;
     assume y in B;
      then for x being set st x in A holds x misses y by A1;
     hence union A misses y by ZFMISC_1:98;
    end;
 hence union A misses union B by ZFMISC_1:98;
end;

begin :: Finite sequences

reserve i,j,k,l,m,n for Nat,
        D for non empty set,
        f for FinSequence of D;

theorem Th5:
 i <= j & i in dom f & j in dom f & k in dom mid(f,i,j) implies k+i-'1 in dom f
proof
  assume that
A1: i <= j and
A2: i in dom f and
A3: j in dom f;
A4: 1+0 <= i & i <= len f by A2,FINSEQ_3:27;
A5: 1 <= j & j <= len f by A3,FINSEQ_3:27;
then A6: len mid(f,i,j) = j -' i +1 by A1,A4,JORDAN3:27;
     k+i >= i by NAT_1:29;
then A7: k+i >= 1 by A4,AXIOMS:22;
 assume
A8: k in dom mid(f,i,j);
  then k <= len mid(f,i,j) by FINSEQ_3:27;
  then k <= j - i +1 by A1,A6,SCMFSA_7:3;
  then k <= j +1 - i by XCMPLX_1:29;
  then k+i <= j +1 by REAL_1:84;
  then k+i - 1 <= j by REAL_1:86;
  then k+i -' 1 <= j by A7,SCMFSA_7:3;
  then A9:  k+i-'1 <= len f by A5,AXIOMS:22;
A10:  1 <= k by A8,FINSEQ_3:27;
    i-1 >= 0 by A4,REAL_1:84;
  then k+0 <= k+(i-1) by AXIOMS:24;
  then 1 <= k+(i-1) by A10,AXIOMS:22;
  then 1 <= k+i-1 by XCMPLX_1:29;
  then 1 <= k+i-'1 by JORDAN3:1;
 hence k+i-'1 in dom f by A9,FINSEQ_3:27;
end;

theorem Th6:
 i > j & i in dom f & j in dom f & k in dom mid(f,i,j) implies i -' k + 1 in
 dom f
proof
 assume that
A1: i > j and
A2: i in dom f and
A3: j in dom f;
A4: 1+0 <= i & i <= len f by A2,FINSEQ_3:27;
A5: 1+0 <= j & j <= len f by A3,FINSEQ_3:27;
then A6: len mid(f,i,j) = i -' j +1 by A1,A4,JORDAN3:27;
    1 - j <= 0 by A5,REAL_2:106;
then A7:  i +(1 - j) <= i + 0 by AXIOMS:24;
 assume
A8: k in dom mid(f,i,j);
  then k <= len mid(f,i,j) by FINSEQ_3:27;
  then k <= i - j +1 by A1,A6,SCMFSA_7:3;
  then k <= i +1 - j by XCMPLX_1:29;
  then k <= i +(1 - j) by XCMPLX_1:29;
  then A9: k <= i by A7,AXIOMS:22;

    k >= 1 by A8,FINSEQ_3:27;
  then 1 - k <= 0 by REAL_2:106;
  then i + (1 - k) <= i+0 by AXIOMS:24;
  then i + 1 - k <= i by XCMPLX_1:29;
  then i - k + 1 <= i by XCMPLX_1:29;
  then i -' k + 1 <= i by A9,SCMFSA_7:3;
  then A10:  i -' k + 1 <= len f by A4,AXIOMS:22;
    1 <= i -' k + 1 by NAT_1:29;
 hence i -' k + 1 in dom f by A10,FINSEQ_3:27;
end;

theorem Th7:
 i <= j & i in dom f & j in dom f & k in dom mid(f,i,j) implies
  (mid(f,i,j))/.k = f/.(k+i-'1)
proof
 assume that
A1: i <= j and
A2: i in dom f and
A3: j in dom f and
A4: k in dom mid(f,i,j);
A5: k+i-'1 in dom f by A1,A2,A3,A4,Th5;
A6: 1 <= i & i <= len f by A2,FINSEQ_3:27;
A7: 1 <= j & j <= len f by A3,FINSEQ_3:27;
A8: 1 <= k & k <= len mid(f,i,j) by A4,FINSEQ_3:27;
 thus (mid(f,i,j))/.k = mid(f,i,j).k by A4,FINSEQ_4:def 4
    .= f.(k+i-'1) by A1,A6,A7,A8,JORDAN3:27
    .= f/.(k+i-'1) by A5,FINSEQ_4:def 4;
end;

theorem Th8:
 i > j & i in dom f & j in dom f & k in dom mid(f,i,j) implies
  (mid(f,i,j))/.k = f/.(i-' k +1)
proof
 assume that
A1: i > j and
A2: i in dom f and
A3: j in dom f and
A4: k in dom mid(f,i,j);
A5: i -' k +1 in dom f by A1,A2,A3,A4,Th6;
A6: 1 <= i & i <= len f by A2,FINSEQ_3:27;
A7: 1 <= j & j <= len f by A3,FINSEQ_3:27;
A8: 1 <= k & k <= len mid(f,i,j) by A4,FINSEQ_3:27;
 thus (mid(f,i,j))/.k = mid(f,i,j).k by A4,FINSEQ_4:def 4
    .= f.(i -' k +1) by A1,A6,A7,A8,JORDAN3:27
    .= f/.(i-' k +1) by A5,FINSEQ_4:def 4;
end;

theorem Th9:
  i in dom f & j in dom f implies len mid(f,i,j) >= 1
proof
 assume i in dom f;
then A1: 1 <= i & i <= len f by FINSEQ_3:27;
 assume j in dom f;
then A2: 1 <= j & j <= len f by FINSEQ_3:27;
    i <= j or j < i;
  then len mid(f,i,j)=i-'j+1 or len mid(f,i,j)=j-'i+1
                                   by A1,A2,JORDAN3:27;
 hence thesis by NAT_1:29;
end;

theorem Th10:
  i in dom f & j in dom f & len mid(f,i,j) = 1 implies i = j
proof
 assume i in dom f;
then A1: 1 <= i & i <= len f by FINSEQ_3:27;
 assume j in dom f;
then A2: 1 <= j & j <= len f by FINSEQ_3:27;
 assume
A3: len mid(f,i,j) = 1;
  per cases;
  suppose
A4: i <= j;
  then 0 + 1 = j -' i + 1 by A1,A2,A3,JORDAN4:20;
  then 0 = j -' i by XCMPLX_1:2;
  then 0 = j - i by A4,SCMFSA_7:3;
 hence thesis by XCMPLX_1:15;
  suppose
A5: i >= j;
  then 0 + 1 = i -' j + 1 by A1,A2,A3,JORDAN4:21;
  then 0 = i -' j by XCMPLX_1:2;
  then 0 = i - j by A5,SCMFSA_7:3;
 hence thesis by XCMPLX_1:15;
end;

theorem Th11:
 i in dom f & j in dom f implies mid(f,i,j) is non empty
proof
 assume i in dom f & j in dom f;
  then len mid(f,i,j) >= 1 by Th9;
 hence mid(f,i,j) is non empty by FINSEQ_3:27,RELAT_1:60;
end;

theorem Th12:
 i in dom f & j in dom f implies (mid(f,i,j))/.1 = f/.i
proof
 assume
A1: i in dom f;
then A2: 1 <= i & i <= len f by FINSEQ_3:27;
 assume
 A3:j in dom f;
then A4: 1 <= j & j <= len f by FINSEQ_3:27;
    mid(f,i,j) is non empty by A1,A3,Th11;
  then 1 in dom mid(f,i,j) by FINSEQ_5:6;
 hence (mid(f,i,j))/.1 = mid(f,i,j).1 by FINSEQ_4:def 4
      .= f.i by A2,A4,JORDAN3:27
      .= f/.i by A1,FINSEQ_4:def 4;
end;

theorem Th13:
 i in dom f & j in dom f implies (mid(f,i,j))/.len mid(f,i,j) = f/.j
proof
 assume
A1: i in dom f;
then A2: 1 <= i & i <= len f by FINSEQ_3:27;
 assume
 A3:j in dom f;
then A4: 1 <= j & j <= len f by FINSEQ_3:27;
    mid(f,i,j) is non empty by A1,A3,Th11;
  then len mid(f,i,j) in dom mid(f,i,j) by FINSEQ_5:6;
 hence (mid(f,i,j))/.len mid(f,i,j)
     = mid(f,i,j).len mid(f,i,j) by FINSEQ_4:def 4
    .= f.j by A2,A4,JORDAN4:23
    .= f/.j by A3,FINSEQ_4:def 4;
end;

begin :: Compact sets on the plane

reserve X for compact Subset of TOP-REAL 2;

theorem Th14:
 for p being Point of TOP-REAL 2 st p in X & p`2 = N-bound X
   holds p in N-most X
proof let p be Point of TOP-REAL 2 such that
A1: p in X and
A2: p`2 = N-bound X;
A3:  N-most X = LSeg(NW-corner X, NE-corner X)/\X by PSCOMP_1:def 39;
A4:  (NW-corner X)`2 = N-bound X &(NE-corner X)`2 = N-bound X
            by PSCOMP_1:75,77;
A5: (NW-corner X)`1 = W-bound X &(NE-corner X)`1 = E-bound X
            by PSCOMP_1:74,76;
    W-bound X <= p`1 & p`1 <= E-bound X by A1,PSCOMP_1:71;
  then p in LSeg(NW-corner X, NE-corner X) by A2,A4,A5,GOBOARD7:9;
 hence p in N-most X by A1,A3,XBOOLE_0:def 3;
end;

theorem Th15:
 for p being Point of TOP-REAL 2 st p in X & p`2 = S-bound X
   holds p in S-most X
proof let p be Point of TOP-REAL 2 such that
A1: p in X and
A2: p`2 = S-bound X;
A3:  S-most X = LSeg(SW-corner X, SE-corner X)/\X by PSCOMP_1:def 41;
A4:  (SW-corner X)`2 = S-bound X &(SE-corner X)`2 = S-bound X
               by PSCOMP_1:73,79;
A5: (SW-corner X)`1 = W-bound X &(SE-corner X)`1 = E-bound X
                                by PSCOMP_1:72,78;
    W-bound X <= p`1 & p`1 <= E-bound X by A1,PSCOMP_1:71;
  then p in LSeg(SW-corner X, SE-corner X) by A2,A4,A5,GOBOARD7:9;
 hence p in S-most X by A1,A3,XBOOLE_0:def 3;
end;

theorem Th16:
 for p being Point of TOP-REAL 2 st p in X & p`1 = W-bound X
   holds p in W-most X
proof let p be Point of TOP-REAL 2 such that
A1: p in X and
A2: p`1 = W-bound X;
A3:  W-most X = LSeg(SW-corner X, NW-corner X)/\X by PSCOMP_1:def 38;
A4:  (SW-corner X)`1 = W-bound X &(NW-corner X)`1 = W-bound X
                                by PSCOMP_1:72,74;
A5: (SW-corner X)`2 = S-bound X &(NW-corner X)`2 = N-bound X
                                by PSCOMP_1:73,75;
    S-bound X <= p`2 & p`2 <= N-bound X by A1,PSCOMP_1:71;
  then p in LSeg(SW-corner X, NW-corner X) by A2,A4,A5,GOBOARD7:8;
 hence p in W-most X by A1,A3,XBOOLE_0:def 3;
end;

theorem Th17:
 for p being Point of TOP-REAL 2 st p in X & p`1 = E-bound X
   holds p in E-most X
proof let p be Point of TOP-REAL 2 such that
A1: p in X and
A2: p`1 = E-bound X;
A3:  E-most X = LSeg(SE-corner X, NE-corner X)/\X by PSCOMP_1:def 40;
A4:  (SE-corner X)`1 = E-bound X &(NE-corner X)`1 = E-bound X
                                by PSCOMP_1:76,78;
A5: (SE-corner X)`2 = S-bound X &(NE-corner X)`2 = N-bound X
                                by PSCOMP_1:77,79;
    S-bound X <= p`2 & p`2 <= N-bound X by A1,PSCOMP_1:71;
  then p in LSeg(SE-corner X, NE-corner X) by A2,A4,A5,GOBOARD7:8;
 hence p in E-most X by A1,A3,XBOOLE_0:def 3;
end;

begin :: Finite sequences on the plane

theorem Th18:
 for f being FinSequence of TOP-REAL 2 st 1 <= i & i <= j & j <= len f
  holds L~mid(f,i,j) = union{ LSeg(f,k): i <= k & k < j}
proof let f be FinSequence of TOP-REAL 2;
 assume that
A1: 1 <= i and
A2: i <= j and
A3: j <= len f;
 set A = { LSeg(mid(f,i,j),m) : 1 <= m & m+1 <= len mid(f,i,j) },
     B = { LSeg(f,l): i <= l & l < j};
 per cases by A2,REAL_1:def 5;
 suppose
A4: i = j;
  then A5: mid(f,i,j) = <*f/.i*> by A1,A3,JORDAN4:27;
    B = {}
   proof assume B <> {};
    then consider z being set such that
A6:   z in B by XBOOLE_0:def 1;
       ex l st z = LSeg(f,l) & i <= l & l < j by A6;
    hence contradiction by A4;
   end;
 hence thesis by A5,SPPOL_2:12,ZFMISC_1:2;
 suppose
A7: i < j;
   A = B
  proof
   hereby let x be set;
    assume x in A;
     then consider m such that
A8:   x = LSeg(mid(f,i,j),m) and
A9:   0+1 <= m and
A10:   m+1 <= len mid(f,i,j);
       m+i >= m by NAT_1:29;
     then A11:   m+i >= 1 by A9,AXIOMS:22;
       len mid(f,i,j) = j -' i + 1 by A1,A3,A7,JORDAN4:20;
     then A12:    m < j -' i + 1 by A10,NAT_1:38;
     then m <= j -' i by NAT_1:38;
     then m <= j - i by A7,SCMFSA_7:3;
     then m+i <= j by REAL_1:84;
     then m+i-'1+1 <= j by A11,AMI_5:4;
then A13:   m+i-'1 < j by NAT_1:38;
       m > 0 by A9,NAT_1:38;
     then i < m+i by REAL_1:69;
then A14:   i <= m+i-'1 by JORDAN3:12;
       x = LSeg(f,m+i-'1) by A1,A3,A7,A8,A9,A12,JORDAN4:31;
    hence x in B by A13,A14;
   end;
   let x be set;
   assume x in B;
    then consider l such that
A15:  x = LSeg(f,l) and
A16:  i <= l and
A17:  l < j;
    set m = l -' i + 1;
A18:  1 <= m by NAT_1:29;
A19:  len mid(f,i,j) = j -' i + 1 by A1,A3,A7,JORDAN4:20;
      j > i by A16,A17,AXIOMS:22;
then A20:  l -' i = l - i & j -' i = j - i by A16,SCMFSA_7:3;
      l - i < j - i by A17,REAL_1:54;
then A21:  m < j-'i+1 by A20,REAL_1:53;
then A22:  m+1 <= len mid(f,i,j) by A19,NAT_1:38;
      m+i-'1 = l -' i + i + 1 -' 1 by XCMPLX_1:1
       .= l + 1 -' 1 by A16,AMI_5:4
       .= l by BINARITH:39;
    then x = LSeg(mid(f,i,j),m) by A1,A3,A7,A15,A18,A21,JORDAN4:31;
   hence x in A by A18,A22;
  end;
 hence L~mid(f,i,j) = union B by TOPREAL1:def 6;
end;

theorem Th19:
 for f being FinSequence of TOP-REAL 2
  holds dom X_axis f = dom f
proof let f be FinSequence of TOP-REAL 2;
    len X_axis f = len f by GOBOARD1:def 3;
 hence dom X_axis f = dom f by FINSEQ_3:31;
end;

theorem Th20:
 for f being FinSequence of TOP-REAL 2
  holds dom Y_axis f = dom f
proof let f be FinSequence of TOP-REAL 2;
    len Y_axis f = len f by GOBOARD1:def 4;
 hence dom Y_axis f = dom f by FINSEQ_3:31;
end;

reserve p,q,r for Real;

theorem Th21:
 for a,b,c being Point of TOP-REAL 2
  st b in LSeg(a,c) & a`1 <= b`1 & c`1 <= b`1
 holds a = b or b = c or a`1 = b`1 & c`1 = b`1
proof let a,b,c be Point of TOP-REAL 2 such that
A1: b in LSeg(a,c) and
A2: a`1 <= b`1 & c`1 <= b`1;
    LSeg(a,c) = { (1-r)*a + r*c : 0 <= r & r <= 1 } by TOPREAL1:def 4;
  then consider r such that
A3: b = (1-r)*a + r*c and
       0 <= r & r <= 1 by A1;
 per cases by A2,REAL_1:def 5;
 suppose that
A4: a`1 = b`1 and
A5: c`1 < b`1;
    b`1 + 0 = ((1-r)*a)`1 + (r*c)`1 by A3,TOPREAL3:7
     .= ((1-r)*a)`1 + r*c`1 by TOPREAL3:9
     .= (1-r)*b`1 + r*c`1 by A4,TOPREAL3:9
     .= 1*b`1-r*b`1 + r*c`1 by XCMPLX_1:40
     .= b`1 + r*c`1-r*b`1 by XCMPLX_1:29
     .= b`1 + (r*c`1-r*b`1) by XCMPLX_1:29;
  then A6: 0 = r*c`1-r*b`1 by XCMPLX_1:2
        .= r*(c`1-b`1) by XCMPLX_1:40;
    c`1-b`1 < 0 by A5,REAL_2:105;
  then r = 0 by A6,XCMPLX_1:6;
  then b = 1*a + 0.REAL 2 by A3,EUCLID:33
        .= 1*a by EUCLID:31
        .= a by EUCLID:33;
 hence thesis;
 suppose that
A7: a`1 < b`1 and
A8: c`1 = b`1;
    b`1 = ((1-r)*a)`1 + (r*c)`1 by A3,TOPREAL3:7
     .= ((1-r)*a)`1 + r*c`1 by TOPREAL3:9
     .= (1-r)*a`1 + r*b`1 by A8,TOPREAL3:9;
  then A9:  0 = (1-r)*a`1 + r*b`1 - b`1 by XCMPLX_1:14
        .= (1-r)*a`1 - b`1 + r*b`1 by XCMPLX_1:29
        .= (1-r)*a`1 - (1*b`1 - r*b`1) by XCMPLX_1:37
        .= (1-r)*a`1-(1-r)*b`1 by XCMPLX_1:40
        .= (1-r)*(a`1-b`1) by XCMPLX_1:40;
    a`1-b`1 < 0 by A7,REAL_2:105;
  then 1 - r = 0 by A9,XCMPLX_1:6;
  then b = 0 * a + 1*c by A3,XCMPLX_1:15
        .= 0.REAL 2 + 1*c by EUCLID:33
        .= 1*c by EUCLID:31
        .= c by EUCLID:33;
 hence thesis;
 suppose that
A10: a`1 < b`1 & c`1 < b`1;
     a`1 <= c`1 or c`1 <= a`1;
  hence thesis by A1,A10,TOPREAL1:9;
 suppose a`1 = b`1 & c`1 = b`1;
 hence thesis;
end;

theorem Th22:
 for a,b,c being Point of TOP-REAL 2
  st b in LSeg(a,c) & a`2 <= b`2 & c`2 <= b`2
 holds a = b or b = c or a`2 = b`2 & c`2 = b`2
proof let a,b,c be Point of TOP-REAL 2 such that
A1: b in LSeg(a,c) and
A2: a`2 <= b`2 & c`2 <= b`2;
     LSeg(a,c) = { (1-r)*a + r*c : 0 <= r & r <= 1 } by TOPREAL1:def 4;
  then consider r such that
A3: b = (1-r)*a + r*c and 0 <= r & r <= 1 by A1;
 per cases by A2,REAL_1:def 5;
 suppose that
A4: a`2 = b`2 and
A5: c`2 < b`2;
    b`2 + 0 = ((1-r)*a)`2 + (r*c)`2 by A3,TOPREAL3:7
     .= ((1-r)*a)`2 + r*c`2 by TOPREAL3:9
     .= (1-r)*b`2 + r*c`2 by A4,TOPREAL3:9
     .= 1*b`2-r*b`2 + r*c`2 by XCMPLX_1:40
     .= b`2 + r*c`2-r*b`2 by XCMPLX_1:29
     .= b`2 + (r*c`2-r*b`2) by XCMPLX_1:29;
  then A6: 0 = r*c`2-r*b`2 by XCMPLX_1:2
        .= r*(c`2-b`2) by XCMPLX_1:40;
    c`2-b`2 < 0 by A5,REAL_2:105;
  then r = 0 by A6,XCMPLX_1:6;
  then b = 1*a + 0.REAL 2 by A3,EUCLID:33
        .= 1*a by EUCLID:31
        .= a by EUCLID:33;
 hence thesis;
 suppose that
A7: a`2 < b`2 and
A8: c`2 = b`2;
    b`2 = ((1-r)*a)`2 + (r*c)`2 by A3,TOPREAL3:7
     .= ((1-r)*a)`2 + r*c`2 by TOPREAL3:9
     .= (1-r)*a`2 + r*b`2 by A8,TOPREAL3:9;
  then A9:  0 = (1-r)*a`2 + r*b`2 - b`2 by XCMPLX_1:14
        .= (1-r)*a`2 - b`2 + r*b`2 by XCMPLX_1:29
        .= (1-r)*a`2 - (1*b`2 - r*b`2) by XCMPLX_1:37
        .= (1-r)*a`2-(1-r)*b`2 by XCMPLX_1:40
        .= (1-r)*(a`2-b`2) by XCMPLX_1:40;
    a`2-b`2 < 0 by A7,REAL_2:105;
  then 1 - r = 0 by A9,XCMPLX_1:6;
  then b = 0 * a + 1*c by A3,XCMPLX_1:15
        .= 0.REAL 2 + 1*c by EUCLID:33
        .= 1*c by EUCLID:31
        .= c by EUCLID:33;
 hence thesis;
 suppose that
A10: a`2 < b`2 & c`2 < b`2;
     a`2 <= c`2 or c`2 <= a`2;
  hence thesis by A1,A10,TOPREAL1:10;
 suppose a`2 = b`2 & c`2 = b`2;
 hence thesis;
end;

theorem Th23:
 for a,b,c being Point of TOP-REAL 2
  st b in LSeg(a,c) & a`1 >= b`1 & c`1 >= b`1
 holds a = b or b = c or a`1 = b`1 & c`1 = b`1
proof let a,b,c be Point of TOP-REAL 2 such that
A1: b in LSeg(a,c) and
A2: a`1 >= b`1 & c`1 >= b`1;
     LSeg(a,c) = { (1-r)*a + r*c : 0 <= r & r <= 1 } by TOPREAL1:def 4;
  then consider r such that
A3: b = (1-r)*a + r*c and 0 <= r & r <= 1 by A1;
 per cases by A2,REAL_1:def 5;
 suppose that
A4: a`1 = b`1 and
A5: c`1 > b`1;
    b`1 + 0 = ((1-r)*a)`1 + (r*c)`1 by A3,TOPREAL3:7
     .= ((1-r)*a)`1 + r*c`1 by TOPREAL3:9
     .= (1-r)*b`1 + r*c`1 by A4,TOPREAL3:9
     .= 1*b`1-r*b`1 + r*c`1 by XCMPLX_1:40
     .= b`1 + r*c`1-r*b`1 by XCMPLX_1:29
     .= b`1 + (r*c`1-r*b`1) by XCMPLX_1:29;
  then A6: 0 = r*c`1-r*b`1 by XCMPLX_1:2
        .= r*(c`1-b`1) by XCMPLX_1:40;
    c`1-b`1 > 0 by A5,SQUARE_1:11;
  then r = 0 by A6,XCMPLX_1:6;
  then b = 1*a + 0.REAL 2 by A3,EUCLID:33
        .= 1*a by EUCLID:31
        .= a by EUCLID:33;
 hence thesis;
 suppose that
A7: a`1 > b`1 and
A8: c`1 = b`1;
    b`1 = ((1-r)*a)`1 + (r*c)`1 by A3,TOPREAL3:7
     .= ((1-r)*a)`1 + r*c`1 by TOPREAL3:9
     .= (1-r)*a`1 + r*b`1 by A8,TOPREAL3:9;
  then A9:  0 = (1-r)*a`1 + r*b`1 - b`1 by XCMPLX_1:14
        .= (1-r)*a`1 - b`1 + r*b`1 by XCMPLX_1:29
        .= (1-r)*a`1 - (1*b`1 - r*b`1) by XCMPLX_1:37
        .= (1-r)*a`1-(1-r)*b`1 by XCMPLX_1:40
        .= (1-r)*(a`1-b`1) by XCMPLX_1:40;
    a`1-b`1 > 0 by A7,SQUARE_1:11;
  then 1 - r = 0 by A9,XCMPLX_1:6;
  then b = 0 * a + 1*c by A3,XCMPLX_1:15
        .= 0.REAL 2 + 1*c by EUCLID:33
        .= 1*c by EUCLID:31
        .= c by EUCLID:33;
 hence thesis;
 suppose that
A10: a`1 > b`1 & c`1 > b`1;
     a`1 >= c`1 or c`1 >= a`1;
  hence thesis by A1,A10,TOPREAL1:9;
 suppose a`1 = b`1 & c`1 = b`1;
 hence thesis;
end;

theorem Th24:
 for a,b,c being Point of TOP-REAL 2
  st b in LSeg(a,c) & a`2 >= b`2 & c`2 >= b`2
 holds a = b or b = c or a`2 = b`2 & c`2 = b`2
proof let a,b,c be Point of TOP-REAL 2 such that
A1: b in LSeg(a,c) and
A2: a`2 >= b`2 & c`2 >= b`2;
     LSeg(a,c) = { (1-r)*a + r*c : 0 <= r & r <= 1 } by TOPREAL1:def 4;
  then consider r such that
A3: b = (1-r)*a + r*c and 0 <= r & r <= 1 by A1;
 per cases by A2,REAL_1:def 5;
 suppose that
A4: a`2 = b`2 and
A5: c`2 > b`2;
    b`2 + 0 = ((1-r)*a)`2 + (r*c)`2 by A3,TOPREAL3:7
     .= ((1-r)*a)`2 + r*c`2 by TOPREAL3:9
     .= (1-r)*b`2 + r*c`2 by A4,TOPREAL3:9
     .= 1*b`2-r*b`2 + r*c`2 by XCMPLX_1:40
     .= b`2 + r*c`2-r*b`2 by XCMPLX_1:29
     .= b`2 + (r*c`2-r*b`2) by XCMPLX_1:29;
  then A6: 0 = r*c`2-r*b`2 by XCMPLX_1:2
        .= r*(c`2-b`2) by XCMPLX_1:40;
    c`2-b`2 > 0 by A5,SQUARE_1:11;
  then r = 0 by A6,XCMPLX_1:6;
  then b = 1*a + 0.REAL 2 by A3,EUCLID:33
        .= 1*a by EUCLID:31
        .= a by EUCLID:33;
 hence thesis;
 suppose that
A7: a`2 > b`2 and
A8: c`2 = b`2;
    b`2 = ((1-r)*a)`2 + (r*c)`2 by A3,TOPREAL3:7
     .= ((1-r)*a)`2 + r*c`2 by TOPREAL3:9
     .= (1-r)*a`2 + r*b`2 by A8,TOPREAL3:9;
  then A9:  0 = (1-r)*a`2 + r*b`2 - b`2 by XCMPLX_1:14
        .= (1-r)*a`2 - b`2 + r*b`2 by XCMPLX_1:29
        .= (1-r)*a`2 - (1*b`2 - r*b`2) by XCMPLX_1:37
        .= (1-r)*a`2-(1-r)*b`2 by XCMPLX_1:40
        .= (1-r)*(a`2-b`2) by XCMPLX_1:40;
    a`2-b`2 > 0 by A7,SQUARE_1:11;
  then 1 - r = 0 by A9,XCMPLX_1:6;
  then b = 0 * a + 1*c by A3,XCMPLX_1:15
        .= 0.REAL 2 + 1*c by EUCLID:33
        .= 1*c by EUCLID:31
        .= c by EUCLID:33;
 hence thesis;
 suppose that
A10: a`2 > b`2 & c`2 > b`2;
     a`2 >= c`2 or c`2 >= a`2;
  hence thesis by A1,A10,TOPREAL1:10;
 suppose a`2 = b`2 & c`2 = b`2;
 hence thesis;
end;

begin :: The area of a sequence

definition
 let f, g be FinSequence of TOP-REAL 2;
 pred g is_in_the_area_of f means
:Def1: for n st n in dom g holds
   W-bound L~f <= (g/.n)`1 & (g/.n)`1 <= E-bound L~f &
   S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f;
end;

theorem Th25:
 for f being non trivial FinSequence of TOP-REAL 2
   holds f is_in_the_area_of f
proof let f be non trivial FinSequence of TOP-REAL 2;
 let n;
A1: len f >= 2 by SPPOL_1:2;
 assume n in dom f;
  then f/.n in L~f by A1,GOBOARD1:16;
 hence W-bound L~f <= (f/.n)`1 & (f/.n)`1 <= E-bound L~f &
   S-bound L~f <= (f/.n)`2 & (f/.n)`2 <= N-bound L~f by PSCOMP_1:71;
end;

theorem Th26:
 for f, g being FinSequence of TOP-REAL 2
   st g is_in_the_area_of f
 for i,j st i in dom g & j in dom g
   holds mid(g,i,j) is_in_the_area_of f
proof
 let f, g be FinSequence of TOP-REAL 2 such that
A1: for n st n in dom g holds
   W-bound L~f <= (g/.n)`1 & (g/.n)`1 <= E-bound L~f &
   S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f;
 let i,j such that
A2: i in dom g and
A3: j in dom g;
  set h = mid(g,i,j);
 per cases;
 suppose
A4: i <= j;
 let n;
 assume
A5: n in dom h;
then A6: n+i-'1 in dom g by A2,A3,A4,Th5;
    h/.n = g/.(n+i-'1) by A2,A3,A4,A5,Th7;
 hence W-bound L~f <= (h/.n)`1 & (h/.n)`1 <= E-bound L~f &
   S-bound L~f <= (h/.n)`2 & (h/.n)`2 <= N-bound L~f by A1,A6;
 suppose
A7: i > j;
 let n;
 assume
A8: n in dom h;
then A9: i -' n + 1 in dom g by A2,A3,A7,Th6;
    h/.n = g/.(i -' n + 1) by A2,A3,A7,A8,Th8;
 hence W-bound L~f <= (h/.n)`1 & (h/.n)`1 <= E-bound L~f &
   S-bound L~f <= (h/.n)`2 & (h/.n)`2 <= N-bound L~f by A1,A9;
end;

theorem Th27:
 for f being non trivial FinSequence of TOP-REAL 2
 for i,j st i in dom f & j in dom f
   holds mid(f,i,j) is_in_the_area_of f
proof let f be non trivial FinSequence of TOP-REAL 2, i,j;
    f is_in_the_area_of f by Th25;
 hence thesis by Th26;
end;

theorem Th28:
 for f,g,h being FinSequence of TOP-REAL 2
   st g is_in_the_area_of f & h is_in_the_area_of f
 holds g^h is_in_the_area_of f
proof
 let f,g,h be FinSequence of TOP-REAL 2 such that
A1: g is_in_the_area_of f and
A2: h is_in_the_area_of f;
 let n;
 assume
A3: n in dom(g^h);
 per cases by A3,FINSEQ_1:38;
 suppose
A4: n in dom g;
  then (g^h)/.n = g/.n by GROUP_5:95;
 hence W-bound L~f <= ((g^h)/.n)`1 & ((g^h)/.n)`1 <= E-bound L~f &
   S-bound L~f <= ((g^h)/.n)`2 & ((g^h)/.n)`2 <= N-bound L~f by A1,A4,Def1;
 suppose ex i st i in dom h & n = len g + i;
  then consider i such that
A5: i in dom h and
A6: n = len g + i;
    (g^h)/.n = h/.i by A5,A6,GROUP_5:96;
 hence W-bound L~f <= ((g^h)/.n)`1 & ((g^h)/.n)`1 <= E-bound L~f &
   S-bound L~f <= ((g^h)/.n)`2 & ((g^h)/.n)`2 <= N-bound L~f by A2,A5,Def1;
end;

theorem Th29:
 for f being non trivial FinSequence of TOP-REAL 2
  holds <*NE-corner L~f*> is_in_the_area_of f
proof let f be non trivial FinSequence of TOP-REAL 2;
  set g = <*NE-corner L~f*>;
 let n;
A1: dom g = {1} by FINSEQ_1:4,55;
 assume n in dom g;
  then n = 1 by A1,TARSKI:def 1;
  then g/.n = NE-corner L~f by FINSEQ_4:25
    .= |[E-bound L~f, N-bound L~f]| by PSCOMP_1:def 36;
  then (g/.n)`1 = E-bound L~f & (g/.n)`2 = N-bound L~f by EUCLID:56;
 hence
     W-bound L~f <= (g/.n)`1 & (g/.n)`1 <= E-bound L~f &
   S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f by SPRECT_1:23,24;
end;

theorem Th30:
 for f being non trivial FinSequence of TOP-REAL 2
  holds <*NW-corner L~f*> is_in_the_area_of f
proof let f be non trivial FinSequence of TOP-REAL 2;
  set g = <*NW-corner L~f*>;
 let n;
A1: dom g = {1} by FINSEQ_1:4,55;
 assume n in dom g;
  then n = 1 by A1,TARSKI:def 1;
  then g/.n = NW-corner L~f by FINSEQ_4:25
    .= |[W-bound L~f, N-bound L~f]| by PSCOMP_1:def 35;
  then (g/.n)`1 = W-bound L~f & (g/.n)`2 = N-bound L~f by EUCLID:56;
 hence
     W-bound L~f <= (g/.n)`1 & (g/.n)`1 <= E-bound L~f &
   S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f by SPRECT_1:23,24;
end;

theorem Th31:
 for f being non trivial FinSequence of TOP-REAL 2
  holds <*SE-corner L~f*> is_in_the_area_of f
proof let f be non trivial FinSequence of TOP-REAL 2;
  set g = <*SE-corner L~f*>;
 let n;
A1: dom g = {1} by FINSEQ_1:4,55;
 assume n in dom g;
  then n = 1 by A1,TARSKI:def 1;
  then g/.n = SE-corner L~f by FINSEQ_4:25
    .= |[E-bound L~f, S-bound L~f]| by PSCOMP_1:def 37;
  then (g/.n)`1 = E-bound L~f & (g/.n)`2 = S-bound L~f by EUCLID:56;
 hence
     W-bound L~f <= (g/.n)`1 & (g/.n)`1 <= E-bound L~f &
   S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f by SPRECT_1:23,24;
end;

theorem Th32:
 for f being non trivial FinSequence of TOP-REAL 2
  holds <*SW-corner L~f*> is_in_the_area_of f
proof let f be non trivial FinSequence of TOP-REAL 2;
  set g = <*SW-corner L~f*>;
 let n;
A1: dom g = {1} by FINSEQ_1:4,55;
 assume n in dom g;
  then n = 1 by A1,TARSKI:def 1;
  then g/.n = SW-corner L~f by FINSEQ_4:25
    .= |[W-bound L~f, S-bound L~f]| by PSCOMP_1:def 34;
  then (g/.n)`1 = W-bound L~f & (g/.n)`2 = S-bound L~f by EUCLID:56;
 hence W-bound L~f <= (g/.n)`1 & (g/.n)`1 <= E-bound L~f &
   S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f by SPRECT_1:23,24;
end;

begin :: Horizontal and vertical connections

definition
 let f, g be FinSequence of TOP-REAL 2;
 pred g is_a_h.c._for f means
:Def2: g is_in_the_area_of f &
   (g/.1)`1 = W-bound L~f & (g/.len g)`1 = E-bound L~f;
 pred g is_a_v.c._for f means
:Def3: g is_in_the_area_of f &
   (g/.1)`2 = S-bound L~f & (g/.len g)`2 = N-bound L~f;
end;

theorem Th33:
 for f being FinSequence of TOP-REAL 2,
     g,h being one-to-one special FinSequence of TOP-REAL 2
  st 2 <= len g & 2 <= len h & g is_a_h.c._for f & h is_a_v.c._for f
holds L~g meets L~h
proof let f be FinSequence of TOP-REAL 2,
       g,h being one-to-one special FinSequence of TOP-REAL 2 such that
A1: 2 <= len g & 2 <= len h and
A2: for n st n in dom g holds
   W-bound L~f <= (g/.n)`1 & (g/.n)`1 <= E-bound L~f &
   S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f and
A3: (g/.1)`1 = W-bound L~f and
A4: (g/.len g)`1 = E-bound L~f and
A5: for n st n in dom h holds
   W-bound L~f <= (h/.n)`1 & (h/.n)`1 <= E-bound L~f &
   S-bound L~f <= (h/.n)`2 & (h/.n)`2 <= N-bound L~f and
A6: (h/.1)`2 = S-bound L~f and
A7: (h/.len h)`2 = N-bound L~f;
    len g <> 0 & len h <> 0 by A1;
  then reconsider g,h as non empty one-to-one special FinSequence of TOP-REAL 2
    by FINSEQ_1:25;
A8: X_axis(g) lies_between (X_axis(g)).1, (X_axis(g)).(len g)
  proof
    set F = X_axis(g), r = (X_axis(g)).1, s = (X_axis(g)).(len g);
   let n;
   assume
A9: n in dom F;
then A10:  n in dom g by Th19;
A11:  F.n = (g/.n)`1 by A9,GOBOARD1:def 3;
      1 in dom F by FINSEQ_5:6;
    then r = W-bound L~f by A3,GOBOARD1:def 3;
   hence r <= F.n by A2,A10,A11;
A12:  len F = len g by GOBOARD1:def 3;
      len F in dom F by FINSEQ_5:6;
    then s = E-bound L~f by A4,A12,GOBOARD1:def 3;
   hence F.n <= s by A2,A10,A11;
  end;
A13: X_axis(h) lies_between (X_axis(g)).1, (X_axis(g)).(len g)
  proof
    set F = X_axis(g), r = (X_axis(g)).1, s = (X_axis(g)).(len g),
        H = X_axis h;
   let n;
   assume
A14: n in dom H;
then A15:  n in dom h by Th19;
A16:  H.n = (h/.n)`1 by A14,GOBOARD1:def 3;
      1 in dom F by FINSEQ_5:6;
    then r = W-bound L~f by A3,GOBOARD1:def 3;
   hence r <= H.n by A5,A15,A16;
A17:  len F = len g by GOBOARD1:def 3;
      len F in dom F by FINSEQ_5:6;
    then s = E-bound L~f by A4,A17,GOBOARD1:def 3;
   hence H.n <= s by A5,A15,A16;
  end;
A18: Y_axis(g) lies_between (Y_axis(h)).1, (Y_axis(h)).(len h)
  proof
    set F = Y_axis(h), r = (Y_axis(h)).1, s = (Y_axis(h)).(len h),
        G = Y_axis g;
   let n;
   assume
A19: n in dom G;
then A20:  n in dom g by Th20;
A21:  G.n = (g/.n)`2 by A19,GOBOARD1:def 4;
      1 in dom F by FINSEQ_5:6;
    then r = S-bound L~f by A6,GOBOARD1:def 4;
   hence r <= G.n by A2,A20,A21;
A22:  len F = len h by GOBOARD1:def 4;
      len F in dom F by FINSEQ_5:6;
    then s = N-bound L~f by A7,A22,GOBOARD1:def 4;
   hence G.n <= s by A2,A20,A21;
  end;
    Y_axis(h) lies_between (Y_axis(h)).1, (Y_axis(h)).(len h)
  proof
    set F = Y_axis h, r = (Y_axis h).1, s = (Y_axis h).(len h);
   let n;
   assume
A23: n in dom F;
then A24:  n in dom h by Th20;
A25:  F.n = (h/.n)`2 by A23,GOBOARD1:def 4;
      1 in dom F by FINSEQ_5:6;
    then r = S-bound L~f by A6,GOBOARD1:def 4;
   hence r <= F.n by A5,A24,A25;
A26:  len F = len h by GOBOARD1:def 4;
      len F in dom F by FINSEQ_5:6;
    then s = N-bound L~f by A7,A26,GOBOARD1:def 4;
   hence F.n <= s by A5,A24,A25;
  end;
 hence thesis by A1,A8,A13,A18,GOBOARD4:5;
end;

begin :: Orientation

definition let f be FinSequence of TOP-REAL 2;
 attr f is clockwise_oriented means
:Def4: (Rotate(f,N-min L~f))/.2 in N-most L~f;
end;

theorem Th34:
 for f being non constant standard special_circular_sequence
    st f/.1 = N-min L~f holds
  f is clockwise_oriented iff f/.2 in N-most L~f
proof let f be non constant standard special_circular_sequence;
 assume f/.1 = N-min L~f;
  then Rotate(f,N-min L~f) = f by FINSEQ_6:95;
 hence f is clockwise_oriented iff f/.2 in N-most L~f by Def4;
end;

definition
 cluster R^2-unit_square -> compact;
 coherence by TOPREAL2:2;
end;

theorem Th35:
 N-bound R^2-unit_square = 1
proof
  set X = R^2-unit_square;
  reconsider Z = (proj2||X).:the carrier of ((TOP-REAL 2)|X) as Subset of REAL;
A1: X = [#]((TOP-REAL 2)|X) by PRE_TOPC:def 10
      .= the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:12;
A2:for p be real number st p in Z holds p <= 1
    proof let p be real number;
     assume p in Z;
      then consider p0 being set such that
A3:    p0 in the carrier of (TOP-REAL 2)|X and
         p0 in the carrier of (TOP-REAL 2)|X and
A4:    p = (proj2||X).p0 by FUNCT_2:115;
      reconsider p0 as Point of TOP-REAL 2 by A1,A3;
          ex q being Point of TOP-REAL 2 st p0 = q &
         (q`1 = 0 & q`2 <= 1 & q`2 >= 0 or
          q`1 <= 1 & q`1 >= 0 & q`2 = 1 or
          q`1 <= 1 & q`1 >= 0 & q`2 = 0 or
          q`1 = 1 & q`2 <= 1 & q`2 >= 0) by A1,A3,TOPREAL1:def 3;
     hence p <= 1 by A1,A3,A4,PSCOMP_1:70;
    end;
A5: for q being real number st
    for p being real number st p in Z holds p <= q holds 1 <= q
   proof let q be real number such that
A6:    for p being real number st p in Z holds p <= q;
       |[1,1]| in LSeg(|[ 1,0 ]|, |[ 1,1 ]|) by TOPREAL1:6;
     then |[1,1]| in LSeg(|[ 0,0 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 1,1 ]|)
                 by XBOOLE_0:def 2;
then A7:   |[1,1]| in X by TOPREAL1:20,XBOOLE_0:def 2;
     then (proj2||X). |[1,1]| = |[1,1]|`2 by PSCOMP_1:70
             .= 1 by EUCLID:56;
     then 1 in Z by A1,A7,FUNCT_2:43;
    hence thesis by A6;
   end;
 thus N-bound X = sup (proj2||X) by PSCOMP_1:def 31
     .= sup Z by PSCOMP_1:def 21
     .= 1 by A2,A5,PSCOMP_1:11;
end;

theorem Th36:
 W-bound R^2-unit_square = 0
proof
  set X = R^2-unit_square;
  reconsider Z = (proj1||X).:the carrier of ((TOP-REAL 2)|X) as Subset of REAL;
A1: X = [#]((TOP-REAL 2)|X) by PRE_TOPC:def 10
      .= the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:12;
A2: for p be real number st p in Z holds p >= 0
    proof let p be real number;
     assume p in Z;
      then consider p0 being set such that
A3:    p0 in the carrier of (TOP-REAL 2)|X and
         p0 in the carrier of (TOP-REAL 2)|X and
A4:    p = (proj1||X).p0 by FUNCT_2:115;
      reconsider p0 as Point of TOP-REAL 2 by A1,A3;
          ex q being Point of TOP-REAL 2 st p0 = q &
         (q`1 = 0 & q`2 <= 1 & q`2 >= 0 or
          q`1 <= 1 & q`1 >= 0 & q`2 = 1 or
          q`1 <= 1 & q`1 >= 0 & q`2 = 0 or
          q`1 = 1 & q`2 <= 1 & q`2 >= 0) by A1,A3,TOPREAL1:def 3;
     hence p >= 0 by A1,A3,A4,PSCOMP_1:69;
    end;
A5: for q be real number st
   for p be real number st p in Z holds p >= q holds 0 >= q
   proof let q be real number such that
A6:    for p be real number st p in Z holds p >= q;
       |[0,0]| in LSeg(|[ 0,0 ]|, |[ 1,0 ]|) by TOPREAL1:6;
     then |[0,0]| in LSeg(|[ 0,0 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 1,1 ]|)
                 by XBOOLE_0:def 2;
then A7:   |[0,0]| in X by TOPREAL1:20,XBOOLE_0:def 2;
     then (proj1||X). |[0,0]| = |[0,0]|`1 by PSCOMP_1:69
             .= 0 by EUCLID:56;
     then 0 in Z by A1,A7,FUNCT_2:43;
    hence thesis by A6;
   end;
 thus W-bound X = inf (proj1||X) by PSCOMP_1:def 30
     .= inf Z by PSCOMP_1:def 20
     .= 0 by A2,A5,PSCOMP_1:9;
end;

theorem Th37:
 E-bound R^2-unit_square = 1
proof
  set X = R^2-unit_square;
  reconsider Z = (proj1||X).:the carrier of ((TOP-REAL 2)|X) as Subset of REAL;
A1: X = [#]((TOP-REAL 2)|X) by PRE_TOPC:def 10
      .= the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:12;
A2:for p be real number st p in Z holds p <= 1
    proof let p be real number;
     assume p in Z;
      then consider p0 being set such that
A3:    p0 in the carrier of (TOP-REAL 2)|X and
         p0 in the carrier of (TOP-REAL 2)|X and
A4:    p = (proj1||X).p0 by FUNCT_2:115;
      reconsider p0 as Point of TOP-REAL 2 by A1,A3;
          ex q being Point of TOP-REAL 2 st p0 = q &
         (q`1 = 0 & q`2 <= 1 & q`2 >= 0 or
          q`1 <= 1 & q`1 >= 0 & q`2 = 1 or
          q`1 <= 1 & q`1 >= 0 & q`2 = 0 or
          q`1 = 1 & q`2 <= 1 & q`2 >= 0) by A1,A3,TOPREAL1:def 3;
     hence p <= 1 by A1,A3,A4,PSCOMP_1:69;
    end;
A5: for q being real number st
    for p being real number st p in Z holds p <= q holds 1 <= q
   proof let q be real number such that
A6:    for p be real number st p in Z holds p <= q;
       |[1,1]| in LSeg(|[ 1,0 ]|, |[ 1,1 ]|) by TOPREAL1:6;
     then |[1,1]| in LSeg(|[ 0,0 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 1,1 ]|)
                 by XBOOLE_0:def 2;
then A7:   |[1,1]| in X by TOPREAL1:20,XBOOLE_0:def 2;
     then (proj1||X). |[1,1]| = |[1,1]|`1 by PSCOMP_1:69
             .= 1 by EUCLID:56;
     then 1 in Z by A1,A7,FUNCT_2:43;
    hence thesis by A6;
   end;
 thus E-bound X = sup (proj1||X) by PSCOMP_1:def 32
     .= sup Z by PSCOMP_1:def 21
     .= 1 by A2,A5,PSCOMP_1:11;
end;

theorem
   S-bound R^2-unit_square = 0
proof
  set X = R^2-unit_square;
  reconsider Z = (proj2||X).:the carrier of ((TOP-REAL 2)|X) as Subset of REAL;
A1: X = [#]((TOP-REAL 2)|X) by PRE_TOPC:def 10
      .= the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:12;
A2:for p be real number st p in Z holds p >= 0
    proof let p be real number;
     assume p in Z;
      then consider p0 being set such that
A3:    p0 in the carrier of (TOP-REAL 2)|X and
         p0 in the carrier of (TOP-REAL 2)|X and
A4:    p = (proj2||X).p0 by FUNCT_2:115;
      reconsider p0 as Point of TOP-REAL 2 by A1,A3;
         ex q being Point of TOP-REAL 2 st p0 = q &
         (q`1 = 0 & q`2 <= 1 & q`2 >= 0 or
          q`1 <= 1 & q`1 >= 0 & q`2 = 1 or
          q`1 <= 1 & q`1 >= 0 & q`2 = 0 or
          q`1 = 1 & q`2 <= 1 & q`2 >= 0) by A1,A3,TOPREAL1:def 3;
     hence p >= 0 by A1,A3,A4,PSCOMP_1:70;
    end;
A5: for q be real number st
   for p be real number st p in Z holds p >= q holds 0 >= q
   proof let q be real number such that
A6:    for p be real number st p in Z holds p >= q;
       |[1,0]| in LSeg(|[ 1,0 ]|, |[ 1,1 ]|) by TOPREAL1:6;
     then |[1,0]| in LSeg(|[ 0,0 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 1,1 ]|)
                 by XBOOLE_0:def 2;
then A7:   |[1,0]| in X by TOPREAL1:20,XBOOLE_0:def 2;
     then (proj2||X). |[1,0]| = |[1,0]|`2 by PSCOMP_1:70
             .= 0 by EUCLID:56;
     then 0 in Z by A1,A7,FUNCT_2:43;
    hence thesis by A6;
   end;
 thus S-bound X = inf (proj2||X) by PSCOMP_1:def 33
     .= inf Z by PSCOMP_1:def 20
     .= 0 by A2,A5,PSCOMP_1:9;
end;

Lm1: NW-corner R^2-unit_square = |[0,1]| by Th35,Th36,PSCOMP_1:def 35;
Lm2: NE-corner R^2-unit_square = |[1,1]| by Th35,Th37,PSCOMP_1:def 36;

theorem Th39:
 N-most R^2-unit_square = LSeg(|[0,1]|,|[1,1]|)
proof set X = R^2-unit_square;
A1: LSeg(|[ 0,0 ]|, |[ 0,1 ]|) \/ LSeg(|[ 0,1 ]|, |[ 1,1 ]|) c= X
                                  by TOPREAL1:20,XBOOLE_1:7;
     LSeg(|[0,1]|,|[1,1]|) c=
   LSeg(|[ 0,0 ]|, |[ 0,1 ]|) \/ LSeg(|[ 0,1 ]|, |[ 1,1 ]|) by XBOOLE_1:7;
then A2: LSeg(|[0,1]|,|[1,1]|) c= X by A1,XBOOLE_1:1;
 thus N-most X = LSeg(NW-corner X, NE-corner X)/\X by PSCOMP_1:def 39
       .= LSeg(|[0,1]|,|[1,1]|) by A2,Lm1,Lm2,XBOOLE_1:28;
end;

theorem
   N-min R^2-unit_square = |[0,1]|
proof
  inf (proj1||LSeg(|[0,1]|,|[1,1]|)) = 0
proof
  set X = LSeg(|[0,1]|,|[1,1]|);
  reconsider Z = (proj1||X).:the carrier of ((TOP-REAL 2)|X) as Subset of REAL;
A1: X = [#]((TOP-REAL 2)|X) by PRE_TOPC:def 10
      .= the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:12;
A2: for p be real number st p in Z holds p >= 0
    proof let p be real number;
     assume p in Z;
      then consider p0 being set such that
A3:    p0 in the carrier of (TOP-REAL 2)|X and
         p0 in the carrier of (TOP-REAL 2)|X and
A4:    p = (proj1||X).p0 by FUNCT_2:115;
      reconsider p0 as Point of TOP-REAL 2 by A1,A3;
        |[0,1]|`1 = 0 & |[1,1]|`1 = 1 by EUCLID:56;
      then p0`1 >= 0 by A1,A3,TOPREAL1:9;
     hence p >= 0 by A1,A3,A4,PSCOMP_1:69;
    end;
A5: for q be real number st
   for p be real number st p in Z holds p >= q holds 0 >= q
   proof let q be real number such that
A6:    for p be real number st p in Z holds p >= q;
A7:   |[0,1]| in X by TOPREAL1:6;
     then (proj1||X). |[0,1]| = |[0,1]|`1 by PSCOMP_1:69
             .= 0 by EUCLID:56;
     then 0 in Z by A1,A7,FUNCT_2:43;
    hence thesis by A6;
   end;
 thus inf (proj1||X) = inf Z by PSCOMP_1:def 20
     .= 0 by A2,A5,PSCOMP_1:9;
end;
 hence N-min R^2-unit_square
       = |[0,1]| by Th35,Th39,PSCOMP_1:def 44;
end;

definition
 let X be non vertical non horizontal non empty compact Subset of TOP-REAL 2;
 cluster SpStSeq X -> clockwise_oriented;
 coherence
  proof set f = SpStSeq X;
A1:  f/.1 = N-min L~f by SPRECT_1:91;
      f/.2 = N-max L~f by SPRECT_1:92;
    then f/.2 in N-most L~f by PSCOMP_1:101;
   hence thesis by A1,Th34;
  end;
end;

definition
 cluster clockwise_oriented (non constant standard special_circular_sequence);
 existence
  proof
   consider X being
     non vertical non horizontal non empty compact Subset of TOP-REAL 2;
   take SpStSeq X;
   thus thesis;
  end;
end;

theorem Th41:
 for f being non constant standard special_circular_sequence,
     i,j st i > j & (1 < j & i <= len f or 1 <= j & i < len f)
  holds mid(f,i,j) is S-Sequence_in_R2
proof let f be non constant standard special_circular_sequence, i,j such that
A1: i > j and
A2: 1 < j & i <= len f or 1 <= j & i < len f;
A3: Rev mid(f,j,i) = mid(f,i,j) by JORDAN4:30;
 per cases by A2;
 suppose 1 < j & i <= len f;
  then mid(f,j,i) is S-Sequence_in_R2 by A1,JORDAN4:52;
 hence mid(f,i,j) is S-Sequence_in_R2 by A3,SPPOL_2:47;
 suppose
A4: 1 <= j & i < len f;
  then i+1 <= len f by NAT_1:38;
  then mid(f,j,i) is S-Sequence_in_R2 by A1,A4,JORDAN4:51;
 hence mid(f,i,j) is S-Sequence_in_R2 by A3,SPPOL_2:47;
end;

theorem Th42:
 for f being non constant standard special_circular_sequence,
     i,j st i < j & (1 < i & j <= len f or 1 <= i & j < len f)
  holds mid(f,i,j) is S-Sequence_in_R2
proof
 let f be non constant standard special_circular_sequence,i,j such that
A1: i < j and
A2:1 < i & j <= len f or 1 <= i & j < len f;
A3: Rev Rev mid(f,i,j) = mid(f,i,j) by FINSEQ_6:29;
    mid(f,j,i) is S-Sequence_in_R2 by A1,A2,Th41;
  then Rev mid(f,i,j) is S-Sequence_in_R2 by JORDAN4:30;
 hence mid(f,i,j) is S-Sequence_in_R2 by A3,SPPOL_2:47;
end;

reserve f for non trivial FinSequence of TOP-REAL 2;

theorem Th43:
  N-min L~f in rng f
proof
  set p = N-min L~f;
  A1: len f >= 2 by SPPOL_1:2;
    p in L~f by SPRECT_1:13;
  then consider i be Nat such that
   A2: 1 <= i & i+1 <= len f and
   A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14;
    i <= i+1 by NAT_1:29;
  then i+1 >= 1 & i <= len f by A2,AXIOMS:22;
  then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27;
  then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16;
  then A6: (f/.i)`2 <= N-bound L~f & (f/.(i+1))`2 <= N-bound L~f
                                                            by PSCOMP_1:71;
  A7: p`2 = N-bound L~f by PSCOMP_1:94;
    now per cases by A3,A6,A7,Th22;
   suppose p = f/.i;
    hence thesis by A4,PARTFUN2:4;
   suppose p = f/.(i+1);
    hence thesis by A4,PARTFUN2:4;
   suppose A8: p`2 = (f/.i)`2 & p`2 = (f/.(i+1))`2;
    then f/.i in N-most L~f & f/.(i+1) in N-most L~f by A5,A7,Th14;
    then A9: (f/.i)`1 >= p`1 & (f/.(i+1))`1 >= p`1 by PSCOMP_1:98;
      (f/.i)`1 <= (f/.(i+1))`1 or (f/.(i+1))`1 <= (f/.i)`1;
    then (f/.i)`1 <= p`1 or (f/.(i+1))`1 <= p`1 by A3,TOPREAL1:9;
    then p`1 = (f/.i)`1 or p`1 = (f/.(i+1))`1 by A9,AXIOMS:21;
    then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11;
    hence thesis by A4,PARTFUN2:4;
  end;
  hence thesis;
end;

theorem Th44:
  N-max L~f in rng f
proof
  set p = N-max L~f;
  A1: len f >= 2 by SPPOL_1:2;
    p in L~f by SPRECT_1:13;
  then consider i be Nat such that
   A2: 1 <= i & i+1 <= len f and
   A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14;
    i <= i+1 by NAT_1:29;
  then i+1 >= 1 & i <= len f by A2,AXIOMS:22;
  then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27;
  then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16;
  then A6: (f/.i)`2 <= N-bound L~f & (f/.(i+1))`2 <= N-bound L~f
                                                            by PSCOMP_1:71;
  A7: p`2 = N-bound L~f by PSCOMP_1:94;
    now per cases by A3,A6,A7,Th22;
   suppose p = f/.i;
    hence thesis by A4,PARTFUN2:4;
   suppose p = f/.(i+1);
    hence thesis by A4,PARTFUN2:4;
   suppose A8: p`2 = (f/.i)`2 & p`2 = (f/.(i+1))`2;
    then f/.i in N-most L~f & f/.(i+1) in N-most L~f by A5,A7,Th14;
    then A9: (f/.i)`1 <= p`1 & (f/.(i+1))`1 <= p`1 by PSCOMP_1:98;
      (f/.i)`1 >= (f/.(i+1))`1 or (f/.(i+1))`1 >= (f/.i)`1;
    then (f/.i)`1 >= p`1 or (f/.(i+1))`1 >= p`1 by A3,TOPREAL1:9;
    then p`1 = (f/.i)`1 or p`1 = (f/.(i+1))`1 by A9,AXIOMS:21;
    then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11;
    hence thesis by A4,PARTFUN2:4;
  end;
  hence thesis;
end;

theorem Th45:
  S-min L~f in rng f
proof
  set p = S-min L~f;
  A1: len f >= 2 by SPPOL_1:2;
    p in L~f by SPRECT_1:14;
  then consider i be Nat such that
   A2: 1 <= i & i+1 <= len f and
   A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14;
    i <= i+1 by NAT_1:29;
  then i+1 >= 1 & i <= len f by A2,AXIOMS:22;
  then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27;
  then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16;
  then A6: (f/.i)`2 >= S-bound L~f & (f/.(i+1))`2 >= S-bound L~f
                                                            by PSCOMP_1:71;
  A7: p`2 = S-bound L~f by PSCOMP_1:114;
    now per cases by A3,A6,A7,Th24;
   suppose p = f/.i;
    hence thesis by A4,PARTFUN2:4;
   suppose p = f/.(i+1);
    hence thesis by A4,PARTFUN2:4;
   suppose A8: p`2 = (f/.i)`2 & p`2 = (f/.(i+1))`2;
    then f/.i in S-most L~f & f/.(i+1) in S-most L~f by A5,A7,Th15;
    then A9: (f/.i)`1 >= p`1 & (f/.(i+1))`1 >= p`1 by PSCOMP_1:118;
      (f/.i)`1 <= (f/.(i+1))`1 or (f/.(i+1))`1 <= (f/.i)`1;
    then (f/.i)`1 <= p`1 or (f/.(i+1))`1 <= p`1 by A3,TOPREAL1:9;
    then p`1 = (f/.i)`1 or p`1 = (f/.(i+1))`1 by A9,AXIOMS:21;
    then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11;
    hence thesis by A4,PARTFUN2:4;
  end;
  hence thesis;
end;

theorem Th46:
  S-max L~f in rng f
proof
  set p = S-max L~f;
  A1: len f >= 2 by SPPOL_1:2;
    p in L~f by SPRECT_1:14;
  then consider i be Nat such that
   A2: 1 <= i & i+1 <= len f and
   A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14;
    i <= i+1 by NAT_1:29;
  then i+1 >= 1 & i <= len f by A2,AXIOMS:22;
  then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27;
  then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16;
  then A6: (f/.i)`2 >= S-bound L~f & (f/.(i+1))`2 >= S-bound L~f
                                                            by PSCOMP_1:71;
  A7: p`2 = S-bound L~f by PSCOMP_1:114;
    now per cases by A3,A6,A7,Th24;
   suppose p = f/.i;
    hence thesis by A4,PARTFUN2:4;
   suppose p = f/.(i+1);
    hence thesis by A4,PARTFUN2:4;
   suppose A8: p`2 = (f/.i)`2 & p`2 = (f/.(i+1))`2;
    then f/.i in S-most L~f & f/.(i+1) in S-most L~f by A5,A7,Th15;
    then A9: (f/.i)`1 <= p`1 & (f/.(i+1))`1 <= p`1 by PSCOMP_1:118;
      (f/.i)`1 >= (f/.(i+1))`1 or (f/.(i+1))`1 >= (f/.i)`1;
    then (f/.i)`1 >= p`1 or (f/.(i+1))`1 >= p`1 by A3,TOPREAL1:9;
    then p`1 = (f/.i)`1 or p`1 = (f/.(i+1))`1 by A9,AXIOMS:21;
    then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11;
    hence thesis by A4,PARTFUN2:4;
  end;
  hence thesis;
end;

theorem Th47:
  W-min L~f in rng f
proof
  set p = W-min L~f;
  A1: len f >= 2 by SPPOL_1:2;
    p in L~f by SPRECT_1:15;
  then consider i be Nat such that
   A2: 1 <= i & i+1 <= len f and
   A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14;
    i <= i+1 by NAT_1:29;
  then i+1 >= 1 & i <= len f by A2,AXIOMS:22;
  then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27;
  then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16;
  then A6: (f/.i)`1 >= W-bound L~f & (f/.(i+1))`1 >= W-bound L~f
                                                            by PSCOMP_1:71;
  A7: p`1 = W-bound L~f by PSCOMP_1:84;
    now per cases by A3,A6,A7,Th23;
   suppose p = f/.i;
    hence thesis by A4,PARTFUN2:4;
   suppose p = f/.(i+1);
    hence thesis by A4,PARTFUN2:4;
   suppose A8: p`1 = (f/.i)`1 & p`1 = (f/.(i+1))`1;
    then f/.i in W-most L~f & f/.(i+1) in W-most L~f by A5,A7,Th16;
    then A9: (f/.i)`2 >= p`2 & (f/.(i+1))`2 >= p`2 by PSCOMP_1:88;
      (f/.i)`2 <= (f/.(i+1))`2 or (f/.(i+1))`2 <= (f/.i)`2;
    then (f/.i)`2 <= p`2 or (f/.(i+1))`2 <= p`2 by A3,TOPREAL1:10;
    then p`2 = (f/.i)`2 or p`2 = (f/.(i+1))`2 by A9,AXIOMS:21;
    then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11;
    hence thesis by A4,PARTFUN2:4;
  end;
  hence thesis;
end;

theorem Th48:
  W-max L~f in rng f
proof
  set p = W-max L~f;
  A1: len f >= 2 by SPPOL_1:2;
    p in L~f by SPRECT_1:15;
  then consider i be Nat such that
   A2: 1 <= i & i+1 <= len f and
   A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14;
    i <= i+1 by NAT_1:29;
  then i+1 >= 1 & i <= len f by A2,AXIOMS:22;
  then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27;
  then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16;
  then A6: (f/.i)`1 >= W-bound L~f & (f/.(i+1))`1 >= W-bound L~f
                                                            by PSCOMP_1:71;
  A7: p`1 = W-bound L~f by PSCOMP_1:84;
    now per cases by A3,A6,A7,Th23;
   suppose p = f/.i;
    hence thesis by A4,PARTFUN2:4;
   suppose p = f/.(i+1);
    hence thesis by A4,PARTFUN2:4;
   suppose A8: p`1 = (f/.i)`1 & p`1 = (f/.(i+1))`1;
    then f/.i in W-most L~f & f/.(i+1) in W-most L~f by A5,A7,Th16;
    then A9: (f/.i)`2 <= p`2 & (f/.(i+1))`2 <= p`2 by PSCOMP_1:88;
      (f/.i)`2 >= (f/.(i+1))`2 or (f/.(i+1))`2 >= (f/.i)`2;
    then (f/.i)`2 >= p`2 or (f/.(i+1))`2 >= p`2 by A3,TOPREAL1:10;
    then p`2 = (f/.i)`2 or p`2 = (f/.(i+1))`2 by A9,AXIOMS:21;
    then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11;
    hence thesis by A4,PARTFUN2:4;
  end;
  hence thesis;
end;

theorem Th49:
  E-min L~f in rng f
proof
  set p = E-min L~f;
  A1: len f >= 2 by SPPOL_1:2;
    p in L~f by SPRECT_1:16;
  then consider i be Nat such that
   A2: 1 <= i & i+1 <= len f and
   A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14;
    i <= i+1 by NAT_1:29;
  then i+1 >= 1 & i <= len f by A2,AXIOMS:22;
  then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27;
  then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16;
  then A6: (f/.i)`1 <= E-bound L~f & (f/.(i+1))`1 <= E-bound L~f
                                                            by PSCOMP_1:71;
  A7: p`1 = E-bound L~f by PSCOMP_1:104;
    now per cases by A3,A6,A7,Th21;
   suppose p = f/.i;
    hence thesis by A4,PARTFUN2:4;
   suppose p = f/.(i+1);
    hence thesis by A4,PARTFUN2:4;
   suppose A8: p`1 = (f/.i)`1 & p`1 = (f/.(i+1))`1;
    then f/.i in E-most L~f & f/.(i+1) in E-most L~f by A5,A7,Th17;
    then A9: (f/.i)`2 >= p`2 & (f/.(i+1))`2 >= p`2 by PSCOMP_1:108;
      (f/.i)`2 <= (f/.(i+1))`2 or (f/.(i+1))`2 <= (f/.i)`2;
    then (f/.i)`2 <= p`2 or (f/.(i+1))`2 <= p`2 by A3,TOPREAL1:10;
    then p`2 = (f/.i)`2 or p`2 = (f/.(i+1))`2 by A9,AXIOMS:21;
    then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11;
    hence thesis by A4,PARTFUN2:4;
  end;
  hence thesis;
end;

theorem Th50:
  E-max L~f in rng f
proof
  set p = E-max L~f;
  A1: len f >= 2 by SPPOL_1:2;
    p in L~f by SPRECT_1:16;
  then consider i be Nat such that
   A2: 1 <= i & i+1 <= len f and
   A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14;
    i <= i+1 by NAT_1:29;
  then i+1 >= 1 & i <= len f by A2,AXIOMS:22;
  then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27;
  then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16;
  then A6: (f/.i)`1 <= E-bound L~f & (f/.(i+1))`1 <= E-bound L~f
                                                            by PSCOMP_1:71;
  A7: p`1 = E-bound L~f by PSCOMP_1:104;
    now per cases by A3,A6,A7,Th21;
   suppose p = f/.i;
    hence thesis by A4,PARTFUN2:4;
   suppose p = f/.(i+1);
    hence thesis by A4,PARTFUN2:4;
   suppose A8: p`1 = (f/.i)`1 & p`1 = (f/.(i+1))`1;
    then f/.i in E-most L~f & f/.(i+1) in E-most L~f by A5,A7,Th17;
    then A9: (f/.i)`2 <= p`2 & (f/.(i+1))`2 <= p`2 by PSCOMP_1:108;
      (f/.i)`2 >= (f/.(i+1))`2 or (f/.(i+1))`2 >= (f/.i)`2;
    then (f/.i)`2 >= p`2 or (f/.(i+1))`2 >= p`2 by A3,TOPREAL1:10;
    then p`2 = (f/.i)`2 or p`2 = (f/.(i+1))`2 by A9,AXIOMS:21;
    then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11;
    hence thesis by A4,PARTFUN2:4;
  end;
  hence thesis;
end;

reserve f for non constant standard special_circular_sequence;

theorem Th51:
 1 <= i & i <= j & j < m & m <= n & n <= len f &
 (1 < i or n < len f) implies L~mid(f,i,j) misses L~mid(f,m,n)
proof assume that
A1: 1 <= i and
A2: i <= j and
A3: j < m and
A4: m <= n and
A5: n <= len f and
A6: 1 < i or n < len f;
  set A = { LSeg(f,k): i <= k & k < j},
      B = { LSeg(f,l): m <= l & l < n};
    m <= len f by A4,A5,AXIOMS:22;
  then j < len f by A3,AXIOMS:22;
then A7: L~mid(f,i,j) = union A by A1,A2,Th18;
    1 <= j by A1,A2,AXIOMS:22;
  then 1 < m by A3,AXIOMS:22;
then A8: L~mid(f,m,n) = union B by A4,A5,Th18;
    for x,y being set st x in A & y in B holds x misses y
   proof let x,y be set;
    assume x in A;
     then consider k such that
A9:   x = LSeg(f,k) and
A10:   i <= k and
A11:   k < j;
    assume y in B;
     then consider l such that
A12:   y = LSeg(f,l) and
A13:   m <= l and
A14:   l < n;
        k+1 <= j by A11,NAT_1:38;
      then k+1 < m by A3,AXIOMS:22;
then A15:    k+1 < l by A13,AXIOMS:22;
A16:    l < len f by A5,A14,AXIOMS:22;
       l+1 <= n by A14,NAT_1:38;
     then k > 1 or l+1 < len f by A6,A10,AXIOMS:22;
    hence x misses y by A9,A12,A15,A16,GOBOARD5:def 4;
   end;
 hence L~mid(f,i,j) misses L~mid(f,m,n) by A7,A8,Th4;
end;

theorem Th52:
 1 <= i & i <= j & j < m & m <= n & n <= len f &
 (1 < i or n < len f) implies L~mid(f,i,j) misses L~mid(f,n,m)
proof mid(f,n,m) = Rev mid(f,m,n) by JORDAN4:30;
 then L~mid(f,n,m) = L~mid(f,m,n) by SPPOL_2:22;
 hence thesis by Th51;
end;

theorem Th53:
 1 <= i & i <= j & j < m & m <= n & n <= len f &
 (1 < i or n < len f) implies L~mid(f,j,i) misses L~mid(f,n,m)
proof mid(f,i,j) = Rev mid(f,j,i) by JORDAN4:30;
 then L~mid(f,i,j) = L~mid(f,j,i) by SPPOL_2:22;
 hence thesis by Th52;
end;

theorem Th54:
 1 <= i & i <= j & j < m & m <= n & n <= len f &
 (1 < i or n < len f) implies L~mid(f,j,i) misses L~mid(f,m,n)
proof mid(f,i,j) = Rev mid(f,j,i) by JORDAN4:30;
 then L~mid(f,i,j) = L~mid(f,j,i) by SPPOL_2:22;
 hence thesis by Th51;
end;

theorem Th55:
 (N-min L~f)`1 < (N-max L~f)`1
proof set p = N-min L~f, i = p..f;
A1: len f > 3+1 by GOBOARD7:36;
then A2: len f >= 1+1 by AXIOMS:22;
A3: p in rng f by Th43;
then A4: i in dom f by FINSEQ_4:30;
A5: p = f.i by A3,FINSEQ_4:29 .= f/.i by A4,FINSEQ_4:def 4;
A6: 1 <= i & i <= len f by A4,FINSEQ_3:27;
A7: p`2 = N-bound L~f by PSCOMP_1:94;
 per cases by A6,REAL_1:def 5;
 suppose
A8: i = 1 or i = len f;
A9:  1 in dom f by FINSEQ_5:6;
A10:  len f in dom f by FINSEQ_5:6;
A11: f/.1 = f/.len f by FINSEQ_6:def 1;
A12: p = f/.1 by A5,A8,FINSEQ_6:def 1;
       len f >= 1 by A1,AXIOMS:22;
then A13:   len f -' 1+1 = len f by AMI_5:4;
     then len f -' 1 > 3 by A1,AXIOMS:24;
then A14:   len f -' 1 > 1 by AXIOMS:22;
       len f -' 1 <= len f by A13,NAT_1:29;
then A15:  len f -' 1 in dom f by A14,FINSEQ_3:27;
A16:  p in LSeg(f,len f -' 1) by A5,A8,A11,A13,A14,TOPREAL1:27;
A17: p in LSeg(f,1) by A2,A12,TOPREAL1:27;
A18:  p <> f/.(len f -' 1) by A5,A8,A10,A11,A13,A15,GOBOARD7:31;
A19: 1+1 in dom f by A2,FINSEQ_3:27;
then A20: p <> f/.(1+1) by A5,A8,A9,A11,GOBOARD7:31;
A21:  f/.(len f -' 1) in LSeg(f,len f -' 1) by A13,A14,TOPREAL1:27;
A22: f/.(1+1) in LSeg(f,1) by A2,TOPREAL1:27;
A23: f/.(len f -' 1) in L~f by A2,A15,GOBOARD1:16;
A24: f/.(1+1) in L~f by A2,A19,GOBOARD1:16;
  A25: not(LSeg(f,len f -' 1) is vertical & LSeg(f,1) is vertical)
   proof assume that
A26:  LSeg(f,len f -' 1) is vertical and
A27:  LSeg(f,1) is vertical;
A28:  LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A2,TOPREAL1:def 5;
A29:  LSeg(f,len f -' 1) = LSeg(f/.1,f/.(len f -' 1)) by A11,A13,A14,TOPREAL1:
def 5;
A30:  p`1 = (f/.(1+1))`1 & p`1 = (f/.(len f -' 1))`1
          by A16,A17,A21,A22,A26,A27,SPPOL_1:def 3;
A31:  p`2 >= (f/.(1+1))`2 & p`2 >= (f/.(len f -' 1))`2
        by A7,A23,A24,PSCOMP_1:71;
       (f/.(1+1))`2 <= (f/.(len f -' 1))`2 or
       (f/.(1+1))`2 >= (f/.(len f -' 1))`2;
     then f/.(len f -' 1) in LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1)
           by A5,A8,A11,A28,A29,A30,A31,GOBOARD7:8;
     then A32:   f/.(len f -' 1) in LSeg(f,len f -' 1) /\ LSeg(f,1) or
        f/.(1+1) in LSeg(f,len f -' 1) /\ LSeg(f,1) by A21,A22,XBOOLE_0:def 3;
A33:  f.1 = f/.1 by A9,FINSEQ_4:def 4;
       LSeg(f,len f -' 1) /\ LSeg(f,1) <> {f/.1}
       by A5,A8,A11,A18,A20,A32,TARSKI:def 1;
    hence contradiction by A33,JORDAN4:54;
   end;
    now per cases by A25,SPPOL_1:41;
   suppose
    LSeg(f,len f -' 1) is horizontal;
then A34:   p`2 = (f/.(len f -' 1))`2 by A16,A21,SPPOL_1:def 2;
then A35:   (f/.(len f -' 1))`1 <> p`1 by A18,TOPREAL3:11;
A36:   f/.(len f -' 1) in N-most L~f by A7,A23,A34,Th14;
     then (f/.(len f -' 1))`1 >= p`1 by PSCOMP_1:98;
     then A37:   (f/.(len f -' 1))`1 > p`1 by A35,REAL_1:def 5;
       (f/.(len f -' 1))`1 <= (N-max L~f)`1 by A36,PSCOMP_1:98;
    hence thesis by A37,AXIOMS:22;
   suppose
    LSeg(f,1) is horizontal;
then A38:   p`2 = (f/.(1+1))`2 by A17,A22,SPPOL_1:def 2;
then A39:   (f/.(1+1))`1 <> p`1 by A20,TOPREAL3:11;
A40:   f/.(1+1) in N-most L~f by A7,A24,A38,Th14;
     then (f/.(1+1))`1 >= p`1 by PSCOMP_1:98;
     then A41:   (f/.(1+1))`1 > p`1 by A39,REAL_1:def 5;
       (f/.(1+1))`1 <= (N-max L~f)`1 by A40,PSCOMP_1:98;
    hence thesis by A41,AXIOMS:22;
  end;
 hence thesis;
 suppose that
A42: 1 < i and
A43: i < len f;
A44:   i-'1+1 = i by A42,AMI_5:4;
then A45:   i-'1 >= 1 by A42,NAT_1:38;
       i-'1 <= i by A44,NAT_1:29;
     then i-'1 <= len f by A43,AXIOMS:22;
then A46:  i-'1 in dom f by A45,FINSEQ_3:27;
A47:  p in LSeg(f,i-'1) by A5,A43,A44,A45,TOPREAL1:27;
A48:  i+1 <= len f by A43,NAT_1:38;
then A49: p in LSeg(f,i) by A5,A42,TOPREAL1:27;
A50:  p <> f/.(i-'1) by A4,A5,A44,A46,GOBOARD7:31;
       i+1 >= 1 by NAT_1:29;
then A51: i+1 in dom f by A48,FINSEQ_3:27;
then A52: p <> f/.(i+1) by A4,A5,GOBOARD7:31;
A53:  f/.(i-'1) in LSeg(f,i-'1) by A43,A44,A45,TOPREAL1:27;
A54: f/.(i+1) in LSeg(f,i) by A42,A48,TOPREAL1:27;
A55:  f/.(i-'1) in L~f by A2,A46,GOBOARD1:16;
A56: f/.(i+1) in L~f by A2,A51,GOBOARD1:16;
  A57: not(LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical)
   proof assume that
A58:  LSeg(f,i-'1) is vertical and
A59:  LSeg(f,i) is vertical;
A60:   i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1;
A61:  LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A42,A48,TOPREAL1:def 5;
A62:  LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A43,A44,A45,TOPREAL1:def 5;
A63:  p`1 = (f/.(i+1))`1 & p`1 = (f/.(i-'1))`1
       by A47,A49,A53,A54,A58,A59,SPPOL_1:def 3;
A64:  p`2 >= (f/.(i+1))`2 & p`2 >= (f/.(i-'1))`2 by A7,A55,A56,PSCOMP_1:71;
       (f/.(i+1))`2 <= (f/.(i-'1))`2 or (f/.(i+1))`2 >= (f/.(i-'1))`2;
     then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1)
           by A5,A61,A62,A63,A64,GOBOARD7:8;
     then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or
        f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A53,A54,XBOOLE_0:def 3;
     then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A50,A52,TARSKI:def 1;
    hence contradiction by A44,A45,A48,A60,TOPREAL1:def 8;
   end;
    now per cases by A57,SPPOL_1:41;
   suppose
    LSeg(f,i-'1) is horizontal;
then A65:   p`2 = (f/.(i-'1))`2 by A47,A53,SPPOL_1:def 2;
then A66:   (f/.(i-'1))`1 <> p`1 by A50,TOPREAL3:11;
A67:   f/.(i-'1) in N-most L~f by A7,A55,A65,Th14;
     then (f/.(i-'1))`1 >= p`1 by PSCOMP_1:98;
     then A68:   (f/.(i-'1))`1 > p`1 by A66,REAL_1:def 5;
       (f/.(i-'1))`1 <= (N-max L~f)`1 by A67,PSCOMP_1:98;
    hence thesis by A68,AXIOMS:22;
   suppose
    LSeg(f,i) is horizontal;
then A69:   p`2 = (f/.(i+1))`2 by A49,A54,SPPOL_1:def 2;
then A70:   (f/.(i+1))`1 <> p`1 by A52,TOPREAL3:11;
A71:   f/.(i+1) in N-most L~f by A7,A56,A69,Th14;
     then (f/.(i+1))`1 >= p`1 by PSCOMP_1:98;
     then A72:   (f/.(i+1))`1 > p`1 by A70,REAL_1:def 5;
       (f/.(i+1))`1 <= (N-max L~f)`1 by A71,PSCOMP_1:98;
    hence thesis by A72,AXIOMS:22;
  end;
 hence thesis;
end;

theorem Th56:
 N-min L~f <> N-max L~f
proof
   (N-min L~f)`1 < (N-max L~f)`1 by Th55;
 hence thesis;
end;

theorem Th57:
 (E-min L~f)`2 < (E-max L~f)`2
proof set p = E-min L~f, i = p..f;
A1: len f > 3+1 by GOBOARD7:36;
then A2: len f >= 1+1 by AXIOMS:22;
A3: p in rng f by Th49;
then A4: i in dom f by FINSEQ_4:30;
A5: p = f.i by A3,FINSEQ_4:29 .= f/.i by A4,FINSEQ_4:def 4;
A6: 1 <= i & i <= len f by A4,FINSEQ_3:27;
A7: p`1 = E-bound L~f by PSCOMP_1:104;
 per cases by A6,REAL_1:def 5;
 suppose
A8: i = 1 or i = len f;
A9:  1 in dom f by FINSEQ_5:6;
A10:  len f in dom f by FINSEQ_5:6;
A11: f/.1 = f/.len f by FINSEQ_6:def 1;
A12: p = f/.1 by A5,A8,FINSEQ_6:def 1;
       len f >= 1 by A1,AXIOMS:22;
then A13:   len f -' 1+1 = len f by AMI_5:4;
     then len f -' 1 > 3 by A1,AXIOMS:24;
then A14:   len f -' 1 > 1 by AXIOMS:22;
       len f -' 1 <= len f by A13,NAT_1:29;
then A15:  len f -' 1 in dom f by A14,FINSEQ_3:27;
A16:  p in LSeg(f,len f -' 1) by A5,A8,A11,A13,A14,TOPREAL1:27;
A17: p in LSeg(f,1) by A2,A12,TOPREAL1:27;
A18:  p <> f/.(len f -' 1) by A5,A8,A10,A11,A13,A15,GOBOARD7:31;
A19: 1+1 in dom f by A2,FINSEQ_3:27;
then A20: p <> f/.(1+1) by A5,A8,A9,A11,GOBOARD7:31;
A21:  f/.(len f -' 1) in LSeg(f,len f -' 1) by A13,A14,TOPREAL1:27;
A22: f/.(1+1) in LSeg(f,1) by A2,TOPREAL1:27;
A23:  f/.(len f -' 1) in L~f by A2,A15,GOBOARD1:16;
A24: f/.(1+1) in L~f by A2,A19,GOBOARD1:16;
  A25: not(LSeg(f,len f -' 1) is horizontal & LSeg(f,1) is horizontal)
   proof assume that
A26:  LSeg(f,len f -' 1) is horizontal and
A27:  LSeg(f,1) is horizontal;
A28:  LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A2,TOPREAL1:def 5;
A29:  LSeg(f,len f -' 1) = LSeg(f/.1,f/.(len f -' 1)) by A11,A13,A14,TOPREAL1:
def 5;
A30:  p`2 = (f/.(1+1))`2 & p`2 = (f/.(len f -' 1))`2
          by A16,A17,A21,A22,A26,A27,SPPOL_1:def 2;
A31:  p`1 >= (f/.(1+1))`1 & p`1 >= (f/.(len f -' 1))`1
       by A7,A23,A24,PSCOMP_1:71;
       (f/.(1+1))`1 <= (f/.(len f -' 1))`1 or
     (f/.(1+1))`1 >= (f/.(len f -' 1))`1;
     then f/.(len f -' 1) in LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1)
           by A5,A8,A11,A28,A29,A30,A31,GOBOARD7:9;
     then A32:   f/.(len f -' 1) in LSeg(f,len f -' 1) /\ LSeg(f,1) or
        f/.(1+1) in LSeg(f,len f -' 1) /\ LSeg(f,1) by A21,A22,XBOOLE_0:def 3;
A33:  f.1 = f/.1 by A9,FINSEQ_4:def 4;
       LSeg(f,len f -' 1) /\ LSeg(f,1) <> {f/.1}
      by A5,A8,A11,A18,A20,A32,TARSKI:def 1;
    hence contradiction by A33,JORDAN4:54;
   end;
    now per cases by A25,SPPOL_1:41;
   suppose
    LSeg(f,len f -' 1) is vertical;
then A34:   p`1 = (f/.(len f -' 1))`1 by A16,A21,SPPOL_1:def 3;
then A35:   (f/.(len f -' 1))`2 <> p`2 by A18,TOPREAL3:11;
A36:   f/.(len f -' 1) in E-most L~f by A7,A23,A34,Th17;
     then (f/.(len f -' 1))`2 >= p`2 by PSCOMP_1:108;
     then A37:   (f/.(len f -' 1))`2 > p`2 by A35,REAL_1:def 5;
       (f/.(len f -' 1))`2 <= (E-max L~f)`2 by A36,PSCOMP_1:108;
    hence thesis by A37,AXIOMS:22;
   suppose
    LSeg(f,1) is vertical;
then A38:   p`1 = (f/.(1+1))`1 by A17,A22,SPPOL_1:def 3;
then A39:   (f/.(1+1))`2 <> p`2 by A20,TOPREAL3:11;
A40:   f/.(1+1) in E-most L~f by A7,A24,A38,Th17;
     then (f/.(1+1))`2 >= p`2 by PSCOMP_1:108;
     then A41:   (f/.(1+1))`2 > p`2 by A39,REAL_1:def 5;
       (f/.(1+1))`2 <= (E-max L~f)`2 by A40,PSCOMP_1:108;
    hence thesis by A41,AXIOMS:22;
  end;
 hence thesis;
 suppose that
A42: 1 < i and
A43: i < len f;
A44:   i-'1+1 = i by A42,AMI_5:4;
then A45:   i-'1 >= 1 by A42,NAT_1:38;
       i-'1 <= i by A44,NAT_1:29;
     then i-'1 <= len f by A43,AXIOMS:22;
then A46:  i-'1 in dom f by A45,FINSEQ_3:27;
A47:  p in LSeg(f,i-'1) by A5,A43,A44,A45,TOPREAL1:27;
A48:  i+1 <= len f by A43,NAT_1:38;
then A49: p in LSeg(f,i) by A5,A42,TOPREAL1:27;
A50:  p <> f/.(i-'1) by A4,A5,A44,A46,GOBOARD7:31;
       i+1 >= 1 by NAT_1:29;
then A51: i+1 in dom f by A48,FINSEQ_3:27;
then A52: p <> f/.(i+1) by A4,A5,GOBOARD7:31;
A53:  f/.(i-'1) in LSeg(f,i-'1) by A43,A44,A45,TOPREAL1:27;
A54: f/.(i+1) in LSeg(f,i) by A42,A48,TOPREAL1:27;
A55:  f/.(i-'1) in L~f by A2,A46,GOBOARD1:16;
A56: f/.(i+1) in L~f by A2,A51,GOBOARD1:16;
  A57: not(LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal)
   proof assume that
A58:  LSeg(f,i-'1) is horizontal and
A59:  LSeg(f,i) is horizontal;
A60:   i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1;
A61:  LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A42,A48,TOPREAL1:def 5;
A62:  LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A43,A44,A45,TOPREAL1:def 5;
A63:  p`2 = (f/.(i+1))`2 & p`2 = (f/.(i-'1))`2
  by A47,A49,A53,A54,A58,A59,SPPOL_1:def 2;
A64:  p`1 >= (f/.(i+1))`1 & p`1 >= (f/.(i-'1))`1 by A7,A55,A56,PSCOMP_1:71;
       (f/.(i+1))`1 <= (f/.(i-'1))`1 or (f/.(i+1))`1 >= (f/.(i-'1))`1;
     then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1)
           by A5,A61,A62,A63,A64,GOBOARD7:9;
     then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or
        f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A53,A54,XBOOLE_0:def 3;
     then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A50,A52,TARSKI:def 1;
    hence contradiction by A44,A45,A48,A60,TOPREAL1:def 8;
   end;
    now per cases by A57,SPPOL_1:41;
   suppose
    LSeg(f,i-'1) is vertical;
then A65:   p`1 = (f/.(i-'1))`1 by A47,A53,SPPOL_1:def 3;
then A66:   (f/.(i-'1))`2 <> p`2 by A50,TOPREAL3:11;
A67:   f/.(i-'1) in E-most L~f by A7,A55,A65,Th17;
     then (f/.(i-'1))`2 >= p`2 by PSCOMP_1:108;
     then A68:   (f/.(i-'1))`2 > p`2 by A66,REAL_1:def 5;
       (f/.(i-'1))`2 <= (E-max L~f)`2 by A67,PSCOMP_1:108;
    hence thesis by A68,AXIOMS:22;
   suppose
    LSeg(f,i) is vertical;
then A69:   p`1 = (f/.(i+1))`1 by A49,A54,SPPOL_1:def 3;
then A70:   (f/.(i+1))`2 <> p`2 by A52,TOPREAL3:11;
A71:   f/.(i+1) in E-most L~f by A7,A56,A69,Th17;
     then (f/.(i+1))`2 >= p`2 by PSCOMP_1:108;
     then A72:   (f/.(i+1))`2 > p`2 by A70,REAL_1:def 5;
       (f/.(i+1))`2 <= (E-max L~f)`2 by A71,PSCOMP_1:108;
    hence thesis by A72,AXIOMS:22;
  end;
 hence thesis;
end;

theorem
   E-min L~f <> E-max L~f
proof
   (E-min L~f)`2 < (E-max L~f)`2 by Th57;
 hence thesis;
end;

theorem Th59:
 (S-min L~f)`1 < (S-max L~f)`1
proof set p = S-min L~f, i = p..f;
A1: len f > 3+1 by GOBOARD7:36;
then A2: len f >= 1+1 by AXIOMS:22;
A3: p in rng f by Th45;
then A4: i in dom f by FINSEQ_4:30;
A5: p = f.i by A3,FINSEQ_4:29 .= f/.i by A4,FINSEQ_4:def 4;
A6: 1 <= i & i <= len f by A4,FINSEQ_3:27;
A7: p`2 = S-bound L~f by PSCOMP_1:114;
 per cases by A6,REAL_1:def 5;
 suppose
A8: i = 1 or i = len f;
A9:  1 in dom f by FINSEQ_5:6;
A10:  len f in dom f by FINSEQ_5:6;
A11: f/.1 = f/.len f by FINSEQ_6:def 1;
A12: p = f/.1 by A5,A8,FINSEQ_6:def 1;
       len f >= 1 by A1,AXIOMS:22;
then A13:   len f -' 1+1 = len f by AMI_5:4;
     then len f -' 1 > 3 by A1,AXIOMS:24;
then A14:   len f -' 1 > 1 by AXIOMS:22;
       len f -' 1 <= len f by A13,NAT_1:29;
then A15:  len f -' 1 in dom f by A14,FINSEQ_3:27;
A16:  p in LSeg(f,len f -' 1) by A5,A8,A11,A13,A14,TOPREAL1:27;
A17: p in LSeg(f,1) by A2,A12,TOPREAL1:27;
A18:  p <> f/.(len f -' 1) by A5,A8,A10,A11,A13,A15,GOBOARD7:31;
A19: 1+1 in dom f by A2,FINSEQ_3:27;
then A20: p <> f/.(1+1) by A5,A8,A9,A11,GOBOARD7:31;
A21:  f/.(len f -' 1) in LSeg(f,len f -' 1) by A13,A14,TOPREAL1:27;
A22: f/.(1+1) in LSeg(f,1) by A2,TOPREAL1:27;
A23:  f/.(len f -' 1) in L~f by A2,A15,GOBOARD1:16;
A24: f/.(1+1) in L~f by A2,A19,GOBOARD1:16;
  A25: not(LSeg(f,len f -' 1) is vertical & LSeg(f,1) is vertical)
   proof assume that
A26:  LSeg(f,len f -' 1) is vertical and
A27:  LSeg(f,1) is vertical;
A28:  LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A2,TOPREAL1:def 5;
A29:  LSeg(f,len f -' 1) = LSeg(f/.1,f/.(len f -' 1)) by A11,A13,A14,TOPREAL1:
def 5;
A30:  p`1 = (f/.(1+1))`1 & p`1 = (f/.(len f -' 1))`1
          by A16,A17,A21,A22,A26,A27,SPPOL_1:def 3;
A31:  p`2 <= (f/.(1+1))`2 & p`2 <= (f/.(len f -' 1))`2
       by A7,A23,A24,PSCOMP_1:71;
       (f/.(1+1))`2 <= (f/.(len f -' 1))`2 or
     (f/.(1+1))`2 >= (f/.(len f -' 1))`2;
     then f/.(len f -' 1) in LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1)
           by A5,A8,A11,A28,A29,A30,A31,GOBOARD7:8;
     then A32:   f/.(len f -' 1) in LSeg(f,len f -' 1) /\ LSeg(f,1) or
        f/.(1+1) in LSeg(f,len f -' 1) /\ LSeg(f,1) by A21,A22,XBOOLE_0:def 3;
A33:  f.1 = f/.1 by A9,FINSEQ_4:def 4;
       LSeg(f,len f -' 1) /\ LSeg(f,1) <> {f/.1}
     by A5,A8,A11,A18,A20,A32,TARSKI:def 1;
    hence contradiction by A33,JORDAN4:54;
   end;
    now per cases by A25,SPPOL_1:41;
   suppose
    LSeg(f,len f -' 1) is horizontal;
then A34:   p`2 = (f/.(len f -' 1))`2 by A16,A21,SPPOL_1:def 2;
then A35:   (f/.(len f -' 1))`1 <> p`1 by A18,TOPREAL3:11;
A36:   f/.(len f -' 1) in S-most L~f by A7,A23,A34,Th15;
     then (f/.(len f -' 1))`1 >= p`1 by PSCOMP_1:118;
     then A37:   (f/.(len f -' 1))`1 > p`1 by A35,REAL_1:def 5;
       (f/.(len f -' 1))`1 <= (S-max L~f)`1 by A36,PSCOMP_1:118;
    hence thesis by A37,AXIOMS:22;
   suppose
    LSeg(f,1) is horizontal;
then A38:   p`2 = (f/.(1+1))`2 by A17,A22,SPPOL_1:def 2;
then A39:   (f/.(1+1))`1 <> p`1 by A20,TOPREAL3:11;
A40:   f/.(1+1) in S-most L~f by A7,A24,A38,Th15;
     then (f/.(1+1))`1 >= p`1 by PSCOMP_1:118;
     then A41:   (f/.(1+1))`1 > p`1 by A39,REAL_1:def 5;
       (f/.(1+1))`1 <= (S-max L~f)`1 by A40,PSCOMP_1:118;
    hence thesis by A41,AXIOMS:22;
  end;
 hence thesis;
 suppose that
A42: 1 < i and
A43: i < len f;
A44:   i-'1+1 = i by A42,AMI_5:4;
then A45:   i-'1 >= 1 by A42,NAT_1:38;
       i-'1 <= i by A44,NAT_1:29;
     then i-'1 <= len f by A43,AXIOMS:22;
then A46:  i-'1 in dom f by A45,FINSEQ_3:27;
A47:  p in LSeg(f,i-'1) by A5,A43,A44,A45,TOPREAL1:27;
A48:  i+1 <= len f by A43,NAT_1:38;
then A49: p in LSeg(f,i) by A5,A42,TOPREAL1:27;
A50:  p <> f/.(i-'1) by A4,A5,A44,A46,GOBOARD7:31;
       i+1 >= 1 by NAT_1:29;
then A51: i+1 in dom f by A48,FINSEQ_3:27;
then A52: p <> f/.(i+1) by A4,A5,GOBOARD7:31;
A53:  f/.(i-'1) in LSeg(f,i-'1) by A43,A44,A45,TOPREAL1:27;
A54: f/.(i+1) in LSeg(f,i) by A42,A48,TOPREAL1:27;
A55:  f/.(i-'1) in L~f by A2,A46,GOBOARD1:16;
A56: f/.(i+1) in L~f by A2,A51,GOBOARD1:16;
  A57: not(LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical)
   proof assume that
A58:  LSeg(f,i-'1) is vertical and
A59:  LSeg(f,i) is vertical;
A60:   i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1;
A61:  LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A42,A48,TOPREAL1:def 5;
A62:  LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A43,A44,A45,TOPREAL1:def 5;
A63:  p`1 = (f/.(i+1))`1 & p`1 = (f/.(i-'1))`1
      by A47,A49,A53,A54,A58,A59,SPPOL_1:def 3;
A64:  p`2 <= (f/.(i+1))`2 & p`2 <= (f/.(i-'1))`2 by A7,A55,A56,PSCOMP_1:71;
       (f/.(i+1))`2 <= (f/.(i-'1))`2 or (f/.(i+1))`2 >= (f/.(i-'1))`2;
     then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1)
           by A5,A61,A62,A63,A64,GOBOARD7:8;
     then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or
        f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A53,A54,XBOOLE_0:def 3;
     then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A50,A52,TARSKI:def 1;
    hence contradiction by A44,A45,A48,A60,TOPREAL1:def 8;
   end;
    now per cases by A57,SPPOL_1:41;
   suppose
    LSeg(f,i-'1) is horizontal;
then A65:   p`2 = (f/.(i-'1))`2 by A47,A53,SPPOL_1:def 2;
then A66:   (f/.(i-'1))`1 <> p`1 by A50,TOPREAL3:11;
A67:   f/.(i-'1) in S-most L~f by A7,A55,A65,Th15;
     then (f/.(i-'1))`1 >= p`1 by PSCOMP_1:118;
     then A68:   (f/.(i-'1))`1 > p`1 by A66,REAL_1:def 5;
       (f/.(i-'1))`1 <= (S-max L~f)`1 by A67,PSCOMP_1:118;
    hence thesis by A68,AXIOMS:22;
   suppose
    LSeg(f,i) is horizontal;
then A69:   p`2 = (f/.(i+1))`2 by A49,A54,SPPOL_1:def 2;
then A70:   (f/.(i+1))`1 <> p`1 by A52,TOPREAL3:11;
A71:   f/.(i+1) in S-most L~f by A7,A56,A69,Th15;
     then (f/.(i+1))`1 >= p`1 by PSCOMP_1:118;
     then A72:   (f/.(i+1))`1 > p`1 by A70,REAL_1:def 5;
       (f/.(i+1))`1 <= (S-max L~f)`1 by A71,PSCOMP_1:118;
    hence thesis by A72,AXIOMS:22;
  end;
 hence thesis;
end;

theorem Th60:
 S-min L~f <> S-max L~f
proof
   (S-min L~f)`1 < (S-max L~f)`1 by Th59;
 hence thesis;
end;

theorem Th61:
 (W-min L~f)`2 < (W-max L~f)`2
proof set p = W-min L~f, i = p..f;
A1: len f > 3+1 by GOBOARD7:36;
then A2: len f >= 1+1 by AXIOMS:22;
A3: p in rng f by Th47;
then A4: i in dom f by FINSEQ_4:30;
A5: p = f.i by A3,FINSEQ_4:29 .= f/.i by A4,FINSEQ_4:def 4;
A6: 1 <= i & i <= len f by A4,FINSEQ_3:27;
A7: p`1 = W-bound L~f by PSCOMP_1:84;
 per cases by A6,REAL_1:def 5;
 suppose
A8: i = 1 or i = len f;
A9:  1 in dom f by FINSEQ_5:6;
A10:  len f in dom f by FINSEQ_5:6;
A11: f/.1 = f/.len f by FINSEQ_6:def 1;
A12: p = f/.1 by A5,A8,FINSEQ_6:def 1;
       len f >= 1 by A1,AXIOMS:22;
then A13:   len f -' 1+1 = len f by AMI_5:4;
     then len f -' 1 > 3 by A1,AXIOMS:24;
then A14:   len f -' 1 > 1 by AXIOMS:22;
       len f -' 1 <= len f by A13,NAT_1:29;
then A15:  len f -' 1 in dom f by A14,FINSEQ_3:27;
A16:  p in LSeg(f,len f -' 1) by A5,A8,A11,A13,A14,TOPREAL1:27;
A17: p in LSeg(f,1) by A2,A12,TOPREAL1:27;
A18:  p <> f/.(len f -' 1) by A5,A8,A10,A11,A13,A15,GOBOARD7:31;
A19: 1+1 in dom f by A2,FINSEQ_3:27;
then A20: p <> f/.(1+1) by A5,A8,A9,A11,GOBOARD7:31;
A21:  f/.(len f -' 1) in LSeg(f,len f -' 1) by A13,A14,TOPREAL1:27;
A22: f/.(1+1) in LSeg(f,1) by A2,TOPREAL1:27;
A23:  f/.(len f -' 1) in L~f by A2,A15,GOBOARD1:16;
A24: f/.(1+1) in L~f by A2,A19,GOBOARD1:16;
  A25: not(LSeg(f,len f -' 1) is horizontal & LSeg(f,1) is horizontal)
   proof assume that
A26:  LSeg(f,len f -' 1) is horizontal and
A27:  LSeg(f,1) is horizontal;
A28:  LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A2,TOPREAL1:def 5;
A29:  LSeg(f,len f -' 1) = LSeg(f/.1,f/.(len f -' 1)) by A11,A13,A14,TOPREAL1:
def 5;
A30:  p`2 = (f/.(1+1))`2 & p`2 = (f/.(len f -' 1))`2
          by A16,A17,A21,A22,A26,A27,SPPOL_1:def 2;
A31:  p`1 <= (f/.(1+1))`1 & p`1 <= (f/.(len f -' 1))`1
       by A7,A23,A24,PSCOMP_1:71;
       (f/.(1+1))`1 <= (f/.(len f -' 1))`1
     or (f/.(1+1))`1 >= (f/.(len f -' 1))`1;
     then f/.(len f -' 1) in LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1)
           by A5,A8,A11,A28,A29,A30,A31,GOBOARD7:9;
     then A32:   f/.(len f -' 1) in LSeg(f,len f -' 1) /\ LSeg(f,1) or
        f/.(1+1) in LSeg(f,len f -' 1) /\ LSeg(f,1) by A21,A22,XBOOLE_0:def 3;
A33:  f.1 = f/.1 by A9,FINSEQ_4:def 4;
       LSeg(f,len f -' 1) /\ LSeg(f,1) <> {f/.1}
     by A5,A8,A11,A18,A20,A32,TARSKI:def 1;
    hence contradiction by A33,JORDAN4:54;
   end;
    now per cases by A25,SPPOL_1:41;
   suppose
    LSeg(f,len f -' 1) is vertical;
then A34:   p`1 = (f/.(len f -' 1))`1 by A16,A21,SPPOL_1:def 3;
then A35:   (f/.(len f -' 1))`2 <> p`2 by A18,TOPREAL3:11;
A36:   f/.(len f -' 1) in W-most L~f by A7,A23,A34,Th16;
     then (f/.(len f -' 1))`2 >= p`2 by PSCOMP_1:88;
     then A37:   (f/.(len f -' 1))`2 > p`2 by A35,REAL_1:def 5;
       (f/.(len f -' 1))`2 <= (W-max L~f)`2 by A36,PSCOMP_1:88;
    hence thesis by A37,AXIOMS:22;
   suppose
    LSeg(f,1) is vertical;
then A38:   p`1 = (f/.(1+1))`1 by A17,A22,SPPOL_1:def 3;
then A39:   (f/.(1+1))`2 <> p`2 by A20,TOPREAL3:11;
A40:   f/.(1+1) in W-most L~f by A7,A24,A38,Th16;
     then (f/.(1+1))`2 >= p`2 by PSCOMP_1:88;
     then A41:   (f/.(1+1))`2 > p`2 by A39,REAL_1:def 5;
       (f/.(1+1))`2 <= (W-max L~f)`2 by A40,PSCOMP_1:88;
    hence thesis by A41,AXIOMS:22;
  end;
 hence thesis;
 suppose that
A42: 1 < i and
A43: i < len f;
A44:   i-'1+1 = i by A42,AMI_5:4;
then A45:   i-'1 >= 1 by A42,NAT_1:38;
       i-'1 <= i by A44,NAT_1:29;
     then i-'1 <= len f by A43,AXIOMS:22;
then A46:  i-'1 in dom f by A45,FINSEQ_3:27;
A47:  p in LSeg(f,i-'1) by A5,A43,A44,A45,TOPREAL1:27;
A48:  i+1 <= len f by A43,NAT_1:38;
then A49: p in LSeg(f,i) by A5,A42,TOPREAL1:27;
A50:  p <> f/.(i-'1) by A4,A5,A44,A46,GOBOARD7:31;
       i+1 >= 1 by NAT_1:29;
then A51: i+1 in dom f by A48,FINSEQ_3:27;
then A52: p <> f/.(i+1) by A4,A5,GOBOARD7:31;
A53:  f/.(i-'1) in LSeg(f,i-'1) by A43,A44,A45,TOPREAL1:27;
A54: f/.(i+1) in LSeg(f,i) by A42,A48,TOPREAL1:27;
A55:  f/.(i-'1) in L~f by A2,A46,GOBOARD1:16;
A56: f/.(i+1) in L~f by A2,A51,GOBOARD1:16;
  A57: not(LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal)
   proof assume that
A58:  LSeg(f,i-'1) is horizontal and
A59:  LSeg(f,i) is horizontal;
A60:   i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1;
A61:  LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A42,A48,TOPREAL1:def 5;
A62:  LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A43,A44,A45,TOPREAL1:def 5;
A63:  p`2 = (f/.(i+1))`2 & p`2 = (f/.(i-'1))`2
  by A47,A49,A53,A54,A58,A59,SPPOL_1:def 2;
A64:  p`1 <= (f/.(i+1))`1 & p`1 <= (f/.(i-'1))`1 by A7,A55,A56,PSCOMP_1:71;
       (f/.(i+1))`1 <= (f/.(i-'1))`1 or (f/.(i+1))`1 >= (f/.(i-'1))`1;
     then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1)
           by A5,A61,A62,A63,A64,GOBOARD7:9;
     then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or
        f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A53,A54,XBOOLE_0:def 3;
     then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A50,A52,TARSKI:def 1;
    hence contradiction by A44,A45,A48,A60,TOPREAL1:def 8;
   end;
    now per cases by A57,SPPOL_1:41;
   suppose
    LSeg(f,i-'1) is vertical;
then A65:   p`1 = (f/.(i-'1))`1 by A47,A53,SPPOL_1:def 3;
then A66:   (f/.(i-'1))`2 <> p`2 by A50,TOPREAL3:11;
A67:   f/.(i-'1) in W-most L~f by A7,A55,A65,Th16;
     then (f/.(i-'1))`2 >= p`2 by PSCOMP_1:88;
     then A68:   (f/.(i-'1))`2 > p`2 by A66,REAL_1:def 5;
       (f/.(i-'1))`2 <= (W-max L~f)`2 by A67,PSCOMP_1:88;
    hence thesis by A68,AXIOMS:22;
   suppose
    LSeg(f,i) is vertical;
then A69:   p`1 = (f/.(i+1))`1 by A49,A54,SPPOL_1:def 3;
then A70:   (f/.(i+1))`2 <> p`2 by A52,TOPREAL3:11;
A71:   f/.(i+1) in W-most L~f by A7,A56,A69,Th16;
     then (f/.(i+1))`2 >= p`2 by PSCOMP_1:88;
     then A72:   (f/.(i+1))`2 > p`2 by A70,REAL_1:def 5;
       (f/.(i+1))`2 <= (W-max L~f)`2 by A71,PSCOMP_1:88;
    hence thesis by A72,AXIOMS:22;
  end;
 hence thesis;
end;

theorem Th62:
 W-min L~f <> W-max L~f
proof
   (W-min L~f)`2 < (W-max L~f)`2 by Th61;
 hence thesis;
end;

theorem Th63:
 LSeg(NW-corner L~f,N-min L~f) misses LSeg(N-max L~f,NE-corner L~f)
proof assume LSeg(NW-corner L~f,N-min L~f) meets LSeg(N-max L~f,NE-corner L~f)
;
  then consider p being set such that
A1: p in LSeg(NW-corner L~f,N-min L~f) and
A2: p in LSeg(N-max L~f,NE-corner L~f) by XBOOLE_0:3;
  reconsider p as Point of TOP-REAL 2 by A1;
     (NW-corner L~f)`1 <= (N-min L~f)`1 by PSCOMP_1:97;
then A3: p`1 <= (N-min L~f)`1 by A1,TOPREAL1:9;
    (N-max L~f)`1 <= (NE-corner L~f)`1 by PSCOMP_1:97;
  then (N-max L~f)`1 <= p`1 by A2,TOPREAL1:9;
then A4:(N-min L~f)`1 >= (N-max L~f)`1 by A3,AXIOMS:22;
    (N-min L~f)`1 <= (N-max L~f)`1 by PSCOMP_1:97;
then A5:(N-min L~f)`1 = (N-max L~f)`1 by A4,AXIOMS:21;
    (N-min L~f)`2 = (N-max L~f)`2 by PSCOMP_1:95;
  then N-min L~f = N-max L~f by A5,TOPREAL3:11;
 hence contradiction by Th56;
end;

theorem Th64:
 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2
  st f is_S-Seq & p <> f/.1 & (p`1 = (f/.1)`1 or p`2 = (f/.1)`2)
    & LSeg(p,f/.1) /\ L~f = {f/.1}
  holds <*p*>^f is S-Sequence_in_R2
proof let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2 such that
A1: f is_S-Seq and
A2: p <> f/.1 and
A3: p`1 = (f/.1)`1 or p`2 = (f/.1)`2 and
A4: LSeg(p,f/.1) /\ L~f = {f/.1};
  reconsider f as S-Sequence_in_R2 by A1;
A5:  1 in dom f by FINSEQ_5:6;
A6: len f >= 1+1 by TOPREAL1:def 10;
then A7:  f/.1 in LSeg(f,1) by TOPREAL1:27;
  set g = <*p*>^f;
    g is being_S-Seq
   proof
A8:   <*p*> is one-to-one by FINSEQ_3:102;
       now assume
A9:    p in rng f;
       A10: rng f c= L~f by A6,SPPOL_2:18;
         p in LSeg(p,f/.1) by TOPREAL1:6;
       then p in {f/.1} by A4,A9,A10,XBOOLE_0:def 3;
      hence contradiction by A2,TARSKI:def 1;
     end;
     then {p} misses rng f by ZFMISC_1:56;
     then rng<*p*> misses rng f by FINSEQ_1:56;
    hence g is one-to-one by A8,FINSEQ_3:98;
       len g = len<*p*> + len f by FINSEQ_1:35;
     then len g >= len f by NAT_1:29;
    hence len g >= 2 by A6,AXIOMS:22;
       LSeg(f,1) c= L~f by TOPREAL3:26;
     then LSeg(p,f/.1) /\ LSeg(f,1) = {f/.1} by A4,A7,Th2;
    hence g is unfolded by SPPOL_2:30;
A11:   len<*p*> = 1 by FINSEQ_1:56;
then A12:   <*p*> is s.n.c. by SPPOL_2:34;
A13:   <*p*>/.len <*p*> = p by A11,FINSEQ_4:25;
        L~<*p*> = {} by SPPOL_2:12;
       then L~<*p*> /\ L~f = {};
then A14:   L~<*p*> misses L~f by XBOOLE_0:def 7;
A15:   now let i such that 1<=i;
      assume
A16:    i+2 <= len <*p*>;
         2 <= i+2 by NAT_1:29;
      hence LSeg(<*p*>,i) misses LSeg(p,f/.1) by A11,A16,AXIOMS:22;
     end;
       now let i such that
A17:   1+1<=i and
A18:   i+1 <= len f;
A19:     2 in dom f by A6,FINSEQ_3:27;
         now assume f/.1 in LSeg(f,i);
then A20:      f/.1 in LSeg(f,1) /\ LSeg(f,i) by A7,XBOOLE_0:def 3;
then A21:       LSeg(f,1) meets LSeg(f,i) by XBOOLE_0:4;
           now per cases by A17,REAL_1:def 5;
          case
A22:        i = 1+1;
           then LSeg(f,1) /\ LSeg(f,1+1) = {f/.2} by A18,TOPREAL1:def 8;
          hence f/.1 = f/.2 by A20,A22,TARSKI:def 1;
          case i > 1+1;
          hence contradiction by A21,TOPREAL1:def 9;
         end;
         then f.1 = f/.2 by A5,FINSEQ_4:def 4 .= f.2 by A19,FINSEQ_4:def 4;
        hence contradiction by A5,A19,FUNCT_1:def 8;
       end;
       then not f/.1 in LSeg(f,i) /\ LSeg(p,f/.1) by XBOOLE_0:def 3;
then A23:     LSeg(f,i) /\ LSeg(p,f/.1) <> {f/.1} by TARSKI:def 1;
         LSeg(f,i) c= L~f by TOPREAL3:26;
       then LSeg(f,i) /\ LSeg(p,f/.1) c= {f/.1} by A4,XBOOLE_1:26;
      then LSeg(f,i) /\ LSeg(p,f/.1) = {} by A23,ZFMISC_1:39;
      hence LSeg(f,i) misses LSeg(p,f/.1) by XBOOLE_0:def 7;
     end;
    hence g is s.n.c. by A12,A13,A14,A15,SPPOL_2:37;
A24: <*p*> is special by SPPOL_2:39;
       <*p*>/.len <*p*> = <*p*>/.1 by FINSEQ_1:56
          .= p by FINSEQ_4:25;
    hence g is special by A3,A24,GOBOARD2:13;
   end;
 hence thesis;
end;

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

begin  :: Appending corners

theorem Th66:
 for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 &
  f/.j = N-max L~f & N-max L~f <> NE-corner L~f
 holds mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2
proof set p = NE-corner L~f;
 let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.j = N-max L~f and
A5: N-max L~f <> NE-corner L~f;
A6:  (mid(f,i,j))/.len mid(f,i,j) = N-max L~f by A1,A2,A4,Th13;
then A7: p`2 = ((mid(f,i,j))/.len mid(f,i,j))`2 by PSCOMP_1:95;
A8: LSeg(NE-corner L~f, N-max L~f)/\L~f = {N-max L~f} by PSCOMP_1:102;
      len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10;
then A9: N-max L~f in L~mid(f,i,j) by A6,JORDAN3:34;
    1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27;
  then L~mid(f,i,j) c= L~f by JORDAN4:47;
  then LSeg(p, (mid(f,i,j))/.len mid(f,i,j)) /\ L~mid(f,i,j)
       = {(mid(f,i,j))/.len mid(f,i,j)} by A6,A8,A9,Th2;
 hence mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2 by A3,A5,A6,A7,Th65;
end;

theorem
   for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 &
  f/.j = E-max L~f & E-max L~f <> NE-corner L~f
 holds mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2
proof set p = NE-corner L~f;
 let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.j = E-max L~f and
A5: E-max L~f <> NE-corner L~f;
A6:  (mid(f,i,j))/.len mid(f,i,j) = E-max L~f by A1,A2,A4,Th13;
then A7: p`1 = ((mid(f,i,j))/.len mid(f,i,j))`1 by PSCOMP_1:105;
A8: LSeg(NE-corner L~f, E-max L~f)/\L~f = {E-max L~f} by PSCOMP_1:112;
      len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10;
then A9: E-max L~f in L~mid(f,i,j) by A6,JORDAN3:34;
    1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27;
  then L~mid(f,i,j) c= L~f by JORDAN4:47;
  then LSeg(p, (mid(f,i,j))/.len mid(f,i,j)) /\ L~mid(f,i,j)
       = {(mid(f,i,j))/.len mid(f,i,j)} by A6,A8,A9,Th2;
 hence mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2 by A3,A5,A6,A7,Th65;
end;

theorem Th68:
 for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 &
  f/.j = S-max L~f & S-max L~f <> SE-corner L~f
 holds mid(f,i,j)^<*SE-corner L~f*> is S-Sequence_in_R2
proof set p = SE-corner L~f;
 let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.j = S-max L~f and
A5: S-max L~f <> SE-corner L~f;
A6:  (mid(f,i,j))/.len mid(f,i,j) = S-max L~f by A1,A2,A4,Th13;
then A7: p`2 = ((mid(f,i,j))/.len mid(f,i,j))`2 by PSCOMP_1:115;
A8: LSeg(SE-corner L~f, S-max L~f)/\L~f = {S-max L~f} by PSCOMP_1:122;
      len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10;
then A9: S-max L~f in L~mid(f,i,j) by A6,JORDAN3:34;
    1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27;
  then L~mid(f,i,j) c= L~f by JORDAN4:47;
  then LSeg(p, (mid(f,i,j))/.len mid(f,i,j)) /\ L~mid(f,i,j)
       = {(mid(f,i,j))/.len mid(f,i,j)} by A6,A8,A9,Th2;
 hence mid(f,i,j)^<*SE-corner L~f*> is S-Sequence_in_R2 by A3,A5,A6,A7,Th65;
end;

theorem Th69:
 for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 &
  f/.j = E-max L~f & E-max L~f <> NE-corner L~f
 holds mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2
proof set p = NE-corner L~f;
 let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.j = E-max L~f and
A5: E-max L~f <> NE-corner L~f;
A6:  (mid(f,i,j))/.len mid(f,i,j) = E-max L~f by A1,A2,A4,Th13;
then A7: p`1 = ((mid(f,i,j))/.len mid(f,i,j))`1 by PSCOMP_1:105;
A8: LSeg(NE-corner L~f, E-max L~f)/\L~f = {E-max L~f} by PSCOMP_1:112;
      len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10;
then A9: E-max L~f in L~mid(f,i,j) by A6,JORDAN3:34;
    1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27;
  then L~mid(f,i,j) c= L~f by JORDAN4:47;
  then LSeg(p, (mid(f,i,j))/.len mid(f,i,j)) /\ L~mid(f,i,j)
       = {(mid(f,i,j))/.len mid(f,i,j)} by A6,A8,A9,Th2;
 hence mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2 by A3,A5,A6,A7,Th65;
end;

theorem Th70:
 for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 &
  f/.i = N-min L~f & N-min L~f <> NW-corner L~f
 holds <*NW-corner L~f*>^mid(f,i,j) is S-Sequence_in_R2
proof set p = NW-corner L~f;
 let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.i = N-min L~f and
A5: N-min L~f <> NW-corner L~f;
A6:  (mid(f,i,j))/.1 = N-min L~f by A1,A2,A4,Th12;
then A7: p`2 = ((mid(f,i,j))/.1)`2 by PSCOMP_1:95;
A8: LSeg(NW-corner L~f, N-min L~f)/\L~f = {N-min L~f} by PSCOMP_1:102;
      len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10;
then A9: N-min L~f in L~mid(f,i,j) by A6,JORDAN3:34;
    1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27;
  then L~mid(f,i,j) c= L~f by JORDAN4:47;
  then LSeg(p, (mid(f,i,j))/.1) /\ L~mid(f,i,j) = {(mid(f,i,j))/.1}
    by A6,A8,A9,Th2;
 hence <*NW-corner L~f*>^mid(f,i,j) is S-Sequence_in_R2 by A3,A5,A6,A7,Th64;
end;

theorem Th71:
 for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 &
  f/.i = W-min L~f & W-min L~f <> SW-corner L~f
 holds <*SW-corner L~f*>^mid(f,i,j) is S-Sequence_in_R2
proof set p = SW-corner L~f;
 let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.i = W-min L~f and
A5: W-min L~f <> SW-corner L~f;
A6:  (mid(f,i,j))/.1 = W-min L~f by A1,A2,A4,Th12;
then A7: p`1 = ((mid(f,i,j))/.1)`1 by PSCOMP_1:85;
A8: LSeg(SW-corner L~f, W-min L~f)/\L~f = {W-min L~f} by PSCOMP_1:92;
      len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10;
then A9: W-min L~f in L~mid(f,i,j) by A6,JORDAN3:34;
    1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27;
  then L~mid(f,i,j) c= L~f by JORDAN4:47;
  then LSeg(p, (mid(f,i,j))/.1) /\ L~mid(f,i,j) = {(mid(f,i,j))/.1}
    by A6,A8,A9,Th2;
 hence <*SW-corner L~f*>^mid(f,i,j) is S-Sequence_in_R2 by A3,A5,A6,A7,Th64;
end;

Lm3:
 for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 &
  f/.i = N-min L~f & N-min L~f <> NW-corner L~f &
  f/.j = N-max L~f & N-max L~f <> NE-corner L~f
 holds <*NW-corner L~f*>^mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2
proof set p = NW-corner L~f, q = NE-corner L~f;
 let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.i = N-min L~f and
A5: N-min L~f <> NW-corner L~f and
A6: f/.j = N-max L~f and
A7: N-max L~f <> NE-corner L~f;
    set g = <*NW-corner L~f*>^mid(f,i,j);
A8: g is S-Sequence_in_R2 by A1,A2,A3,A4,A5,Th70;
A9:  len g = len<*NW-corner L~f*> + len mid(f,i,j) by FINSEQ_1:35;
      len mid(f,i,j) in dom mid(f,i,j) by A3,FINSEQ_5:6;
then A10:  g/.len g = (mid(f,i,j))/.len mid(f,i,j) by A9,GROUP_5:96;
then A11:  g/.len g = N-max L~f by A1,A2,A6,Th13;
then A12: q`2 = (g/.len g)`2 by PSCOMP_1:95;
A13: LSeg(NE-corner L~f, N-max L~f)/\L~f = {N-max L~f} by PSCOMP_1:102;
      len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10;
then A14: N-max L~f in L~mid(f,i,j) by A10,A11,JORDAN3:34;
    1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27;
  then A15:  L~mid(f,i,j) c= L~f by JORDAN4:47;
    (mid(f,i,j))/.1 = f/.i by A1,A2,Th12;
then A16: L~g = LSeg(p,N-min L~f) \/ L~mid(f,i,j) by A3,A4,SPPOL_2:20;
    LSeg(g/.len g,q) misses LSeg(p,N-min L~f) by A11,Th63;
  then LSeg(q, g/.len g) /\ LSeg(p,N-min L~f) = {} by XBOOLE_0:def 7;
  then LSeg(q, g/.len g) /\ L~g
          = LSeg(q, g/.len g) /\ L~mid(f,i,j) \/ {} by A16,XBOOLE_1:23
         .= {g/.len g} by A11,A13,A14,A15,Th2;
 hence <*NW-corner L~f*>^mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2
     by A7,A8,A11,A12,Th65;
end;

definition
 let f be non constant standard special_circular_sequence;
 cluster L~f -> being_simple_closed_curve;
 coherence by JORDAN4:63;
end;

Lm4: LSeg(S-max L~f,SE-corner L~f) misses LSeg(NW-corner L~f,N-min L~f)
proof
 assume LSeg(S-max L~f,SE-corner L~f) meets LSeg(NW-corner L~f,N-min L~f);
  then LSeg(S-max L~f,SE-corner L~f) /\ LSeg(NW-corner L~f,N-min L~f) <> {}
     by XBOOLE_0:def 7;
  then consider x being set such that
A1: x in LSeg(S-max L~f,SE-corner L~f) /\ LSeg(NW-corner L~f,N-min L~f)
                 by XBOOLE_0:def 1;
A2: x in LSeg(S-max L~f,SE-corner L~f) by A1,XBOOLE_0:def 3;
   reconsider p = x as Point of TOP-REAL 2 by A1;
A3: p in LSeg(NW-corner L~f,N-min L~f) by A1,XBOOLE_0:def 3;
     (NW-corner L~f)`2 = N-bound L~f & (N-min L~f)`2 = N-bound L~f
      by PSCOMP_1:75,94;
   then N-bound L~f <= p`2 & p`2 <= N-bound L~f by A3,TOPREAL1:10;
   then A4:  p`2 = N-bound L~f by AXIOMS:21;
    (SE-corner L~f)`2 = S-bound L~f & (S-max L~f)`2 = S-bound L~f
     by PSCOMP_1:79,114
;
  then S-bound L~f <= p`2 & p`2 <= S-bound L~f by A2,TOPREAL1:10;
 hence contradiction by A4,TOPREAL5:22;
end;

Lm5:
 for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 &
  f/.i = N-min L~f & N-min L~f <> NW-corner L~f &
  f/.j = S-max L~f & S-max L~f <> SE-corner L~f
 holds <*NW-corner L~f*>^mid(f,i,j)^<*SE-corner L~f*> is S-Sequence_in_R2
proof set p = NW-corner L~f, q = SE-corner L~f;
 let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.i = N-min L~f and
A5: N-min L~f <> NW-corner L~f and
A6: f/.j = S-max L~f and
A7: S-max L~f <> SE-corner L~f;
    set g = <*NW-corner L~f*>^mid(f,i,j);
A8: g is S-Sequence_in_R2 by A1,A2,A3,A4,A5,Th70;
A9:  len g = len<*NW-corner L~f*> + len mid(f,i,j) by FINSEQ_1:35;
      len mid(f,i,j) in dom mid(f,i,j) by A3,FINSEQ_5:6;
then A10:  g/.len g = (mid(f,i,j))/.len mid(f,i,j) by A9,GROUP_5:96;
then A11:  g/.len g = S-max L~f by A1,A2,A6,Th13;
then A12: q`2 = (g/.len g)`2 by PSCOMP_1:115;
A13: LSeg(SE-corner L~f, S-max L~f)/\L~f = {S-max L~f} by PSCOMP_1:122;
      len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10;
then A14: S-max L~f in L~mid(f,i,j) by A10,A11,JORDAN3:34;
    1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27;
  then A15:  L~mid(f,i,j) c= L~f by JORDAN4:47;
    (mid(f,i,j))/.1 = f/.i by A1,A2,Th12;
then A16: L~g = LSeg(p,N-min L~f) \/ L~mid(f,i,j) by A3,A4,SPPOL_2:20;
    LSeg(g/.len g,q) misses LSeg(p,N-min L~f) by A11,Lm4;
  then LSeg(q, g/.len g) /\ LSeg(p,N-min L~f) = {} by XBOOLE_0:def 7;
  then LSeg(q, g/.len g) /\ L~g
          = LSeg(q, g/.len g) /\ L~mid(f,i,j) \/ {} by A16,XBOOLE_1:23
         .= {g/.len g} by A11,A13,A14,A15,Th2;
 hence <*NW-corner L~f*>^mid(f,i,j)^<*SE-corner L~f*> is S-Sequence_in_R2
     by A7,A8,A11,A12,Th65;
end;

begin :: The order

theorem Th72:
 f/.1 = N-min L~f implies (N-min L~f)..f < (N-max L~f)..f
proof
A1: N-min L~f in rng f by Th43;
A2: N-max L~f in rng f by Th44;
     N-min L~f <> N-max L~f by Th56;
then A3: (N-min L~f)..f <> (N-max L~f)..f by A1,A2,FINSEQ_5:10;
    (N-max L~f)..f in dom f by A2,FINSEQ_4:30;
then A4: (N-max L~f)..f >= 1 by FINSEQ_3:27;
 assume f/.1 = N-min L~f;
  then (N-min L~f)..f = 1 by FINSEQ_6:47;
 hence (N-min L~f)..f < (N-max L~f)..f by A3,A4,REAL_1:def 5;
end;

theorem
   f/.1 = N-min L~f implies (N-max L~f)..f > 1
proof
 assume
A1:  f/.1 = N-min L~f;
  then (N-min L~f)..f = 1 by FINSEQ_6:47;
 hence thesis by A1,Th72;
end;

Lm6:
 f/.1 = N-min L~f implies (N-min L~f)..f < (E-max L~f)..f
proof
A1: E-max L~f in rng f by Th50;
A2: N-min L~f in rng f by Th43;
A3: (N-min L~f)`1 < (N-max L~f)`1 by Th55;
     (N-max L~f)`1 <= (NE-corner L~f)`1 by PSCOMP_1:97;
   then (N-max L~f)`1 <= E-bound L~f by PSCOMP_1:76;
   then (N-min L~f)`1 < E-bound L~f by A3,AXIOMS:22;
   then (N-min L~f)`1 < (E-max L~f)`1 by PSCOMP_1:104;
   then A4: (N-min L~f)..f <> (E-max L~f)..f by A1,A2,FINSEQ_5:10;
 assume f/.1 = N-min L~f;
  then A5: (N-min L~f)..f = 1 by FINSEQ_6:47;
    (E-max L~f)..f >= 1 by A1,FINSEQ_4:31;
 hence (N-min L~f)..f < (E-max L~f)..f by A4,A5,REAL_1:def 5;
end;

reserve z for clockwise_oriented
              (non constant standard special_circular_sequence);

Lm7:
 z/.1 = N-min L~z implies (N-max L~z)..z < (S-max L~z)..z
proof set i1 = (N-max L~z)..z, i2 = (S-max L~z)..z;
 assume that
A1: z/.1 = N-min L~z and
A2: i1 >= i2;
A3: N-max L~z in rng z by Th44;
A4: S-max L~z in rng z by Th46;
A5: i1 in dom z by A3,FINSEQ_4:30;
then A6: 1 <= i1 & i1 <= len z by FINSEQ_3:27;
A7: i2 in dom z by A4,FINSEQ_4:30;
then A8: 1 <= i2 & i2 <= len z by FINSEQ_3:27;
A9: z/.i2 = z.i2 by A7,FINSEQ_4:def 4
          .= S-max L~z by A4,FINSEQ_4:29;
A10:  z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
A11:  z/.i1 = z.i1 by A5,FINSEQ_4:def 4
          .= N-max L~z by A3,FINSEQ_4:29;
      (N-max L~z)`2 = N-bound L~z & (S-max L~z)`2 = S-bound L~z
             by PSCOMP_1:94,114;
    then z/.i1 <> z/.i2 by A9,A11,TOPREAL5:22;
then A12: i1 > i2 by A2,REAL_1:def 5;
then A13: i1 > 1 by A8,AXIOMS:22;
A14: len z in dom z by FINSEQ_5:6;
A15: z/.1 = z/.len z by FINSEQ_6:def 1;
A16: 2 <= len z by SPPOL_1:2;
then A17: 2 in dom z by FINSEQ_3:27;
      z/.2 in N-most L~z by A1,Th34;
    then A18: (z/.2)`2 = (N-min L~z)`2 by PSCOMP_1:98
         .= N-bound L~z by PSCOMP_1:94;
A19: (z/.1)`2 = N-bound L~z by A1,PSCOMP_1:94;
A20: i2 <> 0 by A7,FINSEQ_3:27;
   (z/.i2)`2 = S-bound L~z by A9,PSCOMP_1:114;
    then i2 <> 1 & i2 <> 2 by A18,A19,TOPREAL5:22;
then A21: i2 > 2 by A20,CQC_THE1:3;
  then reconsider h = mid(z,i2,2) as S-Sequence_in_R2 by A8,Th41;
A22: h is_in_the_area_of z by A7,A17,Th27;
      h/.1 = S-max L~z by A7,A9,A17,Th12;
then A23: (h/.1)`2 = S-bound L~z by PSCOMP_1:114;
A24: L~h c= L~z by A8,A16,JORDAN4:47;
      (h/.len h)`2 = N-bound L~z by A7,A17,A18,Th13;
then A25: h is_a_v.c._for z by A22,A23,Def3;
    N-min L~z <> N-max L~z by Th56;
  then A26: i1 < len z by A6,A10,A11,REAL_1:def 5;
 then reconsider M = mid(z,len z,i1) as S-Sequence_in_R2 by A13,Th41;
A27: L~M misses L~h by A6,A12,A21,Th53;
A28: M/.len M = z/.i1 by A5,A14,Th13
          .= N-max L~z by A3,FINSEQ_5:41;
A29: len M = len z -' i1 + 1 by A6,JORDAN4:21;
      i1 + 1 <= len z by A26,NAT_1:38;
    then len z - i1 >= 1 by REAL_1:84;
    then len z -' i1 >= 1 by JORDAN3:1;
    then A30: len z -' i1 + 1 >= 1+1 by AXIOMS:24;
then A31: M/.len M in L~M by A29,JORDAN3:34;
A32:  2 <= len h by TOPREAL1:def 10;
A33: 1 in dom M by FINSEQ_5:6;
A34: M/.1 = z/.1 by A5,A14,A15,Th12;
 per cases;
 suppose that
A35: NW-corner L~z = N-min L~z and
A36: NE-corner L~z = N-max L~z;
A37: M is_in_the_area_of z by A5,A14,Th27;
      M/.1 = z/.len z by A5,A14,Th12;
then A38: (M/.1)`1 = W-bound L~z by A1,A15,A35,PSCOMP_1:74;
      (M/.len M)`1 = E-bound L~z by A28,A36,PSCOMP_1:76;
    then M is_a_h.c._for z by A37,A38,Def2;
 hence contradiction by A25,A27,A29,A30,A32,Th33;
 suppose that
A39: NW-corner L~z = N-min L~z and
A40: NE-corner L~z <> N-max L~z;
  reconsider g = M^<*NE-corner L~z*> as S-Sequence_in_R2
   by A5,A11,A14,A40,Th66;
A41:  len g >= 2 by TOPREAL1:def 10;
A42: M is_in_the_area_of z by A5,A14,Th27;
      <*NE-corner L~z*> is_in_the_area_of z by Th29;
then A43: g is_in_the_area_of z by A42,Th28;
      g/.1 = M/.1 by A33,GROUP_5:95
       .= z/.1 by A5,A14,A15,Th12;
then A44: (g/.1)`1 = W-bound L~z by A1,A39,PSCOMP_1:74;
      len g = len M + len<*NE-corner L~z*> by FINSEQ_1:35
         .= len M + 1 by FINSEQ_1:56;
    then g/.len g = NE-corner L~z by TOPREAL4:1;
    then (g/.len g)`1 = E-bound L~z by PSCOMP_1:76;
then A45: g is_a_h.c._for z by A43,A44,Def2;
A46:  L~g = L~M \/ LSeg(M/.len M,NE-corner L~z) by SPPOL_2:19;
      LSeg(M/.len M,NE-corner L~z) /\ L~h c=
           LSeg(M/.len M,NE-corner L~z) /\ L~z by A24,XBOOLE_1:26;
 then LSeg(M/.len M,NE-corner L~z) /\ L~h c= {M/.len M} by A28,PSCOMP_1:102;
   then L~g misses L~h by A27,A31,A46,Th1;
 hence contradiction by A25,A32,A41,A45,Th33;
 suppose that
A47: NW-corner L~z <> N-min L~z and
A48: NE-corner L~z = N-max L~z;
  reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2
        by A1,A5,A14,A15,A47,Th70;
A49:  len g >= 2 by TOPREAL1:def 10;
A50: M is_in_the_area_of z by A5,A14,Th27;
      <*NW-corner L~z*> is_in_the_area_of z by Th30;
then A51: g is_in_the_area_of z by A50,Th28;
      g/.1 = NW-corner L~z by FINSEQ_5:16;
then A52: (g/.1)`1 = W-bound L~z by PSCOMP_1:74;
A53:  len M in dom M by FINSEQ_5:6;
      len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35;
    then g/.len g = M/.len M by A53,GROUP_5:96
          .= z/.i1 by A5,A14,Th13
          .= N-max L~z by A3,FINSEQ_5:41;
    then (g/.len g)`1 = E-bound L~z by A48,PSCOMP_1:76;
then A54: g is_a_h.c._for z by A51,A52,Def2;
A55:  L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20;
      LSeg(M/.1,NW-corner L~z) /\ L~h c=
           LSeg(M/.1,NW-corner L~z) /\ L~z by A24,XBOOLE_1:26;
then A56: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A34,PSCOMP_1:102;
      M/.1 in L~M by A29,A30,JORDAN3:34;
   then L~g misses L~h by A27,A55,A56,Th1;
 hence contradiction by A25,A32,A49,A54,Th33;
 suppose that
A57: NW-corner L~z <> N-min L~z and
A58: NE-corner L~z <> N-max L~z;
  set K = <*NW-corner L~z*>^M;
  reconsider g = K^<*NE-corner L~z*>
      as S-Sequence_in_R2 by A1,A5,A11,A14,A15,A57,A58,Lm3;
A59:  len g >= 2 by TOPREAL1:def 10;
A60: M is_in_the_area_of z by A5,A14,Th27;
      <*NW-corner L~z*> is_in_the_area_of z by Th30;
then A61: <*NW-corner L~z*>^M is_in_the_area_of z by A60,Th28;
      <*NE-corner L~z*> is_in_the_area_of z by Th29;
then A62: g is_in_the_area_of z by A61,Th28;
      1 in dom(<*NW-corner L~z*>^M) by FINSEQ_5:6;
    then g/.1 = (<*NW-corner L~z*>^M)/.1 by GROUP_5:95
       .= NW-corner L~z by FINSEQ_5:16;
then A63: (g/.1)`1 = W-bound L~z by PSCOMP_1:74;
      len g = len(<*NW-corner L~z*>^M) + len<*NE-corner L~z*>
           by FINSEQ_1:35
         .= len(<*NW-corner L~z*>^M) + 1 by FINSEQ_1:56;
    then g/.len g = NE-corner L~z by TOPREAL4:1;
    then (g/.len g)`1 = E-bound L~z by PSCOMP_1:76;
then A64: g is_a_h.c._for z by A62,A63,Def2;
A65:  L~K = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20;
      LSeg(M/.1,NW-corner L~z) /\ L~h c=
           LSeg(M/.1,NW-corner L~z) /\ L~z by A24,XBOOLE_1:26;
then A66: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A34,PSCOMP_1:102;
      M/.1 in L~M by A29,A30,JORDAN3:34;
then A67: L~K misses L~h by A27,A65,A66,Th1;
      len K = len M + len<*NW-corner L~z*> by FINSEQ_1:35;
    then len K >= len M by NAT_1:29;
     then len K >= 2 by A29,A30,AXIOMS:22;
then A68: K/.len K in L~K by JORDAN3:34;
A69:  L~g = L~K \/ LSeg(K/.len K,NE-corner L~z) by SPPOL_2:19;
A70:  len M in dom M by FINSEQ_5:6;
      len K = len M + len<*NW-corner L~z*> by FINSEQ_1:35;
    then A71: K/.len K = M/.len M by A70,GROUP_5:96
          .= z/.i1 by A5,A14,Th13
          .= N-max L~z by A3,FINSEQ_5:41;
      LSeg(K/.len K,NE-corner L~z) /\ L~h c=
           LSeg(K/.len K,NE-corner L~z) /\ L~z by A24,XBOOLE_1:26;
    then LSeg(K/.len K,NE-corner L~z) /\ L~h c= {K/.len K}
      by A71,PSCOMP_1:102;
   then L~g misses L~h by A67,A68,A69,Th1;
 hence contradiction by A25,A32,A59,A64,Th33;
end;

Lm8:
 z/.1 = N-min L~z implies (N-max L~z)..z < (S-min L~z)..z
proof set i1 = (N-max L~z)..z, i2 = (S-min L~z)..z;
 assume that
A1: z/.1 = N-min L~z and
A2: i1 >= i2;
A3: N-max L~z in rng z by Th44;
A4: S-min L~z in rng z by Th45;
A5: i1 in dom z by A3,FINSEQ_4:30;
then A6: 1 <= i1 & i1 <= len z by FINSEQ_3:27;
A7: i2 in dom z by A4,FINSEQ_4:30;
then A8: 1 <= i2 & i2 <= len z by FINSEQ_3:27;
A9: z/.i2 = z.i2 by A7,FINSEQ_4:def 4
          .= S-min L~z by A4,FINSEQ_4:29;
A10:  z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
A11:  z/.i1 = z.i1 by A5,FINSEQ_4:def 4
          .= N-max L~z by A3,FINSEQ_4:29;
      (N-max L~z)`2 = N-bound L~z & (S-min L~z)`2 = S-bound L~z
             by PSCOMP_1:94,114;
    then z/.i1 <> z/.i2 by A9,A11,TOPREAL5:22;
then A12: i1 > i2 by A2,REAL_1:def 5;
then A13: i1 > 1 by A8,AXIOMS:22;
A14: len z in dom z by FINSEQ_5:6;
A15: z/.1 = z/.len z by FINSEQ_6:def 1;
A16: 2 <= len z by SPPOL_1:2;
then A17: 2 in dom z by FINSEQ_3:27;
      z/.2 in N-most L~z by A1,Th34;
    then A18: (z/.2)`2 = (N-min L~z)`2 by PSCOMP_1:98
         .= N-bound L~z by PSCOMP_1:94;
A19: (z/.1)`2 = N-bound L~z by A1,PSCOMP_1:94;
A20: i2 <> 0 by A7,FINSEQ_3:27;
A21: (z/.i2)`2 = S-bound L~z by A9,PSCOMP_1:114;
      S-bound L~z < N-bound L~z by TOPREAL5:22;
    then A22: i2 > 2 by A18,A19,A20,A21,CQC_THE1:3;
  then reconsider h = mid(z,i2,2) as S-Sequence_in_R2 by A8,Th41;
A23: len h >= 2 by TOPREAL1:def 10;
A24: h is_in_the_area_of z by A7,A17,Th27;
      h/.1 = S-min L~z by A7,A9,A17,Th12;
then A25: (h/.1)`2 = S-bound L~z by PSCOMP_1:114;
A26: L~h c= L~z by A8,A16,JORDAN4:47;
      h/.len h = z/.2 by A7,A17,Th13;
    then A27: h is_a_v.c._for z by A18,A24,A25,Def3;
    N-min L~z <> N-max L~z by Th56;
  then A28: i1 < len z by A6,A10,A11,REAL_1:def 5;
 then reconsider M = mid(z,len z,i1) as S-Sequence_in_R2 by A13,Th41;
A29: L~M misses L~h by A6,A12,A22,Th53;
A30: M/.len M = z/.i1 by A5,A14,Th13
          .= N-max L~z by A3,FINSEQ_5:41;
A31: len M = len z -' i1 + 1 by A6,JORDAN4:21;
      i1 + 1 <= len z by A28,NAT_1:38;
    then len z - i1 >= 1 by REAL_1:84;
    then len z -' i1 >= 1 by JORDAN3:1;
    then A32: len z -' i1 + 1 >= 1+1 by AXIOMS:24;
then A33: M/.len M in L~M by A31,JORDAN3:34;
A34: 1 in dom M by FINSEQ_5:6;
A35: M/.1 = z/.1 by A5,A14,A15,Th12;
 per cases;
 suppose that
A36: NW-corner L~z = N-min L~z and
A37: NE-corner L~z = N-max L~z;
A38: M is_in_the_area_of z by A5,A14,Th27;
      M/.1 = z/.len z by A5,A14,Th12;
then A39: (M/.1)`1 = W-bound L~z by A1,A15,A36,PSCOMP_1:74;
      (M/.len M)`1 = E-bound L~z by A30,A37,PSCOMP_1:76;
    then M is_a_h.c._for z by A38,A39,Def2;
 hence contradiction by A23,A27,A29,A31,A32,Th33;
 suppose that
A40: NW-corner L~z = N-min L~z and
A41: NE-corner L~z <> N-max L~z;
  reconsider g = M^<*NE-corner L~z*> as S-Sequence_in_R2
   by A5,A11,A14,A41,Th66;
A42: len g >= 2 by TOPREAL1:def 10;
A43: M is_in_the_area_of z by A5,A14,Th27;
      <*NE-corner L~z*> is_in_the_area_of z by Th29;
then A44: g is_in_the_area_of z by A43,Th28;
      g/.1 = M/.1 by A34,GROUP_5:95
       .= z/.1 by A5,A14,A15,Th12;
then A45: (g/.1)`1 = W-bound L~z by A1,A40,PSCOMP_1:74;
      len g = len M + len<*NE-corner L~z*> by FINSEQ_1:35
         .= len M + 1 by FINSEQ_1:56;
    then g/.len g = NE-corner L~z by TOPREAL4:1;
    then (g/.len g)`1 = E-bound L~z by PSCOMP_1:76;
then A46: g is_a_h.c._for z by A44,A45,Def2;
A47:  L~g = L~M \/ LSeg(M/.len M,NE-corner L~z) by SPPOL_2:19;
      LSeg(M/.len M,NE-corner L~z) /\ L~h c=
           LSeg(M/.len M,NE-corner L~z) /\ L~z by A26,XBOOLE_1:26;
 then LSeg(M/.len M,NE-corner L~z) /\ L~h c= {M/.len M} by A30,PSCOMP_1:102;
   then L~g misses L~h by A29,A33,A47,Th1;
 hence contradiction by A23,A27,A42,A46,Th33;
 suppose that
A48: NW-corner L~z <> N-min L~z and
A49: NE-corner L~z = N-max L~z;
  reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2
        by A1,A5,A14,A15,A48,Th70;
A50: len g >= 2 by TOPREAL1:def 10;
A51: M is_in_the_area_of z by A5,A14,Th27;
      <*NW-corner L~z*> is_in_the_area_of z by Th30;
then A52: g is_in_the_area_of z by A51,Th28;
      g/.1 = NW-corner L~z by FINSEQ_5:16;
then A53: (g/.1)`1 = W-bound L~z by PSCOMP_1:74;
A54:  len M in dom M by FINSEQ_5:6;
      len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35;
    then g/.len g = M/.len M by A54,GROUP_5:96
          .= z/.i1 by A5,A14,Th13
          .= N-max L~z by A3,FINSEQ_5:41;
    then (g/.len g)`1 = E-bound L~z by A49,PSCOMP_1:76;
then A55: g is_a_h.c._for z by A52,A53,Def2;
A56:  L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20;
      LSeg(M/.1,NW-corner L~z) /\ L~h c=
           LSeg(M/.1,NW-corner L~z) /\ L~z by A26,XBOOLE_1:26;
then A57: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A35,PSCOMP_1:102;
      M/.1 in L~M by A31,A32,JORDAN3:34;
   then L~g misses L~h by A29,A56,A57,Th1;
 hence contradiction by A23,A27,A50,A55,Th33;
 suppose that
A58: NW-corner L~z <> N-min L~z and
A59: NE-corner L~z <> N-max L~z;
  set K = <*NW-corner L~z*>^M;
  reconsider g = K^<*NE-corner L~z*>
      as S-Sequence_in_R2 by A1,A5,A11,A14,A15,A58,A59,Lm3;
A60: len g >= 2 by TOPREAL1:def 10;
A61: M is_in_the_area_of z by A5,A14,Th27;
      <*NW-corner L~z*> is_in_the_area_of z by Th30;
then A62: <*NW-corner L~z*>^M is_in_the_area_of z by A61,Th28;
      <*NE-corner L~z*> is_in_the_area_of z by Th29;
then A63: g is_in_the_area_of z by A62,Th28;
      1 in dom(<*NW-corner L~z*>^M) by FINSEQ_5:6;
    then g/.1 = (<*NW-corner L~z*>^M)/.1 by GROUP_5:95
       .= NW-corner L~z by FINSEQ_5:16;
then A64: (g/.1)`1 = W-bound L~z by PSCOMP_1:74;
      len g = len(<*NW-corner L~z*>^M) + len<*NE-corner L~z*>
           by FINSEQ_1:35
         .= len(<*NW-corner L~z*>^M) + 1 by FINSEQ_1:56;
    then g/.len g = NE-corner L~z by TOPREAL4:1;
    then (g/.len g)`1 = E-bound L~z by PSCOMP_1:76;
then A65: g is_a_h.c._for z by A63,A64,Def2;
A66:  L~K = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20;
      LSeg(M/.1,NW-corner L~z) /\ L~h c=
           LSeg(M/.1,NW-corner L~z) /\ L~z by A26,XBOOLE_1:26;
then A67: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A35,PSCOMP_1:102;
      M/.1 in L~M by A31,A32,JORDAN3:34;
then A68: L~K misses L~h by A29,A66,A67,Th1;
      len K = len M + len<*NW-corner L~z*> by FINSEQ_1:35;
    then len K >= len M by NAT_1:29;
     then len K >= 2 by A31,A32,AXIOMS:22;
then A69: K/.len K in L~K by JORDAN3:34;
A70:  L~g = L~K \/ LSeg(K/.len K,NE-corner L~z) by SPPOL_2:19;
A71:  len M in dom M by FINSEQ_5:6;
      len K = len M + len<*NW-corner L~z*> by FINSEQ_1:35;
    then A72: K/.len K = M/.len M by A71,GROUP_5:96
          .= z/.i1 by A5,A14,Th13
          .= N-max L~z by A3,FINSEQ_5:41;
      LSeg(K/.len K,NE-corner L~z) /\ L~h c=
           LSeg(K/.len K,NE-corner L~z) /\ L~z by A26,XBOOLE_1:26;
 then LSeg(K/.len K,NE-corner L~z) /\ L~h c= {K/.len K} by A72,PSCOMP_1:102;
   then L~g misses L~h by A68,A69,A70,Th1;
 hence contradiction by A23,A27,A60,A65,Th33;
end;

theorem
   z/.1 = N-min L~z & N-max L~z <> E-max L~z
  implies (N-max L~z)..z < (E-max L~z)..z
proof set i1 = (N-max L~z)..z, i2 = (E-max L~z)..z, j = (S-max L~z)..z;
 assume that
A1: z/.1 = N-min L~z and
A2: N-max L~z <> E-max L~z and
A3: i1 >= i2;
A4: E-max L~z in rng z by Th50;
A5: S-max L~z in rng z by Th46;
A6: N-max L~z in rng z by Th44;
A7: 1 in dom z by FINSEQ_5:6;
A8: i1 in dom z by A6,FINSEQ_4:30;
then A9: 1 <= i1 & i1 <= len z by FINSEQ_3:27;
A10: j in dom z by A5,FINSEQ_4:30;
then A11: 1 <= j & j <= len z by FINSEQ_3:27;
A12: z/.j = z.j by A10,FINSEQ_4:def 4
          .= S-max L~z by A5,FINSEQ_4:29;
A13: i2 in dom z by A4,FINSEQ_4:30;
then A14: 1 <= i2 & i2 <= len z by FINSEQ_3:27;
A15: z/.i1 = z.i1 by A8,FINSEQ_4:def 4
          .= N-max L~z by A6,FINSEQ_4:29;
A16: j > i1 by A1,Lm7;
      (N-min L~z)`2 = N-bound L~z & (S-max L~z)`2 = S-bound L~z
             by PSCOMP_1:94,114;
then A17: N-min L~z <> S-max L~z by TOPREAL5:22;
      z/.len z = z/.1 by FINSEQ_6:def 1;
    then A18: j < len z by A1,A11,A12,A17,REAL_1:def 5;
  then reconsider h = mid(z,j,i1) as S-Sequence_in_R2 by A9,A16,Th41;
A19: h is_in_the_area_of z by A8,A10,Th27;
      h/.1 = S-max L~z by A8,A10,A12,Th12;
then A20: (h/.1)`2 = S-bound L~z by PSCOMP_1:114;
A21: L~h c= L~z by A9,A11,JORDAN4:47;
      h/.len h = z/.i1 by A8,A10,Th13;
    then (h/.len h)`2 = N-bound L~z by A15,PSCOMP_1:94;
then A22: h is_a_v.c._for z by A19,A20,Def3;
      (N-min L~z)..z = 1 by A1,FINSEQ_6:47;
    then A23: 1 < i2 by A1,Lm6;
      z/.i2 = z.i2 by A13,FINSEQ_4:def 4
          .= E-max L~z by A4,FINSEQ_4:29;
    then A24: i1 > i2 by A2,A3,A15,REAL_1:def 5;
  then i2 < len z by A9,AXIOMS:22;
  then reconsider M = mid(z,1,i2) as S-Sequence_in_R2 by A23,Th42;
A25: len M >= 2 & len h >= 2 by TOPREAL1:def 10;
A26: L~M misses L~h by A16,A18,A23,A24,Th52;
A27: M/.len M = z/.i2 by A7,A13,Th13
          .= E-max L~z by A4,FINSEQ_5:41;
 per cases;
 suppose
A28:  NW-corner L~z = N-min L~z;
A29: M is_in_the_area_of z by A7,A13,Th27;
      M/.1 = z/.1 by A7,A13,Th12;
then A30: (M/.1)`1 = W-bound L~z by A1,A28,PSCOMP_1:74;
      (M/.len M)`1 = E-bound L~z by A27,PSCOMP_1:104;
    then M is_a_h.c._for z by A29,A30,Def2;
 hence contradiction by A22,A25,A26,Th33;
 suppose
   NW-corner L~z <> N-min L~z;
  then reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2
        by A1,A7,A13,Th70;
A31: len g >= 2 by TOPREAL1:def 10;
A32: M is_in_the_area_of z by A7,A13,Th27;
      <*NW-corner L~z*> is_in_the_area_of z by Th30;
then A33: g is_in_the_area_of z by A32,Th28;
      g/.1 = NW-corner L~z by FINSEQ_5:16;
then A34: (g/.1)`1 = W-bound L~z by PSCOMP_1:74;
A35:  len M in dom M by FINSEQ_5:6;
      len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35;
    then g/.len g = M/.len M by A35,GROUP_5:96
          .= z/.i2 by A7,A13,Th13
          .= E-max L~z by A4,FINSEQ_5:41;
    then (g/.len g)`1 = E-bound L~z by PSCOMP_1:104;
then A36: g is_a_h.c._for z by A33,A34,Def2;
A37:  L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20;
A38: M/.1 = z/.1 by A7,A13,Th12;
      len M = i2 -' 1 + 1 by A14,JORDAN4:20
         .= i2 by A23,AMI_5:4;
then A39: len M >= 1+1 by A23,NAT_1:38;
      LSeg(M/.1,NW-corner L~z) /\ L~h c=
           LSeg(M/.1,NW-corner L~z) /\ L~z by A21,XBOOLE_1:26;
then A40: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A38,PSCOMP_1:102;
      M/.1 in L~M by A39,JORDAN3:34;
   then L~g misses L~h by A26,A37,A40,Th1;
 hence contradiction by A22,A25,A31,A36,Th33;
end;

Lm9:
 z/.1 = N-min L~z implies (E-max L~z)..z < (S-max L~z)..z
proof set i1 = (E-max L~z)..z, i2 = (S-max L~z)..z;
 assume that
A1: z/.1 = N-min L~z and
A2: i1 >= i2;
A3: E-max L~z in rng z by Th50;
A4: S-max L~z in rng z by Th46;
A5: i1 in dom z by A3,FINSEQ_4:30;
then A6: 1 <= i1 & i1 <= len z by FINSEQ_3:27;
A7: i2 in dom z by A4,FINSEQ_4:30;
then A8: 1 <= i2 & i2 <= len z by FINSEQ_3:27;
A9: z/.i2 = z.i2 by A7,FINSEQ_4:def 4
          .= S-max L~z by A4,FINSEQ_4:29;
A10:  z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
A11:  z/.i1 = z.i1 by A5,FINSEQ_4:def 4
          .= E-max L~z by A3,FINSEQ_4:29;
A12:(E-min L~z)`2 < (E-max L~z)`2 by Th57;
    E-min L~z in L~z by SPRECT_1:16;
  then S-bound L~z <= (E-min L~z)`2 by PSCOMP_1:71;
  then E-max L~z <> S-max L~z by A12,PSCOMP_1:114;
    then A13: i1 > i2 by A2,A9,A11,REAL_1:def 5;
then A14: i1 > 1 by A8,AXIOMS:22;
A15: len z in dom z by FINSEQ_5:6;
A16: z/.1 = z/.len z by FINSEQ_6:def 1;
A17: 2 <= len z by SPPOL_1:2;
then A18: 2 in dom z by FINSEQ_3:27;
      z/.2 in N-most L~z by A1,Th34;
    then A19: (z/.2)`2 = (N-min L~z)`2 by PSCOMP_1:98
         .= N-bound L~z by PSCOMP_1:94;
A20: (z/.1)`2 = N-bound L~z by A1,PSCOMP_1:94;
A21: i2 <> 0 by A7,FINSEQ_3:27;
A22: (z/.i2)`2 = S-bound L~z by A9,PSCOMP_1:114;
      S-bound L~z < N-bound L~z by TOPREAL5:22;
    then A23: i2 > 2 by A19,A20,A21,A22,CQC_THE1:3;
  then reconsider h = mid(z,i2,2) as S-Sequence_in_R2 by A8,Th41;
A24: len h >= 2 by TOPREAL1:def 10;
A25: h is_in_the_area_of z by A7,A18,Th27;
      h/.1 = S-max L~z by A7,A9,A18,Th12;
then A26: (h/.1)`2 = S-bound L~z by PSCOMP_1:114;
A27: L~h c= L~z by A8,A17,JORDAN4:47;
      h/.len h = z/.2 by A7,A18,Th13;
    then A28: h is_a_v.c._for z by A19,A25,A26,Def3;
A29:  (N-min L~z)`1 < (N-max L~z)`1 by Th55;
    N-max L~z in L~z by SPRECT_1:13;
  then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:71;
  then i1 <> len z by A10,A11,A29,PSCOMP_1:104;
  then A30: i1 < len z by A6,REAL_1:def 5;
 then reconsider M = mid(z,len z,i1) as S-Sequence_in_R2 by A14,Th41;
A31: len M >= 2 by TOPREAL1:def 10;
A32: L~M misses L~h by A6,A13,A23,Th53;
A33: M/.len M = z/.i1 by A5,A15,Th13
          .= E-max L~z by A3,FINSEQ_5:41;
A34: len M = len z -' i1 + 1 by A6,JORDAN4:21;
      i1 + 1 <= len z by A30,NAT_1:38;
    then len z - i1 >= 1 by REAL_1:84;
    then len z -' i1 >= 1 by JORDAN3:1;
    then A35: len z -' i1 + 1 >= 1+1 by AXIOMS:24;
A36: M/.1 = z/.1 by A5,A15,A16,Th12;
 per cases;
 suppose that
A37: NW-corner L~z = N-min L~z;
A38: M is_in_the_area_of z by A5,A15,Th27;
      M/.1 = z/.len z by A5,A15,Th12;
then A39: (M/.1)`1 = W-bound L~z by A1,A16,A37,PSCOMP_1:74;
      (M/.len M)`1 = E-bound L~z by A33,PSCOMP_1:104;
    then M is_a_h.c._for z by A38,A39,Def2;
 hence contradiction by A24,A28,A31,A32,Th33;
 suppose
   NW-corner L~z <> N-min L~z;
  then reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2
        by A1,A5,A15,A16,Th70;
A40: len g >= 2 by TOPREAL1:def 10;
A41: M is_in_the_area_of z by A5,A15,Th27;
      <*NW-corner L~z*> is_in_the_area_of z by Th30;
then A42: g is_in_the_area_of z by A41,Th28;
      g/.1 = NW-corner L~z by FINSEQ_5:16;
then A43: (g/.1)`1 = W-bound L~z by PSCOMP_1:74;
A44:  len M in dom M by FINSEQ_5:6;
      len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35;
    then g/.len g = M/.len M by A44,GROUP_5:96
          .= z/.i1 by A5,A15,Th13
          .= E-max L~z by A3,FINSEQ_5:41;
    then (g/.len g)`1 = E-bound L~z by PSCOMP_1:104;
then A45: g is_a_h.c._for z by A42,A43,Def2;
A46:  L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20;
      LSeg(M/.1,NW-corner L~z) /\ L~h c=
           LSeg(M/.1,NW-corner L~z) /\ L~z by A27,XBOOLE_1:26;
then A47: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A36,PSCOMP_1:102;
      M/.1 in L~M by A34,A35,JORDAN3:34;
   then L~g misses L~h by A32,A46,A47,Th1;
 hence contradiction by A24,A28,A40,A45,Th33;
end;

Lm10: LSeg(N-min L~f,NW-corner L~f) /\ LSeg(NE-corner L~f,E-max L~f) = {}
proof
 assume LSeg(N-min L~f,NW-corner L~f) /\ LSeg(NE-corner L~f,E-max L~f) <> {};
  then consider x being set such that
A1: x in LSeg(N-min L~f,NW-corner L~f) /\ LSeg(NE-corner L~f,E-max L~f)
                 by XBOOLE_0:def 1;
A2: x in LSeg(N-min L~f,NW-corner L~f) by A1,XBOOLE_0:def 3;
   reconsider p = x as Point of TOP-REAL 2 by A1;
A3: p in LSeg(NE-corner L~f,E-max L~f) by A1,XBOOLE_0:def 3;
     (NE-corner L~f)`1 = E-bound L~f & (E-max L~f)`1 = E-bound L~f
      by PSCOMP_1:76,104;
   then E-bound L~f <= p`1 & p`1 <= E-bound L~f by A3,TOPREAL1:9;
   then A4:  p`1 = E-bound L~f by AXIOMS:21;
    (NW-corner L~f)`1 <= (N-min L~f)`1 by PSCOMP_1:97;
  then A5: p`1 <= (N-min L~f)`1 by A2,TOPREAL1:9;
A6: (N-max L~f)`1 <= (NE-corner L~f)`1 by PSCOMP_1:97;
     (N-min L~f)`1 < (N-max L~f)`1 by Th55;
   then (N-min L~f)`1 < (NE-corner L~f)`1 by A6,AXIOMS:22;
 hence contradiction by A4,A5,PSCOMP_1:76;
end;

theorem
   z/.1 = N-min L~z implies (E-max L~z)..z < (E-min L~z)..z
proof set i1 = (E-max L~z)..z, i2 = (E-min L~z)..z, j = (S-max L~z)..z;
 assume that
A1: z/.1 = N-min L~z and
A2: i1 >= i2;
A3: E-max L~z in rng z by Th50;
A4: S-max L~z in rng z by Th46;
A5: E-min L~z in rng z by Th49;
A6: 1 in dom z by FINSEQ_5:6;
A7: i1 in dom z by A3,FINSEQ_4:30;
then A8: 1 <= i1 & i1 <= len z by FINSEQ_3:27;
A9: i2 in dom z by A5,FINSEQ_4:30;
then A10: 1 <= i2 & i2 <= len z by FINSEQ_3:27;
A11: z/.i2 = z.i2 by A9,FINSEQ_4:def 4
          .= E-min L~z by A5,FINSEQ_4:29;
A12:  z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
A13:  z/.i1 = z.i1 by A7,FINSEQ_4:def 4
          .= E-max L~z by A3,FINSEQ_4:29;
    (E-min L~z)`2 < (E-max L~z)`2 by Th57;
    then A14: i1 > i2 by A2,A11,A13,REAL_1:def 5;
then A15: i1 > 1 by A10,AXIOMS:22;
A16: j in dom z by A4,FINSEQ_4:30;
then A17: 1 <= j & j <= len z by FINSEQ_3:27;
A18: i2 < len z by A8,A14,AXIOMS:22;
A19: z/.j = z.j by A16,FINSEQ_4:def 4
          .= S-max L~z by A4,FINSEQ_4:29;
A20: i1 < j by A1,Lm9;
  then reconsider h = mid(z,j,i1) as S-Sequence_in_R2 by A15,A17,Th41;
A21: h is_in_the_area_of z by A7,A16,Th27;
      h/.1 = S-max L~z by A7,A16,A19,Th12;
then A22: (h/.1)`2 = S-bound L~z by PSCOMP_1:114;
A23: L~h c= L~z by A8,A17,JORDAN4:47;
A24: h/.len h = z/.i1 by A7,A16,Th13;
A25:  (N-min L~z)`1 < (N-max L~z)`1 by Th55;
A26: S-bound L~z < N-bound L~z by TOPREAL5:22;
    (N-min L~z)`2 = N-bound L~z & (S-max L~z)`2 = S-bound L~z by PSCOMP_1:94,
114
;
  then A27: j < len z by A12,A17,A19,A26,REAL_1:def 5;
    N-max L~z in L~z by SPRECT_1:13;
  then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:71;
  then (N-min L~z)`1 < E-bound L~z by A25,AXIOMS:22;
  then (N-min L~z)`1 < (E-min L~z)`1 by PSCOMP_1:104;
  then A28: i2 > 1 by A1,A10,A11,REAL_1:def 5;
 then reconsider M = mid(z,1,i2) as S-Sequence_in_R2 by A18,Th42;
A29: L~M misses L~h by A10,A14,A20,A27,Th52;
      1 <= len z by A10,AXIOMS:22;
then A30: L~M c= L~z by A10,JORDAN4:47;
A31: M/.len M = z/.i2 by A6,A9,Th13
          .= E-min L~z by A5,FINSEQ_5:41;
      len M = i2 -' 1 + 1 by A10,JORDAN4:20
         .= i2 by A10,AMI_5:4;
then A32: len M >= 1+1 by A28,NAT_1:38;
A33: len h >= 1 by A7,A16,Th9;
      len h <> 1 by A7,A16,A20,Th10;
    then len h > 1 by A33,REAL_1:def 5;
then A34: len h >= 1+1 by NAT_1:38;
A35: M/.1 = z/.1 by A6,A9,Th12;
A36: M is_in_the_area_of z by A6,A9,Th27;
A37: (M/.len M)`1 = E-bound L~z by A31,PSCOMP_1:104;
 per cases;
 suppose that
A38: NW-corner L~z = N-min L~z and
A39: NE-corner L~z = E-max L~z;
      (h/.len h)`2 = N-bound L~z by A13,A24,A39,PSCOMP_1:77;
then A40: h is_a_v.c._for z by A21,A22,Def3;
   (M/.1)`1 = W-bound L~z by A1,A35,A38,PSCOMP_1:74;
    then M is_a_h.c._for z by A36,A37,Def2;
 hence contradiction by A29,A32,A34,A40,Th33;
 suppose that
A41: NW-corner L~z <> N-min L~z and
A42: NE-corner L~z = E-max L~z;
      (h/.len h)`2 = N-bound L~z by A13,A24,A42,PSCOMP_1:77;
then A43: h is_a_v.c._for z by A21,A22,Def3;
  reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2
        by A1,A6,A9,A41,Th70;
A44:2 <= len g by TOPREAL1:def 10;
      <*NW-corner L~z*> is_in_the_area_of z by Th30;
then A45: g is_in_the_area_of z by A36,Th28;
      g/.1 = NW-corner L~z by FINSEQ_5:16;
then A46: (g/.1)`1 = W-bound L~z by PSCOMP_1:74;
A47:  len M in dom M by FINSEQ_5:6;
      len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35;
    then g/.len g = M/.len M by A47,GROUP_5:96
          .= z/.i2 by A6,A9,Th13
          .= E-min L~z by A5,FINSEQ_5:41;
    then (g/.len g)`1 = E-bound L~z by PSCOMP_1:104;
then A48: g is_a_h.c._for z by A45,A46,Def2;
A49:  L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20;
      LSeg(M/.1,NW-corner L~z) /\ L~h c=
           LSeg(M/.1,NW-corner L~z) /\ L~z by A23,XBOOLE_1:26;
then A50: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A35,PSCOMP_1:102;
      M/.1 in L~M by A32,JORDAN3:34;
   then L~g misses L~h by A29,A49,A50,Th1;
 hence contradiction by A34,A43,A44,A48,Th33;
 suppose that
A51: NW-corner L~z = N-min L~z and
A52: NE-corner L~z<> E-max L~z;
      M/.1 = z/.1 by A6,A9,Th12;
 then (M/.1)`1 = W-bound L~z by A1,A51,PSCOMP_1:74;
then A53: M is_a_h.c._for z by A36,A37,Def2;
  reconsider N = h^<*NE-corner L~z*> as S-Sequence_in_R2
        by A7,A13,A16,A52,Th69;
A54:len M >= 2 & len N >= 2 by TOPREAL1:def 10;
       <*NE-corner L~z*> is_in_the_area_of z by Th29;
then A55: N is_in_the_area_of z by A21,Th28;
      1 in dom h by FINSEQ_5:6;
then A56: (N/.1)`2 = S-bound L~z by A22,GROUP_5:95;
      len N = len h + len<*NE-corner L~z*> by FINSEQ_1:35
         .= len h + 1 by FINSEQ_1:56;
    then N/.len N = NE-corner L~z by TOPREAL4:1;
    then (N/.len N)`2 = N-bound L~z by PSCOMP_1:77;
then A57: N is_a_v.c._for z by A55,A56,Def3;
A58:  L~N = L~h \/ LSeg(NE-corner L~z,h/.len h) by SPPOL_2:19;
      LSeg(h/.len h,NE-corner L~z) /\ L~M c=
           LSeg(h/.len h,NE-corner L~z) /\ L~z by A30,XBOOLE_1:26;
then A59: LSeg(h/.len h,NE-corner L~z) /\ L~M c= {h/.len h} by A13,A24,PSCOMP_1
:112;
      h/.len h in L~h by A34,JORDAN3:34;
   then L~M misses L~N by A29,A58,A59,Th1;
 hence contradiction by A53,A54,A57,Th33;
 suppose that
A60: NW-corner L~z <> N-min L~z and
A61: NE-corner L~z <> E-max L~z;
  reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2
        by A1,A6,A9,A60,Th70;
      <*NW-corner L~z*> is_in_the_area_of z by Th30;
then A62: g is_in_the_area_of z by A36,Th28;
      g/.1 = NW-corner L~z by FINSEQ_5:16;
then A63: (g/.1)`1 = W-bound L~z by PSCOMP_1:74;
A64:  len M in dom M by FINSEQ_5:6;
      len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35;
    then g/.len g = M/.len M by A64,GROUP_5:96
          .= z/.i2 by A6,A9,Th13
          .= E-min L~z by A5,FINSEQ_5:41;
    then (g/.len g)`1 = E-bound L~z by PSCOMP_1:104;
then A65: g is_a_h.c._for z by A62,A63,Def2;
  reconsider N = h^<*NE-corner L~z*> as S-Sequence_in_R2
        by A7,A13,A16,A61,Th69;
A66:len g >= 2 & len N >= 2 by TOPREAL1:def 10;
       <*NE-corner L~z*> is_in_the_area_of z by Th29;
then A67: N is_in_the_area_of z by A21,Th28;
      1 in dom h by FINSEQ_5:6;
then A68: (N/.1)`2 = S-bound L~z by A22,GROUP_5:95;
      len N = len h + len<*NE-corner L~z*> by FINSEQ_1:35
         .= len h + 1 by FINSEQ_1:56;
    then N/.len N = NE-corner L~z by TOPREAL4:1;
    then (N/.len N)`2 = N-bound L~z by PSCOMP_1:77;
then A69: N is_a_v.c._for z by A67,A68,Def3;
A70:  L~N = L~h \/ LSeg(NE-corner L~z,h/.len h) by SPPOL_2:19;
      LSeg(h/.len h,NE-corner L~z) /\ L~M c=
           LSeg(h/.len h,NE-corner L~z) /\ L~z by A30,XBOOLE_1:26;
then A71: LSeg(h/.len h,NE-corner L~z) /\ L~M c= {h/.len h} by A13,A24,PSCOMP_1
:112;
      h/.len h in L~h by A34,JORDAN3:34;
then A72: L~M misses L~N by A29,A70,A71,Th1;
A73:  L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20;
      LSeg(M/.1,NW-corner L~z) /\ LSeg(NE-corner L~z,h/.len h) = {}
                       by A1,A13,A24,A35,Lm10;
    then LSeg(M/.1,NW-corner L~z) /\ L~N
      = LSeg(M/.1,NW-corner L~z) /\ L~h \/ {} by A70,XBOOLE_1:23
     .= LSeg(M/.1,NW-corner L~z) /\ L~h;
    then LSeg(M/.1,NW-corner L~z) /\ L~N c=
           LSeg(M/.1,NW-corner L~z) /\ L~z by A23,XBOOLE_1:26;
then A74: LSeg(M/.1,NW-corner L~z) /\ L~N c= {M/.1} by A1,A35,PSCOMP_1:102;
      M/.1 in L~M by A32,JORDAN3:34;
   then L~g misses L~N by A72,A73,A74,Th1;
 hence contradiction by A65,A66,A69,Th33;
end;

theorem Th76:
 z/.1 = N-min L~z & E-min L~z <> S-max L~z implies
  (E-min L~z)..z < (S-max L~z)..z
proof set i1 = (E-min L~z)..z, i2 = (S-max L~z)..z;
 assume that
A1: z/.1 = N-min L~z and
A2: E-min L~z <> S-max L~z and
A3: i1 >= i2;
A4: E-min L~z in rng z by Th49;
A5: S-max L~z in rng z by Th46;
A6: i1 in dom z by A4,FINSEQ_4:30;
then A7: 1 <= i1 & i1 <= len z by FINSEQ_3:27;
A8: i2 in dom z by A5,FINSEQ_4:30;
then A9: 1 <= i2 & i2 <= len z by FINSEQ_3:27;
A10: z/.i2 = z.i2 by A8,FINSEQ_4:def 4
          .= S-max L~z by A5,FINSEQ_4:29;
A11:  z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
A12:  z/.i1 = z.i1 by A6,FINSEQ_4:def 4
          .= E-min L~z by A4,FINSEQ_4:29;
    then A13: i1 > i2 by A2,A3,A10,REAL_1:def 5;
then A14: i1 > 1 by A9,AXIOMS:22;
A15: len z in dom z by FINSEQ_5:6;
A16: z/.1 = z/.len z by FINSEQ_6:def 1;
A17: 2 <= len z by SPPOL_1:2;
then A18: 2 in dom z by FINSEQ_3:27;
      z/.2 in N-most L~z by A1,Th34;
    then A19: (z/.2)`2 = (N-min L~z)`2 by PSCOMP_1:98
         .= N-bound L~z by PSCOMP_1:94;
A20: (z/.1)`2 = N-bound L~z by A1,PSCOMP_1:94;
A21: i2 <> 0 by A8,FINSEQ_3:27;
A22: (z/.i2)`2 = S-bound L~z by A10,PSCOMP_1:114;
      S-bound L~z < N-bound L~z by TOPREAL5:22;
    then A23: i2 > 2 by A19,A20,A21,A22,CQC_THE1:3;
  then reconsider h = mid(z,i2,2) as S-Sequence_in_R2 by A9,Th41;
A24: len h >= 2 by TOPREAL1:def 10;
A25: h is_in_the_area_of z by A8,A18,Th27;
      h/.1 = S-max L~z by A8,A10,A18,Th12;
then A26: (h/.1)`2 = S-bound L~z by PSCOMP_1:114;
A27: L~h c= L~z by A9,A17,JORDAN4:47;
      h/.len h = z/.2 by A8,A18,Th13;
    then A28: h is_a_v.c._for z by A19,A25,A26,Def3;
A29:  (N-min L~z)`1 < (N-max L~z)`1 by Th55;
    N-max L~z in L~z by SPRECT_1:13;
  then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:71;
  then (N-min L~z)`1 < E-bound L~z by A29,AXIOMS:22;
  then (N-min L~z)`1 < (E-min L~z)`1 by PSCOMP_1:104;
  then A30: i1 < len z by A7,A11,A12,REAL_1:def 5;
 then reconsider M = mid(z,len z,i1) as S-Sequence_in_R2 by A14,Th41;
A31: L~M misses L~h by A7,A13,A23,Th53;
A32: M/.len M = z/.i1 by A6,A15,Th13
          .= E-min L~z by A4,FINSEQ_5:41;
A33: len M = len z -' i1 + 1 by A7,JORDAN4:21;
      i1 + 1 <= len z by A30,NAT_1:38;
    then len z - i1 >= 1 by REAL_1:84;
    then len z -' i1 >= 1 by JORDAN3:1;
    then A34: len z -' i1 + 1 >= 1+1 by AXIOMS:24;
A35: M/.1 = z/.1 by A6,A15,A16,Th12;
 per cases;
 suppose that
A36: NW-corner L~z = N-min L~z;
A37: M is_in_the_area_of z by A6,A15,Th27;
      M/.1 = z/.len z by A6,A15,Th12;
then A38: (M/.1)`1 = W-bound L~z by A1,A16,A36,PSCOMP_1:74;
      (M/.len M)`1 = E-bound L~z by A32,PSCOMP_1:104;
    then M is_a_h.c._for z by A37,A38,Def2;
 hence contradiction by A24,A28,A31,A33,A34,Th33;
 suppose
   NW-corner L~z <> N-min L~z;
  then reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2
        by A1,A6,A15,A16,Th70;
A39: len g >= 2 by TOPREAL1:def 10;
A40: M is_in_the_area_of z by A6,A15,Th27;
      <*NW-corner L~z*> is_in_the_area_of z by Th30;
then A41: g is_in_the_area_of z by A40,Th28;
      g/.1 = NW-corner L~z by FINSEQ_5:16;
then A42: (g/.1)`1 = W-bound L~z by PSCOMP_1:74;
A43:  len M in dom M by FINSEQ_5:6;
      len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35;
    then g/.len g = M/.len M by A43,GROUP_5:96
          .= z/.i1 by A6,A15,Th13
          .= E-min L~z by A4,FINSEQ_5:41;
    then (g/.len g)`1 = E-bound L~z by PSCOMP_1:104;
then A44: g is_a_h.c._for z by A41,A42,Def2;
A45:  L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20;
      LSeg(M/.1,NW-corner L~z) /\ L~h c=
           LSeg(M/.1,NW-corner L~z) /\ L~z by A27,XBOOLE_1:26;
then A46: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A35,PSCOMP_1:102;
      M/.1 in L~M by A33,A34,JORDAN3:34;
   then L~g misses L~h by A31,A45,A46,Th1;
 hence contradiction by A24,A28,A39,A44,Th33;
end;

theorem Th77:
 z/.1 = N-min L~z implies (S-max L~z)..z < (S-min L~z)..z
proof set i1 = (S-max L~z)..z, i2 = (S-min L~z)..z, j = (N-max L~z)..z;
 assume that
A1: z/.1 = N-min L~z and
A2: i1 >= i2;
A3: N-max L~z in rng z by Th44;
A4: S-min L~z in rng z by Th45;
A5: S-max L~z in rng z by Th46;
then A6: i1 in dom z by FINSEQ_4:30;
then A7: 1 <= i1 & i1 <= len z by FINSEQ_3:27;
A8: i2 in dom z by A4,FINSEQ_4:30;
then A9: 1 <= i2 & i2 <= len z by FINSEQ_3:27;
A10: z/.i2 = z.i2 by A8,FINSEQ_4:def 4
          .= S-min L~z by A4,FINSEQ_4:29;
A11:  z/.i1 = z.i1 by A6,FINSEQ_4:def 4
          .= S-max L~z by A5,FINSEQ_4:29;
      S-min L~z <> S-max L~z by Th60;
    then A12: i1 > i2 by A2,A10,A11,REAL_1:def 5;
A13: z/.1 = z/.len z by FINSEQ_6:def 1;
      (N-min L~z)`2 = N-bound L~z & (S-max L~z)`2 = S-bound L~z
             by PSCOMP_1:94,114;
    then N-min L~z <> S-max L~z by TOPREAL5:22;
then A14: i1 < len z by A1,A7,A11,A13,REAL_1:def 5;
A15: len z in dom z by FINSEQ_5:6;
A16: j in dom z by A3,FINSEQ_4:30;
then A17: 1 <= j & j <= len z by FINSEQ_3:27;
A18: z/.j = z.j by A16,FINSEQ_4:def 4
          .= N-max L~z by A3,FINSEQ_4:29;
then A19: (z/.j)`2 = N-bound L~z by PSCOMP_1:94;
A20: i2 > j by A1,Lm8;
      N-min L~z <> N-max L~z by Th56;
    then A21: 1 < j by A1,A17,A18,REAL_1:def 5;
  then reconsider h = mid(z,i2,j) as S-Sequence_in_R2 by A9,A20,Th41;
A22: len h >= 2 by TOPREAL1:def 10;
A23: h is_in_the_area_of z by A8,A16,Th27;
      h/.1 = S-min L~z by A8,A10,A16,Th12;
then A24: (h/.1)`2 = S-bound L~z by PSCOMP_1:114;
A25: L~h c= L~z by A9,A17,JORDAN4:47;
      h/.len h = z/.j by A8,A16,Th13;
    then A26: h is_a_v.c._for z by A19,A23,A24,Def3;
      j < i1 by A1,Lm7;
 then i1 > 1 by A17,AXIOMS:22;
 then reconsider M = mid(z,len z,i1) as S-Sequence_in_R2 by A14,Th41;
A27: L~h misses L~M by A7,A12,A20,A21,Th53;
A28: M/.len M = S-max L~z by A6,A11,A15,Th13;
A29: len M = len z -' i1 + 1 by A7,JORDAN4:21;
      i1 + 1 <= len z by A14,NAT_1:38;
    then len z - i1 >= 1 by REAL_1:84;
    then len z -' i1 >= 1 by JORDAN3:1;
    then A30: len z -' i1 + 1 >= 1+1 by AXIOMS:24;
then A31: M/.len M in L~M by A29,JORDAN3:34;
A32: 1 in dom M by FINSEQ_5:6;
A33: M/.1 = z/.len z by A6,A15,Th12;
 per cases;
 suppose that
A34: NW-corner L~z = N-min L~z and
A35: SE-corner L~z = S-max L~z;
A36: M is_in_the_area_of z by A6,A15,Th27;
A37: (M/.1)`1 = W-bound L~z by A1,A13,A33,A34,PSCOMP_1:74;
      (M/.len M)`1 = E-bound L~z by A28,A35,PSCOMP_1:78;
    then M is_a_h.c._for z by A36,A37,Def2;
 hence contradiction by A22,A26,A27,A29,A30,Th33;
 suppose that
A38: NW-corner L~z = N-min L~z and
A39: SE-corner L~z <> S-max L~z;
  reconsider g = M^<*SE-corner L~z*> as S-Sequence_in_R2
   by A6,A11,A15,A39,Th68;
A40: len g >= 2 by TOPREAL1:def 10;
A41: M is_in_the_area_of z by A6,A15,Th27;
      <*SE-corner L~z*> is_in_the_area_of z by Th31;
then A42: g is_in_the_area_of z by A41,Th28;
      g/.1 = M/.1 by A32,GROUP_5:95
       .= z/.1 by A6,A13,A15,Th12;
then A43: (g/.1)`1 = W-bound L~z by A1,A38,PSCOMP_1:74;
      len g = len M + len<*SE-corner L~z*> by FINSEQ_1:35
         .= len M + 1 by FINSEQ_1:56;
    then g/.len g = SE-corner L~z by TOPREAL4:1;
    then (g/.len g)`1 = E-bound L~z by PSCOMP_1:78;
then A44: g is_a_h.c._for z by A42,A43,Def2;
A45:  L~g = L~M \/ LSeg(M/.len M,SE-corner L~z) by SPPOL_2:19;
      LSeg(M/.len M,SE-corner L~z) /\ L~h c=
           LSeg(M/.len M,SE-corner L~z) /\ L~z by A25,XBOOLE_1:26;
 then LSeg(M/.len M,SE-corner L~z) /\ L~h c= {M/.len M} by A28,PSCOMP_1:122;
   then L~g misses L~h by A27,A31,A45,Th1;
 hence contradiction by A22,A26,A40,A44,Th33;
 suppose that
A46: NW-corner L~z <> N-min L~z and
A47: SE-corner L~z = S-max L~z;
  reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2
        by A1,A6,A13,A15,A46,Th70;
A48: len g >= 2 by TOPREAL1:def 10;
A49: M is_in_the_area_of z by A6,A15,Th27;
      <*NW-corner L~z*> is_in_the_area_of z by Th30;
then A50: g is_in_the_area_of z by A49,Th28;
      g/.1 = NW-corner L~z by FINSEQ_5:16;
then A51: (g/.1)`1 = W-bound L~z by PSCOMP_1:74;
A52:  len M in dom M by FINSEQ_5:6;
      len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35;
    then g/.len g = M/.len M by A52,GROUP_5:96
          .= S-max L~z by A6,A11,A15,Th13;
    then (g/.len g)`1 = E-bound L~z by A47,PSCOMP_1:78;
then A53: g is_a_h.c._for z by A50,A51,Def2;
A54:  L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20;
      LSeg(M/.1,NW-corner L~z) /\ L~h c=
           LSeg(M/.1,NW-corner L~z) /\ L~z by A25,XBOOLE_1:26;
then A55: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A13,A33,PSCOMP_1:102;
      M/.1 in L~M by A29,A30,JORDAN3:34;
   then L~g misses L~h by A27,A54,A55,Th1;
 hence contradiction by A22,A26,A48,A53,Th33;
 suppose that
A56: NW-corner L~z <> N-min L~z and
A57: SE-corner L~z <> S-max L~z;
  set K = <*NW-corner L~z*>^M;
  reconsider g = K^<*SE-corner L~z*>
      as S-Sequence_in_R2 by A1,A6,A11,A13,A15,A56,A57,Lm5;
A58: len g >= 2 by TOPREAL1:def 10;
A59: M is_in_the_area_of z by A6,A15,Th27;
      <*NW-corner L~z*> is_in_the_area_of z by Th30;
then A60: <*NW-corner L~z*>^M is_in_the_area_of z by A59,Th28;
      <*SE-corner L~z*> is_in_the_area_of z by Th31;
then A61: g is_in_the_area_of z by A60,Th28;
      1 in dom(<*NW-corner L~z*>^M) by FINSEQ_5:6;
    then g/.1 = (<*NW-corner L~z*>^M)/.1 by GROUP_5:95
       .= NW-corner L~z by FINSEQ_5:16;
then A62: (g/.1)`1 = W-bound L~z by PSCOMP_1:74;
      len g = len(<*NW-corner L~z*>^M) + len<*SE-corner L~z*>
           by FINSEQ_1:35
         .= len(<*NW-corner L~z*>^M) + 1 by FINSEQ_1:56;
    then g/.len g = SE-corner L~z by TOPREAL4:1;
    then (g/.len g)`1 = E-bound L~z by PSCOMP_1:78;
then A63: g is_a_h.c._for z by A61,A62,Def2;
A64:  L~K = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20;
      LSeg(M/.1,NW-corner L~z) /\ L~h c=
           LSeg(M/.1,NW-corner L~z) /\ L~z by A25,XBOOLE_1:26;
then A65: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A13,A33,PSCOMP_1:102;
      M/.1 in L~M by A29,A30,JORDAN3:34;
then A66: L~K misses L~h by A27,A64,A65,Th1;
      len K = len M + len<*NW-corner L~z*> by FINSEQ_1:35;
    then len K >= len M by NAT_1:29;
     then len K >= 2 by A29,A30,AXIOMS:22;
then A67: K/.len K in L~K by JORDAN3:34;
A68:  L~g = L~K \/ LSeg(K/.len K,SE-corner L~z) by SPPOL_2:19;
A69:  len M in dom M by FINSEQ_5:6;
      len K = len M + len<*NW-corner L~z*> by FINSEQ_1:35;
    then A70: K/.len K = M/.len M by A69,GROUP_5:96
          .= z/.i1 by A6,A15,Th13
          .= S-max L~z by A5,FINSEQ_5:41;
      LSeg(K/.len K,SE-corner L~z) /\ L~h c=
           LSeg(K/.len K,SE-corner L~z) /\ L~z by A25,XBOOLE_1:26;
 then LSeg(K/.len K,SE-corner L~z) /\ L~h c= {K/.len K} by A70,PSCOMP_1:122;
   then L~g misses L~h by A66,A67,A68,Th1;
 hence contradiction by A22,A26,A58,A63,Th33;
end;

Lm11:
 z/.1 = N-min L~z implies (E-min L~z)..z < (S-min L~z)..z
proof assume
A1: z/.1 = N-min L~z;
  then A2: (E-min L~z)..z <= (S-max L~z)..z by Th76;
    (S-max L~z)..z < (S-min L~z)..z by A1,Th77;
 hence (E-min L~z)..z < (S-min L~z)..z by A2,AXIOMS:22;
end;

Lm12:
 z/.1 = N-min L~z & N-min L~z <> W-max L~z implies
  (E-min L~z)..z < (W-max L~z)..z
proof set i1 = (E-min L~z)..z, i2 = (W-max L~z)..z, j = (S-min L~z)..z;
 assume that
A1: z/.1 = N-min L~z and
A2: N-min L~z <> W-max L~z and
A3: i1 >= i2;
A4: E-min L~z in rng z by Th49;
A5: S-min L~z in rng z by Th45;
A6: W-max L~z in rng z by Th48;
A7: i1 in dom z by A4,FINSEQ_4:30;
then A8: 1 <= i1 & i1 <= len z by FINSEQ_3:27;
A9: i2 in dom z by A6,FINSEQ_4:30;
then A10: 1 <= i2 & i2 <= len z by FINSEQ_3:27;
A11: z/.i2 = z.i2 by A9,FINSEQ_4:def 4
          .= W-max L~z by A6,FINSEQ_4:29;
A12:  z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
A13:  z/.i1 = z.i1 by A7,FINSEQ_4:def 4
          .= E-min L~z by A4,FINSEQ_4:29;
      (W-max L~z)`1 = W-bound L~z & (E-min L~z)`1 = E-bound L~z
       by PSCOMP_1:84,104;
    then (W-max L~z)`1 < (E-min L~z)`1 by TOPREAL5:23;
    then A14: i1 > i2 by A3,A11,A13,REAL_1:def 5;
then A15: i1 > 1 by A10,AXIOMS:22;
A16: len z in dom z by FINSEQ_5:6;
A17: j in dom z by A5,FINSEQ_4:30;
then A18: 1 <= j & j <= len z by FINSEQ_3:27;
A19: z/.j = z.j by A17,FINSEQ_4:def 4
          .= S-min L~z by A5,FINSEQ_4:29;
A20: i2 > 1 by A1,A2,A10,A11,REAL_1:def 5;
A21: z/.j = z.j by A17,FINSEQ_4:def 4
       .= S-min L~z by A5,FINSEQ_4:29;
    (N-min L~z)`2 = N-bound L~z & (S-min L~z)`2 = S-bound L~z by PSCOMP_1:94,
114
;
  then N-min L~z <> S-min L~z by TOPREAL5:22;
  then A22: j < len z by A12,A18,A21,REAL_1:def 5;
A23: i1 < j by A1,Lm11;
  then j > 1 by A15,AXIOMS:22;
  then reconsider h = mid(z,j,len z) as S-Sequence_in_R2 by A22,Th42;
A24: len h >= 2 by TOPREAL1:def 10;
A25: h is_in_the_area_of z by A16,A17,Th27;
      h/.1 = S-min L~z by A16,A17,A19,Th12;
then A26: (h/.1)`2 = S-bound L~z by PSCOMP_1:114;
      h/.len h = z/.len z by A16,A17,Th13;
    then (h/.len h)`2 = N-bound L~z by A12,PSCOMP_1:94;
then A27: h is_a_v.c._for z by A25,A26,Def3;
A28:  (N-min L~z)`1 < (N-max L~z)`1 by Th55;
    N-max L~z in L~z by SPRECT_1:13;
  then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:71;
  then (N-min L~z)`1 < E-bound L~z by A28,AXIOMS:22;
  then (N-min L~z)`1 < (E-min L~z)`1 by PSCOMP_1:104;
  then i1 < len z by A8,A12,A13,REAL_1:def 5;
 then reconsider M = mid(z,i2,i1) as S-Sequence_in_R2 by A10,A14,Th42;
A29: len M >= 2 by TOPREAL1:def 10;
A30: M/.len M = z/.i1 by A7,A9,Th13
          .= E-min L~z by A4,FINSEQ_5:41;
A31: M/.1 = W-max L~z by A7,A9,A11,Th12;
A32: M is_in_the_area_of z by A7,A9,Th27;
A33: (M/.1)`1 = W-bound L~z by A31,PSCOMP_1:84;
      (M/.len M)`1 = E-bound L~z by A30,PSCOMP_1:104;
then A34: M is_a_h.c._for z by A32,A33,Def2;
      L~M misses L~h by A3,A18,A20,A23,Th51;
 hence contradiction by A24,A27,A29,A34,Th33;
end;

Lm13:
 z/.1 = N-min L~z implies (E-min L~z)..z < (W-min L~z)..z
proof set i1 = (E-min L~z)..z, i2 = (W-min L~z)..z, j = (S-min L~z)..z;
 assume that
A1: z/.1 = N-min L~z and
A2: i1 >= i2;
A3: E-min L~z in rng z by Th49;
A4: S-min L~z in rng z by Th45;
A5: W-min L~z in rng z by Th47;
A6: i1 in dom z by A3,FINSEQ_4:30;
then A7: 1 <= i1 & i1 <= len z by FINSEQ_3:27;
A8: i2 in dom z by A5,FINSEQ_4:30;
then A9: 1 <= i2 & i2 <= len z by FINSEQ_3:27;
A10: z/.i2 = z.i2 by A8,FINSEQ_4:def 4
          .= W-min L~z by A5,FINSEQ_4:29;
A11:  z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
A12:  z/.i1 = z.i1 by A6,FINSEQ_4:def 4
          .= E-min L~z by A3,FINSEQ_4:29;
      (W-min L~z)`1 = W-bound L~z & (E-min L~z)`1 = E-bound L~z
       by PSCOMP_1:84,104;
    then z/.i1 <> z/.i2 by A10,A12,TOPREAL5:23;
then A13: i1 > i2 by A2,REAL_1:def 5;
then A14: i1 > 1 by A9,AXIOMS:22;
A15: len z in dom z by FINSEQ_5:6;
A16: j in dom z by A4,FINSEQ_4:30;
then A17: 1 <= j & j <= len z by FINSEQ_3:27;
A18: z/.j = z.j by A16,FINSEQ_4:def 4
          .= S-min L~z by A4,FINSEQ_4:29;
      W-max L~z in L~z & (N-min L~z)`2 = N-bound L~z by PSCOMP_1:94,SPRECT_1:15
;
    then (W-max L~z)`2 <= (N-min L~z)`2 by PSCOMP_1:71;
then N-min L~z <> W-min L~z by Th61;
then A19: i2 > 1 by A1,A9,A10,REAL_1:def 5;
A20: z/.j = z.j by A16,FINSEQ_4:def 4
       .= S-min L~z by A4,FINSEQ_4:29;
    (N-min L~z)`2 = N-bound L~z & (S-min L~z)`2 = S-bound L~z by PSCOMP_1:94,
114
;
  then N-min L~z <> S-min L~z by TOPREAL5:22;
  then A21: j < len z by A11,A17,A20,REAL_1:def 5;
A22: i1 < j by A1,Lm11;
  then j > 1 by A14,AXIOMS:22;
  then reconsider h = mid(z,j,len z) as S-Sequence_in_R2 by A21,Th42;
A23: h is_in_the_area_of z by A15,A16,Th27;
      h/.1 = S-min L~z by A15,A16,A18,Th12;
then A24: (h/.1)`2 = S-bound L~z by PSCOMP_1:114;
      h/.len h = z/.len z by A15,A16,Th13;
    then (h/.len h)`2 = N-bound L~z by A11,PSCOMP_1:94;
then A25: h is_a_v.c._for z by A23,A24,Def3;
A26:  (N-min L~z)`1 < (N-max L~z)`1 by Th55;
    N-max L~z in L~z by SPRECT_1:13;
  then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:71;
  then (N-min L~z)`1 < E-bound L~z by A26,AXIOMS:22;
  then (N-min L~z)`1 < (E-min L~z)`1 by PSCOMP_1:104;
  then i1 < len z by A7,A11,A12,REAL_1:def 5;
 then reconsider M = mid(z,i2,i1) as S-Sequence_in_R2 by A9,A13,Th42;
A27: len h >= 2 & len M >= 2 by TOPREAL1:def 10;
A28: M/.len M = z/.i1 by A6,A8,Th13
          .= E-min L~z by A3,FINSEQ_5:41;
A29: M/.1 = W-min L~z by A6,A8,A10,Th12;
A30: M is_in_the_area_of z by A6,A8,Th27;
A31: (M/.1)`1 = W-bound L~z by A29,PSCOMP_1:84;
      (M/.len M)`1 = E-bound L~z by A28,PSCOMP_1:104;
then A32: M is_a_h.c._for z by A30,A31,Def2;
      L~M misses L~h by A2,A17,A19,A22,Th51;
 hence contradiction by A25,A27,A32,Th33;
end;

theorem
   z/.1 = N-min L~z & S-min L~z <> W-min L~z implies
  (S-min L~z)..z < (W-min L~z)..z
proof set i1 = (E-min L~z)..z, i2 = (W-min L~z)..z, j = (S-min L~z)..z;
 assume that
A1: z/.1 = N-min L~z and
A2: S-min L~z <> W-min L~z and
A3: j >= i2;
A4: i1 < i2 by A1,Lm13;
A5: E-min L~z in rng z by Th49;
A6: S-min L~z in rng z by Th45;
A7: W-min L~z in rng z by Th47;
A8: i1 in dom z by A5,FINSEQ_4:30;
then A9: 1 <= i1 & i1 <= len z by FINSEQ_3:27;
A10: i2 in dom z by A7,FINSEQ_4:30;
then A11: 1 <= i2 & i2 <= len z by FINSEQ_3:27;
A12: z/.i2 = z.i2 by A10,FINSEQ_4:def 4
          .= W-min L~z by A7,FINSEQ_4:29;
A13:  z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
A14: j in dom z by A6,FINSEQ_4:30;
then A15: z/.j = z.j by FINSEQ_4:def 4
          .= S-min L~z by A6,FINSEQ_4:29;
A16:  z/.i1 = z.i1 by A8,FINSEQ_4:def 4
          .= E-min L~z by A5,FINSEQ_4:29;
A17: j > i2 by A2,A3,A12,A15,REAL_1:def 5;
A18:  (N-min L~z)`1 < (N-max L~z)`1 by Th55;
    N-max L~z in L~z by SPRECT_1:13;
  then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:71;
  then (N-min L~z)`1 < E-bound L~z by A18,AXIOMS:22;
  then (N-min L~z)`1 < (E-min L~z)`1 by PSCOMP_1:104;
  then A19: i1 > 1 by A1,A9,A16,REAL_1:def 5;
A20: len z in dom z by FINSEQ_5:6;
A21: 1 <= j & j <= len z by A14,FINSEQ_3:27;
A22: z/.j = z.j by A14,FINSEQ_4:def 4
       .= S-min L~z by A6,FINSEQ_4:29;
    (N-min L~z)`2 = N-bound L~z & (S-min L~z)`2 = S-bound L~z by PSCOMP_1:94,
114
;
  then N-min L~z <> S-min L~z by TOPREAL5:22;
  then A23: j < len z by A13,A21,A22,REAL_1:def 5;
      i1 < j by A1,Lm11;
  then j > 1 by A9,AXIOMS:22;
  then reconsider h = mid(z,j,len z) as S-Sequence_in_R2 by A23,Th42;
A24: h is_in_the_area_of z by A14,A20,Th27;
      h/.1 = S-min L~z by A14,A15,A20,Th12;
then A25: (h/.1)`2 = S-bound L~z by PSCOMP_1:114;
      h/.len h = z/.len z by A14,A20,Th13;
    then (h/.len h)`2 = N-bound L~z by A13,PSCOMP_1:94;
then A26: h is_a_v.c._for z by A24,A25,Def3;
 reconsider M = mid(z,i2,i1) as S-Sequence_in_R2 by A4,A11,A19,Th41;
A27: len h >= 2 & len M >= 2 by TOPREAL1:def 10;
A28: L~M misses L~h by A4,A17,A19,A21,Th54;
A29: M/.len M = z/.i1 by A8,A10,Th13
          .= E-min L~z by A5,FINSEQ_5:41;
A30: M/.1 = W-min L~z by A8,A10,A12,Th12;
A31: M is_in_the_area_of z by A8,A10,Th27;
A32: (M/.1)`1 = W-bound L~z by A30,PSCOMP_1:84;
      (M/.len M)`1 = E-bound L~z by A29,PSCOMP_1:104;
    then M is_a_h.c._for z by A31,A32,Def2;
 hence contradiction by A26,A27,A28,Th33;
end;

theorem Th79:
 z/.1 = N-min L~z & N-min L~z <> W-max L~z
  implies (W-min L~z)..z < (W-max L~z)..z
proof set i1 = (W-min L~z)..z, i2 = (W-max L~z)..z, j = (E-min L~z)..z;
 assume that
A1: z/.1 = N-min L~z and
A2: N-min L~z <> W-max L~z and
A3: i1 >= i2;
A4: E-min L~z in rng z by Th49;
A5: W-max L~z in rng z by Th48;
A6: W-min L~z in rng z by Th47;
then A7: i1 in dom z by FINSEQ_4:30;
then A8: 1 <= i1 & i1 <= len z by FINSEQ_3:27;
A9: i2 in dom z by A5,FINSEQ_4:30;
then A10: 1 <= i2 & i2 <= len z by FINSEQ_3:27;
A11: z/.i2 = z.i2 by A9,FINSEQ_4:def 4
          .= W-max L~z by A5,FINSEQ_4:29;
A12:  z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
A13:  z/.i1 = z.i1 by A7,FINSEQ_4:def 4
          .= W-min L~z by A6,FINSEQ_4:29;
      W-max L~z <> W-min L~z by Th62;
    then A14: i1 > i2 by A3,A11,A13,REAL_1:def 5;
A15: z/.1 = z/.len z by FINSEQ_6:def 1;
      W-max L~z in L~z & (N-min L~z)`2 = N-bound L~z by PSCOMP_1:94,SPRECT_1:15
;
    then (W-max L~z)`2 <= (N-min L~z)`2 by PSCOMP_1:71;
    then N-min L~z <> W-min L~z by Th61;
    then A16: i1 < len z by A1,A8,A13,A15,REAL_1:def 5;
A17: len z in dom z by FINSEQ_5:6;
A18: j in dom z by A4,FINSEQ_4:30;
then A19: 1 <= j & j <= len z by FINSEQ_3:27;
A20: z/.j = z.j by A18,FINSEQ_4:def 4
          .= E-min L~z by A4,FINSEQ_4:29;
then A21: (z/.j)`1 = E-bound L~z by PSCOMP_1:104;
A22: i2 > j by A1,A2,Lm12;
A23:  (N-min L~z)`1 < (N-max L~z)`1 by Th55;
    N-max L~z in L~z by SPRECT_1:13;
  then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:71;
  then (N-min L~z)`1 < E-bound L~z by A23,AXIOMS:22;
  then (N-min L~z)`1 < (E-min L~z)`1 by PSCOMP_1:104;
  then A24: 1 < j by A1,A19,A20,REAL_1:def 5;
  then reconsider h = mid(z,i2,j) as S-Sequence_in_R2 by A10,A22,Th41;
A25: len h >= 2 by TOPREAL1:def 10;
A26: h is_in_the_area_of z by A9,A18,Th27;
      h/.1 = W-max L~z by A9,A11,A18,Th12;
then A27: (h/.1)`1 = W-bound L~z by PSCOMP_1:84;
A28: L~h c= L~z by A10,A19,JORDAN4:47;
      h/.len h = z/.j by A9,A18,Th13;
    then A29: h is_a_h.c._for z by A21,A26,A27,Def2;
      j < i1 by A1,Lm13;
 then i1 > 1 by A19,AXIOMS:22;
 then reconsider M = mid(z,i1,len z) as S-Sequence_in_R2 by A16,Th42;
A30: L~M misses L~h by A8,A14,A22,A24,Th54;
A31: len M = len z -' i1 + 1 by A8,JORDAN4:20;
      i1 + 1 <= len z by A16,NAT_1:38;
    then len z - i1 >= 1 by REAL_1:84;
    then len z -' i1 >= 1 by JORDAN3:1;
    then A32: len z -' i1 + 1 >= 1+1 by AXIOMS:24;
A33: M/.1 = z/.i1 by A7,A17,Th12;
A34: M/.len M = z/.len z by A7,A17,Th13;
A35: M is_in_the_area_of z by A7,A17,Th27;
 per cases;
 suppose
   SW-corner L~z = W-min L~z;
then A36: (M/.1)`2 = S-bound L~z by A13,A33,PSCOMP_1:73;
      (M/.len M)`2 = N-bound L~z by A12,A34,PSCOMP_1:94;
    then M is_a_v.c._for z by A35,A36,Def3;
 hence contradiction by A25,A29,A30,A31,A32,Th33;
 suppose
   SW-corner L~z <> W-min L~z;
  then reconsider g = <*SW-corner L~z*>^M as S-Sequence_in_R2
        by A7,A13,A17,Th71;
A37: len g >= 2 by TOPREAL1:def 10;
      <*SW-corner L~z*> is_in_the_area_of z by Th32;
then A38: g is_in_the_area_of z by A35,Th28;
      g/.1 = SW-corner L~z by FINSEQ_5:16;
then A39: (g/.1)`2 = S-bound L~z by PSCOMP_1:73;
A40:  len M in dom M by FINSEQ_5:6;
      len g = len M + len<*SW-corner L~z*> by FINSEQ_1:35;
    then g/.len g = M/.len M by A40,GROUP_5:96;
    then (g/.len g)`2 = N-bound L~z by A12,A34,PSCOMP_1:94;
then A41: g is_a_v.c._for z by A38,A39,Def3;
A42:  L~g = L~M \/ LSeg(SW-corner L~z,M/.1) by SPPOL_2:20;
      LSeg(M/.1,SW-corner L~z) /\ L~h c=
           LSeg(M/.1,SW-corner L~z) /\ L~z by A28,XBOOLE_1:26;
then A43: LSeg(M/.1,SW-corner L~z) /\ L~h c= {M/.1} by A13,A33,PSCOMP_1:92;
      M/.1 in L~M by A31,A32,JORDAN3:34;
   then L~g misses L~h by A30,A42,A43,Th1;
 hence contradiction by A25,A29,A37,A41,Th33;
end;

theorem
   z/.1 = N-min L~z implies (W-min L~z)..z < len z
proof
A1: W-min L~z in rng z by Th47;
A2: W-max L~z in rng z by Th48;
 assume
A3:  z/.1 = N-min L~z;
 per cases;
 suppose
A4:  N-min L~z = W-max L~z;
A5: (W-min L~z)..z in dom z by A1,FINSEQ_4:30;
  then A6: (W-min L~z)..z <= len z by FINSEQ_3:27;
A7: z/.((W-min L~z)..z) = z.((W-min L~z)..z) by A5,FINSEQ_4:def 4
         .= W-min L~z by A1,FINSEQ_4:29;
   z/.len z = W-max L~z by A3,A4,FINSEQ_6:def 1;
  then (W-min L~z)..z <> len z by A7,Th62;
 hence thesis by A6,REAL_1:def 5;
 suppose N-min L~z <> W-max L~z;
  then A8: (W-min L~z)..z < (W-max L~z)..z by A3,Th79;
    (W-max L~z)..z in dom z by A2,FINSEQ_4:30;
  then (W-max L~z)..z <= len z by FINSEQ_3:27;
 hence thesis by A8,AXIOMS:22;
end;

theorem
   f/.1 = N-min L~f implies (W-max L~f)..f < len f
proof
A1: W-max L~f in rng f by Th48;
 assume
A2: f/.1 = N-min L~f;
  then A3: f/.len f = N-min L~f by FINSEQ_6:def 1;
    (W-max L~f)..f in dom f by A1,FINSEQ_4:30;
then A4: f/.((W-max L~f)..f) = f.((W-max L~f)..f) by FINSEQ_4:def 4
       .= W-max L~f by A1,FINSEQ_4:29;
 per cases;
 suppose N-min L~f = W-max L~f;
   then A5:  (W-max L~f)..f = 1 by A2,FINSEQ_6:47;
     len f > 4 by GOBOARD7:36;
  hence thesis by A5,AXIOMS:22;
 suppose A6: N-min L~f <> W-max L~f;
    (W-max L~f)..f <= len f by A1,FINSEQ_4:31;
 hence (W-max L~f)..f < len f by A3,A4,A6,REAL_1:def 5;
end;


Back to top