jordan18.miz



    begin

    reserve n for Element of NAT ,

V for Subset of ( TOP-REAL n),

s,s1,s2,t,t1,t2 for Point of ( TOP-REAL n),

C for Simple_closed_curve,

P for Subset of ( TOP-REAL 2),

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

    

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

    

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

    theorem :: JORDAN18:1

    for a,b be Real holds ((a - b) ^2 ) = ((b - a) ^2 );

    theorem :: JORDAN18:2

    for S,T be non empty TopStruct, f be Function of S, T, A be Subset of T st f is being_homeomorphism & A is compact holds (f " A) is compact

    proof

      let S,T be non empty TopStruct, f be Function of S, T, A be Subset of T such that

       A1: f is being_homeomorphism and

       A2: A is compact;

      

       A3: ( rng f) = ( [#] T) & f is one-to-one by A1, TOPS_2:def 5;

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

      then

       A4: ( rng (f " )) = ( [#] S) by TOPS_2:def 5;

      (f " ) is continuous by A1, TOPS_2:def 5;

      then ((f " ) .: A) is compact by A2, A4, COMPTS_1: 15;

      hence thesis by A3, TOPS_2: 55;

    end;

    theorem :: JORDAN18:3

    

     Th3: ( proj2 .: ( north_halfline a)) is bounded_below

    proof

      take (a `2 );

      let r be ExtReal;

      assume r in ( proj2 .: ( north_halfline a));

      then

      consider x be object such that

       A1: x in the carrier of ( TOP-REAL 2) and

       A2: x in ( north_halfline a) and

       A3: r = ( proj2 . x) by FUNCT_2: 64;

      reconsider x as Point of ( TOP-REAL 2) by A1;

      r = (x `2 ) by A3, PSCOMP_1:def 6;

      hence thesis by A2, TOPREAL1:def 10;

    end;

    theorem :: JORDAN18:4

    

     Th4: ( proj2 .: ( south_halfline a)) is bounded_above

    proof

      take (a `2 );

      let r be ExtReal;

      assume r in ( proj2 .: ( south_halfline a));

      then

      consider x be object such that

       A1: x in the carrier of ( TOP-REAL 2) and

       A2: x in ( south_halfline a) and

       A3: r = ( proj2 . x) by FUNCT_2: 64;

      reconsider x as Point of ( TOP-REAL 2) by A1;

      r = (x `2 ) by A3, PSCOMP_1:def 6;

      hence thesis by A2, TOPREAL1:def 12;

    end;

    theorem :: JORDAN18:5

    

     Th5: ( proj1 .: ( west_halfline a)) is bounded_above

    proof

      take (a `1 );

      let r be ExtReal;

      assume r in ( proj1 .: ( west_halfline a));

      then

      consider x be object such that

       A1: x in the carrier of ( TOP-REAL 2) and

       A2: x in ( west_halfline a) and

       A3: r = ( proj1 . x) by FUNCT_2: 64;

      reconsider x as Point of ( TOP-REAL 2) by A1;

      r = (x `1 ) by A3, PSCOMP_1:def 5;

      hence thesis by A2, TOPREAL1:def 13;

    end;

    theorem :: JORDAN18:6

    

     Th6: ( proj1 .: ( east_halfline a)) is bounded_below

    proof

      take (a `1 );

      let r be ExtReal;

      assume r in ( proj1 .: ( east_halfline a));

      then

      consider x be object such that

       A1: x in the carrier of ( TOP-REAL 2) and

       A2: x in ( east_halfline a) and

       A3: r = ( proj1 . x) by FUNCT_2: 64;

      reconsider x as Point of ( TOP-REAL 2) by A1;

      r = (x `1 ) by A3, PSCOMP_1:def 5;

      hence thesis by A2, TOPREAL1:def 11;

    end;

    registration

      let a;

      cluster ( proj2 .: ( north_halfline a)) -> non empty;

      coherence by Lm2, RELAT_1: 119;

      cluster ( proj2 .: ( south_halfline a)) -> non empty;

      coherence by Lm2, RELAT_1: 119;

      cluster ( proj1 .: ( west_halfline a)) -> non empty;

      coherence by Lm1, RELAT_1: 119;

      cluster ( proj1 .: ( east_halfline a)) -> non empty;

      coherence by Lm1, RELAT_1: 119;

    end

    theorem :: JORDAN18:7

    

     Th7: ( lower_bound ( proj2 .: ( north_halfline a))) = (a `2 )

    proof

      set X = ( proj2 .: ( north_halfline a));

       A1:

      now

        let r be Real;

        assume r in X;

        then

        consider x be object such that

         A2: x in the carrier of ( TOP-REAL 2) and

         A3: x in ( north_halfline a) and

         A4: r = ( proj2 . x) by FUNCT_2: 64;

        reconsider x as Point of ( TOP-REAL 2) by A2;

        r = (x `2 ) by A4, PSCOMP_1:def 6;

        hence (a `2 ) <= r by A3, TOPREAL1:def 10;

      end;

       A5:

      now

        reconsider r = (a `2 ) as Real;

        let s be Real;

        assume 0 < s;

        then

         A6: (r + 0 ) < ((a `2 ) + s) by XREAL_1: 8;

        take r;

        a in ( north_halfline a) & r = ( proj2 . a) by PSCOMP_1:def 6, TOPREAL1: 38;

        hence r in X by FUNCT_2: 35;

        thus r < ((a `2 ) + s) by A6;

      end;

      X is bounded_below by Th3;

      hence thesis by A1, A5, SEQ_4:def 2;

    end;

    theorem :: JORDAN18:8

    

     Th8: ( upper_bound ( proj2 .: ( south_halfline a))) = (a `2 )

    proof

      set X = ( proj2 .: ( south_halfline a));

       A1:

      now

        let r be Real;

        assume r in X;

        then

        consider x be object such that

         A2: x in the carrier of ( TOP-REAL 2) and

         A3: x in ( south_halfline a) and

         A4: r = ( proj2 . x) by FUNCT_2: 64;

        reconsider x as Point of ( TOP-REAL 2) by A2;

        r = (x `2 ) by A4, PSCOMP_1:def 6;

        hence r <= (a `2 ) by A3, TOPREAL1:def 12;

      end;

       A5:

      now

        reconsider r = (a `2 ) as Real;

        let s be Real;

        assume 0 < s;

        then

         A6: ((a `2 ) - s) < (r - 0 ) by XREAL_1: 15;

        take r;

        a in ( south_halfline a) & r = ( proj2 . a) by PSCOMP_1:def 6, TOPREAL1: 38;

        hence r in X by FUNCT_2: 35;

        thus ((a `2 ) - s) < r by A6;

      end;

      X is bounded_above by Th4;

      hence thesis by A1, A5, SEQ_4:def 1;

    end;

    theorem :: JORDAN18:9

    ( upper_bound ( proj1 .: ( west_halfline a))) = (a `1 )

    proof

      set X = ( proj1 .: ( west_halfline a));

       A1:

      now

        let r be Real;

        assume r in X;

        then

        consider x be object such that

         A2: x in the carrier of ( TOP-REAL 2) and

         A3: x in ( west_halfline a) and

         A4: r = ( proj1 . x) by FUNCT_2: 64;

        reconsider x as Point of ( TOP-REAL 2) by A2;

        r = (x `1 ) by A4, PSCOMP_1:def 5;

        hence r <= (a `1 ) by A3, TOPREAL1:def 13;

      end;

       A5:

      now

        reconsider r = (a `1 ) as Real;

        let s be Real;

        assume 0 < s;

        then

         A6: ((a `1 ) - s) < (r - 0 ) by XREAL_1: 15;

        take r;

        a in ( west_halfline a) & r = ( proj1 . a) by PSCOMP_1:def 5, TOPREAL1: 38;

        hence r in X by FUNCT_2: 35;

        thus ((a `1 ) - s) < r by A6;

      end;

      X is bounded_above by Th5;

      hence thesis by A1, A5, SEQ_4:def 1;

    end;

    theorem :: JORDAN18:10

    ( lower_bound ( proj1 .: ( east_halfline a))) = (a `1 )

    proof

      set X = ( proj1 .: ( east_halfline a));

       A1:

      now

        let r be Real;

        assume r in X;

        then

        consider x be object such that

         A2: x in the carrier of ( TOP-REAL 2) and

         A3: x in ( east_halfline a) and

         A4: r = ( proj1 . x) by FUNCT_2: 64;

        reconsider x as Point of ( TOP-REAL 2) by A2;

        r = (x `1 ) by A4, PSCOMP_1:def 5;

        hence (a `1 ) <= r by A3, TOPREAL1:def 11;

      end;

       A5:

      now

        reconsider r = (a `1 ) as Real;

        let s be Real;

        assume 0 < s;

        then

         A6: (r + 0 ) < ((a `1 ) + s) by XREAL_1: 8;

        take r;

        a in ( east_halfline a) & r = ( proj1 . a) by PSCOMP_1:def 5, TOPREAL1: 38;

        hence r in X by FUNCT_2: 35;

        thus r < ((a `1 ) + s) by A6;

      end;

      X is bounded_below by Th6;

      hence thesis by A1, A5, SEQ_4:def 2;

    end;

    

     Lm3: the TopStruct of ( TOP-REAL 2) = ( TopSpaceMetr ( Euclid 2)) by EUCLID:def 8;

    registration

      let a;

      cluster ( north_halfline a) -> closed;

      coherence

      proof

        set X = ( north_halfline a);

        reconsider XX = (X ` ) as Subset of ( TOP-REAL 2);

        reconsider OO = XX as Subset of ( TopSpaceMetr ( Euclid 2)) by Lm3;

        for p be Point of ( Euclid 2) st p in (X ` ) holds ex r be Real st r > 0 & ( Ball (p,r)) c= (X ` )

        proof

          let p be Point of ( Euclid 2);

          reconsider x = p as Point of ( TOP-REAL 2) by EUCLID: 67;

          assume p in (X ` );

          then

           A1: not p in X by XBOOLE_0:def 5;

          per cases by A1, TOPREAL1:def 10;

            suppose

             A2: (x `1 ) <> (a `1 );

            take r = |.((x `1 ) - (a `1 )).|;

            ((x `1 ) - (a `1 )) <> 0 by A2;

            hence r > 0 by COMPLEX1: 47;

            let b be object;

            assume

             A3: b in ( Ball (p,r));

            then

            reconsider bb = b as Point of ( Euclid 2);

            reconsider c = bb as Point of ( TOP-REAL 2) by EUCLID: 67;

            ( dist (p,bb)) < r by A3, METRIC_1: 11;

            then

             A4: ( dist (x,c)) < r by TOPREAL6:def 1;

            now

              assume (c `1 ) = (a `1 );

              then

               A5: ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) < |.((x `1 ) - (c `1 )).| by A4, TOPREAL6: 92;

              

               A6: 0 <= (((x `1 ) - (c `1 )) ^2 ) by XREAL_1: 63;

              

               A7: 0 <= (((x `2 ) - (c `2 )) ^2 ) by XREAL_1: 63;

              then 0 <= ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) by A6, SQUARE_1:def 2;

              then (( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) ^2 ) < ( |.((x `1 ) - (c `1 )).| ^2 ) by A5, SQUARE_1: 16;

              then (( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) ^2 ) < (((x `1 ) - (c `1 )) ^2 ) by COMPLEX1: 75;

              then ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) < ((((x `1 ) - (c `1 )) ^2 ) + 0 ) by A6, SQUARE_1:def 2;

              hence contradiction by A7, XREAL_1: 7;

            end;

            then not c in X by TOPREAL1:def 10;

            hence b in (X ` ) by XBOOLE_0:def 5;

          end;

            suppose

             A8: (x `2 ) < (a `2 );

            take r = ((a `2 ) - (x `2 ));

            thus r > 0 by A8, XREAL_1: 50;

            let b be object;

            assume

             A9: b in ( Ball (p,r));

            then

            reconsider b as Point of ( Euclid 2);

            reconsider c = b as Point of ( TOP-REAL 2) by EUCLID: 67;

            ( dist (p,b)) < r by A9, METRIC_1: 11;

            then

             A10: ( dist (x,c)) < r by TOPREAL6:def 1;

            now

              assume (c `2 ) >= (a `2 );

              then

               A11: ((a `2 ) - (x `2 )) <= ((c `2 ) - (x `2 )) by XREAL_1: 13;

               0 <= ((a `2 ) - (x `2 )) by A8, XREAL_1: 50;

              then

               A12: (((a `2 ) - (x `2 )) ^2 ) <= (((c `2 ) - (x `2 )) ^2 ) by A11, SQUARE_1: 15;

              

               A13: 0 <= (((x `1 ) - (c `1 )) ^2 ) by XREAL_1: 63;

              

               A14: ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) < ((a `2 ) - (x `2 )) by A10, TOPREAL6: 92;

              

               A15: 0 <= (((x `2 ) - (c `2 )) ^2 ) by XREAL_1: 63;

              then 0 <= ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) by A13, SQUARE_1:def 2;

              then (( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) ^2 ) < (((a `2 ) - (x `2 )) ^2 ) by A14, SQUARE_1: 16;

              then

               A16: ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) < (((a `2 ) - (x `2 )) ^2 ) by A13, A15, SQUARE_1:def 2;

              ( 0 + (((x `2 ) - (c `2 )) ^2 )) <= ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) by A13, XREAL_1: 7;

              hence contradiction by A16, A12, XXREAL_0: 2;

            end;

            then not c in X by TOPREAL1:def 10;

            hence thesis by XBOOLE_0:def 5;

          end;

        end;

        then OO is open by TOPMETR: 15;

        then XX is open by Lm3, PRE_TOPC: 30;

        then (XX ` ) is closed;

        hence thesis;

      end;

      cluster ( south_halfline a) -> closed;

      coherence

      proof

        set X = ( south_halfline a);

        reconsider XX = (X ` ) as Subset of ( TOP-REAL 2);

        reconsider OO = XX as Subset of ( TopSpaceMetr ( Euclid 2)) by Lm3;

        for p be Point of ( Euclid 2) st p in (X ` ) holds ex r be Real st r > 0 & ( Ball (p,r)) c= (X ` )

        proof

          let p be Point of ( Euclid 2);

          reconsider x = p as Point of ( TOP-REAL 2) by EUCLID: 67;

          assume p in (X ` );

          then

           A17: not p in X by XBOOLE_0:def 5;

          per cases by A17, TOPREAL1:def 12;

            suppose

             A18: (x `1 ) <> (a `1 );

            take r = |.((x `1 ) - (a `1 )).|;

            ((x `1 ) - (a `1 )) <> 0 by A18;

            hence r > 0 by COMPLEX1: 47;

            let b be object;

            assume

             A19: b in ( Ball (p,r));

            then

            reconsider b as Point of ( Euclid 2);

            reconsider c = b as Point of ( TOP-REAL 2) by EUCLID: 67;

            ( dist (p,b)) < r by A19, METRIC_1: 11;

            then

             A20: ( dist (x,c)) < r by TOPREAL6:def 1;

            now

              assume (c `1 ) = (a `1 );

              then

               A21: ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) < |.((x `1 ) - (c `1 )).| by A20, TOPREAL6: 92;

              

               A22: 0 <= (((x `1 ) - (c `1 )) ^2 ) by XREAL_1: 63;

              

               A23: 0 <= (((x `2 ) - (c `2 )) ^2 ) by XREAL_1: 63;

              then 0 <= ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) by A22, SQUARE_1:def 2;

              then (( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) ^2 ) < ( |.((x `1 ) - (c `1 )).| ^2 ) by A21, SQUARE_1: 16;

              then (( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) ^2 ) < (((x `1 ) - (c `1 )) ^2 ) by COMPLEX1: 75;

              then ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) < ((((x `1 ) - (c `1 )) ^2 ) + 0 ) by A22, SQUARE_1:def 2;

              hence contradiction by A23, XREAL_1: 7;

            end;

            then not c in X by TOPREAL1:def 12;

            hence thesis by XBOOLE_0:def 5;

          end;

            suppose

             A24: (x `2 ) > (a `2 );

            take r = ((x `2 ) - (a `2 ));

            thus r > 0 by A24, XREAL_1: 50;

            let b be object;

            assume

             A25: b in ( Ball (p,r));

            then

            reconsider b as Point of ( Euclid 2);

            reconsider c = b as Point of ( TOP-REAL 2) by EUCLID: 67;

            ( dist (p,b)) < r by A25, METRIC_1: 11;

            then

             A26: ( dist (x,c)) < r by TOPREAL6:def 1;

            now

              assume (c `2 ) <= (a `2 );

              then

               A27: ((x `2 ) - (c `2 )) >= ((x `2 ) - (a `2 )) by XREAL_1: 13;

               0 <= ((x `2 ) - (a `2 )) by A24, XREAL_1: 50;

              then

               A28: (((x `2 ) - (a `2 )) ^2 ) <= (((x `2 ) - (c `2 )) ^2 ) by A27, SQUARE_1: 15;

              

               A29: 0 <= (((x `1 ) - (c `1 )) ^2 ) by XREAL_1: 63;

              

               A30: ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) < ((x `2 ) - (a `2 )) by A26, TOPREAL6: 92;

              

               A31: 0 <= (((x `2 ) - (c `2 )) ^2 ) by XREAL_1: 63;

              then 0 <= ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) by A29, SQUARE_1:def 2;

              then (( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) ^2 ) < (((x `2 ) - (a `2 )) ^2 ) by A30, SQUARE_1: 16;

              then

               A32: ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) < (((x `2 ) - (a `2 )) ^2 ) by A29, A31, SQUARE_1:def 2;

              ( 0 + (((x `2 ) - (c `2 )) ^2 )) <= ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) by A29, XREAL_1: 7;

              hence contradiction by A32, A28, XXREAL_0: 2;

            end;

            then not c in X by TOPREAL1:def 12;

            hence thesis by XBOOLE_0:def 5;

          end;

        end;

        then OO is open by TOPMETR: 15;

        then XX is open by Lm3, PRE_TOPC: 30;

        then (XX ` ) is closed;

        hence thesis;

      end;

      cluster ( east_halfline a) -> closed;

      coherence

      proof

        set X = ( east_halfline a);

        reconsider XX = (X ` ) as Subset of ( TOP-REAL 2);

        reconsider OO = XX as Subset of ( TopSpaceMetr ( Euclid 2)) by Lm3;

        for p be Point of ( Euclid 2) st p in (X ` ) holds ex r be Real st r > 0 & ( Ball (p,r)) c= (X ` )

        proof

          let p be Point of ( Euclid 2);

          reconsider x = p as Point of ( TOP-REAL 2) by EUCLID: 67;

          assume p in (X ` );

          then

           A33: not p in X by XBOOLE_0:def 5;

          per cases by A33, TOPREAL1:def 11;

            suppose

             A34: (x `2 ) <> (a `2 );

            take r = |.((x `2 ) - (a `2 )).|;

            ((x `2 ) - (a `2 )) <> 0 by A34;

            hence r > 0 by COMPLEX1: 47;

            let b be object;

            assume

             A35: b in ( Ball (p,r));

            then

            reconsider b as Point of ( Euclid 2);

            reconsider c = b as Point of ( TOP-REAL 2) by EUCLID: 67;

            ( dist (p,b)) < r by A35, METRIC_1: 11;

            then

             A36: ( dist (x,c)) < r by TOPREAL6:def 1;

            now

              assume (c `2 ) = (a `2 );

              then

               A37: ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) < |.((x `2 ) - (c `2 )).| by A36, TOPREAL6: 92;

              

               A38: 0 <= (((x `2 ) - (c `2 )) ^2 ) by XREAL_1: 63;

              

               A39: 0 <= (((x `1 ) - (c `1 )) ^2 ) by XREAL_1: 63;

              then 0 <= ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) by A38, SQUARE_1:def 2;

              then (( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) ^2 ) < ( |.((x `2 ) - (c `2 )).| ^2 ) by A37, SQUARE_1: 16;

              then (( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) ^2 ) < (((x `2 ) - (c `2 )) ^2 ) by COMPLEX1: 75;

              then ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) < ((((x `2 ) - (c `2 )) ^2 ) + 0 ) by A38, SQUARE_1:def 2;

              hence contradiction by A39, XREAL_1: 7;

            end;

            then not c in X by TOPREAL1:def 11;

            hence thesis by XBOOLE_0:def 5;

          end;

            suppose

             A40: (x `1 ) < (a `1 );

            take r = ((a `1 ) - (x `1 ));

            thus r > 0 by A40, XREAL_1: 50;

            let b be object;

            assume

             A41: b in ( Ball (p,r));

            then

            reconsider b as Point of ( Euclid 2);

            reconsider c = b as Point of ( TOP-REAL 2) by EUCLID: 67;

            ( dist (p,b)) < r by A41, METRIC_1: 11;

            then

             A42: ( dist (x,c)) < r by TOPREAL6:def 1;

            now

              assume (c `1 ) >= (a `1 );

              then

               A43: ((a `1 ) - (x `1 )) <= ((c `1 ) - (x `1 )) by XREAL_1: 13;

               0 <= ((a `1 ) - (x `1 )) by A40, XREAL_1: 50;

              then

               A44: (((a `1 ) - (x `1 )) ^2 ) <= (((c `1 ) - (x `1 )) ^2 ) by A43, SQUARE_1: 15;

              

               A45: 0 <= (((x `2 ) - (c `2 )) ^2 ) by XREAL_1: 63;

              

               A46: ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) < ((a `1 ) - (x `1 )) by A42, TOPREAL6: 92;

              

               A47: 0 <= (((x `1 ) - (c `1 )) ^2 ) by XREAL_1: 63;

              then 0 <= ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) by A45, SQUARE_1:def 2;

              then (( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) ^2 ) < (((a `1 ) - (x `1 )) ^2 ) by A46, SQUARE_1: 16;

              then

               A48: ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) < (((a `1 ) - (x `1 )) ^2 ) by A45, A47, SQUARE_1:def 2;

              ((((x `1 ) - (c `1 )) ^2 ) + 0 ) <= ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) by A45, XREAL_1: 7;

              hence contradiction by A48, A44, XXREAL_0: 2;

            end;

            then not c in X by TOPREAL1:def 11;

            hence thesis by XBOOLE_0:def 5;

          end;

        end;

        then OO is open by TOPMETR: 15;

        then XX is open by Lm3, PRE_TOPC: 30;

        then (XX ` ) is closed;

        hence thesis;

      end;

      cluster ( west_halfline a) -> closed;

      coherence

      proof

        set X = ( west_halfline a);

        reconsider XX = (X ` ) as Subset of ( TOP-REAL 2);

        reconsider OO = XX as Subset of ( TopSpaceMetr ( Euclid 2)) by Lm3;

        for p be Point of ( Euclid 2) st p in (X ` ) holds ex r be Real st r > 0 & ( Ball (p,r)) c= (X ` )

        proof

          let p be Point of ( Euclid 2);

          reconsider x = p as Point of ( TOP-REAL 2) by EUCLID: 67;

          assume p in (X ` );

          then

           A49: not p in X by XBOOLE_0:def 5;

          per cases by A49, TOPREAL1:def 13;

            suppose

             A50: (x `2 ) <> (a `2 );

            take r = |.((x `2 ) - (a `2 )).|;

            ((x `2 ) - (a `2 )) <> 0 by A50;

            hence r > 0 by COMPLEX1: 47;

            let b be object;

            assume

             A51: b in ( Ball (p,r));

            then

            reconsider b as Point of ( Euclid 2);

            reconsider c = b as Point of ( TOP-REAL 2) by EUCLID: 67;

            ( dist (p,b)) < r by A51, METRIC_1: 11;

            then

             A52: ( dist (x,c)) < r by TOPREAL6:def 1;

            now

              assume (c `2 ) = (a `2 );

              then

               A53: ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) < |.((x `2 ) - (c `2 )).| by A52, TOPREAL6: 92;

              

               A54: 0 <= (((x `2 ) - (c `2 )) ^2 ) by XREAL_1: 63;

              

               A55: 0 <= (((x `1 ) - (c `1 )) ^2 ) by XREAL_1: 63;

              then 0 <= ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) by A54, SQUARE_1:def 2;

              then (( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) ^2 ) < ( |.((x `2 ) - (c `2 )).| ^2 ) by A53, SQUARE_1: 16;

              then (( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) ^2 ) < (((x `2 ) - (c `2 )) ^2 ) by COMPLEX1: 75;

              then ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) < ((((x `2 ) - (c `2 )) ^2 ) + 0 ) by A54, SQUARE_1:def 2;

              hence contradiction by A55, XREAL_1: 7;

            end;

            then not c in X by TOPREAL1:def 13;

            hence thesis by XBOOLE_0:def 5;

          end;

            suppose

             A56: (x `1 ) > (a `1 );

            take r = ((x `1 ) - (a `1 ));

            thus r > 0 by A56, XREAL_1: 50;

            let b be object;

            assume

             A57: b in ( Ball (p,r));

            then

            reconsider b as Point of ( Euclid 2);

            reconsider c = b as Point of ( TOP-REAL 2) by EUCLID: 67;

            ( dist (p,b)) < r by A57, METRIC_1: 11;

            then

             A58: ( dist (x,c)) < r by TOPREAL6:def 1;

            now

              assume (c `1 ) <= (a `1 );

              then

               A59: ((x `1 ) - (c `1 )) >= ((x `1 ) - (a `1 )) by XREAL_1: 13;

               0 <= ((x `1 ) - (a `1 )) by A56, XREAL_1: 50;

              then

               A60: (((x `1 ) - (a `1 )) ^2 ) <= (((x `1 ) - (c `1 )) ^2 ) by A59, SQUARE_1: 15;

              

               A61: 0 <= (((x `2 ) - (c `2 )) ^2 ) by XREAL_1: 63;

              

               A62: ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) < ((x `1 ) - (a `1 )) by A58, TOPREAL6: 92;

              

               A63: 0 <= (((x `1 ) - (c `1 )) ^2 ) by XREAL_1: 63;

              then 0 <= ( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) by A61, SQUARE_1:def 2;

              then (( sqrt ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 ))) ^2 ) < (((x `1 ) - (a `1 )) ^2 ) by A62, SQUARE_1: 16;

              then

               A64: ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) < (((x `1 ) - (a `1 )) ^2 ) by A61, A63, SQUARE_1:def 2;

              ( 0 + (((x `1 ) - (c `1 )) ^2 )) <= ((((x `1 ) - (c `1 )) ^2 ) + (((x `2 ) - (c `2 )) ^2 )) by A61, XREAL_1: 7;

              hence contradiction by A64, A60, XXREAL_0: 2;

            end;

            then not c in X by TOPREAL1:def 13;

            hence thesis by XBOOLE_0:def 5;

          end;

        end;

        then OO is open by TOPMETR: 15;

        then XX is open by Lm3, PRE_TOPC: 30;

        then (XX ` ) is closed;

        hence thesis;

      end;

    end

    theorem :: JORDAN18:11

    

     Th11: a in ( BDD P) implies not ( north_halfline a) c= ( UBD P)

    proof

      

       A1: ( BDD P) misses ( UBD P) & a in ( north_halfline a) by JORDAN2C: 24, TOPREAL1: 38;

      assume a in ( BDD P);

      hence thesis by A1, XBOOLE_0: 3;

    end;

    theorem :: JORDAN18:12

    

     Th12: a in ( BDD P) implies not ( south_halfline a) c= ( UBD P)

    proof

      

       A1: ( BDD P) misses ( UBD P) & a in ( south_halfline a) by JORDAN2C: 24, TOPREAL1: 38;

      assume a in ( BDD P);

      hence thesis by A1, XBOOLE_0: 3;

    end;

    theorem :: JORDAN18:13

    a in ( BDD P) implies not ( east_halfline a) c= ( UBD P)

    proof

      

       A1: ( BDD P) misses ( UBD P) & a in ( east_halfline a) by JORDAN2C: 24, TOPREAL1: 38;

      assume a in ( BDD P);

      hence thesis by A1, XBOOLE_0: 3;

    end;

    theorem :: JORDAN18:14

    a in ( BDD P) implies not ( west_halfline a) c= ( UBD P)

    proof

      

       A1: ( BDD P) misses ( UBD P) & a in ( west_halfline a) by JORDAN2C: 24, TOPREAL1: 38;

      assume a in ( BDD P);

      hence thesis by A1, XBOOLE_0: 3;

    end;

    theorem :: JORDAN18:15

    

     Th15: for C be Simple_closed_curve, P be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2) st P is_an_arc_of (p1,p2) & P c= C holds ex R be non empty Subset of ( TOP-REAL 2) st R is_an_arc_of (p1,p2) & (P \/ R) = C & (P /\ R) = {p1, p2}

    proof

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

       A1: P is_an_arc_of (p1,p2) and

       A2: P c= C;

      

       A3: p1 <> p2 by A1, JORDAN6: 37;

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

      then

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

       A4: P1 is_an_arc_of (p1,p2) and

       A5: P2 is_an_arc_of (p1,p2) and

       A6: C = (P1 \/ P2) and

       A7: (P1 /\ P2) = {p1, p2} by A2, A3, TOPREAL2: 5;

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

      

       A8: P1 c= C & P2 c= C by A6, XBOOLE_1: 7;

       A9:

      now

        assume

         A10: P1 = P2;

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

        hence contradiction by A7, A10, TARSKI:def 2;

      end;

      per cases by A1, A2, A4, A5, A8, A9, JORDAN16: 14;

        suppose

         A11: P = P1;

        take P2;

        thus thesis by A5, A6, A7, A11;

      end;

        suppose

         A12: P = P2;

        take P1;

        thus thesis by A4, A6, A7, A12;

      end;

    end;

    begin

    definition

      let p, P;

      :: JORDAN18:def1

      func North-Bound (p,P) -> Point of ( TOP-REAL 2) equals |[(p `1 ), ( lower_bound ( proj2 .: (P /\ ( north_halfline p))))]|;

      correctness ;

      :: JORDAN18:def2

      func South-Bound (p,P) -> Point of ( TOP-REAL 2) equals |[(p `1 ), ( upper_bound ( proj2 .: (P /\ ( south_halfline p))))]|;

      correctness ;

    end

    theorem :: JORDAN18:16

    (( North-Bound (p,P)) `1 ) = (p `1 ) & (( South-Bound (p,P)) `1 ) = (p `1 ) by EUCLID: 52;

    theorem :: JORDAN18:17

    

     Th17: for C be compact Subset of ( TOP-REAL 2) holds p in ( BDD C) implies ( North-Bound (p,C)) in C & ( North-Bound (p,C)) in ( north_halfline p) & ( South-Bound (p,C)) in C & ( South-Bound (p,C)) in ( south_halfline p)

    proof

      let C be compact Subset of ( TOP-REAL 2);

      set X = (C /\ ( north_halfline p));

      X c= C by XBOOLE_1: 17;

      then ( proj2 .: X) is real-bounded by JCT_MISC: 14, RLTOPSP1: 42;

      then

       A1: ( proj2 .: X) is bounded_below;

      assume

       A2: p in ( BDD C);

      then not ( north_halfline p) c= ( UBD C) by Th11;

      then ( north_halfline p) meets C by JORDAN2C: 129;

      then

       A3: X is non empty;

      X is bounded by RLTOPSP1: 42, XBOOLE_1: 17;

      then ( proj2 .: X) is closed by JCT_MISC: 13;

      then ( lower_bound ( proj2 .: X)) in ( proj2 .: X) by A3, A1, Lm2, RCOMP_1: 13, RELAT_1: 119;

      then

      consider x be object such that

       A4: x in the carrier of ( TOP-REAL 2) and

       A5: x in X and

       A6: ( lower_bound ( proj2 .: X)) = ( proj2 . x) by FUNCT_2: 64;

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

      

       A7: (x `2 ) = ( lower_bound ( proj2 .: X)) by A6, PSCOMP_1:def 6

      .= (( North-Bound (p,C)) `2 ) by EUCLID: 52;

      x in ( north_halfline p) by A5, XBOOLE_0:def 4;

      

      then (x `1 ) = (p `1 ) by TOPREAL1:def 10

      .= (( North-Bound (p,C)) `1 ) by EUCLID: 52;

      then x = ( North-Bound (p,C)) by A7, TOPREAL3: 6;

      hence ( North-Bound (p,C)) in C & ( North-Bound (p,C)) in ( north_halfline p) by A5, XBOOLE_0:def 4;

      set X = (C /\ ( south_halfline p));

      X c= C by XBOOLE_1: 17;

      then ( proj2 .: X) is real-bounded by JCT_MISC: 14, RLTOPSP1: 42;

      then

       A8: ( proj2 .: X) is bounded_above;

       not ( south_halfline p) c= ( UBD C) by A2, Th12;

      then ( south_halfline p) meets C by JORDAN2C: 128;

      then

       A9: X is non empty;

      X is bounded by RLTOPSP1: 42, XBOOLE_1: 17;

      then ( proj2 .: X) is closed by JCT_MISC: 13;

      then ( upper_bound ( proj2 .: X)) in ( proj2 .: X) by A9, A8, Lm2, RCOMP_1: 12, RELAT_1: 119;

      then

      consider x be object such that

       A10: x in the carrier of ( TOP-REAL 2) and

       A11: x in X and

       A12: ( upper_bound ( proj2 .: X)) = ( proj2 . x) by FUNCT_2: 64;

      reconsider x as Point of ( TOP-REAL 2) by A10;

      x in ( south_halfline p) by A11, XBOOLE_0:def 4;

      

      then

       A13: (x `1 ) = (p `1 ) by TOPREAL1:def 12

      .= (( South-Bound (p,C)) `1 ) by EUCLID: 52;

      (x `2 ) = ( upper_bound ( proj2 .: X)) by A12, PSCOMP_1:def 6

      .= (( South-Bound (p,C)) `2 ) by EUCLID: 52;

      then x = ( South-Bound (p,C)) by A13, TOPREAL3: 6;

      hence thesis by A11, XBOOLE_0:def 4;

    end;

    theorem :: JORDAN18:18

    

     Th18: for C be compact Subset of ( TOP-REAL 2) holds p in ( BDD C) implies (( South-Bound (p,C)) `2 ) < (p `2 ) & (p `2 ) < (( North-Bound (p,C)) `2 )

    proof

      let C be compact Subset of ( TOP-REAL 2);

      assume

       A1: p in ( BDD C);

      then ( South-Bound (p,C)) in C & ( South-Bound (p,C)) in ( south_halfline p) by Th17;

      then ( South-Bound (p,C)) in (C /\ ( south_halfline p)) by XBOOLE_0:def 4;

      then

       A2: ( proj2 .: (C /\ ( south_halfline p))) is non empty by Lm2, RELAT_1: 119;

      

       A3: ( BDD C) misses C by JORDAN1A: 7;

       A4:

      now

        

         A5: (( South-Bound (p,C)) `1 ) = (p `1 ) by EUCLID: 52;

        assume (( South-Bound (p,C)) `2 ) = (p `2 );

        then ( South-Bound (p,C)) = p by A5, TOPREAL3: 6;

        then p in C by A1, Th17;

        hence contradiction by A1, A3, XBOOLE_0: 3;

      end;

      ( North-Bound (p,C)) in C & ( North-Bound (p,C)) in ( north_halfline p) by A1, Th17;

      then (C /\ ( north_halfline p)) is non empty by XBOOLE_0:def 4;

      then

       A6: ( proj2 .: (C /\ ( north_halfline p))) is non empty by Lm2, RELAT_1: 119;

      ( proj2 .: ( south_halfline p)) is bounded_above & (C /\ ( south_halfline p)) c= ( south_halfline p) by Th4, XBOOLE_1: 17;

      then

       A7: ( upper_bound ( proj2 .: (C /\ ( south_halfline p)))) <= ( upper_bound ( proj2 .: ( south_halfline p))) by A2, RELAT_1: 123, SEQ_4: 48;

       A8:

      now

        

         A9: (( North-Bound (p,C)) `1 ) = (p `1 ) by EUCLID: 52;

        assume (( North-Bound (p,C)) `2 ) = (p `2 );

        then ( North-Bound (p,C)) = p by A9, TOPREAL3: 6;

        then p in C by A1, Th17;

        hence contradiction by A1, A3, XBOOLE_0: 3;

      end;

      (( South-Bound (p,C)) `2 ) = ( upper_bound ( proj2 .: (C /\ ( south_halfline p)))) & ( upper_bound ( proj2 .: ( south_halfline p))) = (p `2 ) by Th8, EUCLID: 52;

      hence (( South-Bound (p,C)) `2 ) < (p `2 ) by A7, A4, XXREAL_0: 1;

      ( proj2 .: ( north_halfline p)) is bounded_below & (C /\ ( north_halfline p)) c= ( north_halfline p) by Th3, XBOOLE_1: 17;

      then

       A10: ( lower_bound ( proj2 .: (C /\ ( north_halfline p)))) >= ( lower_bound ( proj2 .: ( north_halfline p))) by A6, RELAT_1: 123, SEQ_4: 47;

      ( lower_bound ( proj2 .: ( north_halfline p))) = (p `2 ) & (( North-Bound (p,C)) `2 ) = ( lower_bound ( proj2 .: (C /\ ( north_halfline p)))) by Th7, EUCLID: 52;

      hence thesis by A10, A8, XXREAL_0: 1;

    end;

    theorem :: JORDAN18:19

    

     Th19: for C be compact Subset of ( TOP-REAL 2) holds p in ( BDD C) implies ( lower_bound ( proj2 .: (C /\ ( north_halfline p)))) > ( upper_bound ( proj2 .: (C /\ ( south_halfline p))))

    proof

      let C be compact Subset of ( TOP-REAL 2);

      assume p in ( BDD C);

      then

       A1: (( South-Bound (p,C)) `2 ) < (p `2 ) & (p `2 ) < (( North-Bound (p,C)) `2 ) by Th18;

      (( North-Bound (p,C)) `2 ) = ( lower_bound ( proj2 .: (C /\ ( north_halfline p)))) & (( South-Bound (p,C)) `2 ) = ( upper_bound ( proj2 .: (C /\ ( south_halfline p)))) by EUCLID: 52;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: JORDAN18:20

    for C be compact Subset of ( TOP-REAL 2) holds p in ( BDD C) implies ( South-Bound (p,C)) <> ( North-Bound (p,C))

    proof

      let C be compact Subset of ( TOP-REAL 2);

      assume

       A1: p in ( BDD C);

      

       A2: (( North-Bound (p,C)) `2 ) = ( lower_bound ( proj2 .: (C /\ ( north_halfline p)))) & (( South-Bound (p,C)) `2 ) = ( upper_bound ( proj2 .: (C /\ ( south_halfline p)))) by EUCLID: 52;

      assume not thesis;

      hence thesis by A1, A2, Th19;

    end;

    theorem :: JORDAN18:21

    

     Th21: for C be Subset of ( TOP-REAL 2) holds ( LSeg (( North-Bound (p,C)),( South-Bound (p,C)))) is vertical

    proof

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

      (( North-Bound (p,C)) `1 ) = (p `1 ) & (( South-Bound (p,C)) `1 ) = (p `1 ) by EUCLID: 52;

      hence thesis by SPPOL_1: 16;

    end;

    theorem :: JORDAN18:22

    for C be compact Subset of ( TOP-REAL 2) holds p in ( BDD C) implies (( LSeg (( North-Bound (p,C)),( South-Bound (p,C)))) /\ C) = {( North-Bound (p,C)), ( South-Bound (p,C))}

    proof

      let C be compact Subset of ( TOP-REAL 2);

      set L = ( LSeg (( North-Bound (p,C)),( South-Bound (p,C))));

      assume

       A1: p in ( BDD C);

      then

       A2: ( North-Bound (p,C)) in C & ( South-Bound (p,C)) in C by Th17;

      hereby

        

         A3: (( North-Bound (p,C)) `2 ) = ( lower_bound ( proj2 .: (C /\ ( north_halfline p)))) by EUCLID: 52;

        

         A4: (( South-Bound (p,C)) `2 ) = ( upper_bound ( proj2 .: (C /\ ( south_halfline p)))) by EUCLID: 52;

        let x be object;

        

         A5: (( South-Bound (p,C)) `1 ) = (p `1 ) by EUCLID: 52;

        assume

         A6: x in (L /\ C);

        then

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

        

         A7: x in L by A6, XBOOLE_0:def 4;

        L is vertical & ( South-Bound (p,C)) in L by Th21, RLTOPSP1: 68;

        then

         A8: (y `1 ) = (p `1 ) by A5, A7, SPPOL_1:def 3;

        

         A9: x in C by A6, XBOOLE_0:def 4;

        

         A10: (( North-Bound (p,C)) `1 ) = (p `1 ) by EUCLID: 52;

        now

          (C /\ ( north_halfline p)) is bounded by TOPREAL6: 89;

          then ( proj2 .: (C /\ ( north_halfline p))) is real-bounded by JCT_MISC: 14;

          then

           A11: ( proj2 .: (C /\ ( north_halfline p))) is bounded_below;

          (( South-Bound (p,C)) `2 ) < (p `2 ) & (p `2 ) < (( North-Bound (p,C)) `2 ) by A1, Th18;

          then

           A12: (( South-Bound (p,C)) `2 ) < (( North-Bound (p,C)) `2 ) by XXREAL_0: 2;

          then

           A13: (( South-Bound (p,C)) `2 ) <= (y `2 ) by A7, TOPREAL1: 4;

          assume y <> ( North-Bound (p,C));

          then

           A14: (y `2 ) <> (( North-Bound (p,C)) `2 ) by A10, A8, TOPREAL3: 6;

          

           A15: (y `2 ) = ( proj2 . y) by PSCOMP_1:def 6;

          (y `2 ) <= (( North-Bound (p,C)) `2 ) by A7, A12, TOPREAL1: 4;

          then

           A16: (y `2 ) < (( North-Bound (p,C)) `2 ) by A14, XXREAL_0: 1;

          now

            assume (y `2 ) > (p `2 );

            then y in ( north_halfline p) by A8, TOPREAL1:def 10;

            then y in (C /\ ( north_halfline p)) by A9, XBOOLE_0:def 4;

            then (y `2 ) in ( proj2 .: (C /\ ( north_halfline p))) by A15, FUNCT_2: 35;

            hence contradiction by A3, A16, A11, SEQ_4:def 2;

          end;

          then y in ( south_halfline p) by A8, TOPREAL1:def 12;

          then y in (C /\ ( south_halfline p)) by A9, XBOOLE_0:def 4;

          then

           A17: (y `2 ) in ( proj2 .: (C /\ ( south_halfline p))) by A15, FUNCT_2: 35;

          (C /\ ( south_halfline p)) is bounded by TOPREAL6: 89;

          then ( proj2 .: (C /\ ( south_halfline p))) is real-bounded by JCT_MISC: 14;

          then ( proj2 .: (C /\ ( south_halfline p))) is bounded_above;

          then (y `2 ) <= (( South-Bound (p,C)) `2 ) by A4, A17, SEQ_4:def 1;

          then (y `2 ) = (( South-Bound (p,C)) `2 ) by A13, XXREAL_0: 1;

          hence y = ( South-Bound (p,C)) by A5, A8, TOPREAL3: 6;

        end;

        hence x in {( North-Bound (p,C)), ( South-Bound (p,C))} by TARSKI:def 2;

      end;

      let x be object;

      assume x in {( North-Bound (p,C)), ( South-Bound (p,C))};

      then

       A18: x = ( North-Bound (p,C)) or x = ( South-Bound (p,C)) by TARSKI:def 2;

      then x in L by RLTOPSP1: 68;

      hence thesis by A18, A2, XBOOLE_0:def 4;

    end;

    theorem :: JORDAN18:23

    for C be compact Subset of ( TOP-REAL 2) holds p in ( BDD C) & q in ( BDD C) & (p `1 ) <> (q `1 ) implies (( North-Bound (p,C)),( South-Bound (q,C)),( North-Bound (q,C)),( South-Bound (p,C))) are_mutually_distinct

    proof

      let C be compact Subset of ( TOP-REAL 2);

      set np = ( North-Bound (p,C)), sq = ( South-Bound (q,C)), nq = ( North-Bound (q,C)), sp = ( South-Bound (p,C));

      

       A1: (np `1 ) = (p `1 ) & (sp `1 ) = (p `1 ) by EUCLID: 52;

      

       A2: (( North-Bound (q,C)) `2 ) = ( lower_bound ( proj2 .: (C /\ ( north_halfline q)))) & (( South-Bound (q,C)) `2 ) = ( upper_bound ( proj2 .: (C /\ ( south_halfline q)))) by EUCLID: 52;

      

       A3: (( North-Bound (p,C)) `2 ) = ( lower_bound ( proj2 .: (C /\ ( north_halfline p)))) & (( South-Bound (p,C)) `2 ) = ( upper_bound ( proj2 .: (C /\ ( south_halfline p)))) by EUCLID: 52;

      assume p in ( BDD C) & q in ( BDD C) & (p `1 ) <> (q `1 );

      hence np <> sq & np <> nq & np <> sp & sq <> nq & sq <> sp & nq <> sp by A1, A2, A3, Th19, EUCLID: 52;

    end;

    begin

    definition

      let n, V, s1, s2, t1, t2;

      :: JORDAN18:def3

      pred s1,s2,V -separate t1,t2 means for A be Subset of ( TOP-REAL n) st A is_an_arc_of (s1,s2) & A c= V holds A meets {t1, t2};

    end

    notation

      let n, V, s1, s2, t1, t2;

      antonym s1,s2 are_neighbours_wrt t1,t2,V for s1,s2,V -separate t1,t2;

    end

    theorem :: JORDAN18:24

    (t,t,V) -separate (s1,s2) by JORDAN6: 37;

    theorem :: JORDAN18:25

    (s1,s2,V) -separate (t1,t2) implies (s2,s1,V) -separate (t1,t2) by JORDAN5B: 14;

    theorem :: JORDAN18:26

    (s1,s2,V) -separate (t1,t2) implies (s1,s2,V) -separate (t2,t1);

    theorem :: JORDAN18:27

    

     Th27: (s,t1,V) -separate (s,t2)

    proof

      let A be Subset of ( TOP-REAL n) such that

       A1: A is_an_arc_of (s,t1) and A c= V;

      

       A2: s in {s, t2} by TARSKI:def 2;

      s in A by A1, TOPREAL1: 1;

      hence thesis by A2, XBOOLE_0: 3;

    end;

    theorem :: JORDAN18:28

    

     Th28: (t1,s,V) -separate (t2,s)

    proof

      let A be Subset of ( TOP-REAL n) such that

       A1: A is_an_arc_of (t1,s) and A c= V;

      

       A2: s in {s, t2} by TARSKI:def 2;

      s in A by A1, TOPREAL1: 1;

      hence thesis by A2, XBOOLE_0: 3;

    end;

    theorem :: JORDAN18:29

    

     Th29: (t1,s,V) -separate (s,t2)

    proof

      let A be Subset of ( TOP-REAL n) such that

       A1: A is_an_arc_of (t1,s) and A c= V;

      

       A2: s in {s, t2} by TARSKI:def 2;

      s in A by A1, TOPREAL1: 1;

      hence thesis by A2, XBOOLE_0: 3;

    end;

    theorem :: JORDAN18:30

    

     Th30: (s,t1,V) -separate (t2,s)

    proof

      let A be Subset of ( TOP-REAL n) such that

       A1: A is_an_arc_of (s,t1) and A c= V;

      

       A2: s in {s, t2} by TARSKI:def 2;

      s in A by A1, TOPREAL1: 1;

      hence thesis by A2, XBOOLE_0: 3;

    end;

    theorem :: JORDAN18:31

    for p1,p2,q be Point of ( TOP-REAL 2) st q in C & p1 in C & p2 in C & p1 <> p2 & p1 <> q & p2 <> q holds (p1,p2) are_neighbours_wrt (q,q,C)

    proof

      let p1,p2,q be Point of ( TOP-REAL 2) such that

       A1: q in C and

       A2: p1 in C & p2 in C & p1 <> p2 and

       A3: p1 <> q & p2 <> q;

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

       A4: P1 is_an_arc_of (p1,p2) and

       A5: P2 is_an_arc_of (p1,p2) and

       A6: C = (P1 \/ P2) and

       A7: (P1 /\ P2) = {p1, p2} by A2, TOPREAL2: 5;

      per cases by A1, A6, XBOOLE_0:def 3;

        suppose

         A8: q in P1 & not q in P2;

        take P2;

        thus P2 is_an_arc_of (p1,p2) by A5;

        thus P2 c= C by A6, XBOOLE_1: 7;

        thus P2 misses {q, q} by A8, ZFMISC_1: 51;

      end;

        suppose

         A9: q in P2 & not q in P1;

        take P1;

        thus P1 is_an_arc_of (p1,p2) by A4;

        thus P1 c= C by A6, XBOOLE_1: 7;

        thus P1 misses {q, q} by A9, ZFMISC_1: 51;

      end;

        suppose q in P1 & q in P2;

        then q in (P1 /\ P2) by XBOOLE_0:def 4;

        hence thesis by A3, A7, TARSKI:def 2;

      end;

    end;

    theorem :: JORDAN18:32

    p1 <> p2 & p1 in C & p2 in C implies ((p1,p2,C) -separate (q1,q2) implies (q1,q2,C) -separate (p1,p2))

    proof

      assume that

       A1: p1 <> p2 and

       A2: p1 in C and

       A3: p2 in C and

       A4: (p1,p2,C) -separate (q1,q2);

      per cases ;

        suppose q1 = p1;

        hence thesis by Th27;

      end;

        suppose q2 = p2;

        hence thesis by Th28;

      end;

        suppose q1 = p2;

        hence thesis by Th30;

      end;

        suppose p1 = q2;

        hence thesis by Th29;

      end;

        suppose that

         A5: q1 <> p1 & q2 <> p2 & q1 <> p2 & q2 <> p1;

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

        assume A is_an_arc_of (q1,q2) & A c= C;

        then

        consider B be non empty Subset of ( TOP-REAL 2) such that

         A6: B is_an_arc_of (q1,q2) and

         A7: (A \/ B) = C and (A /\ B) = {q1, q2} by Th15;

        assume

         A8: A misses {p1, p2};

        then not p2 in A by ZFMISC_1: 49;

        then

         A9: p2 in B by A3, A7, XBOOLE_0:def 3;

         not p1 in A by A8, ZFMISC_1: 49;

        then p1 in B by A2, A7, XBOOLE_0:def 3;

        then

        consider P be non empty Subset of ( TOP-REAL 2) such that

         A10: P is_an_arc_of (p1,p2) and

         A11: P c= B and

         A12: P misses {q1, q2} by A1, A5, A6, A9, JORDAN16: 23;

        B c= C by A7, XBOOLE_1: 7;

        then P c= C by A11;

        hence thesis by A4, A10, A12;

      end;

    end;

    theorem :: JORDAN18:33

    p1 in C & p2 in C & q1 in C & p1 <> p2 & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 implies (p1,p2) are_neighbours_wrt (q1,q2,C) or (p1,q1) are_neighbours_wrt (p2,q2,C)

    proof

      assume that

       A1: p1 in C & p2 in C and

       A2: q1 in C and

       A3: p1 <> p2 and

       A4: q1 <> p1 and

       A5: q1 <> p2 and

       A6: q2 <> p1 & q2 <> p2;

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

       A7: P is_an_arc_of (p1,p2) and

       A8: P1 is_an_arc_of (p1,p2) and

       A9: C = (P \/ P1) and

       A10: (P /\ P1) = {p1, p2} by A1, A3, TOPREAL2: 5;

      

       A11: P c= C by A9, XBOOLE_1: 7;

      assume

       A12: for A be Subset of ( TOP-REAL 2) st A is_an_arc_of (p1,p2) & A c= C holds A meets {q1, q2};

      then

       A13: P meets {q1, q2} by A7, A9, XBOOLE_1: 7;

      

       A14: P1 c= C by A9, XBOOLE_1: 7;

      per cases by A13, ZFMISC_1: 51;

        suppose that

         A15: q1 in P and

         A16: not q2 in P;

        now

          take A = ( Segment (P,p1,p2,p1,q1));

           A17:

          now

            

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

            assume p2 in A;

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

            hence contradiction by A5, A7, JORDAN6: 55;

          end;

           LE (p1,q1,P,p1,p2) by A7, A15, JORDAN5C: 10;

          hence A is_an_arc_of (p1,q1) by A4, A7, JORDAN16: 21;

          

           A19: A c= P by JORDAN16: 2;

          hence A c= C by A11;

           not q2 in A by A16, A19;

          hence A misses {p2, q2} by A17, ZFMISC_1: 51;

        end;

        hence thesis;

      end;

        suppose that

         A20: q2 in P and

         A21: not q1 in P;

        now

          take A = ( Segment (P1,p1,p2,p1,q1));

           A22:

          now

            

             A23: A = { q where q be Point of ( TOP-REAL 2) : LE (p1,q,P1,p1,p2) & LE (q,q1,P1,p1,p2) } by JORDAN6: 26;

            assume p2 in A;

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

            hence contradiction by A5, A8, JORDAN6: 55;

          end;

          q1 in P1 by A2, A9, A21, XBOOLE_0:def 3;

          then LE (p1,q1,P1,p1,p2) by A8, JORDAN5C: 10;

          hence A is_an_arc_of (p1,q1) by A4, A8, JORDAN16: 21;

          

           A24: A c= P1 by JORDAN16: 2;

          hence A c= C by A14;

          now

            assume q2 in A;

            then q2 in {p1, p2} by A10, A20, A24, XBOOLE_0:def 4;

            hence contradiction by A6, TARSKI:def 2;

          end;

          hence A misses {p2, q2} by A22, ZFMISC_1: 51;

        end;

        hence thesis;

      end;

        suppose that

         A25: q1 in P & q2 in P;

        P1 meets {q1, q2} by A12, A8, A9, XBOOLE_1: 7;

        then q1 in P1 or q2 in P1 by ZFMISC_1: 51;

        then q1 in {p1, p2} or q2 in {p1, p2} by A10, A25, XBOOLE_0:def 4;

        hence thesis by A4, A5, A6, TARSKI:def 2;

      end;

    end;