:: Properties of Left-, and Right Components
::  by Artur Korni{\l}owicz
::
:: Received May 5, 1999
:: Copyright (c) 1999-2016 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, FUNCT_1, GOBOARD5, SPRECT_2, PRE_TOPC, EUCLID,
      RCOMP_1, SPPOL_1, GOBOARD1, STRUCT_0, JORDAN2C, TOPREAL1, REAL_1,
      XXREAL_0, CARD_1, METRIC_1, TARSKI, XXREAL_2, ARYTM_3, XBOOLE_0,
      COMPLEX1, RELAT_2, CONNSP_1, FINSEQ_1, TREES_1, CARD_3, FUNCOP_1,
      XXREAL_1, RELAT_1, MCART_1, MATRIX_1, ARYTM_1, SQUARE_1, JORDAN8, NEWTON,
      PSCOMP_1, INT_1, POWER, GOBOARD9, RLTOPSP1, GOBOARD2, PARTFUN1, TOPS_1,
      JORDAN1, FINSEQ_6, SPRECT_1, SEQ_4, FINSEQ_2, NAT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
      BINOP_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1,
      XXREAL_0, XXREAL_2, SQUARE_1, NAT_1, INT_1, INT_2, NEWTON, POWER,
      MATRIX_0, NAT_D, MATRIX_1, FUNCT_4, SEQ_4, METRIC_1, TBSP_1, FINSEQ_1,
      CARD_3, FINSEQ_2, FINSEQ_6, STRUCT_0, RCOMP_1, PRE_TOPC, TOPS_1,
      CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2,
      GOBOARD5, GOBOARD9, PSCOMP_1, SPPOL_1, SPRECT_1, SPRECT_2, JORDAN2C,
      JORDAN8, TOPREAL6;
 constructors FUNCT_4, REAL_1, SQUARE_1, RCOMP_1, NEWTON, POWER, NAT_D, TOPS_1,
      CONNSP_1, COMPTS_1, TBSP_1, MONOID_0, TOPREAL4, GOBOARD2, SPPOL_1,
      JORDAN1, PSCOMP_1, GOBOARD9, SPRECT_1, SPRECT_2, JORDAN2C, TOPREAL6,
      JORDAN8, GOBOARD1, SEQ_4, RELSET_1, CONVEX1, BINOP_2, MATRIX_1, BINOP_1;
 registrations SUBSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_6,
      STRUCT_0, PRE_TOPC, TOPS_1, MONOID_0, EUCLID, GOBOARD2, GOBRD11,
      SPRECT_1, SPRECT_3, JORDAN2C, REVROT_1, TOPREAL6, FUNCT_1, FINSEQ_1,
      PSCOMP_1, RELSET_1, JORDAN5A, NEWTON, SQUARE_1, ORDINAL1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, JORDAN2C, SPRECT_1, XBOOLE_0;
 equalities JORDAN2C, XBOOLE_0, SQUARE_1, SUBSET_1, EUCLID;
 expansions TARSKI, JORDAN2C, XBOOLE_0;
 theorems ABSVALUE, CARD_3, FUNCT_4, COMPTS_1, CONNSP_1, EUCLID, FINSEQ_1,
      FUNCT_1, FUNCT_2, GOBOARD5, GOBOARD6, GOBOARD7, GOBOARD9, GOBRD11,
      GOBRD12, INT_1, JORDAN2C, JORDAN8, METRIC_1, NAT_1, POWER, PRE_TOPC,
      PRE_FF, PSCOMP_1, RCOMP_1, RELAT_1, SEQ_4, SPRECT_1, SPRECT_3, SPRECT_4,
      SQUARE_1, SPPOL_2, SUBSET_1, TARSKI, TBSP_1, TDLAT_1, TOPREAL1, TOPREAL3,
      TOPREAL6, TOPS_1, SPRECT_2, REVROT_1, FINSEQ_6, XBOOLE_0, XBOOLE_1,
      XREAL_0, XCMPLX_1, COMPLEX1, XREAL_1, NEWTON, XXREAL_0, FINSEQ_2,
      MATRIX_0, XXREAL_1, NAT_D, RLTOPSP1;

begin  :: Components

reserve i, j, n for Nat,
  f for non constant standard special_circular_sequence,
  g for clockwise_oriented non constant standard special_circular_sequence,
  p, q for Point of TOP-REAL 2,
  P for Subset of TOP-REAL 2,
  C for compact non vertical non horizontal Subset of TOP-REAL 2,
  G for Go-board;

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

theorem
  for p being Point of Euclid 2 st p = 0.REAL 2 & P
  is_outside_component_of L~f
 ex r being Real st r > 0 & Ball(p,r)` c= P
proof
  let p be Point of Euclid 2 such that
A1: p = 0.REAL 2 and
A2: P is_outside_component_of L~f;
  reconsider D = L~f as bounded Subset of Euclid 2 by JORDAN2C:11;
  consider r being Real, c being Point of Euclid 2 such that
A3: 0 < r and
  c in D and
A4: for z being Point of Euclid 2 st z in D holds dist(c,z) <= r by TBSP_1:10;
  set rr = dist(p,c)+r+1;
  take rr;
  set L = (REAL 2) \ {a where a is Point of TOP-REAL 2: |.a.| < rr};
  dist(p,c)+r+0 < rr by XREAL_1:8;
  hence 0 < rr by A3,METRIC_1:5,XREAL_1:8;
  then rr = |.rr.| by ABSVALUE:def 1;
  then for a being Point of TOP-REAL 2 holds a <> |[0,rr]| or |.a.| >= rr by
TOPREAL6:23;
  then not |[0,rr]| in {a where a is Point of TOP-REAL 2: |.a.| < rr};
  then reconsider L as non empty Subset of TOP-REAL 2 by Lm1,XBOOLE_0:def 5;
  let x be object;
  assume
A5: x in Ball(p,rr)`;
  then reconsider y = x as Point of Euclid 2;
  reconsider z = y as Point of TOP-REAL 2 by EUCLID:22;
A6: dist(p,y) = |.z.| by A1,TOPREAL6:25;
A7: D c= Ball(p,rr)
  proof
    let x be object;
A8: dist(p,c) + r + 0 < dist(p,c) + r + 1 by XREAL_1:6;
    assume
A9: x in D;
    then reconsider z = x as Point of Euclid 2;
    dist(c,z) <= r by A4,A9;
    then
A10: dist(p,c) + dist(c,z) <= dist(p,c) + r by XREAL_1:7;
    dist(p,z) <= dist(p,c) + dist(c,z) by METRIC_1:4;
    then dist(p,z) <= dist(p,c) + r by A10,XXREAL_0:2;
    then dist(p,z) < dist(p,c) + r + 1 by A8,XXREAL_0:2;
    hence thesis by METRIC_1:11;
  end;
A11: L c= (L~f)`
  proof
    let l be object;
    assume
A12: l in L;
    then reconsider j = l as Point of TOP-REAL 2;
    reconsider t = j as Point of Euclid 2 by EUCLID:22;
    not l in {a where a is Point of TOP-REAL 2: |.a.| < rr} by A12,
XBOOLE_0:def 5;
    then
A13: |.j.| >= rr;
    now
      assume l in L~f;
      then dist(t,p) < rr by A7,METRIC_1:11;
      hence contradiction by A1,A13,TOPREAL6:25;
    end;
    hence thesis by A12,SUBSET_1:29;
  end;
  L is connected by JORDAN2C:53;
  then consider M being Subset of TOP-REAL 2 such that
A14: M is_a_component_of (L~f)` and
A15: L c= M by A11,GOBOARD9:3;
  M is_outside_component_of L~f
  proof
    reconsider W = L as Subset of Euclid 2;
    thus M is_a_component_of (L~f)` by A14;
    W is not bounded by JORDAN2C:62;
    then L is not bounded by JORDAN2C:11;
    hence thesis by A15,RLTOPSP1:42;
  end;
  then
A16: M in {W where W is Subset of TOP-REAL 2: W is_outside_component_of L~ f };
  not x in Ball(p,rr) by A5,XBOOLE_0:def 5;
  then for k being Point of TOP-REAL 2 holds k <> z or |.k.| >= rr by A6,
METRIC_1:11;
  then z in REAL 2 & not x in {a where a is Point of TOP-REAL 2: |.a.| < rr};
  then
A17: x in L by XBOOLE_0:def 5;
  UBD L~f is_outside_component_of L~f by JORDAN2C:68;
  then P = UBD L~f by A2,JORDAN2C:119;
  hence thesis by A17,A15,A16,TARSKI:def 4;
end;

begin  :: Go-boards

theorem
  for f being FinSequence of TOP-REAL n st L~f <> {} holds 2 <= len f
proof
  let f be FinSequence of TOP-REAL n;
  assume L~f <> {};
  then len f <> 0 & len f <> 1 by TOPREAL1:22;
  then len f > 1 by NAT_1:25;
  then len f >= 1 + 1 by NAT_1:13;
  hence thesis;
end;

theorem Th3:
  1 <= i & i < len G & 1 <= j & j < width G implies cell(G,i,j) =
  product ((1,2) --> ([.G*(i,1)`1,G*(i+1,1)`1.],[.G*(1,j)`2,G*(1,j+1)`2.]))
proof
A1: [.G*(1,j)`2,G*(1,j+1)`2.] =
  {b where b is Real : G*(1,j)`2 <= b & b <= G
  *(1,j+1)`2 } by RCOMP_1:def 1;
  set f = (1,2) --> ([.G*(i,1)`1,G*(i+1,1)`1.],[.G*(1,j)`2,G*(1,j+1)`2.]);
A2: dom f = {1,2} by FUNCT_4:62;
  assume 1 <= i & i < len G & 1 <= j & j < width G;
  then
A3: cell(G,i,j) = { |[r,s]| where r, s is Real:
   G*(i,1)`1 <= r & r <= G*(i+1
  ,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } by GOBRD11:32;
A4: [.G*(i,1)`1,G*(i+1,1)`1.] = {a where a is Real :
   G*(i,1)`1 <= a & a <= G
  *(i+1,1)`1 } by RCOMP_1:def 1;
  thus cell(G,i,j) c= product f
  proof
    let c be object;
    assume c in cell(G,i,j);
    then consider r, s being Real such that
A5: c = |[r,s]| and
A6: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1
    )`2 by A3;
A7: r in [.G*(i,1)`1,G*(i+1,1)`1.] & s in [.G*(1,j)`2,G*(1,j+1)`2.] by A4,A1,A6
;
A8: for x being object st x in dom f holds <*r,s*>.x in f.x
    proof
      let x be object;
A9:   s = |[r,s]|`2 by EUCLID:52
        .= <*r,s*>.2;
      assume x in dom f;
      then
A10:  x = 1 or x = 2 by TARSKI:def 2;
      r = |[r,s]|`1 by EUCLID:52
        .= <*r,s*>.1;
      hence thesis by A7,A10,A9,FUNCT_4:63;
    end;
    dom <*r,s*> = {1,2} by FINSEQ_1:2,89;
    hence thesis by A2,A5,A8,CARD_3:9;
  end;
  let c be object;
  assume c in product f;
  then consider g being Function such that
A11: c = g and
A12: dom g = dom f and
A13: for x being object st x in dom f holds g.x in f.x by CARD_3:def 5;
  2 in dom f by A2,TARSKI:def 2;
  then g.2 in f.2 by A13;
  then g.2 in [.G*(1,j)`2,G*(1,j+1)`2.] by FUNCT_4:63;
  then consider b being Real such that
A14: g.2 = b and
A15: G*(1,j)`2 <= b & b <= G*(1,j+1)`2 by A1;
  1 in dom f by A2,TARSKI:def 2;
  then g.1 in f.1 by A13;
  then g.1 in [.G*(i,1)`1,G*(i+1,1)`1.] by FUNCT_4:63;
  then consider a being Real such that
A16: g.1 = a and
A17: G*(i,1)`1 <= a & a <= G*(i+1,1)`1 by A4;
A18: for k being object st k in dom g holds g.k = <*a,b*>.k
  proof
    let k be object;
    assume k in dom g;
    then k = 1 or k = 2 by A12,TARSKI:def 2;
    hence thesis by A16,A14,FINSEQ_1:44;
  end;
  dom <*a,b*> = {1,2} by FINSEQ_1:2,89;
  then c = |[a,b]| by A11,A12,A18,FUNCT_1:2,FUNCT_4:62;
  hence thesis by A3,A17,A15;
end;

theorem
  1 <= i & i < len G & 1 <= j & j < width G implies cell(G,i,j) is compact
proof
  assume 1 <= i & i < len G & 1 <= j & j < width G;
  then
  cell(G,i,j) = product ((1,2) --> ([.G*(i,1)`1,G*(i+1,1)`1.], [.G*(1,j)`2
  ,G*(1,j+1)`2.])) by Th3;
  hence thesis by TOPREAL6:78;
end;

theorem
  [i,j] in Indices G & [i+n,j] in Indices G implies dist(G*(i,j),G*(i+n,
  j)) = G*(i+n,j)`1 - G*(i,j)`1
proof
  assume that
A1: [i,j] in Indices G and
A2: [i+n,j] in Indices G;
  set x = G*(i,j), y = G*(i+n,j);
  per cases;
  suppose
    n = 0;
    hence thesis by TOPREAL6:93;
  end;
  suppose
A3: n <> 0;
A4: i+n <= len G by A2,MATRIX_0:32;
A5: 1 <= i by A1,MATRIX_0:32;
A6: 1 <= i+n by A2,MATRIX_0:32;
A7: 1 <= j & j <= width G by A1,MATRIX_0:32;
    1 <= n by A3,NAT_1:14;
    then i < i+n by NAT_1:19;
    then x`1 < y`1 by A4,A7,A5,GOBOARD5:3;
    then
A8: x`1 - x`1 < y`1 - x`1 by XREAL_1:14;
    i <= len G by A1,MATRIX_0:32;
    then
A9: x`2 = G*(1,j)`2 by A7,A5,GOBOARD5:1
      .= y`2 by A6,A4,A7,GOBOARD5:1;
    thus dist(G*(i,j),G*(i+n,j)) = sqrt ((x`1-y`1)^2 + (x`2-y`2)^2) by
TOPREAL6:92
      .= |.x`1-y`1.| by A9,COMPLEX1:72
      .= |.-(x`1-y`1).| by COMPLEX1:52
      .= G*(i+n,j)`1 - G*(i,j)`1 by A8,ABSVALUE:def 1;
  end;
end;

theorem
  [i,j] in Indices G & [i,j+n] in Indices G implies dist(G*(i,j),G*(i,j+
  n)) = G*(i,j+n)`2 - G*(i,j)`2
proof
  assume that
A1: [i,j] in Indices G and
A2: [i,j+n] in Indices G;
  set x = G*(i,j), y = G*(i,j+n);
  per cases;
  suppose
    n = 0;
    hence thesis by TOPREAL6:93;
  end;
  suppose
A3: n <> 0;
A4: j+n <= width G by A2,MATRIX_0:32;
A5: 1 <= i & i <= len G by A1,MATRIX_0:32;
A6: 1 <= j+n by A2,MATRIX_0:32;
A7: 1 <= j by A1,MATRIX_0:32;
    1 <= n by A3,NAT_1:14;
    then j < j+n by NAT_1:19;
    then x`2 < y`2 by A4,A7,A5,GOBOARD5:4;
    then
A8: x`2 - x`2 < y`2 - x`2 by XREAL_1:14;
    j <= width G by A1,MATRIX_0:32;
    then
A9: x`1 = G*(i,1)`1 by A7,A5,GOBOARD5:2
      .= y`1 by A6,A4,A5,GOBOARD5:2;
    thus dist(G*(i,j),G*(i,j+n)) = sqrt ((x`1-y`1)^2 + (x`2-y`2)^2) by
TOPREAL6:92
      .= |.x`2-y`2.| by A9,COMPLEX1:72
      .= |.-(x`2-y`2).| by COMPLEX1:52
      .= G*(i,j+n)`2 - G*(i,j)`2 by A8,ABSVALUE:def 1;
  end;
end;

theorem
  3 <= len Gauge(C,n)-'1
proof
  set G = Gauge(C,n);
  4 <= len G by JORDAN8:10;
  then 4 - 1 <= len G-1 by XREAL_1:13;
  hence thesis by XREAL_0:def 2;
end;

theorem
  i <= j implies for a, b being Nat st 2 <= a & a <= len
Gauge(C,i) - 1 & 2 <= b & b <= len Gauge(C,i) - 1 ex c, d being Nat
st 2 <= c & c <= len Gauge(C,j) - 1 & 2 <= d & d <= len Gauge(C,j) - 1 & [c,d]
in Indices Gauge(C,j) & Gauge(C,i)*(a,b) = Gauge(C,j)*(c,d) & c = 2 + 2|^(j-'i)
  *(a-'2) & d = 2 + 2|^(j-'i)*(b-'2)
proof
A1: 0 <> 2|^i by NEWTON:83;
  assume
A2: i <= j;
  then
A3: 2|^(j-'i)*(2|^i) = 2|^j / 2|^i*(2|^i) by TOPREAL6:10
    .= 2|^j by A1,XCMPLX_1:87;
  let a, b be Nat such that
A4: 2 <= a and
A5: a <= len Gauge(C,i) - 1 and
A6: 2 <= b and
A7: b <= len Gauge(C,i) - 1;
A8: 1 <= a & 1 <= b by A4,A6,XXREAL_0:2;
  set c = 2 + 2|^(j-'i)*(a-'2), d = 2 + 2|^(j-'i)*(b-'2);
A9: 0 <= b-2 by A6,XREAL_1:48;
  set n = N-bound C, e = E-bound C, s = S-bound C, w = W-bound C;
A10: 0 <> 2|^j by NEWTON:83;
A11: (n-s)/(2|^j)*(d-2) = (n-s)/(2|^j)*((2|^j/2|^i)*(b-'2)) by A2,TOPREAL6:10
    .= (n-s)/(2|^j)*(2|^j/2|^i)*(b-'2)
    .= (n-s)/((2|^j)/(2|^j/2|^i))*(b-'2) by XCMPLX_1:81
    .= (n-s)/(2|^i)*(b-'2) by A10,XCMPLX_1:52
    .= (n-s)/(2|^i)*(b-2) by A9,XREAL_0:def 2;
  take c, d;
A12: 2+0 <= 2+2|^(j-'i)*(a-'2) by XREAL_1:6;
  then
A13: 1 <= c by XXREAL_0:2;
  2|^i + 2 - 2 >= 0;
  then
A14: 2|^i + 2 -' 2 = 2|^i + 0 by XREAL_0:def 2;
A15: 0 <= a-2 by A4,XREAL_1:48;
A16: (e-w)/(2|^j)*(c-2) = (e-w)/(2|^j)*((2|^j/2|^i)*(a-'2)) by A2,TOPREAL6:10
    .= (e-w)/(2|^j)*(2|^j/2|^i)*(a-'2)
    .= (e-w)/((2|^j)/(2|^j/2|^i))*(a-'2) by XCMPLX_1:81
    .= (e-w)/(2|^i)*(a-'2) by A10,XCMPLX_1:52
    .= (e-w)/(2|^i)*(a-2) by A15,XREAL_0:def 2;
A17: len Gauge(C,j) - 1 < len Gauge(C,j) - 0 by XREAL_1:15;
A18: len Gauge(C,i) - 1 = 2|^i + 3 - 1 by JORDAN8:def 1
    .= 2|^i + 2;
  then a -' 2 <= 2|^i + 2 -' 2 by A5,NAT_D:42;
  then
A19: 2|^(j-'i)*(a-'2) <= 2|^j by A14,A3,XREAL_1:64;
  b -' 2 <= 2|^i + 2 -' 2 by A7,A18,NAT_D:42;
  then
A20: 2|^(j-'i)*(b-'2) <= 2|^j by A14,A3,XREAL_1:64;
A21: len Gauge(C,i) - 1 < len Gauge(C,i) - 0 by XREAL_1:15;
  then
A22: a <= len Gauge(C,i) by A5,XXREAL_0:2;
  len Gauge(C,j) - 1 = 2|^j + 3 - 1 by JORDAN8:def 1
    .= 2|^j + 2;
  hence
A23: 2 <= c & c <= len Gauge(C,j) - 1 & 2 <= d & d <= len Gauge(C,j ) -
  1 by A19,A20,A12,XREAL_1:6;
  then
A24: 1 <= d by XXREAL_0:2;
  width Gauge(C,j) = len Gauge(C,j) by JORDAN8:def 1;
  then
A25: d <= width Gauge(C,j) by A23,A17,XXREAL_0:2;
  c <= len Gauge(C,j) by A23,A17,XXREAL_0:2;
  hence [c,d] in Indices Gauge(C,j) by A13,A24,A25,MATRIX_0:30;
  then
A26: Gauge(C,j)*(c,d) = |[w+(e-w)/(2|^j)*(c-2), s+(n-s)/(2|^j)*(d-2)]| by
JORDAN8:def 1;
  width Gauge(C,i) = len Gauge(C,i) by JORDAN8:def 1;
  then b <= width Gauge(C,i) by A7,A21,XXREAL_0:2;
  then [a,b] in Indices Gauge(C,i) by A22,A8,MATRIX_0:30;
  then
A27: Gauge(C,i)*(a,b) = |[w+(e-w)/(2|^i)*(a-2), s+(n-s)/(2|^i)*(b-2)]| by
JORDAN8:def 1;
  then
A28: Gauge(C,i)*(a,b)`2 = s+(n-s)/(2|^i)*(b-2) by EUCLID:52
    .= Gauge(C,j)*(c,d)`2 by A26,A11,EUCLID:52;
  Gauge(C,i)*(a,b)`1 = w+(e-w)/(2|^i)*(a-2) by A27,EUCLID:52
    .= Gauge(C,j)*(c,d)`1 by A26,A16,EUCLID:52;
  hence Gauge(C,i)*(a,b) = Gauge(C,j)*(c,d) by A28,TOPREAL3:6;
  thus thesis;
end;

theorem Th9:
  [i,j] in Indices Gauge(C,n) & [i,j+1] in Indices Gauge(C,n)
implies dist(Gauge(C,n)*(i,j),Gauge(C,n)*(i,j+1)) = (N-bound C - S-bound C)/2|^
  n
proof
  set G = Gauge(C,n), a = N-bound C, e = E-bound C, s = S-bound C, w = W-bound
  C, p1 = G*(i,j), p2 = G*(i,j+1);
  assume that
A1: [i,j] in Indices G and
A2: [i,j+1] in Indices G;
A3: p2 = |[w+(e-w)/(2|^n)*(i-2), s+(a-s)/(2|^n)*(j+1-2)]| by A2,JORDAN8:def 1;
  a >= s by SPRECT_1:22;
  then
A4: a - s >= s - s by XREAL_1:9;
  set x = (a-s)/(2|^n);
  consider p, q being Point of Euclid 2 such that
A5: p = p1 & q = p2 and
A6: dist(p1,p2) = dist(p,q) by TOPREAL6:def 1;
A7: p1 = |[w+(e-w)/(2|^n)*(i-2), s+(a-s)/(2|^n)*(j-2)]| by A1,JORDAN8:def 1;
  dist(p,q) = (Pitag_dist 2).(p,q) by METRIC_1:def 1
    .= sqrt ((p1`1 - p2`1)^2 + (p1`2 - p2`2)^2) by A5,TOPREAL3:7
    .= sqrt ((w+(e-w)/(2|^n)*(i-2) - p2`1)^2 + (p1`2 - p2`2)^2) by A7,EUCLID:52
    .= sqrt ((w+(e-w)/(2|^n)*(i-2) - (w+(e-w)/(2|^n)*(i-2)))^2 + (p1`2 - p2
  `2)^2) by A3,EUCLID:52
    .= |.p1`2 - p2`2.| by COMPLEX1:72
    .= |.s+x*(j-2) - p2`2.| by A7,EUCLID:52
    .= |.s+x*(j-2) - (s+x*(j+1-2)).| by A3,EUCLID:52
    .= |.-x.|
    .= |.x.| by COMPLEX1:52
    .= |.a-s.|/|.2|^n.| by COMPLEX1:67
    .= (a-s)/|.2|^n.| by A4,ABSVALUE:def 1;
  hence thesis by A6,ABSVALUE:def 1;
end;

theorem Th10:
  [i,j] in Indices Gauge(C,n) & [i+1,j] in Indices Gauge(C,n)
implies dist(Gauge(C,n)*(i,j),Gauge(C,n)*(i+1,j)) = (E-bound C - W-bound C)/2|^
  n
proof
  set G = Gauge(C,n), a = N-bound C, e = E-bound C, s = S-bound C, w = W-bound
  C, p1 = G*(i,j), p2 = G*(i+1,j);
  assume that
A1: [i,j] in Indices G and
A2: [i+1,j] in Indices G;
A3: p2 = |[w+(e-w)/(2|^n)*(i+1-2), s+(a-s)/(2|^n)*(j-2)]| by A2,JORDAN8:def 1;
  e >= w by SPRECT_1:21;
  then
A4: e - w >= w - w by XREAL_1:9;
  set x = (e-w)/(2|^n);
  consider p, q being Point of Euclid 2 such that
A5: p = p1 & q = p2 and
A6: dist(p1,p2) = dist(p,q) by TOPREAL6:def 1;
A7: p1 = |[w+(e-w)/(2|^n)*(i-2), s+(a-s)/(2|^n)*(j-2)]| by A1,JORDAN8:def 1;
  dist(p,q) = (Pitag_dist 2).(p,q) by METRIC_1:def 1
    .= sqrt ((p1`1 - p2`1)^2 + (p1`2 - p2`2)^2) by A5,TOPREAL3:7
    .= sqrt ((p1`1 - p2`1)^2 + (s+(a-s)/(2|^n)*(j-2) - p2`2)^2) by A7,EUCLID:52
    .= sqrt ((p1`1 - p2`1)^2 + (s+(a-s)/(2|^n)*(j-2) - (s+(a-s)/(2|^n)*(j-2)
  ))^2) by A3,EUCLID:52
    .= |.p1`1 - p2`1.| by COMPLEX1:72
    .= |.w+x*(i-2) - p2`1.| by A7,EUCLID:52
    .= |.w+x*(i-2) - (w+x*(i+1-2)).| by A3,EUCLID:52
    .= |.-x.|
    .= |.x.| by COMPLEX1:52
    .= |.e-w.|/|.2|^n.| by COMPLEX1:67
    .= (e-w)/|.2|^n.| by A4,ABSVALUE:def 1;
  hence thesis by A6,ABSVALUE:def 1;
end;

theorem
  for r, t being Real holds r > 0 & t > 0 implies ex n being
  Nat st 1 < n & dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) < r & dist(
  Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < t
proof
  let r, t be Real;
  assume that
A1: r > 0 and
A2: t > 0;
  set n = N-bound C, e = E-bound C, s = S-bound C, w = W-bound C;
  set a = |.[\ log(2,(n-s)/r) /].| + 1, b = |.[\ log(2,(e-w)/t) /].| + 1;
  take i = max(a,b)+1;
A3: 2 to_power i > 0 by POWER:34;
  then
A4: 2|^i > 0 by POWER:41;
  [\ log(2,(n-s)/r) /] <= |.[\ log(2,(n-s)/r) /].| by ABSVALUE:4;
  then
A5: [\ log(2,(n-s)/r) /] + 1 <= a by XREAL_1:6;
  [\ log(2,(n-s)/r) /] > log(2,(n-s)/r) - 1 by INT_1:def 6;
  then [\ log(2,(n-s)/r) /] + 1 > log(2,(n-s)/r) - 1 + 1 by XREAL_1:6;
  then
A6: a > log(2,(n-s)/r) - 1 + 1 by A5,XXREAL_0:2;
  a <= max(a,b) by XXREAL_0:25;
  then
A7: a+1 <= max(a,b)+1 by XREAL_1:6;
  a < a+1 by XREAL_1:29;
  then i > a by A7,XXREAL_0:2;
  then i > log(2,(n-s)/r) by A6,XXREAL_0:2;
  then log(2,2 to_power i) > log(2,(n-s)/r) by A3,POWER:def 3;
  then 2 to_power i > (n-s)/r by A3,PRE_FF:10;
  then 2|^i > (n-s)/r by POWER:41;
  then 2|^i * r > (n-s)/r * r by A1,XREAL_1:68;
  then 2|^i * r > n-s by A1,XCMPLX_1:87;
  then 2|^i * r / 2|^i > (n-s) / 2|^i by A4,XREAL_1:74;
  then
A8: (n-s)/2|^i < r by A4,XCMPLX_1:89;
  a >= 0+1 & max(a,b) >= a by XREAL_1:7,XXREAL_0:25;
  then max(a,b) >= 1 by XXREAL_0:2;
  then max(a,b)+1 >= 1+1 by XREAL_1:7;
  hence 1 < i by XXREAL_0:2;
A9: len Gauge(C,i) >= 4 by JORDAN8:10;
  then
A10: 1 <= len Gauge(C,i) by XXREAL_0:2;
  [\ log(2,(e-w)/t) /] <= |.[\ log(2,(e-w)/t) /].| by ABSVALUE:4;
  then
A11: [\ log(2,(e-w)/t) /] + 1 <= b by XREAL_1:6;
  [\ log(2,(e-w)/t) /] > log(2,(e-w)/t) - 1 by INT_1:def 6;
  then [\ log(2,(e-w)/t) /] + 1 > log(2,(e-w)/t) - 1 + 1 by XREAL_1:6;
  then
A12: b > log(2,(e-w)/t) - 1 + 1 by A11,XXREAL_0:2;
  b <= max(a,b) by XXREAL_0:25;
  then
A13: b+1 <= max(a,b)+1 by XREAL_1:6;
  b < b+1 by XREAL_1:29;
  then i > b by A13,XXREAL_0:2;
  then i > log(2,(e-w)/t) by A12,XXREAL_0:2;
  then log(2,2 to_power i) > log(2,(e-w)/t) by A3,POWER:def 3;
  then 2 to_power i > (e-w)/t by A3,PRE_FF:10;
  then 2|^i > (e-w)/t by POWER:41;
  then 2|^i * t > (e-w)/t * t by A2,XREAL_1:68;
  then 2|^i * t > e-w by A2,XCMPLX_1:87;
  then 2|^i * t / 2|^i > (e-w) / 2|^i by A4,XREAL_1:74;
  then
A14: (e-w)/2|^i < t by A4,XCMPLX_1:89;
A15: len Gauge(C,i) = width Gauge(C,i) by JORDAN8:def 1;
  then
A16: [1,1] in Indices Gauge(C,i) by A10,MATRIX_0:30;
A17: 1+1 <= width Gauge(C,i) by A15,A9,XXREAL_0:2;
  then
A18: [1,1+1] in Indices Gauge(C,i) by A10,MATRIX_0:30;
  [1+1,1] in Indices Gauge(C,i) by A15,A10,A17,MATRIX_0:30;
  hence thesis by A8,A14,A16,A18,Th9,Th10;
end;

begin  :: LeftComp and RightComp

theorem Th12:
  for P being Subset of (TOP-REAL 2)|(L~f)` st P is a_component
  holds P = RightComp f or P = LeftComp f
proof
  let P be Subset of (TOP-REAL 2)|(L~f)`;
  assume that
A1: P is a_component and
A2: P <> RightComp f;
  P <> {}((TOP-REAL 2)|(L~f)`) by A1,CONNSP_1:32;
  then consider a being Point of (TOP-REAL 2)|(L~f)` such that
A3: a in P by SUBSET_1:4;
  the carrier of (TOP-REAL 2)|(L~f)` = (L~f)` & (L~f)` = LeftComp f \/
  RightComp f by GOBRD12:10,PRE_TOPC:8;
  then
A4: a in LeftComp f or a in RightComp f by XBOOLE_0:def 3;
  LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
  then
A5: ex L being Subset of (TOP-REAL 2)|(L~f)` st L = LeftComp f & L
  is a_component by CONNSP_1:def 6;
  RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
  then consider R being Subset of (TOP-REAL 2)|(L~f)` such that
A6: R = RightComp f and
A7: R is a_component by CONNSP_1:def 6;
  P misses R by A1,A2,A6,A7,CONNSP_1:35;
  then P meets LeftComp f by A6,A3,A4,XBOOLE_0:3;
  hence thesis by A1,A5,CONNSP_1:35;
end;

theorem
  for A1, A2 being Subset of TOP-REAL 2 st (L~f)` = A1 \/ A2 & A1 misses
A2 & for C1, C2 being Subset of (TOP-REAL 2)|(L~f)` st C1 = A1 & C2 = A2 holds
C1 is a_component & C2 is a_component
holds A1 = RightComp f & A2 = LeftComp f or A1 = LeftComp f & A2 =
  RightComp f
proof
  let A1, A2 be Subset of TOP-REAL 2 such that
A1: (L~f)` = A1 \/ A2 and
A2: A1 /\ A2 = {} and
A3: for C1, C2 being Subset of (TOP-REAL 2)|(L~f)` st C1 = A1 & C2 = A2
holds C1 is a_component & C2 is a_component;
  the carrier of (TOP-REAL 2)|(L~f)` = (L~f)` by PRE_TOPC:8;
  then reconsider C1 = A1, C2 = A2 as Subset of (TOP-REAL 2)|(L~f)` by A1,
XBOOLE_1:7;
  C1 = A1;
  then C2 is a_component by A3;
  then
A4: C2 = RightComp f or C2 = LeftComp f by Th12;
  C2 = A2;
  then C1 is a_component by A3;
  then
A5: C1 = RightComp f or C1 = LeftComp f by Th12;
  assume not thesis;
  hence contradiction by A2,A5,A4;
end;

theorem Th14:
  LeftComp f misses RightComp f
proof
  assume LeftComp f /\ RightComp f <> {};
  then consider x being object such that
A1: x in LeftComp f /\ RightComp f by XBOOLE_0:def 1;
  now
    take x;
    thus x in LeftComp f & x in RightComp f by A1,XBOOLE_0:def 4;
  end;
  then
A2: LeftComp f meets RightComp f by XBOOLE_0:3;
  LeftComp f is_a_component_of (L~f)` & RightComp f is_a_component_of (L~f
  ) ` by GOBOARD9:def 1,def 2;
  hence thesis by A2,GOBOARD9:1,SPRECT_4:6;
end;

theorem Th15:
  L~f \/ RightComp f \/ LeftComp f = the carrier of TOP-REAL 2
proof
A1: (L~f)` \/ L~f = [#]the carrier of TOP-REAL 2 by SUBSET_1:10
    .= the carrier of TOP-REAL 2;
  (L~f)` = RightComp f \/ LeftComp f by GOBRD12:10;
  hence thesis by A1,XBOOLE_1:4;
end;

theorem Th16:
  p in L~f iff not p in LeftComp f & not p in RightComp f
proof
A1: p in L~f iff not p in (L~f)` by XBOOLE_0:def 5;
  (L~f)` = LeftComp f \/ RightComp f by GOBRD12:10;
  hence thesis by A1,XBOOLE_0:def 3;
end;

theorem Th17:
  p in LeftComp f iff not p in L~f & not p in RightComp f
proof
  LeftComp f misses RightComp f by Th14;
  then
A1: (L~f)` = LeftComp f \/ RightComp f & LeftComp f /\ RightComp f = {} by
GOBRD12:10;
  p in L~f iff not p in (L~f)` by XBOOLE_0:def 5;
  hence thesis by A1,XBOOLE_0:def 3,def 4;
end;

theorem
  p in RightComp f iff not p in L~f & not p in LeftComp f by Th16,Th17;

theorem Th19:
  L~f = (Cl RightComp f) \ RightComp f
proof
  thus L~f c= (Cl RightComp f) \ RightComp f
  proof
    let x be object;
    assume
A1: x in L~f;
    then reconsider p = x as Point of TOP-REAL 2;
    consider i such that
A2: 1 <= i & i+1 <= len f and
A3: p in LSeg(f,i) by A1,SPPOL_2:13;
    for O being Subset of TOP-REAL 2 st O is open holds p in O implies
    RightComp f meets O
    proof
      left_cell(f,i) /\ right_cell(f,i) = LSeg(f,i) by A2,GOBOARD5:31;
      then LSeg(f,i) c= right_cell(f,i) by XBOOLE_1:17;
      then
A4:   p in right_cell(f,i) by A3;
      f is_sequence_on GoB f by GOBOARD5:def 5;
      then consider i1, j1, i2, j2 being Nat such that
A5:   [i1,j1] in Indices GoB f and
A6:   f/.i = GoB f*(i1,j1) and
A7:   [i2,j2] in Indices GoB f and
A8:   f/.(i+1) = GoB f*(i2,j2) and
A9:   i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 =
      j2 or i1 = i2 & j1 = j2+1 by A2,JORDAN8:3;
A10:  1 <= i1 by A5,MATRIX_0:32;
A11:  j2 <= width GoB f by A7,MATRIX_0:32;
A12:  1 <= j1 by A5,MATRIX_0:32;
A13:  j1 <= width GoB f by A5,MATRIX_0:32;
A14:  i1 <= len GoB f by A5,MATRIX_0:32;
A15:  i2 <= len GoB f by A7,MATRIX_0:32;
A16:  now
        per cases by A9;
        case
A17:      i1 = i2 & j1+1 = j2;
          set w = i1-'1;
A18:      w+1 = i1 by A10,XREAL_1:235;
          then right_cell(f,i) = cell(GoB f,w+1,j1) by A2,A5,A6,A7,A8,A17,
GOBOARD5:27;
          hence p in Cl Int right_cell(f,i) by A4,A14,A13,A18,GOBRD11:35;
        end;
        case
A19:      i1+1 = i2 & j1 = j2;
          set w = j1-'1;
          w <= w+1 & w+1 <= width GoB f by A12,A13,NAT_1:11,XREAL_1:235;
          then
A20:      w <= width GoB f by XXREAL_0:2;
          w+1 = j1 by A12,XREAL_1:235;
          then right_cell(f,i) = cell(GoB f,i1,w) by A2,A5,A6,A7,A8,A19,
GOBOARD5:28;
          hence p in Cl Int right_cell(f,i) by A4,A14,A20,GOBRD11:35;
        end;
        case
A21:      i1 = i2+1 & j1 = j2;
          set w = j1-'1;
A22:      w+1 = j1 by A12,XREAL_1:235;
          then right_cell(f,i) = cell(GoB f,i2,w+1) by A2,A5,A6,A7,A8,A21,
GOBOARD5:29;
          hence p in Cl Int right_cell(f,i) by A4,A13,A15,A22,GOBRD11:35;
        end;
        case
A23:      i1 = i2 & j1 = j2+1;
          set z = i1-'1;
          z <= z+1 & z+1 <= len GoB f by A10,A14,NAT_1:11,XREAL_1:235;
          then
A24:      z <= len GoB f by XXREAL_0:2;
          z+1 = i1 by A10,XREAL_1:235;
          then right_cell(f,i) = cell(GoB f,z,j2) by A2,A5,A6,A7,A8,A23,
GOBOARD5:30;
          hence p in Cl Int right_cell(f,i) by A4,A11,A24,GOBRD11:35;
        end;
      end;
      let O be Subset of TOP-REAL 2;
      assume O is open & p in O;
      then O meets Int right_cell(f,i) by A16,PRE_TOPC:def 7;
      hence thesis by A2,GOBOARD9:25,XBOOLE_1:63;
    end;
    then
A25: p in Cl RightComp f by PRE_TOPC:def 7;
    not x in RightComp f by A1,Th16;
    hence thesis by A25,XBOOLE_0:def 5;
  end;
  assume not (Cl RightComp f) \ RightComp f c= L~f;
  then consider q being object such that
A26: q in (Cl RightComp f) \ RightComp f and
A27: not q in L~f;
  reconsider q as Point of TOP-REAL 2 by A26;
  not q in RightComp f by A26,XBOOLE_0:def 5;
  then
A28: q in LeftComp f by A27,Th16;
  q in Cl RightComp f by A26,XBOOLE_0:def 5;
  then LeftComp f meets RightComp f by A28,PRE_TOPC:def 7;
  hence contradiction by Th14;
end;

theorem Th20:
  L~f = (Cl LeftComp f) \ LeftComp f
proof
  thus L~f c= (Cl LeftComp f) \ LeftComp f
  proof
    let x be object;
    assume
A1: x in L~f;
    then reconsider p = x as Point of TOP-REAL 2;
    consider i such that
A2: 1 <= i & i+1 <= len f and
A3: p in LSeg(f,i) by A1,SPPOL_2:13;
    for O being Subset of TOP-REAL 2 st O is open holds p in O implies
    LeftComp f meets O
    proof
      left_cell(f,i) /\ right_cell(f,i) = LSeg(f,i) by A2,GOBOARD5:31;
      then LSeg(f,i) c= left_cell(f,i) by XBOOLE_1:17;
      then
A4:   p in left_cell(f,i) by A3;
      f is_sequence_on GoB f by GOBOARD5:def 5;
      then consider i1, j1, i2, j2 being Nat such that
A5:   [i1,j1] in Indices GoB f and
A6:   f/.i = GoB f*(i1,j1) and
A7:   [i2,j2] in Indices GoB f and
A8:   f/.(i+1) = GoB f*(i2,j2) and
A9:   i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 =
      j2 or i1 = i2 & j1 = j2+1 by A2,JORDAN8:3;
A10:  1 <= i1 by A5,MATRIX_0:32;
A11:  j2 <= width GoB f by A7,MATRIX_0:32;
A12:  1 <= j1 by A5,MATRIX_0:32;
A13:  j1 <= width GoB f by A5,MATRIX_0:32;
A14:  i1 <= len GoB f by A5,MATRIX_0:32;
A15:  i2 <= len GoB f by A7,MATRIX_0:32;
A16:  now
        per cases by A9;
        case
A17:      i1 = i2 & j1+1 = j2;
          set w = i1-'1;
          w <= w+1 & w+1 <= len GoB f by A10,A14,NAT_1:11,XREAL_1:235;
          then
A18:      w <= len GoB f by XXREAL_0:2;
          w+1 = i1 by A10,XREAL_1:235;
          then left_cell(f,i) = cell(GoB f,w,j1) by A2,A5,A6,A7,A8,A17,
GOBOARD5:27;
          hence p in Cl Int left_cell(f,i) by A4,A13,A18,GOBRD11:35;
        end;
        case
A19:      i1+1 = i2 & j1 = j2;
          set w = j1-'1;
          w+1 = j1 by A12,XREAL_1:235;
          then
A20:      left_cell(f,i) = cell(GoB f,i1,w+1) by A2,A5,A6,A7,A8,A19,GOBOARD5:28
;
          w+1 <= width GoB f by A12,A13,XREAL_1:235;
          hence p in Cl Int left_cell(f,i) by A4,A14,A20,GOBRD11:35;
        end;
        case
A21:      i1 = i2+1 & j1 = j2;
          set w = j1-'1;
          w <= w+1 & w+1 <= width GoB f by A12,A13,NAT_1:11,XREAL_1:235;
          then
A22:      w <= width GoB f by XXREAL_0:2;
          w+1 = j1 by A12,XREAL_1:235;
          then left_cell(f,i) = cell(GoB f,i2,w) by A2,A5,A6,A7,A8,A21,
GOBOARD5:29;
          hence p in Cl Int left_cell(f,i) by A4,A15,A22,GOBRD11:35;
        end;
        case
A23:      i1 = i2 & j1 = j2+1;
          set z = i1-'1;
          z+1 = i1 by A10,XREAL_1:235;
          then
A24:      left_cell(f,i) = cell(GoB f,z+1,j2) by A2,A5,A6,A7,A8,A23,GOBOARD5:30
;
          z+1 <= len GoB f by A10,A14,XREAL_1:235;
          hence p in Cl Int left_cell(f,i) by A4,A11,A24,GOBRD11:35;
        end;
      end;
      let O be Subset of TOP-REAL 2;
      assume O is open & p in O;
      then O meets Int left_cell(f,i) by A16,PRE_TOPC:def 7;
      hence thesis by A2,GOBOARD9:21,XBOOLE_1:63;
    end;
    then
A25: p in Cl LeftComp f by PRE_TOPC:def 7;
    not x in LeftComp f by A1,Th16;
    hence thesis by A25,XBOOLE_0:def 5;
  end;
  assume not (Cl LeftComp f) \ LeftComp f c= L~f;
  then consider q being object such that
A26: q in (Cl LeftComp f) \ LeftComp f and
A27: not q in L~f;
  reconsider q as Point of TOP-REAL 2 by A26;
  not q in LeftComp f by A26,XBOOLE_0:def 5;
  then
A28: q in RightComp f by A27,Th16;
  q in Cl LeftComp f by A26,XBOOLE_0:def 5;
  then RightComp f meets LeftComp f by A28,PRE_TOPC:def 7;
  hence contradiction by Th14;
end;

theorem Th21:
  Cl RightComp f = (RightComp f) \/ L~f
proof
  thus Cl RightComp f c= RightComp f \/ L~f
  proof
    let x be object;
    assume
A1: x in Cl RightComp f;
    now
A2:   now
        assume x in LeftComp f;
        then LeftComp f meets RightComp f by A1,TOPS_1:12;
        hence contradiction by Th14;
      end;
      assume not x in RightComp f;
      hence x in L~f by A1,A2,Th16;
    end;
    hence thesis by XBOOLE_0:def 3;
  end;
  (Cl RightComp f) \ RightComp f c= Cl RightComp f by XBOOLE_1:36;
  then RightComp f c= Cl RightComp f & L~f c= Cl RightComp f by Th19,
PRE_TOPC:18;
  hence thesis by XBOOLE_1:8;
end;

theorem
  Cl LeftComp f = (LeftComp f) \/ L~f
proof
  thus Cl LeftComp f c= LeftComp f \/ L~f
  proof
    let x be object;
    assume
A1: x in Cl LeftComp f;
    now
A2:   not x in RightComp f by A1,Th14,TOPS_1:12;
      assume not x in LeftComp f;
      hence x in L~f by A1,A2,Th16;
    end;
    hence thesis by XBOOLE_0:def 3;
  end;
  (Cl LeftComp f) \ LeftComp f c= Cl LeftComp f by XBOOLE_1:36;
  then LeftComp f c= Cl LeftComp f & L~f c= Cl LeftComp f by Th20,PRE_TOPC:18;
  hence thesis by XBOOLE_1:8;
end;

registration
  let f be non constant standard special_circular_sequence;
  cluster L~f -> Jordan;
  coherence
  proof
    thus (L~f)` <> {};
    take A1 = RightComp f, A2 = LeftComp f;
    thus (L~f)` = A1 \/ A2 by GOBRD12:10;
    L~f = (Cl A1) \ A1 by Th19;
    hence thesis by Th14,Th20,GOBOARD9:def 1,def 2;
  end;
end;

reserve f for clockwise_oriented non constant standard
  special_circular_sequence;

theorem Th23:
  p in RightComp f implies W-bound L~f < p`1
proof
  set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
  reconsider u = p as Point of Euclid 2 by EUCLID:22;
  assume p in RightComp f;
  then p in RightComp g by REVROT_1:37;
  then u in Int RightComp g by TOPS_1:23;
  then consider r being Real such that
A2: r > 0 and
A3: Ball(u,r) c= RightComp g by GOBOARD6:5;
  reconsider r as Real;
  reconsider k = |[p`1-r/2,p`2]| as Point of Euclid 2 by EUCLID:22;
  dist(u,k) = (Pitag_dist 2).(u,k) by METRIC_1:def 1
    .= sqrt ((p`1 - |[p`1-r/2,p`2]|`1)^2 + (p`2 - |[p`1-r/2,p`2]|`2)^2) by
TOPREAL3:7
    .= sqrt ((p`1 - (p`1-r/2))^2 + (p`2 - |[p`1-r/2,p`2]|`2)^2) by EUCLID:52
    .= sqrt ((p`1 - (p`1-r/2))^2 + (p`2 - p`2)^2) by EUCLID:52
    .= r/2 by A2,SQUARE_1:22;
  then dist(u,k) < r/1 by A2,XREAL_1:76;
  then
A4: k in Ball(u,r) by METRIC_1:11;
  RightComp g misses LeftComp g by Th14;
  then
A5: not |[p`1-r/2,p`2]| in LeftComp g by A3,A4,XBOOLE_0:3;
  set x = |[p`1-r/2,N-bound L~SpStSeq L~g]|;
A6: LSeg(NW-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by SPRECT_3:14;
A7: proj1.x = x`1 by PSCOMP_1:def 5
    .= p`1-r/2 by EUCLID:52;
  N-min L~f in rng f by SPRECT_2:39;
  then
A8: g/.1 = N-min L~g by A1,FINSEQ_6:92;
  then |[p`1-r/2,p`2]|`1 <= E-bound L~g by A5,JORDAN2C:111;
  then p`1-r/2 <= E-bound L~g by EUCLID:52;
  then
A9: x`1 <= E-bound L~g by EUCLID:52;
  x`2 = N-bound L~SpStSeq L~g by EUCLID:52;
  then
A10: x`2 = N-bound L~g by SPRECT_1:60;
  |[p`1-r/2,p`2]|`1 >= W-bound L~g by A8,A5,JORDAN2C:110;
  then p`1-r/2 >= W-bound L~g by EUCLID:52;
  then
A11: x`1 >= W-bound L~g by EUCLID:52;
  LSeg(NW-corner L~g, NE-corner L~g) = { q : q`1 <= E-bound L~g & q`1 >=
  W-bound L~g & q`2 = N-bound L~g} by SPRECT_1:25;
  then x in LSeg(NW-corner L~g,NE-corner L~g) by A9,A11,A10;
  then
  proj1.:L~SpStSeq L~g is bounded_below & p`1-r/2 in proj1.:L~SpStSeq L~g
  by A6,A7,FUNCT_2:35;
  then
A12: lower_bound(proj1.:L~SpStSeq L~g) <= p`1-r/2 by SEQ_4:def 2;
  r/2 > 0 by A2,XREAL_1:139;
  then
A13: p`1-r/2 < p`1-0 by XREAL_1:15;
  W-bound L~SpStSeq L~g = W-bound L~g & W-bound L~SpStSeq L~g =
  lower_bound( proj1.:L~SpStSeq L~g) by SPRECT_1:43,58;
  hence thesis by A1,A12,A13,XXREAL_0:2;
end;

theorem Th24:
  p in RightComp f implies E-bound L~f > p`1
proof
  set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
  reconsider u = p as Point of Euclid 2 by EUCLID:22;
  assume p in RightComp f;
  then p in RightComp g by REVROT_1:37;
  then u in Int RightComp g by TOPS_1:23;
  then consider r being Real such that
A2: r > 0 and
A3: Ball(u,r) c= RightComp g by GOBOARD6:5;
  reconsider r as Real;
  reconsider k = |[p`1+r/2,p`2]| as Point of Euclid 2 by EUCLID:22;
  dist(u,k) = (Pitag_dist 2).(u,k) by METRIC_1:def 1
    .= sqrt ((p`1 - |[p`1+r/2,p`2]|`1)^2 + (p`2 - |[p`1+r/2,p`2]|`2)^2) by
TOPREAL3:7
    .= sqrt ((p`1 - (p`1+r/2))^2 + (p`2 - |[p`1+r/2,p`2]|`2)^2) by EUCLID:52
    .= sqrt ((p`1 - (p`1+r/2))^2 + (p`2 - p`2)^2) by EUCLID:52
    .= sqrt ((r/2)^2)
    .= r/2 by A2,SQUARE_1:22;
  then dist(u,k) < r/1 by A2,XREAL_1:76;
  then
A4: k in Ball(u,r) by METRIC_1:11;
  RightComp g misses LeftComp g by Th14;
  then
A5: not |[p`1+r/2,p`2]| in LeftComp g by A3,A4,XBOOLE_0:3;
  set x = |[p`1+r/2,N-bound L~SpStSeq L~g]|;
A6: LSeg(NW-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by SPRECT_3:14;
A7: proj1.x = x`1 by PSCOMP_1:def 5
    .= p`1+r/2 by EUCLID:52;
  N-min L~f in rng f by SPRECT_2:39;
  then
A8: g/.1 = N-min L~g by A1,FINSEQ_6:92;
  then |[p`1+r/2,p`2]|`1 <= E-bound L~g by A5,JORDAN2C:111;
  then p`1+r/2 <= E-bound L~g by EUCLID:52;
  then
A9: x`1 <= E-bound L~g by EUCLID:52;
  x`2 = N-bound L~SpStSeq L~g by EUCLID:52;
  then
A10: x`2 = N-bound L~g by SPRECT_1:60;
  |[p`1+r/2,p`2]|`1 >= W-bound L~g by A8,A5,JORDAN2C:110;
  then p`1+r/2 >= W-bound L~g by EUCLID:52;
  then
A11: x`1 >= W-bound L~g by EUCLID:52;
  LSeg(NW-corner L~g, NE-corner L~g) = { q : q`1 <= E-bound L~g & q`1 >=
  W-bound L~g & q`2 = N-bound L~g} by SPRECT_1:25;
  then x in LSeg(NW-corner L~g,NE-corner L~g) by A9,A11,A10;
  then
  proj1.:L~SpStSeq L~g is bounded_above & p`1+r/2 in proj1.:L~SpStSeq L~g
  by A6,A7,FUNCT_2:35;
  then
A12: upper_bound(proj1.:L~SpStSeq L~g) >= p`1+r/2 by SEQ_4:def 1;
  r/2 > 0 by A2,XREAL_1:139;
  then
A13: p`1+r/2 > p`1+0 by XREAL_1:6;
  E-bound L~SpStSeq L~g = E-bound L~g &
   E-bound L~SpStSeq L~g = upper_bound(proj1
  .:L~ SpStSeq L~g) by SPRECT_1:46,61;
  hence thesis by A1,A12,A13,XXREAL_0:2;
end;

theorem Th25:
  p in RightComp f implies N-bound L~f > p`2
proof
  set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
  reconsider u = p as Point of Euclid 2 by EUCLID:22;
  assume p in RightComp f;
  then p in RightComp g by REVROT_1:37;
  then u in Int RightComp g by TOPS_1:23;
  then consider r being Real such that
A2: r > 0 and
A3: Ball(u,r) c= RightComp g by GOBOARD6:5;
  reconsider r as Real;
  reconsider k = |[p`1,p`2+r/2]| as Point of Euclid 2 by EUCLID:22;
  dist(u,k) = (Pitag_dist 2).(u,k) by METRIC_1:def 1
    .= sqrt ((p`1 - |[p`1,p`2+r/2]|`1)^2 + (p`2 - |[p`1,p`2+r/2]|`2)^2) by
TOPREAL3:7
    .= sqrt ((p`1 - p`1)^2 + (p`2 - |[p`1,p`2+r/2]|`2)^2) by EUCLID:52
    .= sqrt ((p`2 - (p`2+r/2))^2) by EUCLID:52
    .= sqrt ((r/2)^2)
    .= r/2 by A2,SQUARE_1:22;
  then dist(u,k) < r/1 by A2,XREAL_1:76;
  then
A4: k in Ball(u,r) by METRIC_1:11;
  RightComp g misses LeftComp g by Th14;
  then
A5: not |[p`1,p`2+r/2]| in LeftComp g by A3,A4,XBOOLE_0:3;
  set x = |[E-bound L~SpStSeq L~g,p`2+r/2]|;
A6: LSeg(SE-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by TOPREAL6:35;
A7: proj2.x = x`2 by PSCOMP_1:def 6
    .= p`2+r/2 by EUCLID:52;
  N-min L~f in rng f by SPRECT_2:39;
  then
A8: g/.1 = N-min L~g by A1,FINSEQ_6:92;
  then |[p`1,p`2+r/2]|`2 <= N-bound L~g by A5,JORDAN2C:113;
  then p`2+r/2 <= N-bound L~g by EUCLID:52;
  then
A9: x`2 <= N-bound L~g by EUCLID:52;
  x`1 = E-bound L~SpStSeq L~g by EUCLID:52;
  then
A10: x`1 = E-bound L~g by SPRECT_1:61;
  |[p`1,p`2+r/2]|`2 >= S-bound L~g by A8,A5,JORDAN2C:112;
  then p`2+r/2 >= S-bound L~g by EUCLID:52;
  then
A11: x`2 >= S-bound L~g by EUCLID:52;
  LSeg(SE-corner L~g, NE-corner L~g) = { q : q`1 = E-bound L~g & q`2 <=
  N-bound L~g & q`2 >= S-bound L~g } by SPRECT_1:23;
  then x in LSeg(SE-corner L~g,NE-corner L~g) by A9,A11,A10;
  then
  proj2.:L~SpStSeq L~g is bounded_above & p`2+r/2 in proj2.:L~SpStSeq L~g
  by A6,A7,FUNCT_2:35;
  then
A12: upper_bound(proj2.:L~SpStSeq L~g) >= p`2+r/2 by SEQ_4:def 1;
  r/2 > 0 by A2,XREAL_1:139;
  then
A13: p`2+r/2 > p`2+0 by XREAL_1:6;
  N-bound L~SpStSeq L~g = N-bound L~g &
   N-bound L~SpStSeq L~g = upper_bound(proj2
  .:L~ SpStSeq L~g) by SPRECT_1:45,60;
  hence thesis by A1,A12,A13,XXREAL_0:2;
end;

theorem Th26:
  p in RightComp f implies S-bound L~f < p`2
proof
  set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
  reconsider u = p as Point of Euclid 2 by EUCLID:22;
  assume p in RightComp f;
  then p in RightComp g by REVROT_1:37;
  then u in Int RightComp g by TOPS_1:23;
  then consider r being Real such that
A2: r > 0 and
A3: Ball(u,r) c= RightComp g by GOBOARD6:5;
  reconsider r as Real;
  reconsider k = |[p`1,p`2-r/2]| as Point of Euclid 2 by EUCLID:22;
  dist(u,k) = (Pitag_dist 2).(u,k) by METRIC_1:def 1
    .= sqrt ((p`1 - |[p`1,p`2-r/2]|`1)^2 + (p`2 - |[p`1,p`2-r/2]|`2)^2) by
TOPREAL3:7
    .= sqrt ((p`1 - p`1)^2 + (p`2 - |[p`1,p`2-r/2]|`2)^2) by EUCLID:52
    .= sqrt ((p`2 - (p`2-r/2))^2) by EUCLID:52
    .= r/2 by A2,SQUARE_1:22;
  then dist(u,k) < r/1 by A2,XREAL_1:76;
  then
A4: k in Ball(u,r) by METRIC_1:11;
  RightComp g misses LeftComp g by Th14;
  then
A5: not |[p`1,p`2-r/2]| in LeftComp g by A3,A4,XBOOLE_0:3;
  set x = |[E-bound L~SpStSeq L~g,p`2-r/2]|;
A6: LSeg(SE-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by TOPREAL6:35;
A7: proj2.x = x`2 by PSCOMP_1:def 6
    .= p`2-r/2 by EUCLID:52;
  N-min L~f in rng f by SPRECT_2:39;
  then
A8: g/.1 = N-min L~g by A1,FINSEQ_6:92;
  then |[p`1,p`2-r/2]|`2 <= N-bound L~g by A5,JORDAN2C:113;
  then p`2-r/2 <= N-bound L~g by EUCLID:52;
  then
A9: x`2 <= N-bound L~g by EUCLID:52;
  x`1 = E-bound L~SpStSeq L~g by EUCLID:52;
  then
A10: x`1 = E-bound L~g by SPRECT_1:61;
  |[p`1,p`2-r/2]|`2 >= S-bound L~g by A8,A5,JORDAN2C:112;
  then p`2-r/2 >= S-bound L~g by EUCLID:52;
  then
A11: x`2 >= S-bound L~g by EUCLID:52;
  LSeg(SE-corner L~g, NE-corner L~g) = { q : q`1 = E-bound L~g & q`2 <=
  N-bound L~g & q`2 >= S-bound L~g } by SPRECT_1:23;
  then x in LSeg(SE-corner L~g,NE-corner L~g) by A9,A11,A10;
  then
  proj2.:L~SpStSeq L~g is bounded_below & p`2-r/2 in proj2.:L~SpStSeq L~g
  by A6,A7,FUNCT_2:35;
  then
A12: lower_bound(proj2.:L~SpStSeq L~g) <= p`2-r/2 by SEQ_4:def 2;
  r/2 > 0 by A2,XREAL_1:139;
  then
A13: p`2-r/2 < p`2-0 by XREAL_1:15;
  S-bound L~SpStSeq L~g = S-bound L~g & S-bound L~SpStSeq L~g =
  lower_bound( proj2.:L~SpStSeq L~g) by SPRECT_1:44,59;
  hence thesis by A1,A12,A13,XXREAL_0:2;
end;

theorem Th27:
  p in RightComp f & q in LeftComp f implies LSeg(p,q) meets L~f
proof
  assume that
A1: p in RightComp f and
A2: q in LeftComp f;
  assume LSeg(p,q) misses L~f;
  then LSeg(p,q) c= (L~f)` by TDLAT_1:2;
  then reconsider A = LSeg(p,q) as Subset of (TOP-REAL 2)|(L~f)` by PRE_TOPC:8;
  LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
  then consider L being Subset of (TOP-REAL 2)|(L~f)` such that
A3: L = LeftComp f and
A4: L is a_component by CONNSP_1:def 6;
  q in A by RLTOPSP1:68;
  then
A5: L meets A by A2,A3,XBOOLE_0:3;
  RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
  then consider R being Subset of (TOP-REAL 2)|(L~f)` such that
A6: R = RightComp f and
A7: R is a_component by CONNSP_1:def 6;
  p in A by RLTOPSP1:68;
  then A is connected & R meets A by A1,A6,CONNSP_1:23,XBOOLE_0:3;
  hence contradiction by A6,A7,A3,A4,A5,JORDAN2C:92,SPRECT_4:6;
end;

theorem Th28:
  Cl RightComp SpStSeq C = product((1,2)-->([.W-bound L~SpStSeq C,
  E-bound L~SpStSeq C.], [.S-bound L~SpStSeq C,N-bound L~SpStSeq C.]))
proof
  set g = (1,2)-->([.W-bound L~SpStSeq C,E-bound L~SpStSeq C.], [.S-bound L~
  SpStSeq C,N-bound L~SpStSeq C.]);
A1: dom g = {1,2} by FUNCT_4:62;
A2: Cl RightComp SpStSeq C = (RightComp SpStSeq C) \/ L~SpStSeq C by Th21;
  hereby
    let a be object;
    assume
A3: a in Cl RightComp SpStSeq C;
    then reconsider b = a as Point of TOP-REAL 2;
    reconsider h = a as FinSequence by A3;
A4: for x being object st x in {1,2} holds h.x in g.x
    proof
      let x be object such that
A5:   x in {1,2};
      per cases by A5,TARSKI:def 2;
      suppose
A6:     x = 1;
        then
A7:     g.x = [.W-bound L~SpStSeq C,E-bound L~SpStSeq C.] by FUNCT_4:63;
        now
          per cases by A2,A3,XBOOLE_0:def 3;
          case
            a in RightComp SpStSeq C;
            then W-bound L~SpStSeq C < b`1 & E-bound L~SpStSeq C > b`1 by Th23
,Th24;
            hence thesis by A6,A7,XXREAL_1:1;
          end;
          case
            a in L~SpStSeq C;
            then W-bound L~SpStSeq C <= b`1 & b`1 <= E-bound L~SpStSeq C by
PSCOMP_1:24;
            hence thesis by A6,A7,XXREAL_1:1;
          end;
        end;
        hence thesis;
      end;
      suppose
A8:     x = 2;
        then
A9:     g.x = [.S-bound L~SpStSeq C,N-bound L~SpStSeq C.] by FUNCT_4:63;
        now
          per cases by A2,A3,XBOOLE_0:def 3;
          case
            a in RightComp SpStSeq C;
            then S-bound L~SpStSeq C < b`2 & N-bound L~SpStSeq C > b`2 by Th25
,Th26;
            hence thesis by A8,A9,XXREAL_1:1;
          end;
          case
            a in L~SpStSeq C;
            then S-bound L~SpStSeq C <= b`2 & b`2 <= N-bound L~SpStSeq C by
PSCOMP_1:24;
            hence thesis by A8,A9,XXREAL_1:1;
          end;
        end;
        hence thesis;
      end;
    end;
    a is Tuple of 2,REAL by A3,Lm1,FINSEQ_2:131;
    then ex r, s being Element of REAL st a = <*r,s*> by FINSEQ_2:100;
    then dom h = {1,2} by FINSEQ_1:2,89;
    hence a in product g by A1,A4,CARD_3:9;
  end;
  let a be object;
  assume a in product g;
  then consider h being Function such that
A10: a = h and
A11: dom h = dom g and
A12: for x being object st x in dom g holds h.x in g.x by CARD_3:def 5;
A13: [.S-bound L~SpStSeq C,N-bound L~SpStSeq C.]
   = {s where s is Real:
  S-bound L~SpStSeq C <= s & s <= N-bound L~SpStSeq C} by RCOMP_1:def 1;
  2 in dom g by A1,TARSKI:def 2;
  then h.2 in g.2 by A12;
  then h.2 in [.S-bound L~SpStSeq C,N-bound L~SpStSeq C.] by FUNCT_4:63;
  then consider s being Real such that
A14: h.2 = s and
A15: S-bound L~SpStSeq C <= s & s <= N-bound L~SpStSeq C by A13;
A16: [.W-bound L~SpStSeq C,E-bound L~SpStSeq C.]
  = {r where r is Real :
  W-bound L~SpStSeq C <= r & r <= E-bound L~SpStSeq C} by RCOMP_1:def 1;
  1 in dom g by A1,TARSKI:def 2;
  then h.1 in g.1 by A12;
  then h.1 in [.W-bound L~SpStSeq C,E-bound L~SpStSeq C.] by FUNCT_4:63;
  then consider r being Real such that
A17: h.1 = r and
A18: W-bound L~SpStSeq C <= r & r <= E-bound L~SpStSeq C by A16;
A19: LeftComp SpStSeq C = {q: not(W-bound L~SpStSeq C <= q`1 & q`1 <=
E-bound L~SpStSeq C & S-bound L~SpStSeq C <= q`2 & q`2 <= N-bound L~SpStSeq C)}
  by SPRECT_3:37;
A20: for k being object st k in dom h holds h.k = <*r,s*>.k
  proof
    let k be object;
    assume k in dom h;
    then k = 1 or k = 2 by A11,TARSKI:def 2;
    hence thesis by A17,A14,FINSEQ_1:44;
  end;
  dom <*r,s*> = {1,2} by FINSEQ_1:2,89;
  then
A21: a = |[r,s]| by A10,A11,A20,FUNCT_1:2,FUNCT_4:62;
  assume not a in Cl RightComp SpStSeq C;
  then ( not a in RightComp SpStSeq C)& not a in L~SpStSeq C by A2,
XBOOLE_0:def 3;
  then a in LeftComp SpStSeq C by A21,Th16;
  then ex q st q = a & not(W-bound L~SpStSeq C <= q`1 & q`1 <= E-bound L~
  SpStSeq C & S-bound L~SpStSeq C <= q`2 & q`2 <= N-bound L~SpStSeq C) by A19;
  hence contradiction by A18,A15,A21,EUCLID:52;
end;

theorem Th29:
  proj1.:(Cl RightComp f) = proj1.:(L~f)
proof
  set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
  N-min L~f in rng f by SPRECT_2:39;
  then
A2: g/.1 = N-min L~g by A1,FINSEQ_6:92;
  thus proj1.:(Cl RightComp f) c= proj1.:(L~f)
  proof
A3: Cl RightComp f = (RightComp f) \/ L~f by Th21;
    let a be object;
    assume a in proj1.:(Cl RightComp f);
    then consider x being object such that
A4: x in the carrier of TOP-REAL 2 and
A5: x in Cl RightComp f and
A6: a = proj1.x by FUNCT_2:64;
    per cases by A5,A3,XBOOLE_0:def 3;
    suppose
A7:   x in RightComp f;
      reconsider x as Point of TOP-REAL 2 by A4;
      set b = |[x`1,N-bound L~f + 1]|;
      b`2 = N-bound L~f + 1 & N-bound L~f + 1 > N-bound L~f + 0 by EUCLID:52
,XREAL_1:6;
      then b in LeftComp g by A1,A2,JORDAN2C:113;
      then b in LeftComp f by REVROT_1:36;
      then LSeg(x,b) meets L~f by A7,Th27;
      then consider c being object such that
A8:   c in LSeg(x,b) and
A9:   c in L~f by XBOOLE_0:3;
      reconsider c as Point of TOP-REAL 2 by A8;
A10:  b`1 = x`1 by EUCLID:52;
      proj1.c = c`1 by PSCOMP_1:def 5
        .= x`1 by A8,A10,GOBOARD7:5
        .= a by A6,PSCOMP_1:def 5;
      hence thesis by A9,FUNCT_2:35;
    end;
    suppose
      x in L~f;
      hence thesis by A6,FUNCT_2:35;
    end;
  end;
  L~f = (Cl RightComp f) \ RightComp f by Th19;
  hence thesis by RELAT_1:123,XBOOLE_1:36;
end;

theorem Th30:
  proj2.:(Cl RightComp f) = proj2.:(L~f)
proof
  set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
  N-min L~f in rng f by SPRECT_2:39;
  then
A2: g/.1 = N-min L~g by A1,FINSEQ_6:92;
  thus proj2.:(Cl RightComp f) c= proj2.:(L~f)
  proof
A3: Cl RightComp f = (RightComp f) \/ L~f by Th21;
    let a be object;
    assume a in proj2.:(Cl RightComp f);
    then consider x being object such that
A4: x in the carrier of TOP-REAL 2 and
A5: x in Cl RightComp f and
A6: a = proj2.x by FUNCT_2:64;
    per cases by A5,A3,XBOOLE_0:def 3;
    suppose
A7:   x in RightComp f;
      reconsider x as Point of TOP-REAL 2 by A4;
      set b = |[E-bound L~f + 1,x`2]|;
      b`1 = E-bound L~f + 1 & E-bound L~f + 1 > E-bound L~f + 0 by EUCLID:52
,XREAL_1:6;
      then b in LeftComp g by A1,A2,JORDAN2C:111;
      then b in LeftComp f by REVROT_1:36;
      then LSeg(x,b) meets L~f by A7,Th27;
      then consider c be object such that
A8:   c in LSeg(x,b) and
A9:   c in L~f by XBOOLE_0:3;
      reconsider c as Point of TOP-REAL 2 by A8;
A10:  b`2 = x`2 by EUCLID:52;
      proj2.c = c`2 by PSCOMP_1:def 6
        .= x`2 by A8,A10,GOBOARD7:6
        .= a by A6,PSCOMP_1:def 6;
      hence thesis by A9,FUNCT_2:35;
    end;
    suppose
      x in L~f;
      hence thesis by A6,FUNCT_2:35;
    end;
  end;
  L~f = (Cl RightComp f) \ RightComp f by Th19;
  hence thesis by RELAT_1:123,XBOOLE_1:36;
end;

theorem Th31:
  RightComp g c= RightComp SpStSeq L~g
proof
  let a be object;
  assume
A1: a in RightComp g;
  then reconsider p = a as Point of TOP-REAL 2;
  p`1 > W-bound L~g by A1,Th23;
  then
A2: p`1 > W-bound L~SpStSeq L~g by SPRECT_1:58;
  p`2 > S-bound L~g by A1,Th26;
  then
A3: p`2 > S-bound L~SpStSeq L~g by SPRECT_1:59;
  p`1 < E-bound L~g by A1,Th24;
  then
A4: p`1 < E-bound L~SpStSeq L~g by SPRECT_1:61;
  p`2 < N-bound L~g by A1,Th25;
  then
A5: p`2 < N-bound L~SpStSeq L~g by SPRECT_1:60;
  RightComp SpStSeq L~g = {q : W-bound L~SpStSeq L~g < q`1 & q`1 <
  E-bound L~SpStSeq L~g & S-bound L~SpStSeq L~g < q`2 & q`2 < N-bound L~SpStSeq
  L~g} by SPRECT_3:37;
  hence thesis by A2,A4,A3,A5;
end;

theorem Th32:
  Cl RightComp g is compact
proof
  Cl RightComp SpStSeq L~g = product((1,2)-->([.W-bound L~SpStSeq L~g,
  E-bound L~SpStSeq L~g.], [.S-bound L~SpStSeq L~g,N-bound L~SpStSeq L~g.]))
by Th28;
  then
A1: Cl RightComp SpStSeq L~g is compact by TOPREAL6:78;
  RightComp g c= RightComp SpStSeq L~g by Th31;
  hence thesis by A1,COMPTS_1:9,PRE_TOPC:19;
end;

theorem Th33:
  LeftComp g is non bounded
proof
  Cl RightComp g is compact by Th32;
  then RightComp g is bounded by PRE_TOPC:18,RLTOPSP1:42;
  then
A1: L~g \/ RightComp g is bounded by TOPREAL6:67;
  L~g \/ RightComp g \/ LeftComp g = the carrier of TOP-REAL 2 by Th15;
  hence thesis by A1,TOPREAL6:66;
end;

theorem Th34:
  LeftComp g is_outside_component_of L~g
by GOBOARD9:def 1,Th33;

theorem
  RightComp g is_inside_component_of L~g
proof
  thus RightComp g is_a_component_of (L~g)` by GOBOARD9:def 2;
  Cl RightComp g is compact by Th32;
  hence thesis by PRE_TOPC:18,RLTOPSP1:42;
end;

theorem Th36:
  UBD L~g = LeftComp g
proof
  UBD L~g is_outside_component_of L~g & LeftComp g is_outside_component_of
  L~g by Th34,JORDAN2C:68;
  hence thesis by JORDAN2C:119;
end;

theorem Th37:
  BDD L~g = RightComp g
proof
A1: (BDD L~g) misses (UBD L~g) by JORDAN2C:24;
A2: (L~g)` = (BDD L~g) \/ (UBD L~g) & LeftComp g misses RightComp g by Th14,
JORDAN2C:27;
  UBD L~g = LeftComp g & (L~g)` = LeftComp g \/ RightComp g by Th36,GOBRD12:10;
  hence thesis by A2,A1,XBOOLE_1:71;
end;

theorem
  P is_outside_component_of L~g implies P = LeftComp g
proof
  assume
A1: P is_outside_component_of L~g;
  UBD L~g is_outside_component_of L~g by JORDAN2C:68;
  then P = UBD L~g by A1,JORDAN2C:119;
  hence thesis by Th36;
end;

theorem Th39:
  P is_inside_component_of L~g implies P meets RightComp g
proof
  assume P is_inside_component_of L~g;
  then
A1: P c= BDD L~g & P is_a_component_of (L~g)` by JORDAN2C:22;
  BDD L~g = RightComp g by Th37;
  hence thesis by A1,SPRECT_1:4,XBOOLE_1:67;
end;

theorem
  P is_inside_component_of L~g implies P = BDD L~g
proof
A1: RightComp g = BDD L~g by Th37;
  BDD L~g is_inside_component_of L~g by JORDAN2C:108;
  then
A2: BDD L~g is_a_component_of (L~g)`;
  assume
A3: P is_inside_component_of L~g;
  thus thesis by A3,A1,A2,Th39,GOBOARD9:1;
end;

theorem
  W-bound L~g = W-bound RightComp g
proof
  set A = (Cl RightComp g) \ RightComp g;
A1: W-bound Cl RightComp g = lower_bound (proj1.:(Cl RightComp g)) by
SPRECT_1:43;
A2: L~g = A by Th19;
  Cl RightComp g is compact by Th32;
  then
A3: RightComp g is bounded by PRE_TOPC:18,RLTOPSP1:42;
  reconsider A as non empty Subset of TOP-REAL 2 by A2;
  proj1.:(Cl RightComp g) = proj1.:(L~g) & W-bound A = lower_bound (proj1
  .:A) by Th29,SPRECT_1:43;
  hence thesis by A2,A3,A1,TOPREAL6:85;
end;

theorem
  E-bound L~g = E-bound RightComp g
proof
  set A = (Cl RightComp g) \ RightComp g;
A1: E-bound Cl RightComp g = upper_bound (proj1.:(Cl RightComp g))
 by SPRECT_1:46;
A2: L~g = A by Th19;
  Cl RightComp g is compact by Th32;
  then
A3: RightComp g is bounded by PRE_TOPC:18,RLTOPSP1:42;
  reconsider A as non empty Subset of TOP-REAL 2 by A2;
  proj1.:(Cl RightComp g) = proj1.:(L~g) & E-bound A =
   upper_bound (proj1.:A) by Th29,SPRECT_1:46;
  hence thesis by A2,A3,A1,TOPREAL6:86;
end;

theorem
  N-bound L~g = N-bound RightComp g
proof
  set A = (Cl RightComp g) \ RightComp g;
A1: N-bound Cl RightComp g = upper_bound (proj2.:(Cl RightComp g))
 by SPRECT_1:45;
A2: L~g = A by Th19;
  Cl RightComp g is compact by Th32;
  then
A3: RightComp g is bounded by PRE_TOPC:18,RLTOPSP1:42;
  reconsider A as non empty Subset of TOP-REAL 2 by A2;
  proj2.:(Cl RightComp g) = proj2.:(L~g) &
   N-bound A = upper_bound (proj2.:A) by Th30,SPRECT_1:45;
  hence thesis by A2,A3,A1,TOPREAL6:87;
end;

theorem
  S-bound L~g = S-bound RightComp g
proof
  set A = (Cl RightComp g) \ RightComp g;
A1: S-bound Cl RightComp g = lower_bound (proj2.:(Cl RightComp g)) by
SPRECT_1:44;
A2: L~g = A by Th19;
  Cl RightComp g is compact by Th32;
  then
A3: RightComp g is bounded by PRE_TOPC:18,RLTOPSP1:42;
  reconsider A as non empty Subset of TOP-REAL 2 by A2;
  proj2.:(Cl RightComp g) = proj2.:(L~g) & S-bound A = lower_bound (proj2
  .:A) by Th30,SPRECT_1:44;
  hence thesis by A2,A3,A1,TOPREAL6:88;
end;