jordan5c.miz



    begin

    theorem :: JORDAN5C:1

    

     Th1: for P,Q be Subset of ( TOP-REAL 2), p1,p2,q1 be Point of ( TOP-REAL 2), f be Function of I[01] , (( TOP-REAL 2) | P), s1 be Real st q1 in P & (f . s1) = q1 & f is being_homeomorphism & (f . 0 ) = p1 & (f . 1) = p2 & 0 <= s1 & s1 <= 1 & (for t be Real st 0 <= t & t < s1 holds not (f . t) in Q) holds for g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = q1 & 0 <= s2 & s2 <= 1 holds for t be Real st 0 <= t & t < s2 holds not (g . t) in Q

    proof

      let P,Q be Subset of ( TOP-REAL 2), p1,p2,q1 be Point of ( TOP-REAL 2), f be Function of I[01] , (( TOP-REAL 2) | P), s1 be Real;

      assume that

       A1: q1 in P and

       A2: (f . s1) = q1 and

       A3: f is being_homeomorphism and

       A4: (f . 0 ) = p1 and

       A5: (f . 1) = p2 and

       A6: 0 <= s1 & s1 <= 1 and

       A7: for t be Real st 0 <= t & t < s1 holds not (f . t) in Q;

      reconsider P9 = P as non empty Subset of ( TOP-REAL 2) by A1;

      let g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real;

      assume that

       A8: g is being_homeomorphism and

       A9: (g . 0 ) = p1 and

       A10: (g . 1) = p2 and

       A11: (g . s2) = q1 and

       A12: 0 <= s2 and

       A13: s2 <= 1;

      reconsider f, g as Function of I[01] , (( TOP-REAL 2) | P9);

      

       A14: f is one-to-one by A3, TOPS_2:def 5;

      

       A15: ( dom f) = ( [#] I[01] ) by A3, TOPS_2:def 5;

      then

       A16: 1 in ( dom f) by BORSUK_1: 43;

      

       A17: ( rng f) = ( [#] (( TOP-REAL 2) | P)) by A3, TOPS_2:def 5;

      then f is onto by FUNCT_2:def 3;

      then

       A18: (f " ) = (f qua Function " ) by A14, TOPS_2:def 4;

      

       A19: ((f " ) . p2) = 1 by A5, A16, A14, A18, FUNCT_1: 32;

      

       A20: 0 in ( dom f) by A15, BORSUK_1: 43;

      

       A21: ((f " ) . p1) = 0 by A4, A20, A14, A18, FUNCT_1: 32;

      set fg = ((f " ) * g);

      

       A22: (f " ) is being_homeomorphism by A3, TOPS_2: 56;

      then fg is being_homeomorphism by A8, TOPS_2: 57;

      then

       A23: fg is continuous & fg is one-to-one by TOPS_2:def 5;

      let t be Real;

      assume that

       A24: 0 <= t and

       A25: t < s2;

      

       A26: t <= 1 by A13, A25, XXREAL_0: 2;

      then

      reconsider t1 = t, s29 = s2 as Point of I[01] by A12, A13, A24, BORSUK_1: 43;

      

       A27: t in the carrier of I[01] by A24, A26, BORSUK_1: 43;

      reconsider Ft = (fg . t1) as Real by BORSUK_1: 40;

      

       A28: ( rng g) = ( [#] (( TOP-REAL 2) | P)) by A8, TOPS_2:def 5;

      

       A29: ( dom g) = ( [#] I[01] ) by A8, TOPS_2:def 5;

      then 1 in ( dom g) by BORSUK_1: 43;

      then

       A30: (((f " ) * g) . 1) = 1 by A10, A19, FUNCT_1: 13;

      

       A31: s1 in ( dom f) by A6, A15, BORSUK_1: 43;

      ( dom (f " )) = ( [#] (( TOP-REAL 2) | P)) by A22, TOPS_2:def 5;

      then

       A32: ( dom ((f " ) * g)) = ( dom g) by A28, RELAT_1: 27;

       0 in ( dom g) by A29, BORSUK_1: 43;

      then

       A33: (((f " ) * g) . 0 ) = 0 by A9, A21, FUNCT_1: 13;

      

       A34: 0 <= Ft

      proof

        per cases by A24;

          suppose 0 < t;

          hence thesis by A23, A33, A30, BORSUK_1:def 14, JORDAN5A: 15, TOPMETR: 20;

        end;

          suppose 0 = t;

          hence thesis by A9, A21, A29, FUNCT_1: 13;

        end;

      end;

      (f * ((f " ) * g)) = (g qua Relation * (f * (f " ))) by RELAT_1: 36

      .= (g qua Relation * ( id ( rng f))) by A17, A14, TOPS_2: 52

      .= (( id ( rng g)) * g) by A8, A17, TOPS_2:def 5

      .= g by RELAT_1: 54;

      then

       A35: (f . (((f " ) * g) . t)) = (g . t) by A29, A27, A32, FUNCT_1: 13;

      s2 in ( dom g) by A12, A13, A29, BORSUK_1: 43;

      

      then (((f " ) * g) . s2) = ((f " ) . q1) by A11, FUNCT_1: 13

      .= s1 by A2, A14, A31, A18, FUNCT_1: 32;

      then (fg . s29) = s1;

      then Ft < s1 by A25, A23, A33, A30, JORDAN5A: 15, TOPMETR: 20;

      hence thesis by A7, A34, A35;

    end;

    definition

      let P,Q be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2);

      assume that

       A1: P meets Q & (P /\ Q) is closed and

       A2: P is_an_arc_of (p1,p2);

      :: JORDAN5C:def1

      func First_Point (P,p1,p2,Q) -> Point of ( TOP-REAL 2) means

      : Def1: it in (P /\ Q) & for g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = it & 0 <= s2 & s2 <= 1 holds for t be Real st 0 <= t & t < s2 holds not (g . t) in Q;

      existence

      proof

        consider EX be Point of ( TOP-REAL 2) such that

         A3: EX in (P /\ Q) and

         A4: ex g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = EX & 0 <= s2 & s2 <= 1 & for t be Real st 0 <= t & t < s2 holds not (g . t) in Q by A1, A2, JORDAN5A: 21;

        EX in P by A3, XBOOLE_0:def 4;

        then for g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = EX & 0 <= s2 & s2 <= 1 holds for t be Real st 0 <= t & t < s2 holds not (g . t) in Q by A4, Th1;

        hence thesis by A3;

      end;

      uniqueness

      proof

        let IT1,IT2 be Point of ( TOP-REAL 2);

        

         A5: (P /\ Q) c= Q by XBOOLE_1: 17;

        

         A6: (P /\ Q) c= P by XBOOLE_1: 17;

        assume that

         A7: IT1 in (P /\ Q) and

         A8: for g1 be Function of I[01] , (( TOP-REAL 2) | P), s1 be Real st g1 is being_homeomorphism & (g1 . 0 ) = p1 & (g1 . 1) = p2 & (g1 . s1) = IT1 & 0 <= s1 & s1 <= 1 holds for t be Real st 0 <= t & t < s1 holds not (g1 . t) in Q;

        assume that

         A9: IT2 in (P /\ Q) and

         A10: for g2 be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g2 is being_homeomorphism & (g2 . 0 ) = p1 & (g2 . 1) = p2 & (g2 . s2) = IT2 & 0 <= s2 & s2 <= 1 holds for t be Real st 0 <= t & t < s2 holds not (g2 . t) in Q;

        consider g be Function of I[01] , (( TOP-REAL 2) | P) such that

         A11: g is being_homeomorphism and

         A12: (g . 0 ) = p1 & (g . 1) = p2 by A2, TOPREAL1:def 1;

        

         A13: ( rng g) = ( [#] (( TOP-REAL 2) | P)) by A11, TOPS_2:def 5

        .= P by PRE_TOPC:def 5;

        then

        consider ss1 be object such that

         A14: ss1 in ( dom g) and

         A15: (g . ss1) = IT1 by A6, A7, FUNCT_1:def 3;

        reconsider ss1 as Real by A14, BORSUK_1: 40;

        

         A16: 0 <= ss1 by A14, BORSUK_1: 43;

        consider ss2 be object such that

         A17: ss2 in ( dom g) and

         A18: (g . ss2) = IT2 by A6, A9, A13, FUNCT_1:def 3;

        reconsider ss2 as Real by A17, BORSUK_1: 40;

        

         A19: 0 <= ss2 by A17, BORSUK_1: 43;

        

         A20: ss1 <= 1 by A14, BORSUK_1: 43;

        

         A21: ss2 <= 1 by A17, BORSUK_1: 43;

        per cases by XXREAL_0: 1;

          suppose ss1 < ss2;

          hence thesis by A5, A7, A10, A11, A12, A15, A18, A16, A21;

        end;

          suppose ss1 = ss2;

          hence thesis by A15, A18;

        end;

          suppose ss1 > ss2;

          hence thesis by A5, A8, A9, A11, A12, A15, A18, A20, A19;

        end;

      end;

    end

    theorem :: JORDAN5C:2

    for P,Q be Subset of ( TOP-REAL 2), p,p1,p2 be Point of ( TOP-REAL 2) st p in P & P is_an_arc_of (p1,p2) & Q = {p} holds ( First_Point (P,p1,p2,Q)) = p

    proof

      let P,Q be Subset of ( TOP-REAL 2), p,p1,p2 be Point of ( TOP-REAL 2);

      assume that

       A1: p in P and

       A2: P is_an_arc_of (p1,p2) and

       A3: Q = {p};

      

       A4: (P /\ {p}) = {p} by A1, ZFMISC_1: 46;

      

       A5: for g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = p & 0 <= s2 & s2 <= 1 holds for t be Real st 0 <= t & t < s2 holds not (g . t) in {p}

      proof

        let g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real;

        assume that

         A6: g is being_homeomorphism and (g . 0 ) = p1 and (g . 1) = p2 and

         A7: (g . s2) = p and

         A8: 0 <= s2 and

         A9: s2 <= 1;

        

         A10: g is one-to-one by A6, TOPS_2:def 5;

        let t be Real;

        assume that

         A11: 0 <= t and

         A12: t < s2;

        

         A13: ( dom g) = the carrier of I[01] by A1, FUNCT_2:def 1;

        t <= 1 by A9, A12, XXREAL_0: 2;

        then

         A14: t in ( dom g) by A13, A11, BORSUK_1: 43;

        s2 in ( dom g) by A8, A9, A13, BORSUK_1: 43;

        then (g . t) <> (g . s2) by A10, A12, A14, FUNCT_1:def 4;

        hence thesis by A7, TARSKI:def 1;

      end;

      

       A15: (P /\ Q) is closed by A3, A4, PCOMPS_1: 7;

      

       A16: p in (P /\ {p}) by A4, TARSKI:def 1;

      then P meets {p};

      hence thesis by A2, A3, A16, A15, A5, Def1;

    end;

    theorem :: JORDAN5C:3

    

     Th3: for P,Q be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2) st p1 in Q & (P /\ Q) is closed & P is_an_arc_of (p1,p2) holds ( First_Point (P,p1,p2,Q)) = p1

    proof

      let P,Q be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2);

      assume that

       A1: p1 in Q and

       A2: (P /\ Q) is closed and

       A3: P is_an_arc_of (p1,p2);

      

       A4: for g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = p1 & 0 <= s2 & s2 <= 1 holds for t be Real st 0 <= t & t < s2 holds not (g . t) in Q

      proof

        let g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real;

        assume that

         A5: g is being_homeomorphism and

         A6: (g . 0 ) = p1 and (g . 1) = p2 and

         A7: (g . s2) = p1 and

         A8: 0 <= s2 & s2 <= 1;

        

         A9: g is one-to-one by A5, TOPS_2:def 5;

        let t be Real;

        assume

         A10: 0 <= t & t < s2;

        

         A11: ( dom g) = ( [#] I[01] ) by A5, TOPS_2:def 5

        .= the carrier of I[01] ;

        then

         A12: 0 in ( dom g) by BORSUK_1: 43;

        s2 in ( dom g) by A8, A11, BORSUK_1: 43;

        hence thesis by A6, A7, A12, A9, A10, FUNCT_1:def 4;

      end;

      p1 in P by A3, TOPREAL1: 1;

      then p1 in (P /\ Q) & P meets Q by A1, XBOOLE_0:def 4;

      hence thesis by A2, A3, A4, Def1;

    end;

    theorem :: JORDAN5C:4

    

     Th4: for P,Q be Subset of ( TOP-REAL 2), p1,p2,q1 be Point of ( TOP-REAL 2), f be Function of I[01] , (( TOP-REAL 2) | P), s1 be Real st q1 in P & (f . s1) = q1 & f is being_homeomorphism & (f . 0 ) = p1 & (f . 1) = p2 & 0 <= s1 & s1 <= 1 & (for t be Real st 1 >= t & t > s1 holds not (f . t) in Q) holds for g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = q1 & 0 <= s2 & s2 <= 1 holds for t be Real st 1 >= t & t > s2 holds not (g . t) in Q

    proof

      let P,Q be Subset of ( TOP-REAL 2), p1,p2,q1 be Point of ( TOP-REAL 2), f be Function of I[01] , (( TOP-REAL 2) | P), s1 be Real;

      assume that

       A1: q1 in P and

       A2: (f . s1) = q1 and

       A3: f is being_homeomorphism and

       A4: (f . 0 ) = p1 and

       A5: (f . 1) = p2 and

       A6: 0 <= s1 & s1 <= 1 and

       A7: for t be Real st 1 >= t & t > s1 holds not (f . t) in Q;

      reconsider P9 = P as non empty Subset of ( TOP-REAL 2) by A1;

      let g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real;

      assume that

       A8: g is being_homeomorphism and

       A9: (g . 0 ) = p1 and

       A10: (g . 1) = p2 and

       A11: (g . s2) = q1 and

       A12: 0 <= s2 and

       A13: s2 <= 1;

      reconsider f, g as Function of I[01] , (( TOP-REAL 2) | P9);

      

       A14: f is one-to-one by A3, TOPS_2:def 5;

      set fg = ((f " ) * g);

      let t be Real;

      assume that

       A15: 1 >= t and

       A16: t > s2;

      reconsider t1 = t, s29 = s2 as Point of I[01] by A12, A13, A15, A16, BORSUK_1: 43;

      

       A17: t in the carrier of I[01] by A12, A15, A16, BORSUK_1: 43;

      reconsider Ft = (fg . t1) as Real by BORSUK_1: 40;

      

       A18: ( rng g) = ( [#] (( TOP-REAL 2) | P)) by A8, TOPS_2:def 5;

      

       A19: (f " ) is being_homeomorphism by A3, TOPS_2: 56;

      then fg is being_homeomorphism by A8, TOPS_2: 57;

      then

       A20: fg is continuous & fg is one-to-one by TOPS_2:def 5;

      

       A21: ( dom f) = ( [#] I[01] ) by A3, TOPS_2:def 5;

      then

       A22: 0 in ( dom f) by BORSUK_1: 43;

      

       A23: ( rng f) = ( [#] (( TOP-REAL 2) | P)) by A3, TOPS_2:def 5;

      then f is onto by FUNCT_2:def 3;

      then

       A24: (f " ) = (f qua Function " ) by A14, TOPS_2:def 4;

      then

       A25: ((f " ) . p1) = 0 by A4, A22, A14, FUNCT_1: 32;

      

       A26: 1 in ( dom f) by A21, BORSUK_1: 43;

      

       A27: ((f " ) . p2) = 1 by A24, A5, A26, A14, FUNCT_1: 32;

      

       A28: ( dom g) = ( [#] I[01] ) by A8, TOPS_2:def 5;

      then 0 in ( dom g) by BORSUK_1: 43;

      then

       A29: (((f " ) * g) . 0 ) = 0 by A9, A25, FUNCT_1: 13;

      1 in ( dom g) by A28, BORSUK_1: 43;

      then

       A30: (((f " ) * g) . 1) = 1 by A10, A27, FUNCT_1: 13;

      

       A31: Ft <= 1

      proof

        per cases by A15, XXREAL_0: 1;

          suppose t < 1;

          hence thesis by A20, A29, A30, BORSUK_1:def 15, JORDAN5A: 15, TOPMETR: 20;

        end;

          suppose t = 1;

          hence thesis by A10, A27, A28, FUNCT_1: 13;

        end;

      end;

      ( dom (f " )) = ( [#] (( TOP-REAL 2) | P)) by A19, TOPS_2:def 5;

      then

       A32: t in ( dom ((f " ) * g)) by A28, A18, A17, RELAT_1: 27;

      (f * ((f " ) * g)) = (g qua Relation * (f * (f " ))) by RELAT_1: 36

      .= (g qua Relation * ( id ( rng f))) by A23, A14, TOPS_2: 52

      .= (( id ( rng g)) * g) by A8, A23, TOPS_2:def 5

      .= g by RELAT_1: 54;

      then

       A33: (f . (((f " ) * g) . t)) = (g . t) by A32, FUNCT_1: 13;

      

       A34: s1 in ( dom f) by A6, A21, BORSUK_1: 43;

      s2 in ( dom g) by A12, A13, A28, BORSUK_1: 43;

      

      then (((f " ) * g) . s2) = ((f " ) . q1) by A11, FUNCT_1: 13

      .= s1 by A2, A14, A34, A24, FUNCT_1: 32;

      then (fg . s29) = s1;

      then s1 < Ft by A16, A20, A29, A30, JORDAN5A: 15, TOPMETR: 20;

      hence thesis by A7, A31, A33;

    end;

    definition

      let P,Q be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2);

      assume that

       A1: P meets Q & (P /\ Q) is closed and

       A2: P is_an_arc_of (p1,p2);

      :: JORDAN5C:def2

      func Last_Point (P,p1,p2,Q) -> Point of ( TOP-REAL 2) means

      : Def2: it in (P /\ Q) & for g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = it & 0 <= s2 & s2 <= 1 holds for t be Real st 1 >= t & t > s2 holds not (g . t) in Q;

      existence

      proof

        consider EX be Point of ( TOP-REAL 2) such that

         A3: EX in (P /\ Q) and

         A4: ex g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = EX & 0 <= s2 & s2 <= 1 & for t be Real st 1 >= t & t > s2 holds not (g . t) in Q by A1, A2, JORDAN5A: 22;

        EX in P by A3, XBOOLE_0:def 4;

        then for g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = EX & 0 <= s2 & s2 <= 1 holds for t be Real st 1 >= t & t > s2 holds not (g . t) in Q by A4, Th4;

        hence thesis by A3;

      end;

      uniqueness

      proof

        let IT1,IT2 be Point of ( TOP-REAL 2);

        

         A5: (P /\ Q) c= P by XBOOLE_1: 17;

        assume that

         A6: IT1 in (P /\ Q) and

         A7: for g1 be Function of I[01] , (( TOP-REAL 2) | P), s1 be Real st g1 is being_homeomorphism & (g1 . 0 ) = p1 & (g1 . 1) = p2 & (g1 . s1) = IT1 & 0 <= s1 & s1 <= 1 holds for t be Real st 1 >= t & t > s1 holds not (g1 . t) in Q;

        assume that

         A8: IT2 in (P /\ Q) and

         A9: for g2 be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g2 is being_homeomorphism & (g2 . 0 ) = p1 & (g2 . 1) = p2 & (g2 . s2) = IT2 & 0 <= s2 & s2 <= 1 holds for t be Real st 1 >= t & t > s2 holds not (g2 . t) in Q;

        consider g be Function of I[01] , (( TOP-REAL 2) | P) such that

         A10: g is being_homeomorphism and

         A11: (g . 0 ) = p1 & (g . 1) = p2 by A2, TOPREAL1:def 1;

        

         A12: ( rng g) = ( [#] (( TOP-REAL 2) | P)) by A10, TOPS_2:def 5

        .= P by PRE_TOPC:def 5;

        then

        consider ss1 be object such that

         A13: ss1 in ( dom g) and

         A14: (g . ss1) = IT1 by A5, A6, FUNCT_1:def 3;

        reconsider ss1 as Real by A13, BORSUK_1: 40;

        

         A15: 0 <= ss1 by A13, BORSUK_1: 43;

        

         A16: (P /\ Q) c= Q & ss1 <= 1 by A13, BORSUK_1: 43, XBOOLE_1: 17;

        consider ss2 be object such that

         A17: ss2 in ( dom g) and

         A18: (g . ss2) = IT2 by A5, A8, A12, FUNCT_1:def 3;

        reconsider ss2 as Real by A17, BORSUK_1: 40;

        

         A19: 0 <= ss2 by A17, BORSUK_1: 43;

        

         A20: ss2 <= 1 by A17, BORSUK_1: 43;

        per cases by XXREAL_0: 1;

          suppose ss1 < ss2;

          hence thesis by A7, A8, A10, A11, A14, A18, A15, A16, A20;

        end;

          suppose ss1 = ss2;

          hence thesis by A14, A18;

        end;

          suppose ss1 > ss2;

          hence thesis by A6, A9, A10, A11, A14, A18, A16, A19, A20;

        end;

      end;

    end

    theorem :: JORDAN5C:5

    for P,Q be Subset of ( TOP-REAL 2), p,p1,p2 be Point of ( TOP-REAL 2) st p in P & P is_an_arc_of (p1,p2) & Q = {p} holds ( Last_Point (P,p1,p2,Q)) = p

    proof

      let P,Q be Subset of ( TOP-REAL 2), p,p1,p2 be Point of ( TOP-REAL 2);

      assume that

       A1: p in P and

       A2: P is_an_arc_of (p1,p2) and

       A3: Q = {p};

      

       A4: (P /\ {p}) = {p} by A1, ZFMISC_1: 46;

      

       A5: for g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = p & 0 <= s2 & s2 <= 1 holds for t be Real st 1 >= t & t > s2 holds not (g . t) in {p}

      proof

        let g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real;

        assume that

         A6: g is being_homeomorphism and (g . 0 ) = p1 and (g . 1) = p2 and

         A7: (g . s2) = p and

         A8: 0 <= s2 and

         A9: s2 <= 1;

        

         A10: g is one-to-one by A6, TOPS_2:def 5;

        

         A11: ( dom g) = the carrier of I[01] by A1, FUNCT_2:def 1;

        then

         A12: s2 in ( dom g) by A8, A9, BORSUK_1: 43;

        let t be Real;

        assume that

         A13: 1 >= t and

         A14: t > s2;

        t in ( dom g) by A8, A11, A13, A14, BORSUK_1: 43;

        then (g . t) <> (g . s2) by A10, A14, A12, FUNCT_1:def 4;

        hence thesis by A7, TARSKI:def 1;

      end;

      

       A15: (P /\ Q) is closed by A3, A4, PCOMPS_1: 7;

      

       A16: p in (P /\ {p}) by A4, TARSKI:def 1;

      then P meets {p};

      hence thesis by A2, A3, A16, A15, A5, Def2;

    end;

    theorem :: JORDAN5C:6

    

     Th6: for P,Q be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2) st p2 in Q & (P /\ Q) is closed & P is_an_arc_of (p1,p2) holds ( Last_Point (P,p1,p2,Q)) = p2

    proof

      let P,Q be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2);

      assume that

       A1: p2 in Q and

       A2: (P /\ Q) is closed and

       A3: P is_an_arc_of (p1,p2);

      

       A4: for g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = p2 & 0 <= s2 & s2 <= 1 holds for t be Real st 1 >= t & t > s2 holds not (g . t) in Q

      proof

        let g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real;

        assume that

         A5: g is being_homeomorphism and (g . 0 ) = p1 and

         A6: (g . 1) = p2 & (g . s2) = p2 and

         A7: 0 <= s2 & s2 <= 1;

        

         A8: g is one-to-one by A5, TOPS_2:def 5;

        let t be Real;

        assume

         A9: 1 >= t & t > s2;

        

         A10: ( dom g) = ( [#] I[01] ) by A5, TOPS_2:def 5

        .= the carrier of I[01] ;

        then

         A11: 1 in ( dom g) by BORSUK_1: 43;

        s2 in ( dom g) by A7, A10, BORSUK_1: 43;

        hence thesis by A6, A11, A8, A9, FUNCT_1:def 4;

      end;

      p2 in P by A3, TOPREAL1: 1;

      then p2 in (P /\ Q) & P meets Q by A1, XBOOLE_0:def 4;

      hence thesis by A2, A3, A4, Def2;

    end;

    theorem :: JORDAN5C:7

    

     Th7: for P,Q be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2) st P c= Q & P is closed & P is_an_arc_of (p1,p2) holds ( First_Point (P,p1,p2,Q)) = p1 & ( Last_Point (P,p1,p2,Q)) = p2

    proof

      let P,Q be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2);

      assume that

       A1: P c= Q and

       A2: P is closed and

       A3: P is_an_arc_of (p1,p2);

      

       A4: p2 in P by A3, TOPREAL1: 1;

      (P /\ Q) = P & p1 in P by A1, A3, TOPREAL1: 1, XBOOLE_1: 28;

      hence thesis by A1, A2, A3, A4, Th3, Th6;

    end;

    begin

    definition

      let P be Subset of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2);

      :: JORDAN5C:def3

      pred LE q1,q2,P,p1,p2 means q1 in P & q2 in P & for g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s1) = q1 & 0 <= s1 & s1 <= 1 & (g . s2) = q2 & 0 <= s2 & s2 <= 1 holds s1 <= s2;

    end

    theorem :: JORDAN5C:8

    

     Th8: for P be Subset of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2), g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real st P is_an_arc_of (p1,p2) & g is being_homeomorphism & (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 Subset of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2), g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real;

      assume that

       A1: P is_an_arc_of (p1,p2) and

       A2: g is being_homeomorphism and

       A3: (g . 0 ) = p1 and

       A4: (g . 1) = p2 and

       A5: (g . s1) = q1 and

       A6: 0 <= s1 & s1 <= 1 and

       A7: (g . s2) = q2 and

       A8: 0 <= s2 & s2 <= 1 and

       A9: s1 <= s2;

      reconsider P9 = P as non empty Subset of ( TOP-REAL 2) by A1, TOPREAL1: 1;

      s1 in the carrier of I[01] by A6, BORSUK_1: 43;

      then

       A10: q1 in ( [#] (( TOP-REAL 2) | P9)) by A5, FUNCT_2: 5;

      reconsider g as Function of I[01] , (( TOP-REAL 2) | P9);

      s2 in the carrier of I[01] by A8, BORSUK_1: 43;

      then (g . s2) in the carrier of (( TOP-REAL 2) | P9) by FUNCT_2: 5;

      then

       A11: q2 in P by A7, A10, PRE_TOPC:def 5;

       A12:

      now

        reconsider s19 = s1, s29 = s2 as Point of I[01] by A6, A8, BORSUK_1: 43;

        let h be Function of I[01] , (( TOP-REAL 2) | P9), t1,t2 be Real;

        assume that

         A13: h is being_homeomorphism and

         A14: (h . 0 ) = p1 and

         A15: (h . 1) = p2 and

         A16: (h . t1) = q1 and

         A17: 0 <= t1 & t1 <= 1 and

         A18: (h . t2) = q2 and

         A19: 0 <= t2 & t2 <= 1;

        

         A20: h is one-to-one by A13, TOPS_2:def 5;

        set hg = ((h " ) * g);

        (h " ) is being_homeomorphism by A13, TOPS_2: 56;

        then hg is being_homeomorphism by A2, TOPS_2: 57;

        then

         A21: hg is continuous & hg is one-to-one by TOPS_2:def 5;

        reconsider hg1 = (hg . s19), hg2 = (hg . s29) as Real by BORSUK_1: 40;

        

         A22: ( dom g) = ( [#] I[01] ) by A2, TOPS_2:def 5;

        then

         A23: 0 in ( dom g) by BORSUK_1: 43;

        

         A24: ( dom h) = ( [#] I[01] ) by A13, TOPS_2:def 5;

        then

         A25: t1 in ( dom h) by A17, BORSUK_1: 43;

        

         A26: 0 in ( dom h) by A24, BORSUK_1: 43;

        ( rng h) = ( [#] (( TOP-REAL 2) | P)) by A13, TOPS_2:def 5;

        then h is onto by FUNCT_2:def 3;

        then

         A27: (h " ) = (h qua Function " ) by A20, TOPS_2:def 4;

        then ((h " ) . p1) = 0 by A14, A26, A20, FUNCT_1: 32;

        then

         A28: (((h " ) * g) . 0 ) = 0 by A3, A23, FUNCT_1: 13;

        s1 in ( dom g) by A6, A22, BORSUK_1: 43;

        

        then

         A29: (((h " ) * g) . s1) = ((h " ) . q1) by A5, FUNCT_1: 13

        .= t1 by A16, A20, A25, A27, FUNCT_1: 32;

        

         A30: t2 in ( dom h) by A19, A24, BORSUK_1: 43;

        s2 in ( dom g) by A8, A22, BORSUK_1: 43;

        

        then

         A31: (((h " ) * g) . s2) = ((h " ) . q2) by A7, FUNCT_1: 13

        .= t2 by A18, A20, A30, A27, FUNCT_1: 32;

        

         A32: 1 in ( dom g) by A22, BORSUK_1: 43;

        

         A33: 1 in ( dom h) by A24, BORSUK_1: 43;

        ((h " ) . p2) = 1 by A15, A33, A20, A27, FUNCT_1: 32;

        then

         A34: (((h " ) * g) . 1) = 1 by A4, A32, FUNCT_1: 13;

        per cases by A9, XXREAL_0: 1;

          suppose s1 < s2;

          then hg1 < hg2 by A21, A28, A34, JORDAN5A: 16;

          hence t1 <= t2 by A29, A31;

        end;

          suppose s1 = s2;

          hence t1 <= t2 by A29, A31;

        end;

      end;

      q1 in P by A10, PRE_TOPC:def 5;

      hence thesis by A11, A12;

    end;

    theorem :: JORDAN5C:9

    

     Th9: for P be Subset of ( TOP-REAL 2), p1,p2,q1 be Point of ( TOP-REAL 2) st q1 in P holds LE (q1,q1,P,p1,p2)

    proof

      let P be Subset of ( TOP-REAL 2), p1,p2,q1 be Point of ( TOP-REAL 2);

      assume

       A1: q1 in P;

      then

      reconsider P as non empty Subset of ( TOP-REAL 2);

      now

        let g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real;

        assume that

         A2: g is being_homeomorphism and (g . 0 ) = p1 and (g . 1) = p2 and

         A3: (g . s1) = q1 and

         A4: 0 <= s1 & s1 <= 1 and

         A5: (g . s2) = q1 and

         A6: 0 <= s2 & s2 <= 1;

        

         A7: g is one-to-one by A2, TOPS_2:def 5;

        s1 in the carrier of I[01] & s2 in the carrier of I[01] by A4, A6, BORSUK_1: 43;

        hence s1 <= s2 by A3, A5, A7, FUNCT_2: 19;

      end;

      hence thesis by A1;

    end;

    theorem :: JORDAN5C:10

    

     Th10: for P be Subset of ( TOP-REAL 2), p1,p2,q1 be Point of ( TOP-REAL 2) st P is_an_arc_of (p1,p2) & q1 in P holds LE (p1,q1,P,p1,p2) & LE (q1,p2,P,p1,p2)

    proof

      let P be Subset of ( TOP-REAL 2), p1,p2,q1 be Point of ( TOP-REAL 2);

      assume that

       A1: P is_an_arc_of (p1,p2) and

       A2: q1 in P;

      reconsider P as non empty Subset of ( TOP-REAL 2) by A2;

       A3:

      now

        

         A4: 0 in the carrier of I[01] by BORSUK_1: 43;

        let g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real;

        assume that

         A5: g is being_homeomorphism and

         A6: (g . 0 ) = p1 and (g . 1) = p2 and

         A7: (g . s1) = p1 and

         A8: 0 <= s1 & s1 <= 1 and (g . s2) = q1 and

         A9: 0 <= s2 and s2 <= 1;

        s1 in the carrier of I[01] & g is one-to-one by A5, A8, BORSUK_1: 43, TOPS_2:def 5;

        hence s1 <= s2 by A6, A7, A9, A4, FUNCT_2: 19;

      end;

       A10:

      now

        

         A11: 1 in the carrier of I[01] by BORSUK_1: 43;

        let g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real;

        assume that

         A12: g is being_homeomorphism and (g . 0 ) = p1 and

         A13: (g . 1) = p2 and (g . s1) = q1 and 0 <= s1 and

         A14: s1 <= 1 & (g . s2) = p2 and

         A15: 0 <= s2 & s2 <= 1;

        s2 in the carrier of I[01] & g is one-to-one by A12, A15, BORSUK_1: 43, TOPS_2:def 5;

        hence s1 <= s2 by A13, A14, A11, FUNCT_2: 19;

      end;

      p1 in P & p2 in P by A1, TOPREAL1: 1;

      hence thesis by A2, A3, A10;

    end;

    theorem :: JORDAN5C:11

    for P be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2) st P is_an_arc_of (p1,p2) holds LE (p1,p2,P,p1,p2)

    proof

      let P be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2);

      assume

       A1: P is_an_arc_of (p1,p2);

      then p2 in P by TOPREAL1: 1;

      hence thesis by A1, Th10;

    end;

    theorem :: JORDAN5C:12

    

     Th12: for P be Subset of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2) st P is_an_arc_of (p1,p2) & LE (q1,q2,P,p1,p2) & LE (q2,q1,P,p1,p2) holds q1 = q2

    proof

      let P be Subset of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2);

      assume that

       A1: P is_an_arc_of (p1,p2) and

       A2: LE (q1,q2,P,p1,p2) and

       A3: LE (q2,q1,P,p1,p2);

      consider f be Function of I[01] , (( TOP-REAL 2) | P) such that

       A4: f is being_homeomorphism and

       A5: (f . 0 ) = p1 & (f . 1) = p2 by A1, TOPREAL1:def 1;

      

       A6: ( dom f) = ( [#] I[01] ) by A4, TOPS_2:def 5

      .= the carrier of I[01] ;

      

       A7: ( rng f) = ( [#] (( TOP-REAL 2) | P)) by A4, TOPS_2:def 5

      .= P by PRE_TOPC:def 5;

      then q2 in ( rng f) by A2;

      then

      consider x be object such that

       A8: x in ( dom f) and

       A9: q2 = (f . x) by FUNCT_1:def 3;

      q1 in ( rng f) by A2, A7;

      then

      consider y be object such that

       A10: y in ( dom f) and

       A11: q1 = (f . y) by FUNCT_1:def 3;

       [. 0 , 1.] = { r1 where r1 be Real : 0 <= r1 & r1 <= 1 } by RCOMP_1:def 1;

      then

      consider s3 be Real such that

       A12: s3 = x and

       A13: 0 <= s3 & s3 <= 1 by A6, A8, BORSUK_1: 40;

       [. 0 , 1.] = { r1 where r1 be Real : 0 <= r1 & r1 <= 1 } by RCOMP_1:def 1;

      then

      consider s4 be Real such that

       A14: s4 = y and

       A15: 0 <= s4 & s4 <= 1 by A6, A10, BORSUK_1: 40;

      s3 <= s4 & s4 <= s3 by A2, A3, A4, A5, A9, A12, A13, A11, A14, A15;

      hence thesis by A9, A12, A11, A14, XXREAL_0: 1;

    end;

    theorem :: JORDAN5C:13

    

     Th13: for P be Subset of ( TOP-REAL 2), p1,p2,q1,q2,q3 be Point of ( TOP-REAL 2) st LE (q1,q2,P,p1,p2) & LE (q2,q3,P,p1,p2) holds LE (q1,q3,P,p1,p2)

    proof

      let P be Subset of ( TOP-REAL 2), p1,p2,q1,q2,q3 be Point of ( TOP-REAL 2);

      assume that

       A1: LE (q1,q2,P,p1,p2) and

       A2: LE (q2,q3,P,p1,p2);

      

       A3: q2 in P by A1;

       A4:

      now

        

         A5: [. 0 , 1.] = { r1 where r1 be Real : 0 <= r1 & r1 <= 1 } by RCOMP_1:def 1;

        let g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real;

        assume that

         A6: g is being_homeomorphism and

         A7: (g . 0 ) = p1 & (g . 1) = p2 & (g . s1) = q1 and 0 <= s1 and

         A8: s1 <= 1 & (g . s2) = q3 & 0 <= s2 & s2 <= 1;

        ( rng g) = ( [#] (( TOP-REAL 2) | P)) by A6, TOPS_2:def 5

        .= P by PRE_TOPC:def 5;

        then

        consider x be object such that

         A9: x in ( dom g) and

         A10: q2 = (g . x) by A3, FUNCT_1:def 3;

        ( dom g) = ( [#] I[01] ) by A6, TOPS_2:def 5

        .= the carrier of I[01] ;

        then

        consider s3 be Real such that

         A11: s3 = x & 0 <= s3 & s3 <= 1 by A9, A5, BORSUK_1: 40;

        s1 <= s3 & s3 <= s2 by A1, A2, A6, A7, A8, A10, A11;

        hence s1 <= s2 by XXREAL_0: 2;

      end;

      q1 in P & q3 in P by A1, A2;

      hence thesis by A4;

    end;

    theorem :: JORDAN5C:14

    for P be Subset of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2) st P is_an_arc_of (p1,p2) & q1 in P & q2 in P & q1 <> q2 holds LE (q1,q2,P,p1,p2) & not LE (q2,q1,P,p1,p2) or LE (q2,q1,P,p1,p2) & not LE (q1,q2,P,p1,p2)

    proof

      let P be Subset of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2);

      assume that

       A1: P is_an_arc_of (p1,p2) and

       A2: q1 in P and

       A3: q2 in P and

       A4: q1 <> q2;

      reconsider P as non empty Subset of ( TOP-REAL 2) by A2;

       not ( LE (q1,q2,P,p1,p2) iff LE (q2,q1,P,p1,p2))

      proof

        consider f be Function of I[01] , (( TOP-REAL 2) | P) such that

         A5: f is being_homeomorphism and

         A6: (f . 0 ) = p1 & (f . 1) = p2 by A1, TOPREAL1:def 1;

        

         A7: ( rng f) = ( [#] (( TOP-REAL 2) | P)) by A5, TOPS_2:def 5

        .= P by PRE_TOPC:def 5;

        then

        consider x be object such that

         A8: x in ( dom f) and

         A9: q1 = (f . x) by A2, FUNCT_1:def 3;

        consider y be object such that

         A10: y in ( dom f) and

         A11: q2 = (f . y) by A3, A7, FUNCT_1:def 3;

        ( dom f) = ( [#] I[01] ) by A5, TOPS_2:def 5

        .= [. 0 , 1.] by BORSUK_1: 40;

        then

        reconsider s1 = x, s2 = y as Real by A8, A10;

        

         A12: 0 <= s1 by A8, BORSUK_1: 43;

        

         A13: s2 <= 1 by A10, BORSUK_1: 43;

        

         A14: 0 <= s2 by A10, BORSUK_1: 43;

        

         A15: s1 <= 1 by A8, BORSUK_1: 43;

        assume

         A16: LE (q1,q2,P,p1,p2) iff LE (q2,q1,P,p1,p2);

        per cases by XXREAL_0: 1;

          suppose s1 < s2;

          hence thesis by A1, A16, A5, A6, A9, A11, A12, A15, A13, Th8;

        end;

          suppose s1 = s2;

          hence thesis by A4, A9, A11;

        end;

          suppose s1 > s2;

          hence thesis by A1, A16, A5, A6, A9, A11, A15, A14, A13, Th8;

        end;

      end;

      hence thesis;

    end;

    begin

    theorem :: JORDAN5C:15

    

     Th15: for f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2) st f is being_S-Seq & (( L~ f) /\ Q) is closed & q in ( L~ f) & q in Q holds LE (( First_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)),q,( L~ f),(f /. 1),(f /. ( len f)))

    proof

      let f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2);

      assume that

       A1: f is being_S-Seq and

       A2: (( L~ f) /\ Q) is closed and

       A3: q in ( L~ f) and

       A4: q in Q;

      set P = ( L~ f);

      

       A5: (( L~ f) /\ Q) c= ( L~ f) by XBOOLE_1: 17;

      set q1 = ( First_Point (P,(f /. 1),(f /. ( len f)),Q));

      ( L~ f) meets Q & P is_an_arc_of ((f /. 1),(f /. ( len f))) by A1, A3, A4, TOPREAL1: 25, XBOOLE_0: 3;

      then q1 in (( L~ f) /\ Q) & for g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real st g is being_homeomorphism & (g . 0 ) = (f /. 1) & (g . 1) = (f /. ( len f)) & (g . s1) = q1 & 0 <= s1 & s1 <= 1 & (g . s2) = q & 0 <= s2 & s2 <= 1 holds s1 <= s2 by A2, A4, Def1;

      hence thesis by A3, A5;

    end;

    theorem :: JORDAN5C:16

    

     Th16: for f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2) st f is being_S-Seq & (( L~ f) /\ Q) is closed & q in ( L~ f) & q in Q holds LE (q,( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)),( L~ f),(f /. 1),(f /. ( len f)))

    proof

      let f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2);

      set P = ( L~ f);

      assume that

       A1: f is being_S-Seq and

       A2: (( L~ f) /\ Q) is closed and

       A3: q in ( L~ f) and

       A4: q in Q;

      set q1 = ( Last_Point (P,(f /. 1),(f /. ( len f)),Q));

      

       A5: (( L~ f) /\ Q) c= ( L~ f) by XBOOLE_1: 17;

      ( L~ f) meets Q & P is_an_arc_of ((f /. 1),(f /. ( len f))) by A1, A3, A4, TOPREAL1: 25, XBOOLE_0: 3;

      then q1 in (( L~ f) /\ Q) & for g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real st g is being_homeomorphism & (g . 0 ) = (f /. 1) & (g . 1) = (f /. ( len f)) & (g . s1) = q & 0 <= s1 & s1 <= 1 & (g . s2) = q1 & 0 <= s2 & s2 <= 1 holds s1 <= s2 by A2, A4, Def2;

      hence thesis by A3, A5;

    end;

    theorem :: JORDAN5C:17

    

     Th17: for q1,q2,p1,p2 be Point of ( TOP-REAL 2) st p1 <> p2 holds LE (q1,q2,( LSeg (p1,p2)),p1,p2) implies LE (q1,q2,p1,p2)

    proof

      let q1,q2,p1,p2 be Point of ( TOP-REAL 2);

      set P = ( LSeg (p1,p2));

      assume p1 <> p2;

      then

      consider f be Function of I[01] , (( TOP-REAL 2) | ( LSeg (p1,p2))) such that

       A1: for x be Real st x in [. 0 , 1.] holds (f . x) = (((1 - x) * p1) + (x * p2)) and

       A2: f is being_homeomorphism & (f . 0 ) = p1 & (f . 1) = p2 by JORDAN5A: 3;

      assume

       A3: LE (q1,q2,P,p1,p2);

      hence q1 in P & q2 in P;

      let r1,r2 be Real;

      assume that

       A4: 0 <= r1 and

       A5: r1 <= 1 and

       A6: q1 = (((1 - r1) * p1) + (r1 * p2)) and

       A7: 0 <= r2 & r2 <= 1 and

       A8: q2 = (((1 - r2) * p1) + (r2 * p2));

      r2 in [. 0 , 1.] by A7, BORSUK_1: 40, BORSUK_1: 43;

      then

       A9: q2 = (f . r2) by A8, A1;

      r1 in [. 0 , 1.] by A4, A5, BORSUK_1: 40, BORSUK_1: 43;

      then q1 = (f . r1) by A6, A1;

      hence thesis by A3, A5, A7, A2, A9;

    end;

    theorem :: JORDAN5C:18

    for P,Q be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2) st P is_an_arc_of (p1,p2) & P meets Q & (P /\ Q) is closed holds ( First_Point (P,p1,p2,Q)) = ( Last_Point (P,p2,p1,Q)) & ( Last_Point (P,p1,p2,Q)) = ( First_Point (P,p2,p1,Q))

    proof

      let P,Q be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2);

      assume that

       A1: P is_an_arc_of (p1,p2) and

       A2: (P /\ Q) <> {} and

       A3: (P /\ Q) is closed;

      reconsider P as non empty Subset of ( TOP-REAL 2) by A2;

      

       A4: P meets Q by A2;

      

       A5: P is_an_arc_of (p2,p1) by A1, JORDAN5B: 14;

      

       A6: for g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = ( Last_Point (P,p2,p1,Q)) & 0 <= s2 & s2 <= 1 holds for t be Real st 0 <= t & t < s2 holds not (g . t) in Q

      proof

        set Ex = ( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1))));

        let f be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real;

        assume that

         A7: f is being_homeomorphism and

         A8: (f . 0 ) = p1 and

         A9: (f . 1) = p2 and

         A10: (f . s2) = ( Last_Point (P,p2,p1,Q)) and

         A11: 0 <= s2 and

         A12: s2 <= 1;

        set s21 = (1 - s2);

        set g = (f * Ex);

        

         A13: Ex is being_homeomorphism by TREAL_1: 18;

        ( dom f) = ( [#] I[01] ) by A7, TOPS_2:def 5;

        then ( rng Ex) = ( dom f) by A13, TOPMETR: 20, TOPS_2:def 5;

        then ( dom g) = ( dom Ex) by RELAT_1: 27;

        then

         A14: ( dom g) = ( [#] I[01] ) by A13, TOPMETR: 20, TOPS_2:def 5;

        reconsider g as Function of I[01] , (( TOP-REAL 2) | P) by TOPMETR: 20;

        

         A15: (1 - 1) <= s21 & s21 <= (1 - 0 ) by A11, A12, XREAL_1: 13;

        then

         A16: s21 in ( dom g) by A14, BORSUK_1: 43;

        (Ex . ( (#) ( 0 ,1))) = 1 by BORSUK_1:def 15, TREAL_1: 5, TREAL_1: 9;

        then

         A17: (g . 0 ) = p2 by A9, A14, BORSUK_1:def 14, FUNCT_1: 12, TREAL_1: 5;

        (Ex . (( 0 ,1) (#) )) = 0 by BORSUK_1:def 14, TREAL_1: 5, TREAL_1: 9;

        then

         A18: (g . 1) = p1 by A8, A14, BORSUK_1:def 15, FUNCT_1: 12, TREAL_1: 5;

        let t be Real;

        assume that

         A19: 0 <= t and

         A20: t < s2;

        

         A21: (1 - t) <= (1 - 0 ) by A19, XREAL_1: 13;

        t <= 1 by A12, A20, XXREAL_0: 2;

        then

         A22: (1 - 1) <= (1 - t) by XREAL_1: 13;

        then

        reconsider r2 = (1 - s2), t9 = (1 - t) as Point of ( Closed-Interval-TSpace ( 0 ,1)) by A15, A21, BORSUK_1: 43, TOPMETR: 20;

        

         A23: (1 - t) in ( dom g) by A14, A22, A21, BORSUK_1: 43;

        (Ex . r2) = (((1 - (1 - s2)) * 1) + ((1 - s2) * 0 )) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1: 5, TREAL_1:def 3

        .= s2;

        then

         A24: (g . s21) = (f . s2) by A16, FUNCT_1: 12;

        (Ex . t9) = (((1 - (1 - t)) * 1) + ((1 - t) * 0 )) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1: 5, TREAL_1:def 3

        .= t;

        then

         A25: (g . t9) = (f . t) by A23, FUNCT_1: 12;

        

         A26: (1 - s2) < (1 - t) by A20, XREAL_1: 15;

        g is being_homeomorphism by A7, A13, TOPMETR: 20, TOPS_2: 57;

        hence thesis by A3, A5, A4, A10, A17, A18, A15, A21, A24, A25, A26, Def2;

      end;

      

       A27: for g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = ( First_Point (P,p2,p1,Q)) & 0 <= s2 & s2 <= 1 holds for t be Real st 1 >= t & t > s2 holds not (g . t) in Q

      proof

        set Ex = ( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1))));

        let f be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real;

        assume that

         A28: f is being_homeomorphism and

         A29: (f . 0 ) = p1 and

         A30: (f . 1) = p2 and

         A31: (f . s2) = ( First_Point (P,p2,p1,Q)) and

         A32: 0 <= s2 and

         A33: s2 <= 1;

        set g = (f * Ex);

        

         A34: Ex is being_homeomorphism by TREAL_1: 18;

        ( dom f) = ( [#] I[01] ) by A28, TOPS_2:def 5;

        then ( rng Ex) = ( dom f) by A34, TOPMETR: 20, TOPS_2:def 5;

        then ( dom g) = ( dom Ex) by RELAT_1: 27;

        then

         A35: ( dom g) = ( [#] I[01] ) by A34, TOPMETR: 20, TOPS_2:def 5;

        let t be Real;

        assume that

         A36: 1 >= t and

         A37: t > s2;

        

         A38: (1 - s2) > (1 - t) by A37, XREAL_1: 15;

        set s21 = (1 - s2);

        

         A39: s21 <= (1 - 0 ) by A32, XREAL_1: 13;

        reconsider g as Function of I[01] , (( TOP-REAL 2) | P) by TOPMETR: 20;

        

         A40: (1 - 1) <= (1 - t) by A36, XREAL_1: 13;

        

         A41: (1 - t) <= (1 - 0 ) by A32, A37, XREAL_1: 13;

        then

         A42: (1 - t) in ( dom g) by A35, A40, BORSUK_1: 43;

        

         A43: (1 - 1) <= s21 by A33, XREAL_1: 13;

        then

         A44: s21 in ( dom g) by A35, A39, BORSUK_1: 43;

        reconsider r2 = (1 - s2), t9 = (1 - t) as Point of ( Closed-Interval-TSpace ( 0 ,1)) by A43, A39, A40, A41, BORSUK_1: 43, TOPMETR: 20;

        (Ex . r2) = (((1 - (1 - s2)) * 1) + ((1 - s2) * 0 )) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1: 5, TREAL_1:def 3

        .= s2;

        then

         A45: (g . s21) = (f . s2) by A44, FUNCT_1: 12;

        (Ex . t9) = (((1 - (1 - t)) * 1) + ((1 - t) * 0 )) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1: 5, TREAL_1:def 3

        .= t;

        then

         A46: (g . t9) = (f . t) by A42, FUNCT_1: 12;

        (Ex . ( (#) ( 0 ,1))) = 1 by BORSUK_1:def 15, TREAL_1: 5, TREAL_1: 9;

        then

         A47: (g . 0 ) = p2 by A30, A35, BORSUK_1:def 14, FUNCT_1: 12, TREAL_1: 5;

        (Ex . (( 0 ,1) (#) )) = 0 by BORSUK_1:def 14, TREAL_1: 5, TREAL_1: 9;

        then

         A48: (g . 1) = p1 by A29, A35, BORSUK_1:def 15, FUNCT_1: 12, TREAL_1: 5;

        g is being_homeomorphism by A28, A34, TOPMETR: 20, TOPS_2: 57;

        hence thesis by A3, A5, A4, A31, A47, A48, A39, A40, A45, A46, A38, Def1;

      end;

      ( Last_Point (P,p2,p1,Q)) in (P /\ Q) & ( First_Point (P,p2,p1,Q)) in (P /\ Q) by A3, A5, A4, Def1, Def2;

      hence thesis by A1, A3, A4, A6, A27, Def1, Def2;

    end;

    theorem :: JORDAN5C:19

    

     Th19: for f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), i be Nat st ( L~ f) meets Q & Q is closed & f is being_S-Seq & 1 <= i & (i + 1) <= ( len f) & ( First_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) in ( LSeg (f,i)) holds ( First_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) = ( First_Point (( LSeg (f,i)),(f /. i),(f /. (i + 1)),Q))

    proof

      let f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), i be Nat;

      assume that

       A1: ( L~ f) meets Q and

       A2: Q is closed and

       A3: f is being_S-Seq and

       A4: 1 <= i & (i + 1) <= ( len f) and

       A5: ( First_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) in ( LSeg (f,i));

      ( len f) >= 2 by A3, TOPREAL1:def 8;

      then

      reconsider P = ( L~ f), R = ( LSeg (f,i)) as non empty Subset of the carrier of ( TOP-REAL 2) by A5, TOPREAL1: 23;

      

       A6: P is_an_arc_of ((f /. 1),(f /. ( len f))) by A3, TOPREAL1: 25;

      set FPO = ( First_Point (R,(f /. i),(f /. (i + 1)),Q)), FPG = ( First_Point (P,(f /. 1),(f /. ( len f)),Q));

      

       A7: (( L~ f) /\ Q) is closed by A2, TOPS_1: 8;

      then ( First_Point (P,(f /. 1),(f /. ( len f)),Q)) in (( L~ f) /\ Q) by A1, A6, Def1;

      then

       A8: ( First_Point (P,(f /. 1),(f /. ( len f)),Q)) in Q by XBOOLE_0:def 4;

      

       A9: (i + 1) in ( dom f) by A4, SEQ_4: 134;

      

       A10: f is one-to-one & i in ( dom f) by A3, A4, SEQ_4: 134, TOPREAL1:def 8;

      

       A11: (f /. i) <> (f /. (i + 1))

      proof

        assume (f /. i) = (f /. (i + 1));

        then i = (i + 1) by A10, A9, PARTFUN2: 10;

        hence thesis;

      end;

      FPG = FPO

      proof

        FPG in (( L~ f) /\ Q) by A1, A7, A6, Def1;

        then

         A12: FPG in ( L~ f) by XBOOLE_0:def 4;

        consider F be Function of I[01] , (( TOP-REAL 2) | P) such that

         A13: F is being_homeomorphism and

         A14: (F . 0 ) = (f /. 1) & (F . 1) = (f /. ( len f)) by A6, TOPREAL1:def 1;

        ( rng F) = ( [#] (( TOP-REAL 2) | P)) by A13, TOPS_2:def 5

        .= ( L~ f) by PRE_TOPC:def 5;

        then

        consider s21 be object such that

         A15: s21 in ( dom F) and

         A16: (F . s21) = FPG by A12, FUNCT_1:def 3;

        

         A17: ( dom F) = ( [#] I[01] ) by A13, TOPS_2:def 5

        .= [. 0 , 1.] by BORSUK_1: 40;

        then

        reconsider s21 as Real by A15;

        

         A18: s21 <= 1 by A15, BORSUK_1: 43;

        

         A19: for g be Function of I[01] , (( TOP-REAL 2) | R), s2 be Real st g is being_homeomorphism & (g . 0 ) = (f /. i) & (g . 1) = (f /. (i + 1)) & (g . s2) = FPG & 0 <= s2 & s2 <= 1 holds for t be Real st 0 <= t & t < s2 holds not (g . t) in Q

        proof

          consider ppi,pi1 be Real such that

           A20: ppi < pi1 and

           A21: 0 <= ppi and ppi <= 1 and 0 <= pi1 and

           A22: pi1 <= 1 and

           A23: ( LSeg (f,i)) = (F .: [.ppi, pi1.]) and

           A24: (F . ppi) = (f /. i) and

           A25: (F . pi1) = (f /. (i + 1)) by A3, A4, A13, A14, JORDAN5B: 7;

          

           A26: ppi in { dd where dd be Real : ppi <= dd & dd <= pi1 } by A20;

          then

          reconsider Poz = [.ppi, pi1.] as non empty Subset of I[01] by A21, A22, BORSUK_1: 40, RCOMP_1:def 1, XXREAL_1: 34;

          consider hh be Function of ( I[01] | Poz), (( TOP-REAL 2) | R) such that

           A27: hh = (F | Poz) and

           A28: hh is being_homeomorphism by A3, A4, A13, A14, A23, JORDAN5B: 8;

          

           A29: hh = (F * ( id Poz)) by A27, RELAT_1: 65;

          

           A30: [.ppi, pi1.] c= [. 0 , 1.] by A21, A22, XXREAL_1: 34;

          reconsider A = ( Closed-Interval-TSpace (ppi,pi1)) as strict SubSpace of I[01] by A20, A21, A22, TOPMETR: 20, TREAL_1: 3;

          Poz = ( [#] A) by A20, TOPMETR: 18;

          then

           A31: ( I[01] | Poz) = A by PRE_TOPC:def 5;

          (hh " ) is being_homeomorphism by A28, TOPS_2: 56;

          then

           A32: (hh " ) is continuous one-to-one by TOPS_2:def 5;

          pi1 in { dd where dd be Real : ppi <= dd & dd <= pi1 } by A20;

          then pi1 in [.ppi, pi1.] by RCOMP_1:def 1;

          then pi1 in (( dom F) /\ Poz) by A17, A30, XBOOLE_0:def 4;

          then

           A33: pi1 in ( dom hh) by A27, RELAT_1: 61;

          then

           A34: (hh . pi1) = (f /. (i + 1)) by A25, A27, FUNCT_1: 47;

          the carrier of (( TOP-REAL 2) | P) = ( [#] (( TOP-REAL 2) | P))

          .= P by PRE_TOPC:def 5;

          then

          reconsider SEG = ( LSeg (f,i)) as non empty Subset of the carrier of (( TOP-REAL 2) | P) by A5, TOPREAL3: 19;

          

           A35: the carrier of ((( TOP-REAL 2) | P) | SEG) = ( [#] ((( TOP-REAL 2) | P) | SEG))

          .= SEG by PRE_TOPC:def 5;

          reconsider SE = SEG as non empty Subset of ( TOP-REAL 2);

          let g be Function of I[01] , (( TOP-REAL 2) | R), s2 be Real;

          assume that

           A36: g is being_homeomorphism and

           A37: (g . 0 ) = (f /. i) and

           A38: (g . 1) = (f /. (i + 1)) and

           A39: (g . s2) = FPG and

           A40: 0 <= s2 and

           A41: s2 <= 1;

          

           A42: g is continuous one-to-one by A36, TOPS_2:def 5;

          reconsider SEG as non empty Subset of (( TOP-REAL 2) | P);

          

           A43: ((( TOP-REAL 2) | P) | SEG) = (( TOP-REAL 2) | SE) by GOBOARD9: 2;

          ppi in [.ppi, pi1.] by A26, RCOMP_1:def 1;

          then ppi in (( dom F) /\ Poz) by A17, A30, XBOOLE_0:def 4;

          then

           A44: ppi in ( dom hh) by A27, RELAT_1: 61;

          then

           A45: (hh . ppi) = (f /. i) by A24, A27, FUNCT_1: 47;

          

           A46: ( dom hh) = ( [#] ( I[01] | Poz)) by A28, TOPS_2:def 5;

          then

           A47: ( dom hh) = Poz by PRE_TOPC:def 5;

          

           A48: ( rng hh) = (hh .: ( dom hh)) by A46, RELSET_1: 22

          .= ( [#] ((( TOP-REAL 2) | P) | SEG)) by A23, A35, A27, A47, RELAT_1: 129;

          let t be Real;

          assume that

           A49: 0 <= t and

           A50: t < s2;

          

           A51: t < 1 by A41, A50, XXREAL_0: 2;

          then

          reconsider w1 = s2, w2 = t as Point of ( Closed-Interval-TSpace ( 0 ,1)) by A40, A41, A49, BORSUK_1: 43, TOPMETR: 20;

          

           A52: F is one-to-one & ( rng F) = ( [#] (( TOP-REAL 2) | P)) by A13, TOPS_2:def 5;

          set H = ((hh " ) * g);

          

           A53: ( rng g) = ( [#] (( TOP-REAL 2) | SE)) by A36, TOPS_2:def 5;

          set ss = (H . t);

          

           A54: hh is one-to-one by A28, TOPS_2:def 5;

          

           A55: hh is one-to-one by A28, TOPS_2:def 5;

          then

           A56: ( dom (hh " )) = ( [#] ((( TOP-REAL 2) | P) | SEG)) by A43, A48, TOPS_2: 49;

          then

           A57: ( rng H) = ( rng (hh " )) by A53, RELAT_1: 28;

          

           A58: ( rng (hh " )) = ( [#] ( I[01] | Poz)) by A43, A55, A48, TOPS_2: 49

          .= Poz by PRE_TOPC:def 5;

          then ( rng H) = Poz by A53, A56, RELAT_1: 28;

          then

           A59: ( rng H) c= the carrier of ( Closed-Interval-TSpace (ppi,pi1)) by A20, TOPMETR: 18;

          hh is onto by A43, A48, FUNCT_2:def 3;

          then

           A60: (hh " ) = (hh qua Function " ) by A55, TOPS_2:def 4;

          

           A61: ( dom g) = ( [#] I[01] ) by A36, TOPS_2:def 5

          .= the carrier of I[01] ;

          then

           A62: ( dom H) = the carrier of ( Closed-Interval-TSpace ( 0 ,1)) by A43, A53, A56, RELAT_1: 27, TOPMETR: 20;

          

           A63: t in ( dom g) by A61, A49, A51, BORSUK_1: 43;

          then (g . t) in ( [#] (( TOP-REAL 2) | SE)) by A53, FUNCT_1:def 3;

          then

           A64: (g . t) in SEG by PRE_TOPC:def 5;

          then

          consider x be object such that

           A65: x in ( dom F) and

           A66: x in Poz and

           A67: (g . t) = (F . x) by A23, FUNCT_1:def 6;

          

           A68: F is one-to-one by A52;

          then

           A69: ((F qua Function " ) . (g . t)) in Poz by A65, A66, A67, FUNCT_1: 32;

          F is onto by A52, FUNCT_2:def 3;

          then

           A70: (F " ) = (F qua Function " ) by A52, TOPS_2:def 4;

          x = ((F qua Function " ) . (g . t)) by A68, A65, A67, FUNCT_1: 32;

          then ((F " ) . (g . t)) in Poz by A66, A70;

          then

           A71: ((F " ) . (g . t)) in ( dom ( id Poz)) by FUNCT_1: 17;

          (g . t) in the carrier of (( TOP-REAL 2) | P) by A64;

          then

           A72: (g . t) in ( dom (F " )) by A52, TOPS_2: 49;

          t in ( dom H) by A43, A53, A63, A56, RELAT_1: 27;

          

          then

           A73: (F . ss) = ((((hh " ) * g) qua Relation * F qua Relation) . t) by FUNCT_1: 13

          .= ((g qua Relation * ((hh " ) qua Relation * F qua Relation)) . t) by RELAT_1: 36

          .= ((F * (hh " )) . (g . t)) by A63, FUNCT_1: 13

          .= ((F * ((F qua Function " ) qua Relation * (( id Poz) qua Function " ) qua Relation)) . (g . t)) by A68, A29, A60, FUNCT_1: 44

          .= ((((F " ) qua Relation * (( id Poz) qua Function " ) qua Relation) * F qua Relation) . (g . t)) by A70

          .= (((F " ) qua Relation * ((( id Poz) qua Function " ) qua Relation * F qua Relation)) . (g . t)) by RELAT_1: 36

          .= (((F " ) qua Relation * (F * ( id Poz)) qua Relation) . (g . t)) by FUNCT_1: 45

          .= ((F * ( id Poz)) . ((F " ) . (g . t))) by A72, FUNCT_1: 13

          .= (F . (( id Poz) . ((F " ) . (g . t)))) by A71, FUNCT_1: 13

          .= (F . ((F qua Function " ) . (g . t))) by A69, A70, FUNCT_1: 17

          .= (g . t) by A52, A64, FUNCT_1: 35;

          1 in ( dom g) by A61, BORSUK_1: 43;

          

          then

           A74: (H . 1) = ((hh " ) . (f /. (i + 1))) by A38, FUNCT_1: 13

          .= pi1 by A54, A33, A34, A60, FUNCT_1: 32;

           0 in ( dom g) by A61, BORSUK_1: 43;

          

          then

           A75: (H . 0 ) = ((hh " ) . (f /. i)) by A37, FUNCT_1: 13

          .= ppi by A54, A44, A45, A60, FUNCT_1: 32;

          ( dom H) = ( dom g) by A43, A53, A56, RELAT_1: 27;

          then ss in Poz by A58, A63, A57, FUNCT_1:def 3;

          then ss in { l where l be Real : ppi <= l & l <= pi1 } by RCOMP_1:def 1;

          then

          consider ss9 be Real such that

           A76: ss9 = ss and

           A77: ppi <= ss9 and ss9 <= pi1;

          reconsider H as Function of ( Closed-Interval-TSpace ( 0 ,1)), ( Closed-Interval-TSpace (ppi,pi1)) by A62, A59, FUNCT_2: 2;

          

           A78: ss9 = (H . w2) by A76;

          ex z be object st z in ( dom F) & z in Poz & (F . s21) = (F . z) by A5, A16, A23, FUNCT_1:def 6;

          then

           A79: s21 in Poz by A15, A68, FUNCT_1:def 4;

          then (hh . s21) = (g . s2) by A16, A39, A27, FUNCT_1: 49;

          then s21 = ((hh qua Function " ) . (g . s2)) by A55, A47, A79, FUNCT_1: 32;

          then

           A80: s21 = ((hh " ) . (g . s2)) by A60;

          s2 in ( dom g) by A40, A41, A61, BORSUK_1: 43;

          then s21 = (H . w1) by A80, FUNCT_1: 13;

          then ss9 < s21 by A20, A50, A75, A74, A42, A32, A31, A78, JORDAN5A: 15, TOPMETR: 20;

          hence thesis by A1, A7, A6, A13, A14, A16, A18, A21, A76, A77, A73, Def1;

        end;

        

         A81: (( LSeg (f,i)) /\ Q) is closed by A2, TOPS_1: 8;

        (( LSeg (f,i)) /\ Q) <> {} by A5, A8, XBOOLE_0:def 4;

        then

         A82: ( LSeg (f,i)) meets Q;

        ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A4, TOPREAL1:def 3;

        then

         A83: R is_an_arc_of ((f /. i),(f /. (i + 1))) by A11, TOPREAL1: 9;

        FPG in (( LSeg (f,i)) /\ Q) by A5, A8, XBOOLE_0:def 4;

        hence thesis by A82, A81, A83, A19, Def1;

      end;

      hence thesis;

    end;

    theorem :: JORDAN5C:20

    

     Th20: for f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), i be Nat st ( L~ f) meets Q & Q is closed & f is being_S-Seq & 1 <= i & (i + 1) <= ( len f) & ( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) in ( LSeg (f,i)) holds ( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) = ( Last_Point (( LSeg (f,i)),(f /. i),(f /. (i + 1)),Q))

    proof

      let f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), i be Nat;

      assume that

       A1: ( L~ f) meets Q and

       A2: Q is closed and

       A3: f is being_S-Seq and

       A4: 1 <= i & (i + 1) <= ( len f) and

       A5: ( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) in ( LSeg (f,i));

      ( len f) >= 2 by A3, TOPREAL1:def 8;

      then

      reconsider P = ( L~ f), R = ( LSeg (f,i)) as non empty Subset of ( TOP-REAL 2) by A5, TOPREAL1: 23;

      

       A6: P is_an_arc_of ((f /. 1),(f /. ( len f))) by A3, TOPREAL1: 25;

      set FPO = ( Last_Point (R,(f /. i),(f /. (i + 1)),Q)), FPG = ( Last_Point (P,(f /. 1),(f /. ( len f)),Q));

      

       A7: (( L~ f) /\ Q) is closed by A2, TOPS_1: 8;

      then ( Last_Point (P,(f /. 1),(f /. ( len f)),Q)) in (( L~ f) /\ Q) by A1, A6, Def2;

      then

       A8: ( Last_Point (P,(f /. 1),(f /. ( len f)),Q)) in Q by XBOOLE_0:def 4;

      

       A9: (i + 1) in ( dom f) by A4, SEQ_4: 134;

      

       A10: f is one-to-one & i in ( dom f) by A3, A4, SEQ_4: 134, TOPREAL1:def 8;

      

       A11: (f /. i) <> (f /. (i + 1))

      proof

        assume (f /. i) = (f /. (i + 1));

        then i = (i + 1) by A10, A9, PARTFUN2: 10;

        hence thesis;

      end;

      FPG = FPO

      proof

        FPG in (( L~ f) /\ Q) by A1, A7, A6, Def2;

        then

         A12: FPG in ( L~ f) by XBOOLE_0:def 4;

        consider F be Function of I[01] , (( TOP-REAL 2) | P) such that

         A13: F is being_homeomorphism and

         A14: (F . 0 ) = (f /. 1) & (F . 1) = (f /. ( len f)) by A6, TOPREAL1:def 1;

        ( rng F) = ( [#] (( TOP-REAL 2) | P)) by A13, TOPS_2:def 5

        .= ( L~ f) by PRE_TOPC:def 5;

        then

        consider s21 be object such that

         A15: s21 in ( dom F) and

         A16: (F . s21) = FPG by A12, FUNCT_1:def 3;

        

         A17: ( dom F) = ( [#] I[01] ) by A13, TOPS_2:def 5

        .= [. 0 , 1.] by BORSUK_1: 40;

        then

        reconsider s21 as Real by A15;

        

         A18: 0 <= s21 & s21 <= 1 by A15, BORSUK_1: 43;

        

         A19: for g be Function of I[01] , (( TOP-REAL 2) | R), s2 be Real st g is being_homeomorphism & (g . 0 ) = (f /. i) & (g . 1) = (f /. (i + 1)) & (g . s2) = FPG & 0 <= s2 & s2 <= 1 holds for t be Real st 1 >= t & t > s2 holds not (g . t) in Q

        proof

          consider ppi,pi1 be Real such that

           A20: ppi < pi1 and

           A21: 0 <= ppi and ppi <= 1 and 0 <= pi1 and

           A22: pi1 <= 1 and

           A23: ( LSeg (f,i)) = (F .: [.ppi, pi1.]) and

           A24: (F . ppi) = (f /. i) and

           A25: (F . pi1) = (f /. (i + 1)) by A3, A4, A13, A14, JORDAN5B: 7;

          

           A26: ppi in { dd where dd be Real : ppi <= dd & dd <= pi1 } by A20;

          then

          reconsider Poz = [.ppi, pi1.] as non empty Subset of I[01] by A21, A22, BORSUK_1: 40, RCOMP_1:def 1, XXREAL_1: 34;

          

           A27: [.ppi, pi1.] c= [. 0 , 1.] by A21, A22, XXREAL_1: 34;

          reconsider A = ( Closed-Interval-TSpace (ppi,pi1)) as strict SubSpace of I[01] by A20, A21, A22, TOPMETR: 20, TREAL_1: 3;

          

           A28: Poz = ( [#] A) by A20, TOPMETR: 18;

          then

           A29: ( I[01] | Poz) = A by PRE_TOPC:def 5;

          ( Closed-Interval-TSpace (ppi,pi1)) is compact by A20, HEINE: 4;

          then ( [#] ( Closed-Interval-TSpace (ppi,pi1))) is compact by COMPTS_1: 1;

          then for P be Subset of A st P = Poz holds P is compact by A20, TOPMETR: 18;

          then Poz is compact by A28, COMPTS_1: 2;

          then

           A30: ( I[01] | Poz) is compact by COMPTS_1: 3;

          reconsider Lf = ( L~ f) as non empty Subset of ( TOP-REAL 2) by A6;

          let g be Function of I[01] , (( TOP-REAL 2) | R), s2 be Real;

          assume that

           A31: g is being_homeomorphism and

           A32: (g . 0 ) = (f /. i) and

           A33: (g . 1) = (f /. (i + 1)) and

           A34: (g . s2) = FPG and

           A35: 0 <= s2 and

           A36: s2 <= 1;

          the carrier of (( TOP-REAL 2) | Lf) = ( [#] (( TOP-REAL 2) | Lf))

          .= Lf by PRE_TOPC:def 5;

          then

          reconsider SEG = ( LSeg (f,i)) as non empty Subset of (( TOP-REAL 2) | Lf) by A5, TOPREAL3: 19;

          reconsider SE = SEG as non empty Subset of ( TOP-REAL 2);

          

           A37: ( rng g) = ( [#] (( TOP-REAL 2) | SE)) by A31, TOPS_2:def 5;

          set gg = (F | Poz);

          

           A38: the carrier of ( I[01] | Poz) = ( [#] ( I[01] | Poz))

          .= Poz by PRE_TOPC:def 5;

          then

          reconsider gg as Function of ( I[01] | Poz), (( TOP-REAL 2) | P) by FUNCT_2: 32;

          let t be Real;

          assume that

           A39: 1 >= t and

           A40: t > s2;

          

           A41: ( rng gg) c= SEG

          proof

            let ii be object;

            assume ii in ( rng gg);

            then

            consider j be object such that

             A42: j in ( dom gg) and

             A43: ii = (gg . j) by FUNCT_1:def 3;

            j in (( dom F) /\ Poz) by A42, RELAT_1: 61;

            then j in ( dom F) by XBOOLE_0:def 4;

            then (F . j) in ( LSeg (f,i)) by A23, A38, A42, FUNCT_1:def 6;

            hence thesis by A38, A42, A43, FUNCT_1: 49;

          end;

          

           A44: the carrier of ((( TOP-REAL 2) | Lf) | SEG) = ( [#] ((( TOP-REAL 2) | Lf) | SEG))

          .= SEG by PRE_TOPC:def 5;

          reconsider SEG as non empty Subset of (( TOP-REAL 2) | Lf);

          reconsider hh9 = gg as Function of ( I[01] | Poz), ((( TOP-REAL 2) | Lf) | SEG) by A44, A41, FUNCT_2: 6;

          reconsider hh = hh9 as Function of ( I[01] | Poz), (( TOP-REAL 2) | SE) by GOBOARD9: 2;

          

           A45: ( dom hh) = ( [#] ( I[01] | Poz)) by FUNCT_2:def 1;

          then

           A46: ( dom hh) = Poz by PRE_TOPC:def 5;

          

           A47: ( rng hh) = (hh .: ( dom hh)) by A45, RELSET_1: 22

          .= ( [#] ((( TOP-REAL 2) | Lf) | SEG)) by A23, A44, A46, RELAT_1: 129;

          

           A48: F is one-to-one by A13, TOPS_2:def 5;

          then

           A49: hh is one-to-one by FUNCT_1: 52;

          set H = ((hh " ) * g);

          

           A50: ((( TOP-REAL 2) | Lf) | SEG) = (( TOP-REAL 2) | SE) by GOBOARD9: 2;

          

           A51: hh9 is one-to-one by A48, FUNCT_1: 52;

          then

           A52: ( dom (hh " )) = ( [#] ((( TOP-REAL 2) | Lf) | SEG)) by A50, A47, TOPS_2: 49;

          then

           A53: ( rng H) = ( rng (hh " )) by A37, RELAT_1: 28;

          

           A54: ( dom g) = ( [#] I[01] ) by A31, TOPS_2:def 5

          .= the carrier of I[01] ;

          then

           A55: ( dom H) = the carrier of ( Closed-Interval-TSpace ( 0 ,1)) by A50, A37, A52, RELAT_1: 27, TOPMETR: 20;

          

           A56: t in ( dom g) by A35, A54, A39, A40, BORSUK_1: 43;

          then (g . t) in ( [#] (( TOP-REAL 2) | SE)) by A37, FUNCT_1:def 3;

          then

           A57: (g . t) in SEG by PRE_TOPC:def 5;

          then

          consider x be object such that

           A58: x in ( dom F) and

           A59: x in Poz and

           A60: (g . t) = (F . x) by A23, FUNCT_1:def 6;

          hh is onto by A50, A47, FUNCT_2:def 3;

          then

           A61: (hh " ) = (hh qua Function " ) by A51, TOPS_2:def 4;

          

           A62: ((F qua Function " ) . (g . t)) in Poz by A48, A58, A59, A60, FUNCT_1: 32;

          ex z be object st z in ( dom F) & z in Poz & (F . s21) = (F . z) by A5, A16, A23, FUNCT_1:def 6;

          then

           A63: s21 in Poz by A15, A48, FUNCT_1:def 4;

          then (hh . s21) = (g . s2) by A16, A34, FUNCT_1: 49;

          then s21 = ((hh qua Function " ) . (g . s2)) by A51, A46, A63, FUNCT_1: 32;

          then

           A64: s21 = ((hh " ) . (g . s2)) by A61;

          

           A65: g is continuous one-to-one by A31, TOPS_2:def 5;

          

           A66: (( TOP-REAL 2) | SE) is T_2 by TOPMETR: 2;

          reconsider w1 = s2, w2 = t as Point of ( Closed-Interval-TSpace ( 0 ,1)) by A35, A36, A39, A40, BORSUK_1: 43, TOPMETR: 20;

          

           A67: hh = (F * ( id Poz)) by RELAT_1: 65;

          set ss = (H . t);

          

           A68: F is one-to-one & ( rng F) = ( [#] (( TOP-REAL 2) | P)) by A13, TOPS_2:def 5;

          

           A69: ( rng (hh " )) = ( [#] ( I[01] | Poz)) by A50, A51, A47, TOPS_2: 49

          .= Poz by PRE_TOPC:def 5;

          then ( rng H) = Poz by A37, A52, RELAT_1: 28;

          then

           A70: ( rng H) c= the carrier of ( Closed-Interval-TSpace (ppi,pi1)) by A20, TOPMETR: 18;

          ( dom H) = ( dom g) by A50, A37, A52, RELAT_1: 27;

          then ss in Poz by A69, A56, A53, FUNCT_1:def 3;

          then ss in { l where l be Real : ppi <= l & l <= pi1 } by RCOMP_1:def 1;

          then

          consider ss9 be Real such that

           A71: ss9 = ss and ppi <= ss9 and

           A72: ss9 <= pi1;

          F is onto by A68, FUNCT_2:def 3;

          then

           A73: (F " ) = (F qua Function " ) by A68, TOPS_2:def 4;

          

           A74: 1 >= ss9 by A22, A72, XXREAL_0: 2;

          x = ((F qua Function " ) . (g . t)) by A48, A58, A60, FUNCT_1: 32;

          then ((F " ) . (g . t)) in Poz by A59, A73;

          then

           A75: ((F " ) . (g . t)) in ( dom ( id Poz)) by FUNCT_1: 17;

          (g . t) in the carrier of (( TOP-REAL 2) | Lf) by A57;

          then

           A76: (g . t) in ( dom (F " )) by A68, TOPS_2: 49;

          t in ( dom H) by A50, A37, A56, A52, RELAT_1: 27;

          

          then

           A77: (F . ss) = ((((hh " ) * g) qua Relation * F qua Relation) . t) by FUNCT_1: 13

          .= ((g qua Relation * ((hh " ) qua Relation * F qua Relation)) . t) by RELAT_1: 36

          .= ((F * (hh " )) . (g . t)) by A56, FUNCT_1: 13

          .= ((F * (hh qua Function " )) . (g . t)) by A61

          .= ((F * ((F qua Function " ) qua Relation * (( id Poz) qua Function " ) qua Relation)) . (g . t)) by A48, A67, FUNCT_1: 44

          .= ((((F " ) qua Relation * (( id Poz) qua Function " ) qua Relation) * F qua Relation) . (g . t)) by A73

          .= (((F " ) qua Relation * ((( id Poz) qua Function " ) qua Relation * F qua Relation)) . (g . t)) by RELAT_1: 36

          .= (((F " ) qua Relation * (F * ( id Poz)) qua Relation) . (g . t)) by FUNCT_1: 45

          .= ((F * ( id Poz)) . ((F " ) . (g . t))) by A76, FUNCT_1: 13

          .= (F . (( id Poz) . ((F " ) . (g . t)))) by A75, FUNCT_1: 13

          .= (F . (( id Poz) . ((F qua Function " ) . (g . t)))) by A73

          .= (F . ((F qua Function " ) . (g . t))) by A62, FUNCT_1: 17

          .= (g . t) by A68, A57, FUNCT_1: 35;

          pi1 in { dd where dd be Real : ppi <= dd & dd <= pi1 } by A20;

          then pi1 in [.ppi, pi1.] by RCOMP_1:def 1;

          then pi1 in (( dom F) /\ Poz) by A17, A27, XBOOLE_0:def 4;

          then

           A78: pi1 in ( dom hh) by RELAT_1: 61;

          then

           A79: (hh . pi1) = (f /. (i + 1)) by A25, FUNCT_1: 47;

          F is continuous by A13, TOPS_2:def 5;

          then gg is continuous by TOPMETR: 7;

          then hh is being_homeomorphism by A50, A51, A47, A30, A66, COMPTS_1: 17, TOPMETR: 6;

          then (hh " ) is being_homeomorphism by TOPS_2: 56;

          then

           A80: (hh " ) is continuous one-to-one by TOPS_2:def 5;

          ppi in [.ppi, pi1.] by A26, RCOMP_1:def 1;

          then ppi in (( dom F) /\ Poz) by A17, A27, XBOOLE_0:def 4;

          then

           A81: ppi in ( dom hh) by RELAT_1: 61;

          then

           A82: (hh . ppi) = (f /. i) by A24, FUNCT_1: 47;

          1 in ( dom g) by A54, BORSUK_1: 43;

          

          then

           A83: (H . 1) = ((hh " ) . (f /. (i + 1))) by A33, FUNCT_1: 13

          .= pi1 by A49, A78, A79, A61, FUNCT_1: 32;

           0 in ( dom g) by A54, BORSUK_1: 43;

          

          then

           A84: (H . 0 ) = ((hh " ) . (f /. i)) by A32, FUNCT_1: 13

          .= ppi by A49, A81, A82, A61, FUNCT_1: 32;

          reconsider H as Function of ( Closed-Interval-TSpace ( 0 ,1)), ( Closed-Interval-TSpace (ppi,pi1)) by A55, A70, FUNCT_2: 2;

          s2 in ( dom g) by A35, A36, A54, BORSUK_1: 43;

          then

           A85: s21 = (H . w1) by A64, FUNCT_1: 13;

          ss9 = (H . w2) by A71;

          then ss9 > s21 by A20, A40, A84, A83, A65, A80, A29, A85, JORDAN5A: 15, TOPMETR: 20;

          hence thesis by A1, A7, A6, A13, A14, A16, A18, A71, A74, A77, Def2;

        end;

        

         A86: (( LSeg (f,i)) /\ Q) is closed by A2, TOPS_1: 8;

        (( LSeg (f,i)) /\ Q) <> {} by A5, A8, XBOOLE_0:def 4;

        then

         A87: ( LSeg (f,i)) meets Q;

        ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A4, TOPREAL1:def 3;

        then

         A88: R is_an_arc_of ((f /. i),(f /. (i + 1))) by A11, TOPREAL1: 9;

        FPG in (( LSeg (f,i)) /\ Q) by A5, A8, XBOOLE_0:def 4;

        hence thesis by A87, A86, A88, A19, Def2;

      end;

      hence thesis;

    end;

    theorem :: JORDAN5C:21

    for f be FinSequence of ( TOP-REAL 2), i be Nat st 1 <= i & (i + 1) <= ( len f) & f is being_S-Seq & ( First_Point (( L~ f),(f /. 1),(f /. ( len f)),( LSeg (f,i)))) in ( LSeg (f,i)) holds ( First_Point (( L~ f),(f /. 1),(f /. ( len f)),( LSeg (f,i)))) = (f /. i)

    proof

      let f be FinSequence of ( TOP-REAL 2), i be Nat;

      assume that

       A1: 1 <= i & (i + 1) <= ( len f) and

       A2: f is being_S-Seq and

       A3: ( First_Point (( L~ f),(f /. 1),(f /. ( len f)),( LSeg (f,i)))) in ( LSeg (f,i));

      reconsider Q = ( LSeg (f,i)) as non empty Subset of ( TOP-REAL 2) by A3;

      Q = ( LSeg ((f /. i),(f /. (i + 1)))) by A1, TOPREAL1:def 3;

      then Q c= ( L~ f) by A1, SPPOL_2: 16;

      then ( L~ f) meets Q by A3, XBOOLE_0: 3;

      then

       A4: ( First_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) = ( First_Point (Q,(f /. i),(f /. (i + 1)),Q)) by A1, A2, A3, Th19;

      Q is closed & Q is_an_arc_of ((f /. i),(f /. (i + 1))) by A1, A2, JORDAN5B: 15;

      hence thesis by A4, Th7;

    end;

    theorem :: JORDAN5C:22

    for f be FinSequence of ( TOP-REAL 2), i be Nat st 1 <= i & (i + 1) <= ( len f) & f is being_S-Seq & ( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),( LSeg (f,i)))) in ( LSeg (f,i)) holds ( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),( LSeg (f,i)))) = (f /. (i + 1))

    proof

      let f be FinSequence of ( TOP-REAL 2), i be Nat;

      assume that

       A1: 1 <= i & (i + 1) <= ( len f) and

       A2: f is being_S-Seq and

       A3: ( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),( LSeg (f,i)))) in ( LSeg (f,i));

      reconsider Q = ( LSeg (f,i)) as non empty Subset of ( TOP-REAL 2) by A3;

      Q = ( LSeg ((f /. i),(f /. (i + 1)))) by A1, TOPREAL1:def 3;

      then Q c= ( L~ f) by A1, SPPOL_2: 16;

      then ( L~ f) meets Q by A3, XBOOLE_0: 3;

      then

       A4: ( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) = ( Last_Point (Q,(f /. i),(f /. (i + 1)),Q)) by A1, A2, A3, Th20;

      Q is closed & Q is_an_arc_of ((f /. i),(f /. (i + 1))) by A1, A2, JORDAN5B: 15;

      hence thesis by A4, Th7;

    end;

    theorem :: JORDAN5C:23

    

     Th23: for f be FinSequence of ( TOP-REAL 2), i be Nat st f is being_S-Seq & 1 <= i & (i + 1) <= ( len f) holds LE ((f /. i),(f /. (i + 1)),( L~ f),(f /. 1),(f /. ( len f)))

    proof

      let f be FinSequence of ( TOP-REAL 2), i be Nat;

      assume that

       A1: f is being_S-Seq and

       A2: 1 <= i & (i + 1) <= ( len f);

      set p1 = (f /. 1), p2 = (f /. ( len f)), q1 = (f /. i), q2 = (f /. (i + 1));

      

       A3: ( len f) >= 2 by A1, TOPREAL1:def 8;

      then

      reconsider P = ( L~ f) as non empty Subset of ( TOP-REAL 2) by TOPREAL1: 23;

      (i + 1) in ( dom f) by A2, SEQ_4: 134;

      then

       A4: q2 in P by A3, GOBOARD1: 1;

      

       A5: for g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s1) = q1 & 0 <= s1 & s1 <= 1 & (g . s2) = q2 & 0 <= s2 & s2 <= 1 holds s1 <= s2

      proof

        let g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real;

        assume that

         A6: g is being_homeomorphism and

         A7: (g . 0 ) = p1 & (g . 1) = p2 and

         A8: (g . s1) = q1 and

         A9: 0 <= s1 & s1 <= 1 and

         A10: (g . s2) = q2 and

         A11: 0 <= s2 & s2 <= 1;

        

         A12: ( dom g) = ( [#] I[01] ) by A6, TOPS_2:def 5

        .= the carrier of I[01] ;

        then

         A13: s1 in ( dom g) by A9, BORSUK_1: 43;

        

         A14: s2 in ( dom g) by A11, A12, BORSUK_1: 43;

        

         A15: g is one-to-one by A6, TOPS_2:def 5;

        consider r1,r2 be Real such that

         A16: r1 < r2 and

         A17: 0 <= r1 and

         A18: r1 <= 1 and 0 <= r2 and

         A19: r2 <= 1 and ( LSeg (f,i)) = (g .: [.r1, r2.]) and

         A20: (g . r1) = q1 and

         A21: (g . r2) = q2 by A1, A2, A6, A7, JORDAN5B: 7;

        

         A22: r2 in ( dom g) by A16, A17, A19, A12, BORSUK_1: 43;

        r1 in ( dom g) by A17, A18, A12, BORSUK_1: 43;

        then s1 = r1 by A8, A20, A13, A15, FUNCT_1:def 4;

        hence thesis by A10, A16, A21, A22, A14, A15, FUNCT_1:def 4;

      end;

      i in ( dom f) by A2, SEQ_4: 134;

      then q1 in P by A3, GOBOARD1: 1;

      hence thesis by A4, A5;

    end;

    theorem :: JORDAN5C:24

    

     Th24: for f be FinSequence of ( TOP-REAL 2), i,j be Nat st f is being_S-Seq & 1 <= i & i <= j & j <= ( len f) holds LE ((f /. i),(f /. j),( L~ f),(f /. 1),(f /. ( len f)))

    proof

      let f be FinSequence of ( TOP-REAL 2), i,j be Nat such that

       A1: f is being_S-Seq and

       A2: 1 <= i and

       A3: i <= j and

       A4: j <= ( len f);

      consider k be Nat such that

       A5: (i + k) = j by A3, NAT_1: 10;

      

       A6: ( len f) >= 2 by A1, TOPREAL1:def 8;

      then

      reconsider P = ( L~ f) as non empty Subset of ( TOP-REAL 2) by TOPREAL1: 23;

      defpred ILE[ Nat] means 1 <= i & (i + $1) <= ( len f) implies LE ((f /. i),(f /. (i + $1)),P,(f /. 1),(f /. ( len f)));

      

       A7: for l be Nat st ILE[l] holds ILE[(l + 1)]

      proof

        let l be Nat;

        assume

         A8: ILE[l];

        

         A9: (i + l) <= ((i + l) + 1) by NAT_1: 11;

        assume that

         A10: 1 <= i and

         A11: (i + (l + 1)) <= ( len f);

        

         A12: ((i + l) + 1) <= ( len f) by A11;

        i <= (i + l) by NAT_1: 11;

        then 1 <= (i + l) by A10, XXREAL_0: 2;

        then LE ((f /. (i + l)),(f /. (i + (l + 1))),P,(f /. 1),(f /. ( len f))) by A1, A12, Th23;

        hence thesis by A8, A10, A11, A9, Th13, XXREAL_0: 2;

      end;

      

       A13: ILE[ 0 ]

      proof

        assume 1 <= i & (i + 0 ) <= ( len f);

        then i in ( dom f) by FINSEQ_3: 25;

        hence thesis by A6, Th9, GOBOARD1: 1;

      end;

      

       A14: for l be Nat holds ILE[l] from NAT_1:sch 2( A13, A7);

      thus thesis by A2, A4, A5, A14;

    end;

    

     Lm1: for f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i be Nat st ( LSeg (f,i)) meets Q & f is being_S-Seq & Q is closed & 1 <= i & (i + 1) <= ( len f) & q in ( LSeg (f,i)) & q in Q holds LE (( First_Point (( LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)),q,(f /. i),(f /. (i + 1)))

    proof

      let f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i be Nat;

      assume that

       A1: ( LSeg (f,i)) meets Q and

       A2: f is being_S-Seq and

       A3: Q is closed and

       A4: 1 <= i & (i + 1) <= ( len f) and

       A5: q in ( LSeg (f,i)) and

       A6: q in Q;

      reconsider P = ( LSeg (f,i)) as non empty Subset of ( TOP-REAL 2) by A5;

      set q1 = ( First_Point (P,(f /. i),(f /. (i + 1)),Q)), p1 = (f /. i), p2 = (f /. (i + 1));

      

       A7: (P /\ Q) c= P by XBOOLE_1: 17;

      

       A8: (i + 1) in ( dom f) by A4, SEQ_4: 134;

      

       A9: f is one-to-one & i in ( dom f) by A2, A4, SEQ_4: 134, TOPREAL1:def 8;

      

       A10: p1 <> p2

      proof

        assume p1 = p2;

        then i = (i + 1) by A9, A8, PARTFUN2: 10;

        hence thesis;

      end;

      

       A11: (P /\ Q) is closed by A3, TOPS_1: 8;

      P is_an_arc_of ((f /. i),(f /. (i + 1))) by A2, A4, JORDAN5B: 15;

      then q1 in (P /\ Q) & for g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s1) = q1 & 0 <= s1 & s1 <= 1 & (g . s2) = q & 0 <= s2 & s2 <= 1 holds s1 <= s2 by A1, A6, A11, Def1;

      then

       A12: LE (q1,q,P,p1,p2) by A5, A7;

      ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A4, TOPREAL1:def 3;

      hence thesis by A10, A12, Th17;

    end;

    

     Lm2: for f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i be Nat st ( L~ f) meets Q & f is being_S-Seq & Q is closed & ( First_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) in ( LSeg (f,i)) & 1 <= i & (i + 1) <= ( len f) & q in ( LSeg (f,i)) & q in Q holds LE (( First_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)),q,(f /. i),(f /. (i + 1)))

    proof

      let f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i be Nat;

      assume that

       A1: ( L~ f) meets Q and

       A2: f is being_S-Seq and

       A3: Q is closed and

       A4: ( First_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) in ( LSeg (f,i)) and

       A5: 1 <= i & (i + 1) <= ( len f) and

       A6: q in ( LSeg (f,i)) & q in Q;

      ( len f) >= 2 by A2, TOPREAL1:def 8;

      then

      reconsider P = ( L~ f), R = ( LSeg (f,i)) as non empty Subset of ( TOP-REAL 2) by A4, TOPREAL1: 23;

      (( LSeg (f,i)) /\ Q) <> {} by A6, XBOOLE_0:def 4;

      then

       A7: ( LSeg (f,i)) meets Q;

      ( First_Point (P,(f /. 1),(f /. ( len f)),Q)) = ( First_Point (R,(f /. i),(f /. (i + 1)),Q)) by A1, A2, A3, A4, A5, Th19;

      hence thesis by A2, A3, A5, A6, A7, Lm1;

    end;

    

     Lm3: for f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i be Nat st ( LSeg (f,i)) meets Q & f is being_S-Seq & Q is closed & 1 <= i & (i + 1) <= ( len f) & q in ( LSeg (f,i)) & q in Q holds LE (q,( Last_Point (( LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)),(f /. i),(f /. (i + 1)))

    proof

      let f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i be Nat;

      assume that

       A1: ( LSeg (f,i)) meets Q and

       A2: f is being_S-Seq and

       A3: Q is closed and

       A4: 1 <= i & (i + 1) <= ( len f) and

       A5: q in ( LSeg (f,i)) and

       A6: q in Q;

      reconsider P = ( LSeg (f,i)) as non empty Subset of ( TOP-REAL 2) by A5;

      set q1 = ( Last_Point (P,(f /. i),(f /. (i + 1)),Q)), p1 = (f /. i), p2 = (f /. (i + 1));

      

       A7: (P /\ Q) c= P by XBOOLE_1: 17;

      

       A8: (i + 1) in ( dom f) by A4, SEQ_4: 134;

      

       A9: f is one-to-one & i in ( dom f) by A2, A4, SEQ_4: 134, TOPREAL1:def 8;

      

       A10: p1 <> p2

      proof

        assume p1 = p2;

        then i = (i + 1) by A9, A8, PARTFUN2: 10;

        hence thesis;

      end;

      

       A11: (P /\ Q) is closed by A3, TOPS_1: 8;

      P is_an_arc_of ((f /. i),(f /. (i + 1))) by A2, A4, JORDAN5B: 15;

      then q1 in (P /\ Q) & for g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s1) = q & 0 <= s1 & s1 <= 1 & (g . s2) = q1 & 0 <= s2 & s2 <= 1 holds s1 <= s2 by A1, A6, A11, Def2;

      then

       A12: LE (q,q1,P,p1,p2) by A5, A7;

      ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A4, TOPREAL1:def 3;

      hence thesis by A10, A12, Th17;

    end;

    

     Lm4: for f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i be Nat st ( L~ f) meets Q & f is being_S-Seq & Q is closed & ( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) in ( LSeg (f,i)) & 1 <= i & (i + 1) <= ( len f) & q in ( LSeg (f,i)) & q in Q holds LE (q,( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)),(f /. i),(f /. (i + 1)))

    proof

      let f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i be Nat;

      assume that

       A1: ( L~ f) meets Q and

       A2: f is being_S-Seq and

       A3: Q is closed and

       A4: ( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) in ( LSeg (f,i)) and

       A5: 1 <= i & (i + 1) <= ( len f) and

       A6: q in ( LSeg (f,i)) & q in Q;

      ( len f) >= 2 by A2, TOPREAL1:def 8;

      then

      reconsider P = ( L~ f), R = ( LSeg (f,i)) as non empty Subset of ( TOP-REAL 2) by A4, TOPREAL1: 23;

      (( LSeg (f,i)) /\ Q) <> {} by A6, XBOOLE_0:def 4;

      then

       A7: ( LSeg (f,i)) meets Q;

      ( Last_Point (P,(f /. 1),(f /. ( len f)),Q)) = ( Last_Point (R,(f /. i),(f /. (i + 1)),Q)) by A1, A2, A3, A4, A5, Th20;

      hence thesis by A2, A3, A5, A6, A7, Lm3;

    end;

    theorem :: JORDAN5C:25

    

     Th25: for f be FinSequence of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i be Nat st f is being_S-Seq & 1 <= i & (i + 1) <= ( len f) & q in ( LSeg (f,i)) holds LE ((f /. i),q,( L~ f),(f /. 1),(f /. ( len f)))

    proof

      let f be FinSequence of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i be Nat;

      assume that

       A1: f is being_S-Seq and

       A2: 1 <= i & (i + 1) <= ( len f) and

       A3: q in ( LSeg (f,i));

      set p1 = (f /. 1), p2 = (f /. ( len f)), q1 = (f /. i);

      

       A4: 2 <= ( len f) by A1, TOPREAL1:def 8;

      then

      reconsider P = ( L~ f) as non empty Subset of ( TOP-REAL 2) by TOPREAL1: 23;

      i in ( dom f) by A2, SEQ_4: 134;

      then

       A5: q1 in P by A4, GOBOARD1: 1;

      

       A6: for g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s1) = q1 & 0 <= s1 & s1 <= 1 & (g . s2) = q & 0 <= s2 & s2 <= 1 holds s1 <= s2

      proof

        let g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real;

        assume that

         A7: g is being_homeomorphism and

         A8: (g . 0 ) = p1 & (g . 1) = p2 and

         A9: (g . s1) = q1 and

         A10: 0 <= s1 & s1 <= 1 and

         A11: (g . s2) = q and

         A12: 0 <= s2 & s2 <= 1;

        

         A13: ( dom g) = ( [#] I[01] ) by A7, TOPS_2:def 5

        .= the carrier of I[01] ;

        then

         A14: s1 in ( dom g) by A10, BORSUK_1: 43;

        consider r1,r2 be Real such that r1 < r2 and

         A15: 0 <= r1 & r1 <= 1 and 0 <= r2 and r2 <= 1 and

         A16: ( LSeg (f,i)) = (g .: [.r1, r2.]) and

         A17: (g . r1) = q1 and (g . r2) = (f /. (i + 1)) by A1, A2, A7, A8, JORDAN5B: 7;

        consider r39 be object such that

         A18: r39 in ( dom g) and

         A19: r39 in [.r1, r2.] and

         A20: (g . r39) = q by A3, A16, FUNCT_1:def 6;

        r39 in { l where l be Real : r1 <= l & l <= r2 } by A19, RCOMP_1:def 1;

        then

        consider r3 be Real such that

         A21: r3 = r39 and

         A22: r1 <= r3 and r3 <= r2;

        

         A23: g is one-to-one by A7, TOPS_2:def 5;

        

         A24: r1 in ( dom g) by A15, A13, BORSUK_1: 43;

        s2 in ( dom g) by A12, A13, BORSUK_1: 43;

        then s2 = r3 by A11, A18, A20, A21, A23, FUNCT_1:def 4;

        hence thesis by A9, A17, A22, A24, A14, A23, FUNCT_1:def 4;

      end;

      q in P by A3, SPPOL_2: 17;

      hence thesis by A5, A6;

    end;

    theorem :: JORDAN5C:26

    

     Th26: for f be FinSequence of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i be Nat st f is being_S-Seq & 1 <= i & (i + 1) <= ( len f) & q in ( LSeg (f,i)) holds LE (q,(f /. (i + 1)),( L~ f),(f /. 1),(f /. ( len f)))

    proof

      let f be FinSequence of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i be Nat;

      assume that

       A1: f is being_S-Seq and

       A2: 1 <= i & (i + 1) <= ( len f) and

       A3: q in ( LSeg (f,i));

      ( len f) >= 2 by A1, TOPREAL1:def 8;

      then

      reconsider P = ( L~ f) as non empty Subset of ( TOP-REAL 2) by TOPREAL1: 23;

      set p1 = (f /. 1), p2 = (f /. ( len f)), q1 = (f /. (i + 1));

      q1 in ( LSeg (f,i)) by A2, TOPREAL1: 21;

      then

       A4: q1 in P by SPPOL_2: 17;

      

       A5: for g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s1) = q & 0 <= s1 & s1 <= 1 & (g . s2) = q1 & 0 <= s2 & s2 <= 1 holds s1 <= s2

      proof

        let g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real;

        assume that

         A6: g is being_homeomorphism and

         A7: (g . 0 ) = p1 & (g . 1) = p2 and

         A8: (g . s1) = q and

         A9: 0 <= s1 & s1 <= 1 and

         A10: (g . s2) = q1 and

         A11: 0 <= s2 & s2 <= 1;

        

         A12: ( dom g) = ( [#] I[01] ) by A6, TOPS_2:def 5

        .= the carrier of I[01] ;

        then

         A13: s2 in ( dom g) by A11, BORSUK_1: 43;

        consider r1,r2 be Real such that

         A14: r1 < r2 & 0 <= r1 and r1 <= 1 and 0 <= r2 and

         A15: r2 <= 1 and

         A16: ( LSeg (f,i)) = (g .: [.r1, r2.]) and (g . r1) = (f /. i) and

         A17: (g . r2) = q1 by A1, A2, A6, A7, JORDAN5B: 7;

        

         A18: r2 in ( dom g) by A14, A15, A12, BORSUK_1: 43;

        consider r39 be object such that

         A19: r39 in ( dom g) and

         A20: r39 in [.r1, r2.] and

         A21: (g . r39) = q by A3, A16, FUNCT_1:def 6;

        r39 in { l where l be Real : r1 <= l & l <= r2 } by A20, RCOMP_1:def 1;

        then

        consider r3 be Real such that

         A22: r3 = r39 and r1 <= r3 and

         A23: r3 <= r2;

        

         A24: g is one-to-one by A6, TOPS_2:def 5;

        s1 in ( dom g) by A9, A12, BORSUK_1: 43;

        then s1 = r3 by A8, A19, A21, A22, A24, FUNCT_1:def 4;

        hence thesis by A10, A17, A23, A18, A13, A24, FUNCT_1:def 4;

      end;

      q in P by A3, SPPOL_2: 17;

      hence thesis by A4, A5;

    end;

    theorem :: JORDAN5C:27

    for f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i,j be Nat st ( L~ f) meets Q & f is being_S-Seq & Q is closed & ( First_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) in ( LSeg (f,i)) & 1 <= i & (i + 1) <= ( len f) & q in ( LSeg (f,j)) & 1 <= j & (j + 1) <= ( len f) & q in Q & ( First_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) <> q holds i <= j & (i = j implies LE (( First_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)),q,(f /. i),(f /. (i + 1))))

    proof

      let f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i,j be Nat;

      assume that

       A1: ( L~ f) meets Q and

       A2: f is being_S-Seq and

       A3: Q is closed and

       A4: ( First_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) in ( LSeg (f,i)) and

       A5: 1 <= i and

       A6: (i + 1) <= ( len f) and

       A7: q in ( LSeg (f,j)) and

       A8: 1 <= j & (j + 1) <= ( len f) and

       A9: q in Q and

       A10: ( First_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) <> q;

      reconsider P = ( L~ f) as non empty Subset of ( TOP-REAL 2) by A4, SPPOL_2: 17;

      set q1 = ( First_Point (P,(f /. 1),(f /. ( len f)),Q)), p1 = (f /. i);

      

       A11: q in ( L~ f) by A7, SPPOL_2: 17;

      thus i <= j

      proof

        (( L~ f) /\ Q) is closed by A3, TOPS_1: 8;

        then

         A12: LE (q1,q,P,(f /. 1),(f /. ( len f))) by A2, A9, A11, Th15;

        

         A13: LE (q,(f /. (j + 1)),P,(f /. 1),(f /. ( len f))) by A2, A7, A8, Th26;

        i <= (i + 1) by NAT_1: 11;

        then

         A14: i <= ( len f) by A6, XXREAL_0: 2;

        assume j < i;

        then

         A15: (j + 1) <= i by NAT_1: 13;

        1 <= (j + 1) by NAT_1: 11;

        then LE ((f /. (j + 1)),p1,P,(f /. 1),(f /. ( len f))) by A2, A15, A14, Th24;

        then

         A16: LE (q,p1,P,(f /. 1),(f /. ( len f))) by A13, Th13;

         LE (p1,q1,P,(f /. 1),(f /. ( len f))) by A2, A4, A5, A6, Th25;

        then LE (q,q1,P,(f /. 1),(f /. ( len f))) by A16, Th13;

        hence contradiction by A2, A10, A12, Th12, TOPREAL1: 25;

      end;

      assume i = j;

      hence thesis by A1, A2, A3, A4, A5, A6, A7, A9, Lm2;

    end;

    theorem :: JORDAN5C:28

    for f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i,j be Nat st ( L~ f) meets Q & f is being_S-Seq & Q is closed & ( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) in ( LSeg (f,i)) & 1 <= i & (i + 1) <= ( len f) & q in ( LSeg (f,j)) & 1 <= j & (j + 1) <= ( len f) & q in Q & ( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) <> q holds i >= j & (i = j implies LE (q,( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)),(f /. i),(f /. (i + 1))))

    proof

      let f be FinSequence of ( TOP-REAL 2), Q be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2), i,j be Nat;

      assume that

       A1: ( L~ f) meets Q and

       A2: f is being_S-Seq and

       A3: Q is closed and

       A4: ( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) in ( LSeg (f,i)) and

       A5: 1 <= i & (i + 1) <= ( len f) and

       A6: q in ( LSeg (f,j)) and

       A7: 1 <= j and

       A8: (j + 1) <= ( len f) and

       A9: q in Q and

       A10: ( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),Q)) <> q;

      reconsider P = ( L~ f) as non empty Subset of ( TOP-REAL 2) by A4, SPPOL_2: 17;

      set q1 = ( Last_Point (P,(f /. 1),(f /. ( len f)),Q)), p2 = (f /. (i + 1));

      

       A11: q in ( L~ f) by A6, SPPOL_2: 17;

      thus i >= j

      proof

        assume j > i;

        then

         A12: (i + 1) <= j by NAT_1: 13;

        j <= (j + 1) by NAT_1: 11;

        then 1 <= (i + 1) & j <= ( len f) by A8, NAT_1: 11, XXREAL_0: 2;

        then

         A13: LE (p2,(f /. j),P,(f /. 1),(f /. ( len f))) by A2, A12, Th24;

         LE ((f /. j),q,P,(f /. 1),(f /. ( len f))) by A2, A6, A7, A8, Th25;

        then

         A14: LE (p2,q,P,(f /. 1),(f /. ( len f))) by A13, Th13;

        (( L~ f) /\ Q) is closed by A3, TOPS_1: 8;

        then

         A15: LE (q,q1,P,(f /. 1),(f /. ( len f))) by A2, A9, A11, Th16;

         LE (q1,p2,P,(f /. 1),(f /. ( len f))) by A2, A4, A5, Th26;

        then LE (q1,q,P,(f /. 1),(f /. ( len f))) by A14, Th13;

        hence contradiction by A2, A10, A15, Th12, TOPREAL1: 25;

      end;

      assume i = j;

      hence thesis by A1, A2, A3, A4, A5, A6, A9, Lm4;

    end;

    theorem :: JORDAN5C:29

    

     Th29: for f be FinSequence of ( TOP-REAL 2), q1,q2 be Point of ( TOP-REAL 2), i be Nat st q1 in ( LSeg (f,i)) & q2 in ( LSeg (f,i)) & f is being_S-Seq & 1 <= i & (i + 1) <= ( len f) holds LE (q1,q2,( L~ f),(f /. 1),(f /. ( len f))) implies LE (q1,q2,( LSeg (f,i)),(f /. i),(f /. (i + 1)))

    proof

      let f be FinSequence of ( TOP-REAL 2), q1,q2 be Point of ( TOP-REAL 2), i be Nat;

      assume that

       A1: q1 in ( LSeg (f,i)) and

       A2: q2 in ( LSeg (f,i)) and

       A3: f is being_S-Seq and

       A4: 1 <= i & (i + 1) <= ( len f);

      ( len f) >= 2 by A3, TOPREAL1:def 8;

      then

      reconsider P = ( L~ f), Q = ( LSeg (f,i)) as non empty Subset of ( TOP-REAL 2) by A1, TOPREAL1: 23;

      ( L~ f) is_an_arc_of ((f /. 1),(f /. ( len f))) by A3, TOPREAL1: 25;

      then

      consider F be Function of I[01] , (( TOP-REAL 2) | P) such that

       A5: F is being_homeomorphism & (F . 0 ) = (f /. 1) & (F . 1) = (f /. ( len f)) by TOPREAL1:def 1;

      consider ppi,pi1 be Real such that

       A6: ppi < pi1 and

       A7: 0 <= ppi and ppi <= 1 and 0 <= pi1 and

       A8: pi1 <= 1 and

       A9: ( LSeg (f,i)) = (F .: [.ppi, pi1.]) and

       A10: (F . ppi) = (f /. i) and

       A11: (F . pi1) = (f /. (i + 1)) by A3, A4, A5, JORDAN5B: 7;

      set Ex = ( L[01] (( (#) (ppi,pi1)),((ppi,pi1) (#) )));

      

       A12: Ex is being_homeomorphism by A6, TREAL_1: 17;

      then

       A13: ( rng Ex) = ( [#] ( Closed-Interval-TSpace (ppi,pi1))) by TOPS_2:def 5;

      

       A14: ppi in { dd where dd be Real : ppi <= dd & dd <= pi1 } by A6;

      then

      reconsider Poz = [.ppi, pi1.] as non empty Subset of I[01] by A7, A8, BORSUK_1: 40, RCOMP_1:def 1, XXREAL_1: 34;

      consider G be Function of ( I[01] | Poz), (( TOP-REAL 2) | Q) such that

       A15: G = (F | Poz) and

       A16: G is being_homeomorphism by A3, A4, A5, A9, JORDAN5B: 8;

      

       A17: ppi in [.ppi, pi1.] by A14, RCOMP_1:def 1;

      set H = (G * Ex);

      

       A18: ( dom G) = ( [#] ( I[01] | Poz)) by A16, TOPS_2:def 5

      .= Poz by PRE_TOPC:def 5

      .= ( [#] ( Closed-Interval-TSpace (ppi,pi1))) by A6, TOPMETR: 18;

      

      then

       A19: ( rng H) = ( rng G) by A13, RELAT_1: 28

      .= ( [#] (( TOP-REAL 2) | ( LSeg (f,i)))) by A16, TOPS_2:def 5;

      pi1 in { dd where dd be Real : ppi <= dd & dd <= pi1 } by A6;

      then

       A20: pi1 in [.ppi, pi1.] by RCOMP_1:def 1;

      

       A21: (Ex . 1) = (Ex . (( 0 ,1) (#) )) by TREAL_1:def 2

      .= ((ppi,pi1) (#) ) by A6, TREAL_1: 9

      .= pi1 by A6, TREAL_1:def 2;

      

       A22: ( dom H) = ( dom Ex) by A13, A18, RELAT_1: 27

      .= ( [#] I[01] ) by A12, TOPMETR: 20, TOPS_2:def 5

      .= the carrier of I[01] ;

      then

      reconsider H as Function of I[01] , (( TOP-REAL 2) | Q) by A19, FUNCT_2: 2;

      q1 in ( rng H) by A1, A19, PRE_TOPC:def 5;

      then

      consider x19 be object such that

       A23: x19 in ( dom H) and

       A24: q1 = (H . x19) by FUNCT_1:def 3;

      x19 in { l where l be Real : 0 <= l & l <= 1 } by A22, A23, BORSUK_1: 40, RCOMP_1:def 1;

      then

      consider x1 be Real such that

       A25: x1 = x19 and

       A26: 0 <= x1 & x1 <= 1;

      assume

       A27: LE (q1,q2,( L~ f),(f /. 1),(f /. ( len f)));

      x1 in the carrier of I[01] by A26, BORSUK_1: 43;

      then x1 in ( dom Ex) by A13, A18, A22, RELAT_1: 27;

      then (Ex . x1) in the carrier of ( Closed-Interval-TSpace (ppi,pi1)) by A13, FUNCT_1:def 3;

      then

       A28: (Ex . x1) in Poz by A6, TOPMETR: 18;

      1 in ( dom H) by A22, BORSUK_1: 43;

      

      then

       A29: (H . 1) = (G . pi1) by A21, FUNCT_1: 12

      .= (f /. (i + 1)) by A11, A20, A15, FUNCT_1: 49;

      

       A30: (Ex . 0 ) = (Ex . ( (#) ( 0 ,1))) by TREAL_1:def 1

      .= ( (#) (ppi,pi1)) by A6, TREAL_1: 9

      .= ppi by A6, TREAL_1:def 1;

      q2 in ( rng H) by A2, A19, PRE_TOPC:def 5;

      then

      consider x29 be object such that

       A31: x29 in ( dom H) and

       A32: q2 = (H . x29) by FUNCT_1:def 3;

      x29 in { l where l be Real : 0 <= l & l <= 1 } by A22, A31, BORSUK_1: 40, RCOMP_1:def 1;

      then

      consider x2 be Real such that

       A33: x2 = x29 and

       A34: 0 <= x2 and

       A35: x2 <= 1;

      reconsider X1 = x1, X2 = x2 as Point of ( Closed-Interval-TSpace ( 0 ,1)) by A26, A34, A35, BORSUK_1: 43, TOPMETR: 20;

      x2 in the carrier of I[01] by A34, A35, BORSUK_1: 43;

      then x2 in ( dom Ex) by A13, A18, A22, RELAT_1: 27;

      then (Ex . x2) in the carrier of ( Closed-Interval-TSpace (ppi,pi1)) by A13, FUNCT_1:def 3;

      then

       A36: (Ex . x2) in Poz by A6, TOPMETR: 18;

      then

      reconsider E1 = (Ex . X1), E2 = (Ex . X2) as Real by A28;

      

       A37: q2 = (G . (Ex . x2)) by A31, A32, A33, FUNCT_1: 12

      .= (F . (Ex . x2)) by A15, A36, FUNCT_1: 49;

      reconsider K1 = ( Closed-Interval-TSpace (ppi,pi1)), K2 = ( I[01] | Poz) as SubSpace of I[01] by A6, A7, A8, TOPMETR: 20, TREAL_1: 3;

      

       A38: Ex is one-to-one continuous by A12, TOPS_2:def 5;

      the carrier of K1 = [.ppi, pi1.] by A6, TOPMETR: 18

      .= ( [#] ( I[01] | Poz)) by PRE_TOPC:def 5

      .= the carrier of K2;

      then ( I[01] | Poz) = ( Closed-Interval-TSpace (ppi,pi1)) by TSEP_1: 5;

      then

       A39: H is being_homeomorphism by A16, A12, TOPMETR: 20, TOPS_2: 57;

      

       A40: q1 = (G . (Ex . x1)) by A23, A24, A25, FUNCT_1: 12

      .= (F . (Ex . x1)) by A15, A28, FUNCT_1: 49;

      

       A41: 0 <= E2 & E2 <= 1 by A36, BORSUK_1: 43;

       0 in ( dom H) by A22, BORSUK_1: 43;

      

      then

       A42: (H . 0 ) = (G . ppi) by A30, FUNCT_1: 12

      .= (f /. i) by A10, A17, A15, FUNCT_1: 49;

      E1 <= 1 by A28, BORSUK_1: 43;

      then E1 <= E2 by A27, A5, A40, A37, A41;

      then x1 <= x2 by A6, A30, A21, A38, JORDAN5A: 15;

      hence thesis by A3, A4, A39, A42, A29, A24, A32, A25, A26, A33, A35, Th8, JORDAN5B: 15;

    end;

    theorem :: JORDAN5C:30

    for f be FinSequence of ( TOP-REAL 2), q1,q2 be Point of ( TOP-REAL 2) st q1 in ( L~ f) & q2 in ( L~ f) & f is being_S-Seq & q1 <> q2 holds LE (q1,q2,( L~ f),(f /. 1),(f /. ( len f))) iff for i,j be Nat st q1 in ( LSeg (f,i)) & q2 in ( LSeg (f,j)) & 1 <= i & (i + 1) <= ( len f) & 1 <= j & (j + 1) <= ( len f) holds i <= j & (i = j implies LE (q1,q2,(f /. i),(f /. (i + 1))))

    proof

      let f be FinSequence of ( TOP-REAL 2), q1,q2 be Point of ( TOP-REAL 2);

      set p3 = (f /. 1), p4 = (f /. ( len f));

      assume that

       A1: q1 in ( L~ f) and

       A2: q2 in ( L~ f) and

       A3: f is being_S-Seq and

       A4: q1 <> q2;

      reconsider P = ( L~ f) as non empty Subset of ( TOP-REAL 2) by A1;

      hereby

        assume

         A5: LE (q1,q2,( L~ f),(f /. 1),(f /. ( len f)));

        thus for i,j be Nat st q1 in ( LSeg (f,i)) & q2 in ( LSeg (f,j)) & 1 <= i & (i + 1) <= ( len f) & 1 <= j & (j + 1) <= ( len f) holds i <= j & (i = j implies LE (q1,q2,(f /. i),(f /. (i + 1))))

        proof

          let i,j be Nat;

          assume that

           A6: q1 in ( LSeg (f,i)) and

           A7: q2 in ( LSeg (f,j)) and

           A8: 1 <= i and

           A9: (i + 1) <= ( len f) and

           A10: 1 <= j & (j + 1) <= ( len f);

          thus i <= j

          proof

            assume j < i;

            then (j + 1) <= i by NAT_1: 13;

            then

            consider m be Nat such that

             A11: ((j + 1) + m) = i by NAT_1: 10;

            

             A12: LE (q2,(f /. (j + 1)),P,p3,p4) by A3, A7, A10, Th26;

            reconsider m as Nat;

            

             A13: 1 <= (j + 1) & (j + 1) <= ((j + 1) + m) by NAT_1: 11;

            i <= (i + 1) by NAT_1: 11;

            then ((j + 1) + m) <= ( len f) by A9, A11, XXREAL_0: 2;

            then LE ((f /. (j + 1)),(f /. ((j + 1) + m)),P,p3,p4) by A3, A13, Th24;

            then

             A14: LE (q2,(f /. ((j + 1) + m)),P,p3,p4) by A12, Th13;

             LE ((f /. ((j + 1) + m)),q1,P,p3,p4) by A3, A6, A8, A9, A11, Th25;

            then LE (q2,q1,P,p3,p4) by A14, Th13;

            hence thesis by A3, A4, A5, Th12, TOPREAL1: 25;

          end;

          assume

           A15: i = j;

          

           A16: f is one-to-one by A3, TOPREAL1:def 8;

          set p1 = (f /. i), p2 = (f /. (i + 1));

          

           A17: i in ( dom f) & (i + 1) in ( dom f) by A8, A9, SEQ_4: 134;

          

           A18: p1 <> p2

          proof

            assume p1 = p2;

            then i = (i + 1) by A17, A16, PARTFUN2: 10;

            hence thesis;

          end;

          ( LSeg (f,i)) = ( LSeg (p1,p2)) by A8, A9, TOPREAL1:def 3;

          hence thesis by A3, A5, A6, A7, A8, A9, A15, A18, Th17, Th29;

        end;

      end;

      consider i be Nat such that

       A19: 1 <= i & (i + 1) <= ( len f) and

       A20: q1 in ( LSeg (f,i)) by A1, SPPOL_2: 13;

      consider j be Nat such that

       A21: 1 <= j and

       A22: (j + 1) <= ( len f) and

       A23: q2 in ( LSeg (f,j)) by A2, SPPOL_2: 13;

      assume

       A24: for i,j be Nat st q1 in ( LSeg (f,i)) & q2 in ( LSeg (f,j)) & 1 <= i & (i + 1) <= ( len f) & 1 <= j & (j + 1) <= ( len f) holds i <= j & (i = j implies LE (q1,q2,(f /. i),(f /. (i + 1))));

      then

       A25: i <= j by A19, A20, A21, A22, A23;

      per cases by A25, XXREAL_0: 1;

        suppose i < j;

        then (i + 1) <= j by NAT_1: 13;

        then

        consider m be Nat such that

         A26: j = ((i + 1) + m) by NAT_1: 10;

        reconsider m as Nat;

        

         A27: 1 <= (i + 1) & (i + 1) <= ((i + 1) + m) by NAT_1: 11;

        

         A28: LE (q1,(f /. (i + 1)),P,(f /. 1),(f /. ( len f))) by A3, A19, A20, Th26;

        j <= (j + 1) by NAT_1: 11;

        then ((i + 1) + m) <= ( len f) by A22, A26, XXREAL_0: 2;

        then LE ((f /. (i + 1)),(f /. ((i + 1) + m)),P,(f /. 1),(f /. ( len f))) by A3, A27, Th24;

        then

         A29: LE (q1,(f /. ((i + 1) + m)),P,(f /. 1),(f /. ( len f))) by A28, Th13;

         LE ((f /. ((i + 1) + m)),q2,P,(f /. 1),(f /. ( len f))) by A3, A21, A22, A23, A26, Th25;

        hence thesis by A29, Th13;

      end;

        suppose

         A30: i = j;

        reconsider Q = ( LSeg (f,i)) as non empty Subset of ( TOP-REAL 2) by A20;

        set p1 = (f /. i), p2 = (f /. (i + 1));

        

         A31: f is one-to-one by A3, TOPREAL1:def 8;

        

         A32: i in ( dom f) & (i + 1) in ( dom f) by A19, SEQ_4: 134;

        p1 <> p2

        proof

          assume p1 = p2;

          then i = (i + 1) by A32, A31, PARTFUN2: 10;

          hence thesis;

        end;

        then

        consider H be Function of I[01] , (( TOP-REAL 2) | ( LSeg (p1,p2))) such that

         A33: for x be Real st x in [. 0 , 1.] holds (H . x) = (((1 - x) * p1) + (x * p2)) and

         A34: H is being_homeomorphism and (H . 0 ) = p1 and (H . 1) = p2 by JORDAN5A: 3;

        

         A35: ( LSeg (f,i)) = ( LSeg (p1,p2)) by A19, TOPREAL1:def 3;

        then

        reconsider H as Function of I[01] , (( TOP-REAL 2) | Q);

        

         A36: LE (q1,q2,(f /. i),(f /. (i + 1))) by A24, A19, A20, A23, A30;

        q1 in P & q2 in P & for g be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real st g is being_homeomorphism & (g . 0 ) = (f /. 1) & (g . 1) = (f /. ( len f)) & (g . s1) = q1 & 0 <= s1 & s1 <= 1 & (g . s2) = q2 & 0 <= s2 & s2 <= 1 holds s1 <= s2

        proof

          

           A37: ( rng H) = ( [#] (( TOP-REAL 2) | ( LSeg (f,i)))) by A34, A35, TOPS_2:def 5

          .= ( LSeg (f,i)) by PRE_TOPC:def 5;

          then

          consider x19 be object such that

           A38: x19 in ( dom H) and

           A39: (H . x19) = q1 by A20, FUNCT_1:def 3;

          

           A40: ( dom H) = ( [#] I[01] ) by A34, TOPS_2:def 5

          .= [. 0 , 1.] by BORSUK_1: 40;

          then x19 in { l where l be Real : 0 <= l & l <= 1 } by A38, RCOMP_1:def 1;

          then

          consider x1 be Real such that

           A41: x1 = x19 and 0 <= x1 and

           A42: x1 <= 1;

          consider x29 be object such that

           A43: x29 in ( dom H) and

           A44: (H . x29) = q2 by A23, A30, A37, FUNCT_1:def 3;

          x29 in { l where l be Real : 0 <= l & l <= 1 } by A40, A43, RCOMP_1:def 1;

          then

          consider x2 be Real such that

           A45: x2 = x29 and

           A46: 0 <= x2 & x2 <= 1;

          

           A47: q2 = (((1 - x2) * p1) + (x2 * p2)) by A33, A40, A43, A44, A45;

          q1 = (((1 - x1) * p1) + (x1 * p2)) by A33, A40, A38, A39, A41;

          then

           A48: x1 <= x2 by A36, A42, A46, A47;

           0 in { l where l be Real : 0 <= l & l <= 1 };

          then

           A49: 0 in [. 0 , 1.] by RCOMP_1:def 1;

          

          then

           A50: (H . 0 ) = (((1 - 0 ) * p1) + ( 0 * p2)) by A33

          .= (p1 + ( 0 * p2)) by RLVECT_1:def 8

          .= (p1 + ( 0. ( TOP-REAL 2))) by RLVECT_1: 10

          .= p1 by RLVECT_1: 4;

          thus q1 in P & q2 in P by A1, A2;

          let F be Function of I[01] , (( TOP-REAL 2) | P), s1,s2 be Real;

          assume that

           A51: F is being_homeomorphism and

           A52: (F . 0 ) = (f /. 1) & (F . 1) = (f /. ( len f)) and

           A53: (F . s1) = q1 and

           A54: 0 <= s1 & s1 <= 1 and

           A55: (F . s2) = q2 and

           A56: 0 <= s2 & s2 <= 1;

          consider ppi,pi1 be Real such that

           A57: ppi < pi1 and

           A58: 0 <= ppi and ppi <= 1 and 0 <= pi1 and

           A59: pi1 <= 1 and

           A60: ( LSeg (f,i)) = (F .: [.ppi, pi1.]) and

           A61: (F . ppi) = (f /. i) and

           A62: (F . pi1) = (f /. (i + 1)) by A3, A19, A51, A52, JORDAN5B: 7;

          

           A63: ppi in { dd where dd be Real : ppi <= dd & dd <= pi1 } by A57;

          then

          reconsider Poz = [.ppi, pi1.] as non empty Subset of I[01] by A58, A59, BORSUK_1: 40, RCOMP_1:def 1, XXREAL_1: 34;

          consider G be Function of ( I[01] | Poz), (( TOP-REAL 2) | Q) such that

           A64: G = (F | Poz) and

           A65: G is being_homeomorphism by A3, A19, A51, A52, A60, JORDAN5B: 8;

          

           A66: ( dom F) = ( [#] I[01] ) by A51, TOPS_2:def 5

          .= the carrier of I[01] ;

          reconsider K1 = ( Closed-Interval-TSpace (ppi,pi1)), K2 = ( I[01] | Poz) as SubSpace of I[01] by A57, A58, A59, TOPMETR: 20, TREAL_1: 3;

          

           A67: the carrier of K1 = [.ppi, pi1.] by A57, TOPMETR: 18

          .= ( [#] ( I[01] | Poz)) by PRE_TOPC:def 5

          .= the carrier of K2;

          then

          reconsider E = ((G " ) * H) as Function of ( Closed-Interval-TSpace ( 0 ,1)), ( Closed-Interval-TSpace (ppi,pi1)) by TOPMETR: 20;

          

           A68: G is one-to-one by A65, TOPS_2:def 5;

          reconsider X1 = x1, X2 = x2 as Point of ( Closed-Interval-TSpace ( 0 ,1)) by A40, A38, A41, A43, A45, TOPMETR: 18;

          

           A69: (G " ) is being_homeomorphism by A65, TOPS_2: 56;

          

           A70: s2 in the carrier of I[01] by A56, BORSUK_1: 43;

          

           A71: F is one-to-one by A51, TOPS_2:def 5;

          ( rng G) = ( [#] (( TOP-REAL 2) | ( LSeg (f,i)))) by A65, TOPS_2:def 5;

          then G is onto by FUNCT_2:def 3;

          then

           A72: (G " ) = (G qua Function " ) by A68, TOPS_2:def 4;

          

           A73: ex x9 be object st x9 in ( dom F) & x9 in [.ppi, pi1.] & q2 = (F . x9) by A23, A30, A60, FUNCT_1:def 6;

          then s2 in Poz by A55, A70, A66, A71, FUNCT_1:def 4;

          then

           A74: (G . s2) = q2 by A55, A64, FUNCT_1: 49;

          ( dom G) = ( [#] ( I[01] | Poz)) by A65, TOPS_2:def 5;

          then

           A75: ( dom G) = Poz by PRE_TOPC:def 5;

          then s2 in ( dom G) by A55, A70, A66, A71, A73, FUNCT_1:def 4;

          

          then

           A76: s2 = ((G " ) . (H . x2)) by A44, A45, A68, A72, A74, FUNCT_1: 32

          .= (E . x2) by A43, A45, FUNCT_1: 13;

          then

           A77: s2 = (E . X2);

          consider x be object such that

           A78: x in ( dom F) and

           A79: x in [.ppi, pi1.] and

           A80: q1 = (F . x) by A20, A60, FUNCT_1:def 6;

          

           A81: s1 in the carrier of I[01] by A54, BORSUK_1: 43;

          then x = s1 by A53, A66, A71, A78, A80, FUNCT_1:def 4;

          then

           A82: (G . s1) = q1 by A64, A79, A80, FUNCT_1: 49;

          ( Closed-Interval-TSpace (ppi,pi1)) = ( I[01] | Poz) by A67, TSEP_1: 5;

          then E is being_homeomorphism by A34, A35, A69, TOPMETR: 20, TOPS_2: 57;

          then

           A83: E is continuous one-to-one by TOPS_2:def 5;

          1 in { l where l be Real : 0 <= l & l <= 1 };

          then

           A84: 1 in [. 0 , 1.] by RCOMP_1:def 1;

          

          then

           A85: (H . 1) = (((1 - 1) * p1) + (1 * p2)) by A33

          .= (( 0. ( TOP-REAL 2)) + (1 * p2)) by RLVECT_1: 10

          .= (( 0. ( TOP-REAL 2)) + p2) by RLVECT_1:def 8

          .= p2 by RLVECT_1: 4;

          s1 in ( dom G) by A53, A81, A66, A71, A75, A79, A80, FUNCT_1:def 4;

          

          then

           A86: s1 = ((G " ) . (H . x1)) by A39, A41, A68, A72, A82, FUNCT_1: 32

          .= (E . x1) by A38, A41, FUNCT_1: 13;

          then

           A87: s1 = (E . X1);

          pi1 in { dd where dd be Real : ppi <= dd & dd <= pi1 } by A57;

          then

           A88: pi1 in [.ppi, pi1.] by RCOMP_1:def 1;

          then (G . pi1) = p2 by A62, A64, FUNCT_1: 49;

          

          then

           A89: pi1 = ((G " ) . (H . 1)) by A88, A68, A75, A72, A85, FUNCT_1: 32

          .= (E . 1) by A40, A84, FUNCT_1: 13;

          

           A90: ppi in [.ppi, pi1.] by A63, RCOMP_1:def 1;

          then (G . ppi) = p1 by A61, A64, FUNCT_1: 49;

          

          then

           A91: ppi = ((G " ) . (H . 0 )) by A90, A68, A75, A72, A50, FUNCT_1: 32

          .= (E . 0 ) by A40, A49, FUNCT_1: 13;

          per cases by A48, XXREAL_0: 1;

            suppose x1 = x2;

            hence thesis by A86, A76;

          end;

            suppose x1 < x2;

            hence thesis by A57, A83, A91, A89, A87, A77, JORDAN5A: 15;

          end;

        end;

        hence thesis;

      end;

    end;