jordan7.miz



    begin

    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 Nat holds (i -' k) <= j implies i <= (j + k)

    proof

      let i,j,k be 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 Nat holds (j + k) <= i implies k <= (i -' j)

    proof

      let i,j,k be 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 :: JORDAN7:1

    

     Th1: for P be 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 :: JORDAN7:2

    

     Th2: for P be 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, JORDAN6:def 10;

      hence thesis by JORDAN6: 54;

    end;

    theorem :: JORDAN7:3

    

     Th3: for P be 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);

      :: JORDAN7:def1

      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 be 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 :: JORDAN7:4

    for P be 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 object;

          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 object;

          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;

      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 object;

          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 object;

          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;

      end;

      hence thesis by A12, A3, Def1;

    end;

    theorem :: JORDAN7:5

    

     Th5: for P be compact non empty Subset of ( TOP-REAL 2), q1,q2 be 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 :: JORDAN7:6

    

     Th6: for P be compact non empty Subset of ( TOP-REAL 2), q1,q2 be 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 :: JORDAN7:7

    

     Th7: for P be compact non empty Subset of ( TOP-REAL 2), q1 be 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 :: JORDAN7:8

    for P be compact non empty Subset of ( TOP-REAL 2), q be 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 be object holds x in ( Segment (q,q,P)) iff x = q

      proof

        let x be object;

        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 :: JORDAN7:9

    for P be compact non empty Subset of ( TOP-REAL 2), q1,q2 be 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 :: JORDAN7:10

    

     Th10: for P be compact non empty Subset of ( TOP-REAL 2), q1,q2,q3 be 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 object;

        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 object;

      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 :: JORDAN7:11

    

     Th11: for P be compact non empty Subset of ( TOP-REAL 2), q1,q2 be 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 object;

        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 object;

      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 :: JORDAN7:12

    

     Th12: for P be compact non empty Subset of ( TOP-REAL 2), q1,q2 be 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 object;

        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 object;

      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 :: JORDAN7:13

    

     Th13: for P be compact non empty Subset of ( TOP-REAL 2), q1,q2,q3,q4 be 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 :: JORDAN7:14

    

     Th14: for P be compact non empty Subset of ( TOP-REAL 2), q1,q2,q3 be 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

    reserve n for Nat;

    theorem :: JORDAN7:15

    

     Th15: for P be non empty Subset of ( TOP-REAL n), f be Function of I[01] , (( TOP-REAL n) | P) st f is being_homeomorphism holds ex g be 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 be 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;

        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 :: JORDAN7:16

    

     Th16: for P be non empty Subset of ( TOP-REAL n), g be Function of I[01] , ( TOP-REAL n) st g is continuous one-to-one & ( rng g) = P holds ex f be 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 be 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 be 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, A9, COMPTS_1: 17;

    end;

     Lm4:

    now

      let h2 be 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 :: JORDAN7:17

    

     Th17: for A be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2) st A is_an_arc_of (p1,p2) holds ex g be 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 be 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 be 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 be 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 :: JORDAN7:18

    

     Th18: for 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 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 be 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 :: JORDAN7:19

    

     Th19: for 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 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 be 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 :: JORDAN7:20

    for P be compact non empty Subset of ( TOP-REAL 2), e be Real st P is being_simple_closed_curve & e > 0 holds ex h be 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 be Nat st 1 <= i & i < ( len h) holds LE ((h /. i),(h /. (i + 1)),P)) & (for i be Nat, W be Subset of ( Euclid 2) st 1 <= i & i < ( len h) & W = ( Segment ((h /. i),(h /. (i + 1)),P)) holds ( diameter W) < e) & (for W be Subset of ( Euclid 2) st W = ( Segment ((h /. ( len h)),(h /. 1),P)) holds ( diameter W) < e) & (for i be 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 be Nat st 1 <= i & i < j & j < ( len h) & (i,j) aren't_adjacent holds ( Segment ((h /. i),(h /. (i + 1)),P)) misses ( Segment ((h /. j),(h /. (j + 1)),P))) & for i be 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 be 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 be 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 be Nat, Q be Subset of I[01] , W be 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 be 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 be 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 be Nat, Q be Subset of I[01] , W be 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 object;

        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 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;

            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, NAT_D: 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, NAT_D: 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;

              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;

              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, NAT_D: 42;

            

             A124: 2 <= (((nx -' ( len h11)) + 2) -' 1) by A108, A115, Lm1, NAT_D: 39, NAT_D: 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;

              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;

              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;

            then (((nx -' ( len h1)) + 2) - 1) = (((ny -' ( len h1)) + 2) -' 1) by A39, A115, Lm1, NAT_D: 39, NAT_D: 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;

      

       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;

      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 be Nat st 1 <= i & i < ( len h0) holds LE ((h0 /. i),(h0 /. (i + 1)),P)

      proof

        let i be 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, NAT_D: 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, NAT_D: 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;

              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;

            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;

        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, NAT_D: 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;

        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;

          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, FUNCT_1: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 be 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 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, 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, NAT_D: 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, NAT_D: 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;

            

             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, 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, NAT_D: 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;

            hence thesis by A46, A32, A323, A331, A327, A328, A326, A318, A329, A330, A332, A325, A315, 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 be Nat, W be 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 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 object;

            

             A362: (h0 /. (i + 1)) <> ( W-min P) by A38, A17, A71, A20, A340, A358, A353, A351;

            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 be 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;

                 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;

                  

                   A374: (h11 . i) <> ( E-max P) by A38, A45, A255, A20, A341, A342;

                  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 be object 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;

                  reconsider z as set by TARSKI: 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 be object 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 be 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 be object 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;

                      then 0 in [.(h1 /. i), (h1 /. (i + 1)).] by A8, A354, A346, A355, XXREAL_1: 1;

                      hence ex y be 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 be 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 be 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 object;

            assume x in (g1 .: [.(h1 /. i), (h1 /. (i + 1)).]);

            then

            consider y be object 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;

            hence thesis by A417, Def1;

          end;

          then W = (g1 .: Q1) by A337, A361;

          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, NAT_D: 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, NAT_D: 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, NAT_D: 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;

            

             A458: (h2 /. j) <= 1 by A29, A442, A445, BORSUK_1: 40, XXREAL_1: 1;

            let x be object;

            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;

            then x in { p : LE ((h0 /. i),p,P) & LE (p,(h0 /. (i + 1)),P) } by A459, Def1;

            then

            consider p be 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;

             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;

             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;

            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 be object 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 object;

            assume x in (g2 .: [.(h2 /. j), (h2 /. (j + 1)).]);

            then

            consider y be object 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;

              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;

             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;

          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, NAT_D: 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, NAT_D: 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;

            

             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 object;

            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;

            then x in { p : LE ((h0 /. i),p,P) & LE (p,(h0 /. (i + 1)),P) } by A523, Def1;

            then

            consider p be 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 be object 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;

            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;

            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 object;

            assume x in (g2 .: [.(h2 /. j), (h2 /. (j + 1)).]);

            then

            consider y be object 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;

              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;

             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;

          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 be 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, NAT_D: 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;

        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 object;

          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 be 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 be object 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 be object 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 object;

          assume x in (g2 .: [.(h2 /. j), (h2 /. (j + 1)).]);

          then

          consider y be object 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;

        hence thesis by A31, A47, A36, A52, A55, A57, A554, A560, A563, Lm1;

      end;

      

       A592: for i be Nat st 1 <= i & (i + 1) < ( len h0) holds LE ((h0 /. (i + 1)),(h0 /. (i + 2)),P)

      proof

        let i be 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, NAT_D: 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, NAT_D: 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;

            (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, NAT_D: 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, XREAL_1: 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;

            hence thesis by A646, A650, A657, A660, A656, JORDAN6:def 10;

          end;

        end;

      end;

      thus for i be 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 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[ 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 be Nat st P[k] holds P[(k + 1)]

        proof

          let k be 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, FUNCT_1: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 be Nat holds P[i] from NAT_1:sch 2( A677, A668);

        

         A679: (h11 . 2) <> ( W-min P) by A38, A17, A71, A15, A20;

        ((( 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;

        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 be Nat st 1 <= i & i < j & j < ( len h0) & (i,j) aren't_adjacent holds ( Segment ((h0 /. i),(h0 /. (i + 1)),P)) misses ( Segment ((h0 /. j),(h0 /. (j + 1)),P))

      proof

        let i,j be Nat;

        assume that

         A684: 1 <= i and

         A685: i < j and

         A686: j < ( len h0) and

         A687: (i,j) aren't_adjacent ;

        

         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;

            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, NAT_D: 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;

              (((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;

              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, NAT_D: 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, NAT_D: 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;

          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;

              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, NAT_D: 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;

            (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 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, NAT_D: 42;

          then 1 < k by A824, XXREAL_0: 2;

          then

           A831: (h0 . ( len h0)) <> ( E-max P) by A46, A76, A77, A32, A829, A827;

          (((( 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;

          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, NAT_D: 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, NAT_D: 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;

        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, NAT_D: 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;

       LE ((h0 /. i),(h0 /. (i + 1)),P) by A256, A812, A813;

      hence thesis by A1, A72, A68, A879, A850, A817, Th14;

    end;