:: On a Dividing Function of the Simple Closed Curve into Segments
::  by Yatsuka Nakamura
::
:: Received June 16, 1998
:: Copyright (c) 1998-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, PRE_TOPC, EUCLID, ARYTM_1, SUBSET_1, XXREAL_0, ARYTM_3,
      RCOMP_1, XBOOLE_0, TOPREAL2, PSCOMP_1, JORDAN6, TOPREAL1, JORDAN3,
      TARSKI, FUNCT_1, BORSUK_1, RELAT_1, TOPS_2, ORDINAL2, STRUCT_0, FINSEQ_1,
      CARD_1, XXREAL_1, REAL_1, PARTFUN1, MEASURE5, GOBRD10, ORDINAL4;
 notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, REAL_1, NAT_1, RCOMP_1, NAT_D,
      FINSEQ_1, FUNCT_1, RELSET_1, PARTFUN1, SEQ_1, VALUED_0, TOPREAL1,
      TOPREAL2, TBSP_1, GOBRD10, PRE_TOPC, TOPS_2, FINSEQ_6, STRUCT_0,
      COMPTS_1, EUCLID, PSCOMP_1, JORDAN5C, JORDAN6, TOPMETR, XXREAL_0;
 constructors REAL_1, RCOMP_1, NAT_D, TOPS_2, COMPTS_1, TBSP_1, TOPMETR,
      TOPREAL1, PSCOMP_1, GOBRD10, SEQ_1, JORDAN5C, JORDAN6, XXREAL_2,
      FINSEQ_6;
 registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0,
      PRE_TOPC, EUCLID, TOPREAL1, BORSUK_2, VALUED_0, COMPTS_1, XXREAL_2,
      FINSEQ_1, FUNCT_1;
 requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
 definitions TARSKI, XBOOLE_0, FUNCT_1, STRUCT_0;
 theorems TARSKI, JORDAN6, TOPREAL1, TOPREAL5, JORDAN5C, UNIFORM1, PRE_TOPC,
      FUNCT_2, TOPS_2, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, NAT_1, FINSEQ_4,
      GOBRD10, SPRECT_1, XBOOLE_0, XBOOLE_1, FINSEQ_3, BORSUK_1, COMPTS_1,
      RELSET_1, JORDAN5B, PARTFUN2, XCMPLX_1, XREAL_1, XXREAL_0, PARTFUN1,
      XXREAL_1, XXREAL_2, SEQM_3, NAT_D, XREAL_0, FINSEQ_6;
 schemes DOMAIN_1, NAT_1;

begin :: Definition of the Segment and its property

reserve p,p1,p2,p3,q for Point of TOP-REAL 2;

Lm1: 2-'1 = 2-1 by XREAL_1:233
  .=1;

Lm2: for i, j, k be Element of NAT holds i-'k <= j implies i <= j + k
proof
  let i, j, k be Element of NAT;
  assume
A1: i-'k <= j;
  per cases;
  suppose
A2: i >= k;
    i-'k +k <= j + k by A1,XREAL_1:6;
    hence thesis by A2,XREAL_1:235;
  end;
  suppose
A3: i <= k;
    k <= j + k by NAT_1:11;
    hence thesis by A3,XXREAL_0:2;
  end;
end;

Lm3: for i, j, k be Element of NAT holds j + k <= i implies k <= i -' j
proof
  let i, j, k be Element of NAT;
  assume
A1: j + k <= i;
  per cases by A1,XXREAL_0:1;
  suppose
    j + k = i;
    hence thesis by NAT_D:34;
  end;
  suppose
    j + k < i;
    hence thesis by Lm2;
  end;
end;

theorem Th1:
  for P being compact non empty Subset of TOP-REAL 2 st P is
  being_simple_closed_curve holds W-min(P) in Lower_Arc(P) & E-max(P) in
  Lower_Arc(P) & W-min(P) in Upper_Arc(P) & E-max(P) in Upper_Arc(P)
proof
  let P be compact non empty Subset of TOP-REAL 2;
  assume P is being_simple_closed_curve;
  then
  Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) & Lower_Arc(P) is_an_arc_of
  E-max(P),W-min(P) by JORDAN6:50;
  hence thesis by TOPREAL1:1;
end;

theorem Th2:
  for P being compact non empty Subset of TOP-REAL 2,q st P is
  being_simple_closed_curve & LE q,W-min(P),P holds q=W-min(P)
proof
  let P be compact non empty Subset of TOP-REAL 2,q;
  assume P is being_simple_closed_curve & LE q,W-min(P),P;
  then
  LE q,W-min(P),Upper_Arc(P),W-min(P),E-max(P) & Upper_Arc(P) is_an_arc_of
  W-min(P),E-max(P) by JORDAN6:def 8,def 10;
  hence thesis by JORDAN6:54;
end;

theorem Th3:
  for P being compact non empty Subset of TOP-REAL 2,q st P is
  being_simple_closed_curve & q in P holds LE W-min(P),q,P
proof
  let P be compact non empty Subset of TOP-REAL 2,q;
  assume that
A1: P is being_simple_closed_curve and
A2: q in P;
A3: q in Upper_Arc(P) \/ Lower_Arc(P) by A1,A2,JORDAN6:50;
A4: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:50;
A5: W-min(P) in Upper_Arc(P) by A1,Th1;
  per cases by A3,XBOOLE_0:def 3;
  suppose
A6: q in Upper_Arc(P);
    then LE W-min(P),q,Upper_Arc(P),W-min(P),E-max(P) by A4,JORDAN5C:10;
    hence thesis by A5,A6,JORDAN6:def 10;
  end;
  suppose
A7: q in Lower_Arc(P);
    per cases;
    suppose
      not q=W-min(P);
      hence thesis by A5,A7,JORDAN6:def 10;
    end;
    suppose
A8:   q=W-min(P);
      then LE W-min(P),q,Upper_Arc(P),W-min(P),E-max(P) by A5,JORDAN5C:9;
      hence thesis by A5,A8,JORDAN6:def 10;
    end;
  end;
end;

definition
  let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL
  2;
  func Segment(q1,q2,P) -> Subset of TOP-REAL 2 equals
  :Def1:
  {p: LE q1,p,P &
LE p,q2,P} if q2<>W-min(P) otherwise {p1: LE q1,p1,P or q1 in P & p1=W-min(P)};
  correctness
  proof
    ex B being Subset of TOP-REAL 2 st (q2<>W-min(P) implies B={p: LE q1,p
,P & LE p,q2,P})& (not q2<>W-min(P) implies B={p1: LE q1,p1,P or q1 in P & p1=
    W-min(P)})
    proof
      per cases;
      suppose
A1:     q2<>W-min(P);
        defpred P[Point of TOP-REAL 2] means LE q1,$1,P & LE $1,q2,P;
        {p: P[p]} is Subset of TOP-REAL 2 from DOMAIN_1:sch 7;
        then reconsider
        C = {p: LE q1,p,P & LE p,q2,P} as Subset of TOP-REAL 2;
        q2<>W-min(P) implies C={p: LE q1,p,P & LE p,q2,P};
        hence thesis by A1;
      end;
      suppose
A2:     not q2<>W-min(P);
        defpred P[Point of TOP-REAL 2] means LE q1,$1,P or q1 in P & $1=W-min(
        P);
        {p1: P[p1]} is Subset of TOP-REAL 2 from DOMAIN_1:sch 7;
        then reconsider
        C = {p1: LE q1,p1,P or q1 in P & p1=W-min(P)} as Subset of
        TOP-REAL 2;
        not q2<>W-min(P) implies C={p1: LE q1,p1,P or q1 in P & p1=W-min(P )};
        hence thesis by A2;
      end;
    end;
    hence thesis;
  end;
end;

theorem
  for P being compact non empty Subset of TOP-REAL 2 st P is
  being_simple_closed_curve holds Segment(W-min(P),E-max(P),P)=Upper_Arc(P) &
  Segment(E-max(P),W-min(P),P)=Lower_Arc(P)
proof
  let P be compact non empty Subset of TOP-REAL 2;
  assume
A1: P is being_simple_closed_curve;
  then
A2: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by JORDAN6:def 8;
A3: {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)} = Lower_Arc(P)
  proof
A4: {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)} c= Lower_Arc(P)
    proof
      let x be set;
      assume x in {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)};
      then consider p1 such that
A5:   p1=x and
A6:   LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P);
      per cases by A6;
      suppose
A7:     LE E-max(P),p1,P;
        per cases by A5,A7,JORDAN6:def 10;
        suppose
          x in Lower_Arc(P);
          hence thesis;
        end;
        suppose
A8:       E-max(P) in Upper_Arc(P) & p1 in Upper_Arc(P) & LE E-max(P)
          ,p1,Upper_Arc(P),W-min(P),E-max(P);
A9:       Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:50;
          then LE p1,E-max(P),Upper_Arc(P),W-min(P),E-max(P) by A8,JORDAN5C:10;
          then
A10:      p1=E-max(P) by A8,A9,JORDAN5C:12;
          Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,JORDAN6:def 9;
          hence thesis by A5,A10,TOPREAL1:1;
        end;
      end;
      suppose
        E-max(P) in P & p1=W-min(P);
        then x in {W-min(P),E-max(P)} by A5,TARSKI:def 2;
        then x in Upper_Arc(P) /\ Lower_Arc(P) by A1,JORDAN6:def 9;
        hence thesis by XBOOLE_0:def 4;
      end;
    end;
    Lower_Arc(P) c= {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P) }
    proof
      let x be set;
      assume
A11:  x in Lower_Arc(P);
      then reconsider p2=x as Point of TOP-REAL 2;
      Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:50;
      then
      not (E-max P in P & p2=W-min P) implies E-max P in Upper_Arc P & p2
      in Lower_Arc P & not p2=W-min P by A11,SPRECT_1:14,TOPREAL1:1;
      then LE E-max(P),p2,P or E-max P in P & p2=W-min P by JORDAN6:def 10;
      hence thesis;
    end;
    hence thesis by A4,XBOOLE_0:def 10;
  end;
A12: E-max(P)<>W-min(P) by A1,TOPREAL5:19;
  {p: LE W-min(P),p,P & LE p,E-max(P),P} = Upper_Arc(P)
  proof
A13: {p: LE W-min(P),p,P & LE p,E-max(P),P} c= Upper_Arc(P)
    proof
      let x be set;
      assume x in {p: LE W-min(P),p,P & LE p,E-max(P),P};
      then consider p such that
A14:  p=x and
      LE W-min(P),p,P and
A15:  LE p,E-max(P),P;
      per cases by A15,JORDAN6:def 10;
      suppose
        p in Upper_Arc(P) & E-max(P) in Lower_Arc(P) & not E-max(P)= W-min(P);
        hence thesis by A14;
      end;
      suppose
        p in Upper_Arc(P) & E-max(P) in Upper_Arc(P) & LE p,E-max(P),
        Upper_Arc(P),W-min(P),E-max(P);
        hence thesis by A14;
      end;
      suppose
A16:    p in Lower_Arc(P) & E-max(P) in Lower_Arc(P) & not E-max(P)=
        W-min(P) & LE p,E-max(P),Lower_Arc(P),E-max(P),W-min(P);
        Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,JORDAN6:def 9;
        then p=E-max(P) by A16,JORDAN6:54;
        hence thesis by A2,A14,TOPREAL1:1;
      end;
    end;
    Upper_Arc(P) c= {p: LE W-min(P),p,P & LE p,E-max(P),P}
    proof
      let x be set;
      assume
A17:  x in Upper_Arc(P);
      then reconsider p2=x as Point of TOP-REAL 2;
      E-max(P) in Lower_Arc(P) by A1,Th1;
      then
A18:  LE p2,E-max(P),P by A12,A17,JORDAN6:def 10;
A19:  W-min(P) in Upper_Arc(P) by A1,Th1;
      LE W-min(P),p2,Upper_Arc(P),W-min(P),E-max(P) by A2,A17,JORDAN5C:10;
      then LE W-min(P),p2,P by A17,A19,JORDAN6:def 10;
      hence thesis by A18;
    end;
    hence thesis by A13,XBOOLE_0:def 10;
  end;
  hence thesis by A12,A3,Def1;
end;

theorem Th5:
  for P being compact non empty Subset of TOP-REAL 2, q1,q2 being
Point of TOP-REAL 2 st P is being_simple_closed_curve & LE q1,q2,P holds q1 in
  P & q2 in P
proof
  let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL
  2;
  assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P;
A3: Upper_Arc(P) \/ Lower_Arc(P)=P by A1,JORDAN6:50;
  per cases by A2,JORDAN6:def 10;
  suppose
    q1 in Upper_Arc(P) & q2 in Lower_Arc(P);
    hence thesis by A3,XBOOLE_0:def 3;
  end;
  suppose
    q1 in Upper_Arc(P) & q2 in Upper_Arc(P);
    hence thesis by A3,XBOOLE_0:def 3;
  end;
  suppose
    q1 in Lower_Arc(P) & q2 in Lower_Arc(P);
    hence thesis by A3,XBOOLE_0:def 3;
  end;
end;

theorem Th6:
  for P being compact non empty Subset of TOP-REAL 2, q1,q2 being
Point of TOP-REAL 2 st P is being_simple_closed_curve & LE q1,q2,P holds q1 in
  Segment(q1,q2,P) & q2 in Segment(q1,q2,P)
proof
  let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL
  2;
  assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P;
  hereby
    per cases;
    suppose
A3:   q2<>W-min(P);
      q1 in P by A1,A2,Th5;
      then LE q1,q1,P by A1,JORDAN6:56;
      then q1 in {p: LE q1,p,P & LE p,q2,P} by A2;
      hence q1 in Segment(q1,q2,P) by A3,Def1;
    end;
    suppose
A4:   q2=W-min(P);
      q1 in P by A1,A2,Th5;
      then LE q1,q1,P by A1,JORDAN6:56;
      then q1 in {p1: LE q1,p1,P or q1 in P & p1=W-min(P)};
      hence q1 in Segment(q1,q2,P) by A4,Def1;
    end;
  end;
  per cases;
  suppose
A5: q2<>W-min(P);
    q2 in P by A1,A2,Th5;
    then LE q2,q2,P by A1,JORDAN6:56;
    then q2 in {p: LE q1,p,P & LE p,q2,P} by A2;
    hence thesis by A5,Def1;
  end;
  suppose
A6: q2=W-min(P);
    q2 in {p1: LE q1,p1,P or q1 in P & p1=W-min(P)} by A2;
    hence thesis by A6,Def1;
  end;
end;

theorem Th7:
  for P being compact non empty Subset of TOP-REAL 2, q1 being
  Point of TOP-REAL 2 st q1 in P & P is being_simple_closed_curve holds q1 in
  Segment(q1,W-min P,P)
proof
  let P be compact non empty Subset of TOP-REAL 2, q1 be Point of TOP-REAL 2
  such that
A1: q1 in P;
  assume P is being_simple_closed_curve;
  then LE q1,q1,P by A1,JORDAN6:56;
  then q1 in {p1: LE q1,p1,P or q1 in P & p1=W-min(P)};
  hence thesis by Def1;
end;

theorem
  for P being compact non empty Subset of TOP-REAL 2, q being Point of
  TOP-REAL 2 st P is being_simple_closed_curve & q in P & q<>W-min(P) holds
  Segment(q,q,P)={q}
proof
  let P be compact non empty Subset of TOP-REAL 2, q be Point of TOP-REAL 2;
  assume that
A1: P is being_simple_closed_curve and
A2: q in P and
A3: q <> W-min P;
  for x being set holds x in Segment(q,q,P) iff x=q
  proof
    let x be set;
    hereby
      assume x in Segment(q,q,P);
      then x in {p: LE q,p,P & LE p,q,P} by A3,Def1;
      then ex p st p=x & LE q,p,P & LE p,q,P;
      hence x=q by A1,JORDAN6:57;
    end;
    assume
A4: x=q;
    LE q,q,P by A1,A2,JORDAN6:56;
    then x in {p: LE q,p,P & LE p,q,P} by A4;
    hence thesis by A3,Def1;
  end;
  hence thesis by TARSKI:def 1;
end;

theorem
  for P being compact non empty Subset of TOP-REAL 2, q1,q2 being Point
  of TOP-REAL 2 st P is being_simple_closed_curve & q1<>W-min(P) & q2<>W-min(P)
  holds not W-min(P) in Segment(q1,q2,P)
proof
  let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL
  2;
  assume that
A1: P is being_simple_closed_curve and
A2: q1<>W-min(P) and
A3: q2<>W-min(P);
A4: Segment(q1,q2,P)={p: LE q1,p,P & LE p,q2,P} by A3,Def1;
  now
A5: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:def 8;
    assume W-min(P) in Segment(q1,q2,P);
    then consider p such that
A6: p=W-min(P) and
A7: LE q1,p,P and
    LE p,q2,P by A4;
    LE q1,p,Upper_Arc(P),W-min(P),E-max(P) by A6,A7,JORDAN6:def 10;
    hence contradiction by A2,A6,A5,JORDAN6:54;
  end;
  hence thesis;
end;

theorem Th10:
  for P being compact non empty Subset of TOP-REAL 2, q1,q2,q3
  being Point of TOP-REAL 2 st P is being_simple_closed_curve & LE q1,q2,P & LE
q2,q3,P & not(q1=q2 & q1=W-min(P)) & not(q2=q3 & q2=W-min(P)) holds Segment(q1,
  q2,P)/\ Segment(q2,q3,P)={q2}
proof
  let P be compact non empty Subset of TOP-REAL 2, q1,q2,q3 be Point of
  TOP-REAL 2;
  assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q3,P and
A4: not(q1=q2 & q1=W-min(P)) and
A5: not(q2=q3 & q2=W-min(P));
A6: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:def 8;
  thus Segment(q1,q2,P)/\ Segment(q2,q3,P) c= {q2}
  proof
    let x be set;
    assume
A7: x in Segment(q1,q2,P)/\ Segment(q2,q3,P);
    then
A8: x in Segment(q2,q3,P) by XBOOLE_0:def 4;
A9: x in Segment(q1,q2,P) by A7,XBOOLE_0:def 4;
    now
      per cases;
      case
        q3<>W-min(P);
        then x in {p: LE q2,p,P & LE p,q3,P} by A8,Def1;
        then
A10:    ex p st p=x & LE q2,p,P & LE p,q3,P;
        per cases;
        suppose
          q2<>W-min(P);
          then x in {p2: LE q1,p2,P & LE p2,q2,P} by A9,Def1;
          then ex p2 st p2=x & LE q1,p2,P & LE p2,q2,P;
          hence x=q2 by A1,A10,JORDAN6:57;
        end;
        suppose
A11:      q2=W-min(P);
          then LE q1,q2,Upper_Arc(P),W-min(P),E-max(P) by A2,JORDAN6:def 10;
          hence x=q2 by A4,A6,A11,JORDAN6:54;
        end;
      end;
      case
A12:    q3=W-min(P);
        then x in {p1: LE q2,p1,P or q2 in P & p1=W-min(P)} by A8,Def1;
        then consider p1 such that
A13:    p1=x and
A14:    LE q2,p1,P or q2 in P & p1=W-min(P);
        p1 in {p: LE q1,p,P & LE p,q2,P} by A5,A9,A12,A13,Def1;
        then ex p st p=p1 & LE q1,p,P & LE p,q2,P;
        hence x=q2 by A1,A3,A12,A13,A14,JORDAN6:57;
      end;
    end;
    hence thesis by TARSKI:def 1;
  end;
  let x be set;
  assume x in {q2};
  then x=q2 by TARSKI:def 1;
  then x in Segment(q1,q2,P) & x in Segment(q2,q3,P) by A1,A2,A3,Th6;
  hence thesis by XBOOLE_0:def 4;
end;

theorem Th11:
  for P being compact non empty Subset of TOP-REAL 2, q1,q2 being
  Point of TOP-REAL 2 st P is being_simple_closed_curve & LE q1,q2,P & q1 <>
  W-min P & q2 <> W-min P holds Segment(q1,q2,P)/\ Segment(q2,W-min P,P)={q2}
proof
  let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL
  2;
  set q3 = W-min P;
  assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: q1<>q3 and
A4: not q2=W-min(P);
  thus Segment(q1,q2,P)/\ Segment(q2,W-min P,P) c= {q2}
  proof
    let x be set;
    assume
A5: x in Segment(q1,q2,P)/\ Segment(q2,q3,P);
    then x in Segment(q2,q3,P) by XBOOLE_0:def 4;
    then x in {p1: LE q2,p1,P or q2 in P & p1=W-min P} by Def1;
    then consider p1 such that
A6: p1=x and
A7: LE q2,p1,P or q2 in P & p1=W-min P;
    x in Segment(q1,q2,P) by A5,XBOOLE_0:def 4;
    then p1 in {p: LE q1,p,P & LE p,q2,P} by A4,A6,Def1;
    then
A8: ex p st p=p1 & LE q1,p,P & LE p,q2,P;
    per cases by A7;
    suppose
      LE q2,p1,P;
      then x=q2 by A1,A6,A8,JORDAN6:57;
      hence thesis by TARSKI:def 1;
    end;
    suppose
      q2 in P & p1=W-min(P);
      hence thesis by A1,A3,A8,Th2;
    end;
  end;
  let x be set;
  assume x in {q2};
  then
A9: x=q2 by TARSKI:def 1;
  q2 in P by A1,A2,Th5;
  then
A10: x in Segment(q2,q3,P) by A1,A9,Th7;
  x in Segment(q1,q2,P) by A1,A2,A9,Th6;
  hence thesis by A10,XBOOLE_0:def 4;
end;

theorem Th12:
  for P being compact non empty Subset of TOP-REAL 2, q1,q2 being
  Point of TOP-REAL 2 st P is being_simple_closed_curve & LE q1,q2,P & q1<>q2 &
  q1<>W-min(P) holds Segment(q2,W-min(P),P)/\ Segment(W-min(P),q1,P)={W-min(P)}
proof
  let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL
  2;
  assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: q1<>q2 and
A4: q1<>W-min(P);
  thus Segment(q2,W-min(P),P)/\ Segment(W-min(P),q1,P) c= {W-min(P)}
  proof
    let x be set;
    assume
A5: x in Segment(q2,W-min(P),P)/\ Segment(W-min(P),q1,P);
    then x in Segment(q2,W-min(P),P) by XBOOLE_0:def 4;
    then x in {p1: LE q2,p1,P or q2 in P & p1=W-min(P)} by Def1;
    then consider p1 such that
A6: p1=x and
A7: LE q2,p1,P or q2 in P & p1=W-min(P);
A8: x in Segment(W-min(P),q1,P) by A5,XBOOLE_0:def 4;
    now
      per cases by A7;
      case
A9:     LE q2,p1,P;
        x in {p: LE W-min(P),p,P & LE p,q1,P} by A4,A8,Def1;
        then ex p2 st p2=x & LE W-min(P),p2,P & LE p2,q1,P;
        then LE q2,q1,P by A1,A6,A9,JORDAN6:58;
        hence contradiction by A1,A2,A3,JORDAN6:57;
      end;
      case
        q2 in P & p1=W-min(P);
        hence x=W-min(P) by A6;
      end;
    end;
    hence thesis by TARSKI:def 1;
  end;
  let x be set;
  assume x in {W-min(P)};
  then
A10: x=W-min(P) by TARSKI:def 1;
  q2 in P by A1,A2,Th5;
  then x in {p1: LE q2,p1,P or q2 in P & p1=W-min(P)} by A10;
  then
A11: x in Segment(q2,W-min(P),P) by Def1;
  q1 in P by A1,A2,Th5;
  then LE W-min(P),q1,P by A1,Th3;
  then x in Segment(W-min(P),q1,P) by A1,A10,Th6;
  hence thesis by A11,XBOOLE_0:def 4;
end;

theorem Th13:
  for P being compact non empty Subset of TOP-REAL 2, q1,q2,q3,q4
  being Point of TOP-REAL 2 st P is being_simple_closed_curve & LE q1,q2,P & LE
q2,q3,P & LE q3,q4,P & q1<>q2 & q2<>q3 holds Segment(q1,q2,P) misses Segment(q3
  ,q4,P)
proof
  let P be compact non empty Subset of TOP-REAL 2, q1,q2,q3,q4 be Point of
  TOP-REAL 2;
  assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q3,P and
A4: LE q3,q4,P and
A5: q1<>q2 and
A6: q2<>q3;
  set x = the Element of Segment(q1,q2,P)/\ Segment(q3,q4,P);
  assume
A7: Segment(q1,q2,P)/\ Segment(q3,q4,P)<>{};
  then
A8: x in Segment(q1,q2,P) by XBOOLE_0:def 4;
A9: x in Segment(q3,q4,P) by A7,XBOOLE_0:def 4;
  per cases;
  suppose
    q4=W-min(P);
    then q3=W-min(P) by A1,A4,Th2;
    hence contradiction by A1,A3,A6,Th2;
  end;
  suppose
A10: q4<>W-min(P);
    q2<>W-min(P) by A1,A2,A5,Th2;
    then x in {p2: LE q1,p2,P & LE p2,q2,P} by A8,Def1;
    then
A11: ex p2 st p2=x & LE q1,p2,P & LE p2,q2,P;
    x in {p1: LE q3,p1,P & LE p1,q4,P} by A9,A10,Def1;
    then ex p1 st p1=x & LE q3,p1,P & LE p1,q4,P;
    then LE q3,q2,P by A1,A11,JORDAN6:58;
    hence contradiction by A1,A3,A6,JORDAN6:57;
  end;
end;

theorem Th14:
  for P being compact non empty Subset of TOP-REAL 2, q1,q2,q3
  being Point of TOP-REAL 2 st P is being_simple_closed_curve & LE q1,q2,P & LE
q2,q3,P & q1<>W-min P & q2<>q3 holds Segment(q1,q2,P) misses Segment(q3,W-min P
  ,P)
proof
  let P be compact non empty Subset of TOP-REAL 2, q1,q2,q3 be Point of
  TOP-REAL 2;
  assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q3,P and
A4: q1<>W-min P and
A5: q2<>q3;
  set x = the Element of Segment(q1,q2,P)/\ Segment(q3,W-min P,P);
  assume
A6: Segment(q1,q2,P)/\ Segment(q3,W-min P,P)<>{};
  then
A7: x in Segment(q1,q2,P) by XBOOLE_0:def 4;
  x in Segment(q3,W-min P,P) by A6,XBOOLE_0:def 4;
  then x in {p1: LE q3,p1,P or q3 in P & p1=W-min P} by Def1;
  then
A8: ex p1 st p1=x &( LE q3,p1,P or q3 in P & p1=W-min P);
  q2 <> W-min P by A1,A2,A4,Th2;
  then x in {p: LE q1,p,P & LE p,q2,P} by A7,Def1;
  then ex p3 st p3 = x & LE q1,p3,P & LE p3,q2,P;
  then LE q3,q2,P by A1,A4,A8,Th2,JORDAN6:58;
  hence contradiction by A1,A3,A5,JORDAN6:57;
end;

begin :: A function to divide the simple closed curve

reserve n for Element of NAT;

theorem Th15:
  for P being non empty Subset of TOP-REAL n, f being Function of
I[01], (TOP-REAL n)|P st f is being_homeomorphism ex g being Function of I[01],
  TOP-REAL n st f=g & g is continuous & g is one-to-one
proof
  let P be non empty Subset of TOP-REAL n, f be Function of I[01], (TOP-REAL n
  )|P;
A1: [#]((TOP-REAL n)|P)= P by PRE_TOPC:def 5;
  the carrier of (TOP-REAL n)|P = [#]((TOP-REAL n)|P) .=P by PRE_TOPC:def 5;
  then reconsider g1=f as Function of I[01],TOP-REAL n by FUNCT_2:7;
  assume
A2: f is being_homeomorphism;
  then
A3: f is one-to-one by TOPS_2:def 5;
A4: [#]((TOP-REAL n)|P) <> {} & f is continuous by A2,TOPS_2:def 5;
A5: for P2 being Subset of TOP-REAL n st P2 is open holds g1"P2 is open
  proof
    let P2 be Subset of TOP-REAL n;
    reconsider B1=P2 /\ P as Subset of (TOP-REAL n)|P by A1,XBOOLE_1:17;
    f"(rng f) c= f"P by A1,RELAT_1:143;
    then
A6: dom f c= f"P by RELAT_1:134;
    assume P2 is open;
    then B1 is open by A1,TOPS_2:24;
    then
A7: f"B1 is open by A4,TOPS_2:43;
    f"P c= dom f by RELAT_1:132;
    then f"B1 = f"P2 /\ f"P & f"P=dom f by A6,FUNCT_1:68,XBOOLE_0:def 10;
    hence thesis by A7,RELAT_1:132,XBOOLE_1:28;
  end;
  [#]TOP-REAL n <> {};
  then g1 is continuous by A5,TOPS_2:43;
  hence thesis by A3;
end;

theorem Th16:
  for P being non empty Subset of TOP-REAL n, g being Function of
  I[01], (TOP-REAL n) st g is continuous one-to-one & rng g = P ex f being
  Function of I[01],(TOP-REAL n)|P st f=g & f is being_homeomorphism
proof
  let P be non empty Subset of TOP-REAL n, g be Function of I[01], TOP-REAL n;
  assume that
A1: g is continuous one-to-one and
A2: rng g = P;
  the carrier of (TOP-REAL n)|P = [#]((TOP-REAL n)|P);
  then
A3: the carrier of (TOP-REAL n)|P = P by PRE_TOPC:def 5;
  then reconsider f=g as Function of I[01],(TOP-REAL n)|P by A2,FUNCT_2:6;
  take f;
  thus f = g;
A4: [#]((TOP-REAL n)|P)= P by PRE_TOPC:def 5;
A5: dom f = the carrier of I[01] by FUNCT_2:def 1
    .= [#]I[01];
A6: [#]TOP-REAL n<>{};
  for P2 being Subset of (TOP-REAL n)|P st P2 is open holds f"P2 is open
  proof
    let P2 be Subset of (TOP-REAL n)|P;
    assume P2 is open;
    then consider C being Subset of TOP-REAL n such that
A7: C is open and
A8: C /\ [#]((TOP-REAL n)|P) = P2 by TOPS_2:24;
    g"P = [#]I[01] by A3,A5,RELSET_1:22;
    then f"P2 = f"C /\ [#]I[01] by A4,A8,FUNCT_1:68
      .= f"C by XBOOLE_1:28;
    hence thesis by A1,A6,A7,TOPS_2:43;
  end;
  then
A9: f is continuous by A4,TOPS_2:43;
  rng f = [#]((TOP-REAL n)|P) by A2,PRE_TOPC:def 5;
  hence thesis by A1,A5,A9,COMPTS_1:17;
end;

Lm4: now
  let h2 be Element of NAT;
  h2<h2+1 by NAT_1:13;
  then
A1: h2-1<h2+1-1 by XREAL_1:9;
  then h2-1-1<h2-1 by XREAL_1:9;
  hence h2-1-1<h2 by A1,XXREAL_0:2;
end;

Lm5: 0 in [.0,1.] by XXREAL_1:1;

Lm6: 1 in [.0,1.] by XXREAL_1:1;

theorem Th17:
  for A being Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL
  2 st A is_an_arc_of p1,p2 ex g being Function of I[01], TOP-REAL 2 st g is
  continuous one-to-one & rng g = A & g.0 = p1 & g.1 = p2
proof
  let A be Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2;
  assume
A1: A is_an_arc_of p1,p2;
  then reconsider A9 = A as non empty Subset of TOP-REAL 2 by TOPREAL1:1;
  consider f being Function of I[01], (TOP-REAL 2)|A9 such that
A2: f is being_homeomorphism and
A3: f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 1;
  consider g being Function of I[01], TOP-REAL 2 such that
A4: f=g and
A5: g is continuous one-to-one by A2,Th15;
  take g;
  thus g is continuous one-to-one by A5;
  rng f=[#]((TOP-REAL 2)|A9) by A2,TOPS_2:def 5;
  hence rng g = A by A4,PRE_TOPC:def 5;
  thus thesis by A3,A4;
end;

theorem Th18:
  for P being non empty Subset of TOP-REAL 2, p1, p2, q1, q2 being
  Point of TOP-REAL 2, g being Function of I[01], TOP-REAL 2, s1, s2 being Real
st P is_an_arc_of p1,p2 & g is continuous one-to-one & rng g = P & g.0 = p1 & g
.1 = p2 & g.s1 = q1 & 0 <= s1 & s1 <= 1 & g.s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <=
  s2 holds LE q1,q2,P,p1,p2
proof
  let P be non empty Subset of TOP-REAL 2, p1, p2, q1, q2 be Point of TOP-REAL
  2, g be Function of I[01], TOP-REAL 2, s1, s2 be Real such that
A1: P is_an_arc_of p1,p2 and
A2: g is continuous one-to-one & rng g = P;
  ex f being Function of I[01],(TOP-REAL 2)|P st f=g & f is
  being_homeomorphism by A2,Th16;
  hence thesis by A1,JORDAN5C:8;
end;

theorem Th19:
  for P being non empty Subset of TOP-REAL 2, p1, p2, q1, q2 being
  Point of TOP-REAL 2, g being Function of I[01], TOP-REAL 2, s1, s2 being Real
st g is continuous one-to-one & rng g = P & g.0 = p1 & g.1 = p2 & g.s1 = q1 & 0
<= s1 & s1 <= 1 & g.s2 = q2 & 0 <= s2 & s2 <= 1 & LE q1,q2,P,p1,p2 holds s1 <=
  s2
proof
  let P be non empty Subset of TOP-REAL 2, p1, p2, q1, q2 be Point of TOP-REAL
  2, g be Function of I[01], TOP-REAL 2, s1, s2 be Real;
  assume g is continuous one-to-one & rng g = P;
  then ex f being Function of I[01],(TOP-REAL 2)|P st f=g & f is
  being_homeomorphism by Th16;
  hence thesis by JORDAN5C:def 3;
end;

theorem :: Dividing simple closed curve into segments.
  for P being compact non empty Subset of TOP-REAL 2, e being Real st P
      is being_simple_closed_curve & e > 0
  ex h being FinSequence of the carrier of TOP-REAL 2
   st h.1=W-min(P) & h is one-to-one & 8<=len h & rng h c= P &(for i
being Element of NAT st 1<=i & i<len h holds LE h/.i,h/.(i+1),P) &(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),P) holds diameter(W)<e) & (for W being Subset of Euclid 2 st W=Segment(
h/.len h,h/.1,P) holds diameter(W)<e) & (for i being Element of NAT st 1<=i & i
+1<len h holds Segment(h/.i,h/.(i+1),P)/\ Segment(h/.(i+1),h/.(i+2),P)={h/.(i+1
)}) & Segment(h/.len h,h/.1,P)/\ Segment(h/.1,h/.2,P)={h/.1} & Segment(h/.(len
h-' 1),h/.len h,P)/\ Segment(h/.len h,h/.1,P)={h/.len h} & Segment(h/.(len h-'1
),h/.len h,P) misses Segment(h/.1,h/.2,P) &(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),P)
misses Segment(h/.j,h/.(j+1),P)) & for i being Element of NAT st 1 < i & i+1 <
  len h holds Segment(h/.len h,h/.1,P) misses Segment(h/.i,h/.(i+1),P)
proof
  let P be compact non empty Subset of TOP-REAL 2, e be Real;
  assume that
A1: P is being_simple_closed_curve and
A2: e > 0;
A3: Upper_Arc P is_an_arc_of W-min P, E-max P by A1,JORDAN6:def 8;
  then consider g1 being Function of I[01], TOP-REAL 2 such that
A4: g1 is continuous one-to-one and
A5: rng g1 = Upper_Arc P and
A6: g1.0 = W-min P and
A7: g1.1 = E-max P by Th17;
  consider h1 being FinSequence of REAL such that
A8: h1.1=0 and
A9: h1.len h1=1 and
A10: 5<=len h1 and
A11: rng h1 c= the carrier of I[01] and
A12: h1 is increasing and
A13: for i being Element of NAT,Q being Subset of I[01], W being Subset
of Euclid 2 st 1<=i & i<len h1 & Q=[.h1/.i,h1/.(i+1).] & W=g1.:Q holds diameter
  (W)<e by A2,A4,UNIFORM1:13;
  h1 is FinSequence of the carrier of I[01] by A11,FINSEQ_1:def 4;
  then reconsider h11=g1*h1 as FinSequence of the carrier of TOP-REAL 2 by
FINSEQ_2:32;
A14: 2<len h1 by A10,XXREAL_0:2;
  then
A15: 2 in dom h1 by FINSEQ_3:25;
A16: 1<=len h1 by A10,XXREAL_0:2;
  then
A17: 1 in dom h1 by FINSEQ_3:25;
A18: 1+1 in dom h1 by A14,FINSEQ_3:25;
  then
A19: h1.(1+1) in rng h1 by FUNCT_1:def 3;
A20: h11 is one-to-one by A4,A12;
A21: Lower_Arc P is_an_arc_of E-max P, W-min P by A1,JORDAN6:def 9;
  then consider g2 being Function of I[01], TOP-REAL 2 such that
A22: g2 is continuous one-to-one and
A23: rng g2 = Lower_Arc P and
A24: g2.0 = E-max P and
A25: g2.1 = W-min P by Th17;
  consider h2 being FinSequence of REAL such that
A26: h2.1=0 and
A27: h2.len h2=1 and
A28: 5<=len h2 and
A29: rng h2 c= the carrier of I[01] and
A30: h2 is increasing and
A31: for i being Element of NAT,Q being Subset of I[01], W being Subset
of Euclid 2 st 1<=i & i<len h2 & Q=[.h2/.i,h2/.(i+1).] & W=g2.:Q holds diameter
  (W)<e by A2,A22,UNIFORM1:13;
  h2 is FinSequence of the carrier of I[01] by A29,FINSEQ_1:def 4;
  then reconsider h21=g2*h2 as FinSequence of the carrier of TOP-REAL 2 by
FINSEQ_2:32;
A32: h21 is one-to-one by A22,A30;
A33: 1<=len h2 by A28,XXREAL_0:2;
  then
A34: len h2 in dom h2 by FINSEQ_3:25;
  then
A35: h21.len h2=W-min P by A25,A27,FUNCT_1:13;
  reconsider h0=h11^(mid(h21,2,len h21-' 1)) as FinSequence of the carrier of
  TOP-REAL 2;
A36: len h0=len h11+len (mid(h21,2,len h21 -'1)) by FINSEQ_1:22;
  set i = len h0-'1;
  take h0;
A37: rng h1 c= dom g1 by A11,FUNCT_2:def 1;
  then
A38: dom h1=dom h11 by RELAT_1:27;
  then
A39: len h1=len h11 by FINSEQ_3:29;
  then
A40: h0.2=h11.2 by A14,FINSEQ_1:64;
A41: h0.(1+1)=h11.(1+1) by A39,A14,FINSEQ_1:64;
  then
A42: h0.(1+1)=g1.(h1.(1+1)) by A18,FUNCT_1:13;
  set k=len h0-'len h11+2-'1;
  0+2<=len h0-'len h11 +2 by XREAL_1:6;
  then
A43: 2-'1<=len h0-'len h11 +2-'1 by NAT_D:42;
A44: 0 in dom g1 by Lm5,BORSUK_1:40,FUNCT_2:def 1;
A45: len h1 in dom h1 by A16,FINSEQ_3:25;
  dom g2=the carrier of I[01] by FUNCT_2:def 1;
  then
A46: dom h2=dom h21 by A29,RELAT_1:27;
  then
A47: len h2=len h21 by FINSEQ_3:29;
  then
A48: 2<=len h21 by A28,XXREAL_0:2;
  len h21<=len h21 +1 by NAT_1:12;
  then
A49: len h21 -1<=len h21 +1-1 by XREAL_1:9;
  then
A50: len h21-'1<=len h21 by A28,A47,XREAL_0:def 2;
  2<=len h21 by A28,A47,XXREAL_0:2;
  then
A51: 1+1-1<=len h21-1 by XREAL_1:9;
  then
A52: len h21-'1=len h21 -1 by XREAL_0:def 2;
  3<len h21 by A28,A47,XXREAL_0:2;
  then
A53: 2+1-1<len h21 -1 by XREAL_1:9;
  then
A54: 2<len h21 -'1 by A51,NAT_D:39;
  then
A55: len h21 -'1-'2=len h21 -'1-2 by XREAL_1:233;
A56: 1<=len h21-'1 by A51,XREAL_0:def 2;
  then
A57: len (mid(h21,2,len h21 -'1)) =(len h21-'1)-'2+1 by A48,A50,A54,
FINSEQ_6:118;
  3+2-2<=len h2 -2 by A28,XREAL_1:9;
  then
A58: 5+3<=len h1+(len h2 -2) by A10,XREAL_1:7;
  then
A59: len h0 > 1+1+1 by A39,A47,A36,A52,A55,A57,XXREAL_0:2;
  then
A60: len h0-'1 > 1+1 by Lm2;
  then
A61: 1<i by XXREAL_0:2;
A62: 3+2-2<=len h2 -2 by A28,XREAL_1:9;
  then
A63: 1<=len h2 -2 by XXREAL_0:2;
  then
A64: len h1+1<=len h0 by A39,A47,A36,A52,A55,A57,XREAL_1:7;
  then
A65: len h0>len h1 by NAT_1:13;
  then
A66: 1<len h0 by A16,XXREAL_0:2;
  then
A67: 1 in dom h0 by FINSEQ_3:25;
  then
A68: h0/.1 = h0.1 by PARTFUN1:def 6;
A69: dom g1=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
  then
A70: 1 in dom (g1*h1) by A8,A17,Lm5,FUNCT_1:11;
  then
A71: h11.1=W-min P by A6,A8,FUNCT_1:12;
  hence
A72: h0.1=W-min P by A70,FINSEQ_1:def 7;
  then
A73: h0/.1=W-min(P) by A67,PARTFUN1:def 6;
A74: len h0 in dom h0 by A66,FINSEQ_3:25;
  then
A75: h0/.len h0=h0.len h0 by PARTFUN1:def 6;
A76: 1 in dom h2 by A33,FINSEQ_3:25;
  then
A77: h21.1=E-max P by A24,A26,FUNCT_1:13;
  thus
A78: h0 is one-to-one
  proof
    let x,y be set;
    assume that
A79: x in dom h0 and
A80: y in dom h0 and
A81: h0.x=h0.y;
    reconsider nx=x,ny=y as Element of NAT by A79,A80;
A82: 1<=nx by A79,FINSEQ_3:25;
A83: nx<=len h0 by A79,FINSEQ_3:25;
A84: 1<=ny by A80,FINSEQ_3:25;
A85: ny<=len h0 by A80,FINSEQ_3:25;
    per cases;
    suppose
      nx<=len h1;
      then
A86:  nx in dom h1 by A82,FINSEQ_3:25;
      then
A87:  h1.nx in rng h1 by FUNCT_1:def 3;
A88:  h0.nx=h11.nx by A38,A86,FINSEQ_1:def 7
        .=g1.(h1.nx) by A38,A86,FUNCT_1:12;
      then
A89:  h0.nx in Upper_Arc(P) by A5,A37,A87,FUNCT_1:def 3;
      per cases;
      suppose
        ny<=len h1;
        then
A90:    ny in dom h1 by A84,FINSEQ_3:25;
        then
A91:    h1.ny in rng h1 by FUNCT_1:def 3;
        h0.ny=h11.ny by A38,A90,FINSEQ_1:def 7
          .=g1.(h1.ny) by A90,FUNCT_1:13;
        then h1.nx=h1.ny by A4,A37,A81,A87,A88,A91,FUNCT_1:def 4;
        hence thesis by A12,A86,A90,FUNCT_1:def 4;
      end;
      suppose
A92:    ny>len h1;
A93:    0+2<=ny-'len h11 +2 by XREAL_1:6;
        then
A94:    1<=(ny-'len h11 +2-'1) by Lm1,NAT_D:42;
        len h1 +1<=ny by A92,NAT_1:13;
        then
A95:    len h1 +1-len h1<=ny-len h1 by XREAL_1:9;
        then 1<=ny-'len h11 by A39,A92,XREAL_1:233;
        then 1+1<=ny-'len h11+1+1-1 by XREAL_1:6;
        then
A96:    2<=ny-'len h11+2-'1 by A93,Lm1,NAT_D:39,42;
A97:    ny-len h11=ny-'len h11 by A39,A92,XREAL_1:233;
        ny-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A85,
XREAL_1:9;
        then
A98:    ny-'len h11+2<=len h2-2+2 by A39,A97,XREAL_1:6;
        then (ny-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
        then
A99:    (ny-'len h11 +2-'1) in dom h21 by A94,FINSEQ_3:25;
        ny-'len h11+2-1<=len h2-1 by A98,XREAL_1:9;
        then
A100:   ny-'len h11+2-'1<=len h2-1 by A93,Lm1,NAT_D:39,42;
A101:   ny<=len h11 + len (mid(h21,2,len h21 -'1)) by A85,FINSEQ_1:22;
        then
A102:   ny-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by XREAL_1:9
;
        len h11+1<=ny by A39,A92,NAT_1:13;
        then
A103:   h0.ny=(mid(h21,2,len h21 -'1)).(ny -len h11) by A101,FINSEQ_1:23;
        then
A104:   h0.ny=h21.(ny-'len h11 +2-'1) by A39,A48,A56,A50,A54,A97,A102,A95,
FINSEQ_6:118;
        then h0.ny in rng h21 by A99,FUNCT_1:def 3;
        then h0.ny in rng g2 by FUNCT_1:14;
        then h0.nx in Upper_Arc(P)/\ Lower_Arc(P) by A23,A81,A89,XBOOLE_0:def 4
;
        then
A105:   h0.nx in {W-min(P),E-max(P)} by A1,JORDAN6:50;
        per cases by A105,TARSKI:def 2;
        suppose
          h0.nx=W-min(P);
          then h21.(ny-'len h11 +2-'1)=W-min(P) by A39,A48,A56,A50,A54,A81,A103
,A97,A102,A95,FINSEQ_6:118;
          then len h21=(ny-'len h11 +2-'1) by A46,A47,A34,A35,A32,A99,
FUNCT_1:def 4;
          then len h21+1<=len h21-1+1 by A47,A100,XREAL_1:6;
          then len h21+1-len h21<=len h21 -len h21 by XREAL_1:9;
          then len h21+1-len h21<=0;
          hence thesis;
        end;
        suppose
          h0.nx=E-max(P);
          then 1=(ny-'len h11 +2-'1) by A46,A76,A77,A32,A81,A104,A99,
FUNCT_1:def 4;
          hence thesis by A96;
        end;
      end;
    end;
    suppose
A106: nx>len h1;
      then len h1 +1<=nx by NAT_1:13;
      then
A107: len h1 +1-len h1<=nx-len h1 by XREAL_1:9;
      then 1<=nx-'len h11 by A39,A106,XREAL_1:233;
      then
A108: 1+1<=nx-'len h11+1+1-1 by XREAL_1:6;
A109: nx<=len h11 + len (mid(h21,2,len h21 -'1)) by A83,FINSEQ_1:22;
      then
A110: nx-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by XREAL_1:9;
A111: nx-len h11=nx-'len h11 by A39,A106,XREAL_1:233;
      nx-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A83,
XREAL_1:9;
      then
A112: nx-'len h11+2<=len h2-2+2 by A39,A111,XREAL_1:6;
      then
A113: nx-'len h11+2-1<=len h2-1 by XREAL_1:9;
A114: (nx-'len h11 +2-'1)<=len h21 by A47,A112,NAT_D:44;
A115: 0+2<=nx-'len h11 +2 by XREAL_1:6;
      then 1<=(nx-'len h11 +2-'1) by Lm1,NAT_D:42;
      then
A116: (nx-'len h11 +2-'1) in dom h21 by A114,FINSEQ_3:25;
      len h11+1<=nx by A39,A106,NAT_1:13;
      then
A117: h0.nx=(mid(h21,2,len h21 -'1)).(nx -len h11) by A109,FINSEQ_1:23;
      then
A118: h0.nx=h21.(nx-'len h11 +2-'1) by A39,A48,A56,A50,A54,A111,A110,A107,
FINSEQ_6:118;
      then h0.nx in rng h21 by A116,FUNCT_1:def 3;
      then
A119: h0.nx in Lower_Arc(P) by A23,FUNCT_1:14;
      per cases;
      suppose
        ny<=len h1;
        then
A120:   ny in dom h1 by A84,FINSEQ_3:25;
        then
A121:   h1.ny in rng h1 by FUNCT_1:def 3;
        h0.ny=h11.ny by A38,A120,FINSEQ_1:def 7
          .=g1.(h1.ny) by A38,A120,FUNCT_1:12;
        then h0.ny in rng g1 by A37,A121,FUNCT_1:def 3;
        then h0.ny in Upper_Arc(P)/\ Lower_Arc(P) by A5,A81,A119,XBOOLE_0:def 4
;
        then
A122:   h0.ny in {W-min(P),E-max(P)} by A1,JORDAN6:50;
A123:   nx-'len h11+2-'1<=len h2-1 by A115,A113,Lm1,NAT_D:39,42;
A124:   2<=nx-'len h11+2-'1 by A108,A115,Lm1,NAT_D:39,42;
        per cases by A122,TARSKI:def 2;
        suppose
          h0.ny=W-min(P);
          then len h21=(nx-'len h11 +2-'1) by A46,A47,A34,A35,A32,A81,A118,A116
,FUNCT_1:def 4;
          then len h21+1<=len h21-1+1 by A47,A123,XREAL_1:6;
          then len h21+1-len h21<=len h21 -len h21 by XREAL_1:9;
          then len h21+1-len h21<=0;
          hence thesis;
        end;
        suppose
          h0.ny=E-max(P);
          then h21.(nx-'len h11 +2-'1)=E-max(P) by A39,A48,A56,A50,A54,A81,A117
,A111,A110,A107,FINSEQ_6:118;
          then 1=(nx-'len h11 +2-'1) by A46,A76,A77,A32,A116,FUNCT_1:def 4;
          hence thesis by A124;
        end;
      end;
      suppose
A125:   ny>len h1;
        then
A126:   ny-len h11=ny-'len h11 by A39,XREAL_1:233;
        len h1 +1<=ny by A125,NAT_1:13;
        then
A127:   h0.ny=(mid(h21,2,len h21 -'1)).(ny -len h11) & len h1 +1-len h1
        <=ny-len h1 by A39,A36,A85,FINSEQ_1:23,XREAL_1:9;
        0+2<=ny-'len h11 +2 by XREAL_1:6;
        then
A128:   1<=(ny-'len h11 +2-'1) by Lm1,NAT_D:42;
        ny-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A85,
XREAL_1:9;
        then
A129:   h0.ny=h21.(ny-'len h11 +2-'1) by A39,A48,A56,A50,A54,A126,A127,
FINSEQ_6:118;
        ny-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A85,
XREAL_1:9;
        then ny-'len h11+2<=len h2-2+2 by A39,A126,XREAL_1:6;
        then (ny-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
        then (ny-'len h11 +2-'1) in dom h21 by A128,FINSEQ_3:25;
        then nx-'len h1+2-'1=ny-'len h1+2-'1 by A39,A32,A81,A118,A116,A129,
FUNCT_1:def 4;
        then nx-'len h1+2-1=ny-'len h1+2-'1 by A39,A115,Lm1,NAT_D:39,42;
        then nx-'len h1+(2-1)=ny-'len h1+2-1 by A39,A128,NAT_D:39;
        then len h1+nx-len h1=len h1+(ny-len h1) by A39,A111,A126,XCMPLX_1:29;
        hence thesis;
      end;
    end;
  end;
  then
A130: h0/.len h0 <> W-min P by A16,A72,A65,A74,A75,A67,FUNCT_1:def 4;
A131: dom g2 = [.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
  thus 8<=len h0 by A38,A47,A36,A52,A55,A57,A58,FINSEQ_3:29;
  rng (mid(h21,2,len h21 -'1)) c= rng h21 & rng (g2*h2) c= rng g2 by
FINSEQ_6:119,RELAT_1:26;
  then rng (g1*h1) c= rng g1 & rng (mid(h21,2,len h21 -'1)) c= rng g2 by
RELAT_1:26,XBOOLE_1:1;
  then rng h11 \/ rng (mid(h21,2,len h21 -'1)) c= Upper_Arc(P) \/ Lower_Arc(P
  ) by A5,A23,XBOOLE_1:13;
  then rng h0 c=Upper_Arc(P) \/ Lower_Arc(P) by FINSEQ_1:31;
  hence rng h0 c= P by A1,JORDAN6:def 9;
A132: dom g1 =[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
  thus for i being Element of NAT st 1<=i & i<len h0 holds LE h0/.i,h0/.(i+1),
  P
  proof
    let i be Element of NAT;
    assume that
A133: 1<=i and
A134: i<len h0;
A135: i+1<=len h0 by A134,NAT_1:13;
A136: i<i+1 by NAT_1:13;
A137: 1<i+1 by A133,NAT_1:13;
    per cases;
    suppose
A138: i<len h1;
      then
A139: i+1<=len h1 by NAT_1:13;
      then
A140: i+1 in dom h1 by A137,FINSEQ_3:25;
      then
A141: h1.(i+1) in rng h1 by FUNCT_1:def 3;
      then
A142: h1.(i+1)<=1 by A11,BORSUK_1:40,XXREAL_1:1;
      h0.(i+1)=h11.(i+1) by A39,A137,A139,FINSEQ_1:64;
      then
A143: h0.(i+1)=g1.(h1.(i+1)) by A140,FUNCT_1:13;
      then
A144: h0.(i+1) in Upper_Arc(P) by A5,A132,A11,A141,BORSUK_1:40,FUNCT_1:def 3;
      i in dom h0 by A133,A134,FINSEQ_3:25;
      then
A145: h0/.i=h0.i by PARTFUN1:def 6;
A146: i in dom h1 by A133,A138,FINSEQ_3:25;
      then
A147: h1.i in rng h1 by FUNCT_1:def 3;
      then
A148: 0<=h1.i & h1.i<=1 by A11,BORSUK_1:40,XXREAL_1:1;
A149: g1.(h1.i) in rng g1 by A132,A11,A147,BORSUK_1:40,FUNCT_1:def 3;
      h0.i=h11.i by A39,A133,A138,FINSEQ_1:64;
      then
A150: h0.i=g1.(h1.i) by A146,FUNCT_1:13;
      i+1 in dom h0 by A135,A137,FINSEQ_3:25;
      then
A151: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
      h1.i<h1.(i+1) by A12,A136,A146,A140,SEQM_3:def 1;
      then LE h0/.i,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A3,A4,A5,A6,A7
,A150,A148,A143,A142,A145,A151,Th18;
      hence thesis by A5,A150,A145,A151,A149,A144,JORDAN6:def 10;
    end;
    suppose
A152: i>=len h1;
      per cases by A152,XXREAL_0:1;
      suppose
A153:   i>len h1;
        then len h11+1<=i by A39,NAT_1:13;
        then
A154:   h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A36,A134,FINSEQ_1:23;
A155:   i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A135
,XREAL_1:9;
        i+1>len h11 by A39,A153,NAT_1:13;
        then
A156:   i+1-len h11=i+1-'len h11 by XREAL_1:233;
A157:   len h1 +1<=i by A153,NAT_1:13;
        then
A158:   len h1 +1-len h1<=i-len h1 by XREAL_1:9;
A159:   i-len h11=i-'len h11 by A39,A153,XREAL_1:233;
A160:   len h1 +1<=i+1 by A157,NAT_1:13;
        then
A161:   len h1 +1-len h1<=i+1-len h1 by XREAL_1:9;
        then
A162:   1<i+1-'len h11+(2-1) by A39,A156,NAT_1:13;
        then
A163:   0<i+1-'len h11+2-1;
        h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A39,A36,A135,A160,
FINSEQ_1:23;
        then
A164:   h0.(i+1)=h21.(i+1-'len h11 +2-'1) by A39,A48,A56,A50,A54,A156,A155,A161
,FINSEQ_6:118;
        set j=i-'len h11+2-'1;
        len h2<len h2+1 by NAT_1:13;
        then
A165:   len h2-1<len h2+1-1 by XREAL_1:9;
A166:   0+2<=i-'len h11 +2 by XREAL_1:6;
        then
A167:   1<=(i-'len h11 +2-'1) by Lm1,NAT_D:42;
        then
A168:   1<j+1 by NAT_1:13;
        i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A134,
XREAL_1:9;
        then
A169:   i-'len h11+2<=len h2-2+2 by A39,A159,XREAL_1:6;
        then (i-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
        then
A170:   j in dom h2 by A46,A167,FINSEQ_3:25;
        i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A134,
XREAL_1:9;
        then h0.i=h21.(i-'len h11 +2-'1) by A39,A48,A56,A50,A54,A154,A159,A158,
FINSEQ_6:118;
        then
A171:   h0.i=g2.(h2.j) by A170,FUNCT_1:13;
A172:   h2.j in rng h2 by A170,FUNCT_1:def 3;
        then
A173:   h0.i in Lower_Arc(P) by A23,A131,A29,A171,BORSUK_1:40,FUNCT_1:def 3;
        i+1 in dom h0 by A135,A137,FINSEQ_3:25;
        then
A174:   h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
        j+1=i-'len h11+1+1-1+1 by A166,Lm1,NAT_D:39,42
          .=i-'len h11+2;
        then
A175:   j+1 in dom h2 by A169,A168,FINSEQ_3:25;
        then
A176:   h2.(j+1) in rng h2 by FUNCT_1:def 3;
        then
A177:   h2.(j+1)<=1 by A29,BORSUK_1:40,XXREAL_1:1;
A178:   j+1=i-len h11+2-1+1 by A159,A166,Lm1,NAT_D:39,42
          .=i+1-'len h11+2-'1 by A156,A163,XREAL_0:def 2;
        then
A179:   h0.(i+1)=g2.(h2.(j+1)) by A164,A175,FUNCT_1:13;
        then
A180:   h0.(i+1) in Lower_Arc(P) by A23,A131,A29,A176,BORSUK_1:40,FUNCT_1:def 3
;
A181:   i+1-'len h11+2-1=i+1-'len h11+2-'1 by A162,XREAL_0:def 2;
        i+1-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A135,
XREAL_1:9;
        then
A182:   i+1-'len h11+2<=len h2-2+2 by A39,A156,XREAL_1:6;
        then i+1-'len h11+2-1<=len h2-1 by XREAL_1:9;
        then i+1-'len h11+2-'1<len h2 by A181,A165,XXREAL_0:2;
        then
A183:   i+1-'len h11+2-'1 in dom h2 by A178,A168,FINSEQ_3:25;
A184:   now
          assume h0/.(i+1)=W-min(P);
          then len h21=(i+1-'len h11 +2-'1) by A46,A47,A34,A35,A32,A164,A174
,A183,FUNCT_1:def 4;
          then len h21+1-len h21<=len h21 -len h21 by A47,A181,A182,XREAL_1:9;
          then len h21+1-len h21<=0;
          hence contradiction;
        end;
        j<j+1 by NAT_1:13;
        then
A185:   h2.j<h2.(j+1) by A30,A170,A175,SEQM_3:def 1;
        i in dom h0 by A133,A134,FINSEQ_3:25;
        then
A186:   h0/.i=h0.i by PARTFUN1:def 6;
        0<=h2.j & h2.j<=1 by A29,A172,BORSUK_1:40,XXREAL_1:1;
        then LE h0/.i,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23
,A24,A25,A171,A179,A177,A185,A186,A174,Th18;
        hence thesis by A186,A174,A173,A180,A184,JORDAN6:def 10;
      end;
      suppose
A187:   i=len h1;
        then h0.i=h11.i & i in dom h1 by A39,A133,FINSEQ_1:64,FINSEQ_3:25;
        then
A188:   h0.i=E-max(P) by A7,A9,A187,FUNCT_1:13;
        i in dom h0 by A133,A134,FINSEQ_3:25;
        then h0/.i=E-max(P) by A188,PARTFUN1:def 6;
        then
A189:   h0/.i in Upper_Arc(P) by A1,Th1;
        i+1 in dom h0 by A135,A137,FINSEQ_3:25;
        then
A190:   h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
        set j=i-'len h11+2-'1;
        len h11-'len h11= len h11-len h11 by XREAL_1:233
          .=0;
        then
A191:   j=2-1 by A39,A187,XREAL_1:233;
        then j+1<=len h2 by A28,XXREAL_0:2;
        then
A192:   j+1 in dom h2 by A191,FINSEQ_3:25;
        then
A193:   h2.(j+1) in rng h2 by FUNCT_1:def 3;
        2<=len h21 by A28,A47,XXREAL_0:2;
        then
A194:   2 in dom h21 by FINSEQ_3:25;
A195:   i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A135
,XREAL_1:9;
A196:   i+1-'len h11+2-'1=1+2-'1 by A39,A187,NAT_D:34
          .=2 by NAT_D:34;
        h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) & i+1-len h11=i
        +1-'len h11 by A39,A36,A135,A136,A187,FINSEQ_1:23,XREAL_1:233;
        then
A197:   h0.(i+1)=h21.(i+1-'len h11 +2-'1) by A39,A48,A56,A50,A54,A187,A195,
FINSEQ_6:118;
        then h0.(i+1)=g2.(h2.(j+1)) by A191,A196,A192,FUNCT_1:13;
        then
A198:   h0.(i+1) in Lower_Arc(P) by A23,A131,A29,A193,BORSUK_1:40,FUNCT_1:def 3
;
        len h21 <> i+1-'len h11 +2-'1 by A28,A47,A196;
        then h0/.(i+1) <> W-min P by A46,A47,A34,A35,A32,A197,A196,A190,A194,
FUNCT_1:def 4;
        hence thesis by A189,A190,A198,JORDAN6:def 10;
      end;
    end;
  end;
A199: i<len h0 by A66,JORDAN5B:1;
  then
A200: i+1<=len h0 by NAT_1:13;
A201: 1+1<=len h0 by A65,A14,XXREAL_0:2;
  then
A202: 1<=i by Lm3;
  then
A203: i in dom h0 by A199,FINSEQ_3:25;
  then
A204: h0/.i=h0.i by PARTFUN1:def 6;
A205: 1+1<=len h0 by A66,NAT_1:13;
  then 1+1 in dom h0 by FINSEQ_3:25;
  then
A206: h0/.(1+1)=h0.(1+1) by PARTFUN1:def 6;
A207: now
A208: 1+1 in dom h1 by A14,FINSEQ_3:25;
    then
A209: h1.(1+1) in rng h1 by FUNCT_1:def 3;
A210: h0.(1+1)=h11.(1+1) by A39,A14,FINSEQ_1:64;
    then h0.(1+1)=g1.(h1.(1+1)) by A208,FUNCT_1:13;
    then
A211: h0.(1+1) in Upper_Arc(P) by A5,A132,A11,A209,BORSUK_1:40,FUNCT_1:def 3;
    assume
A212: h0/.(1+1)=h0/.i;
    per cases;
    suppose
      i<=len h1;
      then h0.i=h11.i & i in dom h1 by A39,A202,FINSEQ_1:64,FINSEQ_3:25;
      hence contradiction by A38,A20,A60,A204,A206,A212,A208,A210,FUNCT_1:def 4
;
    end;
    suppose
A213: i>len h1;
      i in dom h0 by A202,A199,FINSEQ_3:25;
      then
A214: h0/.i=h0.i by PARTFUN1:def 6;
A215: i-len h11=i-'len h11 by A39,A213,XREAL_1:233;
      i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A199,
XREAL_1:9;
      then i-'len h11+2<=len h2-2+2 by A39,A215,XREAL_1:6;
      then
A216: (i-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
      i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A199,
XREAL_1:9;
      then
A217: i-'len h11+2<=len h2-2+2 by A39,A215,XREAL_1:6;
      set k=i-'len h11+2-'1;
A218: i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A199,
XREAL_1:9;
A219: 0+2<=i-'len h11 +2 by XREAL_1:6;
      then
A220: i-'len h11+2-'1=i-'len h11+2-1 by Lm1,NAT_D:39,42;
      1<=(i-'len h11 +2-'1) by A219,Lm1,NAT_D:42;
      then
A221: k in dom h2 by A46,A216,FINSEQ_3:25;
      then h2.k in rng h2 by FUNCT_1:def 3;
      then
A222: g2.(h2.k) in rng g2 by A131,A29,BORSUK_1:40,FUNCT_1:def 3;
A223: len h1 +1<=i by A213,NAT_1:13;
      then h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) & len h1 +1-len h1<=i-
      len h1 by A39,A36,A199,FINSEQ_1:23,XREAL_1:9;
      then
A224: h0.i=h21.(i-'len h11 +2-'1) by A39,A48,A56,A50,A54,A215,A218,FINSEQ_6:118
;
      then h0.i=g2.(h2.k) by A221,FUNCT_1:13;
      then h0.i in Upper_Arc(P) /\ Lower_Arc(P) by A23,A206,A212,A211,A214,A222
,XBOOLE_0:def 4;
      then h0.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
      then
A225: h0.i=W-min(P) or h0.i=E-max(P)by TARSKI:def 2;
      len h11+1-len h11<=i-len h11 by A39,A223,XREAL_1:9;
      then 1<=i-'len h11 by NAT_D:39;
      then 1+2<=i-'len h11+2 by XREAL_1:6;
      then 1+2-1<=i-'len h11+2-1 by XREAL_1:9;
      then
A226: 1<k by A220,XXREAL_0:2;
      i-'len h11+2-'1<i-'len h11+2-1+1 by A220,NAT_1:13;
      hence contradiction by A46,A76,A34,A77,A35,A32,A224,A217,A226,A221,A225,
FUNCT_1:def 4;
    end;
  end;
A227: 1 in dom g2 by Lm6,BORSUK_1:40,FUNCT_2:def 1;
A228: len h2-1-1<len h2 by Lm4;
A229: now
    per cases;
    case
A230: i<=len h1;
A231: h0/.(1+1) in Upper_Arc(P) by A5,A132,A11,A206,A42,A19,BORSUK_1:40
,FUNCT_1:def 3;
A232: 0 <= h1.(1+1) & h1.(1+1) <= 1 by A11,A19,BORSUK_1:40,XXREAL_1:1;
A233: i in dom h1 by A61,A230,FINSEQ_3:25;
      then
A234: h1.i in rng h1 by FUNCT_1:def 3;
      then
A235: h1.i<=1 by A11,BORSUK_1:40,XXREAL_1:1;
      h0.i=h11.i by A39,A61,A230,FINSEQ_1:64;
      then
A236: h0.i=g1.(h1.i) by A233,FUNCT_1:13;
      then
A237: h0/.i in Upper_Arc(P) by A5,A132,A11,A204,A234,BORSUK_1:40,FUNCT_1:def 3;
      h1.(1+1)<h1.i by A12,A60,A18,A233,SEQM_3:def 1;
      then LE h0/.(1+1),h0/.i,Upper_Arc(P),W-min(P),E-max(P) by A3,A4,A5,A6,A7
,A204,A206,A42,A236,A235,A232,Th18;
      hence LE h0/.(1+1),h0/.i,P by A231,A237,JORDAN6:def 10;
    end;
    case
A238: i>len h1;
      1+1 in dom h1 by A14,FINSEQ_3:25;
      then
A239: h11.(1+1)=g1.(h1.(1+1)) by FUNCT_1:13;
A240: i-len h11=i-'len h11 by A39,A238,XREAL_1:233;
      i+1-1<=len h1+(len h2-2)-1 by A39,A47,A36,A52,A55,A57,A200,XREAL_1:9;
      then i-len h11<=len h1+((len h2-2)-1)-len h11 by XREAL_1:9;
      then i-'len h11+2<=len h2-2-1+2 by A39,A240,XREAL_1:6;
      then
A241: i-'len h11+2-1<=len h2-1-1 by XREAL_1:9;
A242: len h1 +1<=i by A238,NAT_1:13;
      then
A243: len h1 +1-len h1<=i-len h1 by XREAL_1:9;
      h1.(1+1) in rng h1 by A15,FUNCT_1:def 3;
      then
A244: g1.(h1.(1+1)) in rng g1 by A132,A11,BORSUK_1:40,FUNCT_1:def 3;
      0+2<=i-'len h11 +2 by XREAL_1:6;
      then
A245: 2-'1<=(i-'len h11 +2-'1) by NAT_D:42;
      set k=i-'len h11+2-'1;
      0+1<=i-'len h11+1+1-1 by XREAL_1:6;
      then
A246: i-'len h11+2-'1=i-'len h11+2-1 by NAT_D:39;
A247: i-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A199,
XREAL_1:9;
      i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A199,
XREAL_1:9;
      then i-'len h11+2<=len h2-2+2 by A39,A240,XREAL_1:6;
      then i-'len h11 +2-'1<=len h21 by A47,NAT_D:44;
      then
A248: (i-'len h11 +2-'1) in dom h21 by A245,Lm1,FINSEQ_3:25;
A249: h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A39,A36,A199,A242,
FINSEQ_1:23;
      then h0.(i)=h21.(i-'len h11 +2-'1) by A39,A48,A56,A50,A54,A240,A247,A243,
FINSEQ_6:118;
      then
A250: h0.i=g2.(h2.k) by A46,A248,FUNCT_1:13;
      h2.k in rng h2 by A46,A248,FUNCT_1:def 3;
      then
A251: h0.i in Lower_Arc(P) by A23,A131,A29,A250,BORSUK_1:40,FUNCT_1:def 3;
      1<=i-len h11 by A38,A243,FINSEQ_3:29;
      then h0.i=h21.k by A48,A56,A50,A54,A240,A247,A249,FINSEQ_6:118;
      then h0/.i <> W-min P by A228,A46,A34,A35,A32,A204,A246,A248,A241,
FUNCT_1:def 4;
      hence LE h0/.(1+1),h0/.i,P by A5,A204,A206,A41,A239,A244,A251,
JORDAN6:def 10;
    end;
  end;
A252: len h0-len h11=len h0-'len h11 by A39,A65,XREAL_1:233;
  then (len h0-'len h11 +2-'1)<=len h21 by A36,A52,A55,A57,NAT_D:44;
  then (len h0-'len h11 +2-'1) in dom h21 by A43,Lm1,FINSEQ_3:25;
  then
A253: h21.k=g2.(h2.k) & h2.k in rng h2 by A46,FUNCT_1:13,def 3;
  h1.len h1 in dom g1 by A9,A69,XXREAL_1:1;
  then
A254: len h1 in dom (g1*h1) by A45,FUNCT_1:11;
  then
A255: h11.len h1=E-max(P) by A7,A9,FUNCT_1:12;
A256: for i being Element of NAT st 1<=i & i+1<=len h0 holds LE h0/.i,h0/.(i
  +1),P & h0/.(i+1)<>W-min(P) & h0/.i<>h0/.(i+1)
  proof
    let i be Element of NAT such that
A257: 1<=i and
A258: i+1<=len h0;
A259: i<i+1 by NAT_1:13;
A260: 1<i+1 by A257,NAT_1:13;
    then i+1 in dom h0 by A258,FINSEQ_3:25;
    then
A261: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A262: i<len h0 by A258,NAT_1:13;
    then i in dom h0 by A257,FINSEQ_3:25;
    then
A263: h0/.i=h0.i by PARTFUN1:def 6;
    per cases;
    suppose
A264: i<len h1;
      then
A265: i+1<=len h1 by NAT_1:13;
      then
A266: i+1 in dom h1 by A260,FINSEQ_3:25;
      then
A267: h1.(i+1) in rng h1 by FUNCT_1:def 3;
      then
A268: (h1.(i+1)) <= 1 by A11,BORSUK_1:40,XXREAL_1:1;
A269: i+1 <> 1 & i+1 <> i by A257,NAT_1:13;
A270: i in dom h1 by A257,A264,FINSEQ_3:25;
      then
A271: h1.i in rng h1 by FUNCT_1:def 3;
      then
A272: 0 <= (h1.i) & (h1.i) <= 1 by A11,BORSUK_1:40,XXREAL_1:1;
A273: h0.(i+1)=h11.(i+1) by A39,A260,A265,FINSEQ_1:64;
      then
A274: h0.(i+1)=g1.(h1.(i+1)) by A266,FUNCT_1:13;
      then
A275: h0.(i+1) in Upper_Arc(P) by A5,A132,A11,A267,BORSUK_1:40,FUNCT_1:def 3;
A276: h0.i=h11.i by A39,A257,A264,FINSEQ_1:64;
      then
A277: g1.(h1.i) = h0/.i by A263,A270,FUNCT_1:13;
      g1.(h1.i) in rng g1 by A132,A11,A271,BORSUK_1:40,FUNCT_1:def 3;
      then
A278: h0.i in Upper_Arc(P) by A5,A276,A270,FUNCT_1:13;
      h1.i<h1.(i+1) by A12,A259,A270,A266,SEQM_3:def 1;
      then LE h0/.i,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A3,A4,A5,A6,A7
,A261,A274,A277,A272,A268,Th18;
      hence
      thesis by A38,A17,A71,A20,A263,A261,A276,A270,A273,A266,A278,A275,A269,
FUNCT_1:def 4,JORDAN6:def 10;
    end;
    suppose
A279: i>=len h1;
      per cases by A279,XXREAL_0:1;
      suppose
A280:   i>len h1;
        i-len h11<len h11+(len h2-2)-len h11 by A47,A36,A52,A55,A57,A262,
XREAL_1:9;
        then
A281:   i-len h11+2<len h2-2+2 by XREAL_1:6;
        i+1>len h11 by A39,A280,NAT_1:13;
        then
A282:   i+1-len h11=i+1-'len h11 by XREAL_1:233;
        set j=i-'len h11+2-'1;
A283:   i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A258
,XREAL_1:9;
A284:   0+2<=i-'len h11 +2 by XREAL_1:6;
        then
A285:   j+1=i-'len h11+(1+1)-1+1 by Lm1,NAT_D:39,42
          .=i-'len h11+(1+1);
A286:   len h1 +1<=i by A280,NAT_1:13;
        then
A287:   len h1 +1-len h1<=i-len h1 by XREAL_1:9;
        i+1 in dom h0 by A258,A260,FINSEQ_3:25;
        then
A288:   h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A289:   len h1 +1<=i+1 by A286,NAT_1:13;
        then
A290:   len h1 +1-len h1<=i+1-len h1 by XREAL_1:9;
        then 1<i+1-'len h11+(2-1) by A39,A282,NAT_1:13;
        then
A291:   0<i+1-'len h11+2-1;
        h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A39,A36,A258,A289,
FINSEQ_1:23;
        then
A292:   h0.(i+1)=h21.(i+1-'len h11 +2-'1) by A39,A48,A56,A50,A54,A282,A283,A290
,FINSEQ_6:118;
A293:   i<=len h11 + len (mid(h21,2,len h21 -'1)) by A262,FINSEQ_1:22;
        len h11+1<=i by A39,A280,NAT_1:13;
        then
A294:   h0.i=(mid(h21, 2,len h21 -'1)).(i -len h11) by A293,FINSEQ_1:23;
A295:   i-len h11=i-'len h11 by A39,A280,XREAL_1:233;
A296:   1<=i-'len h11 +2-'1 by A284,Lm1,NAT_D:42;
        then 1<j+1 by NAT_1:13;
        then
A297:   j+1 in dom h2 by A295,A281,A285,FINSEQ_3:25;
        then
A298:   h2.(j+1) in rng h2 by FUNCT_1:def 3;
        then
A299:   (h2.(j+1)) <= 1 by A29,BORSUK_1:40,XXREAL_1:1;
        i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A262,
XREAL_1:9;
        then i-'len h11+2<=len h2-2+2 by A39,A295,XREAL_1:6;
        then i-'len h11 +2-'1<=len h21 by A47,NAT_D:44;
        then
A300:   j in dom h2 by A46,A296,FINSEQ_3:25;
        j<j+1 by NAT_1:13;
        then
A301:   h2.j<h2.(j+1) by A30,A300,A297,SEQM_3:def 1;
        i in dom h0 by A257,A262,FINSEQ_3:25;
        then
A302:   h0/.i=h0.i by PARTFUN1:def 6;
        i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A293,
XREAL_1:9;
        then
A303:   h0.i=h21.(i-'len h11 +2-'1) by A39,A48,A56,A50,A54,A294,A295,A287,
FINSEQ_6:118;
        then
A304:   h0.i=g2.(h2.j) by A300,FUNCT_1:13;
A305:   j+1=i-len h11+2-1+1 by A295,A284,Lm1,NAT_D:39,42
          .=i+1-'len h11+2-'1 by A282,A291,XREAL_0:def 2;
        then
A306:   h0/.(i+1) <> W-min P by A46,A34,A35,A32,A295,A292,A281,A285,A297,A288,
FUNCT_1:def 4;
A307:   h0.(i+1)=g2.(h2.(j+1)) by A292,A305,A297,FUNCT_1:13;
        then
A308:   h0/.(i+1) in Lower_Arc(P) by A23,A131,A29,A298,A288,BORSUK_1:40
,FUNCT_1:def 3;
A309:   h2.j in rng h2 by A300,FUNCT_1:def 3;
        then
A310:   j < j+1 & h0/.i in Lower_Arc(P) by A23,A131,A29,A304,A302,BORSUK_1:40
,FUNCT_1:def 3,NAT_1:13;
        0 <= (h2.j) & (h2.j) <= 1 by A29,A309,BORSUK_1:40,XXREAL_1:1;
        then LE h0/.i,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23
,A24,A25,A304,A307,A301,A302,A288,A299,Th18;
        hence thesis by A46,A32,A303,A292,A305,A300,A297,A302,A288,A306,A310
,A308,FUNCT_1:def 4,JORDAN6:def 10;
      end;
      suppose
A311:   i=len h1;
        then
A312:   i-len h11=i-'len h11 by A39,XREAL_1:233;
        i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A262,
XREAL_1:9;
        then
A313:   i-'len h11+2<=len h2-2+2 by A39,A312,XREAL_1:6;
        then
A314:   (i-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
        set j=i-'len h11+2-'1;
A315:   j+1 <> j;
A316:   0+2<=i-'len h11 +2 by XREAL_1:6;
        then
A317:   j+1=i-'len h11+(1+1)-1+1 by Lm1,NAT_D:39,42
          .=i-'len h11+2;
        2-'1<=(i-'len h11 +2-'1) by A316,NAT_D:42;
        then 1<j+1 by Lm1,NAT_1:13;
        then
A318:   j+1 in dom h2 by A313,A317,FINSEQ_3:25;
        then
A319:   h2.(j+1) in rng h2 by FUNCT_1:def 3;
        i+1 <=len h11 + len (mid(h21,2,len h21 -'1)) by A258,FINSEQ_1:22;
        then
A320:   i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by
XREAL_1:9;
A321:   i+1-len h11=i+1-'len h11 by A39,A259,A311,XREAL_1:233;
        then
A322:   0<i+1-'len h11+2-1 by A39,A311;
        h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A39,A36,A258,A311,
FINSEQ_1:23;
        then
A323:   h0.(i+1)=h21.(i+1-'len h11 +2-'1) by A39,A48,A56,A50,A54,A311,A321,A320
,FINSEQ_6:118;
A324:   h0.i=E-max(P) by A39,A255,A257,A311,FINSEQ_1:64;
        then
A325:   h0.i in Upper_Arc(P) by A1,Th1;
        len h1-'len h11=len h11-len h11 by A39,XREAL_0:def 2;
        then 0+2-1=len h1-'len h11+2-1;
        then
A326:   h0.i=g2.(h2.j) by A24,A26,A311,A324,NAT_D:39;
        1<=(i-'len h11 +2-'1) by A316,Lm1,NAT_D:42;
        then
A327:   j in dom h2 by A46,A314,FINSEQ_3:25;
        then
A328:   h21.j=g2.(h2.j) by FUNCT_1:13;
        i in dom h0 by A257,A262,FINSEQ_3:25;
        then
A329:   h0/.i=h0.i by PARTFUN1:def 6;
        i+1 in dom h0 by A258,A260,FINSEQ_3:25;
        then
A330:   h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A331:   j+1=i-len h11+2-1+1 by A39,A311,Lm1,XREAL_0:def 2
          .=i+1-'len h11+2-'1 by A321,A322,XREAL_0:def 2;
        then h0.(i+1)=g2.(h2.(j+1)) by A323,A318,FUNCT_1:13;
        then
A332:   h0.(i+1) in Lower_Arc(P) by A23,A131,A29,A319,BORSUK_1:40,FUNCT_1:def 3
;
        i-len h11<len h11+(len h2-2)-len h11 by A47,A36,A52,A55,A57,A262,
XREAL_1:9;
        then i-len h11+2<len h2-2+2 by XREAL_1:6;
        then j+1<len h2 by A39,A311,A317,XREAL_0:def 2;
        then h0/.(i+1) <> W-min P by A46,A34,A35,A32,A323,A331,A318,A330,
FUNCT_1:def 4;
        hence thesis by A46,A32,A323,A331,A327,A328,A326,A318,A329,A330,A332
,A325,A315,FUNCT_1:def 4,JORDAN6:def 10;
      end;
    end;
  end;
  then
A333: LE h0/.1,h0/.(1+1),P & h0/.1<>h0/.(1+1) by A205;
A334: E-max P in Upper_Arc P by A1,Th1;
  thus for i being Element of NAT,W being Subset of Euclid 2 st 1<=i & i<len
  h0 & W=Segment(h0/.i,h0/.(i+1),P) holds diameter(W)<e
  proof
    let i be Element of NAT,W be Subset of Euclid 2;
    assume that
A335: 1<=i and
A336: i<len h0 and
A337: W=Segment(h0/.i,h0/.(i+1),P);
A338: i+1<=len h0 by A336,NAT_1:13;
A339: i<i+1 by NAT_1:13;
A340: 1<i+1 by A335,NAT_1:13;
    per cases by XXREAL_0:1;
    suppose
A341: i<len h1;
      then
A342: i in dom h1 by A335,FINSEQ_3:25;
      then
A343: h1.i in rng h1 by FUNCT_1:def 3;
      then
A344: h1.i<=1 by A11,BORSUK_1:40,XXREAL_1:1;
A345: 0<=h1.i by A11,A343,BORSUK_1:40,XXREAL_1:1;
A346: h1/.i=h1.i by A335,A341,FINSEQ_4:15;
A347: h11.i=g1.(h1.i) by A342,FUNCT_1:13;
      then
A348: h0.i=g1.(h1.i) by A39,A335,A341,FINSEQ_1:64;
      then
A349: h0.i in Upper_Arc(P) by A5,A132,A11,A343,BORSUK_1:40,FUNCT_1:def 3;
      i in dom h0 by A335,A336,FINSEQ_3:25;
      then
A350: h0/.i=h0.i by PARTFUN1:def 6;
      i+1 in dom h0 by A338,A340,FINSEQ_3:25;
      then
A351: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A352: i+1<=len h1 by A341,NAT_1:13;
      then
A353: i+1 in dom h1 by A340,FINSEQ_3:25;
      then
A354: h1.i<h1.(i+1) by A12,A339,A342,SEQM_3:def 1;
A355: h1/.(i+1)=h1.(i+1) by A340,A352,FINSEQ_4:15;
A356: h1.(i+1) in rng h1 by A353,FUNCT_1:def 3;
      then reconsider Q1=[.h1/.i,h1/.(i+1).] as Subset of I[01] by A11,A343
,A346,A355,BORSUK_1:40,XXREAL_2:def 12;
A357: h0.i=h11.i by A39,A335,A341,FINSEQ_1:64;
A358: h0.(i+1)=h11.(i+1) by A39,A340,A352,FINSEQ_1:64;
      then
A359: h0.(i+1)=g1.(h1.(i+1)) by A353,FUNCT_1:13;
      then
A360: h0.(i+1) in Upper_Arc(P) by A5,A132,A11,A356,BORSUK_1:40,FUNCT_1:def 3;
A361: Segment(h0/.i,h0/.(i+1),P) c= g1.:([.h1/.i,h1/.(i+1).])
      proof
        let x be set;
A362:   h0/.(i+1) <> W-min P by A38,A17,A71,A20,A340,A358,A353,A351,
FUNCT_1:def 4;
        assume x in Segment(h0/.i,h0/.(i+1),P);
        then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A362,Def1;
        then consider p being Point of TOP-REAL 2 such that
A363:   p=x and
A364:   LE h0/.i,p,P and
A365:   LE p,h0/.(i+1),P;
A366:   h0/.i in Upper_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) or h0
/.i in Upper_Arc(P) & p in Upper_Arc(P) & LE h0/.i,p,Upper_Arc(P),W-min(P),
E-max(P) or h0/.i in Lower_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) & LE h0/.
        i,p,Lower_Arc(P),E-max(P),W-min(P) by A364,JORDAN6:def 10;
A367:   p in Upper_Arc(P) & h0/.(i+1) in Lower_Arc(P) or p in Upper_Arc(
P) & h0/.(i+1) in Upper_Arc(P) & LE p,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P)
or p in Lower_Arc(P) & h0/.(i+1) in Lower_Arc(P)& LE p,h0/.(i+1),Lower_Arc(P),
        E-max(P),W-min(P) by A365,JORDAN6:def 10;
        now
          per cases by A352,XXREAL_0:1;
          suppose
            i+1<len h1;
            then
A368:       h0/.(i+1) <> E-max P by A38,A45,A255,A20,A358,A353,A351,
FUNCT_1:def 4;
A369:       now
              assume h0/.(i+1) in Lower_Arc(P);
              then
h0/.(i+1) in Upper_Arc(P)/\ Lower_Arc(P) by A351,A360,XBOOLE_0:def 4;
              then h0/.(i+1) in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
              hence contradiction by A362,A368,TARSKI:def 2;
            end;
            then
A370:       LE p,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A365,
JORDAN6:def 10;
            then
A371:       p<>E-max(P) by A3,A368,JORDAN6:55;
A372:       p in Upper_Arc(P) by A365,A369,JORDAN6:def 10;
            per cases by A335,XXREAL_0:1;
            suppose
              i>1;
              then
A373:         h0/.i <> W-min P by A38,A17,A71,A20,A342,A347,A348,A350,
FUNCT_1:def 4;
A374:         h11.i <> E-max(P) by A38,A45,A255,A20,A341,A342,FUNCT_1:def 4;
              now
                assume h0/.i in Lower_Arc(P);
                then h0/.i in Upper_Arc(P)/\ Lower_Arc(P) by A350,A349,
XBOOLE_0:def 4;
                then h0/.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
                hence contradiction by A357,A350,A373,A374,TARSKI:def 2;
              end;
              then
A375:         h0/.i in Upper_Arc(P) & p in Lower_Arc(P) & not p=W-min(P)
or h0/.i in Upper_Arc(P) & p in Upper_Arc(P) & LE h0/.i,p,Upper_Arc(P),W-min(P)
              ,E-max(P) by A364,JORDAN6:def 10;
              then
A376:         p <> W-min P by A3,A373,JORDAN6:54;
A377:         now
                assume p in Lower_Arc(P);
                then p in Upper_Arc(P)/\ Lower_Arc(P) by A372,XBOOLE_0:def 4;
                then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
                hence contradiction by A371,A376,TARSKI:def 2;
              end;
              then consider z being set such that
A378:         z in dom g1 and
A379:         p=g1.z by A5,A375,FUNCT_1:def 3;
              reconsider rz=z as Real by A132,A378;
A380:         rz<=1 by A378,BORSUK_1:40,XXREAL_1:1;
              h1.(i+1) in rng h1 by A353,FUNCT_1:def 3;
              then
A381:         0<=h1/.(i+1) & h1/.(i+1)<=1 by A11,A355,BORSUK_1:40,XXREAL_1:1;
              take z;
              thus z in dom g1 by A378;
A382:         g1.(h1/.i)=h0/.i & h1/.i<=1 by A335,A341,A357,A347,A344,A350,
FINSEQ_4:15;
              g1.(h1/.(i+1))=h0/.(i+1) by A340,A352,A359,A351,FINSEQ_4:15;
              then
A383:         rz<=h1/.(i+1) by A4,A5,A6,A7,A370,A379,A381,A380,Th19;
              0<=rz by A378,BORSUK_1:40,XXREAL_1:1;
              then h1/.i<=rz by A4,A5,A6,A7,A375,A377,A379,A382,A380,Th19;
              hence z in [.h1/.i,h1/.(i+1).] by A383,XXREAL_1:1;
              thus x = g1.z by A363,A379;
            end;
            suppose
A384:         i=1;
              now
                per cases;
                case
A385:             p<>W-min(P);
                  now
                    assume p in Lower_Arc(P);
                    then p in Upper_Arc(P)/\ Lower_Arc(P) by A372,
XBOOLE_0:def 4;
                    then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
                    hence contradiction by A371,A385,TARSKI:def 2;
                  end;
                  then consider z being set such that
A386:             z in dom g1 and
A387:             p=g1.z by A5,A366,FUNCT_1:def 3;
                  reconsider rz=z as Real by A132,A386;
A388:             h1/.1<=rz by A8,A346,A384,A386,BORSUK_1:40,XXREAL_1:1;
                  h1.(1+1) in rng h1 by A353,A384,FUNCT_1:def 3;
                  then
A389:             0<=h1/.(1+1) & h1/.(1+1)<=1 by A11,A355,A384,BORSUK_1:40
,XXREAL_1:1;
A390:             g1.(h1/.(1+1))=h0/.(1+1) by A352,A359,A351,A384,FINSEQ_4:15;
                  take rz;
                  rz<=1 by A386,BORSUK_1:40,XXREAL_1:1;
                  then rz<=h1/.(1+1) by A4,A5,A6,A7,A370,A384,A387,A390,A389
,Th19;
                  hence
                  rz in dom g1 & rz in [.h1/.1,h1/.(1+1).] & x = g1.rz by A363
,A386,A387,A388,XXREAL_1:1;
                end;
                case
A391:             p=W-min(P);
                  thus 0 in [.h1/.1,h1/.(1+1).] by A8,A354,A346,A355,A384,
XXREAL_1:1;
                  thus x = g1.0 by A6,A363,A391;
                end;
              end;
              hence ex y being set st y in dom g1 & y in [.h1/.i,h1/.(i+1).] &
              x = g1.y by A44,A384;
            end;
          end;
          suppose
A392:       i+1=len h1;
            then
A393:       h0/.(i+1)=E-max(P) by A7,A9,A45,A358,A351,FUNCT_1:13;
A394:       now
              assume that
A395:         p in Lower_Arc(P) and
A396:         not p in Upper_Arc(P);
              LE h0/.(i+1),p,Lower_Arc(P),E-max(P),W-min(P) by A21,A393,A395,
JORDAN5C:10;
              hence contradiction by A334,A21,A367,A393,A396,JORDAN5C:12;
            end;
            p in Upper_Arc(P) or p in Lower_Arc(P) by A364,JORDAN6:def 10;
            then
A397:       LE p,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A3,A393,A394,
JORDAN5C:10;
            per cases;
            suppose
A398:         p<>E-max(P);
              now
                per cases;
                case
A399:             p<>W-min(P);
A400:             now
                    assume p in Lower_Arc(P);
                    then p in Upper_Arc(P)/\ Lower_Arc(P) by A394,
XBOOLE_0:def 4;
                    then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
                    hence contradiction by A398,A399,TARSKI:def 2;
                  end;
                  then consider z being set such that
A401:             z in dom g1 and
A402:             p=g1.z by A5,A366,FUNCT_1:def 3;
                  reconsider rz=z as Real by A132,A401;
A403:             rz<=1 by A401,BORSUK_1:40,XXREAL_1:1;
                  h1.(i+1) in rng h1 by A353,FUNCT_1:def 3;
                  then
A404:             0<=h1/.(i+1) & h1/.(i+1)<=1 by A11,A355,BORSUK_1:40
,XXREAL_1:1;
                  g1.(h1/.(i+1))=h0/.(i+1) by A340,A352,A359,A351,FINSEQ_4:15;
                  then
A405:             rz<=h1/.(i+1) by A4,A5,A6,A7,A397,A402,A404,A403,Th19;
                  take rz;
                  0<=rz by A401,BORSUK_1:40,XXREAL_1:1;
                  then h1/.i<=rz by A4,A5,A6,A7,A357,A347,A344,A350,A346,A366
,A400,A402,A403,Th19;
                  hence
                  rz in dom g1 & rz in [.h1/.i,h1/.(i+1).] & x = g1.rz by A363
,A401,A402,A405,XXREAL_1:1;
                end;
                case
A406:             p=W-min(P);
                  then h11.i=W-min(P) by A3,A357,A350,A366,JORDAN6:54;
                  then i=1 by A38,A17,A71,A20,A342,FUNCT_1:def 4;
                  then 0 in [.h1/.i,h1/.(i+1).] by A8,A354,A346,A355,XXREAL_1:1
;
                  hence ex y being set st y in dom g1 & y in [.h1/.i,h1/.(i+1)
                  .] & x = g1.y by A6,A44,A363,A406;
                end;
              end;
              hence ex y being set st y in dom g1 & y in [.h1/.i,h1/.(i+1).] &
              x = g1.y;
            end;
            suppose
A407:         p=E-max(P);
              1 in [.h1/.i,h1/.(i+1).] by A9,A354,A346,A355,A392,XXREAL_1:1;
              hence ex y being set st y in dom g1 & y in [.h1/.i,h1/.(i+1).] &
              x = g1.y by A7,A69,A363,A407,Lm6;
            end;
          end;
        end;
        hence thesis by FUNCT_1:def 6;
      end;
A408: h1.(i+1)<=1 by A11,A356,BORSUK_1:40,XXREAL_1:1;
      g1.:([.h1/.i,h1/.(i+1).]) c= Segment(h0/.i,h0/.(i+1),P)
      proof
A409:   g1.(h1/.i)=h0/.i & 0<=h1/.i by A335,A341,A348,A345,A350,FINSEQ_4:15;
        let x be set;
        assume x in g1.:([.h1/.i,h1/.(i+1).]);
        then consider y being set such that
A410:   y in dom g1 and
A411:   y in [.h1/.i,h1/.(i+1).] and
A412:   x=g1.y by FUNCT_1:def 6;
        reconsider sy=y as Real by A411;
A413:   sy<=1 by A410,BORSUK_1:40,XXREAL_1:1;
A414:   x in Upper_Arc(P) by A5,A410,A412,FUNCT_1:def 3;
        then reconsider p1=x as Point of TOP-REAL 2;
A415:   h1/.i<=1 by A335,A341,A344,FINSEQ_4:15;
        h1/.i<=sy by A411,XXREAL_1:1;
        then LE h0/.i,p1,Upper_Arc(P),W-min(P),E-max(P) by A3,A4,A5,A6,A7,A412
,A409,A415,A413,Th18;
        then
A416:   LE h0/.i,p1,P by A350,A349,A414,JORDAN6:def 10;
        sy<=h1/.(i+1) & 0<=sy by A410,A411,BORSUK_1:40,XXREAL_1:1;
        then LE p1,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A3,A4,A5,A6,A7
,A359,A408,A351,A355,A412,A413,Th18;
        then LE p1,h0/.(i+1),P by A351,A360,A414,JORDAN6:def 10;
        then
A417:   x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A416;
        not h0/.(i+1)=W-min P by A38,A17,A71,A20,A340,A358,A353,A351,
FUNCT_1:def 4;
        hence thesis by A417,Def1;
      end;
      then W=g1.:Q1 by A337,A361,XBOOLE_0:def 10;
      hence thesis by A13,A335,A341;
    end;
    suppose
A418: i>len h1;
      i-len h11<len h11+(len h2-2)-len h11 by A47,A36,A52,A55,A57,A336,
XREAL_1:9;
      then
A419: i-len h11+2<len h2-2+2 by XREAL_1:6;
A420: len h1 +1<=i by A418,NAT_1:13;
      then
A421: len h1 +1-len h1<=i-len h1 by XREAL_1:9;
A422: i-len h11=i-'len h11 by A39,A418,XREAL_1:233;
      i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A336,
XREAL_1:9;
      then
A423: i-'len h11+2<=len h2-2+2 by A39,A422,XREAL_1:6;
      i+1>len h11 by A39,A418,NAT_1:13;
      then
A424: i+1-len h11=i+1-'len h11 by XREAL_1:233;
      i+1 in dom h0 by A338,A340,FINSEQ_3:25;
      then
A425: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A426: i<=len h11 + len (mid(h21,2,len h21 -'1)) by A336,FINSEQ_1:22;
      len h11+1<=i by A39,A418,NAT_1:13;
      then
A427: h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A426,FINSEQ_1:23;
A428: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A338,
XREAL_1:9;
      i in dom h0 by A335,A336,FINSEQ_3:25;
      then
A429: h0/.i=h0.i by PARTFUN1:def 6;
      set j=i-'len h11+2-'1;
      len h2<len h2+1 by NAT_1:13;
      then
A430: len h2-1<len h2+1-1 by XREAL_1:9;
A431: 0+2<=i-'len h11 +2 by XREAL_1:6;
      then
A432: j+1=i-'len h11+1+1-1+1 by Lm1,NAT_D:39,42
        .=i-'len h11+(1+1);
A433: 1<=(i-'len h11 +2-'1) by A431,Lm1,NAT_D:42;
      then
A434: 1<j+1 by NAT_1:13;
      then
A435: j+1 in dom h2 by A423,A432,FINSEQ_3:25;
      then
A436: h2.(j+1) in rng h2 by FUNCT_1:def 3;
      then
A437: h2.(j+1) <= 1 by A29,BORSUK_1:40,XXREAL_1:1;
A438: h2/.(j+1)=h2.(j+1) by A423,A432,A434,FINSEQ_4:15;
      (i-'len h11 +2-'1)<=len h21 by A47,A423,NAT_D:44;
      then
A439: j in dom h2 by A46,A433,FINSEQ_3:25;
      i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A336,
XREAL_1:9;
      then
A440: h0.i=h21.(i-'len h11 +2-'1) by A39,A48,A56,A50,A54,A427,A422,A421,
FINSEQ_6:118;
      then
A441: h0.i=g2.(h2.j) by A439,FUNCT_1:13;
A442: h2.j in rng h2 by A439,FUNCT_1:def 3;
      then g2.(h2.j) in rng g2 by A131,A29,BORSUK_1:40,FUNCT_1:def 3;
      then
A443: h0.i in Lower_Arc(P) by A23,A440,A439,FUNCT_1:13;
      i-'len h11+2-1<=len h2-1 by A423,XREAL_1:9;
      then i-'len h11+2-1<len h2 by A430,XXREAL_0:2;
      then
A444: j< len h2 by A431,Lm1,NAT_D:39,42;
      then
A445: h2/.j=h2.j by A431,Lm1,FINSEQ_4:15,NAT_D:42;
      then reconsider
      Q1=[.h2/.j,h2/.(j+1).] as Subset of I[01] by A29,A442,A436,A438,
BORSUK_1:40,XXREAL_2:def 12;
A446: 0 <= h2.j & h2.j <= 1 by A29,A442,BORSUK_1:40,XXREAL_1:1;
A447: i-'len h11+2-'1=i-'len h11+2-1 by A431,Lm1,NAT_D:39,42;
A448: len h1 +1<=i+1 by A420,NAT_1:13;
      then
A449: len h1 +1-len h1<=i+1-len h1 by XREAL_1:9;
      then 1<i+1-'len h11+(2-1) by A39,A424,NAT_1:13;
      then 0<i+1-'len h11+2-1;
      then
A450: j+1 =i+1-'len h11+2-'1 by A422,A424,A447,XREAL_0:def 2;
      h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A39,A36,A338,A448,
FINSEQ_1:23;
      then
A451: h0.(i+1)=h21.(i+1-'len h11 +2-'1) by A39,A48,A56,A50,A54,A424,A428,A449,
FINSEQ_6:118;
      then h0.(i+1)=g2.(h2.(j+1)) by A450,A435,FUNCT_1:13;
      then
A452: h0.(i+1) in Lower_Arc(P) by A23,A131,A29,A436,BORSUK_1:40,FUNCT_1:def 3;
      len h1 +1<=i by A418,NAT_1:13;
      then len h11+1-len h11<=i-len h11 by A39,XREAL_1:9;
      then 1<=i-'len h11 by NAT_D:39;
      then 1+2<=i-'len h11+2 by XREAL_1:6;
      then 1+2-1<=i-'len h11+2-1 by XREAL_1:9;
      then
A453: 1<j by A447,XXREAL_0:2;
A454: Segment(h0/.i,h0/.(i+1),P) c= g2.:([.h2/.j,h2/.(j+1).])
      proof
        h2.(j+1) in rng h2 by A435,FUNCT_1:def 3;
        then
A455:   0<=h2/.(j+1) & h2/.(j+1)<=1 by A29,A438,BORSUK_1:40,XXREAL_1:1;
A456:   g2.(h2/.(j+1))=h0/.(i+1) by A451,A450,A435,A425,A438,FUNCT_1:13;
        j<len h2 by A423,A432,NAT_1:13;
        then
A457:   h0/.i <> W-min(P) by A46,A34,A35,A32,A440,A439,A429,FUNCT_1:def 4;
A458:   h2/.j<=1 by A29,A442,A445,BORSUK_1:40,XXREAL_1:1;
        let x be set;
        assume
A459:   x in Segment(h0/.i,h0/.(i+1),P);
        h0/.(i+1) <> W-min P by A46,A34,A35,A32,A422,A451,A419,A432,A450,A435
,A425,FUNCT_1:def 4;
        then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A459,Def1;
        then consider p being Point of TOP-REAL 2 such that
A460:   p=x and
A461:   LE h0/.i,p,P and
A462:   LE p,h0/.(i+1),P;
A463:   h0/.i in Upper_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) or h0
/.i in Upper_Arc(P) & p in Upper_Arc(P) & LE h0/.i,p,Upper_Arc(P),W-min(P),
E-max(P) or h0/.i in Lower_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) & LE h0/.
        i,p,Lower_Arc(P),E-max(P),W-min(P) by A461,JORDAN6:def 10;
A464:   h21.j <> E-max P by A46,A76,A77,A32,A453,A439,FUNCT_1:def 4;
A465:   now
          assume h0/.i in Upper_Arc(P);
          then h0/.i in Upper_Arc(P)/\ Lower_Arc(P) by A429,A443,XBOOLE_0:def 4
;
          then h0/.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
          hence contradiction by A440,A429,A457,A464,TARSKI:def 2;
        end;
        then
A466:   LE h0/.i,p,Lower_Arc P, E-max P, W-min P by A461,JORDAN6:def 10;
A467:   h0/.i <> E-max(P) by A46,A76,A77,A32,A440,A453,A439,A429,FUNCT_1:def 4;
A468:   now
          assume p in Upper_Arc(P);
          then p in Upper_Arc P /\ Lower_Arc P by A463,A465,XBOOLE_0:def 4;
          then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
          then p=W-min(P) or p=E-max(P) by TARSKI:def 2;
          hence contradiction by A21,A463,A465,A467,JORDAN6:54;
        end;
A469:   h0/.(i+1) <> E-max P & h21.(j+1) <> W-min P by A46,A76,A34,A77,A35,A32
,A422,A451,A419,A432,A450,A434,A435,A425,FUNCT_1:def 4;
        now
          assume h0/.(i+1) in Upper_Arc(P);
          then h0/.(i+1) in Upper_Arc(P)/\ Lower_Arc(P) by A425,A452,
XBOOLE_0:def 4;
          then h0/.(i+1) in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
          hence contradiction by A451,A450,A425,A469,TARSKI:def 2;
        end;
        then p in Lower_Arc(P) & h0/.(i+1) in Lower_Arc(P)& not h0/.(i+ 1)=
W-min(P) & LE p,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) or p in Upper_Arc(P) &
h0/.(i+1) in Lower_Arc(P) & not h0/.(i+1)=W-min(P) by A462,JORDAN6:def 10;
        then consider z being set such that
A470:   z in dom g2 and
A471:   p=g2.z by A23,A468,FUNCT_1:def 3;
        reconsider rz=z as Real by A131,A470;
A472:   rz<=1 by A470,BORSUK_1:40,XXREAL_1:1;
        LE p,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A462,A468,
JORDAN6:def 10;
        then
A473:   rz<=h2/.(j+1) by A22,A23,A24,A25,A471,A456,A472,A455,Th19;
        0<=rz by A470,BORSUK_1:40,XXREAL_1:1;
        then h2/.j<=rz by A22,A23,A24,A25,A441,A429,A445,A466,A471,A458,A472
,Th19;
        then rz in [.h2/.j,h2/.(j+1).] by A473,XXREAL_1:1;
        hence thesis by A460,A470,A471,FUNCT_1:def 6;
      end;
A474: g2.(h2.(j+1)) = h0/.(i+1) by A451,A450,A435,A425,FUNCT_1:13;
      g2.:([.h2/.j,h2/.(j+1).]) c= Segment(h0/.i,h0/.(i+1),P)
      proof
        let x be set;
        assume x in g2.:([.h2/.j,h2/.(j+1).]);
        then consider y being set such that
A475:   y in dom g2 and
A476:   y in [.h2/.j,h2/.(j+1).] and
A477:   x=g2.y by FUNCT_1:def 6;
        reconsider sy=y as Real by A476;
A478:   sy<=h2/.(j+1) by A476,XXREAL_1:1;
A479:   x in Lower_Arc(P) by A23,A475,A477,FUNCT_1:def 3;
        then reconsider p1=x as Point of TOP-REAL 2;
A480:   h2.(j+1) <> 1 by A27,A30,A34,A422,A419,A432,A435,FUNCT_1:def 4;
A481:   now
          assume p1=W-min(P);
          then 1=sy by A22,A25,A227,A475,A477,FUNCT_1:def 4;
          hence contradiction by A437,A438,A478,A480,XXREAL_0:1;
        end;
A482:   sy<=1 by A475,BORSUK_1:40,XXREAL_1:1;
        h2/.j<=sy by A476,XXREAL_1:1;
        then LE h0/.i,p1,Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23,A24,A25
,A441,A429,A446,A445,A477,A482,Th18;
        then
A483:   LE h0/.i,p1,P by A429,A443,A479,A481,JORDAN6:def 10;
A484:   h0/.(i+1) <> W-min P by A46,A34,A35,A32,A422,A451,A419,A432,A450,A435
,A425,FUNCT_1:def 4;
        0<=sy by A475,BORSUK_1:40,XXREAL_1:1;
        then LE p1,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23,A24
,A25,A474,A437,A438,A477,A478,A482,Th18;
        then LE p1,h0/.(i+1),P by A425,A452,A479,A484,JORDAN6:def 10;
        then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A483;
        hence thesis by A484,Def1;
      end;
      then W=g2.:(Q1) by A337,A454,XBOOLE_0:def 10;
      hence thesis by A31,A433,A444;
    end;
    suppose
A485: i=len h1;
A486: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A338,
XREAL_1:9;
      then 1<=i+1-'len h11 by A39,A339,A485,XREAL_1:233;
      then 1<i+1-'len h11+(2-1) by NAT_1:13;
      then
A487: 0<i+1-'len h11+2-1;
      i in dom h0 by A335,A336,FINSEQ_3:25;
      then
A488: h0/.i=h0.i by PARTFUN1:def 6;
A489: h0.i=E-max(P) by A39,A255,A335,A485,FINSEQ_1:64;
      set j=i-'len h11+2-'1;
A490: 0+2<=i-'len h11 +2 by XREAL_1:6;
      then
A491: j+1=i-'len h11+1+1-1+1 by Lm1,NAT_D:39,42
        .=i-'len h11+(1+1);
A492: len h1-'len h11=len h11-len h11 by A39,XREAL_0:def 2;
      then
A493: 0+2-1=len h1-'len h11+2-1;
      then
A494: h0.i=g2.(h2.j) by A24,A26,A485,A489,NAT_D:39;
A495: i-len h11=i-'len h11 by A39,A485,XREAL_1:233;
      i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A336,
XREAL_1:9;
      then
A496: i-'len h11+2<=len h2-2+2 by A39,A495,XREAL_1:6;
      i-len h11<len h11+(len h2-2)-len h11 by A47,A36,A52,A55,A57,A336,
XREAL_1:9;
      then
A497: i-len h11+2<len h2-2+2 by XREAL_1:6;
      then
A498: j+1<len h2 by A39,A485,A491,XREAL_0:def 2;
A499: h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A39,A36,A338,A485,
FINSEQ_1:23;
      len h2<len h2+1 by NAT_1:13;
      then
A500: len h2-1<len h2+1-1 by XREAL_1:9;
      i+1 in dom h0 by A338,A340,FINSEQ_3:25;
      then
A501: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A502: 1<=(i-'len h11 +2-'1) by A490,Lm1,NAT_D:42;
      then
A503: 1<j+1 by NAT_1:13;
      then
A504: j+1 in dom h2 by A496,A491,FINSEQ_3:25;
      then
A505: h2.(j+1) in rng h2 by FUNCT_1:def 3;
      then
A506: h2.(j+1) <= 1 by A29,BORSUK_1:40,XXREAL_1:1;
      (i-'len h11 +2-'1)<=len h21 by A47,A496,NAT_D:44;
      then
A507: j in dom h2 by A46,A502,FINSEQ_3:25;
      then
A508: h2.j in rng h2 by FUNCT_1:def 3;
      then g2.(h2.j) in rng g2 by A131,A29,BORSUK_1:40,FUNCT_1:def 3;
      then
A509: h0.i in Lower_Arc P by A23,A24,A26,A485,A489,A493,NAT_D:39;
A510: h2/.(j+1)=h2.(j+1) by A496,A491,A503,FINSEQ_4:15;
      i-'len h11+2-1<=len h2-1 by A496,XREAL_1:9;
      then
A511: i-'len h11+2-1<len h2 by A500,XXREAL_0:2;
      then
A512: j<len h2 by A490,Lm1,NAT_D:39,42;
      then h2/.j=h2.j by A490,Lm1,FINSEQ_4:15,NAT_D:42;
      then reconsider
      Q1=[.h2/.j,h2/.(j+1).] as Subset of I[01] by A29,A508,A505,A510,
BORSUK_1:40,XXREAL_2:def 12;
A513: i+1-len h11=i+1-'len h11 by A39,A339,A485,XREAL_1:233;
      j+1=i-len h11+2-1+1 by A39,A485,Lm1,XREAL_0:def 2
        .=i+1-'len h11+2-'1 by A513,A487,XREAL_0:def 2;
      then
A514: h0
.(i+1)=h21.(j+1) by A39,A48,A56,A50,A54,A485,A499,A513,A486,FINSEQ_6:118;
      then
A515: h0.(i+1)=g2.(h2.(j+1)) by A504,FUNCT_1:13;
      then
A516: h0.(i+1) in Lower_Arc P by A23,A131,A29,A505,BORSUK_1:40,FUNCT_1:def 3;
A517: h21.j=g2.(h2.j) by A507,FUNCT_1:13;
A518: Segment(h0/.i,h0/.(i+1),P) c= g2.:([.h2/.j,h2/.(j+1).])
      proof
        j+1<len h2 by A39,A485,A497,A491,XREAL_0:def 2;
        then j<len h2 by NAT_1:13;
        then
A519:   h0/.i<>W-min(P) by A46,A34,A35,A32,A507,A517,A494,A488,FUNCT_1:def 4;
A520:   g2.(h2/.(j+1))=h0/.(i+1) by A496,A491,A503,A515,A501,FINSEQ_4:15;
        h2.(j+1) in rng h2 by A504,FUNCT_1:def 3;
        then
A521:   0<=h2/.(j+1) & h2/.(j+1)<=1 by A29,A510,BORSUK_1:40,XXREAL_1:1;
A522:   h0/.(i+1) in Lower_Arc(P) by A23,A131,A29,A515,A505,A501,BORSUK_1:40
,FUNCT_1:def 3;
        let x be set;
        assume
A523:   x in Segment(h0/.i,h0/.(i+1),P);
        h0/.(i+1) <> W-min P by A46,A34,A35,A32,A498,A514,A504,A501,
FUNCT_1:def 4;
        then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A523,Def1;
        then consider p being Point of TOP-REAL 2 such that
A524:   p=x and
A525:   LE h0/.i,p,P and
A526:   LE p,h0/.(i+1),P;
A527:   h0/.i in Upper_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) or h0
/.i in Upper_Arc(P) & p in Upper_Arc(P) & LE h0/.i,p,Upper_Arc(P),W-min(P),
E-max(P) or h0/.i in Lower_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) & LE h0/.
        i,p,Lower_Arc(P),E-max(P),W-min(P) by A525,JORDAN6:def 10;
        dom (g1*h1) c= dom h0 by FINSEQ_1:26;
        then
A528:   h0/.i=E-max(P) by A254,A485,A489,PARTFUN1:def 6;
A529:   now
          assume
A530:     not p in Lower_Arc(P);
          then p=E-max(P) by A3,A527,A528,JORDAN6:55;
          hence contradiction by A1,A530,Th1;
        end;
A531:   now
          assume p in Upper_Arc(P);
          then p in Upper_Arc(P)/\ Lower_Arc(P) by A529,XBOOLE_0:def 4;
          then
A532:     p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
          p <> W-min P by A3,A527,A519,JORDAN6:54;
          hence p = E-max P by A532,TARSKI:def 2;
        end;
        then p in rng g2 by A1,A23,A525,Th1,JORDAN6:def 10;
        then consider z being set such that
A533:   z in dom g2 and
A534:   p=g2.z by FUNCT_1:def 3;
        reconsider rz=z as Real by A131,A533;
        0<=rz by A533,BORSUK_1:40,XXREAL_1:1;
        then
A535:   h2/.j<=rz by A26,A485,A511,A492,Lm1,FINSEQ_4:15;
A536:   not h0/.(i+1)=E-max(P) by A46,A76,A77,A32,A503,A514,A504,A501,
FUNCT_1:def 4;
        now
          assume h0/.(i+1) in Upper_Arc(P);
          then h0/.(i+1) in Upper_Arc(P)/\ Lower_Arc(P) by A522,XBOOLE_0:def 4;
          then h0/.(i+1) in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
          then h21.(j+1)=W-min(P) by A514,A501,A536,TARSKI:def 2;
          hence contradiction by A46,A34,A35,A32,A498,A504,FUNCT_1:def 4;
        end;
        then p in Lower_Arc(P) & h0/.(i+1) in Lower_Arc(P) & not h0/.(i +1)=
W-min(P) & LE p,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) or p in Upper_Arc(P) &
h0/.(i+1) in Lower_Arc(P) & not h0/.(i+1)=W-min(P) by A526,JORDAN6:def 10;
        then
A537:   LE p,h0/.(i+1),Lower_Arc P, E-max P, W-min P by A21,A531,JORDAN5C:10;
        rz<=1 by A533,BORSUK_1:40,XXREAL_1:1;
        then rz<=h2/.(j+1) by A22,A23,A24,A25,A537,A534,A520,A521,Th19;
        then rz in [.h2/.j,h2/.(j+1).] by A535,XXREAL_1:1;
        hence thesis by A524,A533,A534,FUNCT_1:def 6;
      end;
A538: g2.(h2.(j+1)) = h0/.(i+1) by A514,A504,A501,FUNCT_1:13;
      g2.:([.h2/.j,h2/.(j+1).]) c= Segment(h0/.i,h0/.(i+1),P)
      proof
        let x be set;
        assume x in g2.:([.h2/.j,h2/.(j+1).]);
        then consider y being set such that
A539:   y in dom g2 and
A540:   y in [.h2/.j,h2/.(j+1).] and
A541:   x=g2.y by FUNCT_1:def 6;
        reconsider sy=y as Real by A540;
A542:   sy<=h2/.(j+1) by A540,XXREAL_1:1;
A543:   x in Lower_Arc(P) by A23,A539,A541,FUNCT_1:def 3;
        then reconsider p1=x as Point of TOP-REAL 2;
A544:   h2.(j+1) <> 1 by A27,A30,A34,A498,A504,FUNCT_1:def 4;
A545:   now
          assume p1=W-min(P);
          then 1=sy by A22,A25,A227,A539,A541,FUNCT_1:def 4;
          hence contradiction by A506,A510,A542,A544,XXREAL_0:1;
        end;
A546:   0<=sy & sy<=1 by A539,BORSUK_1:40,XXREAL_1:1;
        then LE h0/.i,p1,Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23,A24,A25
,A489,A488,A541,Th18;
        then
A547:   LE h0/.i,p1,P by A488,A509,A543,A545,JORDAN6:def 10;
A548:   h0/.(i+1) <> W-min(P) by A46,A34,A35,A32,A498,A514,A504,A501,
FUNCT_1:def 4;
        LE p1,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23,A24,A25
,A538,A506,A510,A541,A542,A546,Th18;
        then LE p1,h0/.(i+1),P by A501,A516,A543,A548,JORDAN6:def 10;
        then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A547;
        hence thesis by A548,Def1;
      end;
      then W=g2.:(Q1) by A337,A518,XBOOLE_0:def 10;
      hence thesis by A31,A502,A512;
    end;
  end;
A549: len h0=len h1+(len h2-2) by A38,A47,A36,A52,A55,A57,FINSEQ_3:29;
  thus for W being Subset of Euclid 2 st W=Segment(h0/.len h0,h0/.1,P) holds
  diameter W < e
  proof
    set i=len h0;
    let W be Subset of Euclid 2;
    set j=i-'len h11+2-'1;
A550: 0+2<=i-'len h11 +2 by XREAL_1:6;
    then
A551: 1<=(i-'len h11 +2-'1) by Lm1,NAT_D:42;
    len h11+1-len h11<=i-len h11 by A47,A36,A52,A55,A57,A62,XXREAL_0:2;
    then 1<=i-'len h11 by NAT_D:39;
    then 1+2<=i-'len h11+2 by XREAL_1:6;
    then
A552: 1+2-1<=i-'len h11+2-1 by XREAL_1:9;
    len h0<=len h11 + len mid(h21,2,len h21 -'1) by FINSEQ_1:22;
    then
A553: h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A39,A64,FINSEQ_1:23;
A554: i-len h11=i-'len h11 by A39,A65,XREAL_1:233;
    then (i-'len h11 +2-'1)<=len h21 by A36,A52,A55,A57,NAT_D:44;
    then
A555: j in dom h2 by A46,A551,FINSEQ_3:25;
    then
A556: h2.j in rng h2 by FUNCT_1:def 3;
    i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 & len h1 +
    1-len h1 <=i-len h1 by A549,A62,FINSEQ_1:22,XXREAL_0:2;
    then
A557: h0.i=h21.(i-'len h11 +2-'1) by A39,A48,A56,A50,A54,A553,A554,FINSEQ_6:118
;
    then
A558: h0.i=g2.(h2.j) by A555,FUNCT_1:13;
    then
A559: h0.i in Lower_Arc P by A23,A131,A29,A556,BORSUK_1:40,FUNCT_1:def 3;
A560: 2-'1<=(i-'len h11 +2-'1) by A550,NAT_D:42;
    then
A561: 1<j+1 by Lm1,NAT_1:13;
    then
A562: h2/.(j+1)=h2.(j+1) by A47,A36,A52,A55,A57,A554,FINSEQ_4:15;
    len h2<len h2+1 by NAT_1:13;
    then
A563: len h2-1<len h2+1-1 by XREAL_1:9;
    then
A564: h2/.j=h2.j by A47,A36,A52,A55,A57,A554,A560,Lm1,FINSEQ_4:15;
    j+1 in dom h2 by A46,A36,A52,A55,A57,A554,A561,FINSEQ_3:25;
    then h2.(j+1) in rng h2 by FUNCT_1:def 3;
    then reconsider Q1=[.h2/.j,h2/.(j+1).] as Subset of I[01] by A29,A556,A564
,A562,BORSUK_1:40,XXREAL_2:def 12;
    i in dom h0 by A66,FINSEQ_3:25;
    then
A565: h0/.i=h0.i by PARTFUN1:def 6;
    i-'len h11+2-'1=i-'len h11+2-1 by A550,Lm1,NAT_D:39,42;
    then
A566: 1<j by A552,XXREAL_0:2;
A567: now
      assume h0.i in Upper_Arc(P);
      then h0.i in Upper_Arc(P)/\ Lower_Arc(P) by A559,XBOOLE_0:def 4;
      then h0.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
      then h0.i=W-min(P) or h0.i=E-max(P) by TARSKI:def 2;
      hence contradiction by A46,A47,A76,A34,A77,A35,A36,A52,A55,A57,A32,A554
,A557,A563,A566,A555,FUNCT_1:def 4;
    end;
A568: h2.j<=1 by A29,A556,BORSUK_1:40,XXREAL_1:1;
A569: Segment(h0/.i,h0/.1,P) c= g2.:([.h2/.j,h2/.(j+1).])
    proof
      let x be set;
      assume
A570: x in Segment(h0/.i,h0/.1,P);
      h0/.1=W-min(P) by A72,A67,PARTFUN1:def 6;
      then
A571: x in {p: LE h0/.i,p,P or h0/.i in P & p=W-min(P)} by A570,Def1;
A572: j+1 in dom h2 by A46,A36,A52,A55,A57,A554,A561,FINSEQ_3:25;
      j<j+1 & j in dom h2 by A47,A36,A52,A55,A57,A554,A560,A563,Lm1,FINSEQ_3:25
 ;
      then h2.j<h2.(j+1) by A30,A572,SEQM_3:def 1;
      then
A573: h2/.(j+1) in [.h2/.j, h2/.(j+1).] by A564,A562,XXREAL_1:1;
      consider p being Point of TOP-REAL 2 such that
A574: p=x and
A575: LE h0/.i,p,P or h0/.i in P & p=W-min(P) by A571;
A576: h2/.(j+1)=1 by A27,A47,A34,A36,A52,A55,A57,A554,PARTFUN1:def 6;
      now
        per cases by A575;
        suppose
A577:     LE h0/.i,p,P & (p<>W-min(P) or not h0/.i in P);
          then p in Lower_Arc(P) by A567,A565,JORDAN6:def 10;
          then consider z being set such that
A578:     z in dom g2 and
A579:     p=g2.z by A23,FUNCT_1:def 3;
          take z;
          thus z in dom g2 by A578;
          reconsider rz=z as Real by A131,A578;
A580:     rz<=1 by A578,BORSUK_1:40,XXREAL_1:1;
          then
A581:     rz<=h2/.(j+1) by A27,A47,A36,A52,A55,A57,A554,A561,FINSEQ_4:15;
A582:     LE h0/.i,p,Lower_Arc(P),E-max(P),W-min(P) by A567,A565,A577,
JORDAN6:def 10;
          0<=rz by A578,BORSUK_1:40,XXREAL_1:1;
          then h2/.j<=rz by A22,A23,A24,A25,A558,A568,A565,A564,A582,A579,A580
,Th19;
          hence z in [.h2/.j,h2/.(j+1).] & x = g2.z by A574,A579,A581,
XXREAL_1:1;
        end;
        suppose
          h0/.i in P & p=W-min(P);
          hence ex y being set st y in dom g2 & y in [.h2/.j,h2/.(j+1).] & x =
          g2.y by A25,A227,A574,A573,A576;
        end;
      end;
      hence thesis by FUNCT_1:def 6;
    end;
A583: 0 <= h2.j & h2.j <= 1 by A29,A556,BORSUK_1:40,XXREAL_1:1;
A584: g2.:([.h2/.j,h2/.(j+1).]) c= Segment(h0/.i,h0/.1,P)
    proof
A585: Upper_Arc(P) \/ Lower_Arc(P)=P by A1,JORDAN6:def 9;
      let x be set;
      assume x in g2.:([.h2/.j,h2/.(j+1).]);
      then consider y being set such that
A586: y in dom g2 and
A587: y in [.h2/.j,h2/.(j+1).] and
A588: x=g2.y by FUNCT_1:def 6;
      reconsider sy=y as Real by A587;
A589: x in Lower_Arc(P) by A23,A586,A588,FUNCT_1:def 3;
      then reconsider p1=x as Point of TOP-REAL 2;
      h2/.j<=sy & sy<=1 by A586,A587,BORSUK_1:40,XXREAL_1:1;
      then
A590: LE h0/.i,p1,Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23,A24,A25,A558
,A565,A583,A564,A588,Th18;
      now
        per cases;
        case
          p1=W-min(P);
          hence LE h0/.i,p1,P or h0/.i in P & p1=W-min(P) by A559,A565,A585,
XBOOLE_0:def 3;
        end;
        case
          p1<>W-min(P);
          hence LE h0/.i,p1,P or h0/.i in P & p1=W-min(P) by A559,A565,A589
,A590,JORDAN6:def 10;
        end;
      end;
      then
A591: x in {p: LE h0/.i,p,P or h0/.i in P & p=W-min(P)};
      h0/.1=W-min(P) by A72,A67,PARTFUN1:def 6;
      hence thesis by A591,Def1;
    end;
    assume W=Segment(h0/.len h0,h0/.1,P);
    then W=g2.:Q1 by A569,A584,XBOOLE_0:def 10;
    hence thesis by A31,A47,A36,A52,A55,A57,A554,A560,A563,Lm1;
  end;
A592: for i being Element of NAT st 1<=i & i+1<len h0 holds LE h0/.(i+1),h0
  /.(i+2),P
  proof
    let i be Element of NAT;
    assume that
A593: 1<=i and
A594: i+1<len h0;
A595: i+1+1<=len h0 by A594,NAT_1:13;
A596: i+1<i+1+1 by NAT_1:13;
A597: 1<i+1 by A593,NAT_1:13;
    then
A598: 1<i+1+1 by NAT_1:13;
    per cases;
    suppose
A599: i+1<len h1;
      then
A600: i+1 in dom h1 by A597,FINSEQ_3:25;
      then
A601: h1.(i+1) in rng h1 by FUNCT_1:def 3;
      then
A602: 0<=h1.(i+1) & h1.(i+1)<=1 by A11,BORSUK_1:40,XXREAL_1:1;
A603: 1<i+1+1 by A597,NAT_1:13;
      then (i+1)+1 in dom h0 by A595,FINSEQ_3:25;
      then
A604: h0/.(i+1+1)=h0.(i+1+1) by PARTFUN1:def 6;
A605: i+1+1<=len h1 by A599,NAT_1:13;
      then
A606: i+1+1 in dom h1 by A603,FINSEQ_3:25;
      then
A607: h1.((i+1)+1) in rng h1 by FUNCT_1:def 3;
      then
A608: h1.(i+1+1)<=1 by A11,BORSUK_1:40,XXREAL_1:1;
      h0.(i+1+1)=h11.(i+1+1) by A39,A605,A603,FINSEQ_1:64;
      then
A609: h0.(i+1+1)=g1.(h1.(i+1+1)) by A606,FUNCT_1:13;
      then
A610: h0/.(i+1+1) in Upper_Arc P by A5,A132,A11,A607,A604,BORSUK_1:40
,FUNCT_1:def 3;
      i+1 in dom h0 by A594,A597,FINSEQ_3:25;
      then
A611: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A612: h0.(i+1)=h11.(i+1) by A39,A597,A599,FINSEQ_1:64;
      then
A613: h0.(i+1)=g1.(h1.(i+1)) by A600,FUNCT_1:13;
      g1.(h1.(i+1)) in rng g1 by A132,A11,A601,BORSUK_1:40,FUNCT_1:def 3;
      then
A614: h0/.(i+1) in Upper_Arc P by A5,A612,A600,A611,FUNCT_1:13;
      h1.(i+1)<h1.(i+1+1) by A12,A596,A600,A606,SEQM_3:def 1;
      then LE h0/.(i+1),h0/.((i+1)+1),Upper_Arc(P),W-min(P),E-max(P) by A3,A4
,A5,A6,A7,A613,A602,A609,A608,A611,A604,Th18;
      hence thesis by A614,A610,JORDAN6:def 10;
    end;
    suppose
A615: i+1>=len h1;
      per cases by A615,XXREAL_0:1;
      suppose
A616:   i+1>len h1;
        set j=(i+1)-'len h11+2-'1;
A617:   (i+1)+1-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11
        by A36,A595,XREAL_1:9;
A618:   0+2<=(i+1)-'len h11 +2 by XREAL_1:6;
        then
A619:   1<=((i+1)-'len h11 +2-'1) by Lm1,NAT_D:42;
A620:   j+1=(i+1)-'len h11+(1+1)-1+1 by A618,Lm1,NAT_D:39,42
          .=(i+1)-'len h11+2;
A621:   len h1 +1<=i+1 by A616,NAT_1:13;
        then
A622:   len h1 +1-len h1<=(i+1)-len h1 by XREAL_1:9;
A623:   (i+1)-len h11=(i+1)-'len h11 by A39,A616,XREAL_1:233;
        (i+1)+1>len h11 by A39,A616,NAT_1:13;
        then
A624:   (i+1)+1-len h11=(i+1)+1-'len h11 by XREAL_1:233;
A625:   len h1 +1<=(i+1)+1 by A621,NAT_1:13;
        then
A626:   len h1 +1-len h1<=(i+1)+1-len h1 by XREAL_1:9;
        then 1<(i+1)+1-'len h11+(2-1) by A39,A624,NAT_1:13;
        then
A627:   0<(i+1)+1-'len h11+2-1;
        (i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A618,Lm1,NAT_D:39,42;
        then
A628:   j+1=(i+1)+1-'len h11+2-'1 by A623,A624,A627,XREAL_0:def 2;
        (i+1)-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57
,A594,XREAL_1:9;
        then
A629:   (i+1)-'len h11+2<=len h2-2+2 by A39,A623,XREAL_1:6;
        then ((i+1)-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
        then
A630:   j in dom h2 by A46,A619,FINSEQ_3:25;
        2-'1<=((i+1)-'len h11 +2-'1) by A618,NAT_D:42;
        then 1<j+1 by Lm1,NAT_1:13;
        then
A631:   j+1 in dom h2 by A629,A620,FINSEQ_3:25;
        then
A632:   h2.(j+1) in rng h2 by FUNCT_1:def 3;
        then
A633:   (h2.(j+1)) <= 1 by A29,BORSUK_1:40,XXREAL_1:1;
        j<j+1 by NAT_1:13;
        then
A634:   h2.j<h2.(j+1) by A30,A630,A631,SEQM_3:def 1;
A635:   i+1<=len h11 + len (mid(h21,2,len h21 -'1)) by A594,FINSEQ_1:22;
        len h11+1<=i+1 by A39,A616,NAT_1:13;
        then
A636:   h0.(i+1)=(mid(h21,2,len h21 -'1)).((i+1) -len h11) by A635,FINSEQ_1:23;
        (i+1)-len h11<=len h11 + len (mid(h21,2,len h21 -'1)) -len h11
        by A635,XREAL_1:9;
        then h0.(i+1)=h21.((i+1)-'len h11 +2-'1) by A39,A48,A56,A50,A54,A636
,A623,A622,FINSEQ_6:118;
        then
A637:   h0.(i+1)=g2.(h2.j) by A630,FUNCT_1:13;
A638:   h2.j in rng h2 by A630,FUNCT_1:def 3;
        then
A639:   h0.(i+1) in Lower_Arc(P) by A23,A131,A29,A637,BORSUK_1:40,FUNCT_1:def 3
;
        (i+1)+1 in dom h0 by A595,A598,FINSEQ_3:25;
        then
A640:   h0/.((i+1)+1)=h0.((i+1)+1) by PARTFUN1:def 6;
        h0.((i+1)+1)=(mid(h21,2,len h21 -'1)).((i+1)+1 -len h11) by A39,A36
,A595,A625,FINSEQ_1:23;
        then
A641:   h0.((i+1)+1)=h21.((i+1)+1-'len h11 +2-'1) by A39,A48,A56,A50,A54,A624
,A617,A626,FINSEQ_6:118;
        then
A642:   h0.((i+1)+1)=g2.(h2.(j+1)) by A628,A631,FUNCT_1:13;
        then
A643:   h0.((i+1)+1) in Lower_Arc(P) by A23,A131,A29,A632,BORSUK_1:40
,FUNCT_1:def 3;
        (i+1)-len h11<len h11+(len h2-2)-len h11 by A47,A36,A52,A55,A57,A594,
XREAL_1:9;
        then (i+1)-len h11+2<len h2-2+2 by XREAL_1:6;
        then
A644:   h0/.(i+1+1) <> W-min P by A46,A34,A35,A32,A623,A641,A620,A628,A631,A640
,FUNCT_1:def 4;
        i+1 in dom h0 by A594,A597,FINSEQ_3:25;
        then
A645:   h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
        0<=h2.j & h2.j<=1 by A29,A638,BORSUK_1:40,XXREAL_1:1;
        then LE h0/.(i+1),h0/.((i+1)+1),Lower_Arc(P),E-max(P),W-min(P) by A21
,A22,A23,A24,A25,A637,A642,A634,A645,A640,A633,Th18;
        hence thesis by A645,A640,A639,A643,A644,JORDAN6:def 10;
      end;
      suppose
A646:   i+1=len h1;
        then len h1+1 <=len h11 + len (mid(h21,2,len h21 -'1)) by A595,
FINSEQ_1:22;
        then
A647:   (i+1)+1-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11
        by A646,XREAL_1:9;
        then 1<=(i+1)+1-'len h11 by A39,A596,A646,XREAL_1:233;
        then 1<(i+1)+1-'len h11+(2-1) by NAT_1:13;
        then
A648:   0<(i+1)+1-'len h11+2-1;
A649:   (i+1)+1-len h11=(i+1)+1-'len h11 by A39,A596,A646,XREAL_1:233;
        len h1 in dom h0 by A594,A597,A646,FINSEQ_3:25;
        then
A650:   h0/.len h1=h0.len h1 by PARTFUN1:def 6;
        set j=(i+1)-'len h11+2-'1;
A651:   0+2<=(i+1)-'len h11 +2 by XREAL_1:6;
        then
A652:   j+1=(i+1)-'len h11+(1+1)-1+1 by Lm1,NAT_D:39,42
          .=(i+1)-'len h11+(1+1);
        2-'1<=((i+1)-'len h11 +2-'1) by A651,NAT_D:42;
        then
A653:   1<j+1 by Lm1,NAT_1:13;
        len h1-len h11=len h1-'len h11 & (i+1)-len h11<=len h1+(len h2-2
        )-len h11 by A39,A47,A36,A52,A55,A57,A594,XREAL_1:9,233;
        then (i+1)-'len h11+2<=len h2-2+2 by A39,A646,XREAL_1:6;
        then
A654:   j+1 in dom h2 by A652,A653,FINSEQ_3:25;
        then
A655:   h2.(j+1) in rng h2 by FUNCT_1:def 3;
        h0.len h1 =E-max(P) by A39,A255,A597,A646,FINSEQ_1:64;
        then
A656:   h0.(i+1) in Upper_Arc(P) by A1,A646,Th1;
        (i+1)+1 in dom h0 by A595,A598,FINSEQ_3:25;
        then
A657:   h0/.((i+1)+1)=h0.((i+1)+1) by PARTFUN1:def 6;
        h0.((i+1)+1)=(mid(h21,2,len h21 -'1)).((i+1)+1 -len h11) by A39,A36
,A595,A646,FINSEQ_1:23;
        then
A658:   h0.((i+1)+1)=h21.((i+1)+1-'len h11 +2-'1) by A39,A48,A56,A50,A54,A646
,A649,A647,FINSEQ_6:118;
A659:   j+1=(i+1)-len h11+2-1+1 by A39,A646,Lm1,XREAL_0:def 2
          .=(i+1)+1-'len h11+2-'1 by A649,A648,XREAL_0:def 2;
        then h0.((i+1)+1)=g2.(h2.(j+1)) by A658,A654,FUNCT_1:13;
        then
A660:   h0.(i+1+1) in Lower_Arc P by A23,A131,A29,A655,BORSUK_1:40
,FUNCT_1:def 3;
        (i+1)-len h11<len h11+(len h2-2)-len h11 by A47,A36,A52,A55,A57,A594,
XREAL_1:9;
        then (i+1)-len h11+2<len h2-2+2 by XREAL_1:6;
        then j+1<len h2 by A39,A646,A652,XREAL_0:def 2;
        then h0/.(i+1+1) <> W-min P by A46,A34,A35,A32,A658,A659,A654,A657,
FUNCT_1:def 4;
        hence thesis by A646,A650,A657,A660,A656,JORDAN6:def 10;
      end;
    end;
  end;
  thus for i being Element of NAT st 1<=i & i+1<len h0 holds Segment(h0/.i,h0
  /.(i+1),P)/\ Segment(h0/.(i+1),h0/.(i+2),P) ={h0/.(i+1)}
  proof
    let i be Element of NAT;
    assume
A661: 1<=i & i+1<len h0;
    then
A662: LE h0/.i,h0/.(i+1),P & h0/.(i+1)<>W-min(P) by A256;
    h0/.i<>h0/.(i+1) & LE h0/.(i+1),h0/.(i+2),P by A592,A256,A661;
    hence thesis by A1,A662,Th10;
  end;
A663: 2 in dom h0 by A201,FINSEQ_3:25;
  i <> 1 by A59,Lm2;
  then
A664: h0/.i <> h0/.1 by A67,A78,A203,PARTFUN2:10;
A665: len h1 in dom h1 by A16,FINSEQ_3:25;
  thus Segment(h0/.len h0,h0/.1,P)/\ Segment(h0/.1,h0/.2,P)={h0/.1}
  proof
    defpred P[Element of NAT] means $1+2<=len h0 implies LE h0/.2,h0/.($1+2),P;
    set j=len h0-'len h11+2-'1;
A666: len h0 -len h11 <=len h11 + len mid(h21,2,len h21 -'1) -len h11 by
FINSEQ_1:22;
A667: h0/.2=h0.2 by A663,PARTFUN1:def 6;
A668: for k being Element of NAT st P[k] holds P[k+1]
    proof
      let k be Element of NAT;
      assume
A669: k+2<=len h0 implies LE h0/.2,h0/.(k+2),P;
      now
A670:   k+1+1=k+2;
A671:   k+1+2=k+2+1;
        assume
A672:   k+1+2<=len h0;
        then k+2<len h0 by A671,NAT_1:13;
        then LE h0/.(k+2),h0/.(k+2+1),P by A592,A671,A670,NAT_1:11;
        hence LE h0/.2,h0/.(k+1+2),P by A1,A669,A672,JORDAN6:58,NAT_1:13;
      end;
      hence thesis;
    end;
    len h0 -'2=len h0-2 by A65,A14,XREAL_1:233,XXREAL_0:2;
    then
A673: len h0-'2+2=len h0;
    0+2<=len h0-'len h11 +2 by XREAL_1:6;
    then
A674: 1<=(len h0-'len h11 +2-'1) by Lm1,NAT_D:42;
    (len h0-'len h11 +2-'1)<=len h21 by A36,A52,A55,A57,A252,NAT_D:44;
    then
A675: j in dom h2 by A46,A674,FINSEQ_3:25;
    h0.2=g1.(h1.2) & h1.2 in rng h1 by A15,A40,FUNCT_1:13,def 3;
    then
A676: h0/.2 in Upper_Arc P by A5,A132,A11,A667,BORSUK_1:40,FUNCT_1:def 3;
    Upper_Arc(P) \/ Lower_Arc(P)= P by A1,JORDAN6:50;
    then h0/.2 in P by A676,XBOOLE_0:def 3;
    then
A677: P[0] by A1,JORDAN6:56;
A678: for i being Element of NAT holds P[i] from NAT_1:sch 1(A677,A668);
A679: h11.2 <> W-min(P) by A38,A17,A71,A15,A20,FUNCT_1:def 4;
    len h1 +1-len h1<=len h0 -len h1 & h0.len h0=(mid(h21,2,len h21 -'1)
    ).(len h0 -len h11) by A39,A36,A549,A62,A64,FINSEQ_1:23,XXREAL_0:2;
    then h0.len h0=h21.(len h0-'len h11 +2-'1) by A39,A48,A56,A50,A54,A252,A666
,FINSEQ_6:118;
    then
A680: h0.len h0=g2.(h2.j) by A675,FUNCT_1:13;
A681: now
      h2.j in rng h2 by A675,FUNCT_1:def 3;
      then
A682: g2.(h2.j) in rng g2 by A131,A29,BORSUK_1:40,FUNCT_1:def 3;
      assume h0/.2=h0/.len h0;
      then h0/.2 in Upper_Arc(P)/\ Lower_Arc(P) by A23,A75,A676,A680,A682,
XBOOLE_0:def 4;
      then h0/.2 in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
      then h11.2=E-max(P) by A40,A679,A667,TARSKI:def 2;
      hence contradiction by A38,A665,A255,A14,A15,A20,FUNCT_1:def 4;
    end;
    h0/.2<>W-min(P) by A663,A40,A679,PARTFUN1:def 6;
    hence thesis by A1,A73,A681,A678,A673,Th12;
  end;
A683: i+1 = len h0 by A16,A65,XREAL_1:235,XXREAL_0:2;
  then LE h0/.i,h0/.(i+1),P & h0/.(i+1)<>W-min(P) by A256,A202;
  hence Segment(h0/.i,h0/.len h0,P)/\ Segment(h0/.len h0,h0/.1,P)={h0/.len h0}
  by A1,A73,A683,A664,Th11;
  LE h0/.i,h0/.(i+1),P by A256,A202,A200;
  hence Segment(h0/.i,h0/.len h0,P) misses Segment(h0/.1,h0/.2,P) by A1,A683
,A333,A229,A207,Th13;
  thus for i,j being Element of NAT st 1<=i & i < j & j < len h0 & not i,j
are_adjacent1 holds Segment(h0/.i,h0/.(i+1),P) misses Segment(h0/.j,h0/.(j+1),P
  )
  proof
    let i,j be Element of NAT;
    assume that
A684: 1<=i and
A685: i < j and
A686: j < len h0 and
A687: not i,j are_adjacent1;
A688: 1<j by A684,A685,XXREAL_0:2;
    i<len h0 by A685,A686,XXREAL_0:2;
    then
A689: i+1<=len h0 by NAT_1:13;
    then
A690: LE h0/.i,h0/.(i+1),P & h0/.i<>h0/.(i+1) by A256,A684;
A691: i+1<=j by A685,NAT_1:13;
    then
A692: (i+1)<len h0 by A686,XXREAL_0:2;
A693: not j=i+1 by A687,GOBRD10:def 1;
    then
A694: i+1<j by A691,XXREAL_0:1;
A695: now
      assume
A696: h0/.(i+1)=h0/.j;
      per cases;
      suppose
A697:   i+1<=len h1;
A698:   1<i+1 by A684,NAT_1:13;
        then
A699:   i+1 in dom h1 by A697,FINSEQ_3:25;
        then
A700:   h1.(i+1) in rng h1 by FUNCT_1:def 3;
        i+1 in dom h0 by A689,A698,FINSEQ_3:25;
        then
A701:   h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A702:   h0.(i+1)=h11.(i+1) by A39,A697,A698,FINSEQ_1:64;
        then h0.(i+1)=g1.(h1.(i+1)) by A699,FUNCT_1:13;
        then
A703:   h0.(i+1) in Upper_Arc(P) by A5,A132,A11,A700,BORSUK_1:40,FUNCT_1:def 3;
        per cases;
        suppose
A704:     j<=len h1;
          j in dom h0 by A686,A688,FINSEQ_3:25;
          then
A705:     h0/.j=h0.j by PARTFUN1:def 6;
          h0.(j)=h11.(j) & j in dom h1 by A39,A688,A704,FINSEQ_1:64,FINSEQ_3:25
;
          hence contradiction by A38,A20,A693,A696,A699,A701,A702,A705,
FUNCT_1:def 4;
        end;
        suppose
A706:     j>len h1;
          j in dom h0 by A686,A688,FINSEQ_3:25;
          then
A707:     h0/.j=h0.j by PARTFUN1:def 6;
A708:     j-len h11=j-'len h11 by A39,A706,XREAL_1:233;
          j-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A686,
XREAL_1:9;
          then j-'len h11+2<=len h2-2+2 by A39,A708,XREAL_1:6;
          then
A709:     (j-'len h11 +2-'1)<= len h21 by A47,NAT_D:44;
          j-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A686,
XREAL_1:9;
          then
A710:     j-'len h11+2<=len h2-2+2 by A39,A708,XREAL_1:6;
          set k=j-'len h11+2-'1;
          j<= len h11 + len (mid(h21,2,len h21 -'1)) by A686,FINSEQ_1:22;
          then
A711:     j-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by
XREAL_1:9;
A712:     0+2<=j-'len h11 +2 by XREAL_1:6;
          then
A713:     j-'len h11+2-'1=j-'len h11+2-1 by Lm1,NAT_D:39,42;
          1<=(j-'len h11 +2-'1) by A712,Lm1,NAT_D:42;
          then
A714:     k in dom h2 by A46,A709,FINSEQ_3:25;
          then h2.k in rng h2 by FUNCT_1:def 3;
          then
A715:     g2.(h2.k) in rng g2 by A131,A29,BORSUK_1:40,FUNCT_1:def 3;
A716:     len h1 +1<=j by A706,NAT_1:13;
          then h0.j=(mid(h21,2,len h21 -'1)).(j -len h11) & len h1 +1-len h1
          <=j-len h1 by A39,A36,A686,FINSEQ_1:23,XREAL_1:9;
          then
A717:     h0.j=h21.(j-'len h11 +2-'1) by A39,A48,A56,A50,A54,A708,A711,
FINSEQ_6:118;
          then h0.j=g2.(h2.k) by A714,FUNCT_1:13;
          then h0.j in Upper_Arc(P) /\ Lower_Arc(P) by A23,A696,A701,A703,A707
,A715,XBOOLE_0:def 4;
          then
A718:     h0.j in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
          len h11+1-len h11<=j-len h11 by A39,A716,XREAL_1:9;
          then 1<=j-'len h11 by NAT_D:39;
          then 1+2<=j-'len h11+2 by XREAL_1:6;
          then 1+2-1<=j-'len h11+2-1 by XREAL_1:9;
          then 1<k by A713,XXREAL_0:2;
          then
A719:     h0.j <> E-max P by A46,A76,A77,A32,A717,A714,FUNCT_1:def 4;
          j-'len h11+2-'1<j-'len h11+2-'1+1 by NAT_1:13;
          then h0.j <> W-min P by A46,A34,A35,A32,A717,A713,A710,A714,
FUNCT_1:def 4;
          hence contradiction by A718,A719,TARSKI:def 2;
        end;
      end;
      suppose
A720:   i+1>len h1;
        then
A721:   j>len h1 by A691,XXREAL_0:2;
        then
A722:   len h1 +1<=j by NAT_1:13;
        then
A723:   len h1 +1-len h1<=j-len h1 by XREAL_1:9;
        len h11+1-len h11<=j-len h11 by A39,A722,XREAL_1:9;
        then
A724:   j-'len h11=j-len h11 by NAT_D:39;
A725:   len h1 +1<=i+1 by A720,NAT_1:13;
        then len h11+1-len h11<=(i+1)-len h11 by A39,XREAL_1:9;
        then (i+1)-'len h11=(i+1)-len h11 by NAT_D:39;
        then i+1-'len h11<j-'len h11 by A694,A724,XREAL_1:9;
        then
A726:   i+1-'len h11+2<j-'len h11+2 by XREAL_1:6;
        set k=j-'len h11+2-'1;
        set j0=(i+1)-'len h11+2-'1;
A727:   j<= len h11 + len (mid(h21,2,len h21 -'1)) by A686,FINSEQ_1:22;
A728:   (i+1)-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11
        by A36,A689,XREAL_1:9;
A729:   j-len h11=j-'len h11 by A39,A691,A720,XREAL_1:233,XXREAL_0:2;
        j-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A686,
XREAL_1:9;
        then j-'len h11+2<=len h2-2+2 by A39,A729,XREAL_1:6;
        then
A730:   (j-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
A731:   0+2<=j-'len h11 +2 by XREAL_1:6;
        then
A732:   j-'len h11+2-'1=j-'len h11+2-1 by Lm1,NAT_D:39,42;
        1<=(j-'len h11 +2-'1) by A731,Lm1,NAT_D:42;
        then
A733:   k in dom h2 by A46,A730,FINSEQ_3:25;
A734:   (i+1)-len h11=(i+1)-'len h11 by A39,A720,XREAL_1:233;
        len h11+1<=j by A39,A721,NAT_1:13;
        then
A735:   h0.j=(mid(h21,2,len h21 -'1)).(j -len h11) by A727,FINSEQ_1:23;
        j-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A686,
XREAL_1:9;
        then
A736:   h0.j=h21.(j-'len h11 +2-'1) by A39,A48,A56,A50,A54,A735,A729,A723,
FINSEQ_6:118;
        1<=i+1 by A684,NAT_1:13;
        then i+1 in dom h0 by A689,FINSEQ_3:25;
        then
A737:   h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
        j in dom h0 by A686,A688,FINSEQ_3:25;
        then
A738:   h0/.j=h0.j by PARTFUN1:def 6;
        (i+1)-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57
,A689,XREAL_1:9;
        then (i+1)-'len h11+2<=len h2-2+2 by A39,A734,XREAL_1:6;
        then
A739:   ((i+1)-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
A740:   0+2<=(i+1)-'len h11 +2 by XREAL_1:6;
        then 1<=((i+1)-'len h11 +2-'1) by Lm1,NAT_D:42;
        then
A741:   j0 in dom h2 by A46,A739,FINSEQ_3:25;
        (i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A740,Lm1,NAT_D:39,42;
        then
A742:   (i+1)-'len h11+2-'1<j-'len h11+2-'1 by A732,A726,XREAL_1:9;
        h0.(i+1)=(mid(h21,2,len h21 -'1)).((i+1) -len h11) & len h1 +1-
        len h1<=(i+1) -len h1 by A39,A36,A689,A725,FINSEQ_1:23,XREAL_1:9;
        then h0.(i+1)=h21.((i+1)-'len h11 +2-'1) by A39,A48,A56,A50,A54,A734
,A728,FINSEQ_6:118;
        hence contradiction by A46,A32,A696,A741,A737,A736,A742,A733,A738,
FUNCT_1:def 4;
      end;
    end;
A743: j+1<=len h0 by A686,NAT_1:13;
A744: 1<i+1 by A684,NAT_1:13;
A745: 1<=(i+1) by A684,NAT_1:13;
A746: i+1<len h0 by A686,A691,XXREAL_0:2;
A747: LE h0/.(i+1),h0/.j,P
    proof
      per cases;
      suppose
A748:   i+1<=len h1;
        per cases;
        suppose
A749:     j<=len h1;
A750:     1<j by A694,A745,XXREAL_0:2;
          then
A751:     j in dom h1 by A749,FINSEQ_3:25;
          then
A752:     h1.j in rng h1 by FUNCT_1:def 3;
          then
A753:     (h1.j) <= 1 by A11,BORSUK_1:40,XXREAL_1:1;
          j in dom h0 by A686,A750,FINSEQ_3:25;
          then
A754:     h0/.j=h0.j by PARTFUN1:def 6;
          h0.j=h11.j by A39,A749,A750,FINSEQ_1:64;
          then
A755:     g1.(h1.j) = h0/.j by A751,A754,FUNCT_1:13;
          then
A756:     h0/.j in Upper_Arc(P) by A5,A132,A11,A752,BORSUK_1:40,FUNCT_1:def 3;
          i+1 in dom h0 by A745,A692,FINSEQ_3:25;
          then
A757:     h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A758:     Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:def 8;
A759:     (i+1) in dom h1 by A745,A748,FINSEQ_3:25;
          then
A760:     h1.(i+1) in rng h1 by FUNCT_1:def 3;
          then
A761:     0 <= (h1.(i+1)) & (h1.(i+1)) <= 1 by A11,BORSUK_1:40,XXREAL_1:1;
          h0.(i+1)=h11.(i+1) by A39,A745,A748,FINSEQ_1:64;
          then
A762:     g1.(h1.(i+1)) = h0/.(i+1) by A759,A757,FUNCT_1:13;
          then
A763:     h0/.(i+1) in Upper_Arc(P) by A5,A132,A11,A760,BORSUK_1:40
,FUNCT_1:def 3;
          (h1.(i+1)) <= (h1.j) by A12,A694,A759,A751,SEQM_3:def 1;
          then LE h0/.(i+1),h0/.j,Upper_Arc(P),W-min(P),E-max(P) by A4,A5,A6,A7
,A758,A762,A761,A755,A753,Th18;
          hence thesis by A763,A756,JORDAN6:def 10;
        end;
        suppose
A764:     j>len h1;
          set k=j-'len h11+2-'1;
          0+2<=j-'len h11 +2 by XREAL_1:6;
          then
A765:     2-'1<=j-'len h11 +2-'1 by NAT_D:42;
A766:     j-len h11=j-'len h11 by A39,A764,XREAL_1:233;
          j-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A686,
XREAL_1:9;
          then j-'len h11+2<=len h2-2+2 by A39,A766,XREAL_1:6;
          then (j-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
          then
A767:     (j-'len h11 +2-'1) in dom h21 by A765,Lm1,FINSEQ_3:25;
          j+1-1<=len h1+(len h2-2)-1 by A39,A47,A36,A52,A55,A57,A743,XREAL_1:9
;
          then j-len h11<=len h1+((len h2-2)-1)-len h11 by XREAL_1:9;
          then j-'len h11+2<=len h2-2-1+2 by A39,A766,XREAL_1:6;
          then
A768:     j-'len h11+2-1<=len h2-1-1 by XREAL_1:9;
A769:     h0.(i+1)=h11.(i+1) by A39,A744,A748,FINSEQ_1:64;
          i+1 in dom h1 by A744,A748,FINSEQ_3:25;
          then h1.(i+1) in rng h1 by FUNCT_1:def 3;
          then
A770:     g1.(h1.(i+1)) in rng g1 by A132,A11,BORSUK_1:40,FUNCT_1:def 3;
          0+1<=j-'len h11+1+1-1 by XREAL_1:6;
          then
A771:     j-'len h11+2-'1=j-'len h11+2-1 by NAT_D:39;
          len h1 +1<=j by A764,NAT_1:13;
          then
A772:     h0.j=(mid(h21,2,len h21 -'1)).(j -len h11) & len h1 +1-len h1
          <=j-len h1 by A39,A36,A686,FINSEQ_1:23,XREAL_1:9;
A773:     j-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36
,A686,XREAL_1:9;
          then h0.j=h21.(j-'len h11 +2-'1) by A39,A48,A56,A50,A54,A766,A772,
FINSEQ_6:118;
          then
A774:     h0.j=g2.(h2.k) by A46,A767,FUNCT_1:13;
          j-len h11=j-'len h11 by A39,A764,XREAL_1:233;
          then
A775:     h0.j=h21.k by A39,A48,A56,A50,A54,A773,A772,FINSEQ_6:118;
          j in dom h0 by A686,A688,FINSEQ_3:25;
          then
A776:     h0/.j=h0.j by PARTFUN1:def 6;
          h2.k in rng h2 by A46,A767,FUNCT_1:def 3;
          then
A777:     h0.j in Lower_Arc(P) by A23,A131,A29,A774,BORSUK_1:40,FUNCT_1:def 3;
          i+1 in Seg len h1 by A745,A748,FINSEQ_1:1;
          then i+1 in dom h1 by FINSEQ_1:def 3;
          then
A778:     h11.(i+1)=g1.(h1.(i+1)) by FUNCT_1:13;
          (i+1) in dom h0 by A745,A692,FINSEQ_3:25;
          then
A779:     h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
          len h2-1-1<len h2 by Lm4;
          then h0/.j <> W-min P by A46,A34,A35,A32,A771,A767,A768,A775,A776,
FUNCT_1:def 4;
          hence thesis by A5,A769,A778,A779,A776,A770,A777,JORDAN6:def 10;
        end;
      end;
      suppose
A780:   i+1>len h1;
        set j0=(i+1)-'len h11+2-'1;
        set k=j-'len h11+2-'1;
A781:   0+2<=(i+1)-'len h11 +2 by XREAL_1:6;
        then
A782:   1<=((i+1)-'len h11 +2-'1) by Lm1,NAT_D:42;
A783:   j-len h11=j-'len h11 by A39,A691,A780,XREAL_1:233,XXREAL_0:2;
        len h1<j by A691,A780,XXREAL_0:2;
        then
A784:   len h11+1<=j by A39,NAT_1:13;
        then
A785:   len h1 +1-len h1<=j-len h1 by A39,XREAL_1:9;
        j<=len h11 + len (mid(h21,2,len h21 -'1)) by A686,FINSEQ_1:22;
        then
A786:   h0.j=(mid(h21,2,len h21 -'1)).(j -len h11) by A784,FINSEQ_1:23;
A787:   i+1-len h11<len h11 + len (mid(h21,2,len h21 -'1)) - len h11 by A36
,A746,XREAL_1:9;
        then j-len h11 <= len (mid(h21,2,len h21 -'1)) by A36,A686,XREAL_1:9;
        then
A788:   h0.j=h21.(k) by A39,A48,A56,A50,A54,A783,A786,A785,FINSEQ_6:118;
A789:   (i+1)-len h11=(i+1)-'len h11 by A39,A780,XREAL_1:233;
        then (i+1)-'len h11+2<=len h2-2+2 by A47,A52,A55,A57,A787,XREAL_1:6;
        then ((i+1)-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
        then
A790:   j0 in dom h2 by A46,A782,FINSEQ_3:25;
        then
A791:   h2.j0 in rng h2 by FUNCT_1:def 3;
        then
A792:   0<=h2.j0 & h2.j0<=1 by A29,BORSUK_1:40,XXREAL_1:1;
A793:   g2.(h2.j0) in rng g2 by A131,A29,A791,BORSUK_1:40,FUNCT_1:def 3;
A794:   j-len h11=j-'len h11 by A39,A691,A780,XREAL_1:233,XXREAL_0:2;
        j+1-1<=len h1+(len h2-2)-1 by A39,A47,A36,A52,A55,A57,A743,XREAL_1:9;
        then j-len h11<=len h1+((len h2-2)-1)-len h11 by XREAL_1:9;
        then j-'len h11+2<=len h2-2-1+2 by A39,A794,XREAL_1:6;
        then
A795:   j-'len h11+2-1<=len h2-1-1 by XREAL_1:9;
        0+1<=j-'len h11+1+1-1 by XREAL_1:6;
        then
A796:   j-'len h11+2-'1=j-'len h11+2-1 by NAT_D:39;
        j-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A686,
XREAL_1:9;
        then j-'len h11+2<=len h2-2+2 by A39,A794,XREAL_1:6;
        then
A797:   (j-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
        0+2<=j-'len h11 +2 by XREAL_1:6;
        then 2-'1<=j-'len h11 +2-'1 by NAT_D:42;
        then
A798:   j-'len h11 +2-'1 in dom h21 by A797,Lm1,FINSEQ_3:25;
        then
A799:   h2.k in rng h2 by A46,FUNCT_1:def 3;
        then
A800:   h2.k<=1 by A29,BORSUK_1:40,XXREAL_1:1;
        j-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A686,
XREAL_1:9;
        then
A801:   h0.j=h21.(j-'len h11 +2-'1) by A39,A48,A56,A50,A54,A794,A786,A785,
FINSEQ_6:118;
        then h0.j=g2.(h2.k) by A46,A798,FUNCT_1:13;
        then
A802:   h0.(j) in Lower_Arc(P) by A23,A131,A29,A799,BORSUK_1:40,FUNCT_1:def 3;
A803:   (i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A781,Lm1,NAT_D:39,42;
A804:   i+1<len h11 + len (mid(h21,2,len h21 -'1)) by A746,FINSEQ_1:22;
        (i+1)-len h11<j-len h11 by A694,XREAL_1:9;
        then (i+1)-'len h11+2<j-'len h11+2 by A783,A789,XREAL_1:6;
        then j0<k by A796,A803,XREAL_1:9;
        then
A805:   h2.(j0)<h2.(k) by A30,A46,A798,A790,SEQM_3:def 1;
        (i+1) in dom h0 by A745,A692,FINSEQ_3:25;
        then
A806:   h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
        len h1+1<=i+1 by A780,NAT_1:13;
        then
A807:   len h1+1-len h1<=i+1-len h1 by XREAL_1:9;
        then
A808:   i+1-'len h11=i+1-len h11 by A39,NAT_D:39;
        j in dom h0 by A686,A688,FINSEQ_3:25;
        then
A809:   h0/.j=h0.(j) by PARTFUN1:def 6;
        len h11+1<=i+1 by A39,A780,NAT_1:13;
        then h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A804,
FINSEQ_1:23
          .=h21.(i+1-'len h11+2-'1) by A39,A48,A56,A50,A54,A787,A807,A808,
FINSEQ_6:118;
        then
A810:   h0.(i+1)=g2.(h2.j0) by A790,FUNCT_1:13;
        len h2-1-1<len h2 by Lm4;
        then
A811:   h0/.j <> W-min P by A46,A34,A35,A32,A796,A798,A795,A788,A809,
FUNCT_1:def 4;
        h21.k=g2.(h2.k) by A46,A798,FUNCT_1:13;
        then LE h0/.(i+1),h0/.j,Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23
,A24,A25,A801,A800,A810,A792,A805,A806,A809,Th18;
        hence thesis by A23,A810,A806,A809,A793,A802,A811,JORDAN6:def 10;
      end;
    end;
    LE h0/.j,h0/.(j+1),P by A256,A688,A743;
    hence thesis by A1,A690,A747,A695,Th13;
  end;
  let i be Element of NAT such that
A812: 1 < i and
A813: i+1 < len h0;
A814: 1<i+1 by A812,NAT_1:13;
  then
A815: i+1 in dom h0 by A813,FINSEQ_3:25;
A816: 1<=len h0-len h1 by A549,A62,XXREAL_0:2;
A817: now
    assume
A818: h0/.(i+1)=h0/.len h0;
    per cases;
    suppose
A819: i+1<=len h1;
      then
A820: i+1 in dom h1 by A814,FINSEQ_3:25;
      h0.(i+1)=h11.(i+1) by A39,A814,A819,FINSEQ_1:64;
      then
A821: h0.(i+1)=g1.(h1.(i+1)) by A820,FUNCT_1:13;
      h1.(i+1) in rng h1 by A820,FUNCT_1:def 3;
      then
A822: h0.(i+1) in Upper_Arc(P) by A5,A132,A11,A821,BORSUK_1:40,FUNCT_1:def 3;
      i+1 in dom h0 by A813,A814,FINSEQ_3:25;
      then
A823: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
      1+2<=len h0-'len h11+2 by A47,A36,A52,A55,A57,A63,A252,XREAL_1:6;
      then
A824: 1+2-1<=len h0-'len h11+2-1 by XREAL_1:9;
      set k=len h0-'len h11+2-'1;
A825: 0+2<=len h0-'len h11 +2 by XREAL_1:6;
      then
A826: 2-'1<=(len h0-'len h11 +2-'1) by NAT_D:42;
      len h0-'len h11 +2-'1 <= len h21 by A36,A52,A55,A57,A252,NAT_D:44;
      then
A827: k in dom h2 by A46,A826,Lm1,FINSEQ_3:25;
      then h2.k in rng h2 by FUNCT_1:def 3;
      then
A828: g2.(h2.k) in rng g2 by A131,A29,BORSUK_1:40,FUNCT_1:def 3;
      h0.len h0=(mid(h21,2,len h21 -'1)).(len h0 -len h11) by A39,A36,A64,
FINSEQ_1:23;
      then
A829: h0.len h0=h21.(len h0-'len h11 +2-'1) by A39,A36,A48,A56,A50,A54,A816
,A252,FINSEQ_6:118;
      then h0.len h0=g2.(h2.k) by A827,FUNCT_1:13;
      then h0.len h0 in Upper_Arc(P) /\ Lower_Arc(P) by A23,A75,A818,A823,A822
,A828,XBOOLE_0:def 4;
      then
A830: h0.len h0 in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
      len h0-'len h11+2-'1=len h0-'len h11+2-1 by A825,Lm1,NAT_D:39,42;
      then 1<k by A824,XXREAL_0:2;
      then
A831: h0.len h0 <> E-max P by A46,A76,A77,A32,A829,A827,FUNCT_1:def 4;
      len h0-'len h11+2-'1<len h0-'len h11+2-'1+1 by NAT_1:13;
      then h0.len h0 <> W-min P by A46,A47,A34,A35,A36,A52,A55,A57,A252,A32
,A829,A827,FUNCT_1:def 4;
      hence contradiction by A830,A831,TARSKI:def 2;
    end;
    suppose
A832: i+1>len h1;
      set k=len h0-'len h11+2-'1;
      set j0=(i+1)-'len h11+2-'1;
A833: 0+2<=len h0-'len h11 +2 by XREAL_1:6;
      then
A834: 2-'1<=(len h0-'len h11 +2-'1) by NAT_D:42;
      len h0-'len h11 +2-'1 <= len h21 by A36,A52,A55,A57,A252,NAT_D:44;
      then
A835: k in dom h2 by A46,A834,Lm1,FINSEQ_3:25;
      i+1 <= len h11 + len mid(h21,2,len h21 -'1) by A813,FINSEQ_1:22;
      then
A836: i+1-len h11 <=len h11 + len mid(h21,2,len h21 -'1)-len h11 by XREAL_1:9;
A837: len h1 +1<=i+1 by A832,NAT_1:13;
      then len h11+1-len h11<=(i+1)-len h11 by A39,XREAL_1:9;
      then
A838: (i+1)-'len h11=(i+1)-len h11 by NAT_D:39;
      len h0-'len h11=len h0-len h11 by A36,A57,XREAL_0:def 2;
      then i+1-'len h11<len h0-'len h11 by A813,A838,XREAL_1:9;
      then
A839: i+1-'len h11+2<len h0-'len h11+2 by XREAL_1:6;
      1<=i+1 by A812,NAT_1:13;
      then i+1 in dom h0 by A813,FINSEQ_3:25;
      then
A840: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A841: len h0-'len h11+2-'1=len h0-'len h11+2-1 by A833,Lm1,NAT_D:39,42;
A842: (i+1)-len h11=(i+1)-'len h11 by A39,A832,XREAL_1:233;
      (i+1)-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A813,
XREAL_1:9;
      then (i+1)-'len h11+2<=len h2-2+2 by A39,A842,XREAL_1:6;
      then
A843: (i+1)-'len h11 +2-'1 <= len h21 by A47,NAT_D:44;
A844: 0+2<=(i+1)-'len h11 +2 by XREAL_1:6;
      then 2-'1<=((i+1)-'len h11 +2-'1) by NAT_D:42;
      then
A845: j0 in dom h2 by A46,A843,Lm1,FINSEQ_3:25;
      h0.(i+1)=(mid(h21,2,len h21 -'1)).((i+1) -len h11) & len h1 +1-
      len h1<=(i+1) -len h1 by A39,A36,A813,A837,FINSEQ_1:23,XREAL_1:9;
      then
A846: h0.(i+1)=h21.((i+1)-'len h11 +2-'1) by A39,A48,A56,A50,A54,A842,A836,
FINSEQ_6:118;
      (i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A844,Lm1,NAT_D:39,42;
      then
A847: (i+1)-'len h11+2-'1<k by A841,A839,XREAL_1:9;
      h0.len h0=(mid(h21,2,len h21 -'1)).(len h0 -len h11) by A39,A36,A64,
FINSEQ_1:23;
      then h0.len h0=h21.(len h0-'len h11 +2-'1) by A47,A36,A51,A52,A49,A48,A53
,A55,A57,A63,A252,FINSEQ_6:118;
      hence contradiction by A46,A75,A32,A818,A846,A845,A840,A847,A835,
FUNCT_1:def 4;
    end;
  end;
  h0.len h0=mid(h21,2,len h21 -'1).(len h0 -len h11) by A39,A36,A64,FINSEQ_1:23
;
  then
A848: h0.len h0=h21.(len h0-'len h11 +2-'1) by A39,A36,A48,A56,A50,A54,A816
,A252,FINSEQ_6:118;
  then
A849: h0.len h0 in Lower_Arc(P) by A23,A131,A29,A253,BORSUK_1:40,FUNCT_1:def 3;
A850: LE h0/.(i+1),h0/.len h0,P
  proof
    per cases;
    suppose
A851: i+1<=len h1;
      then i+1 in dom h1 by A814,FINSEQ_3:25;
      then h1.(i+1) in rng h1 by FUNCT_1:def 3;
      then
A852: g1.(h1.(i+1)) in rng g1 by A132,A11,BORSUK_1:40,FUNCT_1:def 3;
A853: h0/.(i+1)=h0.(i+1) by A815,PARTFUN1:def 6;
      i+1 in dom h1 by A814,A851,FINSEQ_3:25;
      then
A854: h11.(i+1)=g1.(h1.(i+1)) by FUNCT_1:13;
      h0.(i+1)=h11.(i+1) by A39,A814,A851,FINSEQ_1:64;
      hence thesis by A5,A75,A130,A849,A854,A853,A852,JORDAN6:def 10;
    end;
    suppose
A855: i+1>len h1;
      then len h1+1<=i+1 by NAT_1:13;
      then
A856: len h1+1-len h1<=i+1-len h1 by XREAL_1:9;
      then
A857: i+1-'len h11=i+1-len h11 by A39,NAT_D:39;
A858: i+1-len h11<len h11 + len (mid(h21,2,len h21 -'1)) - len h11 by A36,A813,
XREAL_1:9;
A859: i+1<len h11 + len (mid(h21,2,len h21 -'1)) by A813,FINSEQ_1:22;
      len h11+1<=i+1 by A39,A855,NAT_1:13;
      then
A860: h0.(i+1) = mid(h21,2,len h21 -'1).(i+1 -len h11) by A859,FINSEQ_1:23
        .= h21.(i+1-'len h11+2-'1) by A39,A48,A56,A50,A54,A858,A856,A857,
FINSEQ_6:118;
      set j0=(i+1)-'len h11+2-'1;
      set k=len h0-'len h11+2-'1;
      0+1<=len h0-'len h11+1+1-1 by XREAL_1:6;
      then
A861: len h0-'len h11+2-'1=len h0-'len h11+2-1 by NAT_D:39;
A862: (len h0-'len h11 +2-'1)<=len h21 by A36,A52,A55,A57,A252,NAT_D:44;
      then
A863: (len h0-'len h11 +2-'1) in dom h21 by A43,Lm1,FINSEQ_3:25;
      then h2.k in rng h2 by A46,FUNCT_1:def 3;
      then
A864: h2.k<=1 by A29,BORSUK_1:40,XXREAL_1:1;
      len h0-'len h11 +2-'1 in dom h21 by A43,A862,Lm1,FINSEQ_3:25;
      then
A865: h21.k=g2.(h2.k) by A46,FUNCT_1:13;
A866: (i+1)-len h11=(i+1)-'len h11 by A39,A855,XREAL_1:233;
      (i+1)-len h11<=len h11+(len h2-2)-len h11 by A47,A36,A52,A55,A57,A813,
XREAL_1:9;
      then (i+1)-'len h11+2<=len h2-2+2 by A866,XREAL_1:6;
      then
A867: (i+1)-'len h11 +2-'1 <= len h21 by A47,NAT_D:44;
      h0.(len h0) in Lower_Arc(P) by A23,A131,A29,A848,A253,BORSUK_1:40
,FUNCT_1:def 3;
      then
A868: h0/.len h0 in Lower_Arc P by A74,PARTFUN1:def 6;
A869: 0+2<=(i+1)-'len h11 +2 by XREAL_1:6;
      then 2-'1<=((i+1)-'len h11 +2-'1) by NAT_D:42;
      then
A870: j0 in dom h2 by A46,A867,Lm1,FINSEQ_3:25;
      then
A871: h2.j0 in rng h2 by FUNCT_1:def 3;
      then
A872: 0<=h2.j0 & h2.j0<=1 by A29,BORSUK_1:40,XXREAL_1:1;
      (i+1)-len h11<len h0-len h11 by A813,XREAL_1:9;
      then
A873: (i+1)-'len h11+2<len h0-'len h11+2 by A252,A866,XREAL_1:6;
      h0.len h0=(mid(h21,2,len h21 -'1)).(len h0 -len h11) by A39,A36,A64,
FINSEQ_1:23;
      then
A874: h0.len h0=h21.(len h0-'len h11 +2-'1) by A39,A36,A48,A56,A50,A54,A816
,A252,FINSEQ_6:118;
A875: h0/.(i+1)=h0.(i+1) by A815,PARTFUN1:def 6;
      g2.(h2.j0) in rng g2 by A131,A29,A871,BORSUK_1:40,FUNCT_1:def 3;
      then
A876: h0.(i+1) in Lower_Arc(P) by A23,A860,A870,FUNCT_1:13;
      (i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A869,Lm1,NAT_D:39,42;
      then j0<k by A861,A873,XREAL_1:9;
      then
A877: h2.(j0)<h2.(k) by A30,A46,A863,A870,SEQM_3:def 1;
      h0.(i+1)=g2.(h2.j0) by A860,A870,FUNCT_1:13;
      then LE h0/.(i+1),h0/.len h0,Lower_Arc(P),E-max(P),W-min(P) by A21,A22
,A23,A24,A25,A75,A874,A865,A864,A872,A877,A875,Th18;
      hence thesis by A130,A875,A876,A868,JORDAN6:def 10;
    end;
  end;
  i<len h0 by A813,NAT_1:13;
  then
A878: i in dom h0 by A812,FINSEQ_3:25;
  then h0/.i = h0.i by PARTFUN1:def 6;
  then
A879: h0/.i<>W-min P by A72,A67,A78,A812,A878,FUNCT_1:def 4;
  LE h0/.i,h0/.(i+1),P by A256,A812,A813;
  hence thesis by A1,A72,A68,A879,A850,A817,Th14;
end;