jordan6.miz



    begin

    reserve x,y for set;

    reserve s,r for Real;

    reserve r1,r2 for Real;

    reserve n for Nat;

    reserve p,q,q1,q2 for Point of ( TOP-REAL 2);

    theorem :: JORDAN6:1

    

     Th1: r <= s implies r <= ((r + s) / 2) & ((r + s) / 2) <= s

    proof

      assume

       A1: r <= s;

      per cases by A1, XXREAL_0: 1;

        suppose r < s;

        hence thesis by XREAL_1: 226;

      end;

        suppose r = s;

        hence thesis;

      end;

    end;

    theorem :: JORDAN6:2

    

     Th2: for TX be non empty TopSpace, P be Subset of TX, A be Subset of (TX | P), B be Subset of TX st B is closed & A = (B /\ P) holds A is closed

    proof

      let TX be non empty TopSpace, P be Subset of TX, A be Subset of (TX | P), B be Subset of TX;

      assume that

       A1: B is closed and

       A2: A = (B /\ P);

      ( [#] (TX | P)) = P by PRE_TOPC:def 5;

      hence thesis by A1, A2, PRE_TOPC: 13;

    end;

    theorem :: JORDAN6:3

    

     Th3: for TX,TY be non empty TopSpace, P be non empty Subset of TY, f be Function of TX, (TY | P) holds f is Function of TX, TY & for f2 be Function of TX, TY st f2 = f & f is continuous holds f2 is continuous

    proof

      let TX,TY be non empty TopSpace, P be non empty Subset of TY, f be Function of TX, (TY | P);

      

       A1: the carrier of (TY | P) = ( [#] (TY | P))

      .= P by PRE_TOPC:def 5;

      hence f is Function of TX, TY by FUNCT_2: 7;

      let f2 be Function of TX, TY such that

       A2: f2 = f and

       A3: f is continuous;

      let P1 be Subset of TY;

      assume

       A4: P1 is closed;

      reconsider P3 = (P1 /\ P) as Subset of (TY | P) by TOPS_2: 29;

      

       A5: P3 is closed by A4, Th2;

      (f2 " P) = the carrier of TX by A1, A2, FUNCT_2: 40

      .= ( dom f2) by FUNCT_2:def 1;

      

      then (f2 " P1) = ((f2 " P1) /\ (f2 " P)) by RELAT_1: 132, XBOOLE_1: 28

      .= (f " P3) by A2, FUNCT_1: 68;

      hence thesis by A3, A5;

    end;

    theorem :: JORDAN6:4

    

     Th4: for r be Real, P be Subset of ( TOP-REAL 2) st P = { p where p be Point of ( TOP-REAL 2) : (p `1 ) >= r } holds P is closed

    proof

      let r be Real, P be Subset of ( TOP-REAL 2);

      assume

       A1: P = { p where p be Point of ( TOP-REAL 2) : (p `1 ) >= r };

      

       A2: 1 in ( Seg 2) by FINSEQ_1: 1;

      

       A3: (P ` ) c= { p where p be Point of ( TOP-REAL 2) : (p `1 ) < r }

      proof

        let x be object;

        assume

         A4: x in (P ` );

        then x in (the carrier of ( TOP-REAL 2) \ P) by SUBSET_1:def 4;

        then

         A5: not x in P by XBOOLE_0:def 5;

        reconsider q = x as Point of ( TOP-REAL 2) by A4;

        (q `1 ) < r by A1, A5;

        hence thesis;

      end;

      { p where p be Point of ( TOP-REAL 2) : (p `1 ) < r } c= (P ` )

      proof

        let x be object;

        assume x in { p where p be Point of ( TOP-REAL 2) : (p `1 ) < r };

        then

         A6: ex p be Point of ( TOP-REAL 2) st (p = x) & ((p `1 ) < r);

        now

          assume x in { q where q be Point of ( TOP-REAL 2) : (q `1 ) >= r };

          then ex q be Point of ( TOP-REAL 2) st (q = x) & ((q `1 ) >= r);

          hence contradiction by A6;

        end;

        then x in (the carrier of ( TOP-REAL 2) \ P) by A1, A6, XBOOLE_0:def 5;

        hence thesis by SUBSET_1:def 4;

      end;

      then

       A7: (P ` ) = { p where p be Point of ( TOP-REAL 2) : (p `1 ) < r } by A3;

      

       A8: (P ` ) c= { p where p be Point of ( TOP-REAL 2) : r > (p /. 1) }

      proof

        let x be object;

        assume x in (P ` );

        then

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

         A9: p = x and

         A10: (p `1 ) < r by A7;

        (p /. 1) < r by A10, JORDAN2B: 29;

        hence thesis by A9;

      end;

      { p where p be Point of ( TOP-REAL 2) : r > (p /. 1) } c= (P ` )

      proof

        let x be object;

        assume x in { p where p be Point of ( TOP-REAL 2) : r > (p /. 1) };

        then

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

         A11: q = x and

         A12: r > (q /. 1);

        (q `1 ) < r by A12, JORDAN2B: 29;

        hence thesis by A7, A11;

      end;

      then

       A13: (P ` ) = { p where p be Point of ( TOP-REAL 2) : r > (p /. 1) } by A8;

      reconsider P1 = (P ` ) as Subset of ( TOP-REAL 2);

      P1 is open by A2, A13, JORDAN2B: 12;

      hence thesis by TOPS_1: 3;

    end;

    theorem :: JORDAN6:5

    

     Th5: for r be Real, P be Subset of ( TOP-REAL 2) st P = { p where p be Point of ( TOP-REAL 2) : (p `1 ) <= r } holds P is closed

    proof

      let r be Real, P be Subset of ( TOP-REAL 2);

      assume

       A1: P = { p where p be Point of ( TOP-REAL 2) : (p `1 ) <= r };

      

       A2: 1 in ( Seg 2) by FINSEQ_1: 1;

      

       A3: (P ` ) c= { p where p be Point of ( TOP-REAL 2) : (p `1 ) > r }

      proof

        let x be object;

        assume

         A4: x in (P ` );

        then x in (the carrier of ( TOP-REAL 2) \ P) by SUBSET_1:def 4;

        then

         A5: not x in P by XBOOLE_0:def 5;

        reconsider q = x as Point of ( TOP-REAL 2) by A4;

        (q `1 ) > r by A1, A5;

        hence thesis;

      end;

      { p where p be Point of ( TOP-REAL 2) : (p `1 ) > r } c= (P ` )

      proof

        let x be object;

        assume x in { p where p be Point of ( TOP-REAL 2) : (p `1 ) > r };

        then

         A6: ex p be Point of ( TOP-REAL 2) st (p = x) & ((p `1 ) > r);

        now

          assume x in { q where q be Point of ( TOP-REAL 2) : (q `1 ) <= r };

          then ex q be Point of ( TOP-REAL 2) st (q = x) & ((q `1 ) <= r);

          hence contradiction by A6;

        end;

        then x in (the carrier of ( TOP-REAL 2) \ P) by A1, A6, XBOOLE_0:def 5;

        hence thesis by SUBSET_1:def 4;

      end;

      then

       A7: (P ` ) = { p where p be Point of ( TOP-REAL 2) : (p `1 ) > r } by A3;

      

       A8: (P ` ) c= { p where p be Point of ( TOP-REAL 2) : r < (p /. 1) }

      proof

        let x be object;

        assume x in (P ` );

        then

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

         A9: p = x and

         A10: (p `1 ) > r by A7;

        (p /. 1) > r by A10, JORDAN2B: 29;

        hence thesis by A9;

      end;

      { p where p be Point of ( TOP-REAL 2) : r < (p /. 1) } c= (P ` )

      proof

        let x be object;

        assume x in { p where p be Point of ( TOP-REAL 2) : r < (p /. 1) };

        then

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

         A11: q = x and

         A12: r < (q /. 1);

        (q `1 ) > r by A12, JORDAN2B: 29;

        hence thesis by A7, A11;

      end;

      then

       A13: (P ` ) = { p where p be Point of ( TOP-REAL 2) : r < (p /. 1) } by A8;

      reconsider P1 = (P ` ) as Subset of ( TOP-REAL 2);

      P1 is open by A2, A13, JORDAN2B: 13;

      hence thesis by TOPS_1: 3;

    end;

    theorem :: JORDAN6:6

    

     Th6: for r be Real, P be Subset of ( TOP-REAL 2) st P = { p where p be Point of ( TOP-REAL 2) : (p `1 ) = r } holds P is closed

    proof

      let r be Real, P be Subset of ( TOP-REAL 2);

      assume

       A1: P = { p where p be Point of ( TOP-REAL 2) : (p `1 ) = r };

      defpred P[ Point of ( TOP-REAL 2)] means ($1 `1 ) >= r;

      { p where p be Element of ( TOP-REAL 2) : P[p] } is Subset of ( TOP-REAL 2) from DOMAIN_1:sch 7;

      then

      reconsider P1 = { p where p be Point of ( TOP-REAL 2) : (p `1 ) >= r } as Subset of ( TOP-REAL 2);

      

       A2: P1 is closed by Th4;

      defpred Q[ Point of ( TOP-REAL 2)] means ($1 `1 ) <= r;

      { p where p be Element of ( TOP-REAL 2) : Q[p] } is Subset of ( TOP-REAL 2) from DOMAIN_1:sch 7;

      then

      reconsider P2 = { p where p be Point of ( TOP-REAL 2) : (p `1 ) <= r } as Subset of ( TOP-REAL 2);

      

       A3: P2 is closed by Th5;

      

       A4: P c= (P1 /\ P2)

      proof

        let x be object;

        assume x in P;

        then

         A5: ex p be Point of ( TOP-REAL 2) st p = x & (p `1 ) = r by A1;

        then

         A6: x in P1;

        x in P2 by A5;

        hence thesis by A6, XBOOLE_0:def 4;

      end;

      (P1 /\ P2) c= P

      proof

        let x be object;

        assume

         A7: x in (P1 /\ P2);

        then

         A8: x in P1 by XBOOLE_0:def 4;

        

         A9: x in P2 by A7, XBOOLE_0:def 4;

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

         A10: q1 = x and

         A11: (q1 `1 ) >= r by A8;

        ex q2 be Point of ( TOP-REAL 2) st (q2 = x) & ((q2 `1 ) <= r) by A9;

        then (q1 `1 ) = r by A10, A11, XXREAL_0: 1;

        hence thesis by A1, A10;

      end;

      then P = (P1 /\ P2) by A4;

      hence thesis by A2, A3, TOPS_1: 8;

    end;

    theorem :: JORDAN6:7

    

     Th7: for r be Real, P be Subset of ( TOP-REAL 2) st P = { p where p be Point of ( TOP-REAL 2) : (p `2 ) >= r } holds P is closed

    proof

      let r be Real, P be Subset of ( TOP-REAL 2);

      assume

       A1: P = { p where p be Point of ( TOP-REAL 2) : (p `2 ) >= r };

      

       A2: 2 in ( Seg 2) by FINSEQ_1: 1;

      

       A3: (P ` ) c= { p where p be Point of ( TOP-REAL 2) : (p `2 ) < r }

      proof

        let x be object;

        assume

         A4: x in (P ` );

        then x in (the carrier of ( TOP-REAL 2) \ P) by SUBSET_1:def 4;

        then

         A5: not x in P by XBOOLE_0:def 5;

        reconsider q = x as Point of ( TOP-REAL 2) by A4;

        (q `2 ) < r by A1, A5;

        hence thesis;

      end;

      { p where p be Point of ( TOP-REAL 2) : (p `2 ) < r } c= (P ` )

      proof

        let x be object;

        assume x in { p where p be Point of ( TOP-REAL 2) : (p `2 ) < r };

        then

         A6: ex p be Point of ( TOP-REAL 2) st (p = x) & ((p `2 ) < r);

        now

          assume x in { q where q be Point of ( TOP-REAL 2) : (q `2 ) >= r };

          then ex q be Point of ( TOP-REAL 2) st (q = x) & ((q `2 ) >= r);

          hence contradiction by A6;

        end;

        then x in (the carrier of ( TOP-REAL 2) \ P) by A1, A6, XBOOLE_0:def 5;

        hence thesis by SUBSET_1:def 4;

      end;

      then

       A7: (P ` ) = { p where p be Point of ( TOP-REAL 2) : (p `2 ) < r } by A3;

      

       A8: (P ` ) c= { p where p be Point of ( TOP-REAL 2) : r > (p /. 2) }

      proof

        let x be object;

        assume x in (P ` );

        then

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

         A9: p = x and

         A10: (p `2 ) < r by A7;

        (p /. 2) < r by A10, JORDAN2B: 29;

        hence thesis by A9;

      end;

      { p where p be Point of ( TOP-REAL 2) : r > (p /. 2) } c= (P ` )

      proof

        let x be object;

        assume x in { p where p be Point of ( TOP-REAL 2) : r > (p /. 2) };

        then

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

         A11: q = x and

         A12: r > (q /. 2);

        (q `2 ) < r by A12, JORDAN2B: 29;

        hence thesis by A7, A11;

      end;

      then

       A13: (P ` ) = { p where p be Point of ( TOP-REAL 2) : r > (p /. 2) } by A8;

      reconsider P1 = (P ` ) as Subset of ( TOP-REAL 2);

      P1 is open by A2, A13, JORDAN2B: 12;

      hence thesis by TOPS_1: 3;

    end;

    theorem :: JORDAN6:8

    

     Th8: for r be Real, P be Subset of ( TOP-REAL 2) st P = { p where p be Point of ( TOP-REAL 2) : (p `2 ) <= r } holds P is closed

    proof

      let r be Real, P be Subset of ( TOP-REAL 2);

      assume

       A1: P = { p where p be Point of ( TOP-REAL 2) : (p `2 ) <= r };

      

       A2: 2 in ( Seg 2) by FINSEQ_1: 1;

      

       A3: (P ` ) c= { p where p be Point of ( TOP-REAL 2) : (p `2 ) > r }

      proof

        let x be object;

        assume

         A4: x in (P ` );

        then x in (the carrier of ( TOP-REAL 2) \ P) by SUBSET_1:def 4;

        then

         A5: not x in P by XBOOLE_0:def 5;

        reconsider q = x as Point of ( TOP-REAL 2) by A4;

        (q `2 ) > r by A1, A5;

        hence thesis;

      end;

      { p where p be Point of ( TOP-REAL 2) : (p `2 ) > r } c= (P ` )

      proof

        let x be object;

        assume x in { p where p be Point of ( TOP-REAL 2) : (p `2 ) > r };

        then

         A6: ex p be Point of ( TOP-REAL 2) st (p = x) & ((p `2 ) > r);

        now

          assume x in { q where q be Point of ( TOP-REAL 2) : (q `2 ) <= r };

          then ex q be Point of ( TOP-REAL 2) st (q = x) & ((q `2 ) <= r);

          hence contradiction by A6;

        end;

        then x in (the carrier of ( TOP-REAL 2) \ P) by A1, A6, XBOOLE_0:def 5;

        hence thesis by SUBSET_1:def 4;

      end;

      then

       A7: (P ` ) = { p where p be Point of ( TOP-REAL 2) : (p `2 ) > r } by A3;

      

       A8: (P ` ) c= { p where p be Point of ( TOP-REAL 2) : r < (p /. 2) }

      proof

        let x be object;

        assume x in (P ` );

        then

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

         A9: p = x and

         A10: (p `2 ) > r by A7;

        (p /. 2) > r by A10, JORDAN2B: 29;

        hence thesis by A9;

      end;

      { p where p be Point of ( TOP-REAL 2) : r < (p /. 2) } c= (P ` )

      proof

        let x be object;

        assume x in { p where p be Point of ( TOP-REAL 2) : r < (p /. 2) };

        then

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

         A11: q = x and

         A12: r < (q /. 2);

        (q `2 ) > r by A12, JORDAN2B: 29;

        hence thesis by A7, A11;

      end;

      then

       A13: (P ` ) = { p where p be Point of ( TOP-REAL 2) : r < (p /. 2) } by A8;

      reconsider P1 = (P ` ) as Subset of ( TOP-REAL 2);

      P1 is open by A2, A13, JORDAN2B: 13;

      hence thesis by TOPS_1: 3;

    end;

    theorem :: JORDAN6:9

    

     Th9: for r be Real, P be Subset of ( TOP-REAL 2) st P = { p where p be Point of ( TOP-REAL 2) : (p `2 ) = r } holds P is closed

    proof

      let r be Real, P be Subset of ( TOP-REAL 2);

      assume

       A1: P = { p where p be Point of ( TOP-REAL 2) : (p `2 ) = r };

      defpred P[ Point of ( TOP-REAL 2)] means ($1 `2 ) >= r;

      { p where p be Element of ( TOP-REAL 2) : P[p] } is Subset of ( TOP-REAL 2) from DOMAIN_1:sch 7;

      then

      reconsider P1 = { p where p be Point of ( TOP-REAL 2) : (p `2 ) >= r } as Subset of ( TOP-REAL 2);

      

       A2: P1 is closed by Th7;

      defpred Q[ Point of ( TOP-REAL 2)] means ($1 `2 ) <= r;

      { p where p be Element of ( TOP-REAL 2) : Q[p] } is Subset of ( TOP-REAL 2) from DOMAIN_1:sch 7;

      then

      reconsider P2 = { p where p be Point of ( TOP-REAL 2) : (p `2 ) <= r } as Subset of ( TOP-REAL 2);

      

       A3: P2 is closed by Th8;

      

       A4: P c= (P1 /\ P2)

      proof

        let x be object;

        assume x in P;

        then

         A5: ex p be Point of ( TOP-REAL 2) st (p = x) & ((p `2 ) = r) by A1;

        then

         A6: x in P1;

        x in P2 by A5;

        hence thesis by A6, XBOOLE_0:def 4;

      end;

      (P1 /\ P2) c= P

      proof

        let x be object;

        assume

         A7: x in (P1 /\ P2);

        then

         A8: x in P1 by XBOOLE_0:def 4;

        

         A9: x in P2 by A7, XBOOLE_0:def 4;

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

         A10: q1 = x and

         A11: (q1 `2 ) >= r by A8;

        ex q2 be Point of ( TOP-REAL 2) st (q2 = x) & ((q2 `2 ) <= r) by A9;

        then (q1 `2 ) = r by A10, A11, XXREAL_0: 1;

        hence thesis by A1, A10;

      end;

      then P = (P1 /\ P2) by A4;

      hence thesis by A2, A3, TOPS_1: 8;

    end;

    theorem :: JORDAN6:10

    

     Th10: for P be Subset of ( TOP-REAL n), p1,p2 be Point of ( TOP-REAL n) st P is_an_arc_of (p1,p2) holds P is connected

    proof

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

      assume

       A1: P is_an_arc_of (p1,p2);

      then

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

       A2: f is being_homeomorphism and (f . 0 ) = p1 and (f . 1) = p2 by TOPREAL1:def 1;

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

      

       A3: f is continuous Function of I[01] , (( TOP-REAL n) | P9) by A2, TOPS_2:def 5;

      

       A4: ( [#] I[01] ) is connected by CONNSP_1: 27, TREAL_1: 19;

      

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

      

       A6: ( [#] (( TOP-REAL n) | P)) = P by PRE_TOPC:def 5;

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

      then

       A7: P = (f .: ( [#] I[01] )) by A5, A6, RELAT_1: 113;

      (f .: ( [#] I[01] )) is connected by A3, A4, TOPS_2: 61;

      hence thesis by A7, CONNSP_1: 23;

    end;

    theorem :: JORDAN6: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 P is closed by COMPTS_1: 7, JORDAN5A: 1;

    theorem :: JORDAN6:12

    

     Th12: 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 ex q be Point of ( TOP-REAL 2) st q in P & (q `1 ) = (((p1 `1 ) + (p2 `1 )) / 2)

    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

       A2: p1 in P by TOPREAL1: 1;

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

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

       A3: f is being_homeomorphism and

       A4: (f . 0 ) = p1 and

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

      

       A6: f is continuous by A3, TOPS_2:def 5;

      consider h be Function of ( TOP-REAL 2), R^1 such that

       A7: for p be Element of ( TOP-REAL 2) holds (h . p) = (p /. 1) by JORDAN2B: 1;

      1 in ( Seg 2) by FINSEQ_1: 1;

      then

       A8: h is continuous by A7, JORDAN2B: 18;

      

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

      .= P9 by PRE_TOPC:def 5;

      then

       A10: f is Function of the carrier of I[01] , the carrier of ( TOP-REAL 2) by FUNCT_2: 7;

      reconsider f1 = f as Function of I[01] , ( TOP-REAL 2) by A9, FUNCT_2: 7;

      

       A11: f1 is continuous by A6, Th3;

      reconsider g = (h * f) as Function of I[01] , R^1 by A10;

      

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

      then

       A13: 0 in ( dom f) by XXREAL_1: 1;

      

       A14: 1 in ( dom f) by A12, XXREAL_1: 1;

      

       A15: (g . 0 ) = (h . (f . 0 )) by A13, FUNCT_1: 13

      .= (p1 /. 1) by A4, A7

      .= (p1 `1 ) by JORDAN2B: 29;

      

       A16: (g . 1) = (h . (f . 1)) by A14, FUNCT_1: 13

      .= (p2 /. 1) by A5, A7

      .= (p2 `1 ) by JORDAN2B: 29;

      per cases ;

        suppose (g . 0 ) <> (g . 1);

        then

        consider r1 be Real such that

         A17: 0 < r1 and

         A18: r1 < 1 and

         A19: (g . r1) = (((p1 `1 ) + (p2 `1 )) / 2) by A8, A11, A15, A16, TOPREAL5: 9;

        

         A20: r1 in [. 0 , 1.] by A17, A18, XXREAL_1: 1;

        

         A21: r1 in the carrier of I[01] by A17, A18, BORSUK_1: 40, XXREAL_1: 1;

        then

        reconsider q1 = (f . r1) as Point of ( TOP-REAL 2) by A10, FUNCT_2: 5;

        (g . r1) = (h . (f . r1)) by A12, A20, FUNCT_1: 13

        .= (q1 /. 1) by A7

        .= (q1 `1 ) by JORDAN2B: 29;

        hence thesis by A9, A19, A21, FUNCT_2: 5;

      end;

        suppose (g . 0 ) = (g . 1);

        hence thesis by A2, A15, A16;

      end;

    end;

    theorem :: JORDAN6:13

    

     Th13: 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) & Q = { q : (q `1 ) = (((p1 `1 ) + (p2 `1 )) / 2) } holds P meets Q & (P /\ Q) is closed

    proof

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

      reconsider W = P as Subset of ( TOP-REAL 2);

      assume

       A1: P is_an_arc_of (p1,p2) & Q = { q : (q `1 ) = (((p1 `1 ) + (p2 `1 )) / 2) };

      consider f be Function of ( TOP-REAL 2), R^1 such that

       A2: for p be Element of ( TOP-REAL 2) holds (f . p) = (p /. 1) by JORDAN2B: 1;

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

      

       A3: 1 in ( Seg 2) by FINSEQ_1: 1;

      

       A4: ( dom f) = the carrier of ( TOP-REAL 2) by FUNCT_2:def 1;

      

       A5: ( [#] (( TOP-REAL 2) | P)) = P by PRE_TOPC:def 5;

      then

       A6: the carrier of (( TOP-REAL 2) | P9) = P9;

      

       A7: ( dom (f | P)) = (the carrier of ( TOP-REAL 2) /\ P) by A4, RELAT_1: 61

      .= P by XBOOLE_1: 28;

      ( rng (f | P)) c= the carrier of R^1 ;

      then

      reconsider g = (f | P) as Function of (( TOP-REAL 2) | P), R^1 by A5, A7, FUNCT_2:def 1, RELSET_1: 4;

      reconsider g as continuous Function of (( TOP-REAL 2) | P9), R^1 by A2, A3, JORDAN2B: 18, TOPMETR: 7;

      

       A8: p1 in P by A1, TOPREAL1: 1;

      

       A9: p2 in P by A1, TOPREAL1: 1;

      reconsider p19 = p1, p29 = p2 as Point of (( TOP-REAL 2) | P) by A1, A5, TOPREAL1: 1;

      

       A10: (g . p19) = (f . p1) by A8, FUNCT_1: 49

      .= (p1 /. 1) by A2

      .= (p1 `1 ) by JORDAN2B: 29;

      

       A11: (g . p29) = (f . p2) by A9, FUNCT_1: 49

      .= (p2 /. 1) by A2

      .= (p2 `1 ) by JORDAN2B: 29;

      W is connected by A1, Th10;

      then

       A12: (( TOP-REAL 2) | P) is connected by CONNSP_1:def 3;

       A13:

      now

        per cases ;

          case

           A14: (p1 `1 ) <= (p2 `1 );

          then

           A15: (p1 `1 ) <= (((p1 `1 ) + (p2 `1 )) / 2) by Th1;

          (((p1 `1 ) + (p2 `1 )) / 2) <= (p2 `1 ) by A14, Th1;

          then

          consider xc be Point of (( TOP-REAL 2) | P) such that

           A16: (g . xc) = (((p1 `1 ) + (p2 `1 )) / 2) by A10, A11, A12, A15, TOPREAL5: 4;

          xc in P by A6;

          then

          reconsider pc = xc as Point of ( TOP-REAL 2);

          (g . xc) = (f . xc) by A5, FUNCT_1: 49

          .= (pc /. 1) by A2

          .= (pc `1 ) by JORDAN2B: 29;

          then xc in Q by A1, A16;

          hence P meets Q by A6, XBOOLE_0: 3;

        end;

          case

           A17: (p1 `1 ) > (p2 `1 );

          then

           A18: (p2 `1 ) <= (((p1 `1 ) + (p2 `1 )) / 2) by Th1;

          (((p1 `1 ) + (p2 `1 )) / 2) <= (p1 `1 ) by A17, Th1;

          then

          consider xc be Point of (( TOP-REAL 2) | P) such that

           A19: (g . xc) = (((p1 `1 ) + (p2 `1 )) / 2) by A10, A11, A12, A18, TOPREAL5: 4;

          xc in P by A6;

          then

          reconsider pc = xc as Point of ( TOP-REAL 2);

          (g . xc) = (f . xc) by A5, FUNCT_1: 49

          .= (pc /. 1) by A2

          .= (pc `1 ) by JORDAN2B: 29;

          then xc in Q by A1, A19;

          hence P meets Q by A6, XBOOLE_0: 3;

        end;

      end;

      reconsider P1 = P, Q1 = Q as Subset of ( TOP-REAL 2);

      

       A20: P1 is closed by A1, COMPTS_1: 7, JORDAN5A: 1;

      Q1 is closed by A1, Th6;

      hence thesis by A13, A20, TOPS_1: 8;

    end;

    theorem :: JORDAN6:14

    

     Th14: 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) & Q = { q : (q `2 ) = (((p1 `2 ) + (p2 `2 )) / 2) } holds P meets Q & (P /\ Q) is closed

    proof

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

      assume

       A1: P is_an_arc_of (p1,p2) & Q1 = { q : (q `2 ) = (((p1 `2 ) + (p2 `2 )) / 2) };

      consider f be Function of ( TOP-REAL 2), R^1 such that

       A2: for p be Element of ( TOP-REAL 2) holds (f . p) = (p /. 2) by JORDAN2B: 1;

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

      

       A3: 2 in ( Seg 2) by FINSEQ_1: 1;

      

       A4: ( dom f) = the carrier of ( TOP-REAL 2) by FUNCT_2:def 1;

      

       A5: ( [#] (( TOP-REAL 2) | P)) = P by PRE_TOPC:def 5;

      then

       A6: the carrier of (( TOP-REAL 2) | P9) = P9;

      

       A7: ( dom (f | P)) = (the carrier of ( TOP-REAL 2) /\ P) by A4, RELAT_1: 61

      .= P by XBOOLE_1: 28;

      ( rng (f | P)) c= the carrier of R^1 ;

      then

      reconsider g = (f | P) as Function of (( TOP-REAL 2) | P), R^1 by A5, A7, FUNCT_2:def 1, RELSET_1: 4;

      reconsider g as continuous Function of (( TOP-REAL 2) | P9), R^1 by A2, A3, JORDAN2B: 18, TOPMETR: 7;

      

       A8: p1 in P by A1, TOPREAL1: 1;

      

       A9: p2 in P by A1, TOPREAL1: 1;

      reconsider p19 = p1, p29 = p2 as Point of (( TOP-REAL 2) | P) by A1, A5, TOPREAL1: 1;

      

       A10: (g . p19) = (f . p1) by A8, FUNCT_1: 49

      .= (p1 /. 2) by A2

      .= (p1 `2 ) by JORDAN2B: 29;

      

       A11: (g . p29) = (f . p2) by A9, FUNCT_1: 49

      .= (p2 /. 2) by A2

      .= (p2 `2 ) by JORDAN2B: 29;

      reconsider W = P as Subset of ( TOP-REAL 2);

      W is connected by A1, Th10;

      then

       A12: (( TOP-REAL 2) | P) is connected by CONNSP_1:def 3;

       A13:

      now

        per cases ;

          case

           A14: (p1 `2 ) <= (p2 `2 );

          then

           A15: (p1 `2 ) <= (((p1 `2 ) + (p2 `2 )) / 2) by Th1;

          (((p1 `2 ) + (p2 `2 )) / 2) <= (p2 `2 ) by A14, Th1;

          then

          consider xc be Point of (( TOP-REAL 2) | P) such that

           A16: (g . xc) = (((p1 `2 ) + (p2 `2 )) / 2) by A10, A11, A12, A15, TOPREAL5: 4;

          xc in P by A6;

          then

          reconsider pc = xc as Point of ( TOP-REAL 2);

          (g . xc) = (f . xc) by A5, FUNCT_1: 49

          .= (pc /. 2) by A2

          .= (pc `2 ) by JORDAN2B: 29;

          then xc in Q1 by A1, A16;

          hence P meets Q1 by A6, XBOOLE_0: 3;

        end;

          case

           A17: (p1 `2 ) > (p2 `2 );

          then

           A18: (p2 `2 ) <= (((p1 `2 ) + (p2 `2 )) / 2) by Th1;

          (((p1 `2 ) + (p2 `2 )) / 2) <= (p1 `2 ) by A17, Th1;

          then

          consider xc be Point of (( TOP-REAL 2) | P) such that

           A19: (g . xc) = (((p1 `2 ) + (p2 `2 )) / 2) by A10, A11, A12, A18, TOPREAL5: 4;

          xc in P by A6;

          then

          reconsider pc = xc as Point of ( TOP-REAL 2);

          (g . xc) = (f . xc) by A5, FUNCT_1: 49

          .= (pc /. 2) by A2

          .= (pc `2 ) by JORDAN2B: 29;

          then xc in Q1 by A1, A19;

          hence P meets Q1 by A6, XBOOLE_0: 3;

        end;

      end;

      reconsider P1 = P, Q2 = Q1 as Subset of ( TOP-REAL 2);

      

       A20: P1 is closed by A1, COMPTS_1: 7, JORDAN5A: 1;

      Q2 is closed by A1, Th9;

      hence thesis by A13, A20, TOPS_1: 8;

    end;

    definition

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

      :: JORDAN6:def1

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

      : Def1: for Q be Subset of ( TOP-REAL 2) st Q = { q : (q `1 ) = (((p1 `1 ) + (p2 `1 )) / 2) } holds it = ( First_Point (P,p1,p2,Q));

      existence

      proof

        { q : (q `1 ) = (((p1 `1 ) + (p2 `1 )) / 2) } c= the carrier of ( TOP-REAL 2)

        proof

          let x be object;

          assume x in { q : (q `1 ) = (((p1 `1 ) + (p2 `1 )) / 2) };

          then ex q be Point of ( TOP-REAL 2) st (q = x) & ((q `1 ) = (((p1 `1 ) + (p2 `1 )) / 2));

          hence thesis;

        end;

        then

        reconsider Q1 = { q : (q `1 ) = (((p1 `1 ) + (p2 `1 )) / 2) } as Subset of ( TOP-REAL 2);

        reconsider q2 = ( First_Point (P,p1,p2,Q1)) as Point of ( TOP-REAL 2);

        for Q be Subset of ( TOP-REAL 2) st Q = { q : (q `1 ) = (((p1 `1 ) + (p2 `1 )) / 2) } holds q2 = ( First_Point (P,p1,p2,Q));

        hence thesis;

      end;

      uniqueness

      proof

        let q3,q4 be Point of ( TOP-REAL 2);

        assume

         A1: (for Q1 be Subset of ( TOP-REAL 2) st Q1 = { q1 : (q1 `1 ) = (((p1 `1 ) + (p2 `1 )) / 2) } holds q3 = ( First_Point (P,p1,p2,Q1))) & for Q2 be Subset of ( TOP-REAL 2) st Q2 = { q2 : (q2 `1 ) = (((p1 `1 ) + (p2 `1 )) / 2) } holds q4 = ( First_Point (P,p1,p2,Q2));

        { q1 : (q1 `1 ) = (((p1 `1 ) + (p2 `1 )) / 2) } c= the carrier of ( TOP-REAL 2)

        proof

          let x be object;

          assume x in { q1 : (q1 `1 ) = (((p1 `1 ) + (p2 `1 )) / 2) };

          then ex q be Point of ( TOP-REAL 2) st (q = x) & ((q `1 ) = (((p1 `1 ) + (p2 `1 )) / 2));

          hence thesis;

        end;

        then

        reconsider Q3 = { q2 : (q2 `1 ) = (((p1 `1 ) + (p2 `1 )) / 2) } as Subset of ( TOP-REAL 2);

        q3 = ( First_Point (P,p1,p2,Q3)) by A1;

        hence thesis by A1;

      end;

    end

    definition

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

      :: JORDAN6:def2

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

      : Def2: for Q be Subset of ( TOP-REAL 2) st Q = { q : (q `2 ) = (((p1 `2 ) + (p2 `2 )) / 2) } holds it = ( First_Point (P,p1,p2,Q));

      existence

      proof

        { q : (q `2 ) = (((p1 `2 ) + (p2 `2 )) / 2) } c= the carrier of ( TOP-REAL 2)

        proof

          let x be object;

          assume x in { q : (q `2 ) = (((p1 `2 ) + (p2 `2 )) / 2) };

          then ex q be Point of ( TOP-REAL 2) st (q = x) & ((q `2 ) = (((p1 `2 ) + (p2 `2 )) / 2));

          hence thesis;

        end;

        then

        reconsider Q1 = { q : (q `2 ) = (((p1 `2 ) + (p2 `2 )) / 2) } as Subset of ( TOP-REAL 2);

        reconsider q2 = ( First_Point (P,p1,p2,Q1)) as Point of ( TOP-REAL 2);

        for Q be Subset of ( TOP-REAL 2) st Q = { q : (q `2 ) = (((p1 `2 ) + (p2 `2 )) / 2) } holds q2 = ( First_Point (P,p1,p2,Q));

        hence thesis;

      end;

      uniqueness

      proof

        let q3,q4 be Point of ( TOP-REAL 2);

        assume

         A1: (for Q1 be Subset of ( TOP-REAL 2) st Q1 = { q1 : (q1 `2 ) = (((p1 `2 ) + (p2 `2 )) / 2) } holds q3 = ( First_Point (P,p1,p2,Q1))) & for Q2 be Subset of ( TOP-REAL 2) st Q2 = { q2 : (q2 `2 ) = (((p1 `2 ) + (p2 `2 )) / 2) } holds q4 = ( First_Point (P,p1,p2,Q2));

        { q1 : (q1 `2 ) = (((p1 `2 ) + (p2 `2 )) / 2) } c= the carrier of ( TOP-REAL 2)

        proof

          let x be object;

          assume x in { q1 : (q1 `2 ) = (((p1 `2 ) + (p2 `2 )) / 2) };

          then ex q be Point of ( TOP-REAL 2) st (q = x) & ((q `2 ) = (((p1 `2 ) + (p2 `2 )) / 2));

          hence thesis;

        end;

        then

        reconsider Q3 = { q2 : (q2 `2 ) = (((p1 `2 ) + (p2 `2 )) / 2) } as Subset of ( TOP-REAL 2);

        q3 = ( First_Point (P,p1,p2,Q3)) by A1;

        hence thesis by A1;

      end;

    end

    theorem :: JORDAN6:15

    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 ( x_Middle (P,p1,p2)) in P & ( y_Middle (P,p1,p2)) in P

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

      deffunc F( Point of ( TOP-REAL 2)) = $1;

      defpred P[ Point of ( TOP-REAL 2)] means ($1 `1 ) = (((p1 `1 ) + (p2 `1 )) / 2);

      reconsider Q = { F(q) : P[q] } as Subset of ( TOP-REAL 2) from DOMAIN_1:sch 8;

      

       A2: ( x_Middle (P,p1,p2)) = ( First_Point (P,p1,p2,Q)) by Def1;

      

       A3: P meets Q by A1, Th13;

      (P /\ Q) is closed by A1, Th13;

      then

       A4: ( x_Middle (P,p1,p2)) in (P /\ Q) by A1, A2, A3, JORDAN5C:def 1;

      defpred Q[ Point of ( TOP-REAL 2)] means ($1 `2 ) = (((p1 `2 ) + (p2 `2 )) / 2);

      reconsider Q2 = { F(q) : Q[q] } as Subset of ( TOP-REAL 2) from DOMAIN_1:sch 8;

      

       A5: ( y_Middle (P,p1,p2)) = ( First_Point (P,p1,p2,Q2)) by Def2;

      

       A6: P meets Q2 by A1, Th14;

      (P /\ Q2) is closed by A1, Th14;

      then ( y_Middle (P,p1,p2)) in (P /\ Q2) by A1, A5, A6, JORDAN5C:def 1;

      hence thesis by A4, XBOOLE_0:def 4;

    end;

    theorem :: JORDAN6:16

    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 p1 = ( x_Middle (P,p1,p2)) iff (p1 `1 ) = (p2 `1 )

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

       A2:

      now

        assume

         A3: p1 = ( x_Middle (P,p1,p2));

        deffunc F( Point of ( TOP-REAL 2)) = $1;

        defpred P[ Point of ( TOP-REAL 2)] means ($1 `1 ) = (((p1 `1 ) + (p2 `1 )) / 2);

        reconsider Q1 = { F(q) : P[q] } as Subset of ( TOP-REAL 2) from DOMAIN_1:sch 8;

        

         A4: P meets Q1 by A1, Th13;

        

         A5: (P /\ Q1) is closed by A1, Th13;

        ( x_Middle (P,p1,p2)) = ( First_Point (P,p1,p2,Q1)) by Def1;

        then p1 in (P /\ Q1) by A1, A3, A4, A5, JORDAN5C:def 1;

        then p1 in Q1 by XBOOLE_0:def 4;

        then ex q st q = p1 & (q `1 ) = (((p1 `1 ) + (p2 `1 )) / 2);

        hence (p1 `1 ) = (p2 `1 );

      end;

      now

        assume

         A6: (p1 `1 ) = (p2 `1 );

        for Q be Subset of ( TOP-REAL 2) st Q = { q : (q `1 ) = (((p1 `1 ) + (p2 `1 )) / 2) } holds p1 = ( First_Point (P,p1,p2,Q))

        proof

          let Q be Subset of ( TOP-REAL 2);

          assume

           A7: Q = { q : (q `1 ) = (((p1 `1 ) + (p2 `1 )) / 2) };

          then

           A8: p1 in Q by A6;

          (P /\ Q) is closed by A1, A7, Th13;

          hence thesis by A1, A8, JORDAN5C: 3;

        end;

        hence p1 = ( x_Middle (P,p1,p2)) by Def1;

      end;

      hence thesis by A2;

    end;

    theorem :: JORDAN6:17

    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 p1 = ( y_Middle (P,p1,p2)) iff (p1 `2 ) = (p2 `2 )

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

       A2:

      now

        assume

         A3: p1 = ( y_Middle (P,p1,p2));

        deffunc F( Point of ( TOP-REAL 2)) = $1;

        defpred P[ Point of ( TOP-REAL 2)] means ($1 `2 ) = (((p1 `2 ) + (p2 `2 )) / 2);

        reconsider Q1 = { F(q) : P[q] } as Subset of ( TOP-REAL 2) from DOMAIN_1:sch 8;

        

         A4: P meets Q1 by A1, Th14;

        

         A5: (P /\ Q1) is closed by A1, Th14;

        ( y_Middle (P,p1,p2)) = ( First_Point (P,p1,p2,Q1)) by Def2;

        then p1 in (P /\ Q1) by A1, A3, A4, A5, JORDAN5C:def 1;

        then p1 in Q1 by XBOOLE_0:def 4;

        then ex q st (q = p1) & ((q `2 ) = (((p1 `2 ) + (p2 `2 )) / 2));

        hence (p1 `2 ) = (p2 `2 );

      end;

      now

        assume

         A6: (p1 `2 ) = (p2 `2 );

        for Q be Subset of ( TOP-REAL 2) st Q = { q : (q `2 ) = (((p1 `2 ) + (p2 `2 )) / 2) } holds p1 = ( First_Point (P,p1,p2,Q))

        proof

          let Q be Subset of ( TOP-REAL 2);

          assume

           A7: Q = { q : (q `2 ) = (((p1 `2 ) + (p2 `2 )) / 2) };

          then

           A8: p1 in Q by A6;

          (P /\ Q) is closed by A1, A7, Th14;

          hence thesis by A1, A8, JORDAN5C: 3;

        end;

        hence p1 = ( y_Middle (P,p1,p2)) by Def2;

      end;

      hence thesis by A2;

    end;

    begin

    theorem :: JORDAN6:18

    

     Th18: 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) holds LE (q2,q1,P,p2,p1)

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

      thus q2 in P & q1 in P by A2;

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

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

      assume that

       A3: f is being_homeomorphism and

       A4: (f . 0 ) = p2 and

       A5: (f . 1) = p1 and

       A6: (f . s1) = q2 and

       A7: 0 <= s1 and

       A8: s1 <= 1 and

       A9: (f . s2) = q1 and

       A10: 0 <= s2 and

       A11: s2 <= 1;

      

       A12: (1 - 0 ) >= (1 - s1) by A7, XREAL_1: 13;

      

       A13: (1 - 0 ) >= (1 - s2) by A10, XREAL_1: 13;

      

       A14: (1 - 1) <= (1 - s1) by A8, XREAL_1: 13;

      

       A15: (1 - 1) <= (1 - s2) by A11, XREAL_1: 13;

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

      

       A16: Ex is being_homeomorphism by TREAL_1: 18;

      set g = (f * Ex);

      

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

      

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

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

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

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

      then

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

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

      

       A20: g is being_homeomorphism by A3, A16, TOPMETR: 20, TOPS_2: 57;

      

       A21: (1 - s1) in ( dom g) by A12, A14, A19, BORSUK_1: 43;

      

       A22: (1 - s2) in ( dom g) by A13, A15, A19, BORSUK_1: 43;

      

       A23: (g . 0 ) = p1 by A5, A18, A19, BORSUK_1:def 14, FUNCT_1: 12, TREAL_1: 5;

      

       A24: (g . 1) = p2 by A4, A17, A19, BORSUK_1:def 15, FUNCT_1: 12, TREAL_1: 5;

      reconsider qs1 = (1 - s1), qs2 = (1 - s2) as Point of ( Closed-Interval-TSpace ( 0 ,1)) by A12, A13, A14, A15, BORSUK_1: 43, TOPMETR: 20;

      

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

      .= s1;

      

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

      .= s2;

      

       A27: (g . (1 - s1)) = q2 by A6, A21, A25, FUNCT_1: 12;

      (g . (1 - s2)) = q1 by A9, A22, A26, FUNCT_1: 12;

      then (1 - s2) <= (1 - s1) by A2, A12, A13, A14, A20, A23, A24, A27;

      then s1 <= (1 - (1 - s2)) by XREAL_1: 11;

      hence thesis;

    end;

    definition

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

      :: JORDAN6:def3

      func L_Segment (P,p1,p2,q1) -> Subset of ( TOP-REAL 2) equals { q : LE (q,q1,P,p1,p2) };

      coherence

      proof

        { q : LE (q,q1,P,p1,p2) } c= the carrier of ( TOP-REAL 2)

        proof

          let x be object;

          assume x in { q : LE (q,q1,P,p1,p2) };

          then ex q st (q = x) & ( LE (q,q1,P,p1,p2));

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

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

      :: JORDAN6:def4

      func R_Segment (P,p1,p2,q1) -> Subset of ( TOP-REAL 2) equals { q : LE (q1,q,P,p1,p2) };

      coherence

      proof

        { q : LE (q1,q,P,p1,p2) } c= the carrier of ( TOP-REAL 2)

        proof

          let x be object;

          assume x in { q : LE (q1,q,P,p1,p2) };

          then ex q st (q = x) & ( LE (q1,q,P,p1,p2));

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: JORDAN6:19

    

     Th19: for P be Subset of ( TOP-REAL 2), p1,p2,q1 be Point of ( TOP-REAL 2) holds ( L_Segment (P,p1,p2,q1)) c= P

    proof

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

      let x be object;

      assume x in ( L_Segment (P,p1,p2,q1));

      then ex q st q = x & LE (q,q1,P,p1,p2);

      hence thesis;

    end;

    theorem :: JORDAN6:20

    

     Th20: for P be Subset of ( TOP-REAL 2), p1,p2,q1 be Point of ( TOP-REAL 2) holds ( R_Segment (P,p1,p2,q1)) c= P

    proof

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

      let x be object;

      assume x in ( R_Segment (P,p1,p2,q1));

      then ex q st q = x & LE (q1,q,P,p1,p2);

      hence thesis;

    end;

    theorem :: JORDAN6:21

    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 ( L_Segment (P,p1,p2,p1)) = {p1}

    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

       A2: p1 in P by TOPREAL1: 1;

      thus ( L_Segment (P,p1,p2,p1)) c= {p1}

      proof

        let x be object;

        assume x in ( L_Segment (P,p1,p2,p1));

        then

        consider q such that

         A3: q = x and

         A4: LE (q,p1,P,p1,p2);

        q in P by A4;

        then LE (p1,q,P,p1,p2) by A1, JORDAN5C: 10;

        then q = p1 by A1, A4, JORDAN5C: 12;

        hence thesis by A3, TARSKI:def 1;

      end;

      let x be object;

      assume x in {p1};

      then

       A5: x = p1 by TARSKI:def 1;

       LE (p1,p1,P,p1,p2) by A2, JORDAN5C: 9;

      hence thesis by A5;

    end;

    theorem :: JORDAN6:22

    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 ( L_Segment (P,p1,p2,p2)) = P

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

      thus ( L_Segment (P,p1,p2,p2)) c= P by Th19;

      let x be object;

      assume

       A2: x in P;

      then

      reconsider p = x as Point of ( TOP-REAL 2);

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

      hence thesis;

    end;

    theorem :: JORDAN6:23

    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 ( R_Segment (P,p1,p2,p2)) = {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

       A2: p2 in P by TOPREAL1: 1;

      thus ( R_Segment (P,p1,p2,p2)) c= {p2}

      proof

        let x be object;

        assume x in ( R_Segment (P,p1,p2,p2));

        then

        consider q such that

         A3: q = x and

         A4: LE (p2,q,P,p1,p2);

        q in P by A4;

        then LE (q,p2,P,p1,p2) by A1, JORDAN5C: 10;

        then q = p2 by A1, A4, JORDAN5C: 12;

        hence thesis by A3, TARSKI:def 1;

      end;

      let x be object;

      assume x in {p2};

      then

       A5: x = p2 by TARSKI:def 1;

       LE (p2,p2,P,p1,p2) by A2, JORDAN5C: 9;

      hence thesis by A5;

    end;

    theorem :: JORDAN6:24

    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 ( R_Segment (P,p1,p2,p1)) = P

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

      thus ( R_Segment (P,p1,p2,p1)) c= P by Th20;

      let x be object;

      assume

       A2: x in P;

      then

      reconsider p = x as Point of ( TOP-REAL 2);

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

      hence thesis;

    end;

    theorem :: JORDAN6:25

    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) holds ( R_Segment (P,p1,p2,q1)) = ( L_Segment (P,p2,p1,q1))

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

      

       A2: { q : LE (q1,q,P,p1,p2) } c= { q2 : LE (q2,q1,P,p2,p1) }

      proof

        let x be object;

        assume x in { q : LE (q1,q,P,p1,p2) };

        then

        consider q such that

         A3: q = x and

         A4: LE (q1,q,P,p1,p2);

         LE (q,q1,P,p2,p1) by A1, A4, Th18;

        hence thesis by A3;

      end;

      { q2 : LE (q2,q1,P,p2,p1) } c= { q : LE (q1,q,P,p1,p2) }

      proof

        let x be object;

        assume x in { q : LE (q,q1,P,p2,p1) };

        then

        consider q such that

         A5: q = x and

         A6: LE (q,q1,P,p2,p1);

         LE (q1,q,P,p1,p2) by A1, A6, Th18, JORDAN5B: 14;

        hence thesis by A5;

      end;

      hence thesis by A2;

    end;

    definition

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

      :: JORDAN6:def5

      func Segment (P,p1,p2,q1,q2) -> Subset of ( TOP-REAL 2) equals (( R_Segment (P,p1,p2,q1)) /\ ( L_Segment (P,p1,p2,q2)));

      correctness ;

    end

    theorem :: JORDAN6:26

    for P be Subset of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2) holds ( Segment (P,p1,p2,q1,q2)) = { q : LE (q1,q,P,p1,p2) & LE (q,q2,P,p1,p2) }

    proof

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

      thus ( Segment (P,p1,p2,q1,q2)) c= { q : LE (q1,q,P,p1,p2) & LE (q,q2,P,p1,p2) }

      proof

        let x be object;

        assume

         A1: x in ( Segment (P,p1,p2,q1,q2));

        then

         A2: x in ( R_Segment (P,p1,p2,q1)) by XBOOLE_0:def 4;

        

         A3: x in ( L_Segment (P,p1,p2,q2)) by A1, XBOOLE_0:def 4;

        

         A4: ex q st (q = x) & ( LE (q1,q,P,p1,p2)) by A2;

        ex p st (p = x) & ( LE (p,q2,P,p1,p2)) by A3;

        hence thesis by A4;

      end;

      let x be object;

      assume x in { q : LE (q1,q,P,p1,p2) & LE (q,q2,P,p1,p2) };

      then

       A5: ex q st (q = x) & ( LE (q1,q,P,p1,p2)) & ( LE (q,q2,P,p1,p2));

      then

       A6: x in ( R_Segment (P,p1,p2,q1));

      x in ( L_Segment (P,p1,p2,q2)) by A5;

      hence thesis by A6, XBOOLE_0:def 4;

    end;

    theorem :: JORDAN6:27

    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 (q2,q1,P,p2,p1) holds LE (q1,q2,P,p1,p2) by Th18, JORDAN5B: 14;

    theorem :: JORDAN6:28

    

     Th28: for P be Subset of ( TOP-REAL 2), p1,p2,q be Point of ( TOP-REAL 2) st P is_an_arc_of (p1,p2) holds ( L_Segment (P,p1,p2,q)) = ( R_Segment (P,p2,p1,q))

    proof

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

      assume that

       A1: P is_an_arc_of (p1,p2);

      thus ( L_Segment (P,p1,p2,q)) c= ( R_Segment (P,p2,p1,q))

      proof

        let x be object;

        assume x in ( L_Segment (P,p1,p2,q));

        then

        consider p such that

         A2: p = x and

         A3: LE (p,q,P,p1,p2);

         LE (q,p,P,p2,p1) by A1, A3, Th18;

        hence thesis by A2;

      end;

      let x be object;

      assume x in ( R_Segment (P,p2,p1,q));

      then

      consider p such that

       A4: p = x and

       A5: LE (q,p,P,p2,p1);

       LE (p,q,P,p1,p2) by A1, A5, Th18, JORDAN5B: 14;

      hence thesis by A4;

    end;

    theorem :: JORDAN6:29

    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) holds ( Segment (P,p1,p2,q1,q2)) = ( Segment (P,p2,p1,q2,q1))

    proof

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

      assume

       A1: P is_an_arc_of (p1,p2);

      then ( L_Segment (P,p1,p2,q2)) = ( R_Segment (P,p2,p1,q2)) by Th28;

      hence thesis by A1, Th28, JORDAN5B: 14;

    end;

    begin

    definition

      let s be Real;

      :: JORDAN6:def6

      func Vertical_Line (s) -> Subset of ( TOP-REAL 2) equals { p where p be Point of ( TOP-REAL 2) : (p `1 ) = s };

      correctness

      proof

        { p where p be Point of ( TOP-REAL 2) : (p `1 ) = s } c= the carrier of ( TOP-REAL 2)

        proof

          let x be object;

          assume x in { p where p be Point of ( TOP-REAL 2) : (p `1 ) = s };

          then ex p be Point of ( TOP-REAL 2) st p = x & (p `1 ) = s;

          hence thesis;

        end;

        hence thesis;

      end;

      :: JORDAN6:def7

      func Horizontal_Line (s) -> Subset of ( TOP-REAL 2) equals { p : (p `2 ) = s };

      correctness

      proof

        { p where p be Point of ( TOP-REAL 2) : (p `2 ) = s } c= the carrier of ( TOP-REAL 2)

        proof

          let x be object;

          assume x in { p where p be Point of ( TOP-REAL 2) : (p `2 ) = s };

          then ex p be Point of ( TOP-REAL 2) st p = x & (p `2 ) = s;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: JORDAN6:30

    for r be Real holds ( Vertical_Line r) is closed & ( Horizontal_Line r) is closed by Th6, Th9;

    theorem :: JORDAN6:31

    

     Th31: for r be Real, p be Point of ( TOP-REAL 2) holds p in ( Vertical_Line r) iff (p `1 ) = r

    proof

      let r be Real, p be Point of ( TOP-REAL 2);

      hereby

        assume p in ( Vertical_Line r);

        then ex q be Point of ( TOP-REAL 2) st q = p & (q `1 ) = r;

        hence (p `1 ) = r;

      end;

      assume (p `1 ) = r;

      hence thesis;

    end;

    theorem :: JORDAN6:32

    for r be Real, p be Point of ( TOP-REAL 2) holds p in ( Horizontal_Line r) iff (p `2 ) = r

    proof

      let r be Real, p be Point of ( TOP-REAL 2);

      hereby

        assume p in ( Horizontal_Line r);

        then ex q be Point of ( TOP-REAL 2) st q = p & (q `2 ) = r;

        hence (p `2 ) = r;

      end;

      assume (p `2 ) = r;

      hence thesis;

    end;

    theorem :: JORDAN6:33

    

     Th33: for P be Subset of ( TOP-REAL 2) st P is being_simple_closed_curve holds ex P1,P2 be non empty Subset of ( TOP-REAL 2) st P1 is_an_arc_of (( W-min P),( E-max P)) & P2 is_an_arc_of (( E-max P),( W-min P)) & (P1 /\ P2) = {( W-min P), ( E-max P)} & (P1 \/ P2) = P & (( First_Point (P1,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) > (( Last_Point (P2,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 )

    proof

      let P be Subset of ( TOP-REAL 2);

      assume P is being_simple_closed_curve;

      then

      reconsider P as Simple_closed_curve;

      

       A1: ( W-min P) in P by SPRECT_1: 13;

      

       A2: ( E-max P) in P by SPRECT_1: 14;

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

      then

      consider P01,P02 be non empty Subset of ( TOP-REAL 2) such that

       A3: P01 is_an_arc_of (( W-min P),( E-max P)) and

       A4: P02 is_an_arc_of (( W-min P),( E-max P)) and

       A5: P = (P01 \/ P02) and

       A6: (P01 /\ P02) = {( W-min P), ( E-max P)} by A1, A2, TOPREAL2: 5;

      reconsider P01, P02 as non empty Subset of ( TOP-REAL 2);

      

       A7: P01 is_an_arc_of (( E-max P),( W-min P)) by A3, JORDAN5B: 14;

      

       A8: P02 is_an_arc_of (( E-max P),( W-min P)) by A4, JORDAN5B: 14;

      reconsider P001 = P01, P002 = P02 as non empty Subset of ( TOP-REAL 2);

      

       A9: (( E-max P) `1 ) = ( E-bound P) by EUCLID: 52;

      

       A10: ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)) is closed by Th6;

      P01 is closed by A3, COMPTS_1: 7, JORDAN5A: 1;

      then

       A11: (P01 /\ ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2))) is closed by A10, TOPS_1: 8;

      

       A12: ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)) is closed by Th6;

      P02 is closed by A4, COMPTS_1: 7, JORDAN5A: 1;

      then

       A13: (P02 /\ ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2))) is closed by A12, TOPS_1: 8;

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

       A14: q1 in P001 and

       A15: (q1 `1 ) = (((( W-min P) `1 ) + (( E-max P) `1 )) / 2) by A3, Th12;

      

       A16: (( W-min P) `1 ) = ( W-bound P) by EUCLID: 52;

      (( E-max P) `1 ) = ( E-bound P) by EUCLID: 52;

      then q1 in { p where p be Point of ( TOP-REAL 2) : (p `1 ) = ((( W-bound P) + ( E-bound P)) / 2) } by A15, A16;

      then (P01 /\ ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2))) <> {} by A14, XBOOLE_0:def 4;

      then

       A17: P01 meets ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2));

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

       A18: q2 in P002 and

       A19: (q2 `1 ) = (((( W-min P) `1 ) + (( E-max P) `1 )) / 2) by A4, Th12;

      q2 in { p where p be Point of ( TOP-REAL 2) : (p `1 ) = ((( W-bound P) + ( E-bound P)) / 2) } by A9, A16, A19;

      then (P02 /\ ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2))) <> {} by A18, XBOOLE_0:def 4;

      then

       A20: P02 meets ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2));

      per cases ;

        suppose (( First_Point (P01,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) > (( Last_Point (P02,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 );

        hence thesis by A3, A5, A6, A8;

      end;

        suppose

         A21: (( First_Point (P01,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) <= (( Last_Point (P02,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 );

        now

          per cases by A21, XXREAL_0: 1;

            case

             A22: (( First_Point (P01,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) < (( Last_Point (P02,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 );

            

             A23: ( First_Point (P01,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) = ( Last_Point (P01,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) by A3, A11, A17, JORDAN5C: 18;

            ( Last_Point (P02,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) = ( First_Point (P02,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) by A4, A13, A20, JORDAN5C: 18;

            hence ex P1,P2 be non empty Subset of ( TOP-REAL 2) st P1 is_an_arc_of (( W-min P),( E-max P)) & P2 is_an_arc_of (( E-max P),( W-min P)) & (P1 /\ P2) = {( W-min P), ( E-max P)} & (P1 \/ P2) = P & (( First_Point (P1,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) > (( Last_Point (P2,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) by A4, A5, A6, A7, A22, A23;

          end;

            case

             A24: (( First_Point (P01,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) = (( Last_Point (P02,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 );

            set p = ( First_Point (P01,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2))));

            set p9 = ( Last_Point (P02,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2))));

            

             A25: p in (P01 /\ ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2))) by A3, A11, A17, JORDAN5C:def 1;

            then

             A26: p in P01 by XBOOLE_0:def 4;

            p in ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)) by A25, XBOOLE_0:def 4;

            then

             A27: (p `1 ) = ((( W-bound P) + ( E-bound P)) / 2) by Th31;

            

             A28: p9 in (P02 /\ ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2))) by A8, A13, A20, JORDAN5C:def 2;

            then

             A29: p9 in P02 by XBOOLE_0:def 4;

            p9 in ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)) by A28, XBOOLE_0:def 4;

            then (p9 `1 ) = ((( W-bound P) + ( E-bound P)) / 2) by Th31;

            then p = p9 by A24, A27, TOPREAL3: 6;

            then p in (P01 /\ P02) by A26, A29, XBOOLE_0:def 4;

            then p = ( W-min P) or p = ( E-max P) by A6, TARSKI:def 2;

            hence contradiction by A9, A16, A27, TOPREAL5: 17;

          end;

        end;

        then

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

         A30: P1 is_an_arc_of (( W-min P),( E-max P)) and

         A31: P2 is_an_arc_of (( E-max P),( W-min P)) and

         A32: (P1 /\ P2) = {( W-min P), ( E-max P)} and

         A33: (P1 \/ P2) = P and

         A34: (( First_Point (P1,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) > (( Last_Point (P2,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 );

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

        take P1, P2;

        thus thesis by A30, A31, A32, A33, A34;

      end;

    end;

    begin

    theorem :: JORDAN6:34

    

     Th34: for P be Subset of I[01] st P = (the carrier of I[01] \ { 0 , 1}) holds P is open

    proof

      let P be Subset of I[01] ;

      assume

       A1: P = (the carrier of I[01] \ { 0 , 1});

      

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

      

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

      reconsider Q0 = { 0 } as Subset of I[01] by A2, BORSUK_1: 40, ZFMISC_1: 31;

      reconsider Q1 = {1} as Subset of I[01] by A3, BORSUK_1: 40, ZFMISC_1: 31;

      (Q0 \/ Q1) is closed by A2, A3, BORSUK_1: 40, TOPS_1: 9;

      then (( [#] I[01] ) \ (Q0 \/ Q1)) is open;

      hence thesis by A1, ENUMSET1: 1;

    end;

    theorem :: JORDAN6:35

    for P be Subset of R^1 , r,s be Real st P = ].r, s.[ holds P is open

    proof

      let P be Subset of R^1 , r,s be Real;

      assume

       A1: P = ].r, s.[;

      { r1 : r < r1 } c= REAL

      proof

        let x be object;

        assume x in { r1 : r < r1 };

        then

        consider r1 such that

         A2: (r1 = x) & (r < r1);

        r1 in REAL by XREAL_0:def 1;

        hence thesis by A2;

      end;

      then

      reconsider P1 = { r1 where r1 be Real : r < r1 } as Subset of R^1 by TOPMETR: 17;

      { r2 : s > r2 } c= REAL

      proof

        let x be object;

        assume x in { r2 : s > r2 };

        then

        consider r2 such that

         A3: (r2 = x) & (s > r2);

        r2 in REAL by XREAL_0:def 1;

        hence thesis by A3;

      end;

      then

      reconsider P2 = { r2 where r2 be Real : s > r2 } as Subset of R^1 by TOPMETR: 17;

      

       A4: P1 is open by JORDAN2B: 25;

      

       A5: P2 is open by JORDAN2B: 24;

      

       A6: P c= (P1 /\ P2)

      proof

        let x be object;

        assume

         A7: x in P;

        then

        reconsider r1 = x as Real;

        

         A8: r < r1 by A1, A7, XXREAL_1: 4;

        

         A9: r1 < s by A1, A7, XXREAL_1: 4;

        

         A10: x in P1 by A8;

        x in P2 by A9;

        hence thesis by A10, XBOOLE_0:def 4;

      end;

      (P1 /\ P2) c= P

      proof

        let x be object;

        assume

         A11: x in (P1 /\ P2);

        then

         A12: x in P1 by XBOOLE_0:def 4;

        

         A13: x in P2 by A11, XBOOLE_0:def 4;

        

         A14: ex r1 st (r1 = x) & (r < r1) by A12;

        ex r2 st (r2 = x) & (s > r2) by A13;

        hence thesis by A1, A14, XXREAL_1: 4;

      end;

      then P = (P1 /\ P2) by A6;

      hence thesis by A4, A5, TOPS_1: 11;

    end;

    theorem :: JORDAN6:36

    

     Th36: for P7 be Subset of I[01] st P7 = (the carrier of I[01] \ { 0 , 1}) holds P7 <> {} & P7 is connected

    proof

      let P7 be Subset of I[01] ;

      assume

       A1: P7 = (the carrier of I[01] \ { 0 , 1});

      

       A2: (1 / 2) in [. 0 , 1.] by XXREAL_1: 1;

      

       A3: not (1 / 2) in { 0 , 1} by TARSKI:def 2;

      

       A4: ( [#] ( I[01] | P7)) = P7 by PRE_TOPC:def 5;

      for A,B be Subset of ( I[01] | P7) st ( [#] ( I[01] | P7)) = (A \/ B) & A <> ( {} ( I[01] | P7)) & B <> ( {} ( I[01] | P7)) & A is open & B is open holds A meets B

      proof

        let A,B be Subset of ( I[01] | P7);

        assume that

         A5: ( [#] ( I[01] | P7)) = (A \/ B) and

         A6: A <> ( {} ( I[01] | P7)) and

         A7: B <> ( {} ( I[01] | P7)) and

         A8: A is open and

         A9: B is open;

        assume

         A10: A misses B;

        

         A11: ]. 0 , 1.[ misses { 0 , 1} by XXREAL_1: 86;

        

         A12: P7 = (( ]. 0 , 1.[ \/ { 0 , 1}) \ { 0 , 1}) by A1, BORSUK_1: 40, XXREAL_1: 128

        .= ( ]. 0 , 1.[ \ { 0 , 1}) by XBOOLE_1: 40

        .= ]. 0 , 1.[ by A11, XBOOLE_1: 83;

        reconsider D1 = [. 0 , 1.] as Subset of R^1 by TOPMETR: 17;

        reconsider P1 = P7 as Subset of R^1 by A12, TOPMETR: 17;

         I[01] = ( R^1 | D1) by TOPMETR: 19, TOPMETR: 20;

        then

         A13: ( I[01] | P7) = ( R^1 | P1) by BORSUK_1: 40, PRE_TOPC: 7;

        P1 = { r1 : 0 < r1 & r1 < 1 } by A12, RCOMP_1:def 2;

        then P1 is open by JORDAN2B: 26;

        then

         A14: ( I[01] | P7) is non empty open SubSpace of R^1 by A1, A2, A3, A4, A13, BORSUK_1: 40, TSEP_1: 16, XBOOLE_0:def 5;

        reconsider P = A, Q = B as non empty Subset of REAL by A4, A6, A7, A12, XBOOLE_1: 1;

        reconsider A0 = P, B0 = Q as non empty Subset of R^1 by METRIC_1:def 13, TOPMETR: 12, TOPMETR:def 6;

        

         A15: A0 is open by A8, A14, TSEP_1: 17;

        

         A16: B0 is open by A9, A14, TSEP_1: 17;

        set xp = the Element of P;

        reconsider xp as Real;

        

         A17: xp in P;

         0 is LowerBound of P

        proof

          let r be ExtReal;

          assume r in P;

          then r in ]. 0 , 1.[ by A4, A12;

          then r in { w where w be Real : 0 < w & w < 1 } by RCOMP_1:def 2;

          then ex u be Real st u = r & 0 < u & u < 1;

          hence 0 <= r;

        end;

        then

         A18: P is bounded_below;

         0 is LowerBound of Q

        proof

          let r be ExtReal;

          assume r in Q;

          then r in ]. 0 , 1.[ by A4, A12;

          then r in { w where w be Real : 0 < w & w < 1 } by RCOMP_1:def 2;

          then ex u be Real st u = r & 0 < u & u < 1;

          hence 0 <= r;

        end;

        then

         A19: Q is bounded_below;

        reconsider l = ( lower_bound Q) as Element of REAL by XREAL_0:def 1;

        reconsider m = l as Point of RealSpace by METRIC_1:def 13;

        reconsider t = m as Point of R^1 by TOPMETR: 12, TOPMETR:def 6;

        

         A20: not l in Q

        proof

          assume l in Q;

          then

          consider s be Real such that

           A21: s > 0 and

           A22: ( Ball (m,s)) c= B0 by A16, TOPMETR: 15, TOPMETR:def 6;

          reconsider s as Element of REAL by XREAL_0:def 1;

          reconsider s2 = (l - (s / 2)) as Element of REAL by XREAL_0:def 1;

          reconsider e1 = s2 as Point of RealSpace by METRIC_1:def 13;

          (s / 2) < s by A21, XREAL_1: 216;

          then |.(l - (l - (s / 2))).| < s by A21, ABSVALUE:def 1;

          then (the distance of RealSpace . (m,e1)) < s by METRIC_1:def 12, METRIC_1:def 13;

          then ( dist (m,e1)) < s by METRIC_1:def 1;

          then e1 in { z where z be Element of RealSpace : ( dist (m,z)) < s };

          then (l - (s / 2)) in ( Ball (m,s)) by METRIC_1: 17;

          then l <= (l - (s / 2)) by A19, A22, SEQ_4:def 2;

          then (l + (s / 2)) <= l by XREAL_1: 19;

          then ((l + (s / 2)) - l) <= (l - l) by XREAL_1: 9;

          hence contradiction by A21, XREAL_1: 139;

        end;

         A23:

        now

          assume

           A24: l <= 0 ;

           0 < xp by A4, A12, A17, XXREAL_1: 4;

          then

          consider r5 be Real such that

           A25: r5 in Q and

           A26: r5 < (l + (xp - l)) by A19, A24, SEQ_4:def 2;

          reconsider r5 as Real;

          

           A27: { s5 where s5 be Real : s5 in P & r5 < s5 } c= P

          proof

            let y be object;

            assume y in { s5 where s5 be Real : s5 in P & r5 < s5 };

            then ex s5 be Real st s5 = y & s5 in P & r5 < s5;

            hence thesis;

          end;

          then

          reconsider P5 = { s5 where s5 be Real : s5 in P & r5 < s5 } as Subset of REAL by XBOOLE_1: 1;

          set PP5 = { s5 where s5 be Real : s5 in P & r5 < s5 };

          

           A28: xp in P5 by A26;

          

           A29: P5 is bounded_below by A18, A27, XXREAL_2: 44;

          reconsider l5 = ( lower_bound P5) as Element of REAL by XREAL_0:def 1;

          reconsider m5 = l5 as Point of RealSpace by METRIC_1:def 13;

           A30:

          now

            assume

             A31: l5 <= r5;

            now

              assume l5 < r5;

              then (r5 - l5) > 0 by XREAL_1: 50;

              then

              consider r be Real such that

               A32: r in P5 and

               A33: r < (l5 + (r5 - l5)) by A28, A29, SEQ_4:def 2;

              ex s6 be Real st (s6 = r) & (s6 in P) & (r5 < s6) by A32;

              hence contradiction by A33;

            end;

            then l5 = r5 by A31, XXREAL_0: 1;

            then

            consider r7 be Real such that

             A34: r7 > 0 and

             A35: ( Ball (m5,r7)) c= B0 by A16, A25, TOPMETR: 15, TOPMETR:def 6;

            consider r9 be Real such that

             A36: r9 in P5 and

             A37: r9 < (l5 + r7) by A28, A29, A34, SEQ_4:def 2;

            reconsider r9 as Element of REAL by XREAL_0:def 1;

            reconsider e8 = r9 as Point of RealSpace by METRIC_1:def 13;

            l5 <= r9 by A29, A36, SEQ_4:def 2;

            then

             A38: (r9 - l5) >= 0 by XREAL_1: 48;

            (r9 - l5) < ((l5 + r7) - l5) by A37, XREAL_1: 9;

            then |.(r9 - l5).| < r7 by A38, ABSVALUE:def 1;

            then (the distance of RealSpace . (e8,m5)) < r7 by METRIC_1:def 12, METRIC_1:def 13;

            then ( dist (e8,m5)) < r7 by METRIC_1:def 1;

            then e8 in { z where z be Element of RealSpace : ( dist (m5,z)) < r7 };

            then e8 in ( Ball (m5,r7)) by METRIC_1: 17;

            hence contradiction by A10, A27, A35, A36, XBOOLE_0: 3;

          end;

          

           A39: 0 < r5 by A4, A12, A25, XXREAL_1: 4;

          

           A40: (l5 - r5) > 0 by A30, XREAL_1: 50;

          set q = the Element of P5;

          

           A41: q in P5 by A28;

          reconsider q1 = q as Real;

          q1 in P by A27, A41;

          then

           A42: q1 < 1 by A4, A12, XXREAL_1: 4;

          l5 <= q1 by A28, A29, SEQ_4:def 2;

          then l5 < 1 by A42, XXREAL_0: 2;

          then l5 in ]. 0 , 1.[ by A30, A39, XXREAL_1: 4;

          then

           A43: l5 in P or l5 in Q by A4, A5, A12, XBOOLE_0:def 3;

          now

            assume l5 in P;

            then

            consider s5 be Real such that

             A44: s5 > 0 and

             A45: ( Ball (m5,s5)) c= P by A15, TOPMETR: 15, TOPMETR:def 6;

            reconsider s5 as Element of REAL by XREAL_0:def 1;

            set s59 = ( min (s5,(l5 - r5)));

            

             A46: s59 > 0 by A40, A44, XXREAL_0: 21;

            

             A47: s59 <= s5 by XXREAL_0: 17;

            

             A48: (s59 / 2) < s59 by A46, XREAL_1: 216;

            s59 <= (l5 - r5) by XXREAL_0: 17;

            then (s59 / 2) < (l5 - r5) by A48, XXREAL_0: 2;

            then ((s59 / 2) + r5) < ((l5 - r5) + r5) by XREAL_1: 6;

            then

             A49: (((s59 / 2) + r5) - (s59 / 2)) < (l5 - (s59 / 2)) by XREAL_1: 9;

            reconsider e1 = (l5 - (s59 / 2)) as Element of REAL by XREAL_0:def 1;

            reconsider e1 as Point of RealSpace by METRIC_1:def 13;

            (s59 / 2) < s59 by A46, XREAL_1: 216;

            then (s59 / 2) < s5 by A47, XXREAL_0: 2;

            then |.(l5 - (l5 - (s59 / 2))).| < s5 by A46, ABSVALUE:def 1;

            then ( real_dist . (l5,(l5 - (s59 / 2)))) < s5 by METRIC_1:def 12;

            then ( dist (m5,e1)) < s5 by METRIC_1:def 1, METRIC_1:def 13;

            then e1 in { z where z be Element of RealSpace : ( dist (m5,z)) < s5 };

            then (l5 - (s59 / 2)) in ( Ball (m5,s5)) by METRIC_1: 17;

            then

             A50: (l5 - (s59 / 2)) in { s7 where s7 be Real : s7 in P & r5 < s7 } by A45, A49;

            l5 < (l5 + (s59 / 2)) by A46, XREAL_1: 29, XREAL_1: 139;

            then (l5 - (s59 / 2)) < ((l5 + (s59 / 2)) - (s59 / 2)) by XREAL_1: 9;

            hence contradiction by A29, A50, SEQ_4:def 2;

          end;

          then

          consider s1 be Real such that

           A51: s1 > 0 and

           A52: ( Ball (m5,s1)) c= B0 by A16, A43, TOPMETR: 15, TOPMETR:def 6;

          (s1 / 2) > 0 by A51, XREAL_1: 139;

          then

          consider r2 be Real such that

           A53: r2 in P5 and

           A54: r2 < (l5 + (s1 / 2)) by A28, A29, SEQ_4:def 2;

          reconsider r2 as Element of REAL by XREAL_0:def 1;

          

           A55: l5 <= r2 by A29, A53, SEQ_4:def 2;

          reconsider s3 = (r2 - l5) as Element of REAL ;

          reconsider e1 = (l5 + s3) as Point of RealSpace by METRIC_1:def 13;

          

           A56: (r2 - l5) >= 0 by A55, XREAL_1: 48;

          

           A57: (r2 - l5) < ((l5 + (s1 / 2)) - l5) by A54, XREAL_1: 14;

          (s1 / 2) < s1 by A51, XREAL_1: 216;

          then

           A58: ((l5 + s3) - l5) < s1 by A57, XXREAL_0: 2;

           |.((l5 + s3) - l5).| = ((l5 + s3) - l5) by A56, ABSVALUE:def 1;

          then ( real_dist . ((l5 + s3),l5)) < s1 by A58, METRIC_1:def 12;

          then ( dist (e1,m5)) < s1 by METRIC_1:def 1, METRIC_1:def 13;

          then (l5 + s3) in { z where z be Element of RealSpace : ( dist (m5,z)) < s1 };

          then (l5 + s3) in ( Ball (m5,s1)) by METRIC_1: 17;

          then

           A59: (l5 + s3) in (P5 /\ Q) by A52, A53, XBOOLE_0:def 4;

          (P5 /\ Q) c= (P /\ Q) by A27, XBOOLE_1: 26;

          hence contradiction by A10, A59;

        end;

        set q = the Element of Q;

        

         A60: q in Q;

        reconsider q1 = q as Real;

        

         A61: q1 < 1 by A4, A12, A60, XXREAL_1: 4;

        l <= q1 by A19, SEQ_4:def 2;

        then l < 1 by A61, XXREAL_0: 2;

        then l in ]. 0 , 1.[ by A23, XXREAL_1: 4;

        then

         A62: t in A0 by A4, A5, A12, A20, XBOOLE_0:def 3;

        A0 is open by A8, A14, TSEP_1: 17;

        then

        consider s1 be Real such that

         A63: s1 > 0 and

         A64: ( Ball (m,s1)) c= A0 by A62, TOPMETR: 15, TOPMETR:def 6;

        (s1 / 2) > 0 by A63, XREAL_1: 139;

        then

        consider r2 be Real such that

         A65: r2 in Q and

         A66: r2 < (l + (s1 / 2)) by A19, SEQ_4:def 2;

        reconsider r2 as Element of REAL by XREAL_0:def 1;

        

         A67: l <= r2 by A19, A65, SEQ_4:def 2;

        set s3 = (r2 - l);

        reconsider e1 = (l + s3) as Point of RealSpace by METRIC_1:def 13;

        

         A68: (r2 - l) >= 0 by A67, XREAL_1: 48;

        

         A69: (r2 - l) < ((l + (s1 / 2)) - l) by A66, XREAL_1: 14;

        (s1 / 2) < s1 by A63, XREAL_1: 216;

        then

         A70: ((l + s3) - l) < s1 by A69, XXREAL_0: 2;

         |.((l + s3) - l).| = ((l + s3) - l) by A68, ABSVALUE:def 1;

        then ( real_dist . ((l + s3),l)) < s1 by A70, METRIC_1:def 12;

        then ( dist (e1,m)) < s1 by METRIC_1:def 1, METRIC_1:def 13;

        then (l + s3) in { z where z be Element of RealSpace : ( dist (m,z)) < s1 };

        then (l + s3) in ( Ball (m,s1)) by METRIC_1: 17;

        hence contradiction by A10, A64, A65, XBOOLE_0: 3;

      end;

      then ( I[01] | P7) is connected by CONNSP_1: 11;

      hence thesis by A1, A2, A3, BORSUK_1: 40, CONNSP_1:def 3, XBOOLE_0:def 5;

    end;

    theorem :: JORDAN6:37

    

     Th37: for P be Subset of ( TOP-REAL n), p1,p2 be Point of ( TOP-REAL n) st P is_an_arc_of (p1,p2) holds p1 <> p2

    proof

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

      assume P is_an_arc_of (p1,p2);

      then

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

       A1: f is being_homeomorphism and

       A2: (f . 0 ) = p1 and

       A3: (f . 1) = p2 by TOPREAL1:def 1;

      1 in ( [#] I[01] ) by BORSUK_1: 40, XXREAL_1: 1;

      then

       A4: 1 in ( dom f) by A1, TOPS_2:def 5;

      

       A5: f is one-to-one by A1, TOPS_2:def 5;

       0 in ( [#] I[01] ) by BORSUK_1: 40, XXREAL_1: 1;

      then 0 in ( dom f) by A1, TOPS_2:def 5;

      hence thesis by A2, A3, A4, A5, FUNCT_1:def 4;

    end;

    theorem :: JORDAN6:38

    for P be Subset of ( TOP-REAL n), Q be Subset of (( TOP-REAL n) | P), p1,p2 be Point of ( TOP-REAL n) st P is_an_arc_of (p1,p2) & Q = (P \ {p1, p2}) holds Q is open

    proof

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

      assume that

       A1: P is_an_arc_of (p1,p2) and

       A2: Q = (P \ {p1, p2});

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

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

       A3: f is being_homeomorphism and

       A4: (f . 0 ) = p1 and

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

      reconsider f1 = f as Function;

      

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

      reconsider g = (f " ) as Function of (( TOP-REAL n) | P), I[01] ;

      reconsider g1 = g as Function;

      reconsider R = (the carrier of I[01] \ { 0 , 1}) as Subset of I[01] ;

      

       A7: ( [#] I[01] ) <> {} ;

      

       A8: R is open by Th34;

      

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

      

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

      

       A11: g is continuous by A3, TOPS_2:def 5;

      

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

       0 in ( [#] I[01] ) by BORSUK_1: 40, XXREAL_1: 1;

      then

       A13: 0 in ( dom f) by A3, TOPS_2:def 5;

      1 in ( [#] I[01] ) by BORSUK_1: 40, XXREAL_1: 1;

      then

       A14: 1 in ( dom f) by A3, TOPS_2:def 5;

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

      then

       A15: ((f " ) " ) = f by A9, TOPS_2: 51;

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

      then g is onto by FUNCT_2:def 3;

      then

       A16: (g1 " ) = f1 by A10, A15, TOPS_2:def 4;

      (g " R) = ((g1 " the carrier of I[01] ) \ (g1 " { 0 , 1})) by FUNCT_1: 69

      .= (((g1 " ) .: the carrier of I[01] ) \ (g1 " { 0 , 1})) by A10, FUNCT_1: 85

      .= ((f1 .: ( [#] I[01] )) \ (f1 .: { 0 , 1})) by A10, A16, FUNCT_1: 85

      .= (( rng f) \ (f .: { 0 , 1})) by A12, RELAT_1: 113

      .= (( [#] (( TOP-REAL n) | P)) \ (f .: { 0 , 1})) by A3, TOPS_2:def 5

      .= (P \ (f .: { 0 , 1})) by PRE_TOPC:def 5

      .= Q by A2, A4, A5, A13, A14, FUNCT_1: 60;

      hence thesis by A7, A8, A11, TOPS_2: 43;

    end;

    theorem :: JORDAN6:39

    

     Th39: for P,P1,P2 be Subset of ( TOP-REAL n), Q be Subset of (( TOP-REAL n) | P), p1,p2 be Point of ( TOP-REAL n) st P2 is_an_arc_of (p1,p2) & (P1 \/ P2) = P & (P1 /\ P2) = {p1, p2} & Q = (P1 \ {p1, p2}) holds Q is open

    proof

      let P,P1,P2 be Subset of ( TOP-REAL n), Q be Subset of (( TOP-REAL n) | P), p1,p2 be Point of ( TOP-REAL n);

      assume that

       A1: P2 is_an_arc_of (p1,p2) and

       A2: (P1 \/ P2) = P and

       A3: (P1 /\ P2) = {p1, p2} and

       A4: Q = (P1 \ {p1, p2});

      reconsider P21 = P2 as Subset of ( TOP-REAL n);

      

       A5: P21 is compact by A1, JORDAN5A: 1;

      p1 in (P1 /\ P2) by A3, TARSKI:def 2;

      then

       A6: p1 in P2 by XBOOLE_0:def 4;

      

       A7: ( [#] (( TOP-REAL n) | P)) = P by PRE_TOPC:def 5;

      then

      reconsider P29 = P21 as Subset of (( TOP-REAL n) | P) by A2, XBOOLE_1: 7;

      p2 in (P1 /\ P2) by A3, TARSKI:def 2;

      then

       A8: p2 in P2 by XBOOLE_0:def 4;

      P29 is compact by A5, A7, COMPTS_1: 2;

      then

       A9: P29 is closed by COMPTS_1: 7;

      

       A10: (P \ P2) = ((P1 \ P2) \/ (P2 \ P2)) by A2, XBOOLE_1: 42

      .= ((P1 \ P2) \/ {} ) by XBOOLE_1: 37

      .= (P1 \ P2);

      

       A11: (P1 \ P2) c= Q

      proof

        let x be object;

        assume

         A12: x in (P1 \ P2);

        then

         A13: x in P1 by XBOOLE_0:def 5;

         not x in P2 by A12, XBOOLE_0:def 5;

        then not x in {p1, p2} by A6, A8, TARSKI:def 2;

        hence thesis by A4, A13, XBOOLE_0:def 5;

      end;

      Q c= (P1 \ P2)

      proof

        let x be object;

        assume

         A14: x in Q;

        then

         A15: x in P1 by A4, XBOOLE_0:def 5;

         not x in {p1, p2} by A4, A14, XBOOLE_0:def 5;

        then not x in P2 by A3, A15, XBOOLE_0:def 4;

        hence thesis by A15, XBOOLE_0:def 5;

      end;

      then (P1 \ P2) = Q by A11;

      then Q = (P29 ` ) by A7, A10, SUBSET_1:def 4;

      hence thesis by A9, TOPS_1: 3;

    end;

    theorem :: JORDAN6:40

    

     Th40: for P be Subset of ( TOP-REAL n), Q be Subset of (( TOP-REAL n) | P), p1,p2 be Point of ( TOP-REAL n) st P is_an_arc_of (p1,p2) & Q = (P \ {p1, p2}) holds Q is connected

    proof

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

      assume that

       A1: P is_an_arc_of (p1,p2) and

       A2: Q = (P \ {p1, p2});

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

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

       A3: f is being_homeomorphism and

       A4: (f . 0 ) = p1 and

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

      reconsider P7 = (the carrier of I[01] \ { 0 , 1}) as Subset of I[01] ;

      

       A6: f is continuous by A3, TOPS_2:def 5;

      

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

      Q = (f .: P7)

      proof

        ( [#] (( TOP-REAL n) | P)) = P by PRE_TOPC:def 5;

        then

         A8: ( rng f) = P by A3, TOPS_2:def 5;

        thus Q c= (f .: P7)

        proof

          let x be object;

          assume

           A9: x in Q;

          then

           A10: x in P by A2, XBOOLE_0:def 5;

          

           A11: not x in {p1, p2} by A2, A9, XBOOLE_0:def 5;

          consider z be object such that

           A12: z in ( dom f) and

           A13: x = (f . z) by A8, A10, FUNCT_1:def 3;

          now

            assume z in { 0 , 1};

            then x = p1 or x = p2 by A4, A5, A13, TARSKI:def 2;

            hence contradiction by A11, TARSKI:def 2;

          end;

          then z in P7 by A12, XBOOLE_0:def 5;

          hence thesis by A12, A13, FUNCT_1:def 6;

        end;

        let y be object;

        assume y in (f .: P7);

        then

        consider x be object such that

         A14: x in ( dom f) and

         A15: x in P7 and

         A16: y = (f . x) by FUNCT_1:def 6;

        

         A17: not x in { 0 , 1} by A15, XBOOLE_0:def 5;

        then

         A18: x <> 0 by TARSKI:def 2;

        

         A19: x <> 1 by A17, TARSKI:def 2;

        

         A20: y in P by A8, A14, A16, FUNCT_1:def 3;

        now

          assume

           A21: y in {p1, p2};

          reconsider f1 = f as Function of the carrier of I[01] , the carrier of (( TOP-REAL n) | P9);

          now

            per cases by A16, A21, TARSKI:def 2;

              case

               A22: (f . x) = p1;

              ( dom f1) = the carrier of I[01] by FUNCT_2:def 1;

              then 0 in ( dom f1) by BORSUK_1: 40, XXREAL_1: 1;

              hence contradiction by A4, A7, A14, A18, A22, FUNCT_1:def 4;

            end;

              case

               A23: (f . x) = p2;

              ( dom f1) = the carrier of I[01] by FUNCT_2:def 1;

              then 1 in ( dom f1) by BORSUK_1: 40, XXREAL_1: 1;

              hence contradiction by A5, A7, A14, A19, A23, FUNCT_1:def 4;

            end;

          end;

          hence contradiction;

        end;

        hence thesis by A2, A20, XBOOLE_0:def 5;

      end;

      hence thesis by A6, Th36, TOPS_2: 61;

    end;

    theorem :: JORDAN6:41

    

     Th41: for GX be TopSpace, P1,P be Subset of GX, Q9 be Subset of (GX | P1), Q be Subset of (GX | P) st P1 c= P & Q = Q9 & Q9 is connected holds Q is connected

    proof

      let GX be TopSpace, P1,P be Subset of GX, Q9 be Subset of (GX | P1), Q be Subset of (GX | P);

      assume that

       A1: P1 c= P and

       A2: Q = Q9 and

       A3: Q9 is connected;

      ( [#] (GX | P)) = P by PRE_TOPC:def 5;

      then

      reconsider P19 = P1 as Subset of (GX | P) by A1;

      (GX | P1) = ((GX | P) | P19) by A1, PRE_TOPC: 7;

      hence thesis by A2, A3, CONNSP_1: 23;

    end;

    theorem :: JORDAN6:42

    

     Th42: for P be Subset of ( TOP-REAL n), p1,p2 be Point of ( TOP-REAL n) st P is_an_arc_of (p1,p2) holds ex p3 be Point of ( TOP-REAL n) st p3 in P & p3 <> p1 & p3 <> p2

    proof

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

      assume P is_an_arc_of (p1,p2);

      then

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

       A1: f is being_homeomorphism and

       A2: (f . 0 ) = p1 and

       A3: (f . 1) = p2 by TOPREAL1:def 1;

      (1 / 2) in ( [#] I[01] ) by BORSUK_1: 40, XXREAL_1: 1;

      then

       A4: (1 / 2) in ( dom f) by A1, TOPS_2:def 5;

      then (f . (1 / 2)) in ( rng f) by FUNCT_1:def 3;

      then (f . (1 / 2)) in the carrier of (( TOP-REAL n) | P);

      then

       A5: (f . (1 / 2)) in P by PRE_TOPC: 8;

      then

      reconsider p = (f . (1 / 2)) as Point of ( TOP-REAL n);

      

       A6: f is one-to-one by A1, TOPS_2:def 5;

       0 in ( [#] I[01] ) by BORSUK_1: 40, XXREAL_1: 1;

      then 0 in ( dom f) by A1, TOPS_2:def 5;

      then

       A7: p1 <> p by A2, A4, A6, FUNCT_1:def 4;

      1 in ( [#] I[01] ) by BORSUK_1: 40, XXREAL_1: 1;

      then 1 in ( dom f) by A1, TOPS_2:def 5;

      then (f . 1) <> (f . (1 / 2)) by A4, A6, FUNCT_1:def 4;

      hence thesis by A3, A5, A7;

    end;

    theorem :: JORDAN6:43

    for P be Subset of ( TOP-REAL n), p1,p2 be Point of ( TOP-REAL n) st P is_an_arc_of (p1,p2) holds (P \ {p1, p2}) <> {}

    proof

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

      assume P is_an_arc_of (p1,p2);

      then

      consider p3 be Point of ( TOP-REAL n) such that

       A1: p3 in P and

       A2: p3 <> p1 and

       A3: p3 <> p2 by Th42;

       not p3 in {p1, p2} by A2, A3, TARSKI:def 2;

      hence thesis by A1, XBOOLE_0:def 5;

    end;

    theorem :: JORDAN6:44

    for P1 be Subset of ( TOP-REAL n), P be Subset of ( TOP-REAL n), Q be Subset of (( TOP-REAL n) | P), p1,p2 be Point of ( TOP-REAL n) st P1 is_an_arc_of (p1,p2) & P1 c= P & Q = (P1 \ {p1, p2}) holds Q is connected

    proof

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

      assume that

       A1: P1 is_an_arc_of (p1,p2) and

       A2: P1 c= P and

       A3: Q = (P1 \ {p1, p2});

      ( [#] (( TOP-REAL n) | P1)) = P1 by PRE_TOPC:def 5;

      then

      reconsider Q9 = Q as Subset of (( TOP-REAL n) | P1) by A3, XBOOLE_1: 36;

      Q9 is connected by A1, A3, Th40;

      hence thesis by A2, Th41;

    end;

    theorem :: JORDAN6:45

    

     Th45: for T,S,V be non empty TopSpace, P1 be non empty Subset of S, P2 be Subset of S, f be Function of T, (S | P1), g be Function of (S | P2), V st P1 c= P2 & f is continuous & g is continuous holds ex h be Function of T, V st h = (g * f) & h is continuous

    proof

      let T,S,V be non empty TopSpace, P1 be non empty Subset of S, P2 be Subset of S, f be Function of T, (S | P1), g be Function of (S | P2), V;

      assume that

       A1: P1 c= P2 and

       A2: f is continuous and

       A3: g is continuous;

      reconsider P3 = P2 as non empty Subset of S by A1, XBOOLE_1: 3;

      

       A4: ( [#] (S | P1)) = P1 by PRE_TOPC:def 5;

      

       A5: ( [#] (S | P2)) = P2 by PRE_TOPC:def 5;

      then

      reconsider f1 = f as Function of T, (S | P3) by A1, A4, FUNCT_2: 7;

      for F1 be Subset of (S | P2) st F1 is closed holds (f1 " F1) is closed

      proof

        let F1 be Subset of (S | P2);

        assume

         A6: F1 is closed;

        reconsider P19 = P1 as non empty Subset of (S | P3) by A1, A5;

        

         A7: ( [#] (S | P1)) = P1 by PRE_TOPC:def 5;

        reconsider P4 = (F1 /\ P19) as Subset of ((S | P3) | P19) by TOPS_2: 29;

        

         A8: (S | P1) = ((S | P3) | P19) by A1, PRE_TOPC: 7;

        

         A9: P4 is closed by A6, Th2;

        (f1 " P1) = the carrier of T by A7, FUNCT_2: 40

        .= ( dom f1) by FUNCT_2:def 1;

        

        then (f1 " F1) = ((f1 " F1) /\ (f1 " P1)) by RELAT_1: 132, XBOOLE_1: 28

        .= (f " P4) by FUNCT_1: 68;

        hence thesis by A2, A8, A9;

      end;

      then f1 is continuous;

      hence thesis by A3;

    end;

    theorem :: JORDAN6:46

    

     Th46: for P1,P2 be Subset of ( TOP-REAL n), p1,p2 be Point of ( TOP-REAL n) st P1 is_an_arc_of (p1,p2) & P2 is_an_arc_of (p1,p2) & P1 c= P2 holds P1 = P2

    proof

      let P1,P2 be Subset of ( TOP-REAL n), p1,p2 be Point of ( TOP-REAL n);

      assume that

       A1: P1 is_an_arc_of (p1,p2) and

       A2: P2 is_an_arc_of (p1,p2) and

       A3: P1 c= P2;

      reconsider P19 = P1, P29 = P2 as non empty Subset of ( TOP-REAL n) by A1, A2, TOPREAL1: 1;

      now

        assume

         A4: (P2 \ P1) <> {} ;

        set p = the Element of (P2 \ P1);

        

         A5: p in P2 by A4, XBOOLE_0:def 5;

        

         A6: not p in P1 by A4, XBOOLE_0:def 5;

        consider f1 be Function of I[01] , (( TOP-REAL n) | P19) such that

         A7: f1 is being_homeomorphism and

         A8: (f1 . 0 ) = p1 and

         A9: (f1 . 1) = p2 by A1, TOPREAL1:def 1;

        

         A10: f1 is continuous by A7, TOPS_2:def 5;

        consider f2 be Function of I[01] , (( TOP-REAL n) | P29) such that

         A11: f2 is being_homeomorphism and

         A12: (f2 . 0 ) = p1 and

         A13: (f2 . 1) = p2 by A2, TOPREAL1:def 1;

        reconsider f4 = f2 as Function;

        

         A14: f2 is one-to-one by A11, TOPS_2:def 5;

        

         A15: ( rng f2) = ( [#] (( TOP-REAL n) | P2)) by A11, TOPS_2:def 5;

        

         A16: (f2 " ) is being_homeomorphism by A11, TOPS_2: 56;

        

        then

         A17: ( dom (f2 " )) = ( [#] (( TOP-REAL n) | P2)) by TOPS_2:def 5

        .= P2 by PRE_TOPC:def 5;

        (f2 " ) is continuous by A11, TOPS_2:def 5;

        then

        consider h be Function of I[01] , I[01] such that

         A18: h = ((f2 " ) * f1) and

         A19: h is continuous by A3, A10, Th45;

        reconsider h1 = h as Function of ( Closed-Interval-TSpace ( 0 ,1)), R^1 by BORSUK_1: 40, FUNCT_2: 7, TOPMETR: 17, TOPMETR: 20;

        for F1 be Subset of R^1 st F1 is closed holds (h1 " F1) is closed

        proof

          let F1 be Subset of R^1 ;

          assume

           A20: F1 is closed;

          reconsider K = the carrier of I[01] as Subset of R^1 by BORSUK_1: 40, TOPMETR: 17;

          

           A21: I[01] = ( R^1 | K) by BORSUK_1: 40, TOPMETR: 19, TOPMETR: 20;

          reconsider P3 = (F1 /\ K) as Subset of ( R^1 | K) by TOPS_2: 29;

          

           A22: P3 is closed by A20, Th2;

          (h1 " K) = the carrier of I[01] by FUNCT_2: 40

          .= ( dom h1) by FUNCT_2:def 1;

          

          then (h1 " F1) = ((h1 " F1) /\ (h1 " K)) by RELAT_1: 132, XBOOLE_1: 28

          .= (h " P3) by FUNCT_1: 68;

          hence thesis by A19, A21, A22, TOPMETR: 20;

        end;

        then

        reconsider g = h1 as continuous Function of ( Closed-Interval-TSpace ( 0 ,1)), R^1 by PRE_TOPC:def 6;

        

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

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

        then

         A24: 0 in ( dom f1) by XXREAL_1: 1;

        

         A25: 1 in ( dom f1) by A23, XXREAL_1: 1;

        

         A26: (g . 0 ) = ((f2 " ) . p1) by A8, A18, A24, FUNCT_1: 13;

        

         A27: (g . 1) = ((f2 " ) . p2) by A9, A18, A25, FUNCT_1: 13;

        

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

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

        then

         A29: 0 in ( dom f2) by XXREAL_1: 1;

        

         A30: 1 in ( dom f2) by A28, XXREAL_1: 1;

        

         A31: f2 is onto by A15, FUNCT_2:def 3;

        then

         A32: ((f2 " ) . p1) = ((f4 " ) . p1) by A14, TOPS_2:def 4;

        

         A33: ((f2 " ) . p2) = ((f4 " ) . p2) by A14, A31, TOPS_2:def 4;

        

         A34: (g . 0 ) = 0 by A12, A14, A26, A29, A32, FUNCT_1: 32;

        

         A35: (g . 1) = 1 by A13, A14, A27, A30, A33, FUNCT_1: 32;

        p in the carrier of (( TOP-REAL n) | P29) by A5, PRE_TOPC: 8;

        then

         A36: ((f2 " ) . p) in the carrier of I[01] by FUNCT_2: 5;

         A37:

        now

          assume ((f2 " ) . p) in ( rng g);

          then

          consider x be object such that

           A38: x in ( dom g) and

           A39: ((f2 " ) . p) = (g . x) by FUNCT_1:def 3;

          

           A40: ((f2 " ) . p) = ((f2 " ) . (f1 . x)) by A18, A38, A39, FUNCT_1: 12;

          

           A41: x in ( dom f1) by A18, A38, FUNCT_1: 11;

          

           A42: (f1 . x) in ( dom (f2 " )) by A18, A38, FUNCT_1: 11;

          (f2 " ) is one-to-one by A16, TOPS_2:def 5;

          then p = (f1 . x) by A5, A17, A40, A42, FUNCT_1:def 4;

          then

           A43: p in ( rng f1) by A41, FUNCT_1:def 3;

          ( rng f1) = ( [#] (( TOP-REAL n) | P1)) by A7, TOPS_2:def 5

          .= P1 by PRE_TOPC:def 5;

          hence contradiction by A4, A43, XBOOLE_0:def 5;

        end;

        reconsider r = ((f2 " ) . p) as Real;

        

         A44: ( rng f2) = ( [#] (( TOP-REAL n) | P2)) by A11, TOPS_2:def 5

        .= P2 by PRE_TOPC:def 5;

        

         A45: r <= 1 by A36, BORSUK_1: 40, XXREAL_1: 1;

         A46:

        now

          assume

           A47: r = 0 ;

          (f2 . r) = (f4 . ((f4 " ) . p)) by A31, A14, TOPS_2:def 4

          .= p by A5, A14, A44, FUNCT_1: 35;

          hence contradiction by A1, A6, A12, A47, TOPREAL1: 1;

        end;

         A48:

        now

          assume

           A49: r = 1;

          (f2 . r) = (f4 . ((f4 " ) . p)) by A31, A14, TOPS_2:def 4

          .= p by A5, A14, A44, FUNCT_1: 35;

          hence contradiction by A1, A6, A13, A49, TOPREAL1: 1;

        end;

        

         A50: 0 < r by A36, A46, BORSUK_1: 40, XXREAL_1: 1;

        r < 1 by A45, A48, XXREAL_0: 1;

        then

        consider rc be Real such that

         A51: (g . rc) = r and

         A52: 0 < rc and

         A53: rc < 1 by A34, A35, A50, TOPREAL5: 6;

        the carrier of (( TOP-REAL n) | P1) = ( [#] (( TOP-REAL n) | P1))

        .= P1 by PRE_TOPC:def 5;

        then ( rng f1) c= ( dom (f2 " )) by A3, A17;

        

        then ( dom g) = ( dom f1) by A18, RELAT_1: 27

        .= ( [#] I[01] ) by A7, TOPS_2:def 5

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

        then rc in ( dom g) by A52, A53, XXREAL_1: 1;

        hence contradiction by A37, A51, FUNCT_1:def 3;

      end;

      then P2 c= P1 by XBOOLE_1: 37;

      hence thesis by A3;

    end;

    theorem :: JORDAN6:47

    

     Th47: for P be Subset of ( TOP-REAL 2), Q be Subset of (( TOP-REAL 2) | P), p1,p2 be Point of ( TOP-REAL 2) st P is being_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = (P \ {p1, p2}) holds not Q is connected

    proof

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

      assume that

       A1: P is being_simple_closed_curve and

       A2: p1 in P and

       A3: p2 in P and

       A4: p1 <> p2 and

       A5: Q = (P \ {p1, p2});

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

       A6: P1 is_an_arc_of (p1,p2) and

       A7: P2 is_an_arc_of (p1,p2) and

       A8: P = (P1 \/ P2) and

       A9: (P1 /\ P2) = {p1, p2} by A1, A2, A3, A4, TOPREAL2: 5;

      

       A10: ( [#] (( TOP-REAL 2) | P)) = P by PRE_TOPC:def 5;

      reconsider P as Simple_closed_curve by A1;

      

       A11: P1 c= P by A8, XBOOLE_1: 7;

      (P1 \ {p1, p2}) c= P1 by XBOOLE_1: 36;

      then

      reconsider P19 = (P1 \ {p1, p2}) as Subset of (( TOP-REAL 2) | P) by A10, A11, XBOOLE_1: 1;

      

       A12: P2 c= P by A8, XBOOLE_1: 7;

      (P2 \ {p1, p2}) c= P2 by XBOOLE_1: 36;

      then

      reconsider P29 = (P2 \ {p1, p2}) as Subset of (( TOP-REAL 2) | P) by A10, A12, XBOOLE_1: 1;

      

       A13: P19 is open by A7, A8, A9, Th39;

      

       A14: P29 is open by A6, A8, A9, Th39;

      

       A15: Q c= (P19 \/ P29)

      proof

        let x be object;

        assume

         A16: x in Q;

        then

         A17: x in P by A5, XBOOLE_0:def 5;

        now

          per cases by A5, A8, A16, A17, XBOOLE_0:def 3, XBOOLE_0:def 5;

            case x in P1 & not x in {p1, p2};

            then x in P19 by XBOOLE_0:def 5;

            hence thesis by XBOOLE_0:def 3;

          end;

            case x in P2 & not x in {p1, p2};

            then x in P29 by XBOOLE_0:def 5;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        hence thesis;

      end;

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

       A18: p3 in P1 and

       A19: p3 <> p1 and

       A20: p3 <> p2 by A6, Th42;

       not p3 in {p1, p2} by A19, A20, TARSKI:def 2;

      then

       A21: P19 <> {} by A18, XBOOLE_0:def 5;

      P19 c= Q

      proof

        let x be object;

        assume

         A22: x in P19;

        then

         A23: x in P1 by XBOOLE_0:def 5;

        

         A24: not x in {p1, p2} by A22, XBOOLE_0:def 5;

        x in P by A8, A23, XBOOLE_0:def 3;

        hence thesis by A5, A24, XBOOLE_0:def 5;

      end;

      then (P19 /\ Q) <> {} by A21, XBOOLE_1: 28;

      then

       A25: P19 meets Q;

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

       A26: p39 in P2 and

       A27: p39 <> p1 and

       A28: p39 <> p2 by A7, Th42;

       not p39 in {p1, p2} by A27, A28, TARSKI:def 2;

      then

       A29: P29 <> {} by A26, XBOOLE_0:def 5;

      P29 c= Q

      proof

        let x be object;

        assume

         A30: x in P29;

        then

         A31: x in P2 by XBOOLE_0:def 5;

        

         A32: not x in {p1, p2} by A30, XBOOLE_0:def 5;

        x in (P1 \/ P2) by A31, XBOOLE_0:def 3;

        hence thesis by A5, A8, A32, XBOOLE_0:def 5;

      end;

      then (P29 /\ Q) <> {} by A29, XBOOLE_1: 28;

      then

       A33: P29 meets Q;

      now

        assume P19 meets P29;

        then

        consider p0 be object such that

         A34: p0 in P19 and

         A35: p0 in P29 by XBOOLE_0: 3;

        

         A36: p0 in P1 by A34, XBOOLE_0:def 5;

        

         A37: not p0 in {p1, p2} by A34, XBOOLE_0:def 5;

        p0 in P2 by A35, XBOOLE_0:def 5;

        hence contradiction by A9, A36, A37, XBOOLE_0:def 4;

      end;

      hence thesis by A13, A14, A15, A25, A33, TOPREAL5: 1;

    end;

    theorem :: JORDAN6:48

    

     Th48: for P,P1,P2,P19,P29 be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2) st P is being_simple_closed_curve & P1 is_an_arc_of (p1,p2) & P2 is_an_arc_of (p1,p2) & (P1 \/ P2) = P & P19 is_an_arc_of (p1,p2) & P29 is_an_arc_of (p1,p2) & (P19 \/ P29) = P holds P1 = P19 & P2 = P29 or P1 = P29 & P2 = P19

    proof

      let P,P1,P2,P19,P29 be Subset of the carrier of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2);

      assume that

       A1: P is being_simple_closed_curve and

       A2: P1 is_an_arc_of (p1,p2) and

       A3: P2 is_an_arc_of (p1,p2) and

       A4: (P1 \/ P2) = P and

       A5: P19 is_an_arc_of (p1,p2) and

       A6: P29 is_an_arc_of (p1,p2) and

       A7: (P19 \/ P29) = P;

      reconsider P as Simple_closed_curve by A1;

      

       A8: p1 <> p2 by A6, Th37;

      

       A9: p1 in P19 by A5, TOPREAL1: 1;

      

       A10: p2 in P19 by A5, TOPREAL1: 1;

      

       A11: p1 in P2 by A3, TOPREAL1: 1;

      

       A12: p2 in P2 by A3, TOPREAL1: 1;

      

       A13: p1 in P1 by A2, TOPREAL1: 1;

      

       A14: p2 in P1 by A2, TOPREAL1: 1;

      

       A15: P1 c= P by A4, XBOOLE_1: 7;

      

       A16: ( [#] (( TOP-REAL 2) | P)) = P by PRE_TOPC:def 5;

      (P1 \ {p1, p2}) c= P1 by XBOOLE_1: 36;

      then

      reconsider Q1 = (P1 \ {p1, p2}) as Subset of (( TOP-REAL 2) | P) by A15, A16, XBOOLE_1: 1;

      

       A17: P2 c= P by A4, XBOOLE_1: 7;

      (P2 \ {p1, p2}) c= P2 by XBOOLE_1: 36;

      then

      reconsider Q2 = (P2 \ {p1, p2}) as Subset of (( TOP-REAL 2) | P) by A16, A17, XBOOLE_1: 1;

      

       A18: P19 c= P by A7, XBOOLE_1: 7;

      (P19 \ {p1, p2}) c= P19 by XBOOLE_1: 36;

      then

      reconsider Q19 = (P19 \ {p1, p2}) as Subset of (( TOP-REAL 2) | P) by A16, A18, XBOOLE_1: 1;

      

       A19: P29 c= P by A7, XBOOLE_1: 7;

      (P29 \ {p1, p2}) c= P29 by XBOOLE_1: 36;

      then

      reconsider Q29 = (P29 \ {p1, p2}) as Subset of (( TOP-REAL 2) | P) by A16, A19, XBOOLE_1: 1;

      

       A20: (Q1 \/ Q2) = (P \ {p1, p2}) by A4, XBOOLE_1: 42;

      

       A21: (Q19 \/ Q29) = (P \ {p1, p2}) by A7, XBOOLE_1: 42;

      then

       A22: (Q19 \/ (Q1 \/ Q2)) = (Q1 \/ Q2) by A20, XBOOLE_1: 7, XBOOLE_1: 12;

      

       A23: (Q29 \/ (Q1 \/ Q2)) = (Q1 \/ Q2) by A20, A21, XBOOLE_1: 7, XBOOLE_1: 12;

      

       A24: (Q1 \/ (Q19 \/ Q29)) = (Q19 \/ Q29) by A20, A21, XBOOLE_1: 7, XBOOLE_1: 12;

      

       A25: (Q2 \/ (Q19 \/ Q29)) = (Q19 \/ Q29) by A20, A21, XBOOLE_1: 7, XBOOLE_1: 12;

      ( [#] (( TOP-REAL 2) | P1)) = P1 by PRE_TOPC:def 5;

      then

      reconsider R1 = Q1 as Subset of (( TOP-REAL 2) | P1) by XBOOLE_1: 36;

      R1 is connected by A2, Th40;

      then

       A26: Q1 is connected by A4, Th41, XBOOLE_1: 7;

      ( [#] (( TOP-REAL 2) | P2)) = P2 by PRE_TOPC:def 5;

      then

      reconsider R2 = Q2 as Subset of (( TOP-REAL 2) | P2) by XBOOLE_1: 36;

      R2 is connected by A3, Th40;

      then

       A27: Q2 is connected by A4, Th41, XBOOLE_1: 7;

      ( [#] (( TOP-REAL 2) | P19)) = P19 by PRE_TOPC:def 5;

      then

      reconsider R19 = Q19 as Subset of (( TOP-REAL 2) | P19) by XBOOLE_1: 36;

      R19 is connected by A5, Th40;

      then

       A28: Q19 is connected by A7, Th41, XBOOLE_1: 7;

      ( [#] (( TOP-REAL 2) | P29)) = P29 by PRE_TOPC:def 5;

      then

      reconsider R29 = Q29 as Subset of (( TOP-REAL 2) | P29) by XBOOLE_1: 36;

      R29 is connected by A6, Th40;

      then

       A29: Q29 is connected by A7, Th41, XBOOLE_1: 7;

      

       A30: {p1, p2} c= P1 by A13, A14, TARSKI:def 2;

      

       A31: {p1, p2} c= P2 by A11, A12, TARSKI:def 2;

      

       A32: {p1, p2} c= P19 by A9, A10, TARSKI:def 2;

      

       A33: {p1, p2} c= P29

      proof

        let x be object;

        assume x in {p1, p2};

        then x = p1 or x = p2 by TARSKI:def 2;

        hence thesis by A6, TOPREAL1: 1;

      end;

      

       A34: (Q1 \/ {p1, p2}) = P1 by A30, XBOOLE_1: 45;

      

       A35: (Q2 \/ {p1, p2}) = P2 by A31, XBOOLE_1: 45;

      

       A36: (Q19 \/ {p1, p2}) = P19 by A32, XBOOLE_1: 45;

      

       A37: (Q29 \/ {p1, p2}) = P29 by A33, XBOOLE_1: 45;

      now

        assume

         A38: not (P1 = P29 & P2 = P19);

        now

          per cases by A38;

            case

             A39: P1 <> P29;

             A40:

            now

              assume that

               A41: (Q1 \ Q29) = {} and

               A42: (Q29 \ Q1) = {} ;

              

               A43: Q1 c= Q29 by A41, XBOOLE_1: 37;

              Q29 c= Q1 by A42, XBOOLE_1: 37;

              hence contradiction by A34, A37, A39, A43, XBOOLE_0:def 10;

            end;

            now

              per cases by A40;

                case

                 A44: (Q1 \ Q29) <> {} ;

                set y = the Element of (Q1 \ Q29);

                

                 A45: y in Q1 by A44, XBOOLE_0:def 5;

                then

                 A46: y in (Q19 \/ Q29) by A20, A21, XBOOLE_0:def 3;

                 not y in Q29 by A44, XBOOLE_0:def 5;

                then y in Q19 by A46, XBOOLE_0:def 3;

                then (Q1 /\ Q19) <> {} by A45, XBOOLE_0:def 4;

                then

                 A47: Q1 meets Q19;

                now

                  assume Q2 meets Q19;

                  then ((Q1 \/ Q19) \/ Q2) is connected by A26, A27, A28, A47, JORDAN1: 4;

                  hence contradiction by A8, A13, A14, A15, A20, A22, Th47, XBOOLE_1: 4;

                end;

                then

                 A48: (Q2 /\ Q19) = {} ;

                

                 A49: Q2 c= Q29

                proof

                  let x be object;

                  assume

                   A50: x in Q2;

                  then x in (Q1 \/ Q2) by XBOOLE_0:def 3;

                  then x in Q19 or x in Q29 by A20, A21, XBOOLE_0:def 3;

                  hence thesis by A48, A50, XBOOLE_0:def 4;

                end;

                Q19 c= Q1

                proof

                  let x be object;

                  assume

                   A51: x in Q19;

                  then x in (Q1 \/ Q2) by A20, A21, XBOOLE_0:def 3;

                  then x in Q1 or x in Q2 by XBOOLE_0:def 3;

                  hence thesis by A48, A51, XBOOLE_0:def 4;

                end;

                hence thesis by A2, A3, A5, A6, A34, A35, A36, A37, A49, Th46, XBOOLE_1: 9;

              end;

                case

                 A52: (Q29 \ Q1) <> {} ;

                set y = the Element of (Q29 \ Q1);

                

                 A53: y in Q29 by A52, XBOOLE_0:def 5;

                then

                 A54: y in (Q2 \/ Q1) by A20, A21, XBOOLE_0:def 3;

                 not y in Q1 by A52, XBOOLE_0:def 5;

                then y in Q2 by A54, XBOOLE_0:def 3;

                then (Q29 /\ Q2) <> {} by A53, XBOOLE_0:def 4;

                then

                 A55: Q29 meets Q2;

                now

                  assume Q19 meets Q2;

                  then ((Q29 \/ Q2) \/ Q19) is connected by A27, A28, A29, A55, JORDAN1: 4;

                  hence contradiction by A8, A13, A14, A15, A21, A25, Th47, XBOOLE_1: 4;

                end;

                then

                 A56: (Q19 /\ Q2) = {} ;

                

                 A57: Q19 c= Q1

                proof

                  let x be object;

                  assume

                   A58: x in Q19;

                  then x in (Q19 \/ Q29) by XBOOLE_0:def 3;

                  then x in Q1 or x in Q2 by A20, A21, XBOOLE_0:def 3;

                  hence thesis by A56, A58, XBOOLE_0:def 4;

                end;

                Q2 c= Q29

                proof

                  let x be object;

                  assume

                   A59: x in Q2;

                  then x in (Q2 \/ Q1) by XBOOLE_0:def 3;

                  then x in Q29 or x in Q19 by A20, A21, XBOOLE_0:def 3;

                  hence thesis by A56, A59, XBOOLE_0:def 4;

                end;

                hence thesis by A2, A3, A5, A6, A34, A35, A36, A37, A57, Th46, XBOOLE_1: 9;

              end;

            end;

            hence thesis;

          end;

            case

             A60: P2 <> P19;

             A61:

            now

              assume that

               A62: (Q2 \ Q19) = {} and

               A63: (Q19 \ Q2) = {} ;

              

               A64: Q2 c= Q19 by A62, XBOOLE_1: 37;

              Q19 c= Q2 by A63, XBOOLE_1: 37;

              hence contradiction by A35, A36, A60, A64, XBOOLE_0:def 10;

            end;

            now

              per cases by A61;

                case

                 A65: (Q2 \ Q19) <> {} ;

                set y = the Element of (Q2 \ Q19);

                

                 A66: y in Q2 by A65, XBOOLE_0:def 5;

                then

                 A67: y in (Q29 \/ Q19) by A20, A21, XBOOLE_0:def 3;

                 not y in Q19 by A65, XBOOLE_0:def 5;

                then y in Q29 by A67, XBOOLE_0:def 3;

                then (Q2 /\ Q29) <> {} by A66, XBOOLE_0:def 4;

                then

                 A68: Q2 meets Q29;

                now

                  assume Q1 meets Q29;

                  then ((Q2 \/ Q29) \/ Q1) is connected by A26, A27, A29, A68, JORDAN1: 4;

                  hence contradiction by A8, A13, A14, A15, A20, A23, Th47, XBOOLE_1: 4;

                end;

                then

                 A69: (Q1 /\ Q29) = {} ;

                

                 A70: Q1 c= Q19

                proof

                  let x be object;

                  assume

                   A71: x in Q1;

                  then x in (Q2 \/ Q1) by XBOOLE_0:def 3;

                  then x in Q29 or x in Q19 by A20, A21, XBOOLE_0:def 3;

                  hence thesis by A69, A71, XBOOLE_0:def 4;

                end;

                Q29 c= Q2

                proof

                  let x be object;

                  assume

                   A72: x in Q29;

                  then x in (Q2 \/ Q1) by A20, A21, XBOOLE_0:def 3;

                  then x in Q2 or x in Q1 by XBOOLE_0:def 3;

                  hence thesis by A69, A72, XBOOLE_0:def 4;

                end;

                hence thesis by A2, A3, A5, A6, A34, A35, A36, A37, A70, Th46, XBOOLE_1: 9;

              end;

                case

                 A73: (Q19 \ Q2) <> {} ;

                set y = the Element of (Q19 \ Q2);

                

                 A74: y in Q19 by A73, XBOOLE_0:def 5;

                then

                 A75: y in (Q1 \/ Q2) by A20, A21, XBOOLE_0:def 3;

                 not y in Q2 by A73, XBOOLE_0:def 5;

                then y in Q1 by A75, XBOOLE_0:def 3;

                then (Q19 /\ Q1) <> {} by A74, XBOOLE_0:def 4;

                then

                 A76: Q19 meets Q1;

                now

                  assume Q29 meets Q1;

                  then ((Q19 \/ Q1) \/ Q29) is connected by A26, A28, A29, A76, JORDAN1: 4;

                  hence contradiction by A8, A13, A14, A15, A21, A24, Th47, XBOOLE_1: 4;

                end;

                then

                 A77: (Q29 /\ Q1) = {} ;

                

                 A78: Q29 c= Q2

                proof

                  let x be object;

                  assume

                   A79: x in Q29;

                  then x in (Q29 \/ Q19) by XBOOLE_0:def 3;

                  then x in Q2 or x in Q1 by A20, A21, XBOOLE_0:def 3;

                  hence thesis by A77, A79, XBOOLE_0:def 4;

                end;

                Q1 c= Q19

                proof

                  let x be object;

                  assume

                   A80: x in Q1;

                  then x in (Q19 \/ Q29) by A20, A21, XBOOLE_0:def 3;

                  then x in Q19 or x in Q29 by XBOOLE_0:def 3;

                  hence thesis by A77, A80, XBOOLE_0:def 4;

                end;

                hence thesis by A2, A3, A5, A6, A34, A35, A36, A37, A78, Th46, XBOOLE_1: 9;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    begin

    

     Lm1: for g be Function of I[01] , R^1 , s1,s2,r be Real st g is continuous & (g . 0[01] ) < r & r < (g . 1[01] ) holds ex r1 st 0 < r1 & r1 < 1 & (g . r1) = r

    proof

      let g be Function of I[01] , R^1 , s1,s2,r be Real;

      assume that

       A1: g is continuous and

       A2: (g . 0[01] ) < r and

       A3: r < (g . 1[01] );

      ex rc be Real st (g . rc) = r & 0 < rc & rc < 1 by A1, A2, A3, BORSUK_1:def 14, BORSUK_1:def 15, TOPMETR: 20, TOPREAL5: 6;

      hence thesis;

    end;

    theorem :: JORDAN6:49

    

     Th49: for P1 be Subset of ( TOP-REAL 2), r be Real, p1,p2 be Point of ( TOP-REAL 2) st (p1 `1 ) <= r & r <= (p2 `1 ) & P1 is_an_arc_of (p1,p2) holds P1 meets ( Vertical_Line r) & (P1 /\ ( Vertical_Line r)) is closed

    proof

      let P1 be Subset of ( TOP-REAL 2), r be Real, p1,p2 be Point of ( TOP-REAL 2);

      assume that

       A1: (p1 `1 ) <= r and

       A2: r <= (p2 `1 ) and

       A3: P1 is_an_arc_of (p1,p2);

      reconsider P19 = P1 as non empty Subset of ( TOP-REAL 2) by A3, TOPREAL1: 1;

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

       A4: f is being_homeomorphism and

       A5: (f . 0 ) = p1 and

       A6: (f . 1) = p2 by A3, TOPREAL1:def 1;

      

       A7: ( [#] (( TOP-REAL 2) | P1)) = P1 by PRE_TOPC:def 5;

      then

      reconsider f1 = f as Function of the carrier of I[01] , the carrier of ( TOP-REAL 2) by FUNCT_2: 7;

      reconsider f2 = f1 as Function of I[01] , ( TOP-REAL 2);

      reconsider proj11 = proj1 as Function of the carrier of ( TOP-REAL 2), REAL ;

      reconsider proj12 = proj1 as Function of ( TOP-REAL 2), R^1 by TOPMETR: 17;

      reconsider g1 = (proj11 * f1) as Function of the carrier of I[01] , REAL ;

      reconsider g = g1 as Function of I[01] , R^1 by TOPMETR: 17;

      f is continuous by A4, TOPS_2:def 5;

      then

       A8: f2 is continuous by Th3;

      

       A9: proj12 is continuous by TOPREAL5: 10;

      

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

      then

       A11: 0 in ( dom f) by XXREAL_1: 1;

      

       A12: 1 in ( dom f) by A10, XXREAL_1: 1;

      

       A13: (g . 0 ) = ( proj1 . p1) by A5, A11, FUNCT_1: 13

      .= (p1 `1 ) by PSCOMP_1:def 5;

      

       A14: (g . 1) = ( proj1 . p2) by A6, A12, FUNCT_1: 13

      .= (p2 `1 ) by PSCOMP_1:def 5;

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

      

       A15: P19 is closed by A3, COMPTS_1: 7, JORDAN5A: 1;

      

       A16: ( Vertical_Line r) is closed by Th6;

      now

        per cases by A1, A2, A13, A14, BORSUK_1:def 14, BORSUK_1:def 15, XXREAL_0: 1;

          case (g . 0 ) = (g . 1);

          then

           A17: (g . 0 ) = r by A1, A2, A13, A14, XXREAL_0: 1;

          

           A18: (f . 0 ) in ( rng f) by A11, FUNCT_1:def 3;

          then (f . 0 ) in P1 by A7;

          then

          reconsider p = (f . 0 ) as Point of ( TOP-REAL 2);

          (p `1 ) = ( proj1 . (f . 0 )) by PSCOMP_1:def 5

          .= r by A11, A17, FUNCT_1: 13;

          then (f . 0 ) in { q where q be Point of ( TOP-REAL 2) : (q `1 ) = r };

          hence P1 meets ( Vertical_Line r) by A7, A18, XBOOLE_0: 3;

        end;

          case

           A19: (g . 0[01] ) = r;

          

           A20: (f . 0 ) in ( rng f) by A11, FUNCT_1:def 3;

          then (f . 0 ) in P19 by A7;

          then

          reconsider p = (f . 0 ) as Point of ( TOP-REAL 2);

          (p `1 ) = ( proj1 . (f . 0 )) by PSCOMP_1:def 5

          .= r by A11, A19, BORSUK_1:def 14, FUNCT_1: 13;

          then (f . 0 ) in { q where q be Point of ( TOP-REAL 2) : (q `1 ) = r };

          hence P1 meets ( Vertical_Line r) by A7, A20, XBOOLE_0: 3;

        end;

          case

           A21: (g . 1[01] ) = r;

          

           A22: (f . 1) in ( rng f) by A12, FUNCT_1:def 3;

          then (f . 1) in P1 by A7;

          then

          reconsider p = (f . 1) as Point of ( TOP-REAL 2);

          (p `1 ) = ( proj1 . (f . 1)) by PSCOMP_1:def 5

          .= r by A12, A21, BORSUK_1:def 15, FUNCT_1: 13;

          then (f . 1) in { q where q be Point of ( TOP-REAL 2) : (q `1 ) = r };

          hence P1 meets ( Vertical_Line r) by A7, A22, XBOOLE_0: 3;

        end;

          case (g . 0[01] ) < r & r < (g . 1[01] );

          then

          consider r1 such that

           A23: 0 < r1 and

           A24: r1 < 1 and

           A25: (g . r1) = r by A8, A9, Lm1;

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

          then

           A26: r1 in ( dom f) by A23, A24, XXREAL_1: 1;

          

           A27: ( [#] (( TOP-REAL 2) | P1)) = P1 by PRE_TOPC:def 5;

          

           A28: (f . r1) in ( rng f) by A26, FUNCT_1:def 3;

          then (f . r1) in P19 by A27;

          then

          reconsider p = (f . r1) as Point of ( TOP-REAL 2);

          (p `1 ) = ( proj1 . (f . r1)) by PSCOMP_1:def 5

          .= r by A25, A26, FUNCT_1: 13;

          then (f . r1) in { q where q be Point of ( TOP-REAL 2) : (q `1 ) = r };

          hence P1 meets ( Vertical_Line r) by A27, A28, XBOOLE_0: 3;

        end;

      end;

      hence thesis by A15, A16, TOPS_1: 8;

    end;

     Lm2:

    now

      let P be Simple_closed_curve;

      let P1,P19 be non empty Subset of ( TOP-REAL 2);

      assume that

       A1: ex P2 be non empty Subset of ( TOP-REAL 2) st P1 is_an_arc_of (( W-min P),( E-max P)) & P2 is_an_arc_of (( E-max P),( W-min P)) & (P1 /\ P2) = {( W-min P), ( E-max P)} & (P1 \/ P2) = P & (( First_Point (P1,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) > (( Last_Point (P2,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) and

       A2: ex P29 be non empty Subset of ( TOP-REAL 2) st P19 is_an_arc_of (( W-min P),( E-max P)) & P29 is_an_arc_of (( E-max P),( W-min P)) & (P19 /\ P29) = {( W-min P), ( E-max P)} & (P19 \/ P29) = P & (( First_Point (P19,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) > (( Last_Point (P29,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 );

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

       A3: P1 is_an_arc_of (( W-min P),( E-max P)) and

       A4: P2 is_an_arc_of (( E-max P),( W-min P)) and (P1 /\ P2) = {( W-min P), ( E-max P)} and

       A5: (P1 \/ P2) = P and

       A6: (( First_Point (P1,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) > (( Last_Point (P2,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) by A1;

      

       A7: P2 is_an_arc_of (( W-min P),( E-max P)) by A4, JORDAN5B: 14;

      consider P29 be non empty Subset of ( TOP-REAL 2) such that

       A8: P19 is_an_arc_of (( W-min P),( E-max P)) and

       A9: P29 is_an_arc_of (( E-max P),( W-min P)) and (P19 /\ P29) = {( W-min P), ( E-max P)} and

       A10: (P19 \/ P29) = P and

       A11: (( First_Point (P19,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) > (( Last_Point (P29,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) by A2;

      

       A12: P29 is_an_arc_of (( W-min P),( E-max P)) by A9, JORDAN5B: 14;

      now

        assume that

         A13: P1 = P29 and

         A14: P2 = P19;

        

         A15: (( W-min P) `1 ) = ( W-bound P) by EUCLID: 52;

        

         A16: (( E-max P) `1 ) = ( E-bound P) by EUCLID: 52;

        then

         A17: (( W-min P) `1 ) < (( E-max P) `1 ) by A15, TOPREAL5: 17;

        then

         A18: (( W-min P) `1 ) <= ((( W-bound P) + ( E-bound P)) / 2) by A15, A16, XREAL_1: 226;

        

         A19: ((( W-bound P) + ( E-bound P)) / 2) <= (( E-max P) `1 ) by A15, A16, A17, XREAL_1: 226;

        then

         A20: P2 meets ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)) by A7, A18, Th49;

        (P2 /\ ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2))) is closed by A7, A18, A19, Th49;

        then

         A21: (( First_Point (P1,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) > (( First_Point (P2,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) by A4, A6, A20, JORDAN5C: 18;

        

         A22: P29 meets ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)) by A12, A18, A19, Th49;

        (P29 /\ ( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2))) is closed by A12, A18, A19, Th49;

        hence contradiction by A9, A11, A13, A14, A21, A22, JORDAN5C: 18;

      end;

      hence P1 = P19 by A3, A5, A7, A8, A10, A12, Th48;

    end;

    definition

      let P be Subset of ( TOP-REAL 2);

      :: JORDAN6:def8

      func Upper_Arc (P) -> non empty Subset of ( TOP-REAL 2) means

      : Def8: it is_an_arc_of (( W-min P),( E-max P)) & ex P2 be non empty Subset of ( TOP-REAL 2) st P2 is_an_arc_of (( E-max P),( W-min P)) & (it /\ P2) = {( W-min P), ( E-max P)} & (it \/ P2) = P & (( First_Point (it ,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) > (( Last_Point (P2,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 );

      existence

      proof

        ex P1,P2 be non empty Subset of ( TOP-REAL 2) st P1 is_an_arc_of (( W-min P),( E-max P)) & P2 is_an_arc_of (( E-max P),( W-min P)) & (P1 /\ P2) = {( W-min P), ( E-max P)} & (P1 \/ P2) = P & (( First_Point (P1,( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) > (( Last_Point (P2,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) by A1, Th33;

        hence thesis;

      end;

      uniqueness by A1, Lm2;

    end

    definition

      let P be Subset of ( TOP-REAL 2);

      assume

       A1: P is being_simple_closed_curve;

      then

       A2: ( Upper_Arc P) is_an_arc_of (( W-min P),( E-max P)) by Def8;

      :: JORDAN6:def9

      func Lower_Arc (P) -> non empty Subset of ( TOP-REAL 2) means

      : Def9: it is_an_arc_of (( E-max P),( W-min P)) & (( Upper_Arc P) /\ it ) = {( W-min P), ( E-max P)} & (( Upper_Arc P) \/ it ) = P & (( First_Point (( Upper_Arc P),( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) > (( Last_Point (it ,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 );

      existence by A1, Def8;

      uniqueness

      proof

        let P1,P19 be non empty Subset of ( TOP-REAL 2);

        assume that

         A3: P1 is_an_arc_of (( E-max P),( W-min P)) and (( Upper_Arc P) /\ P1) = {( W-min P), ( E-max P)} and

         A4: (( Upper_Arc P) \/ P1) = P and (( First_Point (( Upper_Arc P),( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) > (( Last_Point (P1,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) and

         A5: P19 is_an_arc_of (( E-max P),( W-min P)) and (( Upper_Arc P) /\ P19) = {( W-min P), ( E-max P)} and

         A6: (( Upper_Arc P) \/ P19) = P and (( First_Point (( Upper_Arc P),( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) > (( Last_Point (P19,( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 );

        

         A7: P1 is_an_arc_of (( W-min P),( E-max P)) by A3, JORDAN5B: 14;

        P19 is_an_arc_of (( W-min P),( E-max P)) by A5, JORDAN5B: 14;

        then P1 = P19 or ( Upper_Arc P) = P19 & P1 = ( Upper_Arc P) by A1, A2, A4, A6, A7, Th48;

        hence thesis;

      end;

    end

    theorem :: JORDAN6:50

    

     Th50: for P be Subset of ( TOP-REAL 2) st P is being_simple_closed_curve holds ( Upper_Arc P) is_an_arc_of (( W-min P),( E-max P)) & ( Upper_Arc P) is_an_arc_of (( E-max P),( W-min P)) & ( Lower_Arc P) is_an_arc_of (( E-max P),( W-min P)) & ( Lower_Arc P) is_an_arc_of (( W-min P),( E-max P)) & (( Upper_Arc P) /\ ( Lower_Arc P)) = {( W-min P), ( E-max P)} & (( Upper_Arc P) \/ ( Lower_Arc P)) = P & (( First_Point (( Upper_Arc P),( W-min P),( E-max P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 ) > (( Last_Point (( Lower_Arc P),( E-max P),( W-min P),( Vertical_Line ((( W-bound P) + ( E-bound P)) / 2)))) `2 )

    proof

      let P be Subset of ( TOP-REAL 2);

      assume

       A1: P is being_simple_closed_curve;

      then

       A2: ( Upper_Arc P) is_an_arc_of (( W-min P),( E-max P)) by Def8;

      ( Lower_Arc P) is_an_arc_of (( E-max P),( W-min P)) by A1, Def9;

      hence thesis by A1, A2, Def9, JORDAN5B: 14;

    end;

    theorem :: JORDAN6:51

    

     Th51: for P be Subset of ( TOP-REAL 2) st P is being_simple_closed_curve holds ( Lower_Arc P) = ((P \ ( Upper_Arc P)) \/ {( W-min P), ( E-max P)}) & ( Upper_Arc P) = ((P \ ( Lower_Arc P)) \/ {( W-min P), ( E-max P)})

    proof

      let P be Subset of ( TOP-REAL 2);

      assume

       A1: P is being_simple_closed_curve;

      then

       A2: (( Upper_Arc P) /\ ( Lower_Arc P)) = {( W-min P), ( E-max P)} by Def9;

      set B = ( Upper_Arc P), A = ( Lower_Arc P);

      

       A3: (((B \/ A) \ B) \/ (B /\ A)) = ((A \ B) \/ (A /\ B)) by XBOOLE_1: 40

      .= A by XBOOLE_1: 51;

      (((B \/ A) \ A) \/ (B /\ A)) = ((B \ A) \/ (B /\ A)) by XBOOLE_1: 40

      .= B by XBOOLE_1: 51;

      hence thesis by A1, A2, A3, Def9;

    end;

    theorem :: JORDAN6:52

    for P be Subset of ( TOP-REAL 2), P1 be Subset of (( TOP-REAL 2) | P) st P is being_simple_closed_curve & (( Upper_Arc P) /\ P1) = {( W-min P), ( E-max P)} & (( Upper_Arc P) \/ P1) = P holds P1 = ( Lower_Arc P)

    proof

      let P be Subset of ( TOP-REAL 2), P1 be Subset of (( TOP-REAL 2) | P);

      assume that

       A1: P is being_simple_closed_curve and

       A2: (( Upper_Arc P) /\ P1) = {( W-min P), ( E-max P)} and

       A3: (( Upper_Arc P) \/ P1) = P;

      set B = ( Upper_Arc P);

      (((B \/ P1) \ B) \/ (B /\ P1)) = ((P1 \ B) \/ (P1 /\ B)) by XBOOLE_1: 40

      .= P1 by XBOOLE_1: 51;

      hence thesis by A1, A2, A3, Th51;

    end;

    theorem :: JORDAN6:53

    for P be Subset of ( TOP-REAL 2), P1 be Subset of (( TOP-REAL 2) | P) st P is being_simple_closed_curve & (P1 /\ ( Lower_Arc P)) = {( W-min P), ( E-max P)} & (P1 \/ ( Lower_Arc P)) = P holds P1 = ( Upper_Arc P)

    proof

      let P be Subset of ( TOP-REAL 2), P1 be Subset of (( TOP-REAL 2) | P);

      assume that

       A1: P is being_simple_closed_curve and

       A2: (P1 /\ ( Lower_Arc P)) = {( W-min P), ( E-max P)} and

       A3: (P1 \/ ( Lower_Arc P)) = P;

      set B = ( Lower_Arc P);

      (((P1 \/ B) \ B) \/ (P1 /\ B)) = ((P1 /\ B) \/ (P1 \ B)) by XBOOLE_1: 40

      .= P1 by XBOOLE_1: 51;

      hence thesis by A1, A2, A3, Th51;

    end;

    begin

    theorem :: JORDAN6:54

    

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

    proof

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

      assume that

       A1: P is_an_arc_of (p1,p2) and

       A2: LE (q,p1,P,p1,p2);

      q in P by A2;

      then LE (p1,q,P,p1,p2) by A1, JORDAN5C: 10;

      hence thesis by A1, A2, JORDAN5C: 12;

    end;

    theorem :: JORDAN6:55

    

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

    proof

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

      assume that

       A1: P is_an_arc_of (p1,p2) and

       A2: LE (p2,q,P,p1,p2);

      q in P by A2;

      then LE (q,p2,P,p1,p2) by A1, JORDAN5C: 10;

      hence thesis by A1, A2, JORDAN5C: 12;

    end;

    definition

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

      :: JORDAN6:def10

      pred LE q1,q2,P means q1 in ( Upper_Arc P) & q2 in ( Lower_Arc P) & not q2 = ( W-min P) or q1 in ( Upper_Arc P) & q2 in ( Upper_Arc P) & LE (q1,q2,( Upper_Arc P),( W-min P),( E-max P)) or q1 in ( Lower_Arc P) & q2 in ( Lower_Arc P) & not q2 = ( W-min P) & LE (q1,q2,( Lower_Arc P),( E-max P),( W-min P));

    end

    theorem :: JORDAN6:56

    for P be Subset of ( TOP-REAL 2), q be Point of ( TOP-REAL 2) st P is being_simple_closed_curve & q in P holds LE (q,q,P)

    proof

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

      assume that

       A1: P is being_simple_closed_curve and

       A2: q in P;

      

       A3: (( Upper_Arc P) \/ ( Lower_Arc P)) = P by A1, Def9;

      

       A4: ( Upper_Arc P) is_an_arc_of (( W-min P),( E-max P)) by A1, Th50;

      now

        per cases by A2, A3, XBOOLE_0:def 3;

          case q in ( Upper_Arc P);

          then LE (q,q,( Upper_Arc P),( W-min P),( E-max P)) by JORDAN5C: 9;

          hence thesis;

        end;

          case

           A5: q in ( Lower_Arc P) & not q in ( Upper_Arc P);

          then

           A6: LE (q,q,( Lower_Arc P),( E-max P),( W-min P)) by JORDAN5C: 9;

          q <> ( W-min P) by A4, A5, TOPREAL1: 1;

          hence thesis by A6;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN6:57

    for P be Subset of ( TOP-REAL 2), q1,q2 be Point of ( TOP-REAL 2) st P is being_simple_closed_curve & LE (q1,q2,P) & LE (q2,q1,P) holds q1 = q2

    proof

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

      assume that

       A1: P is being_simple_closed_curve and

       A2: LE (q1,q2,P) and

       A3: LE (q2,q1,P);

      

       A4: ( Lower_Arc P) is_an_arc_of (( E-max P),( W-min P)) by A1, Def9;

      

       A5: (( Upper_Arc P) /\ ( Lower_Arc P)) = {( W-min P), ( E-max P)} by A1, Def9;

      

       A6: ( Upper_Arc P) is_an_arc_of (( W-min P),( E-max P)) by A1, Th50;

      now

        per cases by A2;

          case

           A7: q1 in ( Upper_Arc P) & q2 in ( Lower_Arc P) & not q2 = ( W-min P);

          now

            per cases by A3;

              case

               A8: q2 in ( Upper_Arc P) & q1 in ( Lower_Arc P) & not q1 = ( W-min P);

              then q1 in (( Upper_Arc P) /\ ( Lower_Arc P)) by A7, XBOOLE_0:def 4;

              then

               A9: q1 = ( E-max P) by A5, A8, TARSKI:def 2;

              q2 in (( Upper_Arc P) /\ ( Lower_Arc P)) by A7, A8, XBOOLE_0:def 4;

              hence thesis by A5, A7, A9, TARSKI:def 2;

            end;

              case

               A10: q2 in ( Upper_Arc P) & q1 in ( Upper_Arc P) & LE (q2,q1,( Upper_Arc P),( W-min P),( E-max P));

              then q2 in (( Upper_Arc P) /\ ( Lower_Arc P)) by A7, XBOOLE_0:def 4;

              then q2 = ( E-max P) by A5, A7, TARSKI:def 2;

              hence thesis by A6, A10, Th55;

            end;

              case

               A11: q2 in ( Lower_Arc P) & q1 in ( Lower_Arc P) & not q1 = ( W-min P) & LE (q2,q1,( Lower_Arc P),( E-max P),( W-min P));

              then q1 in (( Upper_Arc P) /\ ( Lower_Arc P)) by A7, XBOOLE_0:def 4;

              then q1 = ( E-max P) by A5, A11, TARSKI:def 2;

              hence thesis by A4, A11, Th54;

            end;

          end;

          hence thesis;

        end;

          case

           A12: q1 in ( Upper_Arc P) & q2 in ( Upper_Arc P) & LE (q1,q2,( Upper_Arc P),( W-min P),( E-max P));

          now

            per cases by A3;

              case

               A13: q2 in ( Upper_Arc P) & q1 in ( Lower_Arc P) & not q1 = ( W-min P);

              then q1 in (( Upper_Arc P) /\ ( Lower_Arc P)) by A12, XBOOLE_0:def 4;

              then q1 = ( E-max P) by A5, A13, TARSKI:def 2;

              hence thesis by A6, A12, Th55;

            end;

              case q2 in ( Upper_Arc P) & q1 in ( Upper_Arc P) & LE (q2,q1,( Upper_Arc P),( W-min P),( E-max P));

              hence thesis by A6, A12, JORDAN5C: 12;

            end;

              case

               A14: q2 in ( Lower_Arc P) & q1 in ( Lower_Arc P) & not q1 = ( W-min P) & LE (q2,q1,( Lower_Arc P),( E-max P),( W-min P));

              then q1 in (( Upper_Arc P) /\ ( Lower_Arc P)) by A12, XBOOLE_0:def 4;

              then q1 = ( E-max P) by A5, A14, TARSKI:def 2;

              hence thesis by A4, A14, Th54;

            end;

          end;

          hence thesis;

        end;

          case

           A15: q1 in ( Lower_Arc P) & q2 in ( Lower_Arc P) & not q2 = ( W-min P) & LE (q1,q2,( Lower_Arc P),( E-max P),( W-min P));

          now

            per cases by A3;

              case q2 in ( Upper_Arc P) & q1 in ( Lower_Arc P) & not q1 = ( W-min P);

              then q2 in (( Upper_Arc P) /\ ( Lower_Arc P)) by A15, XBOOLE_0:def 4;

              then q2 = ( E-max P) by A5, A15, TARSKI:def 2;

              hence thesis by A4, A15, Th54;

            end;

              case

               A16: q2 in ( Upper_Arc P) & q1 in ( Upper_Arc P) & LE (q2,q1,( Upper_Arc P),( W-min P),( E-max P));

              then q2 in (( Upper_Arc P) /\ ( Lower_Arc P)) by A15, XBOOLE_0:def 4;

              then q2 = ( E-max P) by A5, A15, TARSKI:def 2;

              hence thesis by A6, A16, Th55;

            end;

              case q2 in ( Lower_Arc P) & q1 in ( Lower_Arc P) & not q1 = ( W-min P) & LE (q2,q1,( Lower_Arc P),( E-max P),( W-min P));

              hence thesis by A4, A15, JORDAN5C: 12;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN6:58

    for P be Subset of ( TOP-REAL 2), q1,q2,q3 be Point of ( TOP-REAL 2) st P is being_simple_closed_curve & LE (q1,q2,P) & LE (q2,q3,P) holds LE (q1,q3,P)

    proof

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

      assume that

       A1: P is being_simple_closed_curve and

       A2: LE (q1,q2,P) and

       A3: LE (q2,q3,P);

      

       A4: ( Lower_Arc P) is_an_arc_of (( E-max P),( W-min P)) by A1, Def9;

      

       A5: (( Upper_Arc P) /\ ( Lower_Arc P)) = {( W-min P), ( E-max P)} by A1, Def9;

      

       A6: ( Upper_Arc P) is_an_arc_of (( W-min P),( E-max P)) by A1, Th50;

      now

        per cases by A2;

          case

           A7: q1 in ( Upper_Arc P) & q2 in ( Lower_Arc P) & not q2 = ( W-min P);

          now

            per cases by A3;

              case q2 in ( Upper_Arc P) & q3 in ( Lower_Arc P) & not q3 = ( W-min P);

              hence thesis by A7;

            end;

              case

               A8: q2 in ( Upper_Arc P) & q3 in ( Upper_Arc P) & LE (q2,q3,( Upper_Arc P),( W-min P),( E-max P));

              then q2 in (( Upper_Arc P) /\ ( Lower_Arc P)) by A7, XBOOLE_0:def 4;

              then q2 = ( E-max P) by A5, A7, TARSKI:def 2;

              hence thesis by A2, A6, A8, Th55;

            end;

              case q2 in ( Lower_Arc P) & q3 in ( Lower_Arc P) & not q3 = ( W-min P) & LE (q2,q3,( Lower_Arc P),( E-max P),( W-min P));

              hence thesis by A7;

            end;

          end;

          hence thesis;

        end;

          case

           A9: q1 in ( Upper_Arc P) & q2 in ( Upper_Arc P) & LE (q1,q2,( Upper_Arc P),( W-min P),( E-max P));

          now

            per cases by A3;

              case q2 in ( Upper_Arc P) & q3 in ( Lower_Arc P) & not q3 = ( W-min P);

              hence thesis by A9;

            end;

              case q2 in ( Upper_Arc P) & q3 in ( Upper_Arc P) & LE (q2,q3,( Upper_Arc P),( W-min P),( E-max P));

              then LE (q1,q3,( Upper_Arc P),( W-min P),( E-max P)) by A9, JORDAN5C: 13;

              hence thesis;

            end;

              case q2 in ( Lower_Arc P) & q3 in ( Lower_Arc P) & not q3 = ( W-min P) & LE (q2,q3,( Lower_Arc P),( E-max P),( W-min P));

              hence thesis by A9;

            end;

          end;

          hence thesis;

        end;

          case

           A10: q1 in ( Lower_Arc P) & q2 in ( Lower_Arc P) & not q2 = ( W-min P) & LE (q1,q2,( Lower_Arc P),( E-max P),( W-min P));

          now

            per cases by A3;

              case

               A11: q2 in ( Upper_Arc P) & q3 in ( Lower_Arc P) & not q3 = ( W-min P);

              then q2 in (( Upper_Arc P) /\ ( Lower_Arc P)) by A10, XBOOLE_0:def 4;

              then q2 = ( E-max P) by A5, A10, TARSKI:def 2;

              then LE (q2,q3,( Lower_Arc P),( E-max P),( W-min P)) by A4, A11, JORDAN5C: 10;

              then LE (q1,q3,( Lower_Arc P),( E-max P),( W-min P)) by A10, JORDAN5C: 13;

              hence thesis by A11;

            end;

              case

               A12: q2 in ( Upper_Arc P) & q3 in ( Upper_Arc P) & LE (q2,q3,( Upper_Arc P),( W-min P),( E-max P));

              then q2 in (( Upper_Arc P) /\ ( Lower_Arc P)) by A10, XBOOLE_0:def 4;

              then q2 = ( E-max P) by A5, A10, TARSKI:def 2;

              hence thesis by A2, A6, A12, Th55;

            end;

              case

               A13: q2 in ( Lower_Arc P) & q3 in ( Lower_Arc P) & not q3 = ( W-min P) & LE (q2,q3,( Lower_Arc P),( E-max P),( W-min P));

              then LE (q1,q3,( Lower_Arc P),( E-max P),( W-min P)) by A10, JORDAN5C: 13;

              hence thesis by A13;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN6:59

    for P be Subset of ( TOP-REAL 2), p1,p2,q be Point of ( TOP-REAL 2) st P is_an_arc_of (p1,p2) & q <> p2 holds not p2 in ( L_Segment (P,p1,p2,q))

    proof

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

       A1: P is_an_arc_of (p1,p2) and

       A2: q <> p2;

      assume p2 in ( L_Segment (P,p1,p2,q));

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

      hence contradiction by A1, A2, Th55;

    end;

    theorem :: JORDAN6:60

    for P be Subset of ( TOP-REAL 2), p1,p2,q be Point of ( TOP-REAL 2) st P is_an_arc_of (p1,p2) & q <> p1 holds not p1 in ( R_Segment (P,p1,p2,q))

    proof

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

       A1: P is_an_arc_of (p1,p2) and

       A2: q <> p1;

      assume p1 in ( R_Segment (P,p1,p2,q));

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

      hence contradiction by A1, A2, Th54;

    end;

    registration

      let S be non empty being_simple_closed_curve Subset of ( TOP-REAL 2);

      cluster ( Lower_Arc S) -> non empty compact;

      coherence

      proof

        ( Lower_Arc S) is_an_arc_of (( E-max S),( W-min S)) by Def9;

        hence thesis by JORDAN5A: 1;

      end;

      cluster ( Upper_Arc S) -> non empty compact;

      coherence

      proof

        ( Upper_Arc S) is_an_arc_of (( W-min S),( E-max S)) by Def8;

        hence thesis by JORDAN5A: 1;

      end;

    end

    theorem :: JORDAN6:61

    

     Th61: for S be being_simple_closed_curve non empty Subset of ( TOP-REAL 2) holds ( Lower_Arc S) c= S & ( Upper_Arc S) c= S

    proof

      let S be being_simple_closed_curve non empty Subset of ( TOP-REAL 2);

      S = (( Lower_Arc S) \/ ( Upper_Arc S)) by Th50;

      hence thesis by XBOOLE_1: 7;

    end;

    reserve C for Simple_closed_curve;

    definition

      let C be Simple_closed_curve;

      :: JORDAN6:def11

      func Lower_Middle_Point C -> Point of ( TOP-REAL 2) equals ( First_Point (( Lower_Arc C),( W-min C),( E-max C),( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2))));

      coherence ;

      :: JORDAN6:def12

      func Upper_Middle_Point C -> Point of ( TOP-REAL 2) equals ( First_Point (( Upper_Arc C),( W-min C),( E-max C),( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2))));

      coherence ;

    end

    theorem :: JORDAN6:62

    

     Th62: ( Lower_Arc C) meets ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2))

    proof

      

       A1: ( W-bound C) <= ( E-bound C) by SPRECT_1: 21;

      (( W-min C) `1 ) = ( W-bound C) by EUCLID: 52;

      then

       A2: (( W-min C) `1 ) <= ((( W-bound C) + ( E-bound C)) / 2) by A1, Th1;

      (( E-max C) `1 ) = ( E-bound C) by EUCLID: 52;

      then

       A3: ((( W-bound C) + ( E-bound C)) / 2) <= (( E-max C) `1 ) by A1, Th1;

      ( Lower_Arc C) is_an_arc_of (( W-min C),( E-max C)) by Th50;

      hence thesis by A2, A3, Th49;

    end;

    theorem :: JORDAN6:63

    

     Th63: ( Upper_Arc C) meets ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2))

    proof

      

       A1: ( W-bound C) <= ( E-bound C) by SPRECT_1: 21;

      (( W-min C) `1 ) = ( W-bound C) by EUCLID: 52;

      then

       A2: (( W-min C) `1 ) <= ((( W-bound C) + ( E-bound C)) / 2) by A1, Th1;

      (( E-max C) `1 ) = ( E-bound C) by EUCLID: 52;

      then

       A3: ((( W-bound C) + ( E-bound C)) / 2) <= (( E-max C) `1 ) by A1, Th1;

      ( Upper_Arc C) is_an_arc_of (( W-min C),( E-max C)) by Th50;

      hence thesis by A2, A3, Th49;

    end;

    theorem :: JORDAN6:64

    (( Lower_Middle_Point C) `1 ) = ((( W-bound C) + ( E-bound C)) / 2)

    proof

      set L = ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2)), p = ( First_Point (( Lower_Arc C),( W-min C),( E-max C),L));

      

       A1: ( Lower_Arc C) meets L by Th62;

      L is closed by Th6;

      then

       A2: (( Lower_Arc C) /\ L) is closed by TOPS_1: 8;

      ( Lower_Arc C) is_an_arc_of (( W-min C),( E-max C)) by Th50;

      then p in (( Lower_Arc C) /\ L) by A1, A2, JORDAN5C:def 1;

      then p in L by XBOOLE_0:def 4;

      hence thesis by Th31;

    end;

    theorem :: JORDAN6:65

    (( Upper_Middle_Point C) `1 ) = ((( W-bound C) + ( E-bound C)) / 2)

    proof

      set L = ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2)), p = ( First_Point (( Upper_Arc C),( W-min C),( E-max C),L));

      

       A1: ( Upper_Arc C) meets L by Th63;

      L is closed by Th6;

      then

       A2: (( Upper_Arc C) /\ L) is closed by TOPS_1: 8;

      ( Upper_Arc C) is_an_arc_of (( W-min C),( E-max C)) by Th50;

      then p in (( Upper_Arc C) /\ L) by A1, A2, JORDAN5C:def 1;

      then p in L by XBOOLE_0:def 4;

      hence thesis by Th31;

    end;

    theorem :: JORDAN6:66

    ( Lower_Middle_Point C) in ( Lower_Arc C)

    proof

      set L = ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2)), p = ( First_Point (( Lower_Arc C),( W-min C),( E-max C),L));

      

       A1: ( Lower_Arc C) meets L by Th62;

      L is closed by Th6;

      then

       A2: (( Lower_Arc C) /\ L) is closed by TOPS_1: 8;

      ( Lower_Arc C) is_an_arc_of (( W-min C),( E-max C)) by Th50;

      then p in (L /\ ( Lower_Arc C)) by A1, A2, JORDAN5C:def 1;

      hence thesis by XBOOLE_0:def 4;

    end;

    theorem :: JORDAN6:67

    

     Th67: ( Upper_Middle_Point C) in ( Upper_Arc C)

    proof

      set L = ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2)), p = ( First_Point (( Upper_Arc C),( W-min C),( E-max C),L));

      

       A1: ( Upper_Arc C) meets L by Th63;

      L is closed by Th6;

      then

       A2: (( Upper_Arc C) /\ L) is closed by TOPS_1: 8;

      

       A3: ( Upper_Arc C) is_an_arc_of (( E-max C),( W-min C)) by Th50;

      then p = ( Last_Point (( Upper_Arc C),( E-max C),( W-min C),L)) by A1, A2, JORDAN5C: 18;

      then p in (L /\ ( Upper_Arc C)) by A1, A2, A3, JORDAN5C:def 2;

      hence thesis by XBOOLE_0:def 4;

    end;

    theorem :: JORDAN6:68

    ( Upper_Middle_Point C) in C

    proof

      

       A1: ( Upper_Middle_Point C) in ( Upper_Arc C) by Th67;

      ( Upper_Arc C) c= C by Th61;

      hence thesis by A1;

    end;

    theorem :: JORDAN6:69

    for C be Simple_closed_curve holds for r be Real st ( W-bound C) <= r & r <= ( E-bound C) holds ( LSeg ( |[r, ( S-bound C)]|, |[r, ( N-bound C)]|)) meets ( Upper_Arc C)

    proof

      let C be Simple_closed_curve;

      let r be Real;

      

       A1: (( W-min C) `1 ) = ( W-bound C) by EUCLID: 52;

      

       A2: (( E-max C) `1 ) = ( E-bound C) by EUCLID: 52;

      assume that

       A3: ( W-bound C) <= r and

       A4: r <= ( E-bound C);

      ( Upper_Arc C) is_an_arc_of (( W-min C),( E-max C)) by Def8;

      then ( Upper_Arc C) meets ( Vertical_Line r) by A1, A2, A3, A4, Th49;

      then

      consider x be object such that

       A5: x in (( Upper_Arc C) /\ ( Vertical_Line r)) by XBOOLE_0: 4;

      

       A6: x in ( Upper_Arc C) by A5, XBOOLE_0:def 4;

      

       A7: x in ( Vertical_Line r) by A5, XBOOLE_0:def 4;

      reconsider fs = x as Point of ( TOP-REAL 2) by A5;

      

       A8: ( Upper_Arc C) c= C by Th61;

      then

       A9: ( S-bound C) <= (fs `2 ) by A6, PSCOMP_1: 24;

      

       A10: (fs `2 ) <= ( N-bound C) by A6, A8, PSCOMP_1: 24;

      

       A11: ( |[r, ( S-bound C)]| `1 ) = r by EUCLID: 52

      .= (fs `1 ) by A7, Th31;

      

       A12: ( |[r, ( N-bound C)]| `1 ) = r by EUCLID: 52

      .= (fs `1 ) by A7, Th31;

      

       A13: ( |[r, ( S-bound C)]| `2 ) = ( S-bound C) by EUCLID: 52;

      ( |[r, ( N-bound C)]| `2 ) = ( N-bound C) by EUCLID: 52;

      then x in ( LSeg ( |[r, ( S-bound C)]|, |[r, ( N-bound C)]|)) by A9, A10, A11, A12, A13, GOBOARD7: 7;

      hence thesis by A6, XBOOLE_0: 3;

    end;

    theorem :: JORDAN6:70

    for C be Simple_closed_curve holds for r be Real st ( W-bound C) <= r & r <= ( E-bound C) holds ( LSeg ( |[r, ( S-bound C)]|, |[r, ( N-bound C)]|)) meets ( Lower_Arc C)

    proof

      let C be Simple_closed_curve;

      let r be Real;

      

       A1: (( W-min C) `1 ) = ( W-bound C) by EUCLID: 52;

      

       A2: (( E-max C) `1 ) = ( E-bound C) by EUCLID: 52;

      assume that

       A3: ( W-bound C) <= r and

       A4: r <= ( E-bound C);

      ( Lower_Arc C) is_an_arc_of (( E-max C),( W-min C)) by Def9;

      then ( Lower_Arc C) is_an_arc_of (( W-min C),( E-max C)) by JORDAN5B: 14;

      then ( Lower_Arc C) meets ( Vertical_Line r) by A1, A2, A3, A4, Th49;

      then

      consider x be object such that

       A5: x in (( Lower_Arc C) /\ ( Vertical_Line r)) by XBOOLE_0: 4;

      

       A6: x in ( Lower_Arc C) by A5, XBOOLE_0:def 4;

      

       A7: x in ( Vertical_Line r) by A5, XBOOLE_0:def 4;

      reconsider fs = x as Point of ( TOP-REAL 2) by A5;

      

       A8: ( Lower_Arc C) c= C by Th61;

      then

       A9: ( S-bound C) <= (fs `2 ) by A6, PSCOMP_1: 24;

      

       A10: (fs `2 ) <= ( N-bound C) by A6, A8, PSCOMP_1: 24;

      

       A11: ( |[r, ( S-bound C)]| `1 ) = r by EUCLID: 52

      .= (fs `1 ) by A7, Th31;

      

       A12: ( |[r, ( N-bound C)]| `1 ) = r by EUCLID: 52

      .= (fs `1 ) by A7, Th31;

      

       A13: ( |[r, ( S-bound C)]| `2 ) = ( S-bound C) by EUCLID: 52;

      ( |[r, ( N-bound C)]| `2 ) = ( N-bound C) by EUCLID: 52;

      then x in ( LSeg ( |[r, ( S-bound C)]|, |[r, ( N-bound C)]|)) by A9, A10, A11, A12, A13, GOBOARD7: 7;

      hence thesis by A6, XBOOLE_0: 3;

    end;