:: On the Segmentation of a Simple Closed Curve
::  by Andrzej Trybulec
::
:: Received August 18, 2003
:: Copyright (c) 2003-2012 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, PRE_TOPC, EUCLID, SUBSET_1, XREAL_0, ORDINAL1,
      XBOOLE_0, ORDINAL2, PSCOMP_1, RCOMP_1, RELAT_1, FUNCT_1, TOPMETR, TARSKI,
      XXREAL_2, ZFMISC_1, XXREAL_0, STRUCT_0, CARD_1, ARYTM_3, SEQ_4, JORDAN6,
      JORDAN3, COMPLEX1, ARYTM_1, CONNSP_2, SETFAM_1, XXREAL_1, PCOMPS_1,
      METRIC_1, REAL_1, WEIERSTR, TOPREAL1, FINSEQ_1, PARTFUN1, GOBRD10,
      MEASURE5, FINSET_1, JORDAN_A, NAT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XREAL_0,
      REAL_1, NAT_1, FINSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1,
      FINSEQ_1, NAT_D, XXREAL_2, SEQ_4, RCOMP_1, TOPMETR, CONNSP_2, STRUCT_0,
      PRE_TOPC, TBSP_1, COMPTS_1, METRIC_1, RLVECT_1, EUCLID, TOPREAL1,
      TOPREAL2, GOBRD10, WEIERSTR, PCOMPS_1, JORDAN5C, JORDAN6, JORDAN7,
      MEASURE6, PSCOMP_1, JORDAN1K, XXREAL_0, BORSUK_1;
 constructors REAL_1, RCOMP_1, NAT_D, TOPS_2, TBSP_1, TOPREAL1, MEASURE6,
      GOBRD10, JORDAN5C, JORDAN6, JORDAN7, JORDAN1K, SEQ_4, FUNCSDOM, BINOP_2,
      RVSUM_1, PSCOMP_1;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS,
      XREAL_0, MEMBERED, FINSEQ_1, RCOMP_1, STRUCT_0, COMPTS_1, BORSUK_1,
      EUCLID, TOPMETR, TOPREAL1, TOPREAL2, PSCOMP_1, WAYBEL_2, TOPREAL6,
      XXREAL_2, PCOMPS_1, PRE_TOPC, MEASURE6, ZFMISC_1, FUNCT_1, JORDAN5A;
 requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
 definitions XBOOLE_0, TARSKI, EUCLID, BINOP_1, PSCOMP_1;
 theorems EUCLID, PCOMPS_1, FINSEQ_3, NAT_1, FINSEQ_5, JGRAPH_1, SPPOL_1,
      ZFMISC_1, JORDAN7, SPRECT_1, JORDAN6, XBOOLE_1, REVROT_1, JORDAN5A,
      JORDAN5C, SEQ_4, PARTFUN2, WEIERSTR, SUBSET_1, METRIC_1, TOPREAL3,
      TARSKI, XBOOLE_0, TOPRNS_1, PSCOMP_1, BORSUK_1, JORDAN16, JORDAN1K,
      RCOMP_1, BORSUK_3, TOPREAL6, TOPMETR, FUNCT_2, BINOP_1, TOPS_1, CONNSP_2,
      FUNCT_1, RELAT_1, TOPREAL5, JORDAN17, TOPREAL1, TOPREAL8, GOBRD10,
      ORDINAL1, XREAL_0, XREAL_1, XXREAL_0, GOBOARD6, PARTFUN1, CARD_1,
      XXREAL_2, XXREAL_1, NAT_D, COMPTS_1, MEASURE6;
 schemes DOMAIN_1, FRAENKEL, FUNCT_7, TOPREAL1;

begin :: Preliminaries

reserve C for Simple_closed_curve,
  p,q,p1 for Point of TOP-REAL 2,
  i,j,k,n for Element of NAT,
  r,s for real number;

theorem Th1:
  for T being non empty TopSpace, f being continuous RealMap of T,
  A being compact Subset of T holds f.:A is compact
proof
  let T be non empty TopSpace, f be continuous RealMap of T,
  A be compact Subset of T;
  reconsider g = f as continuous Function of T,R^1 by JORDAN5A:27,TOPMETR:17;
  [#](g.:A) is compact by WEIERSTR:9,13;
  hence thesis by WEIERSTR:def 1;
end;

theorem Th2:
for A being compact Subset of REAL, B being non empty Subset of REAL st B c= A
  holds lower_bound B in A
proof
  let A be compact Subset of REAL, B be non empty Subset of REAL such that
A1: B c= A;
A2: A is real-bounded by RCOMP_1:10;
  then
A3: B is bounded_below by A1,XXREAL_2:44;
A4: Cl B c= A by A1,MEASURE6:57;
  Cl B is bounded_below by A1,A2,MEASURE6:57,XXREAL_2:44;
  then lower_bound Cl B in Cl B by RCOMP_1:13;
  then lower_bound Cl B in A by A4;
  hence thesis by A3,TOPREAL6:68;
end;

theorem
  for A,B being compact non empty Subset of TOP-REAL n,
  f being continuous RealMap of [:TOP-REAL n, TOP-REAL n:],
  g being RealMap of TOP-REAL n st for p being Point of TOP-REAL n
  ex G being Subset of REAL
  st G = { f.(p,q) where q is Point of TOP-REAL n : q in B } &
   g.p = lower_bound G
  holds lower_bound(f.:[:A,B:]) = lower_bound(g.:A)
proof
  let A,B be compact non empty Subset of TOP-REAL n;
  let f be continuous RealMap of [:TOP-REAL n, TOP-REAL n:];
  let g being RealMap of TOP-REAL n such that
A1: for p being Point of TOP-REAL n ex G being Subset of REAL st
  G = { f.(p,q) where q is Point of TOP-REAL n : q in B } &
   g.p = lower_bound G;
A2: [:A,B:] is compact by BORSUK_3:23;
  then
A3: f.:[:A,B:] is compact by Th1;
A4: f.:[:A,B:] is real-bounded by A2,Th1,RCOMP_1:10;
A5: g.:A c= f.:[:A,B:]
  proof
    let u be set;
    assume u in g.:A;
    then consider p being Point of TOP-REAL n such that
A6: p in A and
A7: u = g.p by FUNCT_2:65;
    consider q being Point of TOP-REAL n such that
A8: q in B by SUBSET_1:4;
    consider G being Subset of REAL such that
A9: G = { f.(p,q1) where q1 is Point of TOP-REAL n : q1 in B } and
A10: u = lower_bound G by A1,A7;
A11: f.(p,q) in G by A8,A9;
    G c= f.:[:A,B:]
    proof
      let u be set;
      assume u in G;
      then consider q1 being Point of TOP-REAL n such that
A12:  u = f.(p,q1) and
A13:  q1 in B by A9;
      [p,q1] in [:A,B:] by A6,A13,ZFMISC_1:87;
      hence thesis by A12,FUNCT_2:35;
    end;
    hence thesis by A3,A10,A11,Th2;
  end;
  then
A14: g.:A is bounded_below by A4,XXREAL_2:44;
A15: for r st r in f.:[:A,B:] holds lower_bound(g.:A)<=r
  proof
    let r;
    assume r in f.:[:A,B:];
    then consider pq being Point of [:TOP-REAL n, TOP-REAL n:] such that
A16: pq in [:A,B:] and
A17: r = f.pq by FUNCT_2:65;
    pq in the carrier of [:TOP-REAL n, TOP-REAL n:];
    then pq in [:the carrier of TOP-REAL n, the carrier of TOP-REAL n:]
    by BORSUK_1:def 2;
    then consider p,q being set such that
A18: p in the carrier of TOP-REAL n and
A19: q in the carrier of TOP-REAL n and
A20: pq = [p,q] by ZFMISC_1:84;
A21: q in B by A16,A20,ZFMISC_1:87;
    reconsider p,q as Point of TOP-REAL n by A18,A19;
    consider G being Subset of REAL such that
A22: G = { f.(p,q1) where q1 is Point of TOP-REAL n : q1 in B } and
A23: g.p = lower_bound G by A1;
A24: p in A by A16,A20,ZFMISC_1:87;
    G c= f.:[:A,B:]
    proof
      let u be set;
      assume u in G;
      then consider q1 being Point of TOP-REAL n such that
A25:  u = f.(p,q1) and
A26:  q1 in B by A22;
      [p,q1] in [:A,B:] by A24,A26,ZFMISC_1:87;
      hence thesis by A25,FUNCT_2:35;
    end;
    then
A27: G is bounded_below by A4,XXREAL_2:44;
    r = f.(p,q) by A17,A20;
    then r in G by A21,A22;
    then
A28: g.p <= r by A23,A27,SEQ_4:def 2;
    g.p in g.:A by A24,FUNCT_2:35;
    then lower_bound(g.:A)<=g.p by A14,SEQ_4:def 2;
    hence thesis by A28,XXREAL_0:2;
  end;
  for s st 0<s ex r st r in f.:[:A,B:] & r<lower_bound(g.:A)+s
  proof
    let s;
    assume 0<s;
    then consider r such that
A29: r in g.:A and
A30: r<lower_bound(g.:A)+s by A14,SEQ_4:def 2;
    take r;
    thus r in f.:[:A,B:] by A5,A29;
    thus thesis by A30;
  end;
  hence thesis by A4,A15,SEQ_4:def 2;
end;

theorem
  for A,B being compact non empty Subset of TOP-REAL n,
  f being continuous RealMap of [:TOP-REAL n, TOP-REAL n:],
  g being RealMap of TOP-REAL n st for q being Point of TOP-REAL n
  ex G being Subset of REAL
  st G = { f.(p,q) where p is Point of TOP-REAL n : p in A } &
   g.q = lower_bound G
  holds lower_bound(f.:[:A,B:]) = lower_bound(g.:B )
proof
  let A,B be compact non empty Subset of TOP-REAL n;
  let f be continuous RealMap of [:TOP-REAL n, TOP-REAL n:];
  let g being RealMap of TOP-REAL n such that
A1: for q being Point of TOP-REAL n ex G being Subset of REAL st
  G = { f.(p,q) where p is Point of TOP-REAL n : p in A } &
  g.q = lower_bound G;
A2: [:A,B:] is compact by BORSUK_3:23;
  then
A3: f.:[:A,B:] is compact by Th1;
A4: f.:[:A,B:] is real-bounded by A2,Th1,RCOMP_1:10;
A5: g.:B c= f.:[:A,B:]
  proof
    let u be set;
    assume u in g.:B;
    then consider q being Point of TOP-REAL n such that
A6: q in B and
A7: u = g.q by FUNCT_2:65;
    consider p being Point of TOP-REAL n such that
A8: p in A by SUBSET_1:4;
    consider G being Subset of REAL such that
A9: G = { f.(p1,q) where p1 is Point of TOP-REAL n : p1 in A } and
A10: u = lower_bound G by A1,A7;
A11: f.(p,q) in G by A8,A9;
    G c= f.:[:A,B:]
    proof
      let u be set;
      assume u in G;
      then consider p1 being Point of TOP-REAL n such that
A12:  u = f.(p1,q) and
A13:  p1 in A by A9;
      [p1,q] in [:A,B:] by A6,A13,ZFMISC_1:87;
      hence thesis by A12,FUNCT_2:35;
    end;
    hence thesis by A3,A10,A11,Th2;
  end;
  then
A14: g.:B is bounded_below by A4,XXREAL_2:44;
A15: for r st r in f.:[:A,B:] holds lower_bound(g.:B)<=r
  proof
    let r;
    assume r in f.:[:A,B:];
    then consider pq being Point of [:TOP-REAL n, TOP-REAL n:] such that
A16: pq in [:A,B:] and
A17: r = f.pq by FUNCT_2:65;
    pq in the carrier of [:TOP-REAL n, TOP-REAL n:];
    then pq in [:the carrier of TOP-REAL n, the carrier of TOP-REAL n:]
    by BORSUK_1:def 2;
    then consider p,q being set such that
A18: p in the carrier of TOP-REAL n and
A19: q in the carrier of TOP-REAL n and
A20: pq = [p,q] by ZFMISC_1:84;
A21: p in A by A16,A20,ZFMISC_1:87;
    reconsider p,q as Point of TOP-REAL n by A18,A19;
    consider G being Subset of REAL such that
A22: G = { f.(p1,q) where p1 is Point of TOP-REAL n : p1 in A } and
A23: g.q = lower_bound G by A1;
A24: q in B by A16,A20,ZFMISC_1:87;
    G c= f.:[:A,B:]
    proof
      let u be set;
      assume u in G;
      then consider p1 being Point of TOP-REAL n such that
A25:  u = f.(p1,q) and
A26:  p1 in A by A22;
      [p1,q] in [:A,B:] by A24,A26,ZFMISC_1:87;
      hence thesis by A25,FUNCT_2:35;
    end;
    then
A27: G is bounded_below by A4,XXREAL_2:44;
    r = f.(p,q) by A17,A20;
    then r in G by A21,A22;
    then
A28: g.q <= r by A23,A27,SEQ_4:def 2;
    g.q in g.:B by A24,FUNCT_2:35;
    then lower_bound(g.:B)<=g.q by A14,SEQ_4:def 2;
    hence thesis by A28,XXREAL_0:2;
  end;
  for s st 0<s ex r st r in f.:[:A,B:] & r<lower_bound(g.:B)+s
  proof
    let s;
    assume 0<s;
    then consider r such that
A29: r in g.:B and
A30: r<lower_bound(g.:B)+s by A14,SEQ_4:def 2;
    take r;
    thus r in f.:[:A,B:] by A5,A29;
    thus thesis by A30;
  end;
  hence thesis by A4,A15,SEQ_4:def 2;
end;

theorem Th5:
  q in Lower_Arc C & q <> W-min C implies LE E-max C, q, C
proof
  E-max C in Upper_Arc C by JORDAN7:1;
  hence thesis by JORDAN6:def 10;
end;

theorem Th6:
  q in Upper_Arc C implies LE q, E-max C, C
proof
A1: E-max C in Lower_Arc C by JORDAN7:1;
  E-max C <> W-min C by TOPREAL5:19;
  hence thesis by A1,JORDAN6:def 10;
end;

begin :: The Euclidean distance

definition
  let n;
A1: [:the carrier of TOP-REAL n, the carrier of TOP-REAL n:]
  = the carrier of [:TOP-REAL n, TOP-REAL n:] by BORSUK_1:def 2;
  func Eucl_dist n -> RealMap of [:TOP-REAL n, TOP-REAL n:] means
  :Def1:
  for p,q being Point of TOP-REAL n holds it.(p,q) =|.p - q.|;
  existence
  proof
    deffunc F(Point of TOP-REAL n,Point of TOP-REAL n) = |.$1 - $2.|;
A2: for p,q being Point of TOP-REAL n holds F(p,q) in REAL;
    consider f
    being Function of [:the carrier of TOP-REAL n, the carrier of TOP-REAL n:],
    REAL such that
A3: for p,q being Point of TOP-REAL n holds f.(p,q) = F(p,q)
    from FUNCT_7:sch 1(A2);
    reconsider f as RealMap of [:TOP-REAL n, TOP-REAL n:] by A1;
    take f;
    let p,q being Point of TOP-REAL n;
    thus thesis by A3;
  end;
  uniqueness
  proof
    let IT1,IT2 be RealMap of [:TOP-REAL n, TOP-REAL n:] such that
A4: for p,q being Point of TOP-REAL n holds IT1.(p,q) =|.p - q.| and
A5: for p,q being Point of TOP-REAL n holds IT2.(p,q) =|.p - q.|;
    now
      let p,q be Point of TOP-REAL n;
      thus IT1.(p,q) = |.p - q.| by A4
        .= IT2.(p,q) by A5;
    end;
    hence thesis by A1,BINOP_1:2;
  end;
end;

definition
  let T be non empty TopSpace, f be RealMap of T;
  redefine attr f is continuous means
  for p being Point of T, N being Neighbourhood of f.p
  ex V being a_neighborhood of p st f.:V c= N;
  compatibility
  proof
    thus f is continuous implies
    for p being Point of T, N being Neighbourhood of f.p
    ex V being a_neighborhood of p st f.:V c= N
    proof
      assume
A1:   f is continuous;
      let p be Point of T, N be Neighbourhood of f.p;
A2:   f"(N`) = (f"N)` by FUNCT_2:100;
      N` is closed by RCOMP_1:def 5;
      then f"(N`) is closed by A1,PSCOMP_1:def 3;
      then
A3:   f"N is open by A2,TOPS_1:4;
      f.p in N by RCOMP_1:16;
      then p in f"N by FUNCT_2:38;
      then reconsider V = f"N as a_neighborhood of p by A3,CONNSP_2:3;
      take V;
      thus thesis by FUNCT_1:75;
    end;
    assume
A4: for p being Point of T, N being Neighbourhood of f.p
    ex V being a_neighborhood of p st f.:V c= N;
    let Y be Subset of REAL;
    assume Y is closed;
    then Y`` is closed;
    then
A5: Y` is open by RCOMP_1:def 5;
    for p being Point of T st p in (f"Y)` ex A being Subset of T st
    A is a_neighborhood of p & A c= (f"Y)`
    proof
      let p be Point of T;
      assume p in (f"Y)`;
      then p in f"Y` by FUNCT_2:100;
      then f.p in Y` by FUNCT_2:38;
      then consider N being Neighbourhood of f.p such that
A6:   N c= Y` by A5,RCOMP_1:18;
      consider V being a_neighborhood of p such that
A7:   f.:V c= N by A4;
      take V;
      thus V is a_neighborhood of p;
      f.:V c= Y` by A6,A7,XBOOLE_1:1;
      then
A8:   f"(f.:V) c= f"Y` by RELAT_1:143;
      V c= f"(f.:V) by FUNCT_2:42;
      then V c= f"Y` by A8,XBOOLE_1:1;
      hence thesis by FUNCT_2:100;
    end;
    then (f"Y)` is open by CONNSP_2:7;
    then (f"Y)`` is closed by TOPS_1:4;
    hence thesis;
  end;
end;

Lm1: for X,Y being TopSpace holds
the TopStruct of [:X,Y:] = [: the TopStruct of X, the TopStruct of Y:]
proof
  let X,Y be TopSpace;
  set T = [: the TopStruct of X, the TopStruct of Y:];
A1: the carrier of T = [: the carrier of the TopStruct of X,
  the carrier of the TopStruct of Y:] by BORSUK_1:def 2
    .= the carrier of [:X,Y:] by BORSUK_1:def 2;
  set tau1 = { union A where A is Subset-Family of T:
  A c= { [:X1,Y1:]
  where X1 is Subset of the TopStruct of X,
  Y1 is Subset of the TopStruct of Y :
  X1 in the topology of the TopStruct of X &
  Y1 in the topology of the TopStruct of Y}};
  set tau2 =
  { union A where A is Subset-Family of T:
  A c= { [:X1,Y1:]
  where X1 is Subset of X,
  Y1 is Subset of Y :
  X1 in the topology of X &
  Y1 in the topology of Y}};
  the topology of T = tau1 by BORSUK_1:def 2
    .= tau2
    .= the topology of [:X,Y:] by A1,BORSUK_1:def 2;
  hence thesis by A1;
end;

registration
  let n;
  cluster Eucl_dist n -> continuous;
  coherence
  proof
    set f = Eucl_dist n;
    let p being Point of [:TOP-REAL n, TOP-REAL n:],
    N being Neighbourhood of f.p;
    consider r such that
A1: 0<r and
A2: N = ].f.p-r,f.p+r.[ by RCOMP_1:def 6;
    p in the carrier of [:TOP-REAL n, TOP-REAL n:];
    then p in [:the carrier of TOP-REAL n, the carrier of TOP-REAL n:]
    by BORSUK_1:def 2;
    then consider p1,p2 being set such that
A3: p1 in the carrier of TOP-REAL n and
A4: p2 in the carrier of TOP-REAL n and
A5: p = [p1,p2] by ZFMISC_1:84;
    reconsider p1,p2 as Point of TOP-REAL n by A3,A4;
    reconsider p19=p1, p29=p2 as Element of Euclid n by TOPREAL3:8;
A6: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
    then reconsider q1=p1, q2=p2 as Point of TopSpaceMetr Euclid n;
    reconsider U = Ball(p19,r/2) as a_neighborhood of q1 by A1,GOBOARD6:91
,XREAL_1:215;
    reconsider W = Ball(p29,r/2) as a_neighborhood of q2 by A1,GOBOARD6:91
,XREAL_1:215;
    reconsider V = [:U,W:]
    as a_neighborhood of p by A5,A6,Lm1;
    take V;
    let s be set;
    assume
A7: s in f.:V;
    then reconsider s as Real;
    consider q being Point of [:TOP-REAL n, TOP-REAL n:] such that
A8: q in V and
A9: f.q = s by A7,FUNCT_2:65;
    q in the carrier of [:TOP-REAL n, TOP-REAL n:];
    then q in [:the carrier of TOP-REAL n, the carrier of TOP-REAL n:]
    by BORSUK_1:def 2;
    then consider q1,q2 being set such that
A10: q1 in the carrier of TOP-REAL n and
A11: q2 in the carrier of TOP-REAL n and
A12: q = [q1,q2] by ZFMISC_1:84;
    reconsider q1,q2 as Point of TOP-REAL n by A10,A11;
    reconsider q19=q1, q29=q2 as Element of Euclid n by TOPREAL3:8;
    reconsider q199=q19, q299=q29, p199=p19, p299=p29 as Element of REAL n;
A13: q19 in Ball(p19,r/2) by A8,A12,ZFMISC_1:87;
A14: q29 in Ball(p29,r/2) by A8,A12,ZFMISC_1:87;
A15: dist(q19,p19) < r/2 by A13,METRIC_1:11;
A16: dist(q29,p29) < r/2 by A14,METRIC_1:11;
A17: |.q1-p1.| < r/2 by A15,SPPOL_1:5;
    |.q2-p2.| < r/2 by A16,SPPOL_1:5;
    then
A18: |.q1-p1.|+|.q2-p2.| < r/2+r/2 by A17,XREAL_1:8;
A19: for p,q being Point of TOP-REAL n holds f. [p,q] =|.p - q.|
    proof
      let p,q be Point of TOP-REAL n;
      thus f. [p,q] = f.(p,q) .=|.p - q.| by Def1;
    end;
    then
A20: f.p = |.p1-p2.| by A5;
A21: s = |.q1-q2.| by A9,A12,A19;
A22: q1-q2-(p1-p2) = q1-q2-p1+p2 by EUCLID:47
      .= q1-(q2+p1)+p2 by EUCLID:46
      .= q1-p1-q2+p2 by EUCLID:46
      .= (q1-p1)-(q2-p2) by EUCLID:47;
A23: |.(q1-p1)-(q2-p2).| <= |.q1-p1.| + |.q2-p2.| by TOPRNS_1:30;
A24: s - f.p <= |.(q1-q2)-(p1-p2).| by A20,A21,TOPRNS_1:32;
    f.p - s <= |.(p1-p2)-(q1-q2).| by A20,A21,TOPRNS_1:32;
    then f.p - s <= |.(q1-q2)-(p1-p2).| by TOPRNS_1:27;
    then f.p - s <= |.q1-p1.| + |.q2-p2.| by A22,A23,XXREAL_0:2;
    then f.p - s < r by A18,XXREAL_0:2;
    then
A25: f.p-r < s by XREAL_1:11;
    s - f.p <= |.q1-p1.| + |.q2-p2.| by A22,A23,A24,XXREAL_0:2;
    then s - f.p < r by A18,XXREAL_0:2;
    then s < f.p+r by XREAL_1:19;
    hence thesis by A2,A25,XXREAL_1:4;
  end;
end;

begin :: On the distance between subsets of a Euclidean space

theorem Th7:

:: JORDAN1K:39, JGRAPH_1:55
  for A,B being non empty compact Subset of TOP-REAL n st A misses B
  holds dist_min(A,B) > 0
proof
  let A,B be non empty compact Subset of TOP-REAL n such that
A1: A misses B;
A2: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
  consider A9,B9 being Subset of TopSpaceMetr Euclid n such that
A3: A = A9 and
A4: B = B9 and
A5: dist_min(A,B) = min_dist_min(A9,B9) by JORDAN1K:def 1;
A6: A9 is compact by A2,A3,COMPTS_1:23;
  B9 is compact by A2,A4,COMPTS_1:23;
  hence thesis by A1,A3,A4,A5,A6,JGRAPH_1:38;
end;

begin :: On the segments

theorem Th8:
  LE p,q,C & LE q, E-max C, C & p <> q implies
  Segment(p,q,C) = Segment(Upper_Arc C,W-min C,E-max C,p,q)
proof
  assume that
A1: LE p,q,C and
A2: LE q, E-max C, C and
A3: p <> q;
A4: Upper_Arc C is_an_arc_of W-min C,E-max C by JORDAN6:50;
A5: LE p, E-max C, C by A1,A2,JORDAN6:58;
A6: p in Upper_Arc C by A1,A2,JORDAN17:3,JORDAN6:58;
A7: q in Upper_Arc C by A2,JORDAN17:3;
A8: Upper_Arc C c= C by JORDAN6:61;
A9: now
    assume q = W-min C;
    then LE q,p,C by A6,A8,JORDAN7:3;
    hence contradiction by A1,A3,JORDAN6:57;
  end;
  defpred P[Point of TOP-REAL 2] means LE p,$1,C & LE $1,q,C;
  defpred Q[Point of TOP-REAL 2] means LE p,$1,Upper_Arc C,W-min C,E-max C &
  LE $1,q,Upper_Arc C,W-min C,E-max C;
A10: P[p1] iff Q[p1]
  proof
    hereby
      assume that
A11:  LE p,p1,C and
A12:  LE p1,q,C;
      hereby per cases;
        suppose p1 = E-max C;
          hence LE p,p1,Upper_Arc C,W-min C,E-max C by A4,A6,JORDAN5C:10;
        end;
        suppose p1 = W-min C;
          then LE p1,p,C by A6,A8,JORDAN7:3;
          then p = p1 by A11,JORDAN6:57;
hence LE p,p1,Upper_Arc C,W-min C,E-max C by A5,JORDAN17:3,JORDAN5C:9;
        end;
        suppose that
A13:      p1 <> E-max C and
A14:      p1 <> W-min C;
          now
            assume
A15:        p1 in Lower_Arc C;
            p1 in Upper_Arc C by A2,A12,JORDAN17:3,JORDAN6:58;
            then p1 in Upper_Arc C /\ Lower_Arc C by A15,XBOOLE_0:def 4;
            then p1 in {W-min C,E-max C} by JORDAN6:50;
            hence contradiction by A13,A14,TARSKI:def 2;
          end;
          hence LE p,p1,Upper_Arc C,W-min C,E-max C by A11,JORDAN6:def 10;
        end;
      end;
      per cases;
      suppose
A16:    q = E-max C;
        then p1 in Upper_Arc C by A12,JORDAN17:3;
        hence LE p1,q,Upper_Arc C,W-min C,E-max C by A4,A16,JORDAN5C:10;
      end;
      suppose
A17:    q <> E-max C;
        now
          assume q in Lower_Arc C;
          then q in Upper_Arc C /\ Lower_Arc C by A7,XBOOLE_0:def 4;
          then q in {W-min C,E-max C} by JORDAN6:50;
          hence contradiction by A9,A17,TARSKI:def 2;
        end;
        hence LE p1,q,Upper_Arc C,W-min C,E-max C by A12,JORDAN6:def 10;
      end;
    end;
    assume that
A18: LE p,p1,Upper_Arc C,W-min C,E-max C and
A19: LE p1,q,Upper_Arc C,W-min C,E-max C;
A20: p1 in Upper_Arc C by A18,JORDAN5C:def 3;
    hence LE p,p1,C by A6,A18,JORDAN6:def 10;
    thus thesis by A7,A19,A20,JORDAN6:def 10;
  end;
  deffunc F(set) = $1;
  set X = {F(p1): P[p1]}, Y = {F(p1): Q[p1]};
A21: X = Y from FRAENKEL:sch 3(A10);
  Segment(p,q,C) = X by A9,JORDAN7:def 1;
  hence thesis by A21,JORDAN6:26;
end;

theorem Th9:
  LE E-max C, q, C implies
  Segment(E-max C,q,C) = Segment(Lower_Arc C,E-max C,W-min C,E-max C,q)
proof
  set p = E-max C;
  assume
A1: LE E-max C, q, C;
A2: Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:50;
A3: p in Lower_Arc C by JORDAN7:1;
A4: q in Lower_Arc C by A1,JORDAN17:4;
A5: Lower_Arc C c= C by JORDAN6:61;
A6: now
    assume
A7: q = W-min C;
    then p = q by A1,JORDAN7:2;
    hence contradiction by A7,TOPREAL5:19;
  end;
  defpred P[Point of TOP-REAL 2] means LE p,$1,C & LE $1,q,C;
  defpred Q[Point of TOP-REAL 2] means LE p,$1,Lower_Arc C,E-max C,W-min C &
  LE $1,q,Lower_Arc C,E-max C, W-min C;
A8: P[p1] iff Q[p1]
  proof
    hereby
      assume that
A9:   LE p,p1,C and
A10:  LE p1,q,C;
A11:  p1 in Lower_Arc C by A9,JORDAN17:4;
      hence LE p,p1,Lower_Arc C,E-max C,W-min C by A2,JORDAN5C:10;
      per cases;
      suppose
A12:    p1 = E-max C;
        then q in Lower_Arc C by A10,JORDAN17:4;
        hence LE p1,q,Lower_Arc C,E-max C,W-min C by A2,A12,JORDAN5C:10;
      end;
      suppose
A13:    p1 <> E-max C;
A14:    now
          assume
A15:      p1 = W-min C;
          then LE p1,p, C by A3,A5,JORDAN7:3;
          hence contradiction by A9,A15,JORDAN6:57,TOPREAL5:19;
        end;
        now
          assume p1 in Upper_Arc C;
          then p1 in Upper_Arc C /\ Lower_Arc C by A11,XBOOLE_0:def 4;
          then p1 in {W-min C,E-max C} by JORDAN6:50;
          hence contradiction by A13,A14,TARSKI:def 2;
        end;
        hence LE p1,q,Lower_Arc C,E-max C,W-min C by A10,JORDAN6:def 10;
      end;
    end;
    assume that
A16: LE p,p1,Lower_Arc C,E-max C,W-min C and
A17: LE p1,q,Lower_Arc C,E-max C,W-min C;
A18: p1 in Lower_Arc C by A16,JORDAN5C:def 3;
    p1 <> W-min C by A2,A6,A17,JORDAN6:55;
    hence LE p,p1,C by A3,A16,A18,JORDAN6:def 10;
    thus thesis by A4,A6,A17,A18,JORDAN6:def 10;
  end;
  deffunc F(set) = $1;
  set X = {F(p1): P[p1]}, Y = {F(p1): Q[p1]};
A19: X = Y from FRAENKEL:sch 3(A8);
  Segment(p,q,C) = X by A6,JORDAN7:def 1;
  hence thesis by A19,JORDAN6:26;
end;

theorem Th10:
  LE E-max C, q, C implies
  Segment(q,W-min C,C) = Segment(Lower_Arc C,E-max C,W-min C,q,W-min C)
proof
  set p = W-min C;
  assume
A1: LE E-max C, q, C;
A2: Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:50;
A3: p in Lower_Arc C by JORDAN7:1;
A4: q in Lower_Arc C by A1,JORDAN17:4;
A5: Lower_Arc C c= C by JORDAN6:61;
  defpred P[Point of TOP-REAL 2] means LE q,$1,C or q in C & $1=W-min C;
  defpred Q[Point of TOP-REAL 2] means LE q,$1,Lower_Arc C,E-max C,W-min C &
  LE $1,p,Lower_Arc C,E-max C, W-min C;
A6: P[p1] iff Q[p1]
  proof
    hereby
      assume
A7:   LE q,p1,C or q in C & p1=W-min C;
      per cases by A7;
      suppose that
A8:     q = E-max C and
A9:     LE q,p1,C;
A10:    p1 in Lower_Arc C by A8,A9,JORDAN17:4;
        hence LE q,p1,Lower_Arc C,E-max C,W-min C by A2,A8,JORDAN5C:10;
        thus LE p1,p,Lower_Arc C,E-max C,W-min C by A2,A10,JORDAN5C:10;
      end;
      suppose that
A11:    q <> E-max C and
A12:    LE q,p1,C;
A13:    p1 in Lower_Arc C by A1,A12,JORDAN17:4,JORDAN6:58;
A14:    now
          assume
A15:      q = W-min C;
          then LE q, E-max C, C by JORDAN7:3,SPRECT_1:14;
          hence contradiction by A1,A15,JORDAN6:57,TOPREAL5:19;
        end;
        now
          assume q in Upper_Arc C;
          then q in Upper_Arc C /\ Lower_Arc C by A4,XBOOLE_0:def 4;
          then q in {E-max C, W-min C} by JORDAN6:def 9;
          hence contradiction by A11,A14,TARSKI:def 2;
        end;
        hence LE q,p1,Lower_Arc C,E-max C,W-min C by A12,JORDAN6:def 10;
        thus LE p1,p,Lower_Arc C,E-max C,W-min C by A2,A13,JORDAN5C:10;
      end;
      suppose that q in C and
A16:    p1 = W-min C;
        thus LE q,p1,Lower_Arc C,E-max C,W-min C by A2,A4,A16,JORDAN5C:10;
        thus LE p1,p,Lower_Arc C,E-max C,W-min C by A3,A16,JORDAN5C:9;
      end;
    end;
    assume that
A17: LE q,p1,Lower_Arc C,E-max C,W-min C and
    LE p1,p,Lower_Arc C,E-max C,W-min C;
A18: p1 in Lower_Arc C by A17,JORDAN5C:def 3;
A19: q in Lower_Arc C by A17,JORDAN5C:def 3;
    per cases;
    suppose p1 <> W-min C;
      hence thesis by A17,A18,A19,JORDAN6:def 10;
    end;
    suppose p1 = W-min C;
      hence thesis by A4,A5;
    end;
  end;
  deffunc F(set) = $1;
  set X = {F(p1): P[p1]}, Y = {F(p1): Q[p1]};
A20: X = Y from FRAENKEL:sch 3(A6);
  Segment(q,p,C) = X by JORDAN7:def 1;
  hence thesis by A20,JORDAN6:26;
end;

theorem Th11:
  LE p,q,C & LE E-max C, p, C implies
  Segment(p,q,C) = Segment(Lower_Arc C,E-max C,W-min C,p,q)
proof
  assume that
A1: LE p,q,C and
A2: LE E-max C, p, C;
  per cases;
  suppose p = E-max C;
    hence thesis by A1,Th9;
  end;
  suppose
A3: p <> E-max C;
A4: Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:50;
A5: q in Lower_Arc C by A1,A2,JORDAN17:4,JORDAN6:58;
A6: p in Lower_Arc C by A2,JORDAN17:4;
A7: Lower_Arc C c= C by JORDAN6:61;
A8: now
      assume
A9:   p = W-min C;
      then LE p, E-max C, C by JORDAN17:2;
      hence contradiction by A2,A9,JORDAN6:57,TOPREAL5:19;
    end;
A10: now
      assume
A11:  q = W-min C;
      then LE q,p,C by A6,A7,JORDAN7:3;
      hence contradiction by A1,A8,A11,JORDAN6:57;
    end;
    defpred P[Point of TOP-REAL 2] means LE p,$1,C & LE $1,q,C;
    defpred Q[Point of TOP-REAL 2] means LE p,$1,Lower_Arc C,E-max C,W-min C &
    LE $1,q,Lower_Arc C,E-max C,W-min C;
A12: P[p1] iff Q[p1]
    proof
      hereby
        assume that
A13:    LE p,p1,C and
A14:    LE p1,q,C;
A15:    now
          assume
A16:      p1 = W-min C;
          then LE p1,p,C by A6,A7,JORDAN7:3;
          hence contradiction by A8,A13,A16,JORDAN6:57;
        end;
A17:    now
          assume
A18:      p in Upper_Arc C;
          p in Lower_Arc C by A2,JORDAN17:4;
          then p in Lower_Arc C /\ Upper_Arc C by A18,XBOOLE_0:def 4;
          then p in {W-min C,E-max C} by JORDAN6:50;
          hence contradiction by A3,A8,TARSKI:def 2;
        end;
        hence LE p,p1,Lower_Arc C,E-max C,W-min C by A13,JORDAN6:def 10;
A19:    p1 in Lower_Arc C by A13,A17,JORDAN6:def 10;
        per cases;
        suppose q = E-max C;
          hence LE p1,q,Lower_Arc C,E-max C,W-min C by A1,A2,A3,JORDAN6:57;
        end;
        suppose p1 = E-max C;
          hence LE p1,q,Lower_Arc C,E-max C,W-min C by A4,A5,JORDAN5C:10;
        end;
        suppose that
A20:      p1 <> E-max C;
          now
            assume p1 in Upper_Arc C;
            then p1 in Lower_Arc C /\ Upper_Arc C by A19,XBOOLE_0:def 4;
            then p1 in {W-min C,E-max C} by JORDAN6:50;
            hence contradiction by A15,A20,TARSKI:def 2;
          end;
          hence LE p1,q,Lower_Arc C,E-max C,W-min C by A14,JORDAN6:def 10;
        end;
      end;
      assume that
A21:  LE p,p1,Lower_Arc C,E-max C,W-min C and
A22:  LE p1,q,Lower_Arc C,E-max C,W-min C;
A23:  p1 <> W-min C by A4,A10,A22,JORDAN6:55;
A24:  p1 in Lower_Arc C by A21,JORDAN5C:def 3;
      hence LE p,p1,C by A6,A21,A23,JORDAN6:def 10;
      thus thesis by A5,A10,A22,A24,JORDAN6:def 10;
    end;
    deffunc F(set) = $1;
    set X = {F(p1): P[p1]}, Y = {F(p1): Q[p1]};
A25: X = Y from FRAENKEL:sch 3(A12);
    Segment(p,q,C) = X by A10,JORDAN7:def 1;
    hence thesis by A25,JORDAN6:26;
  end;
end;

theorem Th12:
  LE p,E-max C,C & LE E-max C, q, C implies
  Segment(p,q,C) = R_Segment(Upper_Arc C,W-min C,E-max C,p)
  \/ L_Segment(Lower_Arc C,E-max C,W-min C,q)
proof
  assume that
A1: LE p,E-max C,C and
A2: LE E-max C, q, C;
A3: p in Upper_Arc C by A1,JORDAN17:3;
A4: q in Lower_Arc C by A2,JORDAN17:4;
A5: now
    assume q = W-min C;
    then W-min C = E-max C by A2,JORDAN7:2;
    hence contradiction by TOPREAL5:19;
  end;
A6: Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:50;
  defpred P[Point of TOP-REAL 2] means LE p,$1,C & LE $1,q,C;
  defpred Q1[Point of TOP-REAL 2] means LE p,$1,Upper_Arc C,W-min C,E-max C;
  defpred Q2[Point of TOP-REAL 2] means LE $1,q,Lower_Arc C,E-max C,W-min C;
  defpred Q[Point of TOP-REAL 2] means Q1[$1] or Q2[$1];
A7: P[p1] iff Q[p1]
  proof
    thus
    LE p,p1,C & LE p1,q,C implies LE p,p1,Upper_Arc C,W-min C,E-max C or
    LE p1,q,Lower_Arc C,E-max C,W-min C
    proof
      assume that
A8:   LE p,p1,C and
A9:   LE p1,q,C;
A10:  now
        assume that
A11:    p1 in Lower_Arc C and
A12:    p1 in Upper_Arc C;
        p1 in Lower_Arc C /\ Upper_Arc C by A11,A12,XBOOLE_0:def 4;
        then p1 in {W-min C,E-max C} by JORDAN6:def 9;
        hence p1 = W-min C or p1 = E-max C by TARSKI:def 2;
      end;
      per cases by A10;
      suppose
A13:    p1 = W-min C;
        then p = W-min C by A8,JORDAN7:2;
        hence thesis by A1,A13,JORDAN17:3,JORDAN5C:9;
      end;
      suppose p1 = E-max C;
        hence thesis by A4,A6,JORDAN5C:10;
      end;
      suppose not p1 in Lower_Arc C;
        hence thesis by A8,JORDAN6:def 10;
      end;
      suppose not p1 in Upper_Arc C;
        hence thesis by A9,JORDAN6:def 10;
      end;
    end;
    assume that
A14: LE p,p1,Upper_Arc C,W-min C,E-max C or
    LE p1,q,Lower_Arc C,E-max C,W-min C;
    per cases by A14;
    suppose
A15:  LE p,p1,Upper_Arc C,W-min C,E-max C;
      then
A16:  p1 in Upper_Arc C by JORDAN5C:def 3;
      hence LE p,p1,C by A3,A15,JORDAN6:def 10;
      thus thesis by A4,A5,A16,JORDAN6:def 10;
    end;
    suppose that
A17:  LE p1,q,Lower_Arc C,E-max C,W-min C and
A18:  p1 <> W-min C;
A19:  p1 in Lower_Arc C by A17,JORDAN5C:def 3;
      hence LE p,p1,C by A3,A18,JORDAN6:def 10;
      thus thesis by A4,A5,A17,A19,JORDAN6:def 10;
    end;
    suppose LE p1,q,Lower_Arc C,E-max C,W-min C & p1 = W-min C;
      hence thesis by A5,A6,JORDAN6:55;
    end;
  end;
  set Y1 = {p1: Q1[p1]}, Y2 = {p1: Q2[p1]};
  deffunc F(set) = $1;
  set X = {F(p1): P[p1]}, Y = {F(p1): Q[p1]}, Y9 = {p1: Q1[p1] or Q2[p1]};
A20: X = Y from FRAENKEL:sch 3(A7);
A21: Segment(p,q,C) = X by A5,JORDAN7:def 1;
A22: L_Segment(Lower_Arc C,E-max C,W-min C,q) = Y2 by JORDAN6:def 3;
  Y9 = Y1 \/ Y2 from TOPREAL1:sch 1;
  hence thesis by A20,A21,A22,JORDAN6:def 4;
end;

theorem Th13:
  LE p,E-max C,C implies
  Segment(p,W-min C,C) = R_Segment(Upper_Arc C,W-min C,E-max C,p)
  \/ L_Segment(Lower_Arc C,E-max C,W-min C,W-min C)
proof
  set q = W-min C;
  assume LE p,E-max C,C;
  then
A1: p in Upper_Arc C by JORDAN17:3;
A2: q in Lower_Arc C by JORDAN7:1;
A3: Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:50;
  defpred P[Point of TOP-REAL 2] means LE p,$1,C or p in C & $1 = W-min C;
  defpred Q1[Point of TOP-REAL 2] means LE p,$1,Upper_Arc C,W-min C,E-max C;
  defpred Q2[Point of TOP-REAL 2] means LE $1,q,Lower_Arc C,E-max C,W-min C;
  defpred Q[Point of TOP-REAL 2] means Q1[$1] or Q2[$1];
A4: P[p1] iff Q[p1]
  proof
    thus LE p,p1,C or p in C & p1=W-min C implies
    LE p,p1,Upper_Arc C,W-min C,E-max C or LE p1,q,Lower_Arc C,E-max C,W-min C
    proof
      assume
A5:   LE p,p1,C or p in C & p1=W-min C;
A6:   now
        assume that
A7:     p1 in Lower_Arc C and
A8:     p1 in Upper_Arc C;
        p1 in Lower_Arc C /\ Upper_Arc C by A7,A8,XBOOLE_0:def 4;
        then p1 in {W-min C,E-max C} by JORDAN6:def 9;
        hence p1 = W-min C or p1 = E-max C by TARSKI:def 2;
      end;
      per cases by A6;
      suppose p1 = W-min C;
        hence thesis by A2,JORDAN5C:9;
      end;
      suppose p1 = E-max C;
        hence thesis by A2,A3,JORDAN5C:10;
      end;
      suppose not p1 in Lower_Arc C & p1 <> W-min C;
        hence thesis by A5,JORDAN6:def 10;
      end;
      suppose that
A9:     not p1 in Upper_Arc C and
A10:    p1 <> W-min C;
A11:    p1 in C by A5,A10,JORDAN7:5;
        C = Lower_Arc C \/ Upper_Arc C by JORDAN6:def 9;
        then p1 in Lower_Arc C by A9,A11,XBOOLE_0:def 3;
        hence thesis by A3,JORDAN5C:10;
      end;
    end;
    assume that
A12: LE p,p1,Upper_Arc C,W-min C,E-max C or
    LE p1,q,Lower_Arc C,E-max C,W-min C;
A13: Upper_Arc C c= C by JORDAN6:61;
    per cases by A12;
    suppose
A14:  LE p,p1,Upper_Arc C,W-min C,E-max C;
      then p1 in Upper_Arc C by JORDAN5C:def 3;
      hence thesis by A1,A14,JORDAN6:def 10;
    end;
    suppose
      LE p1,q,Lower_Arc C,E-max C,W-min C;
      then
A15:  p1 in Lower_Arc C by JORDAN5C:def 3;
      now per cases;
        suppose p1 = W-min C;
          hence thesis by A1,A13;
        end;
        suppose p1 <> W-min C;
          hence thesis by A1,A15,JORDAN6:def 10;
        end;
      end;
      hence thesis;
    end;
  end;
  set Y1 = {p1: Q1[p1]}, Y2 = {p1: Q2[p1]};
  deffunc F(set) = $1;
  set X = {F(p1): P[p1]}, Y = {F(p1): Q[p1]}, Y9 = {p1: Q1[p1] or Q2[p1]};
A16: X = Y from FRAENKEL:sch 3(A4);
A17: Segment(p,q,C) = X by JORDAN7:def 1;
A18: L_Segment(Lower_Arc C,E-max C,W-min C,q) = Y2 by JORDAN6:def 3;
  Y9 = Y1 \/ Y2 from TOPREAL1:sch 1;
  hence thesis by A16,A17,A18,JORDAN6:def 4;
end;

theorem Th14:
  R_Segment(Upper_Arc C,W-min C,E-max C,p) =
  Segment(Upper_Arc C,W-min C,E-max C,p,E-max C)
proof
  Upper_Arc C is_an_arc_of W-min C,E-max C by JORDAN6:50;
  then L_Segment(Upper_Arc C,W-min C,E-max C,E-max C) = Upper_Arc C
  by JORDAN6:22;
  hence Segment(Upper_Arc C,W-min C,E-max C,p,E-max C) =
  R_Segment(Upper_Arc C,W-min C,E-max C,p) /\ Upper_Arc C by JORDAN6:def 5
    .= R_Segment(Upper_Arc C,W-min C,E-max C,p) by JORDAN6:20,XBOOLE_1:28;
end;

theorem Th15:
  L_Segment(Lower_Arc C,E-max C,W-min C,p) =
  Segment(Lower_Arc C,E-max C,W-min C,E-max C,p)
proof
  Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:50;
  then R_Segment(Lower_Arc C,E-max C,W-min C,E-max C) = Lower_Arc C
  by JORDAN6:24;
  hence Segment(Lower_Arc C,E-max C,W-min C,E-max C,p) =
  Lower_Arc C /\ L_Segment(Lower_Arc C,E-max C,W-min C,p) by JORDAN6:def 5
    .= L_Segment(Lower_Arc C,E-max C,W-min C,p) by JORDAN6:19,XBOOLE_1:28;
end;

theorem Th16:
  for p being Point of TOP-REAL 2 st p in C & p <> W-min C
  holds Segment(p,W-min C,C) is_an_arc_of p,W-min C
proof
  set q = W-min C;
  let p be Point of TOP-REAL 2 such that
A1: p in C and
A2: p <> W-min C;
A3: E-max C in C by SPRECT_1:14;
A4: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50;
A5: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
A6: q <> E-max C by TOPREAL5:19;
  per cases by A1,A3,JORDAN16:7;
  suppose that
A7: p <> E-max C and
A8: LE p, E-max C, C;
A9: now
      assume W-min C in R_Segment(Upper_Arc C,W-min C,E-max C,p)
      /\ L_Segment(Lower_Arc C,E-max C,W-min C,q);
      then W-min C in R_Segment(Upper_Arc C,W-min C,E-max C,p) by
XBOOLE_0:def 4;
      hence contradiction by A2,A4,JORDAN6:60;
    end;
    p in Upper_Arc C by A8,JORDAN17:3;
    then
A10: LE p,E-max C,Upper_Arc C,W-min C,E-max C by A4,JORDAN5C:10;
A11: R_Segment(Upper_Arc C,W-min C,E-max C,p) =
    Segment(Upper_Arc C,W-min C,E-max C,p,E-max C) by Th14;
    then
A12: E-max C in R_Segment(Upper_Arc C,W-min C,E-max C,p) by A10,JORDAN16:5;
    q in Lower_Arc C by JORDAN7:1;
    then
A13: LE E-max C,q,Lower_Arc C,E-max C,W-min C by A5,JORDAN5C:10;
A14: L_Segment(Lower_Arc C,E-max C,W-min C,q) =
    Segment(Lower_Arc C,E-max C,W-min C,E-max C,q) by Th15;
    then E-max C in L_Segment(Lower_Arc C,E-max C,W-min C,q) by A13,JORDAN16:5;
    then
A15: E-max C in R_Segment(Upper_Arc C,W-min C,E-max C,p)
    /\ L_Segment(Lower_Arc C,E-max C,W-min C,q) by A12,XBOOLE_0:def 4;
A16: R_Segment(Upper_Arc C,W-min C,E-max C,p) c= Upper_Arc C by JORDAN6:20;
A17: L_Segment(Lower_Arc C,E-max C,W-min C,q) c= Lower_Arc C by JORDAN6:19;
    Upper_Arc C /\ Lower_Arc C = {W-min C, E-max C} by JORDAN6:def 9;
    then
A18: R_Segment(Upper_Arc C,W-min C,E-max C,p)
    /\ L_Segment(Lower_Arc C,E-max C,W-min C,q) = {E-max C}
    by A9,A15,A16,A17,TOPREAL8:1,XBOOLE_1:27;
A19: R_Segment(Upper_Arc C,W-min C,E-max C,p) is_an_arc_of p, E-max C
    by A4,A7,A10,A11,JORDAN16:21;
A20: L_Segment(Lower_Arc C,E-max C,W-min C,q) is_an_arc_of E-max C,q
    by A5,A6,A13,A14,JORDAN16:21;
    Segment(p,W-min C,C) = R_Segment(Upper_Arc C,W-min C,E-max C,p)
    \/ L_Segment(Lower_Arc C,E-max C,W-min C,W-min C) by A8,Th13;
    hence thesis by A18,A19,A20,TOPREAL1:2;
  end;
  suppose
A21: p = E-max C;
    then Segment(p,q,C) = Lower_Arc C by JORDAN7:4;
    hence thesis by A21,JORDAN6:50;
  end;
  suppose that p <> E-max C and
A22: LE E-max C,p, C;
A23: Segment(p,q,C) = Segment(Lower_Arc C,E-max C,W-min C,p,q) by A22,Th10;
    p in Lower_Arc C by A22,JORDAN17:4;
    then LE p, q, Lower_Arc C, E-max C, W-min C by A5,JORDAN5C:10;
    hence thesis by A2,A5,A23,JORDAN16:21;
  end;
end;

theorem Th17:
  for p,q being Point of TOP-REAL 2 st p<> q & LE p,q,C
  holds Segment(p,q,C) is_an_arc_of p,q
proof
  let p,q be Point of TOP-REAL 2 such that
A1: p <> q and
A2: LE p,q,C;
A3: E-max C in C by SPRECT_1:14;
A4: p in C by A2,JORDAN7:5;
A5: q in C by A2,JORDAN7:5;
A6: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50;
A7: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
  per cases by A3,A4,A5,JORDAN16:7;
  suppose q = W-min C;
    hence thesis by A1,A4,Th16;
  end;
  suppose that
A8: LE q, E-max C, C and
A9: not LE E-max C, q, C and
A10: q <> W-min C;
A11: Segment(p,q,C) = Segment(Upper_Arc C,W-min C,E-max C,p,q) by A1,A2,A8,Th8;
    not q in Lower_Arc C by A9,A10,Th5;
    then LE p, q, Upper_Arc C, W-min C, E-max C by A2,JORDAN6:def 10;
    hence thesis by A1,A6,A11,JORDAN16:21;
  end;
  suppose that
A12: p <> E-max C and
A13: LE p, E-max C, C and
A14: LE E-max C,q, C and
A15: q <> E-max C;
A16: now
      assume
A17:  W-min C in R_Segment(Upper_Arc C,W-min C,E-max C,p)
      /\ L_Segment(Lower_Arc C,E-max C,W-min C,q);
      then W-min C in R_Segment(Upper_Arc C,W-min C,E-max C,p) by
XBOOLE_0:def 4;
      then
A18:  p = W-min C by A6,JORDAN6:60;
W-min C in L_Segment(Lower_Arc C,E-max C,W-min C,q) by A17,XBOOLE_0:def 4;
      hence contradiction by A1,A7,A18,JORDAN6:59;
    end;
    p in Upper_Arc C by A13,JORDAN17:3;
    then
A19: LE p,E-max C,Upper_Arc C,W-min C,E-max C by A6,JORDAN5C:10;
A20: R_Segment(Upper_Arc C,W-min C,E-max C,p) =
    Segment(Upper_Arc C,W-min C,E-max C,p,E-max C) by Th14;
    then
A21: E-max C in R_Segment(Upper_Arc C,W-min C,E-max C,p) by A19,JORDAN16:5;
    q in Lower_Arc C by A14,JORDAN17:4;
    then
A22: LE E-max C,q,Lower_Arc C,E-max C,W-min C by A7,JORDAN5C:10;
A23: L_Segment(Lower_Arc C,E-max C,W-min C,q) =
    Segment(Lower_Arc C,E-max C,W-min C,E-max C,q) by Th15;
    then E-max C in L_Segment(Lower_Arc C,E-max C,W-min C,q) by A22,JORDAN16:5;
    then
A24: E-max C in R_Segment(Upper_Arc C,W-min C,E-max C,p)
    /\ L_Segment(Lower_Arc C,E-max C,W-min C,q) by A21,XBOOLE_0:def 4;
A25: R_Segment(Upper_Arc C,W-min C,E-max C,p) c= Upper_Arc C by JORDAN6:20;
A26: L_Segment(Lower_Arc C,E-max C,W-min C,q) c= Lower_Arc C by JORDAN6:19;
    Upper_Arc C /\ Lower_Arc C = {W-min C, E-max C} by JORDAN6:def 9;
    then
A27: R_Segment(Upper_Arc C,W-min C,E-max C,p)
    /\ L_Segment(Lower_Arc C,E-max C,W-min C,q) = {E-max C}
    by A16,A24,A25,A26,TOPREAL8:1,XBOOLE_1:27;
A28: R_Segment(Upper_Arc C,W-min C,E-max C,p) is_an_arc_of p, E-max C
    by A6,A12,A19,A20,JORDAN16:21;
A29: L_Segment(Lower_Arc C,E-max C,W-min C,q) is_an_arc_of E-max C,q
    by A7,A15,A22,A23,JORDAN16:21;
    Segment(p,q,C) = R_Segment(Upper_Arc C,W-min C,E-max C,p)
    \/ L_Segment(Lower_Arc C,E-max C,W-min C,q) by A13,A14,Th12;
    hence thesis by A27,A28,A29,TOPREAL1:2;
  end;
  suppose that
A30: q = E-max C and
A31: LE p, E-max C, C and
A32: LE E-max C,q, C;
    p in Upper_Arc C by A31,JORDAN17:3;
    then
A33: LE p,E-max C,Upper_Arc C,W-min C,E-max C by A6,JORDAN5C:10;
A34: R_Segment(Upper_Arc C,W-min C,E-max C,p) =
    Segment(Upper_Arc C,W-min C,E-max C,p,E-max C) by Th14;
    then
A35: E-max C in R_Segment(Upper_Arc C,W-min C,E-max C,p) by A33,JORDAN16:5;
A36: L_Segment(Lower_Arc C,E-max C,W-min C,q) = {E-max C} by A7,A30,JORDAN6:21;
    Segment(p,q,C) = R_Segment(Upper_Arc C,W-min C,E-max C,p)
    \/ L_Segment(Lower_Arc C,E-max C,W-min C,q) by A31,A32,Th12
      .= R_Segment(Upper_Arc C,W-min C,E-max C,p) by A35,A36,ZFMISC_1:40;
    hence thesis by A1,A6,A30,A33,A34,JORDAN16:21;
  end;
  suppose that
A37: p = E-max C and
A38: LE p, E-max C, C and
A39: LE E-max C,q, C;
    q in Lower_Arc C by A39,JORDAN17:4;
    then
A40: LE E-max C,q,Lower_Arc C,E-max C,W-min C by A7,JORDAN5C:10;
A41: L_Segment(Lower_Arc C,E-max C,W-min C,q) =
    Segment(Lower_Arc C,E-max C,W-min C,E-max C,q) by Th15;
    then
A42: E-max C in L_Segment(Lower_Arc C,E-max C,W-min C,q) by A40,JORDAN16:5;
A43: R_Segment(Upper_Arc C,W-min C,E-max C,p) = {E-max C} by A6,A37,JORDAN6:23;
    Segment(p,q,C) = R_Segment(Upper_Arc C,W-min C,E-max C,p)
    \/ L_Segment(Lower_Arc C,E-max C,W-min C,q) by A38,A39,Th12
      .= L_Segment(Lower_Arc C,E-max C,W-min C,q) by A42,A43,ZFMISC_1:40;
    hence thesis by A1,A7,A37,A40,A41,JORDAN16:21;
  end;
  suppose that
A44: LE E-max C,p, C and
A45: not LE p, E-max C, C;
A46: Segment(p,q,C) = Segment(Lower_Arc C,E-max C,W-min C,p,q) by A2,A44,Th11;
    not p in Upper_Arc C by A45,Th6;
    then LE p, q, Lower_Arc C, E-max C, W-min C by A2,JORDAN6:def 10;
    hence thesis by A1,A7,A46,JORDAN16:21;
  end;
end;

theorem Th18:  :: poprawic JORDAN7:7
  C = Segment(W-min C,W-min C,C)
proof
  set X = {p: LE W-min C,p,C or W-min C in C & p=W-min C};
A1: Segment(W-min C,W-min C,C) = X by JORDAN7:def 1;
  thus C c= Segment(W-min C,W-min C,C)
  proof
    let e be set;
    assume
A2: e in C;
    then reconsider p = e as Point of TOP-REAL 2;
    LE W-min C,p,C by A2,JORDAN7:3;
    hence thesis by A1;
  end;
  thus thesis by JORDAN16:6;
end;

theorem Th19:
  for q being Point of TOP-REAL 2 st q in C
  holds Segment(q,W-min C,C) is compact
proof
  let q be Point of TOP-REAL 2 such that
A1: q in C;
  per cases;
  suppose q = W-min C;
    hence thesis by Th18;
  end;
  suppose q <> W-min C;
    hence thesis by A1,Th16,JORDAN5A:1;
  end;
end;

theorem Th20:
  for q1,q2 being Point of TOP-REAL 2 st LE q1,q2,C
  holds Segment(q1,q2,C) is compact
proof
  let q1,q2 be Point of TOP-REAL 2 such that
A1: LE q1,q2,C;
A2: q1 in C by A1,JORDAN7:5;
  per cases;
  suppose q2 = W-min C;
    hence thesis by A2,Th19;
  end;
  suppose q1 = q2 & q2 <> W-min C;
    then Segment(q1,q2,C) = {q1} by A2,JORDAN7:8;
    hence thesis;
  end;
  suppose q1 <> q2 & q2 <> W-min C;
    hence thesis by A1,Th17,JORDAN5A:1;
  end;
end;

begin :: The concept of a segmentation

definition
  let C;
  mode Segmentation of C -> FinSequence of TOP-REAL 2 means
    :Def3:
    it/.1=W-min C & it is one-to-one & 8<=len it & rng it c= C &
(for i being Element of NAT st 1<=i & i<len it holds LE it/.i,it/.(i+1),C) &
    (for i being Element of NAT st 1<=i & i+1<len it holds
    Segment(it/.i,it/.(i+1),C) /\ Segment(it/.(i+1),it/.(i+2),C)={it/.(i+1)}) &
    Segment(it/.len it,it/.1,C) /\ Segment(it/.1,it/.2,C)={it/.1} &
    Segment(it/.(len it-' 1),it/.len it,C)/\ Segment(it/.len it,it/.1,C)
    ={it/.len it} &
    Segment(it/.(len it-'1),it/.len it,C) misses Segment(it/.1,it/.2,C) &
    (for i,j being Element of NAT st 1<=i & i < j & j < len it &
    not i,j are_adjacent1
    holds Segment(it/.i,it/.(i+1),C) misses Segment(it/.j,it/.(j+1),C)) &
    for i being Element of NAT st 1 < i & i+1 < len it holds
    Segment(it/.len it,it/.1,C) misses Segment(it/.i,it/.(i+1),C);
  existence
  proof
    consider h being FinSequence of the carrier of TOP-REAL 2 such that
A1: h.1=W-min C and
A2: h is one-to-one and
A3: 8<=len h and
A4: rng h c= C and
A5: for i being Element of NAT st 1<=i & i<len h holds LE h/.i,h/.(i+1),C and
    for i being Element of NAT,W being Subset of Euclid 2 st 1<=i & i<len h
    & W=Segment(h/.i,h/.(i+1),C) holds diameter(W)<1
    and for W being Subset of Euclid 2 st W=Segment(h/.len h,h/.1,C) holds
    diameter(W)<1 and
A6: for i being Element of NAT st 1<=i & i+1<len h holds
    Segment(h/.i,h/.(i+1),C)/\ Segment(h/.(i+1),h/.(i+2),C)={h/.(i+1)} and
A7: Segment(h/.len h,h/.1,C)/\ Segment(h/.1,h/.2,C)={h/.1} and
A8: Segment(h/.(len h-' 1),h/.len h,C)/\ Segment(h/.len h,h/.1,C)={h/.len h}
    and
A9: Segment(h/.(len h-'1),h/.len h,C) misses Segment(h/.1,h/.2,C) and
A10: for i,j being Element of NAT st 1<=i & i < j & j < len h &
    not i,j are_adjacent1
    holds Segment(h/.i,h/.(i+1),C) misses Segment(h/.j,h/.(j+1),C) and
A11: for i being Element of NAT st 1 < i & i+1 < len h holds
    Segment(h/.len h,h/.1,C) misses Segment(h/.i,h/.(i+1),C) by JORDAN7:20;
    reconsider h as non empty FinSequence of the carrier of TOP-REAL 2
    by A3,CARD_1:27;
    take h;
    1 in dom h by FINSEQ_5:6;
    hence h/.1=W-min C by A1,PARTFUN1:def 6;
    thus h is one-to-one by A2;
    thus 8<=len h by A3;
    thus rng h c= C by A4;
    thus
    for i being Element of NAT st 1<=i & i<len h holds LE h/.i,h/.(i+1),C
    by A5;
    thus for i being Element of NAT st 1<=i & i+1<len h holds
    Segment(h/.i,h/.(i+1),C) /\ Segment(h/.(i+1),h/.(i+2),C)={h/.(i+1)} by A6;
    thus Segment(h/.len h,h/.1,C) /\ Segment(h/.1,h/.2,C)={h/.1} by A7;
    thus Segment(h/.(len h-' 1),h/.len h,C)/\ Segment(h/.len h,h/.1,C)
    ={h/.len h} by A8;
    thus
    Segment(h/.(len h-'1),h/.len h,C) misses Segment(h/.1,h/.2,C) by A9;
    thus for i,j being Element of NAT
    st 1<=i & i < j & j < len h & not i,j are_adjacent1
    holds Segment(h/.i,h/.(i+1),C) misses Segment(h/.j,h/.(j+1),C) by A10;
    thus thesis by A11;
  end;
end;

registration
  let C;
  cluster -> non trivial for Segmentation of C;
  coherence
  proof
    let S be Segmentation of C;
    len S >= 8 by Def3;
    then len S >= 2 by XXREAL_0:2;
    hence thesis by NAT_D:60;
  end;
end;

theorem Th21:
  for S being Segmentation of C, i st 1<=i & i <= len S holds S/.i in C
proof
  let S be Segmentation of C, i;
  assume that
A1: 1<=i and
A2: i <= len S;
  i in dom S by A1,A2,FINSEQ_3:25;
  then
A3: S/.i in rng S by PARTFUN2:2;
  rng S c= C by Def3;
  hence thesis by A3;
end;

begin :: The segments of a segmentation

definition
  let C;
  let i be Nat;
  let S be Segmentation of C;
  func Segm(S,i) -> Subset of TOP-REAL 2 equals
  :Def4:
  Segment(S/.i,S/.(i+1),C) if 1<=i & i<len S
  otherwise Segment(S/.len S,S/.1,C);
  correctness;
end;

theorem
  for S being Segmentation of C st i in dom S holds Segm(S,i) c= C
proof
  let S be Segmentation of C;
  assume i in dom S;
  then
A1: 1 <= i by FINSEQ_3:25;
  i < len S or i >= len S;
  then Segm(S,i) = Segment(S/.i,S/.(i+1),C) or
  Segm(S,i) = Segment(S/.len S,S/.1,C) by A1,Def4;
  hence thesis by JORDAN16:6;
end;

registration
  let C;
  let S be Segmentation of C, i;
  cluster Segm(S,i) -> non empty compact;
  coherence
  proof
    per cases;
    suppose
A1:   1<=i & i<len S;
      then
A2:   Segm(S,i) = Segment(S/.i,S/.(i+1),C) by Def4;
      LE S/.i,S/.(i+1),C by A1,Def3;
      hence thesis by A2,Th20,JORDAN7:6;
    end;
    suppose not(1<=i & i<len S);
      then
A3:   Segm(S,i) = Segment(S/.len S,S/.1,C) by Def4;
      8 <= len S by Def3;
      then 1 <= len S by XXREAL_0:2;
      then
A4:   S/.len S in C by Th21;
      S/.1 = W-min C by Def3;
      hence thesis by A3,A4,Th19,JORDAN16:19;
    end;
  end;
end;

theorem
  for S being Segmentation of C, p st p in C
  ex i being Nat st i in dom S & p in Segm(S,i)
proof
  let S be Segmentation of C, p such that
A1: p in C;
  set X = { i : i in dom S & LE S/.i, p, C };
A2: X c= dom S
  proof
    let e be set;
    assume e in X;
    then ex i st e = i & i in dom S & LE S/.i, p, C;
    hence thesis;
  end;
A3: 1 in dom S by FINSEQ_5:6;
A4: W-min C = S/.1 by Def3;
  then LE S/.1, p, C by A1,JORDAN7:3;
  then 1 in X by A3;
  then reconsider X as finite non empty Subset of NAT
  by A2,XBOOLE_1:1;
  take max X;
A5: max X in X by XXREAL_2:def 8;
  hence max X in dom S by A2;
A6: 1 <= max X by A2,A5,FINSEQ_3:25;
A7: max X <= len S by A2,A5,FINSEQ_3:25;
A8: ex i st max X = i & i in dom S & LE S/.i, p, C by A5;
  reconsider mX = max X as Element of NAT by ORDINAL1:def 12;
  per cases by A7,XXREAL_0:1;
  suppose
A9: max X < len S;
A10: 1 <= max X + 1 by NAT_1:11;
    max X +1 <= len S by A9,NAT_1:13;
    then
A11: mX + 1 in dom S by A10,FINSEQ_3:25;
A12: S is one-to-one by Def3;
    max X +1 >= 1+1 by A6,XREAL_1:6;
    then max X + 1 <> 1;
    then
A13: S/.(max X+1) <> S/.1 by A3,A11,A12,PARTFUN2:10;
A14: S/.(max X+1) in rng S by A11,PARTFUN2:2;
A15: rng S c= C by Def3;
    now
      assume LE S/.(max X+1),p,C;
      then max X +1 in X by A11;
      then max X +1 <= max X by XXREAL_2:def 8;
      hence contradiction by XREAL_1:29;
    end;
    then LE p,S/.(max X+1),C by A1,A14,A15,JORDAN16:7;
    then p in {p1: LE S/.(max X),p1,C & LE p1,S/.(max X+1),C} by A8;
    then p in Segment(S/.max X,S/.(max X+1),C) by A4,A13,JORDAN7:def 1;
    hence thesis by A6,A9,Def4;
  end;
  suppose
A16: max X = len S;
    now per cases;
      case p<>W-min C;
        thus LE S/.len S,p,C by A8,A16;
      end;
      case p=W-min C;
A17:    S/.len S in rng S by REVROT_1:3;
        rng S c= C by Def3;
        hence S/.len S in C by A17;
      end;
    end;
    then p in {p1: LE S/.len S,p1,C or S/.len S in C & p1=W-min C};
    then p in Segment(S/.len S,S/.1,C) by A4,JORDAN7:def 1;
    hence thesis by A16,Def4;
  end;
end;

theorem Th24:
  for S being Segmentation of C
  for i,j st 1<=i & i< j & j<len S & not i,j are_adjacent1
  holds Segm(S,i) misses Segm(S,j)
proof
  let S be Segmentation of C;
  let i,j such that
A1: 1<=i and
A2: i < j and
A3: j<len S and
A4: not i,j are_adjacent1;
  i < len S by A2,A3,XXREAL_0:2;
  then
A5: Segm(S,i) = Segment(S/.i,S/.(i+1),C) by A1,Def4;
  1 < j by A1,A2,XXREAL_0:2;
  then Segm(S,j) = Segment(S/.j,S/.(j+1),C) by A3,Def4;
  hence thesis by A1,A2,A3,A4,A5,Def3;
end;

theorem Th25:
  for S being Segmentation of C for j st 1<j & j<len S -' 1
  holds Segm(S,len S) misses Segm(S,j)
proof
  let S be Segmentation of C;
  let j such that
A1: 1<j and
A2: j<len S -' 1;
A3: Segm(S,len S) = Segment(S/.len S,S/.1,C) by Def4;
A4: j+1 < len S by A2,NAT_D:53;
  j < len S by A2,NAT_D:44;
  then Segm(S,j) = Segment(S/.j,S/.(j+1),C) by A1,Def4;
  hence thesis by A1,A3,A4,Def3;
end;

theorem Th26:
  for S being Segmentation of C
  for i,j st 1<=i & i< j & j<len S & i,j are_adjacent1
  holds Segm(S,i) /\ Segm(S,j)={S/.(i+1)}
proof
  let S be Segmentation of C;
  let i,j such that
A1: 1<=i and
A2: i< j and
A3: j<len S and
A4: i,j are_adjacent1;
  i < len S by A2,A3,XXREAL_0:2;
  then
A5: Segm(S,i) = Segment(S/.i,S/.(i+1),C) by A1,Def4;
  1 < j by A1,A2,XXREAL_0:2;
  then
A6: Segm(S,j) = Segment(S/.j,S/.(j+1),C) by A3,Def4;
  j+1 > i by A2,NAT_1:13;
  then j = i+1 by A4,GOBRD10:def 1;
  then j+1 = i+(1+1);
  hence thesis by A1,A3,A5,A6,Def3;
end;

theorem Th27:
  for S being Segmentation of C
  for i,j st 1<=i & i< j & j<len S & i,j are_adjacent1
  holds Segm(S,i) meets Segm(S,j)
proof
  let S be Segmentation of C;
  let i,j;
  assume that
A1: 1<=i and
A2: i< j and
A3: j<len S and
A4: i,j are_adjacent1;
  Segm(S,i) /\ Segm(S,j)={S/.(i+1)} by A1,A2,A3,A4,Th26;
  hence thesis by XBOOLE_0:def 7;
end;

theorem Th28:
  for S being Segmentation of C holds Segm(S,len S) /\ Segm(S,1) = {S/.1}
proof
  let S be Segmentation of C;
A1: Segm(S,len S) = Segment(S/.len S,S/.1,C) by Def4;
  len S >= 8 by Def3;
  then 1 < len S by XXREAL_0:2;
  then Segm(S,1) = Segment(S/.1,S/.(1+1),C) by Def4;
  hence thesis by A1,Def3;
end;

theorem Th29:
  for S being Segmentation of C holds Segm(S,len S) meets Segm(S,1)
proof
  let S be Segmentation of C;
  Segm(S,len S) /\ Segm(S,1) = {S/.1} by Th28;
  hence thesis by XBOOLE_0:def 7;
end;

theorem Th30:
  for S being Segmentation of C
  holds Segm(S,len S) /\ Segm(S,len S -' 1) = {S/.len S}
proof
  let S be Segmentation of C;
A1: Segm(S,len S) = Segment(S/.len S,S/.1,C) by Def4;
A2: len S >= 8 by Def3;
  then len S >= 1+1 by XXREAL_0:2;
  then
A3: 1 <= len S -' 1 by NAT_D:55;
A4: len S -' 1 + 1 = len S by A2,XREAL_1:235,XXREAL_0:2;
  then len S -' 1 < len S by NAT_1:13;
  then Segm(S,len S -' 1) = Segment(S/.(len S -' 1),S/.len S,C) by A3,A4,Def4;
  hence thesis by A1,Def3;
end;

theorem Th31:
  for S being Segmentation of C holds Segm(S,len S) meets Segm(S,len S -' 1)
proof
  let S be Segmentation of C;
  Segm(S,len S) /\ Segm(S,len S -' 1) = {S/.len S} by Th30;
  hence thesis by XBOOLE_0:def 7;
end;

begin :: The diameter of a segmentation

definition
  let n;
  let C be Subset of TOP-REAL n;
  func diameter C -> Real means
  :Def5:
  ex W being Subset of Euclid n st W = C & it = diameter W;
  existence
  proof
    the TopStruct of TOP-REAL n =TopSpaceMetr Euclid n by EUCLID:def 8
      .= TopStruct (#the carrier of Euclid n,Family_open_set Euclid n #)
    by PCOMPS_1:def 5;
    then reconsider W = C as Subset of Euclid n;
    take diameter W, W;
    thus thesis;
  end;
  correctness;
end;

definition
  let C;
  let S be Segmentation of C;
  func diameter S -> Real means
  :Def6:
  ex S1 being non empty finite Subset of REAL st
  S1 = { diameter Segm(S,i): i in dom S} & it = max S1;
  existence
  proof
    deffunc F(Element of NAT) = diameter Segm(S,$1);
    defpred P[set] means $1 in dom S;
    set S1 = { F(i): P[i]};
    set S2 = { F(i): i in dom S};
A1: dom S is finite;
A2: S2 is finite from FRAENKEL:sch 21(A1);
A3: S1 is Subset of REAL from DOMAIN_1:sch 8;
    1 in dom S by FINSEQ_5:6;
    then diameter Segm(S,1) in S1;
    then reconsider S1 as non empty finite Subset of REAL by A2,A3;
    reconsider mS1 = max S1 as Element of REAL by XREAL_0:def 1;
    take mS1, S1;
    thus thesis;
  end;
  correctness;
end;

theorem
  for S being Segmentation of C, i holds diameter Segm(S,i) <= diameter S
proof
  let S be Segmentation of C, i;
  consider S1 be non empty finite Subset of REAL such that
A1: S1 = { diameter Segm(S,j): j in dom S} and
A2: diameter S = max S1 by Def6;
  per cases;
  suppose 1 <= i & i < len S;
    then i in dom S by FINSEQ_3:25;
    then diameter Segm(S,i) in S1 by A1;
    hence thesis by A2,XXREAL_2:def 8;
  end;
  suppose
A3: not(1 <= i & i < len S);
A4: Segm(S,len S) = Segment(S/.len S,S/.1,C) by Def4
      .= Segm(S,i) by A3,Def4;
    len S in dom S by FINSEQ_5:6;
    then diameter Segm(S,i) in S1 by A1,A4;
    hence thesis by A2,XXREAL_2:def 8;
  end;
end;

theorem Th33:
  for S being Segmentation of C, e being Real
  st for i holds diameter Segm(S,i) < e holds diameter S < e
proof
  let S be Segmentation of C, e be Real such that
A1: for i holds diameter Segm(S,i) < e;
  consider S1 being non empty finite Subset of REAL such that
A2: S1 = { diameter Segm(S,i): i in dom S} and
A3: diameter S = max S1 by Def6;
  diameter S in S1 by A3,XXREAL_2:def 8;
  then ex i st diameter S = diameter Segm(S,i) & i in dom S by A2;
  hence thesis by A1;
end;

theorem
  for e being Real st e > 0 ex S being Segmentation of C st diameter S < e
proof
  let e be Real;
  assume e > 0;
  then consider h being FinSequence of the carrier of TOP-REAL 2 such that
A1: h.1=W-min C and
A2: h is one-to-one and
A3: 8<=len h and
A4: rng h c= C and
A5: for i being Element of NAT st 1<=i & i<len h holds LE h/.i,h/.(i+1),C and
A6: for i being Element of NAT,W being Subset of Euclid 2
  st 1<=i & i<len h & W=Segment(h/.i,h/.(i+1),C) holds diameter(W)<e and
A7: for W being Subset of Euclid 2 st
  W=Segment(h/.len h,h/.1,C) holds diameter(W)<e and
A8: for i being Element of NAT st 1<=i & i+1<len h holds
  Segment(h/.i,h/.(i+1),C)/\ Segment(h/.(i+1),h/.(i+2),C)={h/.(i+1)} and
A9: Segment(h/.len h,h/.1,C)/\ Segment(h/.1,h/.2,C)={h/.1} and
A10: Segment(h/.(len h-' 1),h/.len h,C)/\ Segment(h/.len h,h/.1,C)={h/.len h}
  and
A11: Segment(h/.(len h-'1),h/.len h,C) misses Segment(h/.1,h/.2,C) and
A12: for i,j being Element of NAT st 1<=i & i < j & j < len h &
  not i,j are_adjacent1
  holds Segment(h/.i,h/.(i+1),C) misses Segment(h/.j,h/.(j+1),C) and
A13: for i being Element of NAT st 1 < i & i+1 < len h holds
  Segment(h/.len h,h/.1,C) misses Segment(h/.i,h/.(i+1),C) by JORDAN7:20;
  h <> {} by A3,CARD_1:27;
  then 1 in dom h by FINSEQ_5:6;
  then h/.1 = W-min C by A1,PARTFUN1:def 6;
  then reconsider h as Segmentation of C
  by A2,A3,A4,A5,A8,A9,A10,A11,A12,A13,Def3;
  take h;
  diameter Segm(h,i) < e
  proof
A14: ex W being Subset of Euclid 2 st ( W = Segm(h,i))&(
    diameter Segm(h,i) = diameter W) by Def5;
    per cases;
    suppose
A15:  1<=i & i<len h;
      then Segm(h,i) = Segment(h/.i,h/.(i+1),C) by Def4;
      hence thesis by A6,A14,A15;
    end;
    suppose not(1<=i & i<len h);
      then Segm(h,i) = Segment(h/.len h,h/.1,C) by Def4;
      hence thesis by A7,A14;
    end;
  end;
  hence thesis by Th33;
end;

begin :: The concept of the gap of a segmentation

definition
  let C;
  let S be Segmentation of C;
  func S-Gap S -> Real means
  :Def7:
  ex S1,S2 being non empty finite Subset of REAL st
  S1 = { dist_min(Segm(S,i),Segm(S,j)):
  1<=i & i< j & j<len S & not i,j are_adjacent1} &
  S2 = { dist_min(Segm(S,len S),Segm(S,k)): 1<k & k<len S -' 1 } &
  it = min(min S1,min S2);
  existence
  proof
    deffunc F(Element of NAT) = dist_min(Segm(S,len S),Segm(S,$1));
    deffunc F(Element of NAT,Element of NAT) = dist_min(Segm(S,$1),Segm(S,$2));
    defpred P[Element of NAT] means 1<$1 & $1<len S -' 1;
    defpred Q[Element of NAT] means $1 in dom S;
    defpred R[Element of NAT,Element of NAT] means
    1<=$1 & $1< $2 & $2<len S & not $1,$2 are_adjacent1;
    defpred W[Element of NAT,Element of NAT] means Q[$1] & Q[$2];
    set S1 = { F(i,j) : R[i,j] };
    set S2 = { F(j) : P[j] };
    set B = { F(i,j) : W[i,j] };
    set B9 = { F(i,j) : i in dom S & j in dom S };
    set A = { F(j) : Q[j] };
    set A9 = { F(j) : j in dom S };
A1: P[j] implies Q[j]
    proof
      assume
A2:   1<j;
A3:   len S -' 1 <= len S by NAT_D:35;
      assume j<len S -' 1;
      then j < len S by A3,XXREAL_0:2;
      hence thesis by A2,FINSEQ_3:25;
    end;
A4: S2 c= A from FRAENKEL:sch 1(A1);
A5: for i, j holds R[i,j] implies W[i,j]
    proof
      let i,j such that
A6:   1<=i and
A7:   i< j and
A8:   j<len S and not i,j are_adjacent1;
      i < len S by A7,A8,XXREAL_0:2;
      hence i in dom S by A6,FINSEQ_3:25;
      1 < j by A6,A7,XXREAL_0:2;
      hence thesis by A8,FINSEQ_3:25;
    end;
A9: S1 c= B from FRAENKEL:sch 2(A5);
A10: S1 c= REAL
    proof
      let x be set;
      assume x in S1;
      then ex i,j st x = dist_min(Segm(S,i),Segm(S,j)) &
      1<=i & i<j & j<len S & not i,j are_adjacent1;
      hence thesis;
    end;
A11: S2 c= REAL
    proof
      let x be set;
      assume x in S2;
      then ex j st x = dist_min(Segm(S,len S),Segm(S,j)) & 1<j & j<len S -' 1;
      hence thesis;
    end;
A12: dom S is finite;
A13: A9 is finite from FRAENKEL:sch 21(A12);
A14: B9 is finite from FRAENKEL:sch 22(A12,A12);
A15: 3 <> 1+1;
    1 <> 3+1;
    then
A16: not 1,3 are_adjacent1 by A15,GOBRD10:def 1;
A17: len S >= 7+1 by Def3;
    then 3<len S by XXREAL_0:2;
    then
A18: dist_min(Segm(S,1),Segm(S,3)) in S1 by A16;
    2+1 < len S by A17,XXREAL_0:2;
    then 2<len S -' 1 by NAT_D:52;
    then dist_min(Segm(S,len S),Segm(S,2)) in S2;
    then reconsider S1, S2 as non empty finite Subset of REAL
    by A4,A9,A10,A11,A13,A14,A18;
    reconsider mm = min(min S1,min S2) as Element of REAL by XREAL_0:def 1;
    take mm,S1,S2;
    thus thesis;
  end;
  correctness;
end;

theorem Th35:
  for S being Segmentation of C ex F being finite non empty Subset of REAL st
  F = { dist_min(Segm(S,i),Segm(S,j)):
  1<=i & i<j & j<=len S & Segm(S,i) misses Segm(S,j)} & S-Gap S = min F
proof
  let S be Segmentation of C;
  consider S1,S2 being non empty finite Subset of REAL such that
A1: S1 = { dist_min(Segm(S,i),Segm(S,j)):
  1<=i & i< j & j<len S & not i,j are_adjacent1} and
A2: S2 = { dist_min(Segm(S,len S),Segm(S,k)): 1<k & k<len S -' 1 } and
A3: S-Gap S = min(min S1,min S2) by Def7;
  take F = S1 \/ S2;
  set X = { dist_min(Segm(S,i),Segm(S,j)):
  1<=i & i<j & j<=len S & Segm(S,i) misses Segm(S,j)};
  thus F c= X
  proof
    let e be set;
    assume
A4: e in F;
    per cases by A4,XBOOLE_0:def 3;
    suppose e in S1;
      then consider i,j such that
A5:   e = dist_min(Segm(S,i),Segm(S,j)) and
A6:   1<=i and
A7:   i< j and
A8:   j<len S and
A9:   not i,j are_adjacent1 by A1;
      Segm(S,i) misses Segm(S,j) by A6,A7,A8,A9,Th24;
      hence thesis by A5,A6,A7,A8;
    end;
    suppose e in S2;
      then consider j such that
A10:  e = dist_min(Segm(S,len S),Segm(S,j)) and
A11:  1<j and
A12:  j<len S -' 1 by A2;
A13:  j < len S by A12,NAT_D:44;
      Segm(S,len S) misses Segm(S,j) by A11,A12,Th25;
      hence thesis by A10,A11,A13;
    end;
  end;
  thus X c= F
  proof
    let e be set;
    assume e in X;
    then consider i,j such that
A14: e = dist_min(Segm(S,i),Segm(S,j)) and
A15: 1<=i and
A16: i<j and
A17: j<=len S and
A18: Segm(S,i) misses Segm(S,j);
A19: i < len S by A16,A17,XXREAL_0:2;
    per cases by A17,XXREAL_0:1;
    suppose that
A20:  j < len S;
      not i,j are_adjacent1 by A15,A16,A18,A20,Th27;
      then e in S1 by A1,A14,A15,A16,A20;
      hence thesis by XBOOLE_0:def 3;
    end;
    suppose
A21:  j = len S;
      then 1 <> i by A18,Th29;
      then
A22:  1 < i by A15,XXREAL_0:1;
A23:  i <= len S -' 1 by A19,NAT_D:49;
      i <> len S -' 1 by A18,A21,Th31;
      then i < len S -' 1 by A23,XXREAL_0:1;
      then e in S2 by A2,A14,A21,A22;
      hence thesis by XBOOLE_0:def 3;
    end;
  end;
  thus thesis by A3,XXREAL_2:9;
end;

theorem
  for S being Segmentation of C holds S-Gap S > 0
proof
  let S be Segmentation of C;
  consider F being finite non empty Subset of REAL such that
A1: F = { dist_min(Segm(S,i),Segm(S,j)):
  1<=i & i<j & j<=len S & Segm(S,i) misses Segm(S,j)} and
A2: S-Gap S = min F by Th35;
  S-Gap S in F by A2,XXREAL_2:def 7;
  then ex i,j st S-Gap S = dist_min(Segm(S,i),Segm(S,j)) &
  1<=i & i<j & j<=len S & Segm(S,i) misses Segm(S,j) by A1;
  hence thesis by Th7;
end;