jordan16.miz



    begin

    reserve C for Simple_closed_curve,

A,A1,A2 for Subset of ( TOP-REAL 2),

p,p1,p2,q,q1,q2 for Point of ( TOP-REAL 2),

n for Element of NAT ;

    theorem :: JORDAN16:1

    ( Lower_Arc C) <> ( Upper_Arc C)

    proof

      assume ( Lower_Arc C) = ( Upper_Arc C);

      then

       A1: ( Lower_Arc C) = ((C \ ( Lower_Arc C)) \/ {( W-min C), ( E-max C)}) by JORDAN6: 51;

      ( Lower_Arc C) is_an_arc_of (( W-min C),( E-max C)) by JORDAN6: 50;

      then

       A2: ex p3 be Point of ( TOP-REAL 2) st p3 in ( Lower_Arc C) & p3 <> ( W-min C) & p3 <> ( E-max C) by JORDAN6: 42;

      ( Lower_Arc C) misses (C \ ( Lower_Arc C)) by XBOOLE_1: 79;

      then ( Lower_Arc C) c= {( W-min C), ( E-max C)} by A1, XBOOLE_1: 73;

      hence contradiction by A2, TARSKI:def 2;

    end;

    theorem :: JORDAN16:2

    

     Th2: ( Segment (A,p1,p2,q1,q2)) c= A

    proof

      ( Segment (A,p1,p2,q1,q2)) = (( R_Segment (A,p1,p2,q1)) /\ ( L_Segment (A,p1,p2,q2))) by JORDAN6:def 5;

      then ( R_Segment (A,p1,p2,q1)) c= A & ( Segment (A,p1,p2,q1,q2)) c= ( R_Segment (A,p1,p2,q1)) by JORDAN6: 20, XBOOLE_1: 17;

      hence thesis;

    end;

    theorem :: JORDAN16:3

    

     Th3: q in A implies q in ( L_Segment (A,p1,p2,q))

    proof

      assume q in A;

      then

       A1: LE (q,q,A,p1,p2) by JORDAN5C: 9;

      ( L_Segment (A,p1,p2,q)) = { q1 : LE (q1,q,A,p1,p2) } by JORDAN6:def 3;

      hence thesis by A1;

    end;

    theorem :: JORDAN16:4

    

     Th4: q in A implies q in ( R_Segment (A,p1,p2,q))

    proof

      assume q in A;

      then

       A1: LE (q,q,A,p1,p2) by JORDAN5C: 9;

      ( R_Segment (A,p1,p2,q)) = { q1 : LE (q,q1,A,p1,p2) } by JORDAN6:def 4;

      hence thesis by A1;

    end;

    theorem :: JORDAN16:5

    

     Th5: LE (q1,q2,A,p1,p2) implies q1 in ( Segment (A,p1,p2,q1,q2)) & q2 in ( Segment (A,p1,p2,q1,q2))

    proof

      

       A1: ( Segment (A,p1,p2,q1,q2)) = (( R_Segment (A,p1,p2,q1)) /\ ( L_Segment (A,p1,p2,q2))) by JORDAN6:def 5;

      assume

       A2: LE (q1,q2,A,p1,p2);

      ( L_Segment (A,p1,p2,q2)) = { q : LE (q,q2,A,p1,p2) } by JORDAN6:def 3;

      then

       A3: q1 in ( L_Segment (A,p1,p2,q2)) by A2;

      q1 in A by A2, JORDAN5C:def 3;

      then q1 in ( R_Segment (A,p1,p2,q1)) by Th4;

      hence q1 in ( Segment (A,p1,p2,q1,q2)) by A1, A3, XBOOLE_0:def 4;

      ( R_Segment (A,p1,p2,q1)) = { q : LE (q1,q,A,p1,p2) } by JORDAN6:def 4;

      then

       A4: q2 in ( R_Segment (A,p1,p2,q1)) by A2;

      q2 in A by A2, JORDAN5C:def 3;

      then q2 in ( L_Segment (A,p1,p2,q2)) by Th3;

      hence thesis by A1, A4, XBOOLE_0:def 4;

    end;

    theorem :: JORDAN16:6

    ( Segment (p,q,C)) c= C

    proof

      set S = ( Segment (p,q,C));

      let e be object such that

       A1: e in S;

      (( Upper_Arc C) \/ ( Lower_Arc C)) = C by JORDAN6: 50;

      then

       A2: ( Upper_Arc C) c= C & ( Lower_Arc C) c= C by XBOOLE_1: 7;

      per cases ;

        suppose q = ( W-min C);

        then S = { p1 : LE (p,p1,C) or p in C & p1 = ( W-min C) } by JORDAN7:def 1;

        then

        consider p1 such that

         A3: e = p1 & ( LE (p,p1,C) or p in C & p1 = ( W-min C)) by A1;

        now

          assume LE (p,p1,C);

          then p1 in ( Upper_Arc C) or p1 in ( Lower_Arc C) by JORDAN6:def 10;

          hence p1 in C by A2;

        end;

        hence thesis by A3, SPRECT_1: 13;

      end;

        suppose q <> ( W-min C);

        then S = { p1 : LE (p,p1,C) & LE (p1,q,C) } by JORDAN7:def 1;

        then

        consider p1 such that

         A4: e = p1 and

         A5: LE (p,p1,C) and LE (p1,q,C) by A1;

        p1 in ( Upper_Arc C) or p1 in ( Lower_Arc C) by A5, JORDAN6:def 10;

        hence thesis by A2, A4;

      end;

    end;

    theorem :: JORDAN16:7

    p in C & q in C implies LE (p,q,C) or LE (q,p,C)

    proof

      assume that

       A1: p in C and

       A2: q in C;

      

       A3: C = (( Lower_Arc C) \/ ( Upper_Arc C)) by JORDAN6: 50;

      per cases by A1, A2, A3, JORDAN7: 1, XBOOLE_0:def 3;

        suppose p = q;

        hence thesis by A1, JORDAN6: 56;

      end;

        suppose that

         A4: p in ( Lower_Arc C) & p <> ( W-min C) & q in ( Lower_Arc C) & q <> ( W-min C) and

         A5: p <> q;

        ( Lower_Arc C) is_an_arc_of (( E-max C),( W-min C)) by JORDAN6: 50;

        then LE (p,q,( Lower_Arc C),( E-max C),( W-min C)) or LE (q,p,( Lower_Arc C),( E-max C),( W-min C)) by A4, A5, JORDAN5C: 14;

        hence thesis by A4, JORDAN6:def 10;

      end;

        suppose p in ( Lower_Arc C) & p <> ( W-min C) & q in ( Upper_Arc C);

        hence thesis by JORDAN6:def 10;

      end;

        suppose p in ( Upper_Arc C) & q in ( Lower_Arc C) & q <> ( W-min C);

        hence thesis by JORDAN6:def 10;

      end;

        suppose that

         A6: p in ( Upper_Arc C) & q in ( Upper_Arc C) and

         A7: p <> q;

        ( Upper_Arc C) is_an_arc_of (( W-min C),( E-max C)) by JORDAN6: 50;

        then LE (p,q,( Upper_Arc C),( W-min C),( E-max C)) or LE (q,p,( Upper_Arc C),( W-min C),( E-max C)) by A6, A7, JORDAN5C: 14;

        hence thesis by A6, JORDAN6:def 10;

      end;

    end;

    theorem :: JORDAN16:8

    

     Th8: for X,Y be non empty TopSpace, Y0 be non empty SubSpace of Y, f be Function of X, Y, g be Function of X, Y0 st f = g & f is continuous holds g is continuous

    proof

      let X,Y be non empty TopSpace, Y0 be non empty SubSpace of Y;

      let f be Function of X, Y, g be Function of X, Y0 such that

       A1: f = g and

       A2: f is continuous;

      let W be Point of X, G be a_neighborhood of (g . W);

      consider V be Subset of Y0 such that

       A3: V is open and

       A4: V c= G and

       A5: (g . W) in V by CONNSP_2: 6;

      (g . W) in ( [#] Y0) & ( [#] Y0) c= ( [#] Y) by PRE_TOPC:def 4;

      then

      reconsider p = (g . W) as Point of Y;

      consider C be Subset of Y such that

       A6: C is open and

       A7: (C /\ ( [#] Y0)) = V by A3, TOPS_2: 24;

      p in C by A5, A7, XBOOLE_0:def 4;

      then C is a_neighborhood of p by A6, CONNSP_2: 3;

      then

      consider H be a_neighborhood of W such that

       A8: (f .: H) c= C by A1, A2;

      take H;

      (g .: H) c= V by A1, A7, A8, XBOOLE_1: 19;

      hence thesis by A4;

    end;

    theorem :: JORDAN16:9

    

     Th9: for S,T be non empty TopSpace, S0 be non empty SubSpace of S, T0 be non empty SubSpace of T, f be Function of S, T st f is being_homeomorphism holds for g be Function of S0, T0 st g = (f | S0) & g is onto holds g is being_homeomorphism

    proof

      let S,T be non empty TopSpace, S0 be non empty SubSpace of S, T0 be non empty SubSpace of T, f be Function of S, T such that

       A1: f is being_homeomorphism;

      

       A2: ( rng f) = ( [#] T) by A1;

      

       A3: (f " ) is continuous by A1;

      let g be Function of S0, T0 such that

       A4: g = (f | S0) and

       A5: g is onto;

      

       A6: g = (f | the carrier of S0) by A4, TMAP_1:def 4;

      

      then

       A7: (f .: the carrier of S0) = ( rng g) by RELAT_1: 115

      .= the carrier of T0 by A5, FUNCT_2:def 3;

      thus ( dom g) = ( [#] S0) by FUNCT_2:def 1;

      thus ( rng g) = ( [#] T0) by A5, FUNCT_2:def 3;

      

       A8: f is one-to-one by A1;

      hence

       A9: g is one-to-one by A6, FUNCT_1: 52;

      

       A10: f is onto by A2, FUNCT_2:def 3;

      f is continuous by A1;

      then g is continuous Function of S0, T by A4;

      hence g is continuous by Th8;

      (g " ) = ((f qua Function | the carrier of S0) " ) by A5, A6, A9, TOPS_2:def 4

      .= ((f qua Function " ) | (f .: the carrier of S0)) by A8, RFUNCT_2: 17

      .= ((f " ) | the carrier of T0) by A10, A8, A7, TOPS_2:def 4

      .= ((f " ) | T0) by TMAP_1:def 4;

      then (g " ) is continuous Function of T0, S by A3;

      hence thesis by Th8;

    end;

    theorem :: JORDAN16:10

    

     Th10: for P1,P2,P3 be Subset of ( TOP-REAL 2) holds for p1,p2 be Point of ( TOP-REAL 2) st P1 is_an_arc_of (p1,p2) & P2 is_an_arc_of (p1,p2) & P3 is_an_arc_of (p1,p2) & (P2 /\ P3) = {p1, p2} & P1 c= (P2 \/ P3) holds P1 = P2 or P1 = P3

    proof

      let P1,P2,P3 be Subset of ( TOP-REAL 2);

      set P = (P2 \/ P3);

      

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

      .= P by PRE_TOPC:def 5;

      then

      reconsider U2 = P2 as Subset of (( TOP-REAL 2) | P) by XBOOLE_1: 7;

      reconsider U3 = P3 as Subset of (( TOP-REAL 2) | P) by A1, XBOOLE_1: 7;

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

      assume that

       A2: P1 is_an_arc_of (p1,p2) and

       A3: P2 is_an_arc_of (p1,p2) and

       A4: P3 is_an_arc_of (p1,p2);

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

       A5: f is being_homeomorphism and

       A6: (f . 0 ) = p1 & (f . 1) = p2 by A2;

      

       A7: f is one-to-one by A5;

      U2 = (P2 /\ P) by XBOOLE_1: 7, XBOOLE_1: 28;

      then

       A8: U2 is closed by A3, JORDAN6: 2, JORDAN6: 11;

      

       A9: ( rng f) = ( [#] (( TOP-REAL 2) | P1)) by A5

      .= P1 by PRE_TOPC:def 5;

      p1 in P2 by A3, TOPREAL1: 1;

      then

      reconsider Q = P as non empty Subset of ( Euclid 2) by TOPREAL3: 8;

      assume that

       A10: (P2 /\ P3) = {p1, p2} and

       A11: P1 c= (P2 \/ P3);

      

       A12: p2 in (P2 /\ P3) & p1 in (P2 /\ P3) by A10, TARSKI:def 2;

      U3 = (P3 /\ P) by XBOOLE_1: 7, XBOOLE_1: 28;

      then

       A13: U3 is closed by A4, JORDAN6: 2, JORDAN6: 11;

      

       A14: f is continuous by A5;

      

       A15: ( dom f) = ( [#] I[01] ) by A5;

      per cases ;

        suppose

         A16: for r be Real st 0 < r & r < 1 holds (f . r) in P3;

        P1 c= P3

        proof

          let y be object;

          assume y in P1;

          then

          consider x be object such that

           A17: x in ( dom f) and

           A18: y = (f . x) by A9, FUNCT_1:def 3;

          reconsider r = x as Real by A17;

          r <= 1 by A17, BORSUK_1: 40, XXREAL_1: 1;

          then r = 0 or r = 1 or 0 < r & r < 1 by A17, BORSUK_1: 40, XXREAL_0: 1, XXREAL_1: 1;

          hence thesis by A12, A6, A16, A18, XBOOLE_0:def 4;

        end;

        hence thesis by A2, A4, JORDAN6: 46;

      end;

        suppose

         A19: ex r be Real st 0 < r & r < 1 & not (f . r) in P3;

        now

          per cases ;

            case

             A20: for r be Real st 0 < r & r < 1 holds (f . r) in P2;

            P1 c= P2

            proof

              let y be object;

              assume y in P1;

              then

              consider x be object such that

               A21: x in ( dom f) and

               A22: y = (f . x) by A9, FUNCT_1:def 3;

              reconsider r = x as Real by A21;

              r <= 1 by A21, BORSUK_1: 40, XXREAL_1: 1;

              then 0 < r & r < 1 or r = 0 or r = 1 by A21, BORSUK_1: 40, XXREAL_0: 1, XXREAL_1: 1;

              hence thesis by A12, A6, A20, A22, XBOOLE_0:def 4;

            end;

            hence thesis by A2, A3, JORDAN6: 46;

          end;

            case ex r be Real st 0 < r & r < 1 & not (f . r) in P2;

            then

            consider r2 be Real such that

             A23: 0 < r2 and

             A24: r2 < 1 and

             A25: not (f . r2) in P2;

            r2 in [. 0 , 1.] by A23, A24, XXREAL_1: 1;

            then (f . r2) in ( rng f) by A15, BORSUK_1: 40, FUNCT_1:def 3;

            then

             A26: (f . r2) in P3 by A11, A9, A25, XBOOLE_0:def 3;

            consider r1 be Real such that

             A27: 0 < r1 and

             A28: r1 < 1 and

             A29: not (f . r1) in P3 by A19;

            r1 in [. 0 , 1.] by A27, A28, XXREAL_1: 1;

            then

             A30: (f . r1) in ( rng f) by A15, BORSUK_1: 40, FUNCT_1:def 3;

            then

             A31: (f . r1) in P2 by A11, A9, A29, XBOOLE_0:def 3;

            now

              per cases ;

                suppose

                 A32: r1 <= r2;

                now

                  per cases by A32, XXREAL_0: 1;

                    suppose r1 = r2;

                    hence contradiction by A11, A9, A25, A29, A30, XBOOLE_0:def 3;

                  end;

                    suppose

                     A33: r1 < r2;

                    

                     A34: the carrier of (( TOP-REAL 2) | P1) = ( [#] (( TOP-REAL 2) | P1))

                    .= P1 by PRE_TOPC:def 5;

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

                    .= P by PRE_TOPC:def 5;

                    then ( rng f) c= the carrier of (( TOP-REAL 2) | P) by A11, A34;

                    then

                    reconsider g = f as Function of I[01] , (( TOP-REAL 2) | P) by A15, FUNCT_2: 2;

                    P = (P1 \/ P) by A11, XBOOLE_1: 12;

                    then

                     A35: (( TOP-REAL 2) | P1) is SubSpace of (( TOP-REAL 2) | P) by TOPMETR: 4;

                    (U2 \/ U3) = the carrier of (( Euclid 2) | Q) & (( TOP-REAL 2) | P) = ( TopSpaceMetr (( Euclid 2) | Q)) by EUCLID: 63, TOPMETR:def 2;

                    then

                    consider r0 be Real such that

                     A36: r1 <= r0 and

                     A37: r0 <= r2 and

                     A38: (g . r0) in (U2 /\ U3) by A14, A8, A13, A24, A27, A26, A31, A33, A35, PRE_TOPC: 26, TOPMETR3: 13;

                    r0 < 1 by A24, A37, XXREAL_0: 2;

                    then

                     A39: r0 in ( dom f) by A15, A27, A36, BORSUK_1: 40, XXREAL_1: 1;

                    

                     A40: 0 in ( dom f) & 1 in ( dom f) by A15, BORSUK_1: 40, XXREAL_1: 1;

                    (g . r0) = p1 or (g . r0) = p2 by A10, A38, TARSKI:def 2;

                    hence contradiction by A6, A7, A24, A27, A36, A37, A39, A40, FUNCT_1:def 4;

                  end;

                end;

                hence contradiction;

              end;

                suppose

                 A41: r1 > r2;

                

                 A42: the carrier of (( TOP-REAL 2) | P1) = ( [#] (( TOP-REAL 2) | P1))

                .= P1 by PRE_TOPC:def 5;

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

                .= P by PRE_TOPC:def 5;

                then ( rng f) c= the carrier of (( TOP-REAL 2) | P) by A11, A42;

                then

                reconsider g = f as Function of I[01] , (( TOP-REAL 2) | P) by A15, FUNCT_2: 2;

                P = (P1 \/ P) by A11, XBOOLE_1: 12;

                then

                 A43: (( TOP-REAL 2) | P1) is SubSpace of (( TOP-REAL 2) | P) by TOPMETR: 4;

                (U2 \/ U3) = the carrier of (( Euclid 2) | Q) & (( TOP-REAL 2) | P) = ( TopSpaceMetr (( Euclid 2) | Q)) by EUCLID: 63, TOPMETR:def 2;

                then

                consider r0 be Real such that

                 A44: r2 <= r0 and

                 A45: r0 <= r1 and

                 A46: (g . r0) in (U2 /\ U3) by A14, A8, A13, A23, A28, A26, A31, A41, A43, PRE_TOPC: 26, TOPMETR3: 13;

                r0 < 1 by A28, A45, XXREAL_0: 2;

                then

                 A47: r0 in ( dom f) by A15, A23, A44, BORSUK_1: 40, XXREAL_1: 1;

                

                 A48: 0 in ( dom f) & 1 in ( dom f) by A15, BORSUK_1: 40, XXREAL_1: 1;

                (g . r0) = p1 or (g . r0) = p2 by A10, A46, TARSKI:def 2;

                hence contradiction by A6, A7, A23, A28, A44, A45, A47, A48, FUNCT_1:def 4;

              end;

            end;

            hence contradiction;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: JORDAN16:11

    

     Th11: for C be Simple_closed_curve, A1,A2 be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2) st A1 is_an_arc_of (p1,p2) & A2 is_an_arc_of (p1,p2) & A1 c= C & A2 c= C & A1 <> A2 holds (A1 \/ A2) = C & (A1 /\ A2) = {p1, p2}

    proof

      let C be Simple_closed_curve, A1,A2 be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2) such that

       A1: A1 is_an_arc_of (p1,p2) and

       A2: A2 is_an_arc_of (p1,p2) and

       A3: A1 c= C and

       A4: A2 c= C & A1 <> A2;

      

       A5: p2 in A1 by A1, TOPREAL1: 1;

      p1 <> p2 & p1 in A1 by A1, JORDAN6: 37, TOPREAL1: 1;

      then

      consider P1,P2 be non empty Subset of ( TOP-REAL 2) such that

       A6: P1 is_an_arc_of (p1,p2) & P2 is_an_arc_of (p1,p2) & C = (P1 \/ P2) & (P1 /\ P2) = {p1, p2} by A3, A5, TOPREAL2: 5;

      reconsider P1, P2 as non empty Subset of ( TOP-REAL 2);

      A1 = P1 or A1 = P2 by A1, A3, A6, Th10;

      hence thesis by A2, A4, A6, Th10;

    end;

    theorem :: JORDAN16:12

    

     Th12: for A1,A2 be Subset of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2) st A1 is_an_arc_of (p1,p2) & (A1 /\ A2) = {q1, q2} holds A1 <> A2

    proof

      let A1,A2 be Subset of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2) such that

       A1: A1 is_an_arc_of (p1,p2) and

       A2: (A1 /\ A2) = {q1, q2} & A1 = A2;

      p1 in A1 by A1, TOPREAL1: 1;

      then

       A3: p1 = q1 or p1 = q2 by A2, TARSKI:def 2;

      p2 in A1 by A1, TOPREAL1: 1;

      then

       A4: p2 = q1 or p2 = q2 by A2, TARSKI:def 2;

      ex p3 be Point of ( TOP-REAL 2) st p3 in A1 & p3 <> p1 & p3 <> p2 by A1, JORDAN6: 42;

      hence contradiction by A1, A2, A3, A4, JORDAN6: 37, TARSKI:def 2;

    end;

    theorem :: JORDAN16:13

    for C be Simple_closed_curve, A1,A2 be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2) st A1 is_an_arc_of (p1,p2) & A2 is_an_arc_of (p1,p2) & A1 c= C & A2 c= C & (A1 /\ A2) = {p1, p2} holds (A1 \/ A2) = C

    proof

      let C be Simple_closed_curve, A1,A2 be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2) such that

       A1: A1 is_an_arc_of (p1,p2) and

       A2: A2 is_an_arc_of (p1,p2) and

       A3: A1 c= C & A2 c= C and

       A4: (A1 /\ A2) = {p1, p2};

      A1 <> A2 by A2, A4, Th12;

      hence thesis by A1, A2, A3, Th11;

    end;

    theorem :: JORDAN16:14

    A1 c= C & A2 c= C & A1 <> A2 & A1 is_an_arc_of (p1,p2) & A2 is_an_arc_of (p1,p2) implies for A st A is_an_arc_of (p1,p2) & A c= C holds A = A1 or A = A2

    proof

      assume that

       A1: A1 c= C & A2 c= C & A1 <> A2 and

       A2: A1 is_an_arc_of (p1,p2) & A2 is_an_arc_of (p1,p2);

      

       A3: (A1 \/ A2) = C & (A1 /\ A2) = {p1, p2} by A1, A2, Th11;

      let A;

      assume A is_an_arc_of (p1,p2) & A c= C;

      hence thesis by A2, A3, Th10;

    end;

    theorem :: JORDAN16:15

    

     Th15: for C be Simple_closed_curve, A be non empty Subset of ( TOP-REAL 2) st A is_an_arc_of (( W-min C),( E-max C)) & A c= C holds A = ( Lower_Arc C) or A = ( Upper_Arc C)

    proof

      let C be Simple_closed_curve, A be non empty Subset of ( TOP-REAL 2) such that

       A1: A is_an_arc_of (( W-min C),( E-max C)) and

       A2: A c= C;

      A is compact by A1, JORDAN5A: 1;

      hence thesis by A1, A2, TOPMETR3: 15;

    end;

    theorem :: JORDAN16:16

    

     Th16: A is_an_arc_of (p1,p2) & LE (q1,q2,A,p1,p2) implies ex g be Function of I[01] , (( TOP-REAL 2) | A), s1,s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s1) = q1 & (g . s2) = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1

    proof

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

       A1: f is being_homeomorphism and

       A2: (f . 0 ) = p1 & (f . 1) = p2;

      

       A3: ( rng f) = ( [#] (( TOP-REAL 2) | A)) by A1

      .= A by PRE_TOPC:def 5;

      assume

       A4: LE (q1,q2,A,p1,p2);

      then q1 in A by JORDAN5C:def 3;

      then

      consider u be object such that

       A5: u in ( dom f) and

       A6: q1 = (f . u) by A3, FUNCT_1:def 3;

      take f;

      

       A7: ( dom f) = ( [#] I[01] ) by A1

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

      then

      reconsider s1 = u as Element of REAL by A5;

      

       A8: s1 <= 1 by A7, A5, XXREAL_1: 1;

      q2 in A by A4, JORDAN5C:def 3;

      then

      consider u be object such that

       A9: u in ( dom f) and

       A10: q2 = (f . u) by A3, FUNCT_1:def 3;

      reconsider s2 = u as Element of REAL by A7, A9;

      take s1, s2;

      thus f is being_homeomorphism & (f . 0 ) = p1 & (f . 1) = p2 by A1, A2;

      thus q1 = (f . s1) & q2 = (f . s2) by A6, A10;

      thus 0 <= s1 by A7, A5, XXREAL_1: 1;

       0 <= s2 & s2 <= 1 by A7, A9, XXREAL_1: 1;

      hence s1 <= s2 by A1, A2, A4, A6, A10, A8, JORDAN5C:def 3;

      thus thesis by A7, A9, XXREAL_1: 1;

    end;

    theorem :: JORDAN16:17

    

     Th17: A is_an_arc_of (p1,p2) & LE (q1,q2,A,p1,p2) & q1 <> q2 implies ex g be Function of I[01] , (( TOP-REAL 2) | A), s1,s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s1) = q1 & (g . s2) = q2 & 0 <= s1 & s1 < s2 & s2 <= 1

    proof

      assume that

       A1: A is_an_arc_of (p1,p2) & LE (q1,q2,A,p1,p2) and

       A2: q1 <> q2;

      consider g be Function of I[01] , (( TOP-REAL 2) | A), s1,s2 be Real such that

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

       A4: (g . s1) = q1 & (g . s2) = q2 and

       A5: 0 <= s1 and

       A6: s1 <= s2 and

       A7: s2 <= 1 by A1, Th16;

      take g, s1, s2;

      thus g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s1) = q1 & (g . s2) = q2 & 0 <= s1 by A3, A4, A5;

      thus s1 < s2 by A2, A4, A6, XXREAL_0: 1;

      thus thesis by A7;

    end;

    theorem :: JORDAN16:18

     LE (q1,q2,A,p1,p2) implies ( Segment (A,p1,p2,q1,q2)) is non empty

    proof

      

       A1: ( Segment (A,p1,p2,q1,q2)) = { q : LE (q1,q,A,p1,p2) & LE (q,q2,A,p1,p2) } by JORDAN6: 26;

      assume

       A2: LE (q1,q2,A,p1,p2);

      then q2 in A by JORDAN5C:def 3;

      then LE (q2,q2,A,p1,p2) by JORDAN5C: 9;

      then q2 in ( Segment (A,p1,p2,q1,q2)) by A2, A1;

      hence thesis;

    end;

    theorem :: JORDAN16:19

    p in C implies p in ( Segment (p,( W-min C),C)) & ( W-min C) in ( Segment (p,( W-min C),C))

    proof

      

       A1: ( Segment (p,( W-min C),C)) = { p1 : LE (p,p1,C) or p in C & p1 = ( W-min C) } by JORDAN7:def 1;

      assume

       A2: p in C;

      then LE (p,p,C) by JORDAN6: 56;

      hence p in ( Segment (p,( W-min C),C)) by A1;

      thus thesis by A2, A1;

    end;

    theorem :: JORDAN16:20

    

     Th20: for f be Function of R^1 , R^1 holds for a,b be Real st a <> 0 & f = ( AffineMap (a,b)) holds f is being_homeomorphism

    proof

      let f be Function of R^1 , R^1 ;

      let a,b be Real such that

       A1: a <> 0 and

       A2: f = ( AffineMap (a,b));

      thus ( dom f) = ( [#] R^1 ) by FUNCT_2:def 1;

      thus

       A3: ( rng f) = ( [#] R^1 ) by A1, A2, FCONT_1: 55, TOPMETR: 17;

      thus

       A4: f is one-to-one by A1, A2, FCONT_1: 50;

      for x be Real holds (f . x) = ((a * x) + b) by A2, FCONT_1:def 4;

      hence f is continuous by TOPMETR: 21;

      f is onto by A3, FUNCT_2:def 3;

      

      then (f " ) = (f qua Function " ) by A4, TOPS_2:def 4

      .= ( AffineMap ((a " ),( - (b / a)))) by A1, A2, FCONT_1: 56;

      then for x be Real holds ((f " ) . x) = (((a " ) * x) + ( - (b / a))) by FCONT_1:def 4;

      hence thesis by TOPMETR: 21;

    end;

    theorem :: JORDAN16:21

    

     Th21: A is_an_arc_of (p1,p2) & LE (q1,q2,A,p1,p2) & q1 <> q2 implies ( Segment (A,p1,p2,q1,q2)) is_an_arc_of (q1,q2)

    proof

      assume that

       A1: A is_an_arc_of (p1,p2) and

       A2: LE (q1,q2,A,p1,p2) & q1 <> q2;

      consider g be Function of I[01] , (( TOP-REAL 2) | A), s1,s2 be Real such that

       A3: g is being_homeomorphism and

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

       A5: (g . s1) = q1 and

       A6: (g . s2) = q2 and

       A7: 0 <= s1 and

       A8: s1 < s2 and

       A9: s2 <= 1 by A1, A2, Th17;

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

      set S = ( Segment (A,p1,p2,q1,q2));

      

       A10: S = { q : LE (q1,q,A,p1,p2) & LE (q,q2,A,p1,p2) } by JORDAN6: 26;

      

       A11: 0 < (s2 - s1) by A8, XREAL_1: 50;

      set f = ((g * ( AffineMap ((s2 - s1),s1))) | [. 0 , 1.]);

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

      reconsider m = ( AffineMap ((s2 - s1),s1)) as Function of R^1 , R^1 by TOPMETR: 17;

      for x be Real holds (m . x) = (((s2 - s1) * x) + s1) by FCONT_1:def 4;

      then

      reconsider m as continuous Function of R^1 , R^1 by TOPMETR: 21;

      set h = (m | I[01] );

      

       A12: h = (m | [. 0 , 1.]) by BORSUK_1: 40, TMAP_1:def 4;

      

      then

       A13: ( rng h) = (m .: [. 0 , 1.]) by RELAT_1: 115

      .= [.s1, ((s2 - s1) + s1).] by A8, FCONT_1: 57, XREAL_1: 50

      .= [.s1, s2.];

      then

       A14: ( rng h) c= [. 0 , 1.] by A7, A9, XXREAL_1: 34;

      

       A15: ( dom m) = REAL by FUNCT_2:def 1;

      then

       A16: ( dom h) = [. 0 , 1.] by A12, RELAT_1: 62;

      then

      reconsider h as Function of I[01] , I[01] by A14, BORSUK_1: 40, RELSET_1: 4;

      

       A17: f = (g * h) by A12, RELAT_1: 83;

      

       A18: [. 0 , 1.] = ( dom g) by BORSUK_1: 40, FUNCT_2:def 1;

      (m .: [. 0 , 1.]) c= ( dom g)

      proof

        let e be object;

        assume e in (m .: [. 0 , 1.]);

        then

         A19: e in [.s1, ((s2 - s1) + s1).] by A8, FCONT_1: 57, XREAL_1: 50;

         [.s1, s2.] c= [. 0 , 1.] by A7, A9, XXREAL_1: 34;

        hence thesis by A18, A19;

      end;

      then

       A20: [. 0 , 1.] c= ( dom (g * m)) by A15, FUNCT_3: 3;

      then

       A21: ( dom f) = ( [#] I[01] ) by BORSUK_1: 40, RELAT_1: 62;

      reconsider CIT = ( Closed-Interval-TSpace (s1,s2)) as non empty SubSpace of I[01] by A7, A8, A9, TOPMETR: 20, TREAL_1: 3;

       [.s1, s2.] c= [. 0 , 1.] by A7, A9, XXREAL_1: 34;

      then

       A22: the carrier of CIT c= ( dom g) by A8, A18, TOPMETR: 18;

      

       A23: ( rng h) = the carrier of CIT by A8, A13, TOPMETR: 18;

      

       A24: ( dom f) = the carrier of I[01] by A20, BORSUK_1: 40, RELAT_1: 62;

      

       A25: s1 < 1 by A8, A9, XXREAL_0: 2;

      for y be object holds y in ( [#] (( TOP-REAL 2) | S)) iff ex x be object st x in ( dom f) & y = (f . x)

      proof

        let y be object;

        thus y in ( [#] (( TOP-REAL 2) | S)) implies ex x be object st x in ( dom f) & y = (f . x)

        proof

          assume y in ( [#] (( TOP-REAL 2) | S));

          then y in S by PRE_TOPC:def 5;

          then

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

           A26: y = q0 and

           A27: LE (q1,q0,A,p1,p2) and

           A28: LE (q0,q2,A,p1,p2) by A10;

          q0 in A by A27, JORDAN5C:def 3;

          then q0 in ( [#] (( TOP-REAL 2) | A)) by PRE_TOPC:def 5;

          then q0 in ( rng g) by A3;

          then

          consider s be object such that

           A29: s in ( dom g) and

           A30: q0 = (g . s) by FUNCT_1:def 3;

          reconsider s as Real by A29;

          take x = ((s - s1) / (s2 - s1));

          

           A31: s <= 1 by A29, BORSUK_1: 40, XXREAL_1: 1;

          then s <= s2 by A3, A4, A6, A7, A8, A9, A28, A30, JORDAN5C:def 3;

          then (s - s1) <= (s2 - s1) by XREAL_1: 9;

          then x <= ((s2 - s1) / (s2 - s1)) by A11, XREAL_1: 72;

          then

           A32: x <= 1 by A11, XCMPLX_1: 60;

           0 <= s by A29, BORSUK_1: 40, XXREAL_1: 1;

          then (s1 + 0 ) <= s by A3, A4, A5, A25, A27, A30, A31, JORDAN5C:def 3;

          then 0 <= (s - s1) by XREAL_1: 19;

          hence

           A33: x in ( dom f) by A11, A21, A32, BORSUK_1: 40, XXREAL_1: 1;

          

           A34: x in REAL by XREAL_0:def 1;

          (m . x) = (((s2 - s1) * x) + s1) by FCONT_1:def 4

          .= ((s - s1) + s1) by A11, XCMPLX_1: 87

          .= s;

          

          hence y = ((g * m) . x) by A15, A26, A30, FUNCT_1: 13, A34

          .= (f . x) by A33, FUNCT_1: 47;

        end;

        given x be object such that

         A35: x in ( dom f) and

         A36: y = (f . x);

        reconsider x as Element of REAL by A35;

        (( AffineMap ((s2 - s1),s1)) . x) in REAL ;

        then

        reconsider s = (m . x) as Element of REAL ;

        (h . x) = (m . x) by A12, A16, A21, A35, BORSUK_1: 40, FUNCT_1: 47;

        then

         A37: s in ( rng h) by A16, A21, A35, BORSUK_1: 40, FUNCT_1:def 3;

        then

         A38: s1 <= s by A13, XXREAL_1: 1;

        y in ( rng f) by A35, A36, FUNCT_1:def 3;

        then y in ( [#] (( TOP-REAL 2) | A));

        then y in A by PRE_TOPC:def 5;

        then

        reconsider q = y as Point of ( TOP-REAL 2);

        

         A39: s <= s2 by A13, A37, XXREAL_1: 1;

        then

         A40: s <= 1 by A9, XXREAL_0: 2;

        

         A41: q = ((g * m) . x) by A35, A36, FUNCT_1: 47

        .= (g . s) by A15, FUNCT_1: 13;

        then

         A42: LE (q1,q,A,p1,p2) by A1, A3, A4, A5, A7, A25, A38, A40, JORDAN5C: 8;

         LE (q,q2,A,p1,p2) by A1, A3, A4, A6, A7, A9, A41, A38, A39, A40, JORDAN5C: 8;

        then q in S by A10, A42;

        hence thesis by PRE_TOPC:def 5;

      end;

      then

       A43: ( rng f) = ( [#] (( TOP-REAL 2) | S)) by FUNCT_1:def 3;

      then

       A44: ( [#] (( TOP-REAL 2) | S)) <> {} by A21, RELAT_1: 42;

      then

      reconsider f as Function of I[01] , (( TOP-REAL 2) | S) by A24, A43, FUNCT_2:def 1, RELSET_1: 4;

      reconsider TS = (( TOP-REAL 2) | S) as non empty SubSpace of (( TOP-REAL 2) | A9) by A44, Th2, TOPMETR: 22;

      take f;

      

       A45: (( AffineMap ((s2 - s1),s1)) . 0 ) = s1 by FCONT_1: 48;

      set o = (g | CIT);

      

       A46: ( dom o) = ( dom (g | the carrier of CIT)) by TMAP_1:def 4

      .= (( dom g) /\ the carrier of CIT) by RELAT_1: 61

      .= the carrier of CIT by A22, XBOOLE_1: 28;

      reconsider h as Function of I[01] , CIT by A16, A23, RELSET_1: 4;

      h is onto by A23, FUNCT_2:def 3;

      then

       A47: h is being_homeomorphism by A11, Th9, Th20;

      

       A48: the carrier of CIT = [.s1, s2.] by A8, TOPMETR: 18;

      then o = (g | ( rng h)) by A13, TMAP_1:def 4;

      then

       A49: f = (o * h) by A17, FUNCT_4: 2;

      then

       A50: ( rng o) = ( rng f) by A13, A46, A48, RELAT_1: 28;

      then

      reconsider o as Function of CIT, TS by A46, RELSET_1: 4;

      o is onto by A43, A50, FUNCT_2:def 3;

      then o is being_homeomorphism by A3, Th9;

      hence f is being_homeomorphism by A49, A47, TOPS_2: 57;

      

       A51: ( dom ( AffineMap ((s2 - s1),s1))) = REAL by FUNCT_2:def 1;

      

       A52: 0 in REAL by XREAL_0:def 1;

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

      

      hence (f . 0 ) = ((g * m) . 0 ) by FUNCT_1: 49

      .= q1 by A5, A45, A51, FUNCT_1: 13, A52;

      

       A53: (( AffineMap ((s2 - s1),s1)) . 1) = ((s2 - s1) + s1) by FCONT_1: 49

      .= s2;

      

       A54: 1 in REAL by XREAL_0:def 1;

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

      

      hence (f . 1) = ((g * m) . 1) by FUNCT_1: 49

      .= q2 by A6, A53, A51, FUNCT_1: 13, A54;

    end;

    theorem :: JORDAN16:22

    for p1,p2 be Point of ( TOP-REAL 2) holds for P be Subset of ( TOP-REAL 2) st P c= C & P is_an_arc_of (p1,p2) & ( W-min C) in P & ( E-max C) in P holds ( Upper_Arc C) c= P or ( Lower_Arc C) c= P

    proof

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

      let P be Subset of ( TOP-REAL 2) such that

       A1: P c= C and

       A2: P is_an_arc_of (p1,p2) and

       A3: ( W-min C) in P and

       A4: ( E-max C) in P;

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

      

       A5: ( W-min C) <> ( E-max C) by TOPREAL5: 19;

      per cases by A2, A3, A4, A5, JORDAN5C: 14;

        suppose

         A6: LE (( W-min C),( E-max C),P,p1,p2);

        set S = ( Segment (P9,p1,p2,( W-min C),( E-max C)));

        reconsider S9 = S as non empty Subset of ( TOP-REAL 2) by A6, Th5;

        S c= P by Th2;

        then S c= C by A1;

        then S9 = ( Lower_Arc C) or S9 = ( Upper_Arc C) by A2, A5, A6, Th15, Th21;

        hence thesis by Th2;

      end;

        suppose

         A7: LE (( E-max C),( W-min C),P,p1,p2);

        set S = ( Segment (P9,p1,p2,( E-max C),( W-min C)));

        reconsider S9 = S as non empty Subset of ( TOP-REAL 2) by A7, Th5;

        S is_an_arc_of (( E-max C),( W-min C)) by A2, A5, A7, Th21;

        then

         A8: S9 is_an_arc_of (( W-min C),( E-max C)) by JORDAN5B: 14;

        S c= P by Th2;

        hence thesis by A1, A8, Th15, XBOOLE_1: 1;

      end;

    end;

    theorem :: JORDAN16:23

    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 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & q1 <> q2 holds ex Q be non empty Subset of ( TOP-REAL 2) st Q is_an_arc_of (q1,q2) & Q c= P & Q misses {p1, p2}

    proof

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

       A1: P is_an_arc_of (p1,p2) and

       A2: q1 in P & q2 in P and

       A3: q1 <> p1 and

       A4: q1 <> p2 and

       A5: q2 <> p1 and

       A6: q2 <> p2 and

       A7: q1 <> q2;

      per cases by A1, A2, A7, JORDAN5C: 14;

        suppose

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

        set S = ( Segment (P,p1,p2,q1,q2));

        S is_an_arc_of (q1,q2) by A1, A7, A8, Th21;

        then

        reconsider S as non empty Subset of ( TOP-REAL 2) by TOPREAL1: 1;

        take S;

        thus S is_an_arc_of (q1,q2) by A1, A7, A8, Th21;

        thus S c= P by Th2;

        now

          

           A9: S = { q where q be Point of ( TOP-REAL 2) : LE (q1,q,P,p1,p2) & LE (q,q2,P,p1,p2) } by JORDAN6: 26;

          assume

           A10: S meets {p1, p2};

          per cases by A10, ZFMISC_1: 51;

            suppose p1 in S;

            then ex q be Point of ( TOP-REAL 2) st q = p1 & LE (q1,q,P,p1,p2) & LE (q,q2,P,p1,p2) by A9;

            hence contradiction by A1, A3, JORDAN6: 54;

          end;

            suppose p2 in S;

            then ex q be Point of ( TOP-REAL 2) st q = p2 & LE (q1,q,P,p1,p2) & LE (q,q2,P,p1,p2) by A9;

            hence contradiction by A1, A6, JORDAN6: 55;

          end;

        end;

        hence thesis;

      end;

        suppose

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

        set S = ( Segment (P,p1,p2,q2,q1));

        S is_an_arc_of (q2,q1) by A1, A7, A11, Th21;

        then

        reconsider S as non empty Subset of ( TOP-REAL 2) by TOPREAL1: 1;

        take S;

        S is_an_arc_of (q2,q1) by A1, A7, A11, Th21;

        hence S is_an_arc_of (q1,q2) by JORDAN5B: 14;

        thus S c= P by Th2;

        now

          

           A12: S = { q where q be Point of ( TOP-REAL 2) : LE (q2,q,P,p1,p2) & LE (q,q1,P,p1,p2) } by JORDAN6: 26;

          assume

           A13: S meets {p1, p2};

          per cases by A13, ZFMISC_1: 51;

            suppose p1 in S;

            then ex q be Point of ( TOP-REAL 2) st q = p1 & LE (q2,q,P,p1,p2) & LE (q,q1,P,p1,p2) by A12;

            hence contradiction by A1, A5, JORDAN6: 54;

          end;

            suppose p2 in S;

            then ex q be Point of ( TOP-REAL 2) st q = p2 & LE (q2,q,P,p1,p2) & LE (q,q1,P,p1,p2) by A12;

            hence contradiction by A1, A4, JORDAN6: 55;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: JORDAN16:24

    for P be non empty 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 & p1 <> q1 holds ( Segment (P,p1,p2,p1,q1)) is_an_arc_of (p1,q1)

    proof

      let P be non empty 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 and

       A3: p1 <> q1;

       LE (p1,q1,P,p1,p2) by A1, A2, JORDAN5C: 10;

      hence thesis by A1, A3, Th21;

    end;