jordan22.miz



    begin

    reserve C for Simple_closed_curve,

i for Nat;

    

     Lm1: for r be Real, X be Subset of ( TOP-REAL 2) st r in ( proj2 .: X) holds ex x be Point of ( TOP-REAL 2) st x in X & ( proj2 . x) = r

    proof

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

      assume r in ( proj2 .: X);

      then ex x be object st x in the carrier of ( TOP-REAL 2) & x in X & ( proj2 . x) = r by FUNCT_2: 64;

      hence thesis;

    end;

    theorem :: JORDAN22:1

    

     Th1: (( Upper_Appr C) . i) c= ( Cl ( RightComp ( Cage (C, 0 ))))

    proof

      

       A1: ( Upper_Arc ( L~ ( Cage (C,i)))) c= ( L~ ( Cage (C,i))) by JORDAN6: 61;

      

       A2: ( L~ ( Cage (C,i))) c= ( Cl ( RightComp ( Cage (C, 0 )))) by JORDAN1H: 46;

      (( Upper_Appr C) . i) = ( Upper_Arc ( L~ ( Cage (C,i)))) by JORDAN19:def 1;

      hence thesis by A1, A2;

    end;

    theorem :: JORDAN22:2

    

     Th2: (( Lower_Appr C) . i) c= ( Cl ( RightComp ( Cage (C, 0 ))))

    proof

      

       A1: ( Lower_Arc ( L~ ( Cage (C,i)))) c= ( L~ ( Cage (C,i))) by JORDAN6: 61;

      

       A2: ( L~ ( Cage (C,i))) c= ( Cl ( RightComp ( Cage (C, 0 )))) by JORDAN1H: 46;

      (( Lower_Appr C) . i) = ( Lower_Arc ( L~ ( Cage (C,i)))) by JORDAN19:def 2;

      hence thesis by A1, A2;

    end;

    registration

      let C be Simple_closed_curve;

      cluster ( Upper_Arc C) -> connected;

      coherence

      proof

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

        hence thesis by JORDAN6: 10;

      end;

      cluster ( Lower_Arc C) -> connected;

      coherence

      proof

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

        hence thesis by JORDAN6: 10;

      end;

    end

    theorem :: JORDAN22:3

    (( Upper_Appr C) . i) is compact connected

    proof

      ( Upper_Arc ( L~ ( Cage (C,i)))) is compact;

      hence (( Upper_Appr C) . i) is compact by JORDAN19:def 1;

      ( Upper_Arc ( L~ ( Cage (C,i)))) is connected;

      hence thesis by JORDAN19:def 1;

    end;

    theorem :: JORDAN22:4

    (( Lower_Appr C) . i) is compact connected

    proof

      ( Lower_Arc ( L~ ( Cage (C,i)))) is compact;

      hence (( Lower_Appr C) . i) is compact by JORDAN19:def 2;

      ( Lower_Arc ( L~ ( Cage (C,i)))) is connected;

      hence thesis by JORDAN19:def 2;

    end;

    registration

      let C be Simple_closed_curve;

      cluster ( North_Arc C) -> compact;

      coherence

      proof

        for i be Nat holds (( Upper_Appr C) . i) c= ( Cl ( RightComp ( Cage (C, 0 )))) by Th1;

        then ( Lim_inf ( Upper_Appr C)) is compact by KURATO_2: 26;

        hence thesis by JORDAN19:def 3;

      end;

      cluster ( South_Arc C) -> compact;

      coherence

      proof

        for i be Nat holds (( Lower_Appr C) . i) c= ( Cl ( RightComp ( Cage (C, 0 )))) by Th2;

        then ( Lim_inf ( Lower_Appr C)) is compact by KURATO_2: 26;

        hence thesis by JORDAN19:def 4;

      end;

    end

    reserve R for non empty Subset of ( TOP-REAL 2),

j,k,m,n for Nat;

    

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

    

     Lm3: 1 <= ( len ( Gauge (R,n)))

    proof

      4 <= ( len ( Gauge (R,n))) by JORDAN8: 10;

      hence thesis by XXREAL_0: 2;

    end;

    theorem :: JORDAN22:5

    

     Th5: [1, 1] in ( Indices ( Gauge (R,n)))

    proof

      

       A1: ( len ( Gauge (R,n))) = ( width ( Gauge (R,n))) by JORDAN8:def 1;

      1 <= ( len ( Gauge (R,n))) by Lm3;

      hence thesis by A1, MATRIX_0: 30;

    end;

    theorem :: JORDAN22:6

    

     Th6: [1, 2] in ( Indices ( Gauge (R,n)))

    proof

      

       A1: ( len ( Gauge (R,n))) = ( width ( Gauge (R,n))) by JORDAN8:def 1;

      

       A2: 4 <= ( len ( Gauge (R,n))) by JORDAN8: 10;

      then

       A3: 2 <= ( len ( Gauge (R,n))) by XXREAL_0: 2;

      1 <= ( len ( Gauge (R,n))) by A2, XXREAL_0: 2;

      hence thesis by A1, A3, MATRIX_0: 30;

    end;

    theorem :: JORDAN22:7

    

     Th7: [2, 1] in ( Indices ( Gauge (R,n)))

    proof

      

       A1: ( len ( Gauge (R,n))) = ( width ( Gauge (R,n))) by JORDAN8:def 1;

      

       A2: 4 <= ( len ( Gauge (R,n))) by JORDAN8: 10;

      then

       A3: 2 <= ( len ( Gauge (R,n))) by XXREAL_0: 2;

      1 <= ( len ( Gauge (R,n))) by A2, XXREAL_0: 2;

      hence thesis by A1, A3, MATRIX_0: 30;

    end;

    theorem :: JORDAN22:8

    

     Th8: for C be non vertical non horizontal compact Subset of ( TOP-REAL 2) holds m > k & [i, j] in ( Indices ( Gauge (C,k))) & [i, (j + 1)] in ( Indices ( Gauge (C,k))) implies ( dist ((( Gauge (C,m)) * (i,j)),(( Gauge (C,m)) * (i,(j + 1))))) < ( dist ((( Gauge (C,k)) * (i,j)),(( Gauge (C,k)) * (i,(j + 1)))))

    proof

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

      assume that

       A1: m > k and

       A2: [i, j] in ( Indices ( Gauge (C,k))) and

       A3: [i, (j + 1)] in ( Indices ( Gauge (C,k)));

      

       A4: ( len ( Gauge (C,k))) < ( len ( Gauge (C,m))) by A1, JORDAN1A: 29;

      

       A5: ( len ( Gauge (C,m))) = ( width ( Gauge (C,m))) by JORDAN8:def 1;

      

       A6: ( len ( Gauge (C,k))) = ( width ( Gauge (C,k))) by JORDAN8:def 1;

      j <= ( width ( Gauge (C,k))) by A2, MATRIX_0: 32;

      then

       A7: j <= ( width ( Gauge (C,m))) by A6, A5, A4, XXREAL_0: 2;

      

       A8: (( N-bound C) - ( S-bound C)) > 0 by SPRECT_1: 32, XREAL_1: 50;

      i <= ( len ( Gauge (C,k))) by A2, MATRIX_0: 32;

      then

       A9: i <= ( len ( Gauge (C,m))) by A4, XXREAL_0: 2;

      (j + 1) <= ( width ( Gauge (C,k))) by A3, MATRIX_0: 32;

      then

       A10: (j + 1) <= ( width ( Gauge (C,m))) by A6, A5, A4, XXREAL_0: 2;

      

       A11: 1 <= i by A2, MATRIX_0: 32;

      1 <= (j + 1) by NAT_1: 11;

      then

       A12: [i, (j + 1)] in ( Indices ( Gauge (C,m))) by A11, A9, A10, MATRIX_0: 30;

      1 <= j by A2, MATRIX_0: 32;

      then [i, j] in ( Indices ( Gauge (C,m))) by A11, A9, A7, MATRIX_0: 30;

      then

       A13: ( dist ((( Gauge (C,m)) * (i,j)),(( Gauge (C,m)) * (i,(j + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ m)) by A12, GOBRD14: 9;

      

       A14: (2 |^ k) > 0 by NEWTON: 83;

      ( dist ((( Gauge (C,k)) * (i,j)),(( Gauge (C,k)) * (i,(j + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ k)) by A2, A3, GOBRD14: 9;

      hence thesis by A1, A13, A14, A8, PEPIN: 66, XREAL_1: 76;

    end;

    theorem :: JORDAN22:9

    

     Th9: for C be non vertical non horizontal compact Subset of ( TOP-REAL 2) holds m > k implies ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,2)))) < ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (1,2))))

    proof

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

      assume

       A1: m > k;

       [1, (1 + 1)] in ( Indices ( Gauge (C,k))) by Th6;

      hence thesis by A1, Th5, Th8;

    end;

    theorem :: JORDAN22:10

    

     Th10: for C be non vertical non horizontal compact Subset of ( TOP-REAL 2) holds m > k & [i, j] in ( Indices ( Gauge (C,k))) & [(i + 1), j] in ( Indices ( Gauge (C,k))) implies ( dist ((( Gauge (C,m)) * (i,j)),(( Gauge (C,m)) * ((i + 1),j)))) < ( dist ((( Gauge (C,k)) * (i,j)),(( Gauge (C,k)) * ((i + 1),j))))

    proof

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

      assume that

       A1: m > k and

       A2: [i, j] in ( Indices ( Gauge (C,k))) and

       A3: [(i + 1), j] in ( Indices ( Gauge (C,k)));

      

       A4: ( len ( Gauge (C,k))) < ( len ( Gauge (C,m))) by A1, JORDAN1A: 29;

      i <= ( len ( Gauge (C,k))) by A2, MATRIX_0: 32;

      then

       A5: i <= ( len ( Gauge (C,m))) by A4, XXREAL_0: 2;

      

       A6: (( E-bound C) - ( W-bound C)) > 0 by SPRECT_1: 31, XREAL_1: 50;

      

       A7: ( len ( Gauge (C,m))) = ( width ( Gauge (C,m))) by JORDAN8:def 1;

      

       A8: ( len ( Gauge (C,k))) = ( width ( Gauge (C,k))) by JORDAN8:def 1;

      j <= ( width ( Gauge (C,k))) by A2, MATRIX_0: 32;

      then

       A9: j <= ( width ( Gauge (C,m))) by A8, A7, A4, XXREAL_0: 2;

      (i + 1) <= ( len ( Gauge (C,k))) by A3, MATRIX_0: 32;

      then

       A10: (i + 1) <= ( len ( Gauge (C,m))) by A4, XXREAL_0: 2;

      

       A11: 1 <= j by A2, MATRIX_0: 32;

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

      then

       A12: [(i + 1), j] in ( Indices ( Gauge (C,m))) by A11, A9, A10, MATRIX_0: 30;

      1 <= i by A2, MATRIX_0: 32;

      then [i, j] in ( Indices ( Gauge (C,m))) by A11, A5, A9, MATRIX_0: 30;

      then

       A13: ( dist ((( Gauge (C,m)) * (i,j)),(( Gauge (C,m)) * ((i + 1),j)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ m)) by A12, GOBRD14: 10;

      

       A14: (2 |^ k) > 0 by NEWTON: 83;

      ( dist ((( Gauge (C,k)) * (i,j)),(( Gauge (C,k)) * ((i + 1),j)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ k)) by A2, A3, GOBRD14: 10;

      hence thesis by A1, A13, A14, A6, PEPIN: 66, XREAL_1: 76;

    end;

    theorem :: JORDAN22:11

    

     Th11: for C be non vertical non horizontal compact Subset of ( TOP-REAL 2) holds m > k implies ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (2,1)))) < ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (2,1))))

    proof

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

      assume

       A1: m > k;

       [(1 + 1), 1] in ( Indices ( Gauge (C,k))) by Th7;

      hence thesis by A1, Th5, Th10;

    end;

    theorem :: JORDAN22:12

    for r,t be Real holds r > 0 & t > 0 implies ex n be Nat st i < n & ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (1,2)))) < r & ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (2,1)))) < t

    proof

      let r,t be Real;

      assume that

       A1: r > 0 and

       A2: t > 0 ;

      consider n be Nat such that 1 < n and

       A3: ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (1,2)))) < r and

       A4: ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (2,1)))) < t by A1, A2, GOBRD14: 11;

      per cases ;

        suppose

         A5: i < n;

        take n;

        thus thesis by A3, A4, A5;

      end;

        suppose

         A6: i >= n;

        take (i + 1);

        

         A7: i > n or i = n by A6, XXREAL_0: 1;

        then

         A8: ( dist ((( Gauge (C,i)) * (1,1)),(( Gauge (C,i)) * (2,1)))) <= ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (2,1)))) by Th11;

        

         A9: ( dist ((( Gauge (C,i)) * (1,1)),(( Gauge (C,i)) * (1,2)))) <= ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (1,2)))) by A7, Th9;

        thus

         A10: i < (i + 1) by NAT_1: 13;

        then ( dist ((( Gauge (C,(i + 1))) * (1,1)),(( Gauge (C,(i + 1))) * (1,2)))) < ( dist ((( Gauge (C,i)) * (1,1)),(( Gauge (C,i)) * (1,2)))) by Th9;

        then

         A11: ( dist ((( Gauge (C,(i + 1))) * (1,1)),(( Gauge (C,(i + 1))) * (1,2)))) < ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (1,2)))) by A9, XXREAL_0: 2;

        ( dist ((( Gauge (C,(i + 1))) * (1,1)),(( Gauge (C,(i + 1))) * (2,1)))) < ( dist ((( Gauge (C,i)) * (1,1)),(( Gauge (C,i)) * (2,1)))) by A10, Th11;

        then ( dist ((( Gauge (C,(i + 1))) * (1,1)),(( Gauge (C,(i + 1))) * (2,1)))) < ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (2,1)))) by A8, XXREAL_0: 2;

        hence thesis by A3, A4, A11, XXREAL_0: 2;

      end;

    end;

    theorem :: JORDAN22:13

    

     Th13: 0 < n implies ( upper_bound ( proj2 .: (( L~ ( Cage (C,n))) /\ ( LSeg ((( Gauge (C,n)) * (( Center ( Gauge (C,n))),1)),(( Gauge (C,n)) * (( Center ( Gauge (C,n))),( len ( Gauge (C,n)))))))))) = ( upper_bound ( proj2 .: (( L~ ( Cage (C,n))) /\ ( Vertical_Line ((( E-bound ( L~ ( Cage (C,n)))) + ( W-bound ( L~ ( Cage (C,n))))) / 2)))))

    proof

      set f = ( Cage (C,n)), G = ( Gauge (C,n)), c = ( Center G);

      set Y = ( proj2 .: (( L~ f) /\ ( Vertical_Line ((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2))));

      set X = ( proj2 .: (( L~ f) /\ ( LSeg ((G * (c,1)),(G * (c,( len G)))))));

      

       A1: ( len G) = ( width G) by JORDAN8:def 1;

      

       A2: 1 <= ( len G) by Lm3;

      assume 0 < n;

      

      then

       A3: ((G * (c,1)) `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by A1, A2, JORDAN1G: 35

      .= ((( W-bound ( L~ f)) + ( E-bound ( L~ f))) / 2) by JORDAN1G: 33;

      then

       A4: (G * (c,1)) in ( Vertical_Line ((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2));

      

       A5: Y is bounded_above by JORDAN21: 13;

      ( LSeg ((G * (c,1)),(G * (c,( len G))))) meets ( Upper_Arc ( L~ f)) by JORDAN1B: 31;

      then ( LSeg ((G * (c,1)),(G * (c,( len G))))) meets ( L~ f) by JORDAN6: 61, XBOOLE_1: 63;

      then

       A6: (( L~ f) /\ ( LSeg ((G * (c,1)),(G * (c,( len G)))))) is non empty by XBOOLE_0:def 7;

      then

       A7: X is non empty by Lm2, RELAT_1: 119;

      

       A8: c <= ( len G) by JORDAN1B: 13;

      1 <= c by JORDAN1B: 11;

      then

       A9: ((G * (c,1)) `1 ) = ((G * (c,( len G))) `1 ) by A1, A2, A8, GOBOARD5: 2;

      then (G * (c,( len G))) in ( Vertical_Line ((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2)) by A3;

      then

       A10: ((( L~ f) /\ ( L~ f)) /\ ( LSeg ((G * (c,1)),(G * (c,( len G)))))) c= (( L~ f) /\ ( Vertical_Line ((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2))) by A4, JORDAN1A: 13, XBOOLE_1: 26;

      then

       A11: X c= Y by RELAT_1: 123;

      then

       A12: for r be Real st r in X holds r <= ( upper_bound Y) by A5, SEQ_4:def 1;

      

       A13: Y is non empty by A11, A6, Lm2, RELAT_1: 119, XBOOLE_1: 3;

      

       A14: for s be Real st 0 < s holds ex r be Real st r in X & (( upper_bound Y) - s) < r

      proof

        let s be Real;

        assume 0 < s;

        then

        consider r be Real such that

         A15: r in Y and

         A16: (( upper_bound Y) - s) < r by A5, A13, SEQ_4:def 1;

        take r;

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

         A17: x in (( L~ f) /\ ( Vertical_Line ((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2))) and

         A18: ( proj2 . x) = r by A15, Lm1;

        

         A19: x in ( L~ f) by A17, XBOOLE_0:def 4;

        x in ( Vertical_Line ((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2)) by A17, XBOOLE_0:def 4;

        then

         A20: ((G * (c,1)) `1 ) = (x `1 ) by A3, JORDAN6: 31;

        

         A21: ( GoB f) = G by JORDAN1H: 44;

        then

         A22: ((G * (c,1)) `2 ) <= (x `2 ) by A8, A19, JORDAN1B: 11, JORDAN5D: 33;

        (x `2 ) <= ((G * (c,( len G))) `2 ) by A1, A8, A19, A21, JORDAN1B: 11, JORDAN5D: 34;

        then x in ( LSeg ((G * (c,1)),(G * (c,( len G))))) by A9, A20, A22, GOBOARD7: 7;

        then x in (( L~ f) /\ ( LSeg ((G * (c,1)),(G * (c,( len G)))))) by A19, XBOOLE_0:def 4;

        hence r in X by A18, FUNCT_2: 35;

        thus thesis by A16;

      end;

      X is bounded_above by A10, A5, RELAT_1: 123, XXREAL_2: 43;

      hence thesis by A7, A12, A14, SEQ_4:def 1;

    end;

    theorem :: JORDAN22:14

    

     Th14: 0 < n implies ( lower_bound ( proj2 .: (( L~ ( Cage (C,n))) /\ ( LSeg ((( Gauge (C,n)) * (( Center ( Gauge (C,n))),1)),(( Gauge (C,n)) * (( Center ( Gauge (C,n))),( len ( Gauge (C,n)))))))))) = ( lower_bound ( proj2 .: (( L~ ( Cage (C,n))) /\ ( Vertical_Line ((( E-bound ( L~ ( Cage (C,n)))) + ( W-bound ( L~ ( Cage (C,n))))) / 2)))))

    proof

      set f = ( Cage (C,n)), G = ( Gauge (C,n)), c = ( Center G);

      set Y = ( proj2 .: (( L~ f) /\ ( Vertical_Line ((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2))));

      set X = ( proj2 .: (( L~ f) /\ ( LSeg ((G * (c,1)),(G * (c,( len G)))))));

      

       A1: ( len G) = ( width G) by JORDAN8:def 1;

      

       A2: 1 <= ( len G) by Lm3;

      assume 0 < n;

      

      then

       A3: ((G * (c,1)) `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by A1, A2, JORDAN1G: 35

      .= ((( W-bound ( L~ f)) + ( E-bound ( L~ f))) / 2) by JORDAN1G: 33;

      then

       A4: (G * (c,1)) in ( Vertical_Line ((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2));

      

       A5: Y is bounded_below by JORDAN21: 13;

      ( LSeg ((G * (c,1)),(G * (c,( len G))))) meets ( Upper_Arc ( L~ f)) by JORDAN1B: 31;

      then ( LSeg ((G * (c,1)),(G * (c,( len G))))) meets ( L~ f) by JORDAN6: 61, XBOOLE_1: 63;

      then

       A6: (( L~ f) /\ ( LSeg ((G * (c,1)),(G * (c,( len G)))))) is non empty by XBOOLE_0:def 7;

      then

       A7: X is non empty by Lm2, RELAT_1: 119;

      

       A8: c <= ( len G) by JORDAN1B: 13;

      1 <= c by JORDAN1B: 11;

      then

       A9: ((G * (c,1)) `1 ) = ((G * (c,( len G))) `1 ) by A1, A2, A8, GOBOARD5: 2;

      then (G * (c,( len G))) in ( Vertical_Line ((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2)) by A3;

      then

       A10: ((( L~ f) /\ ( L~ f)) /\ ( LSeg ((G * (c,1)),(G * (c,( len G)))))) c= (( L~ f) /\ ( Vertical_Line ((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2))) by A4, JORDAN1A: 13, XBOOLE_1: 26;

      then

       A11: X c= Y by RELAT_1: 123;

      then

       A12: for r be Real st r in X holds ( lower_bound Y) <= r by A5, SEQ_4:def 2;

      

       A13: Y is non empty by A11, A6, Lm2, RELAT_1: 119, XBOOLE_1: 3;

      

       A14: for s be Real st 0 < s holds ex r be Real st r in X & r < (( lower_bound Y) + s)

      proof

        let s be Real;

        assume 0 < s;

        then

        consider r be Real such that

         A15: r in Y and

         A16: r < (( lower_bound Y) + s) by A5, A13, SEQ_4:def 2;

        take r;

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

         A17: x in (( L~ f) /\ ( Vertical_Line ((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2))) and

         A18: ( proj2 . x) = r by A15, Lm1;

        

         A19: x in ( L~ f) by A17, XBOOLE_0:def 4;

        x in ( Vertical_Line ((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2)) by A17, XBOOLE_0:def 4;

        then

         A20: ((G * (c,1)) `1 ) = (x `1 ) by A3, JORDAN6: 31;

        

         A21: ( GoB f) = G by JORDAN1H: 44;

        then

         A22: ((G * (c,1)) `2 ) <= (x `2 ) by A8, A19, JORDAN1B: 11, JORDAN5D: 33;

        (x `2 ) <= ((G * (c,( len G))) `2 ) by A1, A8, A19, A21, JORDAN1B: 11, JORDAN5D: 34;

        then x in ( LSeg ((G * (c,1)),(G * (c,( len G))))) by A9, A20, A22, GOBOARD7: 7;

        then x in (( L~ f) /\ ( LSeg ((G * (c,1)),(G * (c,( len G)))))) by A19, XBOOLE_0:def 4;

        hence r in X by A18, FUNCT_2: 35;

        thus thesis by A16;

      end;

      X is bounded_below by A10, A5, RELAT_1: 123, XXREAL_2: 44;

      hence thesis by A7, A12, A14, SEQ_4:def 2;

    end;

    theorem :: JORDAN22:15

     0 < n implies ( UMP ( L~ ( Cage (C,n)))) = |[((( E-bound ( L~ ( Cage (C,n)))) + ( W-bound ( L~ ( Cage (C,n))))) / 2), ( upper_bound ( proj2 .: (( L~ ( Cage (C,n))) /\ ( LSeg ((( Gauge (C,n)) * (( Center ( Gauge (C,n))),1)),(( Gauge (C,n)) * (( Center ( Gauge (C,n))),( len ( Gauge (C,n))))))))))]| by Th13;

    theorem :: JORDAN22:16

     0 < n implies ( LMP ( L~ ( Cage (C,n)))) = |[((( E-bound ( L~ ( Cage (C,n)))) + ( W-bound ( L~ ( Cage (C,n))))) / 2), ( lower_bound ( proj2 .: (( L~ ( Cage (C,n))) /\ ( LSeg ((( Gauge (C,n)) * (( Center ( Gauge (C,n))),1)),(( Gauge (C,n)) * (( Center ( Gauge (C,n))),( len ( Gauge (C,n))))))))))]| by Th14;

    theorem :: JORDAN22:17

    

     Th17: (( UMP C) `2 ) < (( UMP ( L~ ( Cage (C,n)))) `2 )

    proof

      set p = ( UMP ( L~ ( Cage (C,n)))), u = ( UMP C), w = ((( W-bound C) + ( E-bound C)) / 2);

      

       A1: (u `1 ) = w by EUCLID: 52;

      

       A2: p in ( L~ ( Cage (C,n))) by JORDAN21: 30;

      

       A3: u = |[(u `1 ), (u `2 )]| by EUCLID: 53;

      

       A4: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      

       A5: C misses ( L~ ( Cage (C,n))) by JORDAN10: 5;

      

       A6: u in C by JORDAN21: 30;

      

       A7: w = ((( W-bound ( L~ ( Cage (C,n)))) + ( E-bound ( L~ ( Cage (C,n))))) / 2) by JORDAN1G: 33;

      then

       A8: (p `1 ) = w by EUCLID: 52;

      assume

       A9: not thesis;

      per cases by A9, XXREAL_0: 1;

        suppose (u `2 ) = (p `2 );

        hence thesis by A1, A8, A4, A3, A5, A6, A2, XBOOLE_0: 3;

      end;

        suppose

         A10: (u `2 ) > (p `2 );

        

         A11: ( proj2 .: (( L~ ( Cage (C,n))) /\ ( Vertical_Line w))) is non empty bounded_above by A7, JORDAN21: 12, JORDAN21: 13;

        

         A12: (p `2 ) = ( upper_bound ( proj2 .: (( L~ ( Cage (C,n))) /\ ( Vertical_Line w)))) by A7, EUCLID: 52;

        

         A13: (( north_halfline p) \ {p}) misses ( L~ ( Cage (C,n)))

        proof

          assume (( north_halfline p) \ {p}) meets ( L~ ( Cage (C,n)));

          then

          consider x be object such that

           A14: x in (( north_halfline p) \ {p}) and

           A15: x in ( L~ ( Cage (C,n))) by XBOOLE_0: 3;

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

          

           A16: x in ( north_halfline p) by A14, XBOOLE_0:def 5;

          then

           A17: (x `2 ) >= (p `2 ) by TOPREAL1:def 10;

          

           A18: (x `1 ) = w by A8, A16, TOPREAL1:def 10;

          then x in ( Vertical_Line w);

          then

           A19: x in (( L~ ( Cage (C,n))) /\ ( Vertical_Line w)) by A15, XBOOLE_0:def 4;

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

          then (x `2 ) in ( proj2 .: (( L~ ( Cage (C,n))) /\ ( Vertical_Line w))) by A19, FUNCT_2: 35;

          then

           A20: (x `2 ) <= (p `2 ) by A12, A11, SEQ_4:def 1;

           not x in {p} by A14, XBOOLE_0:def 5;

          then x <> p by TARSKI:def 1;

          then (x `2 ) <> (p `2 ) by A8, A18, TOPREAL3: 6;

          hence contradiction by A17, A20, XXREAL_0: 1;

        end;

        (( north_halfline p) \ {p}) is convex by JORDAN21: 6;

        then

         A21: (( north_halfline p) \ {p}) c= ( UBD ( L~ ( Cage (C,n)))) or (( north_halfline p) \ {p}) c= ( BDD ( L~ ( Cage (C,n)))) by A13, JORDAN1K: 19;

        

         A22: ( UBD ( L~ ( Cage (C,n)))) c= ( UBD C) by JORDAN10: 13;

        

         A23: not u in {p} by A10, TARSKI:def 1;

        u in ( north_halfline p) by A1, A8, A10, TOPREAL1:def 10;

        then

         A24: u in (( north_halfline p) \ {p}) by A23, XBOOLE_0:def 5;

        

         A25: ( UBD C) misses C by JORDAN21: 10;

         not ( north_halfline p) is bounded by JORDAN2C: 122;

        then

         A26: not (( north_halfline p) \ {p}) is bounded by JORDAN21: 1, TOPREAL6: 90;

        ( BDD ( L~ ( Cage (C,n)))) is bounded by JORDAN2C: 106;

        then u in ( UBD ( L~ ( Cage (C,n)))) by A21, A26, A24, RLTOPSP1: 42;

        hence thesis by A6, A22, A25, XBOOLE_0: 3;

      end;

    end;

    theorem :: JORDAN22:18

    

     Th18: (( LMP C) `2 ) > (( LMP ( L~ ( Cage (C,n)))) `2 )

    proof

      set p = ( LMP ( L~ ( Cage (C,n)))), u = ( LMP C), w = ((( W-bound C) + ( E-bound C)) / 2);

      

       A1: (u `1 ) = w by EUCLID: 52;

      

       A2: p in ( L~ ( Cage (C,n))) by JORDAN21: 31;

      

       A3: u = |[(u `1 ), (u `2 )]| by EUCLID: 53;

      

       A4: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      

       A5: C misses ( L~ ( Cage (C,n))) by JORDAN10: 5;

      

       A6: u in C by JORDAN21: 31;

      

       A7: w = ((( W-bound ( L~ ( Cage (C,n)))) + ( E-bound ( L~ ( Cage (C,n))))) / 2) by JORDAN1G: 33;

      then

       A8: (p `1 ) = w by EUCLID: 52;

      assume

       A9: not thesis;

      per cases by A9, XXREAL_0: 1;

        suppose (u `2 ) = (p `2 );

        hence thesis by A1, A8, A4, A3, A5, A6, A2, XBOOLE_0: 3;

      end;

        suppose

         A10: (u `2 ) < (p `2 );

        

         A11: ( proj2 .: (( L~ ( Cage (C,n))) /\ ( Vertical_Line w))) is non empty bounded_below by A7, JORDAN21: 12, JORDAN21: 13;

        

         A12: (p `2 ) = ( lower_bound ( proj2 .: (( L~ ( Cage (C,n))) /\ ( Vertical_Line w)))) by A7, EUCLID: 52;

        

         A13: (( south_halfline p) \ {p}) misses ( L~ ( Cage (C,n)))

        proof

          assume (( south_halfline p) \ {p}) meets ( L~ ( Cage (C,n)));

          then

          consider x be object such that

           A14: x in (( south_halfline p) \ {p}) and

           A15: x in ( L~ ( Cage (C,n))) by XBOOLE_0: 3;

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

          

           A16: x in ( south_halfline p) by A14, XBOOLE_0:def 5;

          then

           A17: (x `2 ) <= (p `2 ) by TOPREAL1:def 12;

          

           A18: (x `1 ) = w by A8, A16, TOPREAL1:def 12;

          then x in ( Vertical_Line w);

          then

           A19: x in (( L~ ( Cage (C,n))) /\ ( Vertical_Line w)) by A15, XBOOLE_0:def 4;

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

          then (x `2 ) in ( proj2 .: (( L~ ( Cage (C,n))) /\ ( Vertical_Line w))) by A19, FUNCT_2: 35;

          then

           A20: (x `2 ) >= (p `2 ) by A12, A11, SEQ_4:def 2;

           not x in {p} by A14, XBOOLE_0:def 5;

          then x <> p by TARSKI:def 1;

          then (x `2 ) <> (p `2 ) by A8, A18, TOPREAL3: 6;

          hence contradiction by A17, A20, XXREAL_0: 1;

        end;

        (( south_halfline p) \ {p}) is convex by JORDAN21: 7;

        then

         A21: (( south_halfline p) \ {p}) c= ( UBD ( L~ ( Cage (C,n)))) or (( south_halfline p) \ {p}) c= ( BDD ( L~ ( Cage (C,n)))) by A13, JORDAN1K: 19;

        

         A22: ( UBD ( L~ ( Cage (C,n)))) c= ( UBD C) by JORDAN10: 13;

        

         A23: not u in {p} by A10, TARSKI:def 1;

        u in ( south_halfline p) by A1, A8, A10, TOPREAL1:def 12;

        then

         A24: u in (( south_halfline p) \ {p}) by A23, XBOOLE_0:def 5;

        

         A25: ( UBD C) misses C by JORDAN21: 10;

         not ( south_halfline p) is bounded by JORDAN2C: 123;

        then

         A26: not (( south_halfline p) \ {p}) is bounded by JORDAN21: 1, TOPREAL6: 90;

        ( BDD ( L~ ( Cage (C,n)))) is bounded by JORDAN2C: 106;

        then u in ( UBD ( L~ ( Cage (C,n)))) by A21, A26, A24, RLTOPSP1: 42;

        hence thesis by A6, A22, A25, XBOOLE_0: 3;

      end;

    end;

    theorem :: JORDAN22:19

    

     Th19: 0 < n implies ex i be Nat st 1 <= i & i <= ( len ( Gauge (C,n))) & ( UMP ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (( Center ( Gauge (C,n))),i))

    proof

      set f = ( Cage (C,n)), G = ( Gauge (C,n)), w = ( Center G);

      

       A1: f is_sequence_on G by JORDAN9:def 1;

      

       A2: ( len G) = ( width G) by JORDAN8:def 1;

      ( LSeg ((G * (w,1)),(G * (w,( len G))))) meets ( Upper_Arc ( L~ f)) by JORDAN1B: 31;

      then

       A3: ( LSeg ((G * (w,1)),(G * (w,( len G))))) meets ( L~ f) by JORDAN6: 61, XBOOLE_1: 63;

      

       A4: w <= ( len G) by JORDAN1B: 13;

      assume

       A5: 0 < n;

      then ( UMP ( L~ f)) = |[((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2), ( upper_bound ( proj2 .: (( L~ f) /\ ( LSeg ((G * (w,1)),(G * (w,( len G))))))))]| by Th13;

      then

       A6: (( UMP ( L~ f)) `2 ) = ( upper_bound ( proj2 .: (( L~ f) /\ ( LSeg ((G * (w,1)),(G * (w,( len G)))))))) by EUCLID: 52;

      

       A7: 1 <= ( len G) by Lm3;

      

       A8: 1 <= w by JORDAN1B: 11;

      then

       A9: [w, ( len G)] in ( Indices G) by A2, A7, A4, MATRIX_0: 30;

       [w, 1] in ( Indices G) by A2, A7, A8, A4, MATRIX_0: 30;

      then

      consider i such that

       A10: 1 <= i and

       A11: i <= ( len G) and

       A12: ((G * (w,i)) `2 ) = ( upper_bound ( proj2 .: (( LSeg ((G * (w,1)),(G * (w,( len G))))) /\ ( L~ f)))) by A1, A3, A7, A9, JORDAN1F: 2;

      

       A13: (( UMP ( L~ f)) `1 ) = ((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2) by EUCLID: 52;

      take i;

      thus 1 <= i & i <= ( len G) by A10, A11;

      ((G * (w,i)) `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by A5, A2, A10, A11, JORDAN1G: 35;

      then (( UMP ( L~ f)) `1 ) = ((G * (w,i)) `1 ) by A13, JORDAN1G: 33;

      hence thesis by A12, A6, TOPREAL3: 6;

    end;

    theorem :: JORDAN22:20

    

     Th20: 0 < n implies ex i be Nat st 1 <= i & i <= ( len ( Gauge (C,n))) & ( LMP ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (( Center ( Gauge (C,n))),i))

    proof

      set f = ( Cage (C,n)), G = ( Gauge (C,n)), w = ( Center G);

      

       A1: f is_sequence_on G by JORDAN9:def 1;

      

       A2: ( len G) = ( width G) by JORDAN8:def 1;

      ( LSeg ((G * (w,1)),(G * (w,( len G))))) meets ( Upper_Arc ( L~ f)) by JORDAN1B: 31;

      then

       A3: ( LSeg ((G * (w,1)),(G * (w,( len G))))) meets ( L~ f) by JORDAN6: 61, XBOOLE_1: 63;

      

       A4: w <= ( len G) by JORDAN1B: 13;

      assume

       A5: 0 < n;

      then ( LMP ( L~ f)) = |[((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2), ( lower_bound ( proj2 .: (( L~ f) /\ ( LSeg ((G * (w,1)),(G * (w,( len G))))))))]| by Th14;

      then

       A6: (( LMP ( L~ f)) `2 ) = ( lower_bound ( proj2 .: (( L~ f) /\ ( LSeg ((G * (w,1)),(G * (w,( len G)))))))) by EUCLID: 52;

      

       A7: 1 <= ( len G) by Lm3;

      

       A8: 1 <= w by JORDAN1B: 11;

      then

       A9: [w, ( len G)] in ( Indices G) by A2, A7, A4, MATRIX_0: 30;

       [w, 1] in ( Indices G) by A2, A7, A8, A4, MATRIX_0: 30;

      then

      consider i such that

       A10: 1 <= i and

       A11: i <= ( len G) and

       A12: ((G * (w,i)) `2 ) = ( lower_bound ( proj2 .: (( LSeg ((G * (w,1)),(G * (w,( len G))))) /\ ( L~ f)))) by A1, A3, A7, A9, JORDAN1F: 1;

      

       A13: (( LMP ( L~ f)) `1 ) = ((( E-bound ( L~ f)) + ( W-bound ( L~ f))) / 2) by EUCLID: 52;

      take i;

      thus 1 <= i & i <= ( len G) by A10, A11;

      ((G * (w,i)) `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by A5, A2, A10, A11, JORDAN1G: 35;

      then (( LMP ( L~ f)) `1 ) = ((G * (w,i)) `1 ) by A13, JORDAN1G: 33;

      hence thesis by A12, A6, TOPREAL3: 6;

    end;

    theorem :: JORDAN22:21

    

     Th21: 0 < n implies ( UMP ( L~ ( Cage (C,n)))) = ( UMP ( Upper_Arc ( L~ ( Cage (C,n)))))

    proof

      set f = ( Cage (C,n));

      set w = ((( E-bound C) + ( W-bound C)) / 2);

      

       A1: ( Upper_Arc ( L~ f)) c= ( L~ f) by JORDAN6: 61;

      

       A2: (( W-bound C) + ( E-bound C)) = (( W-bound ( L~ f)) + ( E-bound ( L~ f))) by JORDAN1G: 33;

      

       A3: ( E-bound ( L~ f)) = ( E-bound ( Upper_Arc ( L~ f))) by JORDAN21: 18;

      

       A4: ( W-bound ( L~ f)) = ( W-bound ( Upper_Arc ( L~ f))) by JORDAN21: 17;

      assume

       A5: 0 < n;

      then

       A6: ( 0 + 1) <= n by NAT_1: 13;

      then

       A7: ((n -' 1) + 1) = n by XREAL_1: 235;

       A8:

      now

        

         A9: ( Center ( Gauge (C,1))) <= ( len ( Gauge (C,1))) by JORDAN1B: 13;

        

         A10: ( Center ( Gauge (C,n))) <= ( len ( Gauge (C,n))) by JORDAN1B: 13;

        

         A11: (( Upper_Arc ( L~ f)) \/ ( Lower_Arc ( L~ f))) = ( L~ f) by JORDAN6:def 9;

        assume

         A12: not ( UMP ( L~ f)) in ( Upper_Arc ( L~ f));

        ( UMP ( L~ f)) in ( L~ f) by JORDAN21: 30;

        then

         A13: ( UMP ( L~ f)) in ( Lower_Arc ( L~ f)) by A12, A11, XBOOLE_0:def 3;

        

         A14: ( len ( Gauge (C,n))) = ( width ( Gauge (C,n))) by JORDAN8:def 1;

        

         A15: 1 <= ( Center ( Gauge (C,n))) by JORDAN1B: 11;

        consider j be Nat such that

         A16: 1 <= j and

         A17: j <= ( len ( Gauge (C,n))) and

         A18: ( UMP ( L~ f)) = (( Gauge (C,n)) * (( Center ( Gauge (C,n))),j)) by A5, Th19;

        set a = (( Gauge (C,1)) * (( Center ( Gauge (C,1))),( len ( Gauge (C,1))))), b = (( Gauge (C,n)) * (( Center ( Gauge (C,n))),j)), L = ( LSeg (a,b));

        ( len ( Gauge (C,1))) = ( width ( Gauge (C,1))) by JORDAN8:def 1;

        then L meets ( Upper_Arc ( L~ f)) by A7, A13, A16, A17, A18, A14, JORDAN19: 5;

        then

        consider x be object such that

         A19: x in L and

         A20: x in ( Upper_Arc ( L~ f)) by XBOOLE_0: 3;

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

        

         A21: a in L by RLTOPSP1: 68;

        

         A22: 1 <= ( len ( Gauge (C,1))) by Lm3;

        then

         A23: (a `1 ) = w by JORDAN1A: 38;

        then

         A24: (b `1 ) = w by A5, A16, A17, A22, JORDAN1A: 36;

        then L is vertical by A23, SPPOL_1: 16;

        then

         A25: (x `1 ) = w by A19, A23, A21, SPPOL_1:def 3;

        then x in ( Vertical_Line w);

        then

         A26: x in (( Upper_Arc ( L~ f)) /\ ( Vertical_Line w)) by A20, XBOOLE_0:def 4;

        then

         A27: (( UMP ( Upper_Arc ( L~ f))) `2 ) >= (x `2 ) by A2, A4, A3, JORDAN21: 28;

        1 <= ( Center ( Gauge (C,1))) by JORDAN1B: 11;

        then

         A28: ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),( len ( Gauge (C,1))))) `2 ) >= ((( Gauge (C,n)) * (( Center ( Gauge (C,n))),( len ( Gauge (C,n))))) `2 ) by A6, A15, A10, A9, JORDAN1A: 40;

        ( len ( Gauge (C,n))) = ( width ( Gauge (C,n))) by JORDAN8:def 1;

        then ((( Gauge (C,n)) * (( Center ( Gauge (C,n))),( len ( Gauge (C,n))))) `2 ) >= ((( Gauge (C,n)) * (( Center ( Gauge (C,n))),j)) `2 ) by A16, A17, A15, A10, SPRECT_3: 12;

        then (a `2 ) >= (b `2 ) by A28, XXREAL_0: 2;

        then

         A29: (x `2 ) >= (b `2 ) by A19, TOPREAL1: 4;

        (( UMP ( L~ f)) `2 ) >= (( UMP ( Upper_Arc ( L~ f))) `2 ) by A1, A2, A4, A3, A26, JORDAN21: 13, JORDAN21: 43;

        then (b `2 ) >= (x `2 ) by A18, A27, XXREAL_0: 2;

        then (b `2 ) = (x `2 ) by A29, XXREAL_0: 1;

        hence contradiction by A12, A18, A20, A24, A25, TOPREAL3: 6;

      end;

      ( proj2 .: (( L~ f) /\ ( Vertical_Line w))) is bounded_above by A2, JORDAN21: 13;

      hence thesis by A1, A2, A4, A3, A8, JORDAN21: 21, JORDAN21: 45;

    end;

    theorem :: JORDAN22:22

    

     Th22: 0 < n implies ( LMP ( L~ ( Cage (C,n)))) = ( LMP ( Lower_Arc ( L~ ( Cage (C,n)))))

    proof

      set f = ( Cage (C,n));

      set w = ((( E-bound C) + ( W-bound C)) / 2);

      

       A1: ( Lower_Arc ( L~ f)) c= ( L~ f) by JORDAN6: 61;

      

       A2: (( W-bound C) + ( E-bound C)) = (( W-bound ( L~ f)) + ( E-bound ( L~ f))) by JORDAN1G: 33;

      

       A3: ( E-bound ( L~ f)) = ( E-bound ( Lower_Arc ( L~ f))) by JORDAN21: 20;

      

       A4: ( W-bound ( L~ f)) = ( W-bound ( Lower_Arc ( L~ f))) by JORDAN21: 19;

      assume

       A5: 0 < n;

      then

       A6: ( 0 + 1) <= n by NAT_1: 13;

      then

       A7: ((n -' 1) + 1) = n by XREAL_1: 235;

       A8:

      now

        

         A9: ( Center ( Gauge (C,1))) <= ( len ( Gauge (C,1))) by JORDAN1B: 13;

        

         A10: ( len ( Gauge (C,n))) = ( width ( Gauge (C,n))) by JORDAN8:def 1;

        

         A11: (( Upper_Arc ( L~ f)) \/ ( Lower_Arc ( L~ f))) = ( L~ f) by JORDAN6:def 9;

        assume

         A12: not ( LMP ( L~ f)) in ( Lower_Arc ( L~ f));

        consider j be Nat such that

         A13: 1 <= j and

         A14: j <= ( len ( Gauge (C,n))) and

         A15: ( LMP ( L~ f)) = (( Gauge (C,n)) * (( Center ( Gauge (C,n))),j)) by A5, Th20;

        set a = (( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)), b = (( Gauge (C,n)) * (( Center ( Gauge (C,n))),j)), L = ( LSeg (a,b));

        

         A16: a in L by RLTOPSP1: 68;

        ( LMP ( L~ f)) in ( L~ f) by JORDAN21: 31;

        then ( LMP ( L~ f)) in ( Upper_Arc ( L~ f)) by A12, A11, XBOOLE_0:def 3;

        then L meets ( Lower_Arc ( L~ f)) by A7, A13, A14, A15, A10, JORDAN1J: 62;

        then

        consider x be object such that

         A17: x in L and

         A18: x in ( Lower_Arc ( L~ f)) by XBOOLE_0: 3;

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

        

         A19: 1 <= ( Center ( Gauge (C,n))) by JORDAN1B: 11;

        

         A20: 1 <= ( len ( Gauge (C,1))) by Lm3;

        then

         A21: (a `1 ) = w by JORDAN1A: 38;

        then

         A22: (b `1 ) = w by A5, A13, A14, A20, JORDAN1A: 36;

        then L is vertical by A21, SPPOL_1: 16;

        then

         A23: (x `1 ) = w by A17, A21, A16, SPPOL_1:def 3;

        then x in ( Vertical_Line w);

        then

         A24: x in (( Lower_Arc ( L~ f)) /\ ( Vertical_Line w)) by A18, XBOOLE_0:def 4;

        then

         A25: (( LMP ( Lower_Arc ( L~ f))) `2 ) <= (x `2 ) by A2, A4, A3, JORDAN21: 29;

        

         A26: ( Center ( Gauge (C,n))) <= ( len ( Gauge (C,n))) by JORDAN1B: 13;

        1 <= ( Center ( Gauge (C,1))) by JORDAN1B: 11;

        then

         A27: ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)) `2 ) <= ((( Gauge (C,n)) * (( Center ( Gauge (C,n))),1)) `2 ) by A6, A19, A26, A9, JORDAN1A: 43;

        ((( Gauge (C,n)) * (( Center ( Gauge (C,n))),1)) `2 ) <= ((( Gauge (C,n)) * (( Center ( Gauge (C,n))),j)) `2 ) by A13, A14, A10, A19, A26, SPRECT_3: 12;

        then (a `2 ) <= (b `2 ) by A27, XXREAL_0: 2;

        then

         A28: (x `2 ) <= (b `2 ) by A17, TOPREAL1: 4;

        (( LMP ( L~ f)) `2 ) <= (( LMP ( Lower_Arc ( L~ f))) `2 ) by A1, A2, A4, A3, A24, JORDAN21: 13, JORDAN21: 44;

        then (b `2 ) <= (x `2 ) by A15, A25, XXREAL_0: 2;

        then (b `2 ) = (x `2 ) by A28, XXREAL_0: 1;

        hence contradiction by A12, A15, A18, A22, A23, TOPREAL3: 6;

      end;

      ( proj2 .: (( L~ f) /\ ( Vertical_Line w))) is bounded_below by A2, JORDAN21: 13;

      hence thesis by A1, A2, A4, A3, A8, JORDAN21: 22, JORDAN21: 46;

    end;

    theorem :: JORDAN22:23

    

     Th23: 0 < n implies (( UMP C) `2 ) < (( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) `2 )

    proof

      assume 0 < n;

      then ( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) = ( UMP ( L~ ( Cage (C,n)))) by Th21;

      hence thesis by Th17;

    end;

    theorem :: JORDAN22:24

    

     Th24: 0 < n implies (( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) `2 ) < (( LMP C) `2 )

    proof

      assume 0 < n;

      then ( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) = ( LMP ( L~ ( Cage (C,n)))) by Th22;

      hence thesis by Th18;

    end;

    theorem :: JORDAN22:25

    

     Th25: i <= j implies (( UMP ( L~ ( Cage (C,j)))) `2 ) <= (( UMP ( L~ ( Cage (C,i)))) `2 )

    proof

      set w = ((( E-bound C) + ( W-bound C)) / 2), ui = ( UMP ( L~ ( Cage (C,i)))), uj = ( UMP ( L~ ( Cage (C,j))));

      assume i <= j;

      then

       A1: ( LeftComp ( Cage (C,i))) c= ( LeftComp ( Cage (C,j))) by JORDAN1H: 47;

      

       A2: (( W-bound ( L~ ( Cage (C,j)))) + ( E-bound ( L~ ( Cage (C,j))))) = (( W-bound C) + ( E-bound C)) by JORDAN1G: 33;

      then

       A3: (uj `2 ) = ( upper_bound ( proj2 .: (( L~ ( Cage (C,j))) /\ ( Vertical_Line w)))) by EUCLID: 52;

      assume (( UMP ( L~ ( Cage (C,j)))) `2 ) > (( UMP ( L~ ( Cage (C,i)))) `2 );

      then

       A4: ((uj `2 ) - (ui `2 )) > 0 by XREAL_1: 50;

      

       A5: (( W-bound ( L~ ( Cage (C,i)))) + ( E-bound ( L~ ( Cage (C,i))))) = (( W-bound C) + ( E-bound C)) by JORDAN1G: 33;

      then

       A6: (ui `2 ) = ( upper_bound ( proj2 .: (( L~ ( Cage (C,i))) /\ ( Vertical_Line w)))) by EUCLID: 52;

      

       A7: ( proj2 .: (( L~ ( Cage (C,i))) /\ ( Vertical_Line w))) is non empty bounded_above by A5, JORDAN21: 12, JORDAN21: 13;

      ( proj2 .: (( L~ ( Cage (C,j))) /\ ( Vertical_Line w))) is non empty bounded_above by A2, JORDAN21: 12, JORDAN21: 13;

      then

      consider r be Real such that

       A8: r in ( proj2 .: (( L~ ( Cage (C,j))) /\ ( Vertical_Line w))) and

       A9: (( upper_bound ( proj2 .: (( L~ ( Cage (C,j))) /\ ( Vertical_Line w)))) - ((uj `2 ) - (ui `2 ))) < r by A4, SEQ_4:def 1;

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

       A10: x in (( L~ ( Cage (C,j))) /\ ( Vertical_Line w)) and

       A11: ( proj2 . x) = r by A8, Lm1;

      

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

      ( north_halfline x) misses ( L~ ( Cage (C,i)))

      proof

        

         A13: x in ( Vertical_Line w) by A10, XBOOLE_0:def 4;

        assume ( north_halfline x) meets ( L~ ( Cage (C,i)));

        then

        consider y be object such that

         A14: y in ( north_halfline x) and

         A15: y in ( L~ ( Cage (C,i))) by XBOOLE_0: 3;

        reconsider y as Point of ( TOP-REAL 2) by A15;

        (y `1 ) = (x `1 ) by A14, TOPREAL1:def 10

        .= w by A13, JORDAN6: 31;

        then y in ( Vertical_Line w);

        then

         A16: y in (( L~ ( Cage (C,i))) /\ ( Vertical_Line w)) by A15, XBOOLE_0:def 4;

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

        then (y `2 ) in ( proj2 .: (( L~ ( Cage (C,i))) /\ ( Vertical_Line w))) by A16, FUNCT_2: 35;

        then

         A17: (y `2 ) <= (ui `2 ) by A6, A7, SEQ_4:def 1;

        (y `2 ) >= (x `2 ) by A14, TOPREAL1:def 10;

        hence contradiction by A3, A9, A12, A17, XXREAL_0: 2;

      end;

      then

       A18: ( north_halfline x) c= ( UBD ( L~ ( Cage (C,i)))) by JORDAN2C: 129;

      x in ( north_halfline x) by TOPREAL1: 38;

      then x in ( UBD ( L~ ( Cage (C,i)))) by A18;

      then

       A19: x in ( LeftComp ( Cage (C,i))) by GOBRD14: 36;

      x in ( L~ ( Cage (C,j))) by A10, XBOOLE_0:def 4;

      then ( LeftComp ( Cage (C,j))) meets ( L~ ( Cage (C,j))) by A1, A19, XBOOLE_0: 3;

      hence thesis by SPRECT_3: 26;

    end;

    theorem :: JORDAN22:26

    

     Th26: i <= j implies (( LMP ( L~ ( Cage (C,i)))) `2 ) <= (( LMP ( L~ ( Cage (C,j)))) `2 )

    proof

      set w = ((( E-bound C) + ( W-bound C)) / 2), ui = ( LMP ( L~ ( Cage (C,i)))), uj = ( LMP ( L~ ( Cage (C,j))));

      assume i <= j;

      then

       A1: ( LeftComp ( Cage (C,i))) c= ( LeftComp ( Cage (C,j))) by JORDAN1H: 47;

      

       A2: (( W-bound ( L~ ( Cage (C,j)))) + ( E-bound ( L~ ( Cage (C,j))))) = (( W-bound C) + ( E-bound C)) by JORDAN1G: 33;

      then

       A3: (uj `2 ) = ( lower_bound ( proj2 .: (( L~ ( Cage (C,j))) /\ ( Vertical_Line w)))) by EUCLID: 52;

      assume (( LMP ( L~ ( Cage (C,i)))) `2 ) > (( LMP ( L~ ( Cage (C,j)))) `2 );

      then

       A4: ((ui `2 ) - (uj `2 )) > 0 by XREAL_1: 50;

      

       A5: (( W-bound ( L~ ( Cage (C,i)))) + ( E-bound ( L~ ( Cage (C,i))))) = (( W-bound C) + ( E-bound C)) by JORDAN1G: 33;

      then

       A6: (ui `2 ) = ( lower_bound ( proj2 .: (( L~ ( Cage (C,i))) /\ ( Vertical_Line w)))) by EUCLID: 52;

      

       A7: ( proj2 .: (( L~ ( Cage (C,i))) /\ ( Vertical_Line w))) is non empty bounded_below by A5, JORDAN21: 12, JORDAN21: 13;

      ( proj2 .: (( L~ ( Cage (C,j))) /\ ( Vertical_Line w))) is non empty bounded_below by A2, JORDAN21: 12, JORDAN21: 13;

      then

      consider r be Real such that

       A8: r in ( proj2 .: (( L~ ( Cage (C,j))) /\ ( Vertical_Line w))) and

       A9: r < (( lower_bound ( proj2 .: (( L~ ( Cage (C,j))) /\ ( Vertical_Line w)))) + ((ui `2 ) - (uj `2 ))) by A4, SEQ_4:def 2;

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

       A10: x in (( L~ ( Cage (C,j))) /\ ( Vertical_Line w)) and

       A11: ( proj2 . x) = r by A8, Lm1;

      

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

      ( south_halfline x) misses ( L~ ( Cage (C,i)))

      proof

        

         A13: x in ( Vertical_Line w) by A10, XBOOLE_0:def 4;

        assume ( south_halfline x) meets ( L~ ( Cage (C,i)));

        then

        consider y be object such that

         A14: y in ( south_halfline x) and

         A15: y in ( L~ ( Cage (C,i))) by XBOOLE_0: 3;

        reconsider y as Point of ( TOP-REAL 2) by A15;

        (y `1 ) = (x `1 ) by A14, TOPREAL1:def 12

        .= w by A13, JORDAN6: 31;

        then y in ( Vertical_Line w);

        then

         A16: y in (( L~ ( Cage (C,i))) /\ ( Vertical_Line w)) by A15, XBOOLE_0:def 4;

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

        then (y `2 ) in ( proj2 .: (( L~ ( Cage (C,i))) /\ ( Vertical_Line w))) by A16, FUNCT_2: 35;

        then

         A17: (y `2 ) >= (ui `2 ) by A6, A7, SEQ_4:def 2;

        (y `2 ) <= (x `2 ) by A14, TOPREAL1:def 12;

        hence contradiction by A3, A9, A12, A17, XXREAL_0: 2;

      end;

      then

       A18: ( south_halfline x) c= ( UBD ( L~ ( Cage (C,i)))) by JORDAN2C: 128;

      x in ( south_halfline x) by TOPREAL1: 38;

      then x in ( UBD ( L~ ( Cage (C,i)))) by A18;

      then

       A19: x in ( LeftComp ( Cage (C,i))) by GOBRD14: 36;

      x in ( L~ ( Cage (C,j))) by A10, XBOOLE_0:def 4;

      then ( LeftComp ( Cage (C,j))) meets ( L~ ( Cage (C,j))) by A1, A19, XBOOLE_0: 3;

      hence thesis by SPRECT_3: 26;

    end;

    theorem :: JORDAN22:27

    

     Th27: 0 < i & i <= j implies (( UMP ( Upper_Arc ( L~ ( Cage (C,j))))) `2 ) <= (( UMP ( Upper_Arc ( L~ ( Cage (C,i))))) `2 )

    proof

      assume that

       A1: 0 < i and

       A2: i <= j;

      

       A3: (( UMP ( Upper_Arc ( L~ ( Cage (C,i))))) `2 ) = (( UMP ( L~ ( Cage (C,i)))) `2 ) by A1, Th21;

      (( UMP ( Upper_Arc ( L~ ( Cage (C,j))))) `2 ) = (( UMP ( L~ ( Cage (C,j)))) `2 ) by A1, A2, Th21;

      hence thesis by A2, A3, Th25;

    end;

    theorem :: JORDAN22:28

    

     Th28: 0 < i & i <= j implies (( LMP ( Lower_Arc ( L~ ( Cage (C,i))))) `2 ) <= (( LMP ( Lower_Arc ( L~ ( Cage (C,j))))) `2 )

    proof

      assume that

       A1: 0 < i and

       A2: i <= j;

      

       A3: (( LMP ( Lower_Arc ( L~ ( Cage (C,i))))) `2 ) = (( LMP ( L~ ( Cage (C,i)))) `2 ) by A1, Th22;

      (( LMP ( Lower_Arc ( L~ ( Cage (C,j))))) `2 ) = (( LMP ( L~ ( Cage (C,j)))) `2 ) by A1, A2, Th22;

      hence thesis by A2, A3, Th26;

    end;

    begin

    theorem :: JORDAN22:29

    

     Th29: ( W-min C) in ( North_Arc C)

    proof

      reconsider w = ( W-min C) as Point of ( Euclid 2) by EUCLID: 67;

      

       A1: for r be Real st r > 0 holds ex k be Nat st for m be Nat st m > k holds (( Upper_Appr C) . m) meets ( Ball (w,r))

      proof

        let r be Real;

        assume r > 0 ;

        then (r / 2) > 0 ;

        then

        consider k be Nat such that 1 < k and

         A2: ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (1,2)))) < (r / 2) and

         A3: ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (2,1)))) < (r / 2) by GOBRD14: 11;

        reconsider k as Nat;

        take k;

        let m be Nat such that

         A4: m > k;

        ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,2)))) < ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (1,2)))) by A4, Th9;

        then

         A5: ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,2)))) < (r / 2) by A2, XXREAL_0: 2;

        ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (2,1)))) < ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (2,1)))) by A4, Th11;

        then

         A6: ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (2,1)))) < (r / 2) by A3, XXREAL_0: 2;

        

         A7: (1 + 1) <= ( len ( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m))))))) by GOBOARD7: 34, XXREAL_0: 2;

        then

         A8: (( left_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1)) /\ ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1))) = ( LSeg (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1)) by GOBOARD5: 31;

        reconsider p = ( W-min ( L~ ( Cage (C,m)))) as Point of ( Euclid 2) by EUCLID: 67;

        

         A9: ( W-min ( L~ ( Cage (C,m)))) in ( Upper_Arc ( L~ ( Cage (C,m)))) by JORDAN7: 1;

        ( Cage (C,m)) is_sequence_on ( Gauge (C,m)) by JORDAN9:def 1;

        then

         A10: ( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))) is_sequence_on ( Gauge (C,m)) by REVROT_1: 34;

        ( W-min ( L~ ( Cage (C,m)))) in ( rng ( Cage (C,m))) by SPRECT_2: 43;

        then

         A11: ( W-min ( L~ ( Cage (C,m)))) = (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))) /. 1) by FINSEQ_6: 92;

        then (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))) /. 1) = ( W-min ( L~ ( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))))) by REVROT_1: 33;

        then

        consider i,j be Nat such that

         A12: [i, j] in ( Indices ( Gauge (C,m))) and

         A13: [i, (j + 1)] in ( Indices ( Gauge (C,m))) and

         A14: (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))) /. 1) = (( Gauge (C,m)) * (i,j)) and

         A15: (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))) /. (1 + 1)) = (( Gauge (C,m)) * (i,(j + 1))) by A7, A10, JORDAN1I: 21;

        

         A16: 1 <= j by A12, MATRIX_0: 32;

        i < ( len ( Gauge (C,m))) by A7, A10, A12, A13, A14, A15, JORDAN1I: 14;

        then

         A17: (i + 1) <= ( len ( Gauge (C,m))) by NAT_1: 13;

        

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

        j <= ( width ( Gauge (C,m))) by A12, MATRIX_0: 32;

        then

         A19: [(i + 1), j] in ( Indices ( Gauge (C,m))) by A16, A18, A17, MATRIX_0: 30;

         [(1 + 1), 1] in ( Indices ( Gauge (C,m))) by Th7;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * ((1 + 1),1)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ m)) by Th5, GOBRD14: 10;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * ((1 + 1),1)))) = ( dist ((( Gauge (C,m)) * (i,j)),(( Gauge (C,m)) * ((i + 1),j)))) by A12, A19, GOBRD14: 10;

        then

         A20: (((( Gauge (C,m)) * ((i + 1),j)) `1 ) - ((( Gauge (C,m)) * (i,j)) `1 )) < (r / 2) by A12, A19, A6, GOBRD14: 5;

         [1, (1 + 1)] in ( Indices ( Gauge (C,m))) by Th6;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,(1 + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ m)) by Th5, GOBRD14: 9;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,(1 + 1))))) = ( dist ((( Gauge (C,m)) * (i,j)),(( Gauge (C,m)) * (i,(j + 1))))) by A12, A13, GOBRD14: 9;

        then (((( Gauge (C,m)) * (i,(j + 1))) `2 ) - ((( Gauge (C,m)) * (i,j)) `2 )) < (r / 2) by A12, A13, A5, GOBRD14: 6;

        then

         A21: ((((( Gauge (C,m)) * ((i + 1),j)) `1 ) - ((( Gauge (C,m)) * (i,j)) `1 )) + (((( Gauge (C,m)) * (i,(j + 1))) `2 ) - ((( Gauge (C,m)) * (i,j)) `2 ))) < ((r / 2) + (r / 2)) by A20, XREAL_1: 8;

        

         A22: 1 <= i by A12, MATRIX_0: 32;

        ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1)) = ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1,( GoB ( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m))))))))) by A7, JORDAN1H: 23

        .= ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1,( GoB ( Cage (C,m))))) by REVROT_1: 28

        .= ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1,( Gauge (C,m)))) by JORDAN1H: 44;

        then

         A23: ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1)) = ( cell (( Gauge (C,m)),i,j)) by A7, A10, A12, A13, A14, A15, GOBRD13: 22;

        

         A24: (j + 1) <= ( width ( Gauge (C,m))) by A13, MATRIX_0: 32;

        (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))) /. 1) in ( LSeg (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1)) by A7, TOPREAL1: 21;

        then

         A25: ( W-min ( L~ ( Cage (C,m)))) in ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1)) by A11, A8, XBOOLE_0:def 4;

        then

         A26: ((( Gauge (C,m)) * (i,j)) `1 ) <= (( W-min ( L~ ( Cage (C,m)))) `1 ) by A23, A22, A16, A24, A17, JORDAN9: 17;

        

         A27: ( W-min C) in ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1)) by JORDAN1I: 6;

        then

         A28: (( W-min C) `1 ) <= ((( Gauge (C,m)) * ((i + 1),j)) `1 ) by A23, A22, A16, A24, A17, JORDAN9: 17;

        

         A29: ((( Gauge (C,m)) * (i,j)) `2 ) <= (( W-min ( L~ ( Cage (C,m)))) `2 ) by A25, A23, A22, A16, A24, A17, JORDAN9: 17;

        

         A30: (( W-min ( L~ ( Cage (C,m)))) `1 ) <= ((( Gauge (C,m)) * ((i + 1),j)) `1 ) by A25, A23, A22, A16, A24, A17, JORDAN9: 17;

        

         A31: (( W-min ( L~ ( Cage (C,m)))) `2 ) <= ((( Gauge (C,m)) * (i,(j + 1))) `2 ) by A25, A23, A22, A16, A24, A17, JORDAN9: 17;

        

         A32: (( W-min C) `2 ) <= ((( Gauge (C,m)) * (i,(j + 1))) `2 ) by A27, A23, A22, A16, A24, A17, JORDAN9: 17;

        

         A33: ((( Gauge (C,m)) * (i,j)) `2 ) <= (( W-min C) `2 ) by A27, A23, A22, A16, A24, A17, JORDAN9: 17;

        ((( Gauge (C,m)) * (i,j)) `1 ) <= (( W-min C) `1 ) by A27, A23, A22, A16, A24, A17, JORDAN9: 17;

        then ( dist (( W-min C),( W-min ( L~ ( Cage (C,m)))))) <= ((((( Gauge (C,m)) * ((i + 1),j)) `1 ) - ((( Gauge (C,m)) * (i,j)) `1 )) + (((( Gauge (C,m)) * (i,(j + 1))) `2 ) - ((( Gauge (C,m)) * (i,j)) `2 ))) by A28, A33, A32, A26, A30, A29, A31, TOPREAL6: 95;

        then ( dist (( W-min C),( W-min ( L~ ( Cage (C,m)))))) < r by A21, XXREAL_0: 2;

        then ( dist (w,p)) < r by TOPREAL6:def 1;

        then

         A34: p in ( Ball (w,r)) by METRIC_1: 11;

        (( Upper_Appr C) . m) = ( Upper_Arc ( L~ ( Cage (C,m)))) by JORDAN19:def 1;

        hence thesis by A9, A34, XBOOLE_0: 3;

      end;

      ( North_Arc C) = ( Lim_inf ( Upper_Appr C)) by JORDAN19:def 3;

      hence thesis by A1, KURATO_2: 14;

    end;

    theorem :: JORDAN22:30

    

     Th30: ( E-max C) in ( North_Arc C)

    proof

      reconsider w = ( E-max C) as Point of ( Euclid 2) by EUCLID: 67;

      

       A1: for r be Real st r > 0 holds ex k be Nat st for m be Nat st m > k holds (( Upper_Appr C) . m) meets ( Ball (w,r))

      proof

        let r be Real;

        assume r > 0 ;

        then (r / 2) > 0 ;

        then

        consider k be Nat such that 1 < k and

         A2: ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (1,2)))) < (r / 2) and

         A3: ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (2,1)))) < (r / 2) by GOBRD14: 11;

        reconsider k as Nat;

        take k;

        let m be Nat such that

         A4: m > k;

        ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,2)))) < ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (1,2)))) by A4, Th9;

        then

         A5: ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,2)))) < (r / 2) by A2, XXREAL_0: 2;

        ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (2,1)))) < ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (2,1)))) by A4, Th11;

        then

         A6: ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (2,1)))) < (r / 2) by A3, XXREAL_0: 2;

        reconsider p = ( E-max ( L~ ( Cage (C,m)))) as Point of ( Euclid 2) by EUCLID: 67;

        

         A7: ( E-max ( L~ ( Cage (C,m)))) in ( Upper_Arc ( L~ ( Cage (C,m)))) by JORDAN7: 1;

        

         A8: (1 + 1) <= ( len ( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m))))))) by GOBOARD7: 34, XXREAL_0: 2;

        then

         A9: (( left_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1)) /\ ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1))) = ( LSeg (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1)) by GOBOARD5: 31;

        ( Cage (C,m)) is_sequence_on ( Gauge (C,m)) by JORDAN9:def 1;

        then

         A10: ( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))) is_sequence_on ( Gauge (C,m)) by REVROT_1: 34;

        ( E-max ( L~ ( Cage (C,m)))) in ( rng ( Cage (C,m))) by SPRECT_2: 46;

        then

         A11: ( E-max ( L~ ( Cage (C,m)))) = (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))) /. 1) by FINSEQ_6: 92;

        then (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))) /. 1) = ( E-max ( L~ ( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))))) by REVROT_1: 33;

        then

        consider i,j be Nat such that

         A12: [i, (j + 1)] in ( Indices ( Gauge (C,m))) and

         A13: [i, j] in ( Indices ( Gauge (C,m))) and

         A14: (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))) /. 1) = (( Gauge (C,m)) * (i,(j + 1))) and

         A15: (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))) /. (1 + 1)) = (( Gauge (C,m)) * (i,j)) by A8, A10, JORDAN1I: 23;

        

         A16: i <= ( len ( Gauge (C,m))) by A12, MATRIX_0: 32;

        i > 1 by A8, A10, A12, A13, A14, A15, JORDAN1I: 16;

        then

         A17: (i - 1) > (1 - 1) by XREAL_1: 14;

        then

         A18: (i -' 1) = (i - 1) by XREAL_0:def 2;

        then

         A19: (i -' 1) <= ( len ( Gauge (C,m))) by A16, XREAL_1: 146, XXREAL_0: 2;

        (i - 1) in NAT by A17, INT_1: 3;

        then

         A20: (i - 1) >= ( 0 + 1) by A17, NAT_1: 13;

        then

         A21: ((i -' 1) + 1) = i by NAT_D: 43;

        ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1)) = ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1,( GoB ( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m))))))))) by A8, JORDAN1H: 23

        .= ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1,( GoB ( Cage (C,m))))) by REVROT_1: 28

        .= ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1,( Gauge (C,m)))) by JORDAN1H: 44;

        then

         A22: ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1)) = ( cell (( Gauge (C,m)),(i -' 1),j)) by A8, A10, A12, A13, A14, A15, GOBRD13: 28;

        

         A23: (j + 1) <= ( width ( Gauge (C,m))) by A12, MATRIX_0: 32;

        1 <= (j + 1) by NAT_1: 11;

        then

         A24: [(i -' 1), (j + 1)] in ( Indices ( Gauge (C,m))) by A23, A20, A18, A19, MATRIX_0: 30;

        

         A25: 1 <= j by A13, MATRIX_0: 32;

        j <= ( width ( Gauge (C,m))) by A13, MATRIX_0: 32;

        then

         A26: [(i -' 1), j] in ( Indices ( Gauge (C,m))) by A25, A20, A18, A19, MATRIX_0: 30;

         [1, (1 + 1)] in ( Indices ( Gauge (C,m))) by Th6;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,(1 + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ m)) by Th5, GOBRD14: 9;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,(1 + 1))))) = ( dist ((( Gauge (C,m)) * ((i -' 1),j)),(( Gauge (C,m)) * ((i -' 1),(j + 1))))) by A26, A24, GOBRD14: 9;

        then

         A27: (((( Gauge (C,m)) * ((i -' 1),(j + 1))) `2 ) - ((( Gauge (C,m)) * ((i -' 1),j)) `2 )) < (r / 2) by A26, A24, A5, GOBRD14: 6;

         [(1 + 1), 1] in ( Indices ( Gauge (C,m))) by Th7;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * ((1 + 1),1)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ m)) by Th5, GOBRD14: 10;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * ((1 + 1),1)))) = ( dist ((( Gauge (C,m)) * ((i -' 1),j)),(( Gauge (C,m)) * (((i -' 1) + 1),j)))) by A13, A21, A26, GOBRD14: 10;

        then (((( Gauge (C,m)) * (((i -' 1) + 1),j)) `1 ) - ((( Gauge (C,m)) * ((i -' 1),j)) `1 )) < (r / 2) by A13, A21, A26, A6, GOBRD14: 5;

        then

         A28: ((((( Gauge (C,m)) * (((i -' 1) + 1),j)) `1 ) - ((( Gauge (C,m)) * ((i -' 1),j)) `1 )) + (((( Gauge (C,m)) * ((i -' 1),(j + 1))) `2 ) - ((( Gauge (C,m)) * ((i -' 1),j)) `2 ))) < ((r / 2) + (r / 2)) by A27, XREAL_1: 8;

        

         A29: ( E-max C) in ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1)) by JORDAN1I: 7;

        then

         A30: (( E-max C) `1 ) <= ((( Gauge (C,m)) * (((i -' 1) + 1),j)) `1 ) by A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))) /. 1) in ( LSeg (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1)) by A8, TOPREAL1: 21;

        then

         A31: ( E-max ( L~ ( Cage (C,m)))) in ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1)) by A11, A9, XBOOLE_0:def 4;

        then

         A32: ((( Gauge (C,m)) * ((i -' 1),j)) `1 ) <= (( E-max ( L~ ( Cage (C,m)))) `1 ) by A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        

         A33: ((( Gauge (C,m)) * ((i -' 1),j)) `2 ) <= (( E-max ( L~ ( Cage (C,m)))) `2 ) by A31, A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        

         A34: (( E-max ( L~ ( Cage (C,m)))) `1 ) <= ((( Gauge (C,m)) * (((i -' 1) + 1),j)) `1 ) by A31, A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        

         A35: (( E-max ( L~ ( Cage (C,m)))) `2 ) <= ((( Gauge (C,m)) * ((i -' 1),(j + 1))) `2 ) by A31, A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        

         A36: (( E-max C) `2 ) <= ((( Gauge (C,m)) * ((i -' 1),(j + 1))) `2 ) by A29, A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        

         A37: ((( Gauge (C,m)) * ((i -' 1),j)) `2 ) <= (( E-max C) `2 ) by A29, A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        ((( Gauge (C,m)) * ((i -' 1),j)) `1 ) <= (( E-max C) `1 ) by A29, A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        then ( dist (( E-max C),( E-max ( L~ ( Cage (C,m)))))) <= ((((( Gauge (C,m)) * (((i -' 1) + 1),j)) `1 ) - ((( Gauge (C,m)) * ((i -' 1),j)) `1 )) + (((( Gauge (C,m)) * ((i -' 1),(j + 1))) `2 ) - ((( Gauge (C,m)) * ((i -' 1),j)) `2 ))) by A30, A37, A36, A32, A34, A33, A35, TOPREAL6: 95;

        then ( dist (( E-max C),( E-max ( L~ ( Cage (C,m)))))) < r by A28, XXREAL_0: 2;

        then ( dist (w,p)) < r by TOPREAL6:def 1;

        then

         A38: p in ( Ball (w,r)) by METRIC_1: 11;

        (( Upper_Appr C) . m) = ( Upper_Arc ( L~ ( Cage (C,m)))) by JORDAN19:def 1;

        hence thesis by A7, A38, XBOOLE_0: 3;

      end;

      ( North_Arc C) = ( Lim_inf ( Upper_Appr C)) by JORDAN19:def 3;

      hence thesis by A1, KURATO_2: 14;

    end;

    theorem :: JORDAN22:31

    

     Th31: ( W-min C) in ( South_Arc C)

    proof

      reconsider w = ( W-min C) as Point of ( Euclid 2) by EUCLID: 67;

      

       A1: for r be Real st r > 0 holds ex k be Nat st for m be Nat st m > k holds (( Lower_Appr C) . m) meets ( Ball (w,r))

      proof

        let r be Real;

        assume r > 0 ;

        then (r / 2) > 0 ;

        then

        consider k be Nat such that 1 < k and

         A2: ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (1,2)))) < (r / 2) and

         A3: ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (2,1)))) < (r / 2) by GOBRD14: 11;

        reconsider k as Nat;

        take k;

        let m be Nat such that

         A4: m > k;

        ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,2)))) < ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (1,2)))) by A4, Th9;

        then

         A5: ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,2)))) < (r / 2) by A2, XXREAL_0: 2;

        ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (2,1)))) < ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (2,1)))) by A4, Th11;

        then

         A6: ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (2,1)))) < (r / 2) by A3, XXREAL_0: 2;

        

         A7: (1 + 1) <= ( len ( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m))))))) by GOBOARD7: 34, XXREAL_0: 2;

        then

         A8: (( left_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1)) /\ ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1))) = ( LSeg (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1)) by GOBOARD5: 31;

        reconsider p = ( W-min ( L~ ( Cage (C,m)))) as Point of ( Euclid 2) by EUCLID: 67;

        

         A9: ( W-min ( L~ ( Cage (C,m)))) in ( Lower_Arc ( L~ ( Cage (C,m)))) by JORDAN7: 1;

        ( Cage (C,m)) is_sequence_on ( Gauge (C,m)) by JORDAN9:def 1;

        then

         A10: ( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))) is_sequence_on ( Gauge (C,m)) by REVROT_1: 34;

        ( W-min ( L~ ( Cage (C,m)))) in ( rng ( Cage (C,m))) by SPRECT_2: 43;

        then

         A11: ( W-min ( L~ ( Cage (C,m)))) = (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))) /. 1) by FINSEQ_6: 92;

        then (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))) /. 1) = ( W-min ( L~ ( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))))) by REVROT_1: 33;

        then

        consider i,j be Nat such that

         A12: [i, j] in ( Indices ( Gauge (C,m))) and

         A13: [i, (j + 1)] in ( Indices ( Gauge (C,m))) and

         A14: (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))) /. 1) = (( Gauge (C,m)) * (i,j)) and

         A15: (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))) /. (1 + 1)) = (( Gauge (C,m)) * (i,(j + 1))) by A7, A10, JORDAN1I: 21;

        

         A16: 1 <= j by A12, MATRIX_0: 32;

        i < ( len ( Gauge (C,m))) by A7, A10, A12, A13, A14, A15, JORDAN1I: 14;

        then

         A17: (i + 1) <= ( len ( Gauge (C,m))) by NAT_1: 13;

        

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

        j <= ( width ( Gauge (C,m))) by A12, MATRIX_0: 32;

        then

         A19: [(i + 1), j] in ( Indices ( Gauge (C,m))) by A16, A18, A17, MATRIX_0: 30;

         [(1 + 1), 1] in ( Indices ( Gauge (C,m))) by Th7;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * ((1 + 1),1)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ m)) by Th5, GOBRD14: 10;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * ((1 + 1),1)))) = ( dist ((( Gauge (C,m)) * (i,j)),(( Gauge (C,m)) * ((i + 1),j)))) by A12, A19, GOBRD14: 10;

        then

         A20: (((( Gauge (C,m)) * ((i + 1),j)) `1 ) - ((( Gauge (C,m)) * (i,j)) `1 )) < (r / 2) by A12, A19, A6, GOBRD14: 5;

         [1, (1 + 1)] in ( Indices ( Gauge (C,m))) by Th6;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,(1 + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ m)) by Th5, GOBRD14: 9;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,(1 + 1))))) = ( dist ((( Gauge (C,m)) * (i,j)),(( Gauge (C,m)) * (i,(j + 1))))) by A12, A13, GOBRD14: 9;

        then (((( Gauge (C,m)) * (i,(j + 1))) `2 ) - ((( Gauge (C,m)) * (i,j)) `2 )) < (r / 2) by A12, A13, A5, GOBRD14: 6;

        then

         A21: ((((( Gauge (C,m)) * ((i + 1),j)) `1 ) - ((( Gauge (C,m)) * (i,j)) `1 )) + (((( Gauge (C,m)) * (i,(j + 1))) `2 ) - ((( Gauge (C,m)) * (i,j)) `2 ))) < ((r / 2) + (r / 2)) by A20, XREAL_1: 8;

        

         A22: 1 <= i by A12, MATRIX_0: 32;

        ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1)) = ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1,( GoB ( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m))))))))) by A7, JORDAN1H: 23

        .= ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1,( GoB ( Cage (C,m))))) by REVROT_1: 28

        .= ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1,( Gauge (C,m)))) by JORDAN1H: 44;

        then

         A23: ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1)) = ( cell (( Gauge (C,m)),i,j)) by A7, A10, A12, A13, A14, A15, GOBRD13: 22;

        

         A24: (j + 1) <= ( width ( Gauge (C,m))) by A13, MATRIX_0: 32;

        (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))) /. 1) in ( LSeg (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1)) by A7, TOPREAL1: 21;

        then

         A25: ( W-min ( L~ ( Cage (C,m)))) in ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1)) by A11, A8, XBOOLE_0:def 4;

        then

         A26: ((( Gauge (C,m)) * (i,j)) `1 ) <= (( W-min ( L~ ( Cage (C,m)))) `1 ) by A23, A22, A16, A24, A17, JORDAN9: 17;

        

         A27: ( W-min C) in ( right_cell (( Rotate (( Cage (C,m)),( W-min ( L~ ( Cage (C,m)))))),1)) by JORDAN1I: 6;

        then

         A28: (( W-min C) `1 ) <= ((( Gauge (C,m)) * ((i + 1),j)) `1 ) by A23, A22, A16, A24, A17, JORDAN9: 17;

        

         A29: ((( Gauge (C,m)) * (i,j)) `2 ) <= (( W-min ( L~ ( Cage (C,m)))) `2 ) by A25, A23, A22, A16, A24, A17, JORDAN9: 17;

        

         A30: (( W-min ( L~ ( Cage (C,m)))) `1 ) <= ((( Gauge (C,m)) * ((i + 1),j)) `1 ) by A25, A23, A22, A16, A24, A17, JORDAN9: 17;

        

         A31: (( W-min ( L~ ( Cage (C,m)))) `2 ) <= ((( Gauge (C,m)) * (i,(j + 1))) `2 ) by A25, A23, A22, A16, A24, A17, JORDAN9: 17;

        

         A32: (( W-min C) `2 ) <= ((( Gauge (C,m)) * (i,(j + 1))) `2 ) by A27, A23, A22, A16, A24, A17, JORDAN9: 17;

        

         A33: ((( Gauge (C,m)) * (i,j)) `2 ) <= (( W-min C) `2 ) by A27, A23, A22, A16, A24, A17, JORDAN9: 17;

        ((( Gauge (C,m)) * (i,j)) `1 ) <= (( W-min C) `1 ) by A27, A23, A22, A16, A24, A17, JORDAN9: 17;

        then ( dist (( W-min C),( W-min ( L~ ( Cage (C,m)))))) <= ((((( Gauge (C,m)) * ((i + 1),j)) `1 ) - ((( Gauge (C,m)) * (i,j)) `1 )) + (((( Gauge (C,m)) * (i,(j + 1))) `2 ) - ((( Gauge (C,m)) * (i,j)) `2 ))) by A28, A33, A32, A26, A30, A29, A31, TOPREAL6: 95;

        then ( dist (( W-min C),( W-min ( L~ ( Cage (C,m)))))) < r by A21, XXREAL_0: 2;

        then ( dist (w,p)) < r by TOPREAL6:def 1;

        then

         A34: p in ( Ball (w,r)) by METRIC_1: 11;

        (( Lower_Appr C) . m) = ( Lower_Arc ( L~ ( Cage (C,m)))) by JORDAN19:def 2;

        hence thesis by A9, A34, XBOOLE_0: 3;

      end;

      ( South_Arc C) = ( Lim_inf ( Lower_Appr C)) by JORDAN19:def 4;

      hence thesis by A1, KURATO_2: 14;

    end;

    theorem :: JORDAN22:32

    

     Th32: ( E-max C) in ( South_Arc C)

    proof

      reconsider w = ( E-max C) as Point of ( Euclid 2) by EUCLID: 67;

      

       A1: for r be Real st r > 0 holds ex k be Nat st for m be Nat st m > k holds (( Lower_Appr C) . m) meets ( Ball (w,r))

      proof

        let r be Real;

        assume r > 0 ;

        then (r / 2) > 0 ;

        then

        consider k be Nat such that 1 < k and

         A2: ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (1,2)))) < (r / 2) and

         A3: ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (2,1)))) < (r / 2) by GOBRD14: 11;

        take k;

        let m be Nat such that

         A4: m > k;

        ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,2)))) < ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (1,2)))) by A4, Th9;

        then

         A5: ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,2)))) < (r / 2) by A2, XXREAL_0: 2;

        ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (2,1)))) < ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (2,1)))) by A4, Th11;

        then

         A6: ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (2,1)))) < (r / 2) by A3, XXREAL_0: 2;

        reconsider p = ( E-max ( L~ ( Cage (C,m)))) as Point of ( Euclid 2) by EUCLID: 67;

        

         A7: ( E-max ( L~ ( Cage (C,m)))) in ( Lower_Arc ( L~ ( Cage (C,m)))) by JORDAN7: 1;

        

         A8: (1 + 1) <= ( len ( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m))))))) by GOBOARD7: 34, XXREAL_0: 2;

        then

         A9: (( left_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1)) /\ ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1))) = ( LSeg (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1)) by GOBOARD5: 31;

        ( Cage (C,m)) is_sequence_on ( Gauge (C,m)) by JORDAN9:def 1;

        then

         A10: ( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))) is_sequence_on ( Gauge (C,m)) by REVROT_1: 34;

        ( E-max ( L~ ( Cage (C,m)))) in ( rng ( Cage (C,m))) by SPRECT_2: 46;

        then

         A11: ( E-max ( L~ ( Cage (C,m)))) = (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))) /. 1) by FINSEQ_6: 92;

        then (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))) /. 1) = ( E-max ( L~ ( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))))) by REVROT_1: 33;

        then

        consider i,j be Nat such that

         A12: [i, (j + 1)] in ( Indices ( Gauge (C,m))) and

         A13: [i, j] in ( Indices ( Gauge (C,m))) and

         A14: (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))) /. 1) = (( Gauge (C,m)) * (i,(j + 1))) and

         A15: (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))) /. (1 + 1)) = (( Gauge (C,m)) * (i,j)) by A8, A10, JORDAN1I: 23;

        

         A16: i <= ( len ( Gauge (C,m))) by A12, MATRIX_0: 32;

        i > 1 by A8, A10, A12, A13, A14, A15, JORDAN1I: 16;

        then

         A17: (i - 1) > (1 - 1) by XREAL_1: 14;

        then

         A18: (i -' 1) = (i - 1) by XREAL_0:def 2;

        then

         A19: (i -' 1) <= ( len ( Gauge (C,m))) by A16, XREAL_1: 146, XXREAL_0: 2;

        (i - 1) in NAT by A17, INT_1: 3;

        then

         A20: (i - 1) >= ( 0 + 1) by A17, NAT_1: 13;

        then

         A21: ((i -' 1) + 1) = i by NAT_D: 43;

        ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1)) = ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1,( GoB ( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m))))))))) by A8, JORDAN1H: 23

        .= ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1,( GoB ( Cage (C,m))))) by REVROT_1: 28

        .= ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1,( Gauge (C,m)))) by JORDAN1H: 44;

        then

         A22: ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1)) = ( cell (( Gauge (C,m)),(i -' 1),j)) by A8, A10, A12, A13, A14, A15, GOBRD13: 28;

        

         A23: (j + 1) <= ( width ( Gauge (C,m))) by A12, MATRIX_0: 32;

        1 <= (j + 1) by NAT_1: 11;

        then

         A24: [(i -' 1), (j + 1)] in ( Indices ( Gauge (C,m))) by A23, A20, A18, A19, MATRIX_0: 30;

        

         A25: 1 <= j by A13, MATRIX_0: 32;

        j <= ( width ( Gauge (C,m))) by A13, MATRIX_0: 32;

        then

         A26: [(i -' 1), j] in ( Indices ( Gauge (C,m))) by A25, A20, A18, A19, MATRIX_0: 30;

         [1, (1 + 1)] in ( Indices ( Gauge (C,m))) by Th6;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,(1 + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ m)) by Th5, GOBRD14: 9;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * (1,(1 + 1))))) = ( dist ((( Gauge (C,m)) * ((i -' 1),j)),(( Gauge (C,m)) * ((i -' 1),(j + 1))))) by A26, A24, GOBRD14: 9;

        then

         A27: (((( Gauge (C,m)) * ((i -' 1),(j + 1))) `2 ) - ((( Gauge (C,m)) * ((i -' 1),j)) `2 )) < (r / 2) by A26, A24, A5, GOBRD14: 6;

         [(1 + 1), 1] in ( Indices ( Gauge (C,m))) by Th7;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * ((1 + 1),1)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ m)) by Th5, GOBRD14: 10;

        then ( dist ((( Gauge (C,m)) * (1,1)),(( Gauge (C,m)) * ((1 + 1),1)))) = ( dist ((( Gauge (C,m)) * ((i -' 1),j)),(( Gauge (C,m)) * (((i -' 1) + 1),j)))) by A13, A21, A26, GOBRD14: 10;

        then (((( Gauge (C,m)) * (((i -' 1) + 1),j)) `1 ) - ((( Gauge (C,m)) * ((i -' 1),j)) `1 )) < (r / 2) by A13, A21, A26, A6, GOBRD14: 5;

        then

         A28: ((((( Gauge (C,m)) * (((i -' 1) + 1),j)) `1 ) - ((( Gauge (C,m)) * ((i -' 1),j)) `1 )) + (((( Gauge (C,m)) * ((i -' 1),(j + 1))) `2 ) - ((( Gauge (C,m)) * ((i -' 1),j)) `2 ))) < ((r / 2) + (r / 2)) by A27, XREAL_1: 8;

        

         A29: ( E-max C) in ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1)) by JORDAN1I: 7;

        then

         A30: (( E-max C) `1 ) <= ((( Gauge (C,m)) * (((i -' 1) + 1),j)) `1 ) by A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))) /. 1) in ( LSeg (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1)) by A8, TOPREAL1: 21;

        then

         A31: ( E-max ( L~ ( Cage (C,m)))) in ( right_cell (( Rotate (( Cage (C,m)),( E-max ( L~ ( Cage (C,m)))))),1)) by A11, A9, XBOOLE_0:def 4;

        then

         A32: ((( Gauge (C,m)) * ((i -' 1),j)) `1 ) <= (( E-max ( L~ ( Cage (C,m)))) `1 ) by A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        

         A33: ((( Gauge (C,m)) * ((i -' 1),j)) `2 ) <= (( E-max ( L~ ( Cage (C,m)))) `2 ) by A31, A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        

         A34: (( E-max ( L~ ( Cage (C,m)))) `1 ) <= ((( Gauge (C,m)) * (((i -' 1) + 1),j)) `1 ) by A31, A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        

         A35: (( E-max ( L~ ( Cage (C,m)))) `2 ) <= ((( Gauge (C,m)) * ((i -' 1),(j + 1))) `2 ) by A31, A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        

         A36: (( E-max C) `2 ) <= ((( Gauge (C,m)) * ((i -' 1),(j + 1))) `2 ) by A29, A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        

         A37: ((( Gauge (C,m)) * ((i -' 1),j)) `2 ) <= (( E-max C) `2 ) by A29, A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        ((( Gauge (C,m)) * ((i -' 1),j)) `1 ) <= (( E-max C) `1 ) by A29, A22, A25, A23, A20, A21, A16, JORDAN9: 17;

        then ( dist (( E-max C),( E-max ( L~ ( Cage (C,m)))))) <= ((((( Gauge (C,m)) * (((i -' 1) + 1),j)) `1 ) - ((( Gauge (C,m)) * ((i -' 1),j)) `1 )) + (((( Gauge (C,m)) * ((i -' 1),(j + 1))) `2 ) - ((( Gauge (C,m)) * ((i -' 1),j)) `2 ))) by A30, A37, A36, A32, A34, A33, A35, TOPREAL6: 95;

        then ( dist (( E-max C),( E-max ( L~ ( Cage (C,m)))))) < r by A28, XXREAL_0: 2;

        then ( dist (w,p)) < r by TOPREAL6:def 1;

        then

         A38: p in ( Ball (w,r)) by METRIC_1: 11;

        (( Lower_Appr C) . m) = ( Lower_Arc ( L~ ( Cage (C,m)))) by JORDAN19:def 2;

        hence thesis by A7, A38, XBOOLE_0: 3;

      end;

      ( South_Arc C) = ( Lim_inf ( Lower_Appr C)) by JORDAN19:def 4;

      hence thesis by A1, KURATO_2: 14;

    end;

    

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

    theorem :: JORDAN22:33

    

     Th33: ( UMP C) in ( North_Arc C)

    proof

      set w = ((( W-bound C) + ( E-bound C)) / 2);

      set p = ( UMP C);

      set U = { ( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) where n be Nat : 0 < n };

      set n0 = ( N-bound ( L~ ( Cage (C,1))));

      set H = ( LSeg (p, |[w, n0]|));

      

       A1: ( |[w, ( N-bound C)]| `1 ) = w by EUCLID: 52;

      

       A2: ( |[w, n0]| `1 ) = w by EUCLID: 52;

      { ( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) where n be Nat : 0 < n } c= the carrier of ( TOP-REAL 2)

      proof

        let x be object;

        assume x in { ( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) where n be Nat : 0 < n };

        then ex n be Nat st x = ( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) & 0 < n;

        hence thesis;

      end;

      then

      reconsider U as Subset of ( TOP-REAL 2);

      set q = ( lower_bound ( proj2 .: (H /\ U)));

      set S = ( LSeg ( |[w, q]|, |[w, n0]|));

      

       A3: ( |[w, ( N-bound C)]| `2 ) = ( N-bound C) by EUCLID: 52;

      

       A4: ( |[w, n0]| `2 ) = n0 by EUCLID: 52;

      

       A5: for n be Nat holds (( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) `1 ) = w

      proof

        let n be Nat;

        

         A6: (( W-bound ( L~ ( Cage (C,n)))) + ( E-bound ( L~ ( Cage (C,n))))) = (( W-bound C) + ( E-bound C)) by JORDAN1G: 33;

        

        thus (( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) `1 ) = ((( W-bound ( Upper_Arc ( L~ ( Cage (C,n))))) + ( E-bound ( Upper_Arc ( L~ ( Cage (C,n)))))) / 2) by EUCLID: 52

        .= ((( W-bound ( L~ ( Cage (C,n)))) + ( E-bound ( Upper_Arc ( L~ ( Cage (C,n)))))) / 2) by JORDAN21: 17

        .= w by A6, JORDAN21: 18;

      end;

      

       A7: (p `2 ) <= (( UMP ( Upper_Arc ( L~ ( Cage (C,1))))) `2 ) by Th23;

      

       A8: (( LSeg (p, |[w, ( N-bound C)]|)) /\ C) = {p} by JORDAN21: 34;

      

       A9: (( UMP ( Upper_Arc ( L~ ( Cage (C,1))))) `2 ) <= n0 by JORDAN21: 47;

      (H /\ U) is bounded by TOPREAL6: 89;

      then ( proj2 .: (H /\ U)) is real-bounded by JCT_MISC: 14;

      then

       A10: ( proj2 .: (H /\ U)) is bounded_below;

      

       A11: (p `1 ) = w by EUCLID: 52;

      

       A12: for n be Nat st 0 < n holds (( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) `2 ) in ( proj2 .: (H /\ U))

      proof

        let n be Nat;

        set f = ( Cage (C,n));

        set s = ( UMP ( Upper_Arc ( L~ f)));

        assume

         A13: 0 < n;

        then

         A14: s in U;

        ( 0 + 1) <= n by A13, NAT_1: 13;

        then 1 < n or n = 1 by XXREAL_0: 1;

        then

         A15: ( N-bound ( L~ ( Cage (C,n)))) <= ( N-bound ( L~ ( Cage (C,1)))) by JORDAN10: 7;

        (s `2 ) <= ( N-bound ( L~ f)) by JORDAN21: 47;

        then

         A16: (s `2 ) <= n0 by A15, XXREAL_0: 2;

        

         A17: (s `1 ) = w by A5;

        (p `2 ) <= (s `2 ) by A13, Th23;

        then s in H by A2, A4, A11, A16, A17, GOBOARD7: 7;

        then

         A18: s in (H /\ U) by A14, XBOOLE_0:def 4;

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

        hence thesis by A18, FUNCT_2: 35;

      end;

      then

       A19: (( UMP ( Upper_Arc ( L~ ( Cage (C,1))))) `2 ) in ( proj2 .: (H /\ U));

      then q <= (( UMP ( Upper_Arc ( L~ ( Cage (C,1))))) `2 ) by A10, SEQ_4:def 2;

      then

       A20: q <= n0 by A9, XXREAL_0: 2;

      

       A21: ( |[w, q]| `1 ) = w by EUCLID: 52;

      then

       A22: S is vertical by A2, SPPOL_1: 16;

      

       A23: |[w, q]| in S by RLTOPSP1: 68;

      

       A24: ( |[w, q]| `2 ) = q by EUCLID: 52;

      per cases ;

        suppose

         A25: p <> |[w, q]|;

        consider S9,C9 be Subset of ( TopSpaceMetr ( Euclid 2)) such that

         A26: S = S9 and

         A27: C = C9 and

         A28: ( dist_min (S,C)) = ( min_dist_min (S9,C9)) by JORDAN1K:def 1;

        

         A29: S9 is compact by A26, Lm4, COMPTS_1: 23;

        

         A30: C9 is compact by A27, Lm4, COMPTS_1: 23;

         A31:

        now

          assume

           A32: (p `2 ) >= q;

          per cases by A32, XXREAL_0: 1;

            suppose (p `2 ) = q;

            hence contradiction by A25, EUCLID: 52;

          end;

            suppose (p `2 ) > q;

            then 0 < ((p `2 ) - q) by XREAL_1: 50;

            then

            consider r be Real such that

             A33: r in ( proj2 .: (H /\ U)) and

             A34: r < (q + ((p `2 ) - q)) by A10, A19, SEQ_4:def 2;

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

             A35: t in (H /\ U) and

             A36: ( proj2 . t) = r by A33, Lm1;

            

             A37: t in H by A35, XBOOLE_0:def 4;

            

             A38: (p `2 ) <= n0 by A9, A7, XXREAL_0: 2;

            (t `2 ) = r by A36, PSCOMP_1:def 6;

            hence contradiction by A4, A34, A38, A37, TOPREAL1: 4;

          end;

        end;

        S misses C

        proof

          assume S meets C;

          then

          consider x be object such that

           A39: x in S and

           A40: x in C by XBOOLE_0: 3;

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

          

           A41: (x `2 ) <= ( N-bound C) by A40, PSCOMP_1: 24;

          

           A42: (x `1 ) = w by A21, A23, A22, A39, SPPOL_1:def 3;

          

           A43: q <= (x `2 ) by A4, A24, A20, A39, TOPREAL1: 4;

          then (p `2 ) < (x `2 ) by A31, XXREAL_0: 2;

          then x in ( LSeg (p, |[w, ( N-bound C)]|)) by A1, A3, A11, A41, A42, GOBOARD7: 7;

          then x in {p} by A8, A40, XBOOLE_0:def 4;

          hence contradiction by A31, A43, TARSKI:def 1;

        end;

        then ( dist_min (S,C)) > 0 by A26, A27, A28, A29, A30, JGRAPH_1: 38;

        then (( dist_min (S,C)) / 2) > 0 ;

        then

        consider k be Nat such that

         A44: 1 < k and

         A45: ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (1,2)))) < (( dist_min (S,C)) / 2) and

         A46: ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (2,1)))) < (( dist_min (S,C)) / 2) by GOBRD14: 11;

        set f = ( Cage (C,k)), G = ( Gauge (C,k));

        set s = ( UMP ( Upper_Arc ( L~ f)));

        

         A47: (s `2 ) <= ( N-bound ( L~ f)) by JORDAN21: 47;

        

         A48: (( dist ((G * (1,1)),(G * ((1 + 1),1)))) + ( dist ((G * (1,1)),(G * (1,(1 + 1)))))) < ((( dist_min (S,C)) / 2) + (( dist_min (S,C)) / 2)) by A45, A46, XREAL_1: 8;

        ( N-bound ( L~ ( Cage (C,k)))) <= ( N-bound ( L~ ( Cage (C,1)))) by A44, JORDAN10: 7;

        then

         A49: (s `2 ) <= n0 by A47, XXREAL_0: 2;

        (s `2 ) in ( proj2 .: (H /\ U)) by A12, A44;

        then

         A50: q <= (s `2 ) by A10, SEQ_4:def 2;

         [1, (1 + 1)] in ( Indices G) by Th6;

        then

         A51: ( dist ((G * (1,1)),(G * (1,(1 + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ k)) by Th5, GOBRD14: 9;

         [(1 + 1), 1] in ( Indices G) by Th7;

        then

         A52: ( dist ((G * (1,1)),(G * ((1 + 1),1)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ k)) by Th5, GOBRD14: 10;

        

         A53: s in ( Upper_Arc ( L~ f)) by JORDAN21: 30;

        ( Upper_Arc ( L~ f)) c= ( L~ f) by JORDAN6: 61;

        then

        consider i be Nat such that

         A54: 1 <= i and

         A55: (i + 1) <= ( len f) and

         A56: s in ( LSeg (f,i)) by A53, SPPOL_2: 13;

        

         A57: f is_sequence_on G by JORDAN9:def 1;

        then

        consider i1,j1,i2,j2 be Nat such that

         A58: [i1, j1] in ( Indices G) and

         A59: (f /. i) = (G * (i1,j1)) and

         A60: [i2, j2] in ( Indices G) and

         A61: (f /. (i + 1)) = (G * (i2,j2)) and

         A62: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A54, A55, JORDAN8: 3;

        

         A63: 1 <= i1 by A58, MATRIX_0: 32;

        ( right_cell (f,i,G)) meets C by A54, A55, JORDAN9: 31;

        then

        consider c be object such that

         A64: c in ( right_cell (f,i,G)) and

         A65: c in C by XBOOLE_0: 3;

        reconsider c as Point of ( TOP-REAL 2) by A65;

        reconsider s9 = s, c9 = c as Point of ( Euclid 2) by EUCLID: 67;

        (s `1 ) = w by A5;

        then s in S by A2, A4, A21, A24, A49, A50, GOBOARD7: 7;

        then

         A66: ( min_dist_min (S9,C9)) <= ( dist (s9,c9)) by A26, A27, A29, A30, A65, WEIERSTR: 34;

        

         A67: ( dist (s9,c9)) = ( dist (s,c)) by TOPREAL6:def 1;

        

         A68: 1 <= j2 by A60, MATRIX_0: 32;

        (( left_cell (f,i,G)) /\ ( right_cell (f,i,G))) = ( LSeg (f,i)) by A54, A55, A57, GOBRD13: 29;

        then

         A69: s in ( right_cell (f,i,G)) by A56, XBOOLE_0:def 4;

        

         A70: j2 <= ( width G) by A60, MATRIX_0: 32;

        

         A71: ((j2 + 1) + 1) <> j2;

        

         A72: 1 <= i2 by A60, MATRIX_0: 32;

        

         A73: j1 <= ( width G) by A58, MATRIX_0: 32;

        

         A74: 1 <= (j1 + 1) by NAT_1: 11;

        

         A75: (i1 + 1) <> (i1 + 0 );

        

         A76: i1 <= ( len G) by A58, MATRIX_0: 32;

        

         A77: i2 <= ( len G) by A60, MATRIX_0: 32;

        

         A78: ((i2 + 1) + 1) <> i2;

        

         A79: 1 <= j1 by A58, MATRIX_0: 32;

        

         A80: 1 <= (i1 + 1) by NAT_1: 11;

        now

          per cases by A62;

            suppose

             A81: i1 = i2 & (j1 + 1) = j2;

            then

             A82: ( dist ((G * (i1,j1)),(G * (i1,(j1 + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ k)) by A58, A60, GOBRD14: 9;

            

             A83: ( dist ((G * (i1,j1)),(G * (i1,(j1 + 1))))) = (((G * (i1,(j1 + 1))) `2 ) - ((G * (i1,j1)) `2 )) by A58, A60, A81, GOBRD14: 6;

            i1 < ( len G) by A54, A55, A58, A59, A60, A61, A81, JORDAN10: 1;

            then

             A84: (i1 + 1) <= ( len G) by NAT_1: 13;

            then

             A85: [(i1 + 1), j1] in ( Indices G) by A79, A80, A73, MATRIX_0: 30;

            then

             A86: ( dist ((G * (i1,j1)),(G * ((i1 + 1),j1)))) = (((G * ((i1 + 1),j1)) `1 ) - ((G * (i1,j1)) `1 )) by A58, GOBRD14: 5;

            

             A87: ( dist ((G * (i1,j1)),(G * ((i1 + 1),j1)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ k)) by A58, A85, GOBRD14: 10;

            

             A88: (j1 + 1) <= ( width G) by A60, A81, MATRIX_0: 32;

            

             A89: ( right_cell (f,i,G)) = ( cell (G,i1,j1)) by A54, A55, A57, A58, A59, A60, A61, A75, A71, A81, GOBRD13:def 2;

            then

             A90: (c `1 ) <= ((G * ((i1 + 1),j1)) `1 ) by A64, A63, A79, A88, A84, JORDAN9: 17;

            

             A91: (s `2 ) <= ((G * (i1,(j1 + 1))) `2 ) by A69, A63, A79, A88, A84, A89, JORDAN9: 17;

            

             A92: ((G * (i1,j1)) `2 ) <= (s `2 ) by A69, A63, A79, A88, A84, A89, JORDAN9: 17;

            

             A93: (s `1 ) <= ((G * ((i1 + 1),j1)) `1 ) by A69, A63, A79, A88, A84, A89, JORDAN9: 17;

            

             A94: ((G * (i1,j1)) `1 ) <= (s `1 ) by A69, A63, A79, A88, A84, A89, JORDAN9: 17;

            

             A95: (c `2 ) <= ((G * (i1,(j1 + 1))) `2 ) by A64, A63, A79, A88, A84, A89, JORDAN9: 17;

            

             A96: ((G * (i1,j1)) `2 ) <= (c `2 ) by A64, A63, A79, A88, A84, A89, JORDAN9: 17;

            ((G * (i1,j1)) `1 ) <= (c `1 ) by A64, A63, A79, A88, A84, A89, JORDAN9: 17;

            then ( dist (s,c)) <= ((((G * ((i1 + 1),j1)) `1 ) - ((G * (i1,j1)) `1 )) + (((G * (i1,(j1 + 1))) `2 ) - ((G * (i1,j1)) `2 ))) by A90, A96, A95, A94, A93, A92, A91, TOPREAL6: 95;

            hence contradiction by A28, A48, A66, A67, A51, A52, A86, A83, A82, A87, XXREAL_0: 2;

          end;

            suppose

             A97: (i1 + 1) = i2 & j1 = j2;

            then 1 < j1 by A54, A55, A58, A59, A60, A61, JORDAN10: 3;

            then

             A98: 1 <= (j1 -' 1) by NAT_D: 49;

            then

             A99: ((j1 -' 1) + 1) = j1 by NAT_D: 43;

            

             A100: (j1 -' 1) <= ( width G) by A73, NAT_D: 44;

            then

             A101: [i1, (j1 -' 1)] in ( Indices G) by A63, A76, A98, MATRIX_0: 30;

            then

             A102: ( dist ((G * (i1,(j1 -' 1))),(G * (i1,((j1 -' 1) + 1))))) = (((G * (i1,((j1 -' 1) + 1))) `2 ) - ((G * (i1,(j1 -' 1))) `2 )) by A58, A99, GOBRD14: 6;

            

             A103: [(i1 + 1), (j1 -' 1)] in ( Indices G) by A72, A77, A97, A98, A100, MATRIX_0: 30;

            then

             A104: ( dist ((G * (i1,(j1 -' 1))),(G * ((i1 + 1),(j1 -' 1))))) = (((G * ((i1 + 1),(j1 -' 1))) `1 ) - ((G * (i1,(j1 -' 1))) `1 )) by A101, GOBRD14: 5;

            

             A105: ( dist ((G * (i1,(j1 -' 1))),(G * (i1,((j1 -' 1) + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ k)) by A58, A99, A101, GOBRD14: 9;

            

             A106: ( dist ((G * (i1,(j1 -' 1))),(G * ((i1 + 1),(j1 -' 1))))) = ((( E-bound C) - ( W-bound C)) / (2 |^ k)) by A101, A103, GOBRD14: 10;

            

             A107: (i1 + 1) <= ( len G) by A60, A97, MATRIX_0: 32;

            

             A108: ( right_cell (f,i,G)) = ( cell (G,i1,(j1 -' 1))) by A54, A55, A57, A58, A59, A60, A61, A75, A78, A97, GOBRD13:def 2;

            then

             A109: (c `1 ) <= ((G * ((i1 + 1),(j1 -' 1))) `1 ) by A64, A63, A73, A107, A98, A99, JORDAN9: 17;

            

             A110: (s `2 ) <= ((G * (i1,((j1 -' 1) + 1))) `2 ) by A69, A63, A73, A107, A98, A99, A108, JORDAN9: 17;

            

             A111: ((G * (i1,(j1 -' 1))) `2 ) <= (s `2 ) by A69, A63, A73, A107, A98, A99, A108, JORDAN9: 17;

            

             A112: (s `1 ) <= ((G * ((i1 + 1),(j1 -' 1))) `1 ) by A69, A63, A73, A107, A98, A99, A108, JORDAN9: 17;

            

             A113: ((G * (i1,(j1 -' 1))) `1 ) <= (s `1 ) by A69, A63, A73, A107, A98, A99, A108, JORDAN9: 17;

            

             A114: (c `2 ) <= ((G * (i1,((j1 -' 1) + 1))) `2 ) by A64, A63, A73, A107, A98, A99, A108, JORDAN9: 17;

            

             A115: ((G * (i1,(j1 -' 1))) `2 ) <= (c `2 ) by A64, A63, A73, A107, A98, A99, A108, JORDAN9: 17;

            ((G * (i1,(j1 -' 1))) `1 ) <= (c `1 ) by A64, A63, A73, A107, A98, A99, A108, JORDAN9: 17;

            then ( dist (s,c)) <= ((((G * ((i1 + 1),(j1 -' 1))) `1 ) - ((G * (i1,(j1 -' 1))) `1 )) + (((G * (i1,((j1 -' 1) + 1))) `2 ) - ((G * (i1,(j1 -' 1))) `2 ))) by A109, A115, A114, A113, A112, A111, A110, TOPREAL6: 95;

            hence contradiction by A28, A48, A66, A67, A51, A52, A104, A102, A105, A106, XXREAL_0: 2;

          end;

            suppose

             A116: i1 = (i2 + 1) & j1 = j2;

            then

             A117: ( dist ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ k)) by A58, A60, GOBRD14: 10;

            

             A118: ( dist ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = (((G * ((i2 + 1),j2)) `1 ) - ((G * (i2,j2)) `1 )) by A58, A60, A116, GOBRD14: 5;

            

             A119: (i2 + 1) <= ( len G) by A58, A116, MATRIX_0: 32;

            j1 < ( width G) by A54, A55, A58, A59, A60, A61, A116, JORDAN10: 4;

            then

             A120: (j1 + 1) <= ( width G) by NAT_1: 13;

            then

             A121: [i2, (j2 + 1)] in ( Indices G) by A72, A74, A77, A116, MATRIX_0: 30;

            then

             A122: ( dist ((G * (i2,j2)),(G * (i2,(j2 + 1))))) = (((G * (i2,(j2 + 1))) `2 ) - ((G * (i2,j2)) `2 )) by A60, GOBRD14: 6;

            

             A123: ( right_cell (f,i,G)) = ( cell (G,i2,j2)) by A54, A55, A57, A58, A59, A60, A61, A75, A78, A116, GOBRD13:def 2;

            then

             A124: (c `1 ) <= ((G * ((i2 + 1),j2)) `1 ) by A64, A79, A72, A116, A119, A120, JORDAN9: 17;

            

             A125: (s `2 ) <= ((G * (i2,(j2 + 1))) `2 ) by A69, A79, A72, A116, A119, A120, A123, JORDAN9: 17;

            

             A126: ((G * (i2,j2)) `2 ) <= (c `2 ) by A64, A79, A72, A116, A119, A120, A123, JORDAN9: 17;

            

             A127: ( dist ((G * (i2,j2)),(G * (i2,(j2 + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ k)) by A60, A121, GOBRD14: 9;

            

             A128: ((G * (i2,j2)) `2 ) <= (s `2 ) by A69, A79, A72, A116, A119, A120, A123, JORDAN9: 17;

            

             A129: (s `1 ) <= ((G * ((i2 + 1),j2)) `1 ) by A69, A79, A72, A116, A119, A120, A123, JORDAN9: 17;

            

             A130: ((G * (i2,j2)) `1 ) <= (s `1 ) by A69, A79, A72, A116, A119, A120, A123, JORDAN9: 17;

            

             A131: (c `2 ) <= ((G * (i2,(j2 + 1))) `2 ) by A64, A79, A72, A116, A119, A120, A123, JORDAN9: 17;

            ((G * (i2,j2)) `1 ) <= (c `1 ) by A64, A79, A72, A116, A119, A120, A123, JORDAN9: 17;

            then ( dist (s,c)) <= ((((G * ((i2 + 1),j2)) `1 ) - ((G * (i2,j2)) `1 )) + (((G * (i2,(j2 + 1))) `2 ) - ((G * (i2,j2)) `2 ))) by A124, A126, A131, A130, A129, A128, A125, TOPREAL6: 95;

            hence contradiction by A28, A48, A66, A67, A51, A52, A118, A122, A127, A117, XXREAL_0: 2;

          end;

            suppose

             A132: i1 = i2 & j1 = (j2 + 1);

            then 1 < i1 by A54, A55, A58, A59, A60, A61, JORDAN10: 2;

            then

             A133: 1 <= (i1 -' 1) by NAT_D: 49;

            

             A134: (i1 -' 1) <= ( len G) by A76, NAT_D: 44;

            then

             A135: [(i1 -' 1), j2] in ( Indices G) by A68, A70, A133, MATRIX_0: 30;

            

             A136: [(i1 -' 1), (j2 + 1)] in ( Indices G) by A79, A73, A132, A133, A134, MATRIX_0: 30;

            then

             A137: ( dist ((G * ((i1 -' 1),j2)),(G * ((i1 -' 1),(j2 + 1))))) = (((G * ((i1 -' 1),(j2 + 1))) `2 ) - ((G * ((i1 -' 1),j2)) `2 )) by A135, GOBRD14: 6;

            

             A138: ( dist ((G * ((i1 -' 1),j2)),(G * ((i1 -' 1),(j2 + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ k)) by A135, A136, GOBRD14: 9;

            

             A139: (j2 + 1) <= ( width G) by A58, A132, MATRIX_0: 32;

            

             A140: ((i1 -' 1) + 1) = i1 by A133, NAT_D: 43;

            then

             A141: [((i1 -' 1) + 1), j2] in ( Indices G) by A63, A68, A76, A70, MATRIX_0: 30;

            then

             A142: ( dist ((G * ((i1 -' 1),j2)),(G * (((i1 -' 1) + 1),j2)))) = (((G * (((i1 -' 1) + 1),j2)) `1 ) - ((G * ((i1 -' 1),j2)) `1 )) by A135, GOBRD14: 5;

            

             A143: ( right_cell (f,i,G)) = ( cell (G,(i1 -' 1),j2)) by A54, A55, A57, A58, A59, A60, A61, A75, A71, A132, GOBRD13:def 2;

            then

             A144: (c `1 ) <= ((G * (((i1 -' 1) + 1),j2)) `1 ) by A64, A68, A76, A139, A133, A140, JORDAN9: 17;

            

             A145: (s `2 ) <= ((G * ((i1 -' 1),(j2 + 1))) `2 ) by A69, A68, A76, A139, A133, A140, A143, JORDAN9: 17;

            

             A146: ((G * ((i1 -' 1),j2)) `2 ) <= (s `2 ) by A69, A68, A76, A139, A133, A140, A143, JORDAN9: 17;

            

             A147: (s `1 ) <= ((G * (((i1 -' 1) + 1),j2)) `1 ) by A69, A68, A76, A139, A133, A140, A143, JORDAN9: 17;

            

             A148: ((G * ((i1 -' 1),j2)) `1 ) <= (s `1 ) by A69, A68, A76, A139, A133, A140, A143, JORDAN9: 17;

            

             A149: (c `2 ) <= ((G * ((i1 -' 1),(j2 + 1))) `2 ) by A64, A68, A76, A139, A133, A140, A143, JORDAN9: 17;

            

             A150: ((G * ((i1 -' 1),j2)) `2 ) <= (c `2 ) by A64, A68, A76, A139, A133, A140, A143, JORDAN9: 17;

            

             A151: ( dist ((G * ((i1 -' 1),j2)),(G * (((i1 -' 1) + 1),j2)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ k)) by A135, A141, GOBRD14: 10;

            ((G * ((i1 -' 1),j2)) `1 ) <= (c `1 ) by A64, A68, A76, A139, A133, A140, A143, JORDAN9: 17;

            then ( dist (s,c)) <= ((((G * (((i1 -' 1) + 1),j2)) `1 ) - ((G * ((i1 -' 1),j2)) `1 )) + (((G * ((i1 -' 1),(j2 + 1))) `2 ) - ((G * ((i1 -' 1),j2)) `2 ))) by A144, A150, A149, A148, A147, A146, A145, TOPREAL6: 95;

            hence contradiction by A28, A48, A66, A67, A51, A52, A142, A137, A138, A151, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

        suppose p = |[w, q]|;

        then

         A152: (p `2 ) = q by EUCLID: 52;

        

         A153: ex S be Real_Sequence of 2 st S is convergent & (for x be Nat holds (S . x) in (( Upper_Appr C) . x)) & p = ( lim S)

        proof

          set R = { (( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) `2 ) where n be Nat : 0 < n };

          R c= REAL

          proof

            let x be object;

            assume x in R;

            then ex n be Nat st x = (( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) `2 ) & 0 < n;

            hence thesis by XREAL_0:def 1;

          end;

          then

          reconsider R as Subset of REAL ;

          deffunc f( Nat) = ( UMP ( Upper_Arc ( L~ ( Cage (C,$1)))));

          reconsider pp = p as Element of ( REAL 2) by EUCLID: 22;

          reconsider p1 = p as Element of ( TOP-REAL 2);

          

           A154: for x be Element of NAT holds f(x) is Element of ( REAL 2) by EUCLID: 22;

          consider S be sequence of ( REAL 2) such that

           A155: for n be Element of NAT holds (S . n) = f(n) from FUNCT_2:sch 9( A154);

          the carrier of ( TOP-REAL 2) = ( REAL 2) by EUCLID: 22;

          then

          reconsider SS = S as Real_Sequence of 2;

          take SS;

          

           A156: R is bounded_below

          proof

            take q;

            let r be ExtReal;

            assume r in R;

            then ex n be Nat st r = (( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) `2 ) & 0 < n;

            then r in ( proj2 .: (H /\ U)) by A12;

            hence thesis by A10, SEQ_4:def 2;

          end;

          

           A157: (( UMP ( Upper_Arc ( L~ ( Cage (C,1))))) `2 ) in R;

          

           A158: for r be Real st 0 < r holds ex n be Nat st for m be Nat st n <= m holds |.((S . m) - pp).| < r

          proof

            

             A159: for s be Real st 0 < s holds ex r be Real st r in R & r < (q + s)

            proof

              let s be Real;

              assume 0 < s;

              then

              consider r be Real such that

               A160: r in ( proj2 .: (H /\ U)) and

               A161: r < (q + s) by A10, A19, SEQ_4:def 2;

              take r;

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

               A162: x in (H /\ U) and

               A163: ( proj2 . x) = r by A160, Lm1;

              x in U by A162, XBOOLE_0:def 4;

              then

              consider n be Nat such that

               A164: x = ( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) and

               A165: 0 < n;

              r = (( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) `2 ) by A163, A164, PSCOMP_1:def 6;

              hence thesis by A161, A165;

            end;

            let r be Real;

            assume 0 < r;

            then

            consider v be Real such that

             A166: v in R and

             A167: v < (( lower_bound R) + r) by A157, A156, SEQ_4:def 2;

            

             A168: (v - ( lower_bound R)) < ((( lower_bound R) + r) - ( lower_bound R)) by A167, XREAL_1: 14;

            consider n be Nat such that

             A169: v = (( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) `2 ) and

             A170: 0 < n by A166;

            take n;

            let m be Nat;

            reconsider Sm = (S . m) as Element of ( TOP-REAL 2) by EUCLID: 22;

            

             A171: m in NAT by ORDINAL1:def 12;

            assume

             A172: n <= m;

            then (( UMP ( Upper_Arc ( L~ ( Cage (C,m))))) `2 ) <= (( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) `2 ) by A170, Th27;

            then (Sm `2 ) <= v by A155, A169, A171;

            then

             A173: ((Sm `2 ) - (p `2 )) <= (v - (p `2 )) by XREAL_1: 13;

            reconsider SSm = Sm as Point of ( TOP-REAL 2);

            

             A174: (SSm - p1) = ((S . m) - pp);

            

             A175: (S . m) = ( UMP ( Upper_Arc ( L~ ( Cage (C,m))))) by A155, A171;

            then (Sm `1 ) = w by A5;

            then |.((Sm `1 ) - (p `1 )).| = 0 by A11, ABSVALUE:def 1;

            then

             A176: |.((S . m) - pp).| <= ( 0 + |.((Sm `2 ) - (p `2 )).|) by A174, JGRAPH_1: 32;

             0 < ((Sm `2 ) - (p `2 )) by A170, A175, A172, Th23, XREAL_1: 50;

            then

             A177: |.((S . m) - pp).| <= ((Sm `2 ) - (p `2 )) by A176, ABSVALUE:def 1;

            for r be Real st r in R holds q <= r

            proof

              let r be Real;

              assume r in R;

              then ex n be Nat st r = (( UMP ( Upper_Arc ( L~ ( Cage (C,n))))) `2 ) & 0 < n;

              then r in ( proj2 .: (H /\ U)) by A12;

              hence thesis by A10, SEQ_4:def 2;

            end;

            then ( lower_bound R) = q by A157, A156, A159, SEQ_4:def 2;

            then ((Sm `2 ) - (p `2 )) < r by A152, A168, A173, XXREAL_0: 2;

            hence thesis by A177, XXREAL_0: 2;

          end;

          thus

           A178: SS is convergent

          proof

            take p;

            let r be Real;

            assume 0 < r;

            then

            consider n be Nat such that

             A179: for m be Nat st n <= m holds |.((S . m) - pp).| < r by A158;

            take n;

            let m be Nat;

            assume n <= m;

            then |.((S . m) - pp).| < r by A179;

            hence |.((SS . m) - p).| < r;

          end;

          hereby

            let x be Nat;

            

             A180: x in NAT by ORDINAL1:def 12;

            

             A181: (( Upper_Appr C) . x) = ( Upper_Arc ( L~ ( Cage (C,x)))) by JORDAN19:def 1;

            (S . x) = ( UMP ( Upper_Arc ( L~ ( Cage (C,x))))) by A155, A180;

            hence (SS . x) in (( Upper_Appr C) . x) by A181, JORDAN21: 30;

          end;

          for r be Real st 0 < r holds ex n st for m st n <= m holds |.((SS . m) - p).| < r

          proof

            let r be Real;

            assume 0 < r;

            then

            consider n be Nat such that

             A182: for m be Nat st n <= m holds |.((S . m) - pp).| < r by A158;

            take n;

            let m be Nat;

            assume n <= m;

            then |.((S . m) - pp).| < r by A182;

            hence |.((SS . m) - p).| < r;

          end;

          hence p = ( lim SS) by A178, TOPRNS_1:def 9;

        end;

        ( North_Arc C) = ( Lim_inf ( Upper_Appr C)) by JORDAN19:def 3;

        hence thesis by A153, KURATO_2: 21;

      end;

    end;

    theorem :: JORDAN22:34

    

     Th34: ( LMP C) in ( South_Arc C)

    proof

      set w = ((( W-bound C) + ( E-bound C)) / 2);

      set p = ( LMP C);

      set U = { ( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) where n be Nat : 0 < n };

      set n0 = ( S-bound ( L~ ( Cage (C,1))));

      set H = ( LSeg (p, |[w, n0]|));

      

       A1: ( |[w, ( S-bound C)]| `1 ) = w by EUCLID: 52;

      

       A2: ( |[w, n0]| `1 ) = w by EUCLID: 52;

      { ( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) where n be Nat : 0 < n } c= the carrier of ( TOP-REAL 2)

      proof

        let x be object;

        assume x in { ( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) where n be Nat : 0 < n };

        then ex n be Nat st x = ( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) & 0 < n;

        hence thesis;

      end;

      then

      reconsider U as Subset of ( TOP-REAL 2);

      set q = ( upper_bound ( proj2 .: (H /\ U)));

      set S = ( LSeg ( |[w, q]|, |[w, n0]|));

      

       A3: ( |[w, ( S-bound C)]| `2 ) = ( S-bound C) by EUCLID: 52;

      

       A4: ( |[w, n0]| `2 ) = n0 by EUCLID: 52;

      

       A5: for n be Nat holds (( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) `1 ) = w

      proof

        let n be Nat;

        

         A6: (( W-bound ( L~ ( Cage (C,n)))) + ( E-bound ( L~ ( Cage (C,n))))) = (( W-bound C) + ( E-bound C)) by JORDAN1G: 33;

        

        thus (( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) `1 ) = ((( W-bound ( Lower_Arc ( L~ ( Cage (C,n))))) + ( E-bound ( Lower_Arc ( L~ ( Cage (C,n)))))) / 2) by EUCLID: 52

        .= ((( W-bound ( L~ ( Cage (C,n)))) + ( E-bound ( Lower_Arc ( L~ ( Cage (C,n)))))) / 2) by JORDAN21: 19

        .= w by A6, JORDAN21: 20;

      end;

      

       A7: (p `2 ) >= (( LMP ( Lower_Arc ( L~ ( Cage (C,1))))) `2 ) by Th24;

      

       A8: (( LSeg (p, |[w, ( S-bound C)]|)) /\ C) = {p} by JORDAN21: 35;

      

       A9: (( LMP ( Lower_Arc ( L~ ( Cage (C,1))))) `2 ) >= n0 by JORDAN21: 48;

      (H /\ U) is bounded by TOPREAL6: 89;

      then ( proj2 .: (H /\ U)) is real-bounded by JCT_MISC: 14;

      then

       A10: ( proj2 .: (H /\ U)) is bounded_above;

      

       A11: (p `1 ) = w by EUCLID: 52;

      

       A12: for n be Nat st 0 < n holds (( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) `2 ) in ( proj2 .: (H /\ U))

      proof

        let n be Nat;

        set f = ( Cage (C,n));

        set s = ( LMP ( Lower_Arc ( L~ f)));

        assume

         A13: 0 < n;

        then

         A14: s in U;

        ( 0 + 1) <= n by A13, NAT_1: 13;

        then n = 1 or n > 1 by XXREAL_0: 1;

        then

         A15: ( S-bound ( L~ ( Cage (C,n)))) >= ( S-bound ( L~ ( Cage (C,1)))) by JORDAN1A: 69;

        ( S-bound ( L~ f)) <= (s `2 ) by JORDAN21: 48;

        then

         A16: (s `2 ) >= n0 by A15, XXREAL_0: 2;

        

         A17: (s `1 ) = w by A5;

        (p `2 ) >= (s `2 ) by A13, Th24;

        then s in H by A2, A4, A11, A16, A17, GOBOARD7: 7;

        then

         A18: s in (H /\ U) by A14, XBOOLE_0:def 4;

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

        hence thesis by A18, FUNCT_2: 35;

      end;

      then

       A19: (( LMP ( Lower_Arc ( L~ ( Cage (C,1))))) `2 ) in ( proj2 .: (H /\ U));

      then q >= (( LMP ( Lower_Arc ( L~ ( Cage (C,1))))) `2 ) by A10, SEQ_4:def 1;

      then

       A20: q >= n0 by A9, XXREAL_0: 2;

      

       A21: ( |[w, q]| `1 ) = w by EUCLID: 52;

      then

       A22: S is vertical by A2, SPPOL_1: 16;

      

       A23: |[w, q]| in S by RLTOPSP1: 68;

      

       A24: ( |[w, q]| `2 ) = q by EUCLID: 52;

      per cases ;

        suppose

         A25: p <> |[w, q]|;

        consider S9,C9 be Subset of ( TopSpaceMetr ( Euclid 2)) such that

         A26: S = S9 and

         A27: C = C9 and

         A28: ( dist_min (S,C)) = ( min_dist_min (S9,C9)) by JORDAN1K:def 1;

        

         A29: S9 is compact by A26, Lm4, COMPTS_1: 23;

        

         A30: C9 is compact by A27, Lm4, COMPTS_1: 23;

         A31:

        now

          assume

           A32: (p `2 ) <= q;

          per cases by A32, XXREAL_0: 1;

            suppose (p `2 ) = q;

            hence contradiction by A25, EUCLID: 52;

          end;

            suppose (p `2 ) < q;

            then 0 < (q - (p `2 )) by XREAL_1: 50;

            then

            consider r be Real such that

             A33: r in ( proj2 .: (H /\ U)) and

             A34: (q - (q - (p `2 ))) < r by A10, A19, SEQ_4:def 1;

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

             A35: t in (H /\ U) and

             A36: ( proj2 . t) = r by A33, Lm1;

            

             A37: t in H by A35, XBOOLE_0:def 4;

            

             A38: (p `2 ) >= n0 by A9, A7, XXREAL_0: 2;

            (t `2 ) = r by A36, PSCOMP_1:def 6;

            hence contradiction by A4, A34, A38, A37, TOPREAL1: 4;

          end;

        end;

        S misses C

        proof

          assume S meets C;

          then

          consider x be object such that

           A39: x in S and

           A40: x in C by XBOOLE_0: 3;

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

          

           A41: (x `2 ) >= ( S-bound C) by A40, PSCOMP_1: 24;

          

           A42: (x `1 ) = w by A21, A23, A22, A39, SPPOL_1:def 3;

          

           A43: q >= (x `2 ) by A4, A24, A20, A39, TOPREAL1: 4;

          then (p `2 ) > (x `2 ) by A31, XXREAL_0: 2;

          then x in ( LSeg (p, |[w, ( S-bound C)]|)) by A1, A3, A11, A41, A42, GOBOARD7: 7;

          then x in {p} by A8, A40, XBOOLE_0:def 4;

          hence contradiction by A31, A43, TARSKI:def 1;

        end;

        then ( dist_min (S,C)) > 0 by A26, A27, A28, A29, A30, JGRAPH_1: 38;

        then (( dist_min (S,C)) / 2) > 0 ;

        then

        consider k be Nat such that

         A44: 1 < k and

         A45: ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (1,2)))) < (( dist_min (S,C)) / 2) and

         A46: ( dist ((( Gauge (C,k)) * (1,1)),(( Gauge (C,k)) * (2,1)))) < (( dist_min (S,C)) / 2) by GOBRD14: 11;

        set f = ( Cage (C,k)), G = ( Gauge (C,k));

        set s = ( LMP ( Lower_Arc ( L~ f)));

        

         A47: (s `2 ) >= ( S-bound ( L~ f)) by JORDAN21: 48;

        

         A48: (( dist ((G * (1,1)),(G * ((1 + 1),1)))) + ( dist ((G * (1,1)),(G * (1,(1 + 1)))))) < ((( dist_min (S,C)) / 2) + (( dist_min (S,C)) / 2)) by A45, A46, XREAL_1: 8;

        ( S-bound ( L~ ( Cage (C,k)))) >= ( S-bound ( L~ ( Cage (C,1)))) by A44, JORDAN1A: 69;

        then

         A49: (s `2 ) >= n0 by A47, XXREAL_0: 2;

        (s `2 ) in ( proj2 .: (H /\ U)) by A12, A44;

        then

         A50: q >= (s `2 ) by A10, SEQ_4:def 1;

         [1, (1 + 1)] in ( Indices G) by Th6;

        then

         A51: ( dist ((G * (1,1)),(G * (1,(1 + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ k)) by Th5, GOBRD14: 9;

         [(1 + 1), 1] in ( Indices G) by Th7;

        then

         A52: ( dist ((G * (1,1)),(G * ((1 + 1),1)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ k)) by Th5, GOBRD14: 10;

        

         A53: s in ( Lower_Arc ( L~ f)) by JORDAN21: 31;

        ( Lower_Arc ( L~ f)) c= ( L~ f) by JORDAN6: 61;

        then

        consider i be Nat such that

         A54: 1 <= i and

         A55: (i + 1) <= ( len f) and

         A56: s in ( LSeg (f,i)) by A53, SPPOL_2: 13;

        

         A57: f is_sequence_on G by JORDAN9:def 1;

        then

        consider i1,j1,i2,j2 be Nat such that

         A58: [i1, j1] in ( Indices G) and

         A59: (f /. i) = (G * (i1,j1)) and

         A60: [i2, j2] in ( Indices G) and

         A61: (f /. (i + 1)) = (G * (i2,j2)) and

         A62: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A54, A55, JORDAN8: 3;

        

         A63: 1 <= i1 by A58, MATRIX_0: 32;

        ( right_cell (f,i,G)) meets C by A54, A55, JORDAN9: 31;

        then

        consider c be object such that

         A64: c in ( right_cell (f,i,G)) and

         A65: c in C by XBOOLE_0: 3;

        reconsider c as Point of ( TOP-REAL 2) by A65;

        reconsider s9 = s, c9 = c as Point of ( Euclid 2) by EUCLID: 67;

        (s `1 ) = w by A5;

        then s in S by A2, A4, A21, A24, A49, A50, GOBOARD7: 7;

        then

         A66: ( min_dist_min (S9,C9)) <= ( dist (s9,c9)) by A26, A27, A29, A30, A65, WEIERSTR: 34;

        

         A67: ( dist (s9,c9)) = ( dist (s,c)) by TOPREAL6:def 1;

        

         A68: 1 <= j2 by A60, MATRIX_0: 32;

        (( left_cell (f,i,G)) /\ ( right_cell (f,i,G))) = ( LSeg (f,i)) by A54, A55, A57, GOBRD13: 29;

        then

         A69: s in ( right_cell (f,i,G)) by A56, XBOOLE_0:def 4;

        

         A70: j2 <= ( width G) by A60, MATRIX_0: 32;

        

         A71: ((j2 + 1) + 1) <> j2;

        

         A72: 1 <= i2 by A60, MATRIX_0: 32;

        

         A73: j1 <= ( width G) by A58, MATRIX_0: 32;

        

         A74: 1 <= (j1 + 1) by NAT_1: 11;

        

         A75: (i1 + 1) <> (i1 + 0 );

        

         A76: i1 <= ( len G) by A58, MATRIX_0: 32;

        

         A77: i2 <= ( len G) by A60, MATRIX_0: 32;

        

         A78: ((i2 + 1) + 1) <> i2;

        

         A79: 1 <= j1 by A58, MATRIX_0: 32;

        

         A80: 1 <= (i1 + 1) by NAT_1: 11;

        now

          per cases by A62;

            suppose

             A81: i1 = i2 & (j1 + 1) = j2;

            then

             A82: ( dist ((G * (i1,j1)),(G * (i1,(j1 + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ k)) by A58, A60, GOBRD14: 9;

            

             A83: ( dist ((G * (i1,j1)),(G * (i1,(j1 + 1))))) = (((G * (i1,(j1 + 1))) `2 ) - ((G * (i1,j1)) `2 )) by A58, A60, A81, GOBRD14: 6;

            i1 < ( len G) by A54, A55, A58, A59, A60, A61, A81, JORDAN10: 1;

            then

             A84: (i1 + 1) <= ( len G) by NAT_1: 13;

            then

             A85: [(i1 + 1), j1] in ( Indices G) by A79, A80, A73, MATRIX_0: 30;

            then

             A86: ( dist ((G * (i1,j1)),(G * ((i1 + 1),j1)))) = (((G * ((i1 + 1),j1)) `1 ) - ((G * (i1,j1)) `1 )) by A58, GOBRD14: 5;

            

             A87: ( dist ((G * (i1,j1)),(G * ((i1 + 1),j1)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ k)) by A58, A85, GOBRD14: 10;

            

             A88: (j1 + 1) <= ( width G) by A60, A81, MATRIX_0: 32;

            

             A89: ( right_cell (f,i,G)) = ( cell (G,i1,j1)) by A54, A55, A57, A58, A59, A60, A61, A75, A71, A81, GOBRD13:def 2;

            then

             A90: (c `1 ) <= ((G * ((i1 + 1),j1)) `1 ) by A64, A63, A79, A88, A84, JORDAN9: 17;

            

             A91: (s `2 ) <= ((G * (i1,(j1 + 1))) `2 ) by A69, A63, A79, A88, A84, A89, JORDAN9: 17;

            

             A92: ((G * (i1,j1)) `2 ) <= (s `2 ) by A69, A63, A79, A88, A84, A89, JORDAN9: 17;

            

             A93: (s `1 ) <= ((G * ((i1 + 1),j1)) `1 ) by A69, A63, A79, A88, A84, A89, JORDAN9: 17;

            

             A94: ((G * (i1,j1)) `1 ) <= (s `1 ) by A69, A63, A79, A88, A84, A89, JORDAN9: 17;

            

             A95: (c `2 ) <= ((G * (i1,(j1 + 1))) `2 ) by A64, A63, A79, A88, A84, A89, JORDAN9: 17;

            

             A96: ((G * (i1,j1)) `2 ) <= (c `2 ) by A64, A63, A79, A88, A84, A89, JORDAN9: 17;

            ((G * (i1,j1)) `1 ) <= (c `1 ) by A64, A63, A79, A88, A84, A89, JORDAN9: 17;

            then ( dist (s,c)) <= ((((G * ((i1 + 1),j1)) `1 ) - ((G * (i1,j1)) `1 )) + (((G * (i1,(j1 + 1))) `2 ) - ((G * (i1,j1)) `2 ))) by A90, A96, A95, A94, A93, A92, A91, TOPREAL6: 95;

            hence contradiction by A28, A48, A66, A67, A51, A52, A86, A83, A82, A87, XXREAL_0: 2;

          end;

            suppose

             A97: (i1 + 1) = i2 & j1 = j2;

            then 1 < j1 by A54, A55, A58, A59, A60, A61, JORDAN10: 3;

            then

             A98: 1 <= (j1 -' 1) by NAT_D: 49;

            then

             A99: ((j1 -' 1) + 1) = j1 by NAT_D: 43;

            

             A100: (j1 -' 1) <= ( width G) by A73, NAT_D: 44;

            then

             A101: [i1, (j1 -' 1)] in ( Indices G) by A63, A76, A98, MATRIX_0: 30;

            then

             A102: ( dist ((G * (i1,(j1 -' 1))),(G * (i1,((j1 -' 1) + 1))))) = (((G * (i1,((j1 -' 1) + 1))) `2 ) - ((G * (i1,(j1 -' 1))) `2 )) by A58, A99, GOBRD14: 6;

            

             A103: [(i1 + 1), (j1 -' 1)] in ( Indices G) by A72, A77, A97, A98, A100, MATRIX_0: 30;

            then

             A104: ( dist ((G * (i1,(j1 -' 1))),(G * ((i1 + 1),(j1 -' 1))))) = (((G * ((i1 + 1),(j1 -' 1))) `1 ) - ((G * (i1,(j1 -' 1))) `1 )) by A101, GOBRD14: 5;

            

             A105: ( dist ((G * (i1,(j1 -' 1))),(G * (i1,((j1 -' 1) + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ k)) by A58, A99, A101, GOBRD14: 9;

            

             A106: ( dist ((G * (i1,(j1 -' 1))),(G * ((i1 + 1),(j1 -' 1))))) = ((( E-bound C) - ( W-bound C)) / (2 |^ k)) by A101, A103, GOBRD14: 10;

            

             A107: (i1 + 1) <= ( len G) by A60, A97, MATRIX_0: 32;

            

             A108: ( right_cell (f,i,G)) = ( cell (G,i1,(j1 -' 1))) by A54, A55, A57, A58, A59, A60, A61, A75, A78, A97, GOBRD13:def 2;

            then

             A109: (c `1 ) <= ((G * ((i1 + 1),(j1 -' 1))) `1 ) by A64, A63, A73, A107, A98, A99, JORDAN9: 17;

            

             A110: (s `2 ) <= ((G * (i1,((j1 -' 1) + 1))) `2 ) by A69, A63, A73, A107, A98, A99, A108, JORDAN9: 17;

            

             A111: ((G * (i1,(j1 -' 1))) `2 ) <= (s `2 ) by A69, A63, A73, A107, A98, A99, A108, JORDAN9: 17;

            

             A112: (s `1 ) <= ((G * ((i1 + 1),(j1 -' 1))) `1 ) by A69, A63, A73, A107, A98, A99, A108, JORDAN9: 17;

            

             A113: ((G * (i1,(j1 -' 1))) `1 ) <= (s `1 ) by A69, A63, A73, A107, A98, A99, A108, JORDAN9: 17;

            

             A114: (c `2 ) <= ((G * (i1,((j1 -' 1) + 1))) `2 ) by A64, A63, A73, A107, A98, A99, A108, JORDAN9: 17;

            

             A115: ((G * (i1,(j1 -' 1))) `2 ) <= (c `2 ) by A64, A63, A73, A107, A98, A99, A108, JORDAN9: 17;

            ((G * (i1,(j1 -' 1))) `1 ) <= (c `1 ) by A64, A63, A73, A107, A98, A99, A108, JORDAN9: 17;

            then ( dist (s,c)) <= ((((G * ((i1 + 1),(j1 -' 1))) `1 ) - ((G * (i1,(j1 -' 1))) `1 )) + (((G * (i1,((j1 -' 1) + 1))) `2 ) - ((G * (i1,(j1 -' 1))) `2 ))) by A109, A115, A114, A113, A112, A111, A110, TOPREAL6: 95;

            hence contradiction by A28, A48, A66, A67, A51, A52, A104, A102, A105, A106, XXREAL_0: 2;

          end;

            suppose

             A116: i1 = (i2 + 1) & j1 = j2;

            then

             A117: ( dist ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ k)) by A58, A60, GOBRD14: 10;

            

             A118: ( dist ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = (((G * ((i2 + 1),j2)) `1 ) - ((G * (i2,j2)) `1 )) by A58, A60, A116, GOBRD14: 5;

            

             A119: (i2 + 1) <= ( len G) by A58, A116, MATRIX_0: 32;

            j1 < ( width G) by A54, A55, A58, A59, A60, A61, A116, JORDAN10: 4;

            then

             A120: (j1 + 1) <= ( width G) by NAT_1: 13;

            then

             A121: [i2, (j2 + 1)] in ( Indices G) by A72, A74, A77, A116, MATRIX_0: 30;

            then

             A122: ( dist ((G * (i2,j2)),(G * (i2,(j2 + 1))))) = (((G * (i2,(j2 + 1))) `2 ) - ((G * (i2,j2)) `2 )) by A60, GOBRD14: 6;

            

             A123: ( right_cell (f,i,G)) = ( cell (G,i2,j2)) by A54, A55, A57, A58, A59, A60, A61, A75, A78, A116, GOBRD13:def 2;

            then

             A124: (c `1 ) <= ((G * ((i2 + 1),j2)) `1 ) by A64, A79, A72, A116, A119, A120, JORDAN9: 17;

            

             A125: (s `2 ) <= ((G * (i2,(j2 + 1))) `2 ) by A69, A79, A72, A116, A119, A120, A123, JORDAN9: 17;

            

             A126: ((G * (i2,j2)) `2 ) <= (c `2 ) by A64, A79, A72, A116, A119, A120, A123, JORDAN9: 17;

            

             A127: ( dist ((G * (i2,j2)),(G * (i2,(j2 + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ k)) by A60, A121, GOBRD14: 9;

            

             A128: ((G * (i2,j2)) `2 ) <= (s `2 ) by A69, A79, A72, A116, A119, A120, A123, JORDAN9: 17;

            

             A129: (s `1 ) <= ((G * ((i2 + 1),j2)) `1 ) by A69, A79, A72, A116, A119, A120, A123, JORDAN9: 17;

            

             A130: ((G * (i2,j2)) `1 ) <= (s `1 ) by A69, A79, A72, A116, A119, A120, A123, JORDAN9: 17;

            

             A131: (c `2 ) <= ((G * (i2,(j2 + 1))) `2 ) by A64, A79, A72, A116, A119, A120, A123, JORDAN9: 17;

            ((G * (i2,j2)) `1 ) <= (c `1 ) by A64, A79, A72, A116, A119, A120, A123, JORDAN9: 17;

            then ( dist (s,c)) <= ((((G * ((i2 + 1),j2)) `1 ) - ((G * (i2,j2)) `1 )) + (((G * (i2,(j2 + 1))) `2 ) - ((G * (i2,j2)) `2 ))) by A124, A126, A131, A130, A129, A128, A125, TOPREAL6: 95;

            hence contradiction by A28, A48, A66, A67, A51, A52, A118, A122, A127, A117, XXREAL_0: 2;

          end;

            suppose

             A132: i1 = i2 & j1 = (j2 + 1);

            then 1 < i1 by A54, A55, A58, A59, A60, A61, JORDAN10: 2;

            then

             A133: 1 <= (i1 -' 1) by NAT_D: 49;

            

             A134: (i1 -' 1) <= ( len G) by A76, NAT_D: 44;

            then

             A135: [(i1 -' 1), j2] in ( Indices G) by A68, A70, A133, MATRIX_0: 30;

            

             A136: [(i1 -' 1), (j2 + 1)] in ( Indices G) by A79, A73, A132, A133, A134, MATRIX_0: 30;

            then

             A137: ( dist ((G * ((i1 -' 1),j2)),(G * ((i1 -' 1),(j2 + 1))))) = (((G * ((i1 -' 1),(j2 + 1))) `2 ) - ((G * ((i1 -' 1),j2)) `2 )) by A135, GOBRD14: 6;

            

             A138: ( dist ((G * ((i1 -' 1),j2)),(G * ((i1 -' 1),(j2 + 1))))) = ((( N-bound C) - ( S-bound C)) / (2 |^ k)) by A135, A136, GOBRD14: 9;

            

             A139: (j2 + 1) <= ( width G) by A58, A132, MATRIX_0: 32;

            

             A140: ((i1 -' 1) + 1) = i1 by A133, NAT_D: 43;

            then

             A141: [((i1 -' 1) + 1), j2] in ( Indices G) by A63, A68, A76, A70, MATRIX_0: 30;

            then

             A142: ( dist ((G * ((i1 -' 1),j2)),(G * (((i1 -' 1) + 1),j2)))) = (((G * (((i1 -' 1) + 1),j2)) `1 ) - ((G * ((i1 -' 1),j2)) `1 )) by A135, GOBRD14: 5;

            

             A143: ( right_cell (f,i,G)) = ( cell (G,(i1 -' 1),j2)) by A54, A55, A57, A58, A59, A60, A61, A75, A71, A132, GOBRD13:def 2;

            then

             A144: (c `1 ) <= ((G * (((i1 -' 1) + 1),j2)) `1 ) by A64, A68, A76, A139, A133, A140, JORDAN9: 17;

            

             A145: (s `2 ) <= ((G * ((i1 -' 1),(j2 + 1))) `2 ) by A69, A68, A76, A139, A133, A140, A143, JORDAN9: 17;

            

             A146: ((G * ((i1 -' 1),j2)) `2 ) <= (s `2 ) by A69, A68, A76, A139, A133, A140, A143, JORDAN9: 17;

            

             A147: (s `1 ) <= ((G * (((i1 -' 1) + 1),j2)) `1 ) by A69, A68, A76, A139, A133, A140, A143, JORDAN9: 17;

            

             A148: ((G * ((i1 -' 1),j2)) `1 ) <= (s `1 ) by A69, A68, A76, A139, A133, A140, A143, JORDAN9: 17;

            

             A149: (c `2 ) <= ((G * ((i1 -' 1),(j2 + 1))) `2 ) by A64, A68, A76, A139, A133, A140, A143, JORDAN9: 17;

            

             A150: ((G * ((i1 -' 1),j2)) `2 ) <= (c `2 ) by A64, A68, A76, A139, A133, A140, A143, JORDAN9: 17;

            

             A151: ( dist ((G * ((i1 -' 1),j2)),(G * (((i1 -' 1) + 1),j2)))) = ((( E-bound C) - ( W-bound C)) / (2 |^ k)) by A135, A141, GOBRD14: 10;

            ((G * ((i1 -' 1),j2)) `1 ) <= (c `1 ) by A64, A68, A76, A139, A133, A140, A143, JORDAN9: 17;

            then ( dist (s,c)) <= ((((G * (((i1 -' 1) + 1),j2)) `1 ) - ((G * ((i1 -' 1),j2)) `1 )) + (((G * ((i1 -' 1),(j2 + 1))) `2 ) - ((G * ((i1 -' 1),j2)) `2 ))) by A144, A150, A149, A148, A147, A146, A145, TOPREAL6: 95;

            hence contradiction by A28, A48, A66, A67, A51, A52, A142, A137, A138, A151, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

        suppose p = |[w, q]|;

        then

         A152: (p `2 ) = q by EUCLID: 52;

        

         A153: ex S be Real_Sequence of 2 st S is convergent & (for x be Nat holds (S . x) in (( Lower_Appr C) . x)) & p = ( lim S)

        proof

          set R = { (( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) `2 ) where n be Nat : 0 < n };

          R c= REAL

          proof

            let x be object;

            assume x in R;

            then ex n be Nat st x = (( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) `2 ) & 0 < n;

            hence thesis by XREAL_0:def 1;

          end;

          then

          reconsider R as Subset of REAL ;

          deffunc g( Nat) = ( LMP ( Lower_Arc ( L~ ( Cage (C,$1)))));

          reconsider pp = p as Element of ( REAL 2) by EUCLID: 22;

          

           A154: for x be Element of NAT holds g(x) is Element of ( REAL 2) by EUCLID: 22;

          consider S be sequence of ( REAL 2) such that

           A155: for n be Element of NAT holds (S . n) = g(n) from FUNCT_2:sch 9( A154);

          the carrier of ( TOP-REAL 2) = ( REAL 2) by EUCLID: 22;

          then

          reconsider SS = S as Real_Sequence of 2;

          take SS;

          

           A156: R is bounded_above

          proof

            take q;

            let r be ExtReal;

            assume r in R;

            then ex n be Nat st r = (( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) `2 ) & 0 < n;

            then r in ( proj2 .: (H /\ U)) by A12;

            hence thesis by A10, SEQ_4:def 1;

          end;

          

           A157: (( LMP ( Lower_Arc ( L~ ( Cage (C,1))))) `2 ) in R;

          

           A158: for r be Real st 0 < r holds ex n be Nat st for m be Nat st n <= m holds |.((S . m) - pp).| < r

          proof

            

             A159: for s be Real st 0 < s holds ex r be Real st r in R & (q - s) < r

            proof

              let s be Real;

              assume 0 < s;

              then

              consider r be Real such that

               A160: r in ( proj2 .: (H /\ U)) and

               A161: (q - s) < r by A10, A19, SEQ_4:def 1;

              take r;

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

               A162: x in (H /\ U) and

               A163: ( proj2 . x) = r by A160, Lm1;

              x in U by A162, XBOOLE_0:def 4;

              then

              consider n be Nat such that

               A164: x = ( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) and

               A165: 0 < n;

              r = (( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) `2 ) by A163, A164, PSCOMP_1:def 6;

              hence thesis by A161, A165;

            end;

            reconsider p1 = p as Element of ( TOP-REAL 2);

            let r be Real;

            assume 0 < r;

            then

            consider v be Real such that

             A166: v in R and

             A167: (( upper_bound R) - r) < v by A157, A156, SEQ_4:def 1;

            consider n be Nat such that

             A168: v = (( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) `2 ) and

             A169: 0 < n by A166;

            ((( upper_bound R) - r) + r) < (v + r) by A167, XREAL_1: 6;

            then

             A170: (( upper_bound R) - v) < ((v + r) - v) by XREAL_1: 14;

            take n;

            let m be Nat;

            

             A171: m in NAT by ORDINAL1:def 12;

            reconsider Sm = (S . m) as Point of ( TOP-REAL 2) by EUCLID: 22;

            assume

             A172: n <= m;

            then (( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) `2 ) <= (( LMP ( Lower_Arc ( L~ ( Cage (C,m))))) `2 ) by A169, Th28;

            then (Sm `2 ) >= v by A155, A168, A171;

            then

             A173: ((p `2 ) - (Sm `2 )) <= ((p `2 ) - v) by XREAL_1: 13;

            reconsider SSm = Sm as Point of ( TOP-REAL 2);

            

             A174: (SSm - p1) = ((S . m) - pp);

            

             A175: (S . m) = ( LMP ( Lower_Arc ( L~ ( Cage (C,m))))) by A155, A171;

            then (Sm `1 ) = w by A5;

            then |.((Sm `1 ) - (p `1 )).| = 0 by A11, ABSVALUE:def 1;

            then

             A176: |.((S . m) - pp).| <= ( 0 + |.((Sm `2 ) - (p `2 )).|) by A174, JGRAPH_1: 32;

             0 > ((Sm `2 ) - (p `2 )) by A169, A175, A172, Th24, XREAL_1: 49;

            then

             A177: |.((S . m) - pp).| <= ( - ((Sm `2 ) - (p `2 ))) by A176, ABSVALUE:def 1;

            for r be Real st r in R holds q >= r

            proof

              let r be Real;

              assume r in R;

              then ex n be Nat st r = (( LMP ( Lower_Arc ( L~ ( Cage (C,n))))) `2 ) & 0 < n;

              then r in ( proj2 .: (H /\ U)) by A12;

              hence thesis by A10, SEQ_4:def 1;

            end;

            then ( upper_bound R) = q by A157, A156, A159, SEQ_4:def 1;

            then ((p `2 ) - (Sm `2 )) < r by A152, A170, A173, XXREAL_0: 2;

            hence thesis by A177, XXREAL_0: 2;

          end;

          thus

           A178: SS is convergent

          proof

            take p;

            let r be Real;

            assume 0 < r;

            then

            consider n be Nat such that

             A179: for m be Nat st n <= m holds |.((S . m) - pp).| < r by A158;

            take n;

            let m be Nat;

            assume n <= m;

            then |.((S . m) - pp).| < r by A179;

            hence |.((SS . m) - p).| < r;

          end;

          hereby

            let x be Nat;

            

             A180: x in NAT by ORDINAL1:def 12;

            

             A181: (( Lower_Appr C) . x) = ( Lower_Arc ( L~ ( Cage (C,x)))) by JORDAN19:def 2;

            (S . x) = ( LMP ( Lower_Arc ( L~ ( Cage (C,x))))) by A155, A180;

            hence (SS . x) in (( Lower_Appr C) . x) by A181, JORDAN21: 31;

          end;

          for r be Real st 0 < r holds ex n st for m st n <= m holds |.((SS . m) - p).| < r

          proof

            let r be Real;

            assume 0 < r;

            then

            consider n be Nat such that

             A182: for m be Nat st n <= m holds |.((S . m) - pp).| < r by A158;

            take n;

            let m be Nat;

            assume n <= m;

            then |.((S . m) - pp).| < r by A182;

            hence |.((SS . m) - p).| < r;

          end;

          hence p = ( lim SS) by A178, TOPRNS_1:def 9;

        end;

        ( South_Arc C) = ( Lim_inf ( Lower_Appr C)) by JORDAN19:def 4;

        hence thesis by A153, KURATO_2: 21;

      end;

    end;

    theorem :: JORDAN22:35

    

     Th35: ( North_Arc C) c= C

    proof

      

       A1: ( North_Arc C) = ( Lim_inf ( Upper_Appr C)) by JORDAN19:def 3;

      reconsider OO = ( BDD C) as Subset of ( TopSpaceMetr ( Euclid 2)) by Lm4;

      let x be object;

      assume

       A2: x in ( North_Arc C);

      assume

       A3: not x in C;

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

      

       A4: x in (C ` ) by A3, SUBSET_1: 29;

      

       A5: (( BDD C) \/ ( UBD C)) = (C ` ) by JORDAN2C: 27;

      reconsider e = x as Point of ( Euclid 2) by EUCLID: 67;

      per cases by A4, A5, XBOOLE_0:def 3;

        suppose

         A6: x in ( BDD C);

        OO is open by Lm4, PRE_TOPC: 30;

        then

        consider r be Real such that

         A7: r > 0 and

         A8: ( Ball (e,r)) c= ( BDD C) by A6, TOPMETR: 15;

        consider k be Nat such that

         A9: for m be Nat st m > k holds (( Upper_Appr C) . m) meets ( Ball (e,r)) by A2, A1, A7, KURATO_2: 14;

        

         A10: ( Upper_Arc ( L~ ( Cage (C,(k + 1))))) c= ( L~ ( Cage (C,(k + 1)))) by JORDAN6: 61;

        

         A11: (( Upper_Appr C) . (k + 1)) = ( Upper_Arc ( L~ ( Cage (C,(k + 1))))) by JORDAN19:def 1;

        

         A12: (k + 0 ) < (k + 1) by XREAL_1: 8;

        ( Ball (e,r)) misses ( L~ ( Cage (C,(k + 1)))) by A8, JORDAN10: 19, XBOOLE_1: 63;

        hence thesis by A9, A12, A11, A10, XBOOLE_1: 63;

      end;

        suppose

         A13: x in ( UBD C);

        ( union ( UBD-Family C)) = ( UBD C) by JORDAN10: 14;

        then

        consider A be set such that

         A14: x in A and

         A15: A in ( UBD-Family C) by A13, TARSKI:def 4;

        ( UBD-Family C) = the set of all ( UBD ( L~ ( Cage (C,m)))) where m be Nat by JORDAN10:def 1;

        then

        consider m be Nat such that

         A16: A = ( UBD ( L~ ( Cage (C,m)))) by A15;

        reconsider OO = ( LeftComp ( Cage (C,m))) as Subset of ( TopSpaceMetr ( Euclid 2)) by Lm4;

        

         A17: OO is open by Lm4, PRE_TOPC: 30;

        x in ( LeftComp ( Cage (C,m))) by A14, A16, GOBRD14: 36;

        then

        consider r be Real such that

         A18: r > 0 and

         A19: ( Ball (e,r)) c= ( LeftComp ( Cage (C,m))) by A17, TOPMETR: 15;

        consider k be Nat such that

         A20: for m be Nat st m > k holds (( Upper_Appr C) . m) meets ( Ball (e,r)) by A2, A1, A18, KURATO_2: 14;

        thus thesis

        proof

          per cases ;

            suppose

             A21: m > k;

            

             A22: (( Upper_Appr C) . m) = ( Upper_Arc ( L~ ( Cage (C,m)))) by JORDAN19:def 1;

            

             A23: ( Upper_Arc ( L~ ( Cage (C,m)))) c= ( L~ ( Cage (C,m))) by JORDAN6: 61;

            ( Ball (e,r)) misses ( L~ ( Cage (C,m))) by A19, SPRECT_3: 26, XBOOLE_1: 63;

            hence thesis by A20, A21, A22, A23, XBOOLE_1: 63;

          end;

            suppose m <= k;

            then ( LeftComp ( Cage (C,m))) c= ( LeftComp ( Cage (C,k))) by JORDAN1H: 47;

            then

             A24: ( Ball (e,r)) c= ( LeftComp ( Cage (C,k))) by A19;

            

             A25: (k + 0 ) < (k + 1) by XREAL_1: 8;

            then ( LeftComp ( Cage (C,k))) c= ( LeftComp ( Cage (C,(k + 1)))) by JORDAN1H: 47;

            then ( Ball (e,r)) c= ( LeftComp ( Cage (C,(k + 1)))) by A24;

            then

             A26: ( Ball (e,r)) misses ( L~ ( Cage (C,(k + 1)))) by SPRECT_3: 26, XBOOLE_1: 63;

            

             A27: ( Upper_Arc ( L~ ( Cage (C,(k + 1))))) c= ( L~ ( Cage (C,(k + 1)))) by JORDAN6: 61;

            (( Upper_Appr C) . (k + 1)) = ( Upper_Arc ( L~ ( Cage (C,(k + 1))))) by JORDAN19:def 1;

            hence thesis by A20, A25, A26, A27, XBOOLE_1: 63;

          end;

        end;

      end;

    end;

    theorem :: JORDAN22:36

    

     Th36: ( South_Arc C) c= C

    proof

      let x be object;

      assume

       A1: x in ( South_Arc C);

      assume

       A2: not x in C;

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

      

       A3: x in (C ` ) by A2, SUBSET_1: 29;

      reconsider e = x as Point of ( Euclid 2) by EUCLID: 67;

      

       A4: ( South_Arc C) = ( Lim_inf ( Lower_Appr C)) by JORDAN19:def 4;

      

       A5: (( BDD C) \/ ( UBD C)) = (C ` ) by JORDAN2C: 27;

      per cases by A3, A5, XBOOLE_0:def 3;

        suppose

         A6: x in ( BDD C);

        reconsider OO = ( BDD C) as Subset of ( TopSpaceMetr ( Euclid 2)) by Lm4;

        OO is open by Lm4, PRE_TOPC: 30;

        then

        consider r be Real such that

         A7: r > 0 and

         A8: ( Ball (e,r)) c= ( BDD C) by A6, TOPMETR: 15;

        consider k be Nat such that

         A9: for m be Nat st m > k holds (( Lower_Appr C) . m) meets ( Ball (e,r)) by A1, A4, A7, KURATO_2: 14;

        

         A10: ( Lower_Arc ( L~ ( Cage (C,(k + 1))))) c= ( L~ ( Cage (C,(k + 1)))) by JORDAN6: 61;

        

         A11: (( Lower_Appr C) . (k + 1)) = ( Lower_Arc ( L~ ( Cage (C,(k + 1))))) by JORDAN19:def 2;

        

         A12: (k + 0 ) < (k + 1) by XREAL_1: 8;

        ( Ball (e,r)) misses ( L~ ( Cage (C,(k + 1)))) by A8, JORDAN10: 19, XBOOLE_1: 63;

        hence thesis by A9, A12, A11, A10, XBOOLE_1: 63;

      end;

        suppose

         A13: x in ( UBD C);

        ( union ( UBD-Family C)) = ( UBD C) by JORDAN10: 14;

        then

        consider A be set such that

         A14: x in A and

         A15: A in ( UBD-Family C) by A13, TARSKI:def 4;

        ( UBD-Family C) = the set of all ( UBD ( L~ ( Cage (C,m)))) where m be Nat by JORDAN10:def 1;

        then

        consider m be Nat such that

         A16: A = ( UBD ( L~ ( Cage (C,m)))) by A15;

        reconsider OO = ( LeftComp ( Cage (C,m))) as Subset of ( TopSpaceMetr ( Euclid 2)) by Lm4;

        

         A17: OO is open by Lm4, PRE_TOPC: 30;

        x in ( LeftComp ( Cage (C,m))) by A14, A16, GOBRD14: 36;

        then

        consider r be Real such that

         A18: r > 0 and

         A19: ( Ball (e,r)) c= ( LeftComp ( Cage (C,m))) by A17, TOPMETR: 15;

        consider k be Nat such that

         A20: for m be Nat st m > k holds (( Lower_Appr C) . m) meets ( Ball (e,r)) by A1, A4, A18, KURATO_2: 14;

        thus thesis

        proof

          per cases ;

            suppose

             A21: m > k;

            

             A22: (( Lower_Appr C) . m) = ( Lower_Arc ( L~ ( Cage (C,m)))) by JORDAN19:def 2;

            

             A23: ( Lower_Arc ( L~ ( Cage (C,m)))) c= ( L~ ( Cage (C,m))) by JORDAN6: 61;

            ( Ball (e,r)) misses ( L~ ( Cage (C,m))) by A19, SPRECT_3: 26, XBOOLE_1: 63;

            hence thesis by A20, A21, A22, A23, XBOOLE_1: 63;

          end;

            suppose m <= k;

            then ( LeftComp ( Cage (C,m))) c= ( LeftComp ( Cage (C,k))) by JORDAN1H: 47;

            then

             A24: ( Ball (e,r)) c= ( LeftComp ( Cage (C,k))) by A19;

            

             A25: (k + 0 ) < (k + 1) by XREAL_1: 8;

            then ( LeftComp ( Cage (C,k))) c= ( LeftComp ( Cage (C,(k + 1)))) by JORDAN1H: 47;

            then ( Ball (e,r)) c= ( LeftComp ( Cage (C,(k + 1)))) by A24;

            then

             A26: ( Ball (e,r)) misses ( L~ ( Cage (C,(k + 1)))) by SPRECT_3: 26, XBOOLE_1: 63;

            

             A27: ( Lower_Arc ( L~ ( Cage (C,(k + 1))))) c= ( L~ ( Cage (C,(k + 1)))) by JORDAN6: 61;

            (( Lower_Appr C) . (k + 1)) = ( Lower_Arc ( L~ ( Cage (C,(k + 1))))) by JORDAN19:def 2;

            hence thesis by A20, A25, A26, A27, XBOOLE_1: 63;

          end;

        end;

      end;

    end;

    theorem :: JORDAN22:37

    ( LMP C) in ( Lower_Arc C) & ( UMP C) in ( Upper_Arc C) or ( UMP C) in ( Lower_Arc C) & ( LMP C) in ( Upper_Arc C)

    proof

      

       A1: ( LMP C) in ( South_Arc C) by Th34;

      

       A2: ( North_Arc C) c= C by Th35;

      

       A3: ( UMP C) in ( North_Arc C) by Th33;

      

       A4: ( South_Arc C) c= C by Th36;

      now

        per cases by A4, A1, A2, A3, JORDAN16: 7;

          case LE (( LMP C),( UMP C),C);

          then ( LMP C) in ( Upper_Arc C) & ( UMP C) in ( Lower_Arc C) or ( LMP C) in ( Lower_Arc C) & ( UMP C) in ( Lower_Arc C) or ( LMP C) in ( Upper_Arc C) & ( UMP C) in ( Upper_Arc C);

          hence ( UMP C) in ( Lower_Arc C) & ( LMP C) in ( Upper_Arc C) by JORDAN21: 49, JORDAN21: 50;

        end;

          case LE (( UMP C),( LMP C),C);

          then ( UMP C) in ( Upper_Arc C) & ( LMP C) in ( Lower_Arc C) or ( LMP C) in ( Lower_Arc C) & ( UMP C) in ( Lower_Arc C) or ( LMP C) in ( Upper_Arc C) & ( UMP C) in ( Upper_Arc C);

          hence ( LMP C) in ( Lower_Arc C) & ( UMP C) in ( Upper_Arc C) by JORDAN21: 49, JORDAN21: 50;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN22:38

    ( W-bound C) = ( W-bound ( North_Arc C))

    proof

      

       A1: ( W-min C) in ( North_Arc C) by Th29;

      ( North_Arc C) c= C by Th35;

      hence thesis by A1, JORDAN1J: 65;

    end;

    theorem :: JORDAN22:39

    ( E-bound C) = ( E-bound ( North_Arc C))

    proof

      

       A1: ( E-max C) in ( North_Arc C) by Th30;

      ( North_Arc C) c= C by Th35;

      hence thesis by A1, JORDAN1J: 66;

    end;

    theorem :: JORDAN22:40

    ( W-bound C) = ( W-bound ( South_Arc C))

    proof

      

       A1: ( W-min C) in ( South_Arc C) by Th31;

      ( South_Arc C) c= C by Th36;

      hence thesis by A1, JORDAN1J: 65;

    end;

    theorem :: JORDAN22:41

    ( E-bound C) = ( E-bound ( South_Arc C))

    proof

      

       A1: ( E-max C) in ( South_Arc C) by Th32;

      ( South_Arc C) c= C by Th36;

      hence thesis by A1, JORDAN1J: 66;

    end;