JORDAN22

:: On Some Points of a Simple Closed Curve. {P}art {II}
::  by Artur Korni{\l}owicz and Adam Grabowski
::
:: Received October 6, 2004
:: Copyright (c) 2004-2026 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, TOPREAL2, SUBSET_1, EUCLID, RELAT_1, PRE_TOPC, FUNCT_1,
      STRUCT_0, JORDAN19, TARSKI, GOBOARD9, JORDAN9, CARD_1, JORDAN6, TOPREAL1,
      RELAT_2, PSCOMP_1, RCOMP_1, KURATO_2, XBOOLE_0, XXREAL_0, FINSEQ_1,
      JORDAN8, MATRIX_1, TREES_1, SPPOL_1, ARYTM_3, METRIC_1, ARYTM_1, NEWTON,
      ORDINAL2, RLTOPSP1, JORDAN1A, MCART_1, XXREAL_2, SEQ_4, GOBOARD2,
      JORDAN21, JORDAN2C, GOBOARD1, FINSEQ_6, GOBOARD5, PARTFUN1, PCOMPS_1,
      WEIERSTR, SEQ_1, SEQ_2, REAL_1, COMPLEX1, JORDAN10, JORDAN3, CONVEX1,
      NAT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, XXREAL_0,
      XCMPLX_0, XREAL_0, REAL_1, COMPLEX1, NAT_1, NAT_D, RELSET_1, PARTFUN1,
      FUNCT_2, XXREAL_2, SEQ_4, NEWTON, FINSEQ_1, MATRIX_0, DOMAIN_1, STRUCT_0,
      PRE_TOPC, COMPTS_1, FINSEQ_6, CONNSP_1, METRIC_1, PCOMPS_1, PSCOMP_1,
      RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD1, GOBOARD2,
      WEIERSTR, SPPOL_1, GOBOARD5, TOPRNS_1, JORDAN2C, JORDAN6, GOBOARD9,
      JORDAN8, JORDAN9, GOBRD13, TOPREAL6, JORDAN10, JORDAN1K, JORDAN1A,
      KURATO_2, JORDAN19, JORDAN21;
 constructors REAL_1, RCOMP_1, NEWTON, BINARITH, CONNSP_1, MONOID_0, TOPRNS_1,
      TOPREAL4, GOBOARD2, PSCOMP_1, GOBOARD9, JORDAN5C, JORDAN6, JORDAN2C,
      TOPREAL6, JORDAN1K, JORDAN21, JORDAN8, GOBRD13, JORDAN9, JORDAN10,
      JORDAN1A, KURATO_2, JORDAN19, NAT_D, SEQ_4, FUNCSDOM, CONVEX1, JORDAN11;
 registrations XBOOLE_0, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
      MEMBERED, FINSEQ_6, STRUCT_0, COMPTS_1, EUCLID, TOPREAL1, TOPREAL2,
      GOBOARD2, SPPOL_2, TOPREAL5, SPRECT_2, JORDAN6, SPRECT_3, JORDAN2C,
      REVROT_1, TOPREAL6, JORDAN21, JORDAN8, JORDAN10, VALUED_0, FUNCT_1,
      ORDINAL1, RLTOPSP1, JORDAN1, XCMPLX_0, NEWTON;
 requirements SUBSET, BOOLE, REAL, NUMERALS, ARITHM;
 definitions TARSKI, TOPRNS_1, XXREAL_2;
 equalities JORDAN6, JORDAN21;
 expansions TARSKI, JORDAN6, XXREAL_2;
 theorems XBOOLE_1, JORDAN1A, JORDAN6, XBOOLE_0, JORDAN1K, EUCLID, TOPREAL1,
      TARSKI, JORDAN16, METRIC_1, SPRECT_3, TOPMETR, JORDAN7, GOBRD14,
      JORDAN1I, INT_1, GOBOARD5, FINSEQ_6, REVROT_1, SPRECT_2, GOBOARD7,
      JGRAPH_1, JORDAN1H, JORDAN9, GOBRD13, NAT_1, JORDAN8, SUBSET_1, JORDAN2C,
      JORDAN10, PSCOMP_1, SPPOL_2, SPPOL_1, SEQ_4, FUNCT_2, WEIERSTR, JORDAN1G,
      TOPRNS_1, ABSVALUE, JORDAN19, KURATO_2, JORDAN21, XREAL_1, JORDAN1J,
      JORDAN1B, RELAT_1, JORDAN5D, TOPREAL3, JORDAN1F, NEWTON, SPRECT_1,
      XXREAL_0, PEPIN, TOPREAL6, JCT_MISC, MATRIX_0, XXREAL_2, NAT_D, XREAL_0,
      COMPTS_1, PRE_TOPC, RLTOPSP1, ORDINAL1;
 schemes FUNCT_2;

begin :: Properties of the Approximations

reserve C for Simple_closed_curve,
  i for Nat;

Lm1: for r being Real, X being Subset of TOP-REAL 2 st r in proj2.:X ex
x being Point of TOP-REAL 2 st x in X & proj2.x = r
proof
  let r be Real, X be Subset of TOP-REAL 2;
  assume r in proj2.:X;
  then
  ex x being object st x in the carrier of TOP-REAL 2 & x in X & proj2.x = r
  by FUNCT_2:64;
  hence thesis;
end;

theorem Th1:
  (Upper_Appr C).i c= Cl RightComp Cage(C,0)
proof
A1: Upper_Arc L~Cage (C,i) c= L~Cage (C,i) by JORDAN6:61;
A2: L~Cage (C,i) c= Cl RightComp Cage(C,0) by JORDAN1H:46;
  (Upper_Appr C).i = Upper_Arc L~Cage (C,i) by JORDAN19:def 1;
  hence thesis by A1,A2;
end;

theorem Th2:
  (Lower_Appr C).i c= Cl RightComp Cage(C,0)
proof
A1: Lower_Arc L~Cage (C,i) c= L~Cage (C,i) by JORDAN6:61;
A2: L~Cage (C,i) c= Cl RightComp Cage(C,0) by JORDAN1H:46;
  (Lower_Appr C).i = Lower_Arc L~Cage (C,i) by JORDAN19:def 2;
  hence thesis by A1,A2;
end;

registration
  let C be Simple_closed_curve;
  cluster Upper_Arc C -> connected;
  coherence
  proof
    Upper_Arc C is_an_arc_of W-min C,E-max C by JORDAN6:def 8;
    hence thesis by JORDAN6:10;
  end;
  cluster Lower_Arc C -> connected;
  coherence
  proof
    Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:def 9;
    hence thesis by JORDAN6:10;
  end;
end;

theorem
  (Upper_Appr C).i is compact connected
proof
  Upper_Arc L~Cage(C,i) is compact;
  hence (Upper_Appr C).i is compact by JORDAN19:def 1;
  Upper_Arc L~Cage(C,i) is connected;
  hence thesis by JORDAN19:def 1;
end;

theorem
  (Lower_Appr C).i is compact connected
proof
  Lower_Arc L~Cage(C,i) is compact;
  hence (Lower_Appr C).i is compact by JORDAN19:def 2;
  Lower_Arc L~Cage(C,i) is connected;
  hence thesis by JORDAN19:def 2;
end;

registration
  let C be Simple_closed_curve;
  cluster North_Arc C -> compact;
  coherence
  proof
    for i being Nat holds (Upper_Appr C).i c= Cl RightComp Cage
    (C,0) by Th1;
    then Lim_inf Upper_Appr C is compact by KURATO_2:26;
    hence thesis by JORDAN19:def 3;
  end;
  cluster South_Arc C -> compact;
  coherence
  proof
    for i being Nat holds (Lower_Appr C).i c= Cl RightComp Cage
    (C,0) by Th2;
    then Lim_inf Lower_Appr C is compact by KURATO_2:26;
    hence thesis by JORDAN19:def 4;
  end;
end;

:: Moved from JORDAN21, AK, 22.02.2006

reserve R for non empty Subset of TOP-REAL 2,
  j, k, m, n for Nat;

Lm2: dom proj2 = the carrier of TOP-REAL 2 by FUNCT_2:def 1;

Lm3: 1 <= len Gauge(R,n)
proof
  4 <= len Gauge(R,n) by JORDAN8:10;
  hence thesis by XXREAL_0:2;
end;

theorem Th5:
  [1,1] in Indices Gauge(R,n)
proof
A1: len Gauge(R,n) = width Gauge(R,n) by JORDAN8:def 1;
  1 <= len Gauge(R,n) by Lm3;
  hence thesis by A1,MATRIX_0:30;
end;

theorem Th6:
  [1,2] in Indices Gauge(R,n)
proof
A1: len Gauge(R,n) = width Gauge(R,n) by JORDAN8:def 1;
A2: 4 <= len Gauge(R,n) by JORDAN8:10;
  then
A3: 2 <= len Gauge(R,n) by XXREAL_0:2;
  1 <= len Gauge(R,n) by A2,XXREAL_0:2;
  hence thesis by A1,A3,MATRIX_0:30;
end;

theorem Th7:
  [2,1] in Indices Gauge(R,n)
proof
A1: len Gauge(R,n) = width Gauge(R,n) by JORDAN8:def 1;
A2: 4 <= len Gauge(R,n) by JORDAN8:10;
  then
A3: 2 <= len Gauge(R,n) by XXREAL_0:2;
  1 <= len Gauge(R,n) by A2,XXREAL_0:2;
  hence thesis by A1,A3,MATRIX_0:30;
end;

theorem Th8:
  for C being non vertical non horizontal compact Subset of
TOP-REAL 2 holds m > k & [i,j] in Indices Gauge(C,k) & [i,j+1] in Indices Gauge
(C,k) implies dist(Gauge(C,m)*(i,j),Gauge(C,m)*(i,j+1)) < dist(Gauge(C,k)*(i,j)
  ,Gauge(C,k)*(i,j+1))
proof
  let C be non vertical non horizontal compact Subset of TOP-REAL 2;
  assume that
A1: m > k and
A2: [i,j] in Indices Gauge(C,k) and
A3: [i,j+1] in Indices Gauge(C,k);
A4: len Gauge(C,k) < len Gauge(C,m) by A1,JORDAN1A:29;
A5: len Gauge(C,m) = width Gauge(C,m) by JORDAN8:def 1;
A6: len Gauge(C,k) = width Gauge(C,k) by JORDAN8:def 1;
  j <= width Gauge(C,k) by A2,MATRIX_0:32;
  then
A7: j <= width Gauge(C,m) by A6,A5,A4,XXREAL_0:2;
A8: N-bound C - S-bound C > 0 by SPRECT_1:32,XREAL_1:50;
  i <= len Gauge(C,k) by A2,MATRIX_0:32;
  then
A9: i <= len Gauge(C,m) by A4,XXREAL_0:2;
  j+1 <= width Gauge(C,k) by A3,MATRIX_0:32;
  then
A10: j+1 <= width Gauge(C,m) by A6,A5,A4,XXREAL_0:2;
A11: 1 <= i by A2,MATRIX_0:32;
  1 <= j+1 by NAT_1:11;
  then
A12: [i,j+1] in Indices Gauge(C,m) by A11,A9,A10,MATRIX_0:30;
  1 <= j by A2,MATRIX_0:32;
  then [i,j] in Indices Gauge(C,m) by A11,A9,A7,MATRIX_0:30;
  then
A13: dist(Gauge(C,m)*(i,j),Gauge(C,m)*(i,j+1)) = (N-bound C - S-bound C)/2|^
  m by A12,GOBRD14:9;
A14: 2|^k > 0 by NEWTON:83;
  dist(Gauge(C,k)*(i,j),Gauge(C,k)*(i,j+1)) = (N-bound C - S-bound C)/2|^k
  by A2,A3,GOBRD14:9;
  hence thesis by A1,A13,A14,A8,PEPIN:66,XREAL_1:76;
end;

theorem Th9:
  for C being non vertical non horizontal compact Subset of
TOP-REAL 2 holds m > k implies dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,2)) < dist(
  Gauge(C,k)*(1,1),Gauge(C,k)*(1,2))
proof
  let C be non vertical non horizontal compact Subset of TOP-REAL 2;
  assume
A1: m > k;
  [1,1+1] in Indices Gauge(C,k) by Th6;
  hence thesis by A1,Th5,Th8;
end;

theorem Th10:
  for C being non vertical non horizontal compact Subset of
TOP-REAL 2 holds m > k & [i,j] in Indices Gauge(C,k) & [i+1,j] in Indices Gauge
(C,k) implies dist(Gauge(C,m)*(i,j),Gauge(C,m)*(i+1,j)) < dist(Gauge(C,k)*(i,j)
  ,Gauge(C,k)*(i+1,j))
proof
  let C be non vertical non horizontal compact Subset of TOP-REAL 2;
  assume that
A1: m > k and
A2: [i,j] in Indices Gauge(C,k) and
A3: [i+1,j] in Indices Gauge(C,k);
A4: len Gauge(C,k) < len Gauge(C,m) by A1,JORDAN1A:29;
  i <= len Gauge(C,k) by A2,MATRIX_0:32;
  then
A5: i <= len Gauge(C,m) by A4,XXREAL_0:2;
A6: E-bound C - W-bound C > 0 by SPRECT_1:31,XREAL_1:50;
A7: len Gauge(C,m) = width Gauge(C,m) by JORDAN8:def 1;
A8: len Gauge(C,k) = width Gauge(C,k) by JORDAN8:def 1;
  j <= width Gauge(C,k) by A2,MATRIX_0:32;
  then
A9: j <= width Gauge(C,m) by A8,A7,A4,XXREAL_0:2;
  i+1 <= len Gauge(C,k) by A3,MATRIX_0:32;
  then
A10: i+1 <= len Gauge(C,m) by A4,XXREAL_0:2;
A11: 1 <= j by A2,MATRIX_0:32;
  1 <= i+1 by NAT_1:11;
  then
A12: [i+1,j] in Indices Gauge(C,m) by A11,A9,A10,MATRIX_0:30;
  1 <= i by A2,MATRIX_0:32;
  then [i,j] in Indices Gauge(C,m) by A11,A5,A9,MATRIX_0:30;
  then
A13: dist(Gauge(C,m)*(i,j),Gauge(C,m)*(i+1,j)) = (E-bound C - W-bound C)/2|^
  m by A12,GOBRD14:10;
A14: 2|^k > 0 by NEWTON:83;
  dist(Gauge(C,k)*(i,j),Gauge(C,k)*(i+1,j)) = (E-bound C - W-bound C)/2|^k
  by A2,A3,GOBRD14:10;
  hence thesis by A1,A13,A14,A6,PEPIN:66,XREAL_1:76;
end;

theorem Th11:
  for C being non vertical non horizontal compact Subset of
TOP-REAL 2 holds m > k implies dist(Gauge(C,m)*(1,1),Gauge(C,m)*(2,1)) < dist(
  Gauge(C,k)*(1,1),Gauge(C,k)*(2,1))
proof
  let C be non vertical non horizontal compact Subset of TOP-REAL 2;
  assume
A1: m > k;
  [1+1,1] in Indices Gauge(C,k) by Th7;
  hence thesis by A1,Th5,Th10;
end;

theorem
  for r, t being Real holds r > 0 & t > 0 implies ex n being
  Nat st i < 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;
  consider n being Nat such that
  1 < n and
A3: dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) < r and
A4: dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < t by A1,A2,GOBRD14:11;
  per cases;
  suppose
A5: i < n;
    take n;
    thus thesis by A3,A4,A5;
  end;
  suppose
A6: i >= n;
    take i+1;
A7: i > n or i = n by A6,XXREAL_0:1;
    then
A8: dist(Gauge(C,i)*(1,1),Gauge(C,i)*(2,1)) <= dist(Gauge(C,n)*(1,1),
    Gauge(C,n)*(2,1)) by Th11;
A9: dist(Gauge(C,i)*(1,1),Gauge(C,i)*(1,2)) <= dist(Gauge(C,n)*(1,1),
    Gauge(C,n)*(1,2)) by A7,Th9;
    thus
A10: i < i+1 by NAT_1:13;
    then dist(Gauge(C,i+1)*(1,1),Gauge(C,i+1)*(1,2)) < dist(Gauge(C,i)*(1,1),
    Gauge(C,i)*(1,2)) by Th9;
    then
A11: dist(Gauge(C,i+1)*(1,1),Gauge(C,i+1)*(1,2)) < dist(Gauge(C,n)*(1,1),
    Gauge(C,n)*(1,2)) by A9,XXREAL_0:2;
    dist(Gauge(C,i+1)*(1,1),Gauge(C,i+1)*(2,1)) < dist(Gauge(C,i)*(1,1),
    Gauge(C,i)*(2,1)) by A10,Th11;
    then dist(Gauge(C,i+1)*(1,1),Gauge(C,i+1)*(2,1)) < dist(Gauge(C,n)*(1,1),
    Gauge(C,n)*(2,1)) by A8,XXREAL_0:2;
    hence thesis by A3,A4,A11,XXREAL_0:2;
  end;
end;

theorem Th13:
  0 < n implies upper_bound (proj2.:(L~Cage(C,n) /\ LSeg(Gauge(C,n)*(
Center Gauge(C,n),1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n)))))
 = upper_bound (
proj2.:(L~Cage(C,n) /\ Vertical_Line ((E-bound L~Cage(C,n) + W-bound L~Cage(C,n
  )) / 2)))
proof
  set f = Cage(C,n), G = Gauge(C,n), c = Center G;
  set Y = proj2.:(L~f /\ Vertical_Line ((E-bound L~f + W-bound L~f) / 2));
  set X = proj2.:(L~f /\ LSeg(G*(c,1),G*(c,len G)));
A1: len G = width G by JORDAN8:def 1;
A2: 1 <= len G by Lm3;
  assume 0 < n;
  then
A3: G*(c,1)`1 = (W-bound C + E-bound C) / 2 by A1,A2,JORDAN1G:35
    .= (W-bound L~f + E-bound L~f) / 2 by JORDAN1G:33;
  then
A4: G*(c,1) in Vertical_Line ((E-bound L~f + W-bound L~f) / 2);
A5: Y is bounded_above by JORDAN21:13;
  LSeg(G*(c,1),G*(c,len G)) meets Upper_Arc L~f by JORDAN1B:31;
  then LSeg(G*(c,1),G*(c,len G)) meets L~f by JORDAN6:61,XBOOLE_1:63;
  then
A6: L~f /\ LSeg(G*(c,1),G*(c,len G)) is non empty by XBOOLE_0:def 7;
  then
A7: X is non empty by Lm2,RELAT_1:119;
A8: c <= len G by JORDAN1B:13;
  1 <= c by JORDAN1B:11;
  then
A9: G*(c,1)`1 = G*(c,len G)`1 by A1,A2,A8,GOBOARD5:2;
  then G*(c,len G) in Vertical_Line ((E-bound L~f + W-bound L~f) / 2) by A3;
  then
A10: L~f /\ L~f /\ LSeg(G*(c,1),G*(c,len G)) c= L~f /\ Vertical_Line ((
  E-bound L~f + W-bound L~f) / 2) by A4,JORDAN1A:13,XBOOLE_1:26;
  then
A11: X c= Y by RELAT_1:123;
  then
A12: for r being Real st r in X holds r<=upper_bound Y
by A5,SEQ_4:def 1;
A13: Y is non empty by A11,A6,Lm2,RELAT_1:119,XBOOLE_1:3;
A14: for s being Real st 0<s ex r being Real st r in X &
  upper_bound Y-s < r
  proof
    let s be Real;
    assume 0<s;
    then consider r being Real such that
A15: r in Y and
A16: upper_bound Y-s<r by A5,A13,SEQ_4:def 1;
    take r;
    consider x being Point of TOP-REAL 2 such that
A17: x in L~f /\ Vertical_Line ((E-bound L~f + W-bound L~f) / 2) and
A18: proj2.x = r by A15,Lm1;
A19: x in L~f by A17,XBOOLE_0:def 4;
    x in Vertical_Line ((E-bound L~f + W-bound L~f)/2) by A17,XBOOLE_0:def 4;
    then
A20: G*(c,1)`1 = x`1 by A3,JORDAN6:31;
A21: GoB f = G by JORDAN1H:44;
    then
A22: G*(c,1)`2 <= x`2 by A8,A19,JORDAN1B:11,JORDAN5D:33;
    x`2 <= G*(c,len G)`2 by A1,A8,A19,A21,JORDAN1B:11,JORDAN5D:34;
    then x in LSeg(G*(c,1),G*(c,len G)) by A9,A20,A22,GOBOARD7:7;
    then x in L~f /\ LSeg(G*(c,1),G*(c,len G)) by A19,XBOOLE_0:def 4;
    hence r in X by A18,FUNCT_2:35;
    thus thesis by A16;
  end;
  X is bounded_above by A10,A5,RELAT_1:123,XXREAL_2:43;
  hence thesis by A7,A12,A14,SEQ_4:def 1;
end;

theorem Th14:
  0 < n implies lower_bound (proj2.:(L~Cage(C,n) /\ LSeg(Gauge(C,n)*(
Center Gauge(C,n),1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n)))))
 = lower_bound (
proj2.:(L~Cage(C,n) /\ Vertical_Line ((E-bound L~Cage(C,n) + W-bound L~Cage(C,n
  )) / 2)))
proof
  set f = Cage(C,n), G = Gauge(C,n), c = Center G;
  set Y = proj2.:(L~f /\ Vertical_Line ((E-bound L~f + W-bound L~f) / 2));
  set X = proj2.:(L~f /\ LSeg(G*(c,1),G*(c,len G)));
A1: len G = width G by JORDAN8:def 1;
A2: 1 <= len G by Lm3;
  assume 0 < n;
  then
A3: G*(c,1)`1 = (W-bound C + E-bound C) / 2 by A1,A2,JORDAN1G:35
    .= (W-bound L~f + E-bound L~f) / 2 by JORDAN1G:33;
  then
A4: G*(c,1) in Vertical_Line ((E-bound L~f + W-bound L~f) / 2);
A5: Y is bounded_below by JORDAN21:13;
  LSeg(G*(c,1),G*(c,len G)) meets Upper_Arc L~f by JORDAN1B:31;
  then LSeg(G*(c,1),G*(c,len G)) meets L~f by JORDAN6:61,XBOOLE_1:63;
  then
A6: L~f /\ LSeg(G*(c,1),G*(c,len G)) is non empty by XBOOLE_0:def 7;
  then
A7: X is non empty by Lm2,RELAT_1:119;
A8: c <= len G by JORDAN1B:13;
  1 <= c by JORDAN1B:11;
  then
A9: G*(c,1)`1 = G*(c,len G)`1 by A1,A2,A8,GOBOARD5:2;
  then G*(c,len G) in Vertical_Line ((E-bound L~f + W-bound L~f) / 2) by A3;
  then
A10: L~f /\ L~f /\ LSeg(G*(c,1),G*(c,len G)) c= L~f /\ Vertical_Line ((
  E-bound L~f + W-bound L~f) / 2) by A4,JORDAN1A:13,XBOOLE_1:26;
  then
A11: X c= Y by RELAT_1:123;
  then
A12: for r being Real st r in X holds lower_bound Y<=r
by A5,SEQ_4:def 2;
A13: Y is non empty by A11,A6,Lm2,RELAT_1:119,XBOOLE_1:3;
A14: for s being Real st 0<s ex r being Real st r in X & r<
  lower_bound Y + s
  proof
    let s be Real;
    assume 0<s;
    then consider r being Real such that
A15: r in Y and
A16: r<lower_bound Y+s by A5,A13,SEQ_4:def 2;
    take r;
    consider x being Point of TOP-REAL 2 such that
A17: x in L~f /\ Vertical_Line ((E-bound L~f + W-bound L~f) / 2) and
A18: proj2.x = r by A15,Lm1;
A19: x in L~f by A17,XBOOLE_0:def 4;
    x in Vertical_Line ((E-bound L~f + W-bound L~f)/2) by A17,XBOOLE_0:def 4;
    then
A20: G*(c,1)`1 = x`1 by A3,JORDAN6:31;
A21: GoB f = G by JORDAN1H:44;
    then
A22: G*(c,1)`2 <= x`2 by A8,A19,JORDAN1B:11,JORDAN5D:33;
    x`2 <= G*(c,len G)`2 by A1,A8,A19,A21,JORDAN1B:11,JORDAN5D:34;
    then x in LSeg(G*(c,1),G*(c,len G)) by A9,A20,A22,GOBOARD7:7;
    then x in L~f /\ LSeg(G*(c,1),G*(c,len G)) by A19,XBOOLE_0:def 4;
    hence r in X by A18,FUNCT_2:35;
    thus thesis by A16;
  end;
  X is bounded_below by A10,A5,RELAT_1:123,XXREAL_2:44;
  hence thesis by A7,A12,A14,SEQ_4:def 2;
end;

theorem
  0 < n implies UMP L~Cage(C,n) = |[ (E-bound L~Cage(C,n) + W-bound L~
Cage(C,n)) / 2, upper_bound (proj2.:(L~Cage(C,n) /\
 LSeg(Gauge(C,n)*(Center Gauge(C,n),
  1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))))) ]| by Th13;

theorem
  0 < n implies LMP L~Cage(C,n) = |[ (E-bound L~Cage(C,n) + W-bound L~
Cage(C,n)) / 2, lower_bound (proj2.:(L~Cage(C,n) /\
 LSeg(Gauge(C,n)*(Center Gauge(C,n),
  1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))))) ]| by Th14;

theorem Th17:
  (UMP C)`2 < (UMP L~Cage(C,n))`2
proof
  set p = UMP L~Cage(C,n), u = UMP C, w = (W-bound C + E-bound C) / 2;
A1: u`1 = w by EUCLID:52;
A2: p in L~Cage(C,n) by JORDAN21:30;
A3: u = |[u`1,u`2]| by EUCLID:53;
A4: p = |[p`1,p`2]| by EUCLID:53;
A5: C misses L~Cage(C,n) by JORDAN10:5;
A6: u in C by JORDAN21:30;
A7: w = (W-bound L~Cage(C,n) + E-bound L~Cage(C,n)) / 2 by JORDAN1G:33;
  then
A8: p`1 = w by EUCLID:52;
  assume
A9: not thesis;
  per cases by A9,XXREAL_0:1;
  suppose
    u`2 = p`2;
    hence thesis by A1,A8,A4,A3,A5,A6,A2,XBOOLE_0:3;
  end;
  suppose
A10: u`2 > p`2;
A11: proj2.:(L~Cage(C,n) /\ Vertical_Line w) is non empty bounded_above by A7,
JORDAN21:12,13;
A12: p`2 = upper_bound (proj2.:(L~Cage(C,n) /\ Vertical_Line w))
by A7,EUCLID:52;
A13: north_halfline p \ {p} misses L~Cage(C,n)
    proof
      assume north_halfline p \ {p} meets L~Cage(C,n);
      then consider x being object such that
A14:  x in north_halfline p \ {p} and
A15:  x in L~Cage(C,n) by XBOOLE_0:3;
      reconsider x as Point of TOP-REAL 2 by A15;
A16:  x in north_halfline p by A14,XBOOLE_0:def 5;
      then
A17:  x`2 >= p`2 by TOPREAL1:def 10;
A18:  x`1 = w by A8,A16,TOPREAL1:def 10;
      then x in Vertical_Line w;
      then
A19:  x in L~Cage(C,n) /\ Vertical_Line w by A15,XBOOLE_0:def 4;
      proj2.x = x`2 by PSCOMP_1:def 6;
      then x`2 in proj2.:(L~Cage(C,n) /\ Vertical_Line w) by A19,FUNCT_2:35;
      then
A20:  x`2 <= p`2 by A12,A11,SEQ_4:def 1;
      not x in {p} by A14,XBOOLE_0:def 5;
      then x <> p by TARSKI:def 1;
      then x`2 <> p`2 by A8,A18,TOPREAL3:6;
      hence contradiction by A17,A20,XXREAL_0:1;
    end;
    north_halfline p \ {p} is convex by JORDAN21:6;
    then
A21: north_halfline p \ {p} c= UBD L~Cage(C,n) or north_halfline p \ {p}
    c= BDD L~Cage(C,n) by A13,JORDAN1K:19;
A22: UBD L~Cage(C,n) c= UBD C by JORDAN10:13;
A23: not u in {p} by A10,TARSKI:def 1;
    u in north_halfline p by A1,A8,A10,TOPREAL1:def 10;
    then
A24: u in north_halfline p \ {p} by A23,XBOOLE_0:def 5;
A25: UBD C misses C by JORDAN21:10;
    north_halfline p is not bounded by JORDAN2C:122;
    then
A26: north_halfline p \ {p} is not bounded by JORDAN21:1,TOPREAL6:90;
    BDD L~Cage(C,n) is bounded by JORDAN2C:106;
    then u in UBD L~Cage(C,n) by A21,A26,A24,RLTOPSP1:42;
    hence thesis by A6,A22,A25,XBOOLE_0:3;
  end;
end;

theorem Th18:
  (LMP C)`2 > (LMP L~Cage(C,n))`2
proof
  set p = LMP L~Cage(C,n), u = LMP C, w = (W-bound C + E-bound C) / 2;
A1: u`1 = w by EUCLID:52;
A2: p in L~Cage(C,n) by JORDAN21:31;
A3: u = |[u`1,u`2]| by EUCLID:53;
A4: p = |[p`1,p`2]| by EUCLID:53;
A5: C misses L~Cage(C,n) by JORDAN10:5;
A6: u in C by JORDAN21:31;
A7: w = (W-bound L~Cage(C,n) + E-bound L~Cage(C,n)) / 2 by JORDAN1G:33;
  then
A8: p`1 = w by EUCLID:52;
  assume
A9: not thesis;
  per cases by A9,XXREAL_0:1;
  suppose
    u`2 = p`2;
    hence thesis by A1,A8,A4,A3,A5,A6,A2,XBOOLE_0:3;
  end;
  suppose
A10: u`2 < p`2;
A11: proj2.:(L~Cage(C,n) /\ Vertical_Line w) is non empty bounded_below by A7,
JORDAN21:12,13;
A12: p`2 = lower_bound (proj2.:(L~Cage(C,n) /\ Vertical_Line w))
by A7,EUCLID:52;
A13: south_halfline p \ {p} misses L~Cage(C,n)
    proof
      assume south_halfline p \ {p} meets L~Cage(C,n);
      then consider x being object such that
A14:  x in south_halfline p \ {p} and
A15:  x in L~Cage(C,n) by XBOOLE_0:3;
      reconsider x as Point of TOP-REAL 2 by A15;
A16:  x in south_halfline p by A14,XBOOLE_0:def 5;
      then
A17:  x`2 <= p`2 by TOPREAL1:def 12;
A18:  x`1 = w by A8,A16,TOPREAL1:def 12;
      then x in Vertical_Line w;
      then
A19:  x in L~Cage(C,n) /\ Vertical_Line w by A15,XBOOLE_0:def 4;
      proj2.x = x`2 by PSCOMP_1:def 6;
      then x`2 in proj2.:(L~Cage(C,n) /\ Vertical_Line w) by A19,FUNCT_2:35;
      then
A20:  x`2 >= p`2 by A12,A11,SEQ_4:def 2;
      not x in {p} by A14,XBOOLE_0:def 5;
      then x <> p by TARSKI:def 1;
      then x`2 <> p`2 by A8,A18,TOPREAL3:6;
      hence contradiction by A17,A20,XXREAL_0:1;
    end;
    south_halfline p \ {p} is convex by JORDAN21:7;
    then
A21: south_halfline p \ {p} c= UBD L~Cage(C,n) or south_halfline p \ {p}
    c= BDD L~Cage(C,n) by A13,JORDAN1K:19;
A22: UBD L~Cage(C,n) c= UBD C by JORDAN10:13;
A23: not u in {p} by A10,TARSKI:def 1;
    u in south_halfline p by A1,A8,A10,TOPREAL1:def 12;
    then
A24: u in south_halfline p \ {p} by A23,XBOOLE_0:def 5;
A25: UBD C misses C by JORDAN21:10;
    south_halfline p is not bounded by JORDAN2C:123;
    then
A26: south_halfline p \ {p} is not bounded by JORDAN21:1,TOPREAL6:90;
    BDD L~Cage(C,n) is bounded by JORDAN2C:106;
    then u in UBD L~Cage(C,n) by A21,A26,A24,RLTOPSP1:42;
    hence thesis by A6,A22,A25,XBOOLE_0:3;
  end;
end;

theorem Th19:
  0 < n implies ex i being Nat st 1 <= i & i <= len
  Gauge(C,n) & UMP L~Cage(C,n) = Gauge(C,n)*(Center Gauge(C,n),i)
proof
  set f = Cage(C,n), G = Gauge(C,n), w = Center G;
A1: f is_sequence_on G by JORDAN9:def 1;
A2: len G = width G by JORDAN8:def 1;
  LSeg(G*(w,1),G*(w,len G)) meets Upper_Arc L~f by JORDAN1B:31;
  then
A3: LSeg(G*(w,1),G*(w,len G)) meets L~f by JORDAN6:61,XBOOLE_1:63;
A4: w <= len G by JORDAN1B:13;
  assume
A5: 0 < n;
  then
  UMP L~f = |[ (E-bound L~f + W-bound L~f) / 2,
  upper_bound (proj2.:(L~f /\ LSeg(G
  *(w,1),G*(w,len G)))) ]| by Th13;
  then
A6: (UMP L~f)`2 = upper_bound (proj2.:(L~f /\ LSeg(G*(w,1),G*(w,len G))))
by EUCLID:52;
A7: 1 <= len G by Lm3;
A8: 1 <= w by JORDAN1B:11;
  then
A9: [w,len G] in Indices G by A2,A7,A4,MATRIX_0:30;
  [w,1] in Indices G by A2,A7,A8,A4,MATRIX_0:30;
  then consider i such that
A10: 1 <= i and
A11: i <= len G and
A12: G*(w,i)`2 = upper_bound(proj2.:(LSeg(G*(w,1),G*(w,len G)) /\ L~f))
by A1,A3,A7,A9,JORDAN1F:2;
A13: (UMP L~f)`1 = (E-bound L~f + W-bound L~f) / 2 by EUCLID:52;
  take i;
  thus 1 <= i & i <= len G by A10,A11;
  G*(w,i)`1 = (W-bound C + E-bound C) / 2 by A5,A2,A10,A11,JORDAN1G:35;
  then (UMP L~f)`1 = G*(w,i)`1 by A13,JORDAN1G:33;
  hence thesis by A12,A6,TOPREAL3:6;
end;

theorem Th20:
  0 < n implies ex i being Nat st 1 <= i & i <= len
  Gauge(C,n) & LMP L~Cage(C,n) = Gauge(C,n)*(Center Gauge(C,n),i)
proof
  set f = Cage(C,n), G = Gauge(C,n), w = Center G;
A1: f is_sequence_on G by JORDAN9:def 1;
A2: len G = width G by JORDAN8:def 1;
  LSeg(G*(w,1),G*(w,len G)) meets Upper_Arc L~f by JORDAN1B:31;
  then
A3: LSeg(G*(w,1),G*(w,len G)) meets L~f by JORDAN6:61,XBOOLE_1:63;
A4: w <= len G by JORDAN1B:13;
  assume
A5: 0 < n;
  then
  LMP L~f = |[ (E-bound L~f + W-bound L~f) / 2,
   lower_bound (proj2.:(L~f /\ LSeg(G
  *(w,1),G*(w,len G)))) ]| by Th14;
  then
A6: (LMP L~f)`2 = lower_bound (proj2.:(L~f /\ LSeg(G*(w,1),G*(w,len G))))
 by EUCLID:52;
A7: 1 <= len G by Lm3;
A8: 1 <= w by JORDAN1B:11;
  then
A9: [w,len G] in Indices G by A2,A7,A4,MATRIX_0:30;
  [w,1] in Indices G by A2,A7,A8,A4,MATRIX_0:30;
  then consider i such that
A10: 1 <= i and
A11: i <= len G and
A12: G*(w,i)`2 = lower_bound(proj2.:(LSeg(G*(w,1),G*(w,len G)) /\ L~f))
 by A1,A3,A7,A9,JORDAN1F:1;
A13: (LMP L~f)`1 = (E-bound L~f + W-bound L~f) / 2 by EUCLID:52;
  take i;
  thus 1 <= i & i <= len G by A10,A11;
  G*(w,i)`1 = (W-bound C + E-bound C) / 2 by A5,A2,A10,A11,JORDAN1G:35;
  then (LMP L~f)`1 = G*(w,i)`1 by A13,JORDAN1G:33;
  hence thesis by A12,A6,TOPREAL3:6;
end;

theorem Th21:
  0 < n implies UMP L~Cage(C,n) = UMP Upper_Arc L~Cage(C,n)
proof
  set f = Cage(C,n);
  set w = (E-bound C + W-bound C) / 2;
A1: Upper_Arc L~f c= L~f by JORDAN6:61;
A2: W-bound C + E-bound C = W-bound L~f + E-bound L~f by JORDAN1G:33;
A3: E-bound L~f = E-bound Upper_Arc L~f by JORDAN21:18;
A4: W-bound L~f = W-bound Upper_Arc L~f by JORDAN21:17;
  assume
A5: 0 < n;
  then
A6: 0+1 <= n by NAT_1:13;
  then
A7: n-'1+1 = n by XREAL_1:235;
A8: now
A9: Center Gauge(C,1) <= len Gauge(C,1) by JORDAN1B:13;
A10: Center Gauge(C,n) <= len Gauge(C,n) by JORDAN1B:13;
A11: Upper_Arc L~f \/ Lower_Arc L~f = L~f by JORDAN6:def 9;
    assume
A12: not UMP L~f in Upper_Arc L~f;
    UMP L~f in L~f by JORDAN21:30;
    then
A13: UMP L~f in Lower_Arc L~f by A12,A11,XBOOLE_0:def 3;
A14: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
A15: 1 <= Center Gauge(C,n) by JORDAN1B:11;
    consider j being Nat such that
A16: 1 <= j and
A17: j <= len Gauge(C,n) and
A18: UMP L~f = Gauge(C,n)*(Center Gauge(C,n),j) by A5,Th19;
    set a = Gauge(C,1)*(Center Gauge(C,1),len Gauge(C,1)), b = Gauge(C,n)*(
    Center Gauge(C,n),j), L = LSeg(a,b);
    len Gauge(C,1) = width Gauge(C,1) by JORDAN8:def 1;
    then L meets Upper_Arc L~f by A7,A13,A16,A17,A18,A14,JORDAN19:5;
    then consider x being object such that
A19: x in L and
A20: x in Upper_Arc L~f by XBOOLE_0:3;
    reconsider x as Point of TOP-REAL 2 by A19;
A21: a in L by RLTOPSP1:68;
A22: 1 <= len Gauge(C,1) by Lm3;
    then
A23: a`1 = w by JORDAN1A:38;
    then
A24: b`1 = w by A5,A16,A17,A22,JORDAN1A:36;
    then L is vertical by A23,SPPOL_1:16;
    then
A25: x`1 = w by A19,A23,A21,SPPOL_1:def 3;
    then x in Vertical_Line w;
    then
A26: x in Upper_Arc L~f /\ Vertical_Line w by A20,XBOOLE_0:def 4;
    then
A27: (UMP Upper_Arc L~f)`2 >= x`2 by A2,A4,A3,JORDAN21:28;
    1 <= Center Gauge(C,1) by JORDAN1B:11;
    then
A28: Gauge(C,1)*(Center Gauge(C,1),len Gauge(C,1))`2 >= Gauge(C,n)*(Center
    Gauge(C,n),len Gauge(C,n))`2 by A6,A15,A10,A9,JORDAN1A:40;
    len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
    then
    Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))`2 >= Gauge(C,n)*(Center
    Gauge(C,n),j)`2 by A16,A17,A15,A10,SPRECT_3:12;
    then a`2 >= b`2 by A28,XXREAL_0:2;
    then
A29: x`2 >= b`2 by A19,TOPREAL1:4;
    (UMP L~f)`2 >= (UMP Upper_Arc L~f)`2 by A1,A2,A4,A3,A26,JORDAN21:13,43;
    then b`2 >= x`2 by A18,A27,XXREAL_0:2;
    then b`2 = x`2 by A29,XXREAL_0:1;
    hence contradiction by A12,A18,A20,A24,A25,TOPREAL3:6;
  end;
  proj2.:(L~f /\ Vertical_Line w) is bounded_above by A2,JORDAN21:13;
  hence thesis by A1,A2,A4,A3,A8,JORDAN21:21,45;
end;

theorem Th22:
  0 < n implies LMP L~Cage(C,n) = LMP Lower_Arc L~Cage(C,n)
proof
  set f = Cage(C,n);
  set w = (E-bound C + W-bound C) / 2;
A1: Lower_Arc L~f c= L~f by JORDAN6:61;
A2: W-bound C + E-bound C = W-bound L~f + E-bound L~f by JORDAN1G:33;
A3: E-bound L~f = E-bound Lower_Arc L~f by JORDAN21:20;
A4: W-bound L~f = W-bound Lower_Arc L~f by JORDAN21:19;
  assume
A5: 0 < n;
  then
A6: 0+1 <= n by NAT_1:13;
  then
A7: n-'1+1 = n by XREAL_1:235;
A8: now
A9: Center Gauge(C,1) <= len Gauge(C,1) by JORDAN1B:13;
A10: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
A11: Upper_Arc L~f \/ Lower_Arc L~f = L~f by JORDAN6:def 9;
    assume
A12: not LMP L~f in Lower_Arc L~f;
    consider j being Nat such that
A13: 1 <= j and
A14: j <= len Gauge(C,n) and
A15: LMP L~f = Gauge(C,n)*(Center Gauge(C,n),j) by A5,Th20;
    set a = Gauge(C,1)*(Center Gauge(C,1),1), b = Gauge(C,n)*(Center Gauge(C,n
    ),j), L = LSeg(a,b);
A16: a in L by RLTOPSP1:68;
    LMP L~f in L~f by JORDAN21:31;
    then LMP L~f in Upper_Arc L~f by A12,A11,XBOOLE_0:def 3;
    then L meets Lower_Arc L~f by A7,A13,A14,A15,A10,JORDAN1J:62;
    then consider x being object such that
A17: x in L and
A18: x in Lower_Arc L~f by XBOOLE_0:3;
    reconsider x as Point of TOP-REAL 2 by A17;
A19: 1 <= Center Gauge(C,n) by JORDAN1B:11;
A20: 1 <= len Gauge(C,1) by Lm3;
    then
A21: a`1 = w by JORDAN1A:38;
    then
A22: b`1 = w by A5,A13,A14,A20,JORDAN1A:36;
    then L is vertical by A21,SPPOL_1:16;
    then
A23: x`1 = w by A17,A21,A16,SPPOL_1:def 3;
    then x in Vertical_Line w;
    then
A24: x in Lower_Arc L~f /\ Vertical_Line w by A18,XBOOLE_0:def 4;
    then
A25: (LMP Lower_Arc L~f)`2 <= x`2 by A2,A4,A3,JORDAN21:29;
A26: Center Gauge(C,n) <= len Gauge(C,n) by JORDAN1B:13;
    1 <= Center Gauge(C,1) by JORDAN1B:11;
    then
A27: Gauge(C,1)*(Center Gauge(C,1),1)`2 <= Gauge(C,n)*(Center Gauge(C, n)
    ,1)`2 by A6,A19,A26,A9,JORDAN1A:43;
    Gauge(C,n)*(Center Gauge(C,n),1)`2 <= Gauge(C,n)*(Center Gauge(C,n),j
    ) `2 by A13,A14,A10,A19,A26,SPRECT_3:12;
    then a`2 <= b`2 by A27,XXREAL_0:2;
    then
A28: x`2 <= b`2 by A17,TOPREAL1:4;
    (LMP L~f)`2 <= (LMP Lower_Arc L~f)`2 by A1,A2,A4,A3,A24,JORDAN21:13,44;
    then b`2 <= x`2 by A15,A25,XXREAL_0:2;
    then b`2 = x`2 by A28,XXREAL_0:1;
    hence contradiction by A12,A15,A18,A22,A23,TOPREAL3:6;
  end;
  proj2.:(L~f /\ Vertical_Line w) is bounded_below by A2,JORDAN21:13;
  hence thesis by A1,A2,A4,A3,A8,JORDAN21:22,46;
end;

theorem Th23:
  0 < n implies (UMP C)`2 < (UMP Upper_Arc L~Cage(C,n))`2
proof
  assume 0 < n;
  then UMP Upper_Arc L~Cage(C,n) = UMP L~Cage(C,n) by Th21;
  hence thesis by Th17;
end;

theorem Th24:
  0 < n implies (LMP Lower_Arc L~Cage(C,n))`2 < (LMP C)`2
proof
  assume 0 < n;
  then LMP Lower_Arc L~Cage(C,n) = LMP L~Cage(C,n) by Th22;
  hence thesis by Th18;
end;

theorem Th25:
  i <= j implies (UMP L~Cage(C,j))`2 <= (UMP L~Cage(C,i))`2
proof
  set w = (E-bound C + W-bound C) / 2, ui = UMP L~Cage(C,i), uj = UMP L~Cage(C
  ,j);
  assume i <= j;
  then
A1: LeftComp(Cage(C,i)) c= LeftComp(Cage(C,j)) by JORDAN1H:47;
A2: W-bound L~Cage(C,j) + E-bound L~Cage(C,j) = W-bound C + E-bound C by
JORDAN1G:33;
  then
A3: uj`2 = upper_bound (proj2.:(L~Cage(C,j) /\ Vertical_Line w)) by EUCLID:52;
  assume (UMP L~Cage(C,j))`2 > (UMP L~Cage(C,i))`2;
  then
A4: uj`2 - ui`2 > 0 by XREAL_1:50;
A5: W-bound L~Cage(C,i) + E-bound L~Cage(C,i) = W-bound C + E-bound C by
JORDAN1G:33;
  then
A6: ui`2 = upper_bound (proj2.:(L~Cage(C,i) /\ Vertical_Line w)) by EUCLID:52;
A7: proj2.:(L~Cage(C,i) /\ Vertical_Line w) is non empty bounded_above by A5,
JORDAN21:12,13;
  proj2.:(L~Cage(C,j) /\ Vertical_Line w) is non empty bounded_above by A2,
JORDAN21:12,13;
  then consider r being Real such that
A8: r in proj2.:(L~Cage(C,j) /\ Vertical_Line w) and
A9: upper_bound (proj2.:(L~Cage(C,j) /\ Vertical_Line w)) - (uj`2 - ui`2) < r
  by A4,SEQ_4:def 1;
  consider x being Point of TOP-REAL 2 such that
A10: x in L~Cage(C,j) /\ Vertical_Line w and
A11: proj2.x = r by A8,Lm1;
A12: x`2 = r by A11,PSCOMP_1:def 6;
  north_halfline x misses L~Cage(C,i)
  proof
A13: x in Vertical_Line w by A10,XBOOLE_0:def 4;
    assume north_halfline x meets L~Cage(C,i);
    then consider y being object such that
A14: y in north_halfline x and
A15: y in L~Cage(C,i) by XBOOLE_0:3;
    reconsider y as Point of TOP-REAL 2 by A15;
    y`1 = x`1 by A14,TOPREAL1:def 10
      .= w by A13,JORDAN6:31;
    then y in Vertical_Line w;
    then
A16: y in L~Cage(C,i) /\ Vertical_Line w by A15,XBOOLE_0:def 4;
    proj2.y = y`2 by PSCOMP_1:def 6;
    then y`2 in proj2.:(L~Cage(C,i) /\ Vertical_Line w) by A16,FUNCT_2:35;
    then
A17: y`2 <= ui`2 by A6,A7,SEQ_4:def 1;
    y`2 >= x`2 by A14,TOPREAL1:def 10;
    hence contradiction by A3,A9,A12,A17,XXREAL_0:2;
  end;
  then
A18: north_halfline x c= UBD L~Cage(C,i) by JORDAN2C:129;
  x in north_halfline x by TOPREAL1:38;
  then x in UBD L~Cage(C,i) by A18;
  then
A19: x in LeftComp Cage(C,i) by GOBRD14:36;
  x in L~Cage(C,j) by A10,XBOOLE_0:def 4;
  then LeftComp Cage(C,j) meets L~Cage(C,j) by A1,A19,XBOOLE_0:3;
  hence thesis by SPRECT_3:26;
end;

theorem Th26:
  i <= j implies (LMP L~Cage(C,i))`2 <= (LMP L~Cage(C,j))`2
proof
  set w = (E-bound C + W-bound C) / 2, ui = LMP L~Cage(C,i), uj = LMP L~Cage(C
  ,j);
  assume i <= j;
  then
A1: LeftComp(Cage(C,i)) c= LeftComp(Cage(C,j)) by JORDAN1H:47;
A2: W-bound L~Cage(C,j) + E-bound L~Cage(C,j) = W-bound C + E-bound C by
JORDAN1G:33;
  then
A3: uj`2 = lower_bound (proj2.:(L~Cage(C,j) /\ Vertical_Line w)) by EUCLID:52;
  assume (LMP L~Cage(C,i))`2 > (LMP L~Cage(C,j))`2;
  then
A4: ui`2 - uj`2 > 0 by XREAL_1:50;
A5: W-bound L~Cage(C,i) + E-bound L~Cage(C,i) = W-bound C + E-bound C by
JORDAN1G:33;
  then
A6: ui`2 = lower_bound (proj2.:(L~Cage(C,i) /\ Vertical_Line w)) by EUCLID:52;
A7: proj2.:(L~Cage(C,i) /\ Vertical_Line w) is non empty bounded_below by A5,
JORDAN21:12,13;
  proj2.:(L~Cage(C,j) /\ Vertical_Line w) is non empty bounded_below by A2,
JORDAN21:12,13;
  then consider r being Real such that
A8: r in proj2.:(L~Cage(C,j) /\ Vertical_Line w) and
A9: r < lower_bound (proj2.:(L~Cage(C,j) /\ Vertical_Line w)) + (ui`2 - uj`2)
  by A4,SEQ_4:def 2;
  consider x being Point of TOP-REAL 2 such that
A10: x in L~Cage(C,j) /\ Vertical_Line w and
A11: proj2.x = r by A8,Lm1;
A12: x`2 = r by A11,PSCOMP_1:def 6;
  south_halfline x misses L~Cage(C,i)
  proof
A13: x in Vertical_Line w by A10,XBOOLE_0:def 4;
    assume south_halfline x meets L~Cage(C,i);
    then consider y being object such that
A14: y in south_halfline x and
A15: y in L~Cage(C,i) by XBOOLE_0:3;
    reconsider y as Point of TOP-REAL 2 by A15;
    y`1 = x`1 by A14,TOPREAL1:def 12
      .= w by A13,JORDAN6:31;
    then y in Vertical_Line w;
    then
A16: y in L~Cage(C,i) /\ Vertical_Line w by A15,XBOOLE_0:def 4;
    proj2.y = y`2 by PSCOMP_1:def 6;
    then y`2 in proj2.:(L~Cage(C,i) /\ Vertical_Line w) by A16,FUNCT_2:35;
    then
A17: y`2 >= ui`2 by A6,A7,SEQ_4:def 2;
    y`2 <= x`2 by A14,TOPREAL1:def 12;
    hence contradiction by A3,A9,A12,A17,XXREAL_0:2;
  end;
  then
A18: south_halfline x c= UBD L~Cage(C,i) by JORDAN2C:128;
  x in south_halfline x by TOPREAL1:38;
  then x in UBD L~Cage(C,i) by A18;
  then
A19: x in LeftComp Cage(C,i) by GOBRD14:36;
  x in L~Cage(C,j) by A10,XBOOLE_0:def 4;
  then LeftComp Cage(C,j) meets L~Cage(C,j) by A1,A19,XBOOLE_0:3;
  hence thesis by SPRECT_3:26;
end;

theorem Th27:
  0 < i & i <= j implies (UMP Upper_Arc L~Cage(C,j))`2 <= (UMP
  Upper_Arc L~Cage(C,i))`2
proof
  assume that
A1: 0 < i and
A2: i <= j;
A3: (UMP Upper_Arc L~Cage(C,i))`2 = (UMP L~Cage(C,i))`2 by A1,Th21;
  (UMP Upper_Arc L~Cage(C,j))`2 = (UMP L~Cage(C,j))`2 by A1,A2,Th21;
  hence thesis by A2,A3,Th25;
end;

theorem Th28:
  0 < i & i <= j implies (LMP Lower_Arc L~Cage(C,i))`2 <= (LMP
  Lower_Arc L~Cage(C,j))`2
proof
  assume that
A1: 0 < i and
A2: i <= j;
A3: (LMP Lower_Arc L~Cage(C,i))`2 = (LMP L~Cage(C,i))`2 by A1,Th22;
  (LMP Lower_Arc L~Cage(C,j))`2 = (LMP L~Cage(C,j))`2 by A1,A2,Th22;
  hence thesis by A2,A3,Th26;
end;

begin :: On Special Points of Approximations

theorem Th29:
  W-min C in North_Arc C
proof
  reconsider w = W-min C as Point of Euclid 2 by EUCLID:67;
A1: for r being Real st r > 0 ex k being Nat st
   for m being Nat st m > k holds (Upper_Appr C).m meets Ball(w,r)
  proof
    let r be Real;
    assume r > 0;
    then r/2 > 0;
    then consider k being Nat such that
    1 < k and
A2: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(1,2)) < r/2 and
A3: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(2,1)) < r/2 by GOBRD14:11;
     reconsider k as Nat;
    take k;
    let m be Nat such that
A4: m > k;
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,2)) < dist(Gauge(C,k)*(1,1),Gauge
    (C,k)*(1,2)) by A4,Th9;
    then
A5: dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,2)) < r/2 by A2,XXREAL_0:2;
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(2,1)) < dist(Gauge(C,k)*(1,1),Gauge
    (C,k)*(2,1)) by A4,Th11;
    then
A6: dist(Gauge(C,m)*(1,1),Gauge(C,m)*(2,1)) < r/2 by A3,XXREAL_0:2;
A7: 1+1 <= len Rotate(Cage(C,m),W-min L~Cage(C,m)) by GOBOARD7:34,XXREAL_0:2;
    then
A8: left_cell(Rotate(Cage(C,m),W-min L~Cage(C,m)),1) /\ right_cell(Rotate
(Cage(C,m),W-min L~Cage(C,m)),1) = LSeg(Rotate(Cage(C,m),W-min L~Cage(C,m)),1)
    by GOBOARD5:31;
    reconsider p = W-min L~Cage(C,m) as Point of Euclid 2 by EUCLID:67;
A9: W-min L~Cage(C,m) in Upper_Arc L~Cage(C,m) by JORDAN7:1;
    Cage(C,m) is_sequence_on Gauge(C,m) by JORDAN9:def 1;
    then
A10: Rotate(Cage(C,m),W-min L~Cage(C,m)) is_sequence_on Gauge(C,m) by
REVROT_1:34;
    W-min L~Cage(C,m) in rng Cage(C,m) by SPRECT_2:43;
    then
A11: W-min L~Cage(C,m) = Rotate(Cage(C,m),W-min L~Cage(C,m))/.1 by FINSEQ_6:92;
    then Rotate(Cage(C,m),W-min L~Cage(C,m))/.1 = W-min L~Rotate(Cage(C,m),
    W-min L~Cage(C,m)) by REVROT_1:33;
    then consider i, j being Nat such that
A12: [i,j] in Indices Gauge(C,m) and
A13: [i,j+1] in Indices Gauge(C,m) and
A14: Rotate(Cage(C,m),W-min L~Cage(C,m))/.1 = Gauge(C,m)*(i,j) and
A15: Rotate(Cage(C,m),W-min L~Cage(C,m))/.(1+1) = Gauge(C,m)*(i,j+1)
    by A7,A10,JORDAN1I:21;
A16: 1 <= j by A12,MATRIX_0:32;
    i < len Gauge(C,m) by A7,A10,A12,A13,A14,A15,JORDAN1I:14;
    then
A17: i+1 <= len Gauge(C,m) by NAT_1:13;
A18: 1 <= i+1 by NAT_1:11;
    j <= width Gauge(C,m) by A12,MATRIX_0:32;
    then
A19: [i+1,j] in Indices Gauge(C,m) by A16,A18,A17,MATRIX_0:30;
    [1+1,1] in Indices Gauge(C,m) by Th7;
    then
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1+1,1)) = (E-bound C - W-bound C)/2
    |^m by Th5,GOBRD14:10;
    then dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1+1,1)) = dist(Gauge(C,m)*(i,j),
    Gauge(C,m)*(i+1,j)) by A12,A19,GOBRD14:10;
    then
A20: Gauge(C,m)*(i+1,j)`1 - Gauge(C,m)*(i,j)`1 < r/2 by A12,A19,A6,GOBRD14:5;
    [1,1+1] in Indices Gauge(C,m) by Th6;
    then
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,1+1)) = (N-bound C - S-bound C)/2
    |^m by Th5,GOBRD14:9;
    then dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,1+1)) = dist(Gauge(C,m)*(i,j),
    Gauge(C,m)*(i,j+1)) by A12,A13,GOBRD14:9;
    then Gauge(C,m)*(i,j+1)`2 - Gauge(C,m)*(i,j)`2 < r/2 by A12,A13,A5,
GOBRD14:6;
    then
A21: (Gauge(C,m)*(i+1,j)`1-Gauge(C,m)*(i,j)`1) + (Gauge(C,m)*(i,j+1)`2-
    Gauge(C,m)*(i,j)`2) < r/2 + r/2 by A20,XREAL_1:8;
A22: 1 <= i by A12,MATRIX_0:32;
    right_cell(Rotate(Cage(C,m),W-min L~Cage(C,m)),1) = right_cell(Rotate
(Cage(C,m),W-min L~Cage(C,m)),1, GoB Rotate(Cage(C,m),W-min L~Cage(C,m))) by A7
,JORDAN1H:23
      .= right_cell(Rotate(Cage(C,m),W-min L~Cage(C,m)),1,GoB Cage(C,m)) by
REVROT_1:28
      .= right_cell(Rotate(Cage(C,m),W-min L~Cage(C,m)),1,Gauge(C,m)) by
JORDAN1H:44;
    then
A23: right_cell(Rotate(Cage(C,m),W-min L~Cage(C,m)),1) = cell(Gauge(C,m),i
    ,j) by A7,A10,A12,A13,A14,A15,GOBRD13:22;
A24: j+1 <= width Gauge(C,m) by A13,MATRIX_0:32;
    Rotate(Cage(C,m),W-min L~Cage(C,m))/.1 in LSeg(Rotate(Cage(C,m),W-min
    L~Cage(C,m)),1) by A7,TOPREAL1:21;
    then
A25: W-min L~Cage(C,m) in right_cell(Rotate(Cage(C,m),W-min L~Cage (C, m))
    ,1) by A11,A8,XBOOLE_0:def 4;
    then
A26: Gauge(C,m)*(i,j)`1 <= (W-min L~Cage(C,m))`1 by A23,A22,A16,A24,A17,
JORDAN9:17;
A27: W-min C in right_cell(Rotate(Cage(C,m),W-min L~Cage(C,m)),1) by JORDAN1I:6
;
    then
A28: (W-min C)`1 <= Gauge(C,m)*(i+1,j)`1 by A23,A22,A16,A24,A17,JORDAN9:17;
A29: Gauge(C,m)*(i,j)`2 <= (W-min L~Cage(C,m))`2 by A25,A23,A22,A16,A24,A17,
JORDAN9:17;
A30: (W-min L~Cage(C,m))`1 <= Gauge(C,m)*(i+1,j)`1 by A25,A23,A22,A16,A24,A17,
JORDAN9:17;
A31: (W-min L~Cage(C,m))`2 <= Gauge(C,m)*(i,j+1)`2 by A25,A23,A22,A16,A24,A17,
JORDAN9:17;
A32: (W-min C)`2 <= Gauge(C,m)*(i,j+1)`2 by A27,A23,A22,A16,A24,A17,JORDAN9:17;
A33: Gauge(C,m)*(i,j)`2 <= (W-min C)`2 by A27,A23,A22,A16,A24,A17,JORDAN9:17;
    Gauge(C,m)*(i,j)`1 <= (W-min C)`1 by A27,A23,A22,A16,A24,A17,JORDAN9:17;
    then
    dist(W-min C,W-min L~Cage(C,m)) <= (Gauge(C,m)*(i+1,j)`1-Gauge(C,m)*(
    i,j)`1) + (Gauge(C,m)*(i,j+1)`2-Gauge(C,m)*(i,j)`2) by A28,A33,A32,A26,A30
,A29,A31,TOPREAL6:95;
    then dist(W-min C,W-min L~Cage(C,m)) < r by A21,XXREAL_0:2;
    then dist(w,p) < r by TOPREAL6:def 1;
    then
A34: p in Ball(w,r) by METRIC_1:11;
    (Upper_Appr C).m = Upper_Arc L~Cage(C,m) by JORDAN19:def 1;
    hence thesis by A9,A34,XBOOLE_0:3;
  end;
  North_Arc C = Lim_inf Upper_Appr C by JORDAN19:def 3;
  hence thesis by A1,KURATO_2:14;
end;

theorem Th30:
  E-max C in North_Arc C
proof
  reconsider w = E-max C as Point of Euclid 2 by EUCLID:67;
A1: for r being Real st r > 0
  ex k being Nat st
    for m being Nat st m > k
   holds (Upper_Appr C).m meets Ball(w,r)
  proof
    let r be Real;
    assume r > 0;
    then r/2 > 0;
    then consider k being Nat such that
    1 < k and
A2: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(1,2)) < r/2 and
A3: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(2,1)) < r/2 by GOBRD14:11;
     reconsider k as Nat;
    take k;
    let m be Nat such that
A4: m > k;
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,2)) < dist(Gauge(C,k)*(1,1),Gauge
    (C,k)*(1,2)) by A4,Th9;
    then
A5: dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,2)) < r/2 by A2,XXREAL_0:2;
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(2,1)) < dist(Gauge(C,k)*(1,1),Gauge
    (C,k)*(2,1)) by A4,Th11;
    then
A6: dist(Gauge(C,m)*(1,1),Gauge(C,m)*(2,1)) < r/2 by A3,XXREAL_0:2;
    reconsider p = E-max L~Cage(C,m) as Point of Euclid 2 by EUCLID:67;
A7: E-max L~Cage(C,m) in Upper_Arc L~Cage(C,m) by JORDAN7:1;
A8: 1+1 <= len Rotate(Cage(C,m),E-max L~Cage(C,m)) by GOBOARD7:34,XXREAL_0:2;
    then
A9: left_cell(Rotate(Cage(C,m),E-max L~Cage(C,m)),1) /\ right_cell(Rotate
(Cage(C,m),E-max L~Cage(C,m)),1) = LSeg(Rotate(Cage(C,m),E-max L~Cage(C,m)),1)
    by GOBOARD5:31;
    Cage(C,m) is_sequence_on Gauge(C,m) by JORDAN9:def 1;
    then
A10: Rotate(Cage(C,m),E-max L~Cage(C,m)) is_sequence_on Gauge(C,m) by
REVROT_1:34;
    E-max L~Cage(C,m) in rng Cage(C,m) by SPRECT_2:46;
    then
A11: E-max L~Cage(C,m) = Rotate(Cage(C,m),E-max L~Cage(C,m))/.1 by FINSEQ_6:92;
    then Rotate(Cage(C,m),E-max L~Cage(C,m))/.1 = E-max L~Rotate(Cage(C,m),
    E-max L~Cage(C,m)) by REVROT_1:33;
    then consider i, j being Nat such that
A12: [i,j+1] in Indices Gauge(C,m) and
A13: [i,j] in Indices Gauge(C,m) and
A14: Rotate(Cage(C,m),E-max L~Cage(C,m))/.1 = Gauge(C,m)*(i,j+1) and
A15: Rotate(Cage(C,m),E-max L~Cage(C,m))/.(1+1) = Gauge(C,m)*(i,j) by A8,A10,
JORDAN1I:23;
A16: i <= len Gauge(C,m) by A12,MATRIX_0:32;
    i > 1 by A8,A10,A12,A13,A14,A15,JORDAN1I:16;
    then
A17: i - 1 > 1 - 1 by XREAL_1:14;
    then
A18: i-'1 = i-1 by XREAL_0:def 2;
    then
A19: i-'1 <= len Gauge(C,m) by A16,XREAL_1:146,XXREAL_0:2;
    i - 1 in NAT by A17,INT_1:3;
    then
A20: i - 1 >= 0 + 1 by A17,NAT_1:13;
    then
A21: i-'1+1 = i by NAT_D:43;
    right_cell(Rotate(Cage(C,m),E-max L~Cage(C,m)),1) = right_cell(Rotate
(Cage(C,m),E-max L~Cage(C,m)),1, GoB Rotate(Cage(C,m),E-max L~Cage(C,m))) by A8
,JORDAN1H:23
      .= right_cell(Rotate(Cage(C,m),E-max L~Cage(C,m)),1,GoB Cage(C,m)) by
REVROT_1:28
      .= right_cell(Rotate(Cage(C,m),E-max L~Cage(C,m)),1,Gauge(C,m)) by
JORDAN1H:44;
    then
A22: right_cell(Rotate(Cage(C,m),E-max L~Cage(C,m)),1) = cell(Gauge(C,m),i
    -'1,j) by A8,A10,A12,A13,A14,A15,GOBRD13:28;
A23: j+1 <= width Gauge(C,m) by A12,MATRIX_0:32;
    1 <= j+1 by NAT_1:11;
    then
A24: [i-'1,j+1] in Indices Gauge(C,m) by A23,A20,A18,A19,MATRIX_0:30;
A25: 1 <= j by A13,MATRIX_0:32;
    j <= width Gauge(C,m) by A13,MATRIX_0:32;
    then
A26: [i-'1,j] in Indices Gauge(C,m) by A25,A20,A18,A19,MATRIX_0:30;
    [1,1+1] in Indices Gauge(C,m) by Th6;
    then
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,1+1)) = (N-bound C - S-bound C)/2
    |^m by Th5,GOBRD14:9;
    then
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,1+1)) = dist(Gauge(C,m)*(i-'1,j),
    Gauge(C,m)*(i-'1,j+1)) by A26,A24,GOBRD14:9;
    then
A27: Gauge(C,m)*(i-'1,j+1)`2 - Gauge(C,m)*(i-'1,j)`2 < r/2 by A26,A24,A5,
GOBRD14:6;
    [1+1,1] in Indices Gauge(C,m) by Th7;
    then
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1+1,1)) = (E-bound C - W-bound C)/2
    |^m by Th5,GOBRD14:10;
    then
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1+1,1)) = dist(Gauge(C,m)*(i-'1,j),
    Gauge(C,m)*(i-'1+1,j)) by A13,A21,A26,GOBRD14:10;
    then
    Gauge(C,m)*(i-'1+1,j)`1 - Gauge(C,m)*(i-'1,j)`1 < r/2 by A13,A21,A26,A6,
GOBRD14:5;
    then
A28: (Gauge(C,m)*(i-'1+1,j)`1-Gauge(C,m)*(i-'1,j)`1) + (Gauge(C,m)*(i-'1,j
    +1)`2-Gauge(C,m)*(i-'1,j)`2) < r/2 + r/2 by A27,XREAL_1:8;
A29: E-max C in right_cell(Rotate(Cage(C,m),E-max L~Cage(C,m)),1) by JORDAN1I:7
;
    then
A30: (E-max C)`1 <= Gauge(C,m)*(i-'1+1,j)`1 by A22,A25,A23,A20,A21,A16,
JORDAN9:17;
    Rotate(Cage(C,m),E-max L~Cage(C,m))/.1 in LSeg(Rotate(Cage(C,m),E-max
    L~Cage(C,m)),1) by A8,TOPREAL1:21;
    then
A31: E-max L~Cage(C,m) in right_cell(Rotate(Cage(C,m),E-max L~Cage (C, m))
    ,1) by A11,A9,XBOOLE_0:def 4;
    then
A32: Gauge(C,m)*(i-'1,j)`1 <= (E-max L~Cage(C,m))`1 by A22,A25,A23,A20,A21,A16,
JORDAN9:17;
A33: Gauge(C,m)*(i-'1,j)`2 <= (E-max L~Cage(C,m))`2 by A31,A22,A25,A23,A20,A21
,A16,JORDAN9:17;
A34: (E-max L~Cage(C,m))`1 <= Gauge(C,m)*(i-'1+1,j)`1 by A31,A22,A25,A23,A20
,A21,A16,JORDAN9:17;
A35: (E-max L~Cage(C,m))`2 <= Gauge(C,m)*(i-'1,j+1)`2 by A31,A22,A25,A23,A20
,A21,A16,JORDAN9:17;
A36: (E-max C)`2 <= Gauge(C,m)*(i-'1,j+1)`2 by A29,A22,A25,A23,A20,A21,A16,
JORDAN9:17;
A37: Gauge(C,m)*(i-'1,j)`2 <= (E-max C)`2 by A29,A22,A25,A23,A20,A21,A16,
JORDAN9:17;
    Gauge(C,m)*(i-'1,j)`1 <= (E-max C)`1 by A29,A22,A25,A23,A20,A21,A16,
JORDAN9:17;
    then
    dist(E-max C,E-max L~Cage(C,m)) <= (Gauge(C,m)*(i-'1+1,j)`1-Gauge(C,m
    )*(i-'1,j)`1) + (Gauge(C,m)*(i-'1,j+1)`2-Gauge(C,m)*(i-'1,j)`2) by A30,A37
,A36,A32,A34,A33,A35,TOPREAL6:95;
    then dist(E-max C,E-max L~Cage(C,m)) < r by A28,XXREAL_0:2;
    then dist(w,p) < r by TOPREAL6:def 1;
    then
A38: p in Ball(w,r) by METRIC_1:11;
    (Upper_Appr C).m = Upper_Arc L~Cage(C,m) by JORDAN19:def 1;
    hence thesis by A7,A38,XBOOLE_0:3;
  end;
  North_Arc C = Lim_inf Upper_Appr C by JORDAN19:def 3;
  hence thesis by A1,KURATO_2:14;
end;

theorem Th31:
  W-min C in South_Arc C
proof
  reconsider w = W-min C as Point of Euclid 2 by EUCLID:67;
A1: for r being Real st r > 0
  ex k being Nat st for m
  being Nat st m > k holds (Lower_Appr C).m meets Ball(w,r)
  proof
    let r be Real;
    assume r > 0;
    then r/2 > 0;
    then consider k being Nat such that
    1 < k and
A2: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(1,2)) < r/2 and
A3: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(2,1)) < r/2 by GOBRD14:11;
     reconsider k as Nat;
    take k;
    let m be Nat such that
A4: m > k;
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,2)) < dist(Gauge(C,k)*(1,1),Gauge
    (C,k)*(1,2)) by A4,Th9;
    then
A5: dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,2)) < r/2 by A2,XXREAL_0:2;
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(2,1)) < dist(Gauge(C,k)*(1,1),Gauge
    (C,k)*(2,1)) by A4,Th11;
    then
A6: dist(Gauge(C,m)*(1,1),Gauge(C,m)*(2,1)) < r/2 by A3,XXREAL_0:2;
A7: 1+1 <= len Rotate(Cage(C,m),W-min L~Cage(C,m)) by GOBOARD7:34,XXREAL_0:2;
    then
A8: left_cell(Rotate(Cage(C,m),W-min L~Cage(C,m)),1) /\ right_cell(Rotate
(Cage(C,m),W-min L~Cage(C,m)),1) = LSeg(Rotate(Cage(C,m),W-min L~Cage(C,m)),1)
    by GOBOARD5:31;
    reconsider p = W-min L~Cage(C,m) as Point of Euclid 2 by EUCLID:67;
A9: W-min L~Cage(C,m) in Lower_Arc L~Cage(C,m) by JORDAN7:1;
    Cage(C,m) is_sequence_on Gauge(C,m) by JORDAN9:def 1;
    then
A10: Rotate(Cage(C,m),W-min L~Cage(C,m)) is_sequence_on Gauge(C,m) by
REVROT_1:34;
    W-min L~Cage(C,m) in rng Cage(C,m) by SPRECT_2:43;
    then
A11: W-min L~Cage(C,m) = Rotate(Cage(C,m),W-min L~Cage(C,m))/.1 by FINSEQ_6:92;
    then Rotate(Cage(C,m),W-min L~Cage(C,m))/.1 = W-min L~Rotate(Cage(C,m),
    W-min L~Cage(C,m)) by REVROT_1:33;
    then consider i, j being Nat such that
A12: [i,j] in Indices Gauge(C,m) and
A13: [i,j+1] in Indices Gauge(C,m) and
A14: Rotate(Cage(C,m),W-min L~Cage(C,m))/.1 = Gauge(C,m)*(i,j) and
A15: Rotate(Cage(C,m),W-min L~Cage(C,m))/.(1+1) = Gauge(C,m)*(i,j+1)
    by A7,A10,JORDAN1I:21;
A16: 1 <= j by A12,MATRIX_0:32;
    i < len Gauge(C,m) by A7,A10,A12,A13,A14,A15,JORDAN1I:14;
    then
A17: i+1 <= len Gauge(C,m) by NAT_1:13;
A18: 1 <= i+1 by NAT_1:11;
    j <= width Gauge(C,m) by A12,MATRIX_0:32;
    then
A19: [i+1,j] in Indices Gauge(C,m) by A16,A18,A17,MATRIX_0:30;
    [1+1,1] in Indices Gauge(C,m) by Th7;
    then
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1+1,1)) = (E-bound C - W-bound C)/2
    |^m by Th5,GOBRD14:10;
    then dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1+1,1)) = dist(Gauge(C,m)*(i,j),
    Gauge(C,m)*(i+1,j)) by A12,A19,GOBRD14:10;
    then
A20: Gauge(C,m)*(i+1,j)`1 - Gauge(C,m)*(i,j)`1 < r/2 by A12,A19,A6,GOBRD14:5;
    [1,1+1] in Indices Gauge(C,m) by Th6;
    then
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,1+1)) = (N-bound C - S-bound C)/2
    |^m by Th5,GOBRD14:9;
    then dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,1+1)) = dist(Gauge(C,m)*(i,j),
    Gauge(C,m)*(i,j+1)) by A12,A13,GOBRD14:9;
    then Gauge(C,m)*(i,j+1)`2 - Gauge(C,m)*(i,j)`2 < r/2 by A12,A13,A5,
GOBRD14:6;
    then
A21: (Gauge(C,m)*(i+1,j)`1-Gauge(C,m)*(i,j)`1) + (Gauge(C,m)*(i,j+1)`2-
    Gauge(C,m)*(i,j)`2) < r/2 + r/2 by A20,XREAL_1:8;
A22: 1 <= i by A12,MATRIX_0:32;
    right_cell(Rotate(Cage(C,m),W-min L~Cage(C,m)),1) = right_cell(Rotate
(Cage(C,m),W-min L~Cage(C,m)),1, GoB Rotate(Cage(C,m),W-min L~Cage(C,m))) by A7
,JORDAN1H:23
      .= right_cell(Rotate(Cage(C,m),W-min L~Cage(C,m)),1,GoB Cage(C,m)) by
REVROT_1:28
      .= right_cell(Rotate(Cage(C,m),W-min L~Cage(C,m)),1,Gauge(C,m)) by
JORDAN1H:44;
    then
A23: right_cell(Rotate(Cage(C,m),W-min L~Cage(C,m)),1) = cell(Gauge(C,m),i
    ,j) by A7,A10,A12,A13,A14,A15,GOBRD13:22;
A24: j+1 <= width Gauge(C,m) by A13,MATRIX_0:32;
    Rotate(Cage(C,m),W-min L~Cage(C,m))/.1 in LSeg(Rotate(Cage(C,m),W-min
    L~Cage(C,m)),1) by A7,TOPREAL1:21;
    then
A25: W-min L~Cage(C,m) in right_cell(Rotate(Cage(C,m),W-min L~Cage (C, m))
    ,1) by A11,A8,XBOOLE_0:def 4;
    then
A26: Gauge(C,m)*(i,j)`1 <= (W-min L~Cage(C,m))`1 by A23,A22,A16,A24,A17,
JORDAN9:17;
A27: W-min C in right_cell(Rotate(Cage(C,m),W-min L~Cage(C,m)),1) by JORDAN1I:6
;
    then
A28: (W-min C)`1 <= Gauge(C,m)*(i+1,j)`1 by A23,A22,A16,A24,A17,JORDAN9:17;
A29: Gauge(C,m)*(i,j)`2 <= (W-min L~Cage(C,m))`2 by A25,A23,A22,A16,A24,A17,
JORDAN9:17;
A30: (W-min L~Cage(C,m))`1 <= Gauge(C,m)*(i+1,j)`1 by A25,A23,A22,A16,A24,A17,
JORDAN9:17;
A31: (W-min L~Cage(C,m))`2 <= Gauge(C,m)*(i,j+1)`2 by A25,A23,A22,A16,A24,A17,
JORDAN9:17;
A32: (W-min C)`2 <= Gauge(C,m)*(i,j+1)`2 by A27,A23,A22,A16,A24,A17,JORDAN9:17;
A33: Gauge(C,m)*(i,j)`2 <= (W-min C)`2 by A27,A23,A22,A16,A24,A17,JORDAN9:17;
    Gauge(C,m)*(i,j)`1 <= (W-min C)`1 by A27,A23,A22,A16,A24,A17,JORDAN9:17;
    then
    dist(W-min C,W-min L~Cage(C,m)) <= (Gauge(C,m)*(i+1,j)`1-Gauge(C,m)*(
    i,j)`1) + (Gauge(C,m)*(i,j+1)`2-Gauge(C,m)*(i,j)`2) by A28,A33,A32,A26,A30
,A29,A31,TOPREAL6:95;
    then dist(W-min C,W-min L~Cage(C,m)) < r by A21,XXREAL_0:2;
    then dist(w,p) < r by TOPREAL6:def 1;
    then
A34: p in Ball(w,r) by METRIC_1:11;
    (Lower_Appr C).m = Lower_Arc L~Cage(C,m) by JORDAN19:def 2;
    hence thesis by A9,A34,XBOOLE_0:3;
  end;
  South_Arc C = Lim_inf Lower_Appr C by JORDAN19:def 4;
  hence thesis by A1,KURATO_2:14;
end;

theorem Th32:
  E-max C in South_Arc C
proof
  reconsider w = E-max C as Point of Euclid 2 by EUCLID:67;
A1: for r being Real st r > 0 ex k being Nat st for m
  being Nat st m > k holds (Lower_Appr C).m meets Ball(w,r)
  proof
    let r be Real;
    assume r > 0;
    then r/2 > 0;
    then consider k being Nat such that
    1 < k and
A2: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(1,2)) < r/2 and
A3: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(2,1)) < r/2 by GOBRD14:11;
    take k;
    let m be Nat such that
A4: m > k;
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,2)) < dist(Gauge(C,k)*(1,1),Gauge
    (C,k)*(1,2)) by A4,Th9;
    then
A5: dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,2)) < r/2 by A2,XXREAL_0:2;
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(2,1)) < dist(Gauge(C,k)*(1,1),Gauge
    (C,k)*(2,1)) by A4,Th11;
    then
A6: dist(Gauge(C,m)*(1,1),Gauge(C,m)*(2,1)) < r/2 by A3,XXREAL_0:2;
    reconsider p = E-max L~Cage(C,m) as Point of Euclid 2 by EUCLID:67;
A7: E-max L~Cage(C,m) in Lower_Arc L~Cage(C,m) by JORDAN7:1;
A8: 1+1 <= len Rotate(Cage(C,m),E-max L~Cage(C,m)) by GOBOARD7:34,XXREAL_0:2;
    then
A9: left_cell(Rotate(Cage(C,m),E-max L~Cage(C,m)),1) /\ right_cell(Rotate
(Cage(C,m),E-max L~Cage(C,m)),1) = LSeg(Rotate(Cage(C,m),E-max L~Cage(C,m)),1)
    by GOBOARD5:31;
    Cage(C,m) is_sequence_on Gauge(C,m) by JORDAN9:def 1;
    then
A10: Rotate(Cage(C,m),E-max L~Cage(C,m)) is_sequence_on Gauge(C,m) by
REVROT_1:34;
    E-max L~Cage(C,m) in rng Cage(C,m) by SPRECT_2:46;
    then
A11: E-max L~Cage(C,m) = Rotate(Cage(C,m),E-max L~Cage(C,m))/.1 by FINSEQ_6:92;
    then Rotate(Cage(C,m),E-max L~Cage(C,m))/.1 = E-max L~Rotate(Cage(C,m),
    E-max L~Cage(C,m)) by REVROT_1:33;
    then consider i, j being Nat such that
A12: [i,j+1] in Indices Gauge(C,m) and
A13: [i,j] in Indices Gauge(C,m) and
A14: Rotate(Cage(C,m),E-max L~Cage(C,m))/.1 = Gauge(C,m)*(i,j+1) and
A15: Rotate(Cage(C,m),E-max L~Cage(C,m))/.(1+1) = Gauge(C,m)*(i,j) by A8,A10,
JORDAN1I:23;
A16: i <= len Gauge(C,m) by A12,MATRIX_0:32;
    i > 1 by A8,A10,A12,A13,A14,A15,JORDAN1I:16;
    then
A17: i - 1 > 1 - 1 by XREAL_1:14;
    then
A18: i-'1 = i-1 by XREAL_0:def 2;
    then
A19: i-'1 <= len Gauge(C,m) by A16,XREAL_1:146,XXREAL_0:2;
    i - 1 in NAT by A17,INT_1:3;
    then
A20: i - 1 >= 0 + 1 by A17,NAT_1:13;
    then
A21: i-'1+1 = i by NAT_D:43;
    right_cell(Rotate(Cage(C,m),E-max L~Cage(C,m)),1) = right_cell(Rotate
(Cage(C,m),E-max L~Cage(C,m)),1, GoB Rotate(Cage(C,m),E-max L~Cage(C,m))) by A8
,JORDAN1H:23
      .= right_cell(Rotate(Cage(C,m),E-max L~Cage(C,m)),1,GoB Cage(C,m)) by
REVROT_1:28
      .= right_cell(Rotate(Cage(C,m),E-max L~Cage(C,m)),1,Gauge(C,m)) by
JORDAN1H:44;
    then
A22: right_cell(Rotate(Cage(C,m),E-max L~Cage(C,m)),1) = cell(Gauge(C,m),i
    -'1,j) by A8,A10,A12,A13,A14,A15,GOBRD13:28;
A23: j+1 <= width Gauge(C,m) by A12,MATRIX_0:32;
    1 <= j+1 by NAT_1:11;
    then
A24: [i-'1,j+1] in Indices Gauge(C,m) by A23,A20,A18,A19,MATRIX_0:30;
A25: 1 <= j by A13,MATRIX_0:32;
    j <= width Gauge(C,m) by A13,MATRIX_0:32;
    then
A26: [i-'1,j] in Indices Gauge(C,m) by A25,A20,A18,A19,MATRIX_0:30;
    [1,1+1] in Indices Gauge(C,m) by Th6;
    then
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,1+1)) = (N-bound C - S-bound C)/2
    |^m by Th5,GOBRD14:9;
    then
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,1+1)) = dist(Gauge(C,m)*(i-'1,j),
    Gauge(C,m)*(i-'1,j+1)) by A26,A24,GOBRD14:9;
    then
A27: Gauge(C,m)*(i-'1,j+1)`2 - Gauge(C,m)*(i-'1,j)`2 < r/2 by A26,A24,A5,
GOBRD14:6;
    [1+1,1] in Indices Gauge(C,m) by Th7;
    then
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1+1,1)) = (E-bound C - W-bound C)/2
    |^m by Th5,GOBRD14:10;
    then
    dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1+1,1)) = dist(Gauge(C,m)*(i-'1,j),
    Gauge(C,m)*(i-'1+1,j)) by A13,A21,A26,GOBRD14:10;
    then
    Gauge(C,m)*(i-'1+1,j)`1 - Gauge(C,m)*(i-'1,j)`1 < r/2 by A13,A21,A26,A6,
GOBRD14:5;
    then
A28: (Gauge(C,m)*(i-'1+1,j)`1-Gauge(C,m)*(i-'1,j)`1) + (Gauge(C,m)*(i-'1,j
    +1)`2-Gauge(C,m)*(i-'1,j)`2) < r/2 + r/2 by A27,XREAL_1:8;
A29: E-max C in right_cell(Rotate(Cage(C,m),E-max L~Cage(C,m)),1) by JORDAN1I:7
;
    then
A30: (E-max C)`1 <= Gauge(C,m)*(i-'1+1,j)`1 by A22,A25,A23,A20,A21,A16,
JORDAN9:17;
    Rotate(Cage(C,m),E-max L~Cage(C,m))/.1 in LSeg(Rotate(Cage(C,m),E-max
    L~Cage(C,m)),1) by A8,TOPREAL1:21;
    then
A31: E-max L~Cage(C,m) in right_cell(Rotate(Cage(C,m),E-max L~Cage (C, m))
    ,1) by A11,A9,XBOOLE_0:def 4;
    then
A32: Gauge(C,m)*(i-'1,j)`1 <= (E-max L~Cage(C,m))`1 by A22,A25,A23,A20,A21,A16,
JORDAN9:17;
A33: Gauge(C,m)*(i-'1,j)`2 <= (E-max L~Cage(C,m))`2 by A31,A22,A25,A23,A20,A21
,A16,JORDAN9:17;
A34: (E-max L~Cage(C,m))`1 <= Gauge(C,m)*(i-'1+1,j)`1 by A31,A22,A25,A23,A20
,A21,A16,JORDAN9:17;
A35: (E-max L~Cage(C,m))`2 <= Gauge(C,m)*(i-'1,j+1)`2 by A31,A22,A25,A23,A20
,A21,A16,JORDAN9:17;
A36: (E-max C)`2 <= Gauge(C,m)*(i-'1,j+1)`2 by A29,A22,A25,A23,A20,A21,A16,
JORDAN9:17;
A37: Gauge(C,m)*(i-'1,j)`2 <= (E-max C)`2 by A29,A22,A25,A23,A20,A21,A16,
JORDAN9:17;
    Gauge(C,m)*(i-'1,j)`1 <= (E-max C)`1 by A29,A22,A25,A23,A20,A21,A16,
JORDAN9:17;
    then
    dist(E-max C,E-max L~Cage(C,m)) <= (Gauge(C,m)*(i-'1+1,j)`1-Gauge(C,m
    )*(i-'1,j)`1) + (Gauge(C,m)*(i-'1,j+1)`2-Gauge(C,m)*(i-'1,j)`2) by A30,A37
,A36,A32,A34,A33,A35,TOPREAL6:95;
    then dist(E-max C,E-max L~Cage(C,m)) < r by A28,XXREAL_0:2;
    then dist(w,p) < r by TOPREAL6:def 1;
    then
A38: p in Ball(w,r) by METRIC_1:11;
    (Lower_Appr C).m = Lower_Arc L~Cage(C,m) by JORDAN19:def 2;
    hence thesis by A7,A38,XBOOLE_0:3;
  end;
  South_Arc C = Lim_inf Lower_Appr C by JORDAN19:def 4;
  hence thesis by A1,KURATO_2:14;
end;

Lm4: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8;

theorem Th33:
  UMP C in North_Arc C
proof
  set w = (W-bound C + E-bound C) / 2;
  set p = UMP C;
  set U = {UMP Upper_Arc L~Cage(C,n) where n is Nat: 0 < n};
  set n0 = N-bound L~Cage(C,1);
  set H = LSeg(p,|[w,n0]|);
A1: |[w,N-bound C]|`1 = w by EUCLID:52;
A2: |[w,n0]|`1 = w by EUCLID:52;
  {UMP Upper_Arc L~Cage(C,n) where n is Nat: 0 < n} c= the
  carrier of TOP-REAL 2
  proof
    let x be object;
    assume x in {UMP Upper_Arc L~Cage(C,n) where n is Nat: 0 < n};
    then ex n being Nat st x = UMP Upper_Arc L~Cage(C,n) & 0 < n;
    hence thesis;
  end;
  then reconsider U as Subset of TOP-REAL 2;
  set q = lower_bound(proj2.:(H /\ U));
  set S = LSeg(|[w,q]|, |[w,n0]|);
A3: |[w,N-bound C]|`2 = N-bound C by EUCLID:52;
A4: |[w,n0]|`2 = n0 by EUCLID:52;
A5: for n being Nat holds (UMP Upper_Arc L~Cage(C,n))`1 = w
  proof
    let n be Nat;
A6: W-bound L~Cage(C,n) + E-bound L~Cage(C,n) = W-bound C + E-bound C by
JORDAN1G:33;
    thus (UMP Upper_Arc L~Cage(C,n))`1 = (W-bound Upper_Arc L~Cage(C,n) +
    E-bound Upper_Arc L~Cage(C,n))/2 by EUCLID:52
      .= (W-bound L~Cage(C,n) + E-bound Upper_Arc L~Cage(C,n))/2 by JORDAN21:17
      .= w by A6,JORDAN21:18;
  end;
A7: p`2 <= (UMP Upper_Arc L~Cage(C,1))`2 by Th23;
A8: LSeg(p, |[w, N-bound C]|) /\ C = {p} by JORDAN21:34;
A9: (UMP Upper_Arc L~Cage(C,1))`2 <= n0 by JORDAN21:47;
  H /\ U is bounded by TOPREAL6:89;
  then proj2.:(H /\ U) is real-bounded by JCT_MISC:14;
  then
A10: proj2.:(H /\ U) is bounded_below;
A11: p`1 = w by EUCLID:52;
A12: for n being Nat st 0 < n holds (UMP Upper_Arc L~Cage(C,n))`2
  in proj2.:(H /\ U)
  proof
    let n be Nat;
    set f = Cage(C,n);
    set s = UMP Upper_Arc L~f;
    assume
A13: 0 < n;
    then
A14: s in U;
    0+1 <= n by A13,NAT_1:13;
    then 1 < n or n = 1 by XXREAL_0:1;
    then
A15: N-bound L~Cage(C,n) <= N-bound L~Cage(C,1) by JORDAN10:7;
    s`2 <= N-bound L~f by JORDAN21:47;
    then
A16: s`2 <= n0 by A15,XXREAL_0:2;
A17: s`1 = w by A5;
    p`2 <= s`2 by A13,Th23;
    then s in H by A2,A4,A11,A16,A17,GOBOARD7:7;
    then
A18: s in H /\ U by A14,XBOOLE_0:def 4;
    s`2 = proj2.s by PSCOMP_1:def 6;
    hence thesis by A18,FUNCT_2:35;
  end;
  then
A19: (UMP Upper_Arc L~Cage(C,1))`2 in proj2.:(H /\ U);
  then q <= (UMP Upper_Arc L~Cage(C,1))`2 by A10,SEQ_4:def 2;
  then
A20: q <= n0 by A9,XXREAL_0:2;
A21: |[w,q]|`1 = w by EUCLID:52;
  then
A22: S is vertical by A2,SPPOL_1:16;
A23: |[w,q]| in S by RLTOPSP1:68;
A24: |[w,q]|`2 = q by EUCLID:52;
  per cases;
  suppose
A25: p <> |[w,q]|;
    consider S9,C9 being Subset of TopSpaceMetr Euclid 2 such that
A26: S = S9 and
A27: C = C9 and
A28: dist_min(S,C) = min_dist_min(S9,C9) by JORDAN1K:def 1;
A29: S9 is compact by A26,Lm4,COMPTS_1:23;
A30: C9 is compact by A27,Lm4,COMPTS_1:23;
A31: now
      assume
A32:  p`2 >= q;
      per cases by A32,XXREAL_0:1;
      suppose
        p`2 = q;
        hence contradiction by A25,EUCLID:52;
      end;
      suppose
        p`2 > q;
        then 0 < p`2 - q by XREAL_1:50;
        then consider r being Real such that
A33:    r in proj2.:(H /\ U) and
A34:    r < q+(p`2 - q) by A10,A19,SEQ_4:def 2;
        consider t being Point of TOP-REAL 2 such that
A35:    t in H /\ U and
A36:    proj2.t = r by A33,Lm1;
A37:    t in H by A35,XBOOLE_0:def 4;
A38:    p`2 <= n0 by A9,A7,XXREAL_0:2;
        t`2 = r by A36,PSCOMP_1:def 6;
        hence contradiction by A4,A34,A38,A37,TOPREAL1:4;
      end;
    end;
    S misses C
    proof
      assume S meets C;
      then consider x being object such that
A39:  x in S and
A40:  x in C by XBOOLE_0:3;
      reconsider x as Point of TOP-REAL 2 by A39;
A41:  x`2 <= N-bound C by A40,PSCOMP_1:24;
A42:  x`1 = w by A21,A23,A22,A39,SPPOL_1:def 3;
A43:  q <= x`2 by A4,A24,A20,A39,TOPREAL1:4;
      then p`2 < x`2 by A31,XXREAL_0:2;
      then x in LSeg(p, |[w, N-bound C]|) by A1,A3,A11,A41,A42,GOBOARD7:7;
      then x in {p} by A8,A40,XBOOLE_0:def 4;
      hence contradiction by A31,A43,TARSKI:def 1;
    end;
    then dist_min(S,C) > 0 by A26,A27,A28,A29,A30,JGRAPH_1:38;
    then dist_min(S,C)/2 > 0;
    then consider k being Nat such that
A44: 1 < k and
A45: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(1,2)) < dist_min(S,C)/2 and
A46: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(2,1)) < dist_min(S,C)/2 by GOBRD14:11;
    set f = Cage(C,k), G = Gauge(C,k);
    set s = UMP Upper_Arc L~f;
A47: s`2 <= N-bound L~f by JORDAN21:47;
A48: dist(G*(1,1),G*(1+1,1)) + dist(G*(1,1),G*(1,1+1)) < dist_min(S,C)/2 +
    dist_min(S,C)/2 by A45,A46,XREAL_1:8;
    N-bound L~Cage(C,k) <= N-bound L~Cage(C,1) by A44,JORDAN10:7;
    then
A49: s`2 <= n0 by A47,XXREAL_0:2;
    s`2 in proj2.:(H /\ U) by A12,A44;
    then
A50: q <= s`2 by A10,SEQ_4:def 2;
    [1,1+1] in Indices G by Th6;
    then
A51: dist(G*(1,1),G*(1,1+1)) = (N-bound C - S-bound C)/2|^k by Th5,GOBRD14:9;
    [1+1,1] in Indices G by Th7;
    then
A52: dist(G*(1,1),G*(1+1,1)) = (E-bound C - W-bound C)/2|^k by Th5,GOBRD14:10;
A53: s in Upper_Arc L~f by JORDAN21:30;
    Upper_Arc L~f c= L~f by JORDAN6:61;
    then consider i being Nat such that
A54: 1 <= i and
A55: i+1 <= len f and
A56: s in LSeg(f,i) by A53,SPPOL_2:13;
A57: f is_sequence_on G by JORDAN9:def 1;
    then consider i1,j1,i2,j2 being Nat such that
A58: [i1,j1] in Indices G and
A59: f/.i = G*(i1,j1) and
A60: [i2,j2] in Indices G and
A61: f/.(i+1) = G*(i2,j2) and
A62: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
    or i1 = i2 & j1 = j2+1 by A54,A55,JORDAN8:3;
A63: 1 <= i1 by A58,MATRIX_0:32;
    right_cell(f,i,G) meets C by A54,A55,JORDAN9:31;
    then consider c being object such that
A64: c in right_cell(f,i,G) and
A65: c in C by XBOOLE_0:3;
    reconsider c as Point of TOP-REAL 2 by A65;
    reconsider s9 = s, c9 = c as Point of Euclid 2 by EUCLID:67;
    s`1 = w by A5;
    then s in S by A2,A4,A21,A24,A49,A50,GOBOARD7:7;
    then
A66: min_dist_min(S9,C9) <= dist(s9,c9) by A26,A27,A29,A30,A65,WEIERSTR:34;
A67: dist(s9,c9) = dist(s,c) by TOPREAL6:def 1;
A68: 1 <= j2 by A60,MATRIX_0:32;
    left_cell(f,i,G) /\ right_cell(f,i,G) = LSeg(f,i) by A54,A55,A57,GOBRD13:29
;
    then
A69: s in right_cell(f,i,G) by A56,XBOOLE_0:def 4;
A70: j2 <= width G by A60,MATRIX_0:32;
A71: j2+1+1<>j2;
A72: 1 <= i2 by A60,MATRIX_0:32;
A73: j1 <= width G by A58,MATRIX_0:32;
A74: 1 <= j1+1 by NAT_1:11;
A75: i1+1<>i1+0;
A76: i1 <= len G by A58,MATRIX_0:32;
A77: i2 <= len G by A60,MATRIX_0:32;
A78: i2+1+1<>i2;
A79: 1 <= j1 by A58,MATRIX_0:32;
A80: 1 <= i1+1 by NAT_1:11;
    now
      per cases by A62;
      suppose
A81:    i1 = i2 & j1+1 = j2;
        then
A82:    dist(G*(i1,j1),G*(i1,j1+1)) = (N-bound C - S-bound C)/2|^k by A58,A60,
GOBRD14:9;
A83:    dist(G*(i1,j1),G*(i1,j1+1)) = G*(i1,j1+1)`2 - G*(i1,j1)`2 by A58,A60
,A81,GOBRD14:6;
        i1 < len G by A54,A55,A58,A59,A60,A61,A81,JORDAN10:1;
        then
A84:    i1+1 <= len G by NAT_1:13;
        then
A85:    [i1+1,j1] in Indices G by A79,A80,A73,MATRIX_0:30;
        then
A86:    dist(G*(i1,j1),G*(i1+1,j1)) = G*(i1+1,j1)`1 - G*(i1,j1)`1 by A58,
GOBRD14:5;
A87:    dist(G*(i1,j1),G*(i1+1,j1)) = (E-bound C - W-bound C)/2|^k by A58,A85,
GOBRD14:10;
A88:    j1+1 <= width G by A60,A81,MATRIX_0:32;
A89:    right_cell(f,i,G) = cell(G,i1,j1) by A54,A55,A57,A58,A59,A60,A61,A75
,A71,A81,GOBRD13:def 2;
        then
A90:    c`1 <= G*(i1+1,j1)`1 by A64,A63,A79,A88,A84,JORDAN9:17;
A91:    s`2 <= G*(i1,j1+1)`2 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A92:    G*(i1,j1)`2 <= s`2 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A93:    s`1 <= G*(i1+1,j1)`1 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A94:    G*(i1,j1)`1 <= s`1 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A95:    c`2 <= G*(i1,j1+1)`2 by A64,A63,A79,A88,A84,A89,JORDAN9:17;
A96:    G*(i1,j1)`2 <= c`2 by A64,A63,A79,A88,A84,A89,JORDAN9:17;
        G*(i1,j1)`1 <= c`1 by A64,A63,A79,A88,A84,A89,JORDAN9:17;
        then dist(s,c) <= (G*(i1+1,j1)`1-G*(i1,j1)`1) + (G*(i1,j1+1)`2- G*(i1
        ,j1)`2) by A90,A96,A95,A94,A93,A92,A91,TOPREAL6:95;
        hence contradiction by A28,A48,A66,A67,A51,A52,A86,A83,A82,A87,
XXREAL_0:2;
      end;
      suppose
A97:    i1+1 = i2 & j1 = j2;
        then 1 < j1 by A54,A55,A58,A59,A60,A61,JORDAN10:3;
        then
A98:    1 <= j1-'1 by NAT_D:49;
        then
A99:    j1-'1+1 = j1 by NAT_D:43;
A100:   j1-'1 <= width G by A73,NAT_D:44;
        then
A101:   [i1,j1-'1] in Indices G by A63,A76,A98,MATRIX_0:30;
        then
A102:   dist(G*(i1,j1-'1),G*(i1,j1-'1+1)) = G*(i1,j1-'1+1)`2 - G*(i1,j1
        -'1)`2 by A58,A99,GOBRD14:6;
A103:   [i1+1,j1-'1] in Indices G by A72,A77,A97,A98,A100,MATRIX_0:30;
        then
A104:   dist(G*(i1,j1-'1),G*(i1+1,j1-'1)) = G*(i1+1,j1-'1)`1 - G*( i1,
        j1-'1)`1 by A101,GOBRD14:5;
A105:   dist(G*(i1,j1-'1),G*(i1,j1-'1+1)) = (N-bound C - S-bound C)/2|^k
        by A58,A99,A101,GOBRD14:9;
A106:   dist(G*(i1,j1-'1),G*(i1+1,j1-'1)) = (E-bound C - W-bound C)/2|^k
        by A101,A103,GOBRD14:10;
A107:   i1+1 <= len G by A60,A97,MATRIX_0:32;
A108:   right_cell(f,i,G) = cell(G,i1,j1-'1) by A54,A55,A57,A58,A59,A60,A61,A75
,A78,A97,GOBRD13:def 2;
        then
A109:   c`1 <= G*(i1+1,j1-'1)`1 by A64,A63,A73,A107,A98,A99,JORDAN9:17;
A110:   s`2 <= G*(i1,j1-'1+1)`2 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A111:   G*(i1,j1-'1)`2 <= s`2 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A112:   s`1 <= G*(i1+1,j1-'1)`1 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A113:   G*(i1,j1-'1)`1 <= s`1 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A114:   c`2 <= G*(i1,j1-'1+1)`2 by A64,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A115:   G*(i1,j1-'1)`2 <= c`2 by A64,A63,A73,A107,A98,A99,A108,JORDAN9:17;
        G*(i1,j1-'1)`1 <= c`1 by A64,A63,A73,A107,A98,A99,A108,JORDAN9:17;
        then dist(s,c) <= (G*(i1+1,j1-'1)`1-G*(i1,j1-'1)`1) + (G*(i1,j1-'1+1)
        `2-G*(i1,j1-'1)`2) by A109,A115,A114,A113,A112,A111,A110,TOPREAL6:95;
        hence contradiction by A28,A48,A66,A67,A51,A52,A104,A102,A105,A106,
XXREAL_0:2;
      end;
      suppose
A116:   i1 = i2+1 & j1 = j2;
        then
A117:   dist(G*(i2,j2),G*(i2+1,j2)) = (E-bound C - W-bound C)/2|^k by A58,A60,
GOBRD14:10;
A118:   dist(G*(i2,j2),G*(i2+1,j2)) = G*(i2+1,j2)`1 - G*(i2,j2)`1 by A58,A60
,A116,GOBRD14:5;
A119:   i2+1 <= len G by A58,A116,MATRIX_0:32;
        j1 < width G by A54,A55,A58,A59,A60,A61,A116,JORDAN10:4;
        then
A120:   j1+1 <= width G by NAT_1:13;
        then
A121:   [i2,j2+1] in Indices G by A72,A74,A77,A116,MATRIX_0:30;
        then
A122:   dist(G*(i2,j2),G*(i2,j2+1)) = G*(i2,j2+1)`2 - G*(i2,j2)`2 by A60,
GOBRD14:6;
A123:   right_cell(f,i,G) = cell(G,i2,j2) by A54,A55,A57,A58,A59,A60,A61,A75
,A78,A116,GOBRD13:def 2;
        then
A124:   c`1 <= G*(i2+1,j2)`1 by A64,A79,A72,A116,A119,A120,JORDAN9:17;
A125:   s`2 <= G*(i2,j2+1)`2 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A126:   G*(i2,j2)`2 <= c`2 by A64,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A127:   dist(G*(i2,j2),G*(i2,j2+1)) = (N-bound C - S-bound C)/2|^k by A60,A121,
GOBRD14:9;
A128:   G*(i2,j2)`2 <= s`2 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A129:   s`1 <= G*(i2+1,j2)`1 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A130:   G*(i2,j2)`1 <= s`1 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A131:   c`2 <= G*(i2,j2+1)`2 by A64,A79,A72,A116,A119,A120,A123,JORDAN9:17;
        G*(i2,j2)`1 <= c`1 by A64,A79,A72,A116,A119,A120,A123,JORDAN9:17;
        then dist(s,c) <= (G*(i2+1,j2)`1-G*(i2,j2)`1) + (G*(i2,j2+1)`2- G*(i2
        ,j2)`2) by A124,A126,A131,A130,A129,A128,A125,TOPREAL6:95;
        hence contradiction by A28,A48,A66,A67,A51,A52,A118,A122,A127,A117,
XXREAL_0:2;
      end;
      suppose
A132:   i1 = i2 & j1 = j2+1;
        then 1 < i1 by A54,A55,A58,A59,A60,A61,JORDAN10:2;
        then
A133:   1 <= i1-'1 by NAT_D:49;
A134:   i1-'1 <= len G by A76,NAT_D:44;
        then
A135:   [i1-'1,j2] in Indices G by A68,A70,A133,MATRIX_0:30;
A136:   [i1-'1,j2+1] in Indices G by A79,A73,A132,A133,A134,MATRIX_0:30;
        then
A137:   dist(G*(i1-'1,j2),G*(i1-'1,j2+1)) = G*(i1-'1,j2+1)`2 - G*( i1 -'
        1,j2)`2 by A135,GOBRD14:6;
A138:   dist(G*(i1-'1,j2),G*(i1-'1,j2+1)) = (N-bound C - S-bound C)/2|^k
        by A135,A136,GOBRD14:9;
A139:   j2+1 <= width G by A58,A132,MATRIX_0:32;
A140:   i1-'1+1 = i1 by A133,NAT_D:43;
        then
A141:   [i1-'1+1,j2] in Indices G by A63,A68,A76,A70,MATRIX_0:30;
        then
A142:   dist(G*(i1-'1,j2),G*(i1-'1+1,j2)) = G*(i1-'1+1,j2)`1 - G*( i1 -'
        1,j2)`1 by A135,GOBRD14:5;
A143:   right_cell(f,i,G) = cell(G,i1-'1,j2) by A54,A55,A57,A58,A59,A60,A61,A75
,A71,A132,GOBRD13:def 2;
        then
A144:   c`1 <= G*(i1-'1+1,j2)`1 by A64,A68,A76,A139,A133,A140,JORDAN9:17;
A145:   s`2 <= G*(i1-'1,j2+1)`2 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A146:   G*(i1-'1,j2)`2 <= s`2 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A147:   s`1 <= G*(i1-'1+1,j2)`1 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A148:   G*(i1-'1,j2)`1 <= s`1 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A149:   c`2 <= G*(i1-'1,j2+1)`2 by A64,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A150:   G*(i1-'1,j2)`2 <= c`2 by A64,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A151:   dist(G*(i1-'1,j2),G*(i1-'1+1,j2)) = (E-bound C - W-bound C)/2|^k
        by A135,A141,GOBRD14:10;
        G*(i1-'1,j2)`1 <= c`1 by A64,A68,A76,A139,A133,A140,A143,JORDAN9:17;
        then dist(s,c) <= (G*(i1-'1+1,j2)`1-G*(i1-'1,j2)`1) + (G*(i1-'1,j2+1)
        `2-G*(i1-'1,j2)`2) by A144,A150,A149,A148,A147,A146,A145,TOPREAL6:95;
        hence contradiction by A28,A48,A66,A67,A51,A52,A142,A137,A138,A151,
XXREAL_0:2;
      end;
    end;
    hence thesis;
  end;
  suppose
    p = |[w,q]|;
    then
A152: p`2 = q by EUCLID:52;
A153: ex S being Real_Sequence of 2 st S is convergent & (for x being
    Nat holds S.x in (Upper_Appr C).x) & p = lim S
    proof
      set R = {(UMP Upper_Arc L~Cage(C,n))`2 where n is Nat: 0 < n};
      R c= REAL
      proof
        let x be object;
        assume x in R;
        then ex n being Nat st x = (UMP Upper_Arc L~Cage(C,n))`2 &
        0 < n;
        hence thesis by XREAL_0:def 1;
      end;
      then reconsider R as Subset of REAL;
      deffunc f(Nat) = UMP Upper_Arc L~Cage(C,$1);
      reconsider pp=p as Element of REAL 2 by EUCLID:22;
      reconsider p1=p as Element of TOP-REAL 2;
A154: for x being Element of NAT holds f(x) is Element of REAL 2 by EUCLID:22;
      consider S being sequence of  REAL 2 such that
A155: for n being Element of NAT holds S.n = f(n) from FUNCT_2:sch 9
      (A154);
      the carrier of TOP-REAL 2 = REAL 2 by EUCLID:22;
      then reconsider SS=S as Real_Sequence of 2;
      take SS;
A156: R is bounded_below
      proof
        take q;
        let r be ExtReal;
        assume r in R;
        then ex n being Nat st r = (UMP Upper_Arc L~Cage(C,n))`2 &
        0 < n;
        then r in proj2.:(H /\ U) by A12;
        hence thesis by A10,SEQ_4:def 2;
      end;
A157: (UMP Upper_Arc L~Cage(C,1))`2 in R;
A158: for r being Real st 0<r ex n being Nat st for m being
      Nat st n<=m holds |. S.m-pp .| < r
      proof
A159:   for s being Real st 0<s ex r being Real st r in R & r<q+s
        proof
          let s be Real;
          assume 0<s;
          then consider r being Real such that
A160:     r in proj2.:(H /\ U) and
A161:     r<q+s by A10,A19,SEQ_4:def 2;
          take r;
          consider x being Point of TOP-REAL 2 such that
A162:     x in H /\ U and
A163:     proj2.x = r by A160,Lm1;
          x in U by A162,XBOOLE_0:def 4;
          then consider n being Nat such that
A164:     x = UMP Upper_Arc L~Cage(C,n) and
A165:     0 < n;
          r = (UMP Upper_Arc L~Cage(C,n))`2 by A163,A164,PSCOMP_1:def 6;
          hence thesis by A161,A165;
        end;
        let r be Real;
        assume 0 < r;
        then consider v being Real such that
A166:   v in R and
A167:   v < lower_bound R + r by A157,A156,SEQ_4:def 2;
A168:   v - lower_bound R < lower_bound R + r - lower_bound R
 by A167,XREAL_1:14;
        consider n being Nat such that
A169:   v = (UMP Upper_Arc L~Cage(C,n))`2 and
A170:   0 < n by A166;
        take n;
        let m be Nat;
        reconsider Sm = S.m as Element of TOP-REAL 2 by EUCLID:22;
A171:     m in NAT by ORDINAL1:def 12;
        assume
A172:   n <= m;
        then (UMP Upper_Arc L~Cage(C,m))`2 <= (UMP Upper_Arc L~Cage(C,n))`2
        by A170,Th27;
        then (Sm)`2 <= v by A155,A169,A171;
        then
A173:   (Sm)`2 - p`2 <= v - p`2 by XREAL_1:13;
        reconsider SSm = Sm as Point of TOP-REAL 2;
A174:   SSm-p1 = S.m-pp;
A175:   S.m = UMP Upper_Arc L~Cage(C,m) by A155,A171;
        then (Sm)`1 = w by A5;
        then |.(Sm)`1-p`1.| = 0 by A11,ABSVALUE:def 1;
        then
A176:   |. S.m-pp .|<=0+|.(Sm)`2-p`2.| by A174,JGRAPH_1:32;
        0 < (Sm)`2-p`2 by A170,A175,A172,Th23,XREAL_1:50;
        then
A177:   |. S.m-pp .|<=(Sm)`2-p`2 by A176,ABSVALUE:def 1;
        for r being Real st r in R holds q<=r
        proof
          let r be Real;
          assume r in R;
          then ex n being Nat st r = (UMP Upper_Arc L~Cage(C,n))`2
          & 0 < n;
          then r in proj2.:(H /\ U) by A12;
          hence thesis by A10,SEQ_4:def 2;
        end;
        then lower_bound R = q by A157,A156,A159,SEQ_4:def 2;
        then (Sm)`2-p`2 < r by A152,A168,A173,XXREAL_0:2;
        hence thesis by A177,XXREAL_0:2;
      end;
      thus
A178: SS is convergent
      proof
        take p;
        let r be Real;
        assume 0<r;
        then consider n being Nat such that
A179:   for m being Nat st n<=m holds |. S.m-pp .| < r by A158;
        take n;
        let m be Nat;
        assume n<=m;
        then |. S.m-pp .| < r by A179;
        hence |.SS.m-p.| < r;
      end;
      hereby
        let x be Nat;
A180:     x in NAT by ORDINAL1:def 12;
A181:   (Upper_Appr C).x = Upper_Arc L~Cage(C,x) by JORDAN19:def 1;
        S.x = UMP Upper_Arc L~Cage(C,x) by A155,A180;
        hence SS.x in (Upper_Appr C).x by A181,JORDAN21:30;
      end;
      for r being Real st 0<r
ex n st for m st n<=m holds |.SS.m-p.| < r
      proof
        let r be Real;
        assume 0<r;
        then consider n being Nat such that
A182:   for m being Nat st n<=m holds |. S.m-pp .| < r by A158;
        take n;
        let m be Nat;
        assume n<=m;
        then |. S.m-pp .| < r by A182;
        hence |.SS.m-p.| < r;
      end;
      hence p = lim SS by A178,TOPRNS_1:def 9;
    end;
    North_Arc C = Lim_inf Upper_Appr C by JORDAN19:def 3;
    hence thesis by A153,KURATO_2:21;
  end;
end;

theorem Th34:
  LMP C in South_Arc C
proof
  set w = (W-bound C + E-bound C) / 2;
  set p = LMP C;
  set U = {LMP Lower_Arc L~Cage(C,n) where n is Nat: 0 < n};
  set n0 = S-bound L~Cage(C,1);
  set H = LSeg(p,|[w,n0]|);
A1: |[w,S-bound C]|`1 = w by EUCLID:52;
A2: |[w,n0]|`1 = w by EUCLID:52;
  {LMP Lower_Arc L~Cage(C,n) where n is Nat: 0 < n} c= the
  carrier of TOP-REAL 2
  proof
    let x be object;
    assume x in {LMP Lower_Arc L~Cage(C,n) where n is Nat: 0 < n};
    then ex n being Nat st x = LMP Lower_Arc L~Cage(C,n) & 0 < n;
    hence thesis;
  end;
  then reconsider U as Subset of TOP-REAL 2;
  set q = upper_bound(proj2.:(H /\ U));
  set S = LSeg(|[w,q]|, |[w,n0]|);
A3: |[w,S-bound C]|`2 = S-bound C by EUCLID:52;
A4: |[w,n0]|`2 = n0 by EUCLID:52;
A5: for n being Nat holds (LMP Lower_Arc L~Cage(C,n))`1 = w
  proof
    let n be Nat;
A6: W-bound L~Cage(C,n) + E-bound L~Cage(C,n) = W-bound C + E-bound C by
JORDAN1G:33;
    thus (LMP Lower_Arc L~Cage(C,n))`1 = (W-bound Lower_Arc L~Cage(C,n) +
    E-bound Lower_Arc L~Cage(C,n))/2 by EUCLID:52
      .= (W-bound L~Cage(C,n) + E-bound Lower_Arc L~Cage(C,n))/2 by JORDAN21:19
      .= w by A6,JORDAN21:20;
  end;
A7: p`2 >= (LMP Lower_Arc L~Cage(C,1))`2 by Th24;
A8: LSeg(p, |[w, S-bound C]|) /\ C = {p} by JORDAN21:35;
A9: (LMP Lower_Arc L~Cage(C,1))`2 >= n0 by JORDAN21:48;
  H /\ U is bounded by TOPREAL6:89;
  then proj2.:(H /\ U) is real-bounded by JCT_MISC:14;
  then
A10: proj2.:(H /\ U) is bounded_above;
A11: p`1 = w by EUCLID:52;
A12: for n being Nat st 0 < n holds (LMP Lower_Arc L~Cage(C,n))`2
  in proj2.:(H /\ U)
  proof
    let n be Nat;
    set f = Cage(C,n);
    set s = LMP Lower_Arc L~f;
    assume
A13: 0 < n;
    then
A14: s in U;
    0+1 <= n by A13,NAT_1:13;
    then n = 1 or n > 1 by XXREAL_0:1;
    then
A15: S-bound L~Cage(C,n) >= S-bound L~Cage(C,1) by JORDAN1A:69;
    S-bound L~f <= s`2 by JORDAN21:48;
    then
A16: s`2 >= n0 by A15,XXREAL_0:2;
A17: s`1 = w by A5;
    p`2 >= s`2 by A13,Th24;
    then s in H by A2,A4,A11,A16,A17,GOBOARD7:7;
    then
A18: s in H /\ U by A14,XBOOLE_0:def 4;
    s`2 = proj2.s by PSCOMP_1:def 6;
    hence thesis by A18,FUNCT_2:35;
  end;
  then
A19: (LMP Lower_Arc L~Cage(C,1))`2 in proj2.:(H /\ U);
  then q >= (LMP Lower_Arc L~Cage(C,1))`2 by A10,SEQ_4:def 1;
  then
A20: q >= n0 by A9,XXREAL_0:2;
A21: |[w,q]|`1 = w by EUCLID:52;
  then
A22: S is vertical by A2,SPPOL_1:16;
A23: |[w,q]| in S by RLTOPSP1:68;
A24: |[w,q]|`2 = q by EUCLID:52;
  per cases;
  suppose
A25: p <> |[w,q]|;
    consider S9,C9 being Subset of TopSpaceMetr Euclid 2 such that
A26: S = S9 and
A27: C = C9 and
A28: dist_min(S,C) = min_dist_min(S9,C9) by JORDAN1K:def 1;
A29: S9 is compact by A26,Lm4,COMPTS_1:23;
A30: C9 is compact by A27,Lm4,COMPTS_1:23;
A31: now
      assume
A32:  p`2 <= q;
      per cases by A32,XXREAL_0:1;
      suppose
        p`2 = q;
        hence contradiction by A25,EUCLID:52;
      end;
      suppose
        p`2 < q;
        then 0 < q - p`2 by XREAL_1:50;
        then consider r being Real such that
A33:    r in proj2.:(H /\ U) and
A34:    q-(q-p`2) < r by A10,A19,SEQ_4:def 1;
        consider t being Point of TOP-REAL 2 such that
A35:    t in H /\ U and
A36:    proj2.t = r by A33,Lm1;
A37:    t in H by A35,XBOOLE_0:def 4;
A38:    p`2 >= n0 by A9,A7,XXREAL_0:2;
        t`2 = r by A36,PSCOMP_1:def 6;
        hence contradiction by A4,A34,A38,A37,TOPREAL1:4;
      end;
    end;
    S misses C
    proof
      assume S meets C;
      then consider x being object such that
A39:  x in S and
A40:  x in C by XBOOLE_0:3;
      reconsider x as Point of TOP-REAL 2 by A39;
A41:  x`2 >= S-bound C by A40,PSCOMP_1:24;
A42:  x`1 = w by A21,A23,A22,A39,SPPOL_1:def 3;
A43:  q >= x`2 by A4,A24,A20,A39,TOPREAL1:4;
      then p`2 > x`2 by A31,XXREAL_0:2;
      then x in LSeg(p, |[w, S-bound C]|) by A1,A3,A11,A41,A42,GOBOARD7:7;
      then x in {p} by A8,A40,XBOOLE_0:def 4;
      hence contradiction by A31,A43,TARSKI:def 1;
    end;
    then dist_min(S,C) > 0 by A26,A27,A28,A29,A30,JGRAPH_1:38;
    then dist_min(S,C)/2 > 0;
    then consider k being Nat such that
A44: 1 < k and
A45: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(1,2)) < dist_min(S,C)/2 and
A46: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(2,1)) < dist_min(S,C)/2 by GOBRD14:11;
    set f = Cage(C,k), G = Gauge(C,k);
    set s = LMP Lower_Arc L~f;
A47: s`2 >= S-bound L~f by JORDAN21:48;
A48: dist(G*(1,1),G*(1+1,1)) + dist(G*(1,1),G*(1,1+1)) < dist_min(S,C)/2 +
    dist_min(S,C)/2 by A45,A46,XREAL_1:8;
    S-bound L~Cage(C,k) >= S-bound L~Cage(C,1) by A44,JORDAN1A:69;
    then
A49: s`2 >= n0 by A47,XXREAL_0:2;
    s`2 in proj2.:(H /\ U) by A12,A44;
    then
A50: q >= s`2 by A10,SEQ_4:def 1;
    [1,1+1] in Indices G by Th6;
    then
A51: dist(G*(1,1),G*(1,1+1)) = (N-bound C - S-bound C)/2|^k by Th5,GOBRD14:9;
    [1+1,1] in Indices G by Th7;
    then
A52: dist(G*(1,1),G*(1+1,1)) = (E-bound C - W-bound C)/2|^k by Th5,GOBRD14:10;
A53: s in Lower_Arc L~f by JORDAN21:31;
    Lower_Arc L~f c= L~f by JORDAN6:61;
    then consider i being Nat such that
A54: 1 <= i and
A55: i+1 <= len f and
A56: s in LSeg(f,i) by A53,SPPOL_2:13;
A57: f is_sequence_on G by JORDAN9:def 1;
    then consider i1,j1,i2,j2 being Nat such that
A58: [i1,j1] in Indices G and
A59: f/.i = G*(i1,j1) and
A60: [i2,j2] in Indices G and
A61: f/.(i+1) = G*(i2,j2) and
A62: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
    or i1 = i2 & j1 = j2+1 by A54,A55,JORDAN8:3;
A63: 1 <= i1 by A58,MATRIX_0:32;
    right_cell(f,i,G) meets C by A54,A55,JORDAN9:31;
    then consider c being object such that
A64: c in right_cell(f,i,G) and
A65: c in C by XBOOLE_0:3;
    reconsider c as Point of TOP-REAL 2 by A65;
    reconsider s9 = s, c9 = c as Point of Euclid 2 by EUCLID:67;
    s`1 = w by A5;
    then s in S by A2,A4,A21,A24,A49,A50,GOBOARD7:7;
    then
A66: min_dist_min(S9,C9) <= dist(s9,c9) by A26,A27,A29,A30,A65,WEIERSTR:34;
A67: dist(s9,c9) = dist(s,c) by TOPREAL6:def 1;
A68: 1 <= j2 by A60,MATRIX_0:32;
    left_cell(f,i,G) /\ right_cell(f,i,G) = LSeg(f,i) by A54,A55,A57,GOBRD13:29
;
    then
A69: s in right_cell(f,i,G) by A56,XBOOLE_0:def 4;
A70: j2 <= width G by A60,MATRIX_0:32;
A71: j2+1+1<>j2;
A72: 1 <= i2 by A60,MATRIX_0:32;
A73: j1 <= width G by A58,MATRIX_0:32;
A74: 1 <= j1+1 by NAT_1:11;
A75: i1+1<>i1+0;
A76: i1 <= len G by A58,MATRIX_0:32;
A77: i2 <= len G by A60,MATRIX_0:32;
A78: i2+1+1<>i2;
A79: 1 <= j1 by A58,MATRIX_0:32;
A80: 1 <= i1+1 by NAT_1:11;
    now
      per cases by A62;
      suppose
A81:    i1 = i2 & j1+1 = j2;
        then
A82:    dist(G*(i1,j1),G*(i1,j1+1)) = (N-bound C - S-bound C)/2|^k by A58,A60,
GOBRD14:9;
A83:    dist(G*(i1,j1),G*(i1,j1+1)) = G*(i1,j1+1)`2 - G*(i1,j1)`2 by A58,A60
,A81,GOBRD14:6;
        i1 < len G by A54,A55,A58,A59,A60,A61,A81,JORDAN10:1;
        then
A84:    i1+1 <= len G by NAT_1:13;
        then
A85:    [i1+1,j1] in Indices G by A79,A80,A73,MATRIX_0:30;
        then
A86:    dist(G*(i1,j1),G*(i1+1,j1)) = G*(i1+1,j1)`1 - G*(i1,j1)`1 by A58,
GOBRD14:5;
A87:    dist(G*(i1,j1),G*(i1+1,j1)) = (E-bound C - W-bound C)/2|^k by A58,A85,
GOBRD14:10;
A88:    j1+1 <= width G by A60,A81,MATRIX_0:32;
A89:    right_cell(f,i,G) = cell(G,i1,j1) by A54,A55,A57,A58,A59,A60,A61,A75
,A71,A81,GOBRD13:def 2;
        then
A90:    c`1 <= G*(i1+1,j1)`1 by A64,A63,A79,A88,A84,JORDAN9:17;
A91:    s`2 <= G*(i1,j1+1)`2 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A92:    G*(i1,j1)`2 <= s`2 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A93:    s`1 <= G*(i1+1,j1)`1 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A94:    G*(i1,j1)`1 <= s`1 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A95:    c`2 <= G*(i1,j1+1)`2 by A64,A63,A79,A88,A84,A89,JORDAN9:17;
A96:    G*(i1,j1)`2 <= c`2 by A64,A63,A79,A88,A84,A89,JORDAN9:17;
        G*(i1,j1)`1 <= c`1 by A64,A63,A79,A88,A84,A89,JORDAN9:17;
        then dist(s,c) <= (G*(i1+1,j1)`1-G*(i1,j1)`1) + (G*(i1,j1+1)`2- G*(i1
        ,j1)`2) by A90,A96,A95,A94,A93,A92,A91,TOPREAL6:95;
        hence contradiction by A28,A48,A66,A67,A51,A52,A86,A83,A82,A87,
XXREAL_0:2;
      end;
      suppose
A97:    i1+1 = i2 & j1 = j2;
        then 1 < j1 by A54,A55,A58,A59,A60,A61,JORDAN10:3;
        then
A98:    1 <= j1-'1 by NAT_D:49;
        then
A99:    j1-'1+1 = j1 by NAT_D:43;
A100:   j1-'1 <= width G by A73,NAT_D:44;
        then
A101:   [i1,j1-'1] in Indices G by A63,A76,A98,MATRIX_0:30;
        then
A102:   dist(G*(i1,j1-'1),G*(i1,j1-'1+1)) = G*(i1,j1-'1+1)`2 - G*(i1,j1
        -'1)`2 by A58,A99,GOBRD14:6;
A103:   [i1+1,j1-'1] in Indices G by A72,A77,A97,A98,A100,MATRIX_0:30;
        then
A104:   dist(G*(i1,j1-'1),G*(i1+1,j1-'1)) = G*(i1+1,j1-'1)`1 - G*( i1,
        j1-'1)`1 by A101,GOBRD14:5;
A105:   dist(G*(i1,j1-'1),G*(i1,j1-'1+1)) = (N-bound C - S-bound C)/2|^k
        by A58,A99,A101,GOBRD14:9;
A106:   dist(G*(i1,j1-'1),G*(i1+1,j1-'1)) = (E-bound C - W-bound C)/2|^k
        by A101,A103,GOBRD14:10;
A107:   i1+1 <= len G by A60,A97,MATRIX_0:32;
A108:   right_cell(f,i,G) = cell(G,i1,j1-'1) by A54,A55,A57,A58,A59,A60,A61,A75
,A78,A97,GOBRD13:def 2;
        then
A109:   c`1 <= G*(i1+1,j1-'1)`1 by A64,A63,A73,A107,A98,A99,JORDAN9:17;
A110:   s`2 <= G*(i1,j1-'1+1)`2 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A111:   G*(i1,j1-'1)`2 <= s`2 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A112:   s`1 <= G*(i1+1,j1-'1)`1 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A113:   G*(i1,j1-'1)`1 <= s`1 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A114:   c`2 <= G*(i1,j1-'1+1)`2 by A64,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A115:   G*(i1,j1-'1)`2 <= c`2 by A64,A63,A73,A107,A98,A99,A108,JORDAN9:17;
        G*(i1,j1-'1)`1 <= c`1 by A64,A63,A73,A107,A98,A99,A108,JORDAN9:17;
        then dist(s,c) <= (G*(i1+1,j1-'1)`1-G*(i1,j1-'1)`1) + (G*(i1,j1-'1+1)
        `2-G*(i1,j1-'1)`2) by A109,A115,A114,A113,A112,A111,A110,TOPREAL6:95;
        hence contradiction by A28,A48,A66,A67,A51,A52,A104,A102,A105,A106,
XXREAL_0:2;
      end;
      suppose
A116:   i1 = i2+1 & j1 = j2;
        then
A117:   dist(G*(i2,j2),G*(i2+1,j2)) = (E-bound C - W-bound C)/2|^k by A58,A60,
GOBRD14:10;
A118:   dist(G*(i2,j2),G*(i2+1,j2)) = G*(i2+1,j2)`1 - G*(i2,j2)`1 by A58,A60
,A116,GOBRD14:5;
A119:   i2+1 <= len G by A58,A116,MATRIX_0:32;
        j1 < width G by A54,A55,A58,A59,A60,A61,A116,JORDAN10:4;
        then
A120:   j1+1 <= width G by NAT_1:13;
        then
A121:   [i2,j2+1] in Indices G by A72,A74,A77,A116,MATRIX_0:30;
        then
A122:   dist(G*(i2,j2),G*(i2,j2+1)) = G*(i2,j2+1)`2 - G*(i2,j2)`2 by A60,
GOBRD14:6;
A123:   right_cell(f,i,G) = cell(G,i2,j2) by A54,A55,A57,A58,A59,A60,A61,A75
,A78,A116,GOBRD13:def 2;
        then
A124:   c`1 <= G*(i2+1,j2)`1 by A64,A79,A72,A116,A119,A120,JORDAN9:17;
A125:   s`2 <= G*(i2,j2+1)`2 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A126:   G*(i2,j2)`2 <= c`2 by A64,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A127:   dist(G*(i2,j2),G*(i2,j2+1)) = (N-bound C - S-bound C)/2|^k by A60,A121,
GOBRD14:9;
A128:   G*(i2,j2)`2 <= s`2 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A129:   s`1 <= G*(i2+1,j2)`1 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A130:   G*(i2,j2)`1 <= s`1 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A131:   c`2 <= G*(i2,j2+1)`2 by A64,A79,A72,A116,A119,A120,A123,JORDAN9:17;
        G*(i2,j2)`1 <= c`1 by A64,A79,A72,A116,A119,A120,A123,JORDAN9:17;
        then dist(s,c) <= (G*(i2+1,j2)`1-G*(i2,j2)`1) + (G*(i2,j2+1)`2- G*(i2
        ,j2)`2) by A124,A126,A131,A130,A129,A128,A125,TOPREAL6:95;
        hence contradiction by A28,A48,A66,A67,A51,A52,A118,A122,A127,A117,
XXREAL_0:2;
      end;
      suppose
A132:   i1 = i2 & j1 = j2+1;
        then 1 < i1 by A54,A55,A58,A59,A60,A61,JORDAN10:2;
        then
A133:   1 <= i1-'1 by NAT_D:49;
A134:   i1-'1 <= len G by A76,NAT_D:44;
        then
A135:   [i1-'1,j2] in Indices G by A68,A70,A133,MATRIX_0:30;
A136:   [i1-'1,j2+1] in Indices G by A79,A73,A132,A133,A134,MATRIX_0:30;
        then
A137:   dist(G*(i1-'1,j2),G*(i1-'1,j2+1)) = G*(i1-'1,j2+1)`2 - G*( i1 -'
        1,j2)`2 by A135,GOBRD14:6;
A138:   dist(G*(i1-'1,j2),G*(i1-'1,j2+1)) = (N-bound C - S-bound C)/2|^k
        by A135,A136,GOBRD14:9;
A139:   j2+1 <= width G by A58,A132,MATRIX_0:32;
A140:   i1-'1+1 = i1 by A133,NAT_D:43;
        then
A141:   [i1-'1+1,j2] in Indices G by A63,A68,A76,A70,MATRIX_0:30;
        then
A142:   dist(G*(i1-'1,j2),G*(i1-'1+1,j2)) = G*(i1-'1+1,j2)`1 - G*( i1 -'
        1,j2)`1 by A135,GOBRD14:5;
A143:   right_cell(f,i,G) = cell(G,i1-'1,j2) by A54,A55,A57,A58,A59,A60,A61,A75
,A71,A132,GOBRD13:def 2;
        then
A144:   c`1 <= G*(i1-'1+1,j2)`1 by A64,A68,A76,A139,A133,A140,JORDAN9:17;
A145:   s`2 <= G*(i1-'1,j2+1)`2 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A146:   G*(i1-'1,j2)`2 <= s`2 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A147:   s`1 <= G*(i1-'1+1,j2)`1 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A148:   G*(i1-'1,j2)`1 <= s`1 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A149:   c`2 <= G*(i1-'1,j2+1)`2 by A64,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A150:   G*(i1-'1,j2)`2 <= c`2 by A64,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A151:   dist(G*(i1-'1,j2),G*(i1-'1+1,j2)) = (E-bound C - W-bound C)/2|^k
        by A135,A141,GOBRD14:10;
        G*(i1-'1,j2)`1 <= c`1 by A64,A68,A76,A139,A133,A140,A143,JORDAN9:17;
        then dist(s,c) <= (G*(i1-'1+1,j2)`1-G*(i1-'1,j2)`1) + (G*(i1-'1,j2+1)
        `2-G*(i1-'1,j2)`2) by A144,A150,A149,A148,A147,A146,A145,TOPREAL6:95;
        hence contradiction by A28,A48,A66,A67,A51,A52,A142,A137,A138,A151,
XXREAL_0:2;
      end;
    end;
    hence thesis;
  end;
  suppose
    p = |[w,q]|;
    then
A152: p`2 = q by EUCLID:52;
A153: ex S being Real_Sequence of 2 st S is convergent & (for x being
    Nat holds S.x in (Lower_Appr C).x) & p = lim S
    proof
      set R = {(LMP Lower_Arc L~Cage(C,n))`2 where n is Nat: 0 < n};
      R c= REAL
      proof
        let x be object;
        assume x in R;
        then ex n being Nat st x = (LMP Lower_Arc L~Cage(C,n))`2 &
        0 < n;
        hence thesis by XREAL_0:def 1;
      end;
      then reconsider R as Subset of REAL;
      deffunc g(Nat) = LMP Lower_Arc L~Cage(C,$1);
      reconsider pp = p as Element of REAL 2 by EUCLID:22;
A154: for x being Element of NAT holds g(x) is Element of REAL 2 by EUCLID:22;
      consider S being sequence of  REAL 2 such that
A155: for n being Element of NAT holds S.n = g(n) from FUNCT_2:sch 9
      (A154);
      the carrier of TOP-REAL 2 = REAL 2 by EUCLID:22;
      then reconsider SS=S as Real_Sequence of 2;
      take SS;
A156: R is bounded_above
      proof
        take q;
        let r be ExtReal;
        assume r in R;
        then ex n being Nat st r = (LMP Lower_Arc L~Cage(C,n))`2 &
        0 < n;
        then r in proj2.:(H /\ U) by A12;
        hence thesis by A10,SEQ_4:def 1;
      end;
A157: (LMP Lower_Arc L~Cage(C,1))`2 in R;
A158: for r being Real st 0<r ex n being Nat st for m being
      Nat st n<=m holds |. S.m-pp .| < r
      proof
A159:   for s being Real st 0<s ex r being Real st r in R & q-s<r
        proof
          let s be Real;
          assume 0<s;
          then consider r being Real such that
A160:     r in proj2.:(H /\ U) and
A161:     q-s<r by A10,A19,SEQ_4:def 1;
          take r;
          consider x being Point of TOP-REAL 2 such that
A162:     x in H /\ U and
A163:     proj2.x = r by A160,Lm1;
          x in U by A162,XBOOLE_0:def 4;
          then consider n being Nat such that
A164:     x = LMP Lower_Arc L~Cage(C,n) and
A165:     0 < n;
          r = (LMP Lower_Arc L~Cage(C,n))`2 by A163,A164,PSCOMP_1:def 6;
          hence thesis by A161,A165;
        end;
        reconsider p1=p as Element of TOP-REAL 2;
        let r be Real;
        assume 0 < r;
        then consider v being Real such that
A166:   v in R and
A167:   upper_bound R - r < v by A157,A156,SEQ_4:def 1;
        consider n being Nat such that
A168:   v = (LMP Lower_Arc L~Cage(C,n))`2 and
A169:   0 < n by A166;
        upper_bound R - r + r < v + r by A167,XREAL_1:6;
        then
A170:   upper_bound R - v < v + r - v by XREAL_1:14;
        take n;
        let m be Nat;
A171:     m in NAT by ORDINAL1:def 12;
        reconsider Sm = S.m as Point of TOP-REAL 2 by EUCLID:22;
        assume
A172:   n <= m;
        then (LMP Lower_Arc L~Cage(C,n))`2 <= (LMP Lower_Arc L~Cage(C,m))`2
        by A169,Th28;
        then (Sm)`2 >= v by A155,A168,A171;
        then
A173:   p`2 - (Sm)`2 <= p`2 - v by XREAL_1:13;
        reconsider SSm = Sm as Point of TOP-REAL 2;
A174:   SSm-p1 = S.m-pp;
A175:   S.m = LMP Lower_Arc L~Cage(C,m) by A155,A171;
        then (Sm)`1 = w by A5;
        then |.(Sm)`1-p`1.| = 0 by A11,ABSVALUE:def 1;
        then
A176:   |. S.m-pp .|<=0+|.(Sm)`2-p`2.| by A174,JGRAPH_1:32;
        0 > (Sm)`2-p`2 by A169,A175,A172,Th24,XREAL_1:49;
        then
A177:   |. S.m-pp .|<=-((Sm)`2-p`2) by A176,ABSVALUE:def 1;
        for r being Real st r in R holds q>=r
        proof
          let r be Real;
          assume r in R;
          then ex n being Nat st r = (LMP Lower_Arc L~Cage(C,n))`2
          & 0 < n;
          then r in proj2.:(H /\ U) by A12;
          hence thesis by A10,SEQ_4:def 1;
        end;
        then upper_bound R = q by A157,A156,A159,SEQ_4:def 1;
        then p`2-(Sm)`2 < r by A152,A170,A173,XXREAL_0:2;
        hence thesis by A177,XXREAL_0:2;
      end;
      thus
A178: SS is convergent
      proof
        take p;
        let r be Real;
        assume 0<r;
        then consider n being Nat such that
A179:   for m being Nat st n<=m holds |. S.m-pp .| < r by A158;
        take n;
        let m be Nat;
        assume n<=m;
        then |. S.m-pp .| < r by A179;
        hence |.SS.m-p.| < r;
      end;
      hereby
        let x be Nat;
A180:     x in NAT by ORDINAL1:def 12;
A181:   (Lower_Appr C).x = Lower_Arc L~Cage(C,x) by JORDAN19:def 2;
        S.x = LMP Lower_Arc L~Cage(C,x) by A155,A180;
        hence SS.x in (Lower_Appr C).x by A181,JORDAN21:31;
      end;
      for r being Real st 0<r
         ex n st for m st n<=m holds |.SS.m-p.| < r
      proof
        let r be Real;
        assume 0<r;
        then consider n being Nat such that
A182:   for m being Nat st n<=m holds |. S.m-pp .| < r by A158;
        take n;
        let m be Nat;
        assume n<=m;
        then |. S.m-pp .| < r by A182;
        hence |.SS.m-p.| < r;
      end;
      hence p = lim SS by A178,TOPRNS_1:def 9;
    end;
    South_Arc C = Lim_inf Lower_Appr C by JORDAN19:def 4;
    hence thesis by A153,KURATO_2:21;
  end;
end;

theorem Th35:
  North_Arc C c= C
proof
A1: North_Arc C = Lim_inf Upper_Appr C by JORDAN19:def 3;
  reconsider OO = BDD C as Subset of TopSpaceMetr Euclid 2 by Lm4;
  let x be object;
  assume
A2: x in North_Arc C;
  assume
A3: not x in C;
  reconsider x as Point of TOP-REAL 2 by A2;
A4: x in C` by A3,SUBSET_1:29;
A5: (BDD C) \/ (UBD C) = C` by JORDAN2C:27;
  reconsider e = x as Point of Euclid 2 by EUCLID:67;
  per cases by A4,A5,XBOOLE_0:def 3;
  suppose
A6: x in BDD C;
    OO is open by Lm4,PRE_TOPC:30;
    then consider r being Real such that
A7: r > 0 and
A8: Ball(e,r) c= BDD C by A6,TOPMETR:15;
    consider k being Nat such that
A9: for m being Nat st m > k holds (Upper_Appr C).m meets
    Ball(e,r) by A2,A1,A7,KURATO_2:14;
A10: Upper_Arc L~Cage(C,k+1) c= L~Cage(C,k+1) by JORDAN6:61;
A11: (Upper_Appr C).(k+1) = Upper_Arc L~Cage(C,k+1) by JORDAN19:def 1;
A12: k+0 < k+1 by XREAL_1:8;
    Ball(e,r) misses L~Cage(C,k+1) by A8,JORDAN10:19,XBOOLE_1:63;
    hence thesis by A9,A12,A11,A10,XBOOLE_1:63;
  end;
  suppose
A13: x in UBD C;
    union UBD-Family C = UBD C by JORDAN10:14;
    then consider A being set such that
A14: x in A and
A15: A in UBD-Family C by A13,TARSKI:def 4;
    UBD-Family C = the set of all UBD L~Cage(C,m) where m is Nat
 by JORDAN10:def 1;
    then consider m being Nat such that
A16: A = UBD L~Cage(C,m) by A15;
    reconsider OO = LeftComp Cage(C,m) as Subset of TopSpaceMetr Euclid 2 by
Lm4;
A17: OO is open by Lm4,PRE_TOPC:30;
    x in LeftComp Cage(C,m) by A14,A16,GOBRD14:36;
    then consider r being Real such that
A18: r > 0 and
A19: Ball(e,r) c= LeftComp Cage(C,m) by A17,TOPMETR:15;
    consider k being Nat such that
A20: for m being Nat st m > k holds (Upper_Appr C).m meets
    Ball(e,r) by A2,A1,A18,KURATO_2:14;
    thus thesis
    proof
      per cases;
      suppose
A21:    m > k;
A22:    (Upper_Appr C).m = Upper_Arc L~Cage(C,m) by JORDAN19:def 1;
A23:    Upper_Arc L~Cage(C,m) c= L~Cage(C,m) by JORDAN6:61;
        Ball(e,r) misses L~Cage(C,m) by A19,SPRECT_3:26,XBOOLE_1:63;
        hence thesis by A20,A21,A22,A23,XBOOLE_1:63;
      end;
      suppose
        m <= k;
        then LeftComp Cage(C,m) c= LeftComp Cage(C,k) by JORDAN1H:47;
        then
A24:    Ball(e,r) c= LeftComp Cage(C,k) by A19;
A25:    k+0 < k+1 by XREAL_1:8;
        then LeftComp Cage(C,k) c= LeftComp Cage(C,k+1) by JORDAN1H:47;
        then Ball(e,r) c= LeftComp Cage(C,k+1) by A24;
        then
A26:    Ball(e,r) misses L~Cage(C,k+1) by SPRECT_3:26,XBOOLE_1:63;
A27:    Upper_Arc L~Cage(C,k+1) c= L~Cage(C,k+1) by JORDAN6:61;
        (Upper_Appr C).(k+1) = Upper_Arc L~Cage(C,k+1) by JORDAN19:def 1;
        hence thesis by A20,A25,A26,A27,XBOOLE_1:63;
      end;
    end;
  end;
end;

theorem Th36:
  South_Arc C c= C
proof
  let x be object;
  assume
A1: x in South_Arc C;
  assume
A2: not x in C;
  reconsider x as Point of TOP-REAL 2 by A1;
A3: x in C` by A2,SUBSET_1:29;
  reconsider e = x as Point of Euclid 2 by EUCLID:67;
A4: South_Arc C = Lim_inf Lower_Appr C by JORDAN19:def 4;
A5: (BDD C) \/ (UBD C) = C` by JORDAN2C:27;
  per cases by A3,A5,XBOOLE_0:def 3;
  suppose
A6: x in BDD C;
    reconsider OO = BDD C as Subset of TopSpaceMetr Euclid 2 by Lm4;
    OO is open by Lm4,PRE_TOPC:30;
    then consider r being Real such that
A7: r > 0 and
A8: Ball(e,r) c= BDD C by A6,TOPMETR:15;
    consider k being Nat such that
A9: for m being Nat st m > k holds (Lower_Appr C).m meets
    Ball(e,r) by A1,A4,A7,KURATO_2:14;
A10: Lower_Arc L~Cage(C,k+1) c= L~Cage(C,k+1) by JORDAN6:61;
A11: (Lower_Appr C).(k+1) = Lower_Arc L~Cage(C,k+1) by JORDAN19:def 2;
A12: k+0 < k+1 by XREAL_1:8;
    Ball(e,r) misses L~Cage(C,k+1) by A8,JORDAN10:19,XBOOLE_1:63;
    hence thesis by A9,A12,A11,A10,XBOOLE_1:63;
  end;
  suppose
A13: x in UBD C;
    union UBD-Family C = UBD C by JORDAN10:14;
    then consider A being set such that
A14: x in A and
A15: A in UBD-Family C by A13,TARSKI:def 4;
    UBD-Family C = the set of all UBD L~Cage(C,m) where m is Nat
 by JORDAN10:def 1;
    then consider m being Nat such that
A16: A = UBD L~Cage(C,m) by A15;
    reconsider OO = LeftComp Cage(C,m) as Subset of TopSpaceMetr Euclid 2 by
Lm4;
A17: OO is open by Lm4,PRE_TOPC:30;
    x in LeftComp Cage(C,m) by A14,A16,GOBRD14:36;
    then consider r being Real such that
A18: r > 0 and
A19: Ball(e,r) c= LeftComp Cage(C,m) by A17,TOPMETR:15;
    consider k being Nat such that
A20: for m being Nat st m > k holds (Lower_Appr C).m meets
    Ball(e,r) by A1,A4,A18,KURATO_2:14;
    thus thesis
    proof
      per cases;
      suppose
A21:    m > k;
A22:    (Lower_Appr C).m = Lower_Arc L~Cage(C,m) by JORDAN19:def 2;
A23:    Lower_Arc L~Cage(C,m) c= L~Cage(C,m) by JORDAN6:61;
        Ball(e,r) misses L~Cage(C,m) by A19,SPRECT_3:26,XBOOLE_1:63;
        hence thesis by A20,A21,A22,A23,XBOOLE_1:63;
      end;
      suppose
        m <= k;
        then LeftComp Cage(C,m) c= LeftComp Cage(C,k) by JORDAN1H:47;
        then
A24:    Ball(e,r) c= LeftComp Cage(C,k) by A19;
A25:    k+0 < k+1 by XREAL_1:8;
        then LeftComp Cage(C,k) c= LeftComp Cage(C,k+1) by JORDAN1H:47;
        then Ball(e,r) c= LeftComp Cage(C,k+1) by A24;
        then
A26:    Ball(e,r) misses L~Cage(C,k+1) by SPRECT_3:26,XBOOLE_1:63;
A27:    Lower_Arc L~Cage(C,k+1) c= L~Cage(C,k+1) by JORDAN6:61;
        (Lower_Appr C).(k+1) = Lower_Arc L~Cage(C,k+1) by JORDAN19:def 2;
        hence thesis by A20,A25,A26,A27,XBOOLE_1:63;
      end;
    end;
  end;
end;

theorem
  LMP C in Lower_Arc C & UMP C in Upper_Arc C or UMP C in Lower_Arc C &
  LMP C in Upper_Arc C
proof
A1: LMP C in South_Arc C by Th34;
A2: North_Arc C c= C by Th35;
A3: UMP C in North_Arc C by Th33;
A4: South_Arc C c= C by Th36;
  now
    per cases by A4,A1,A2,A3,JORDAN16:7;
    case
      LE LMP C, UMP C, C;
      then
      LMP C in Upper_Arc C & UMP C in Lower_Arc C or LMP C in Lower_Arc C
      & UMP C in Lower_Arc C or LMP C in Upper_Arc C & UMP C in Upper_Arc C;
      hence UMP C in Lower_Arc C & LMP C in Upper_Arc C by JORDAN21:49,50;
    end;
    case
      LE UMP C, LMP C, C;
      then
      UMP C in Upper_Arc C & LMP C in Lower_Arc C or LMP C in Lower_Arc C
      & UMP C in Lower_Arc C or LMP C in Upper_Arc C & UMP C in Upper_Arc C;
      hence LMP C in Lower_Arc C & UMP C in Upper_Arc C by JORDAN21:49,50;
    end;
  end;
  hence thesis;
end;

:: Moved from JORDAN, AG 20.01.2006

theorem
  W-bound C = W-bound North_Arc C
proof
A1: W-min C in North_Arc C by Th29;
  North_Arc C c= C by Th35;
  hence thesis by A1,JORDAN1J:65;
end;

theorem
  E-bound C = E-bound North_Arc C
proof
A1: E-max C in North_Arc C by Th30;
  North_Arc C c= C by Th35;
  hence thesis by A1,JORDAN1J:66;
end;

theorem
  W-bound C = W-bound South_Arc C
proof
A1: W-min C in South_Arc C by Th31;
  South_Arc C c= C by Th36;
  hence thesis by A1,JORDAN1J:65;
end;

theorem
  E-bound C = E-bound South_Arc C
proof
A1: E-max C in South_Arc C by Th32;
  South_Arc C c= C by Th36;
  hence thesis by A1,JORDAN1J:66;
end;