jordan10.miz



    begin

    registration

      cluster connected compact non vertical non horizontal for Subset of ( TOP-REAL 2);

      existence

      proof

        take R^2-unit_square ;

        thus thesis;

      end;

    end

    reserve i,j,k,n for Nat,

P for Subset of ( TOP-REAL 2),

C for connected compact non vertical non horizontal Subset of ( TOP-REAL 2);

    theorem :: JORDAN10:1

    

     Th1: 1 <= k & (k + 1) <= ( len ( Cage (C,n))) & [i, j] in ( Indices ( Gauge (C,n))) & [i, (j + 1)] in ( Indices ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (i,j)) & (( Cage (C,n)) /. (k + 1)) = (( Gauge (C,n)) * (i,(j + 1))) implies i < ( len ( Gauge (C,n)))

    proof

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

      assume that

       A1: 1 <= k & (k + 1) <= ( len ( Cage (C,n))) and

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

       A3: [i, (j + 1)] in ( Indices ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (i,j)) & (( Cage (C,n)) /. (k + 1)) = (( Gauge (C,n)) * (i,(j + 1)));

      assume

       A4: i >= ( len G);

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

      then

       A5: j <= ( len G) by A2, MATRIX_0: 32;

      i <= ( len G) by A2, MATRIX_0: 32;

      then

       A6: i = ( len G) by A4, XXREAL_0: 1;

      f is_sequence_on G by JORDAN9:def 1;

      then ( right_cell (f,k,G)) = ( cell (G,i,j)) by A1, A2, A3, GOBRD13: 22;

      hence contradiction by A1, A6, A5, JORDAN8: 16, JORDAN9: 31;

    end;

    theorem :: JORDAN10:2

    

     Th2: 1 <= k & (k + 1) <= ( len ( Cage (C,n))) & [i, j] in ( Indices ( Gauge (C,n))) & [i, (j + 1)] in ( Indices ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (i,(j + 1))) & (( Cage (C,n)) /. (k + 1)) = (( Gauge (C,n)) * (i,j)) implies i > 1

    proof

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

      assume that

       A1: 1 <= k & (k + 1) <= ( len ( Cage (C,n))) and

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

       A3: [i, (j + 1)] in ( Indices ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (i,(j + 1))) & (( Cage (C,n)) /. (k + 1)) = (( Gauge (C,n)) * (i,j));

      assume

       A4: i <= 1;

      1 <= i by A2, MATRIX_0: 32;

      then i = 1 by A4, XXREAL_0: 1;

      then

       A5: (i -' 1) = 0 by XREAL_1: 232;

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

      then

       A6: j <= ( len G) by A2, MATRIX_0: 32;

      f is_sequence_on G by JORDAN9:def 1;

      then ( right_cell (f,k,G)) = ( cell (G,(i -' 1),j)) by A1, A2, A3, GOBRD13: 28;

      hence contradiction by A1, A5, A6, JORDAN8: 18, JORDAN9: 31;

    end;

    theorem :: JORDAN10:3

    

     Th3: 1 <= k & (k + 1) <= ( len ( Cage (C,n))) & [i, j] in ( Indices ( Gauge (C,n))) & [(i + 1), j] in ( Indices ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (i,j)) & (( Cage (C,n)) /. (k + 1)) = (( Gauge (C,n)) * ((i + 1),j)) implies j > 1

    proof

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

      assume that

       A1: 1 <= k & (k + 1) <= ( len ( Cage (C,n))) and

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

       A3: [(i + 1), j] in ( Indices ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (i,j)) & (( Cage (C,n)) /. (k + 1)) = (( Gauge (C,n)) * ((i + 1),j));

      assume

       A4: j <= 1;

      1 <= j by A2, MATRIX_0: 32;

      then j = 1 by A4, XXREAL_0: 1;

      then

       A5: (j -' 1) = 0 by XREAL_1: 232;

      

       A6: i <= ( len G) by A2, MATRIX_0: 32;

      f is_sequence_on G by JORDAN9:def 1;

      then ( right_cell (f,k,G)) = ( cell (G,i,(j -' 1))) by A1, A2, A3, GOBRD13: 24;

      hence contradiction by A1, A5, A6, JORDAN8: 17, JORDAN9: 31;

    end;

    theorem :: JORDAN10:4

    

     Th4: 1 <= k & (k + 1) <= ( len ( Cage (C,n))) & [i, j] in ( Indices ( Gauge (C,n))) & [(i + 1), j] in ( Indices ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * ((i + 1),j)) & (( Cage (C,n)) /. (k + 1)) = (( Gauge (C,n)) * (i,j)) implies j < ( width ( Gauge (C,n)))

    proof

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

      assume that

       A1: 1 <= k & (k + 1) <= ( len ( Cage (C,n))) and

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

       A3: [(i + 1), j] in ( Indices ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * ((i + 1),j)) & (( Cage (C,n)) /. (k + 1)) = (( Gauge (C,n)) * (i,j));

      assume

       A4: j >= ( width G);

      j <= ( width G) by A2, MATRIX_0: 32;

      then

       A5: j = ( width G) by A4, XXREAL_0: 1;

      

       A6: ( len G) = ( width G) & i <= ( len G) by A2, JORDAN8:def 1, MATRIX_0: 32;

      f is_sequence_on G by JORDAN9:def 1;

      then ( right_cell (f,k,G)) = ( cell (G,i,j)) by A1, A2, A3, GOBRD13: 26;

      hence contradiction by A1, A5, A6, JORDAN8: 15, JORDAN9: 31;

    end;

    theorem :: JORDAN10:5

    

     Th5: C misses ( L~ ( Cage (C,n)))

    proof

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

      assume not thesis;

      then

      consider c be object such that

       A1: c in C and

       A2: c in ( L~ f) by XBOOLE_0: 3;

      ( L~ f) = ( union { ( LSeg (f,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f) }) by TOPREAL1:def 4;

      then

      consider Z be set such that

       A3: c in Z and

       A4: Z in { ( LSeg (f,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f) } by A2, TARSKI:def 4;

      consider i be Nat such that

       A5: Z = ( LSeg (f,i)) and

       A6: 1 <= i & (i + 1) <= ( len f) by A4;

      f is_sequence_on G by JORDAN9:def 1;

      then ( LSeg (f,i)) = (( left_cell (f,i,G)) /\ ( right_cell (f,i,G))) by A6, GOBRD13: 29;

      then

       A7: c in ( left_cell (f,i,G)) by A3, A5, XBOOLE_0:def 4;

      ( left_cell (f,i,G)) misses C by A6, JORDAN9: 31;

      hence contradiction by A1, A7, XBOOLE_0: 3;

    end;

    theorem :: JORDAN10:6

    

     Th6: ( N-bound ( L~ ( Cage (C,n)))) = (( N-bound C) + ((( N-bound C) - ( S-bound C)) / (2 |^ n)))

    proof

      set a = ( N-bound C), s = ( S-bound C), w = ( W-bound C), f = ( Cage (C,n)), G = ( Gauge (C,n));

      consider i such that

       A1: 1 <= i and

       A2: (i + 1) <= ( len G) and

       A3: (f /. 1) = (G * (i,( width G))) and (f /. 2) = (G * ((i + 1),( width G))) and ( N-min C) in ( cell (G,i,(( width G) -' 1))) and ( N-min C) <> (G * (i,(( width G) -' 1))) by JORDAN9:def 1;

      

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

      4 <= ( len G) by JORDAN8: 10;

      then

       A5: 1 <= ( len G) by XXREAL_0: 2;

      (i + 0 ) <= (i + 1) by XREAL_1: 6;

      then i <= ( len G) by A2, XXREAL_0: 2;

      then

       A6: [i, ( len G)] in ( Indices G) by A1, A4, A5, MATRIX_0: 30;

      

       A7: (2 |^ n) <> 0 by NEWTON: 83;

      

      thus ( N-bound ( L~ f)) = (( N-min ( L~ f)) `2 ) by EUCLID: 52

      .= ((f /. 1) `2 ) by JORDAN9: 32

      .= ( |[(w + (((( E-bound C) - w) / (2 |^ n)) * (i - 2))), (s + (((a - s) / (2 |^ n)) * (( len G) - 2)))]| `2 ) by A3, A4, A6, JORDAN8:def 1

      .= (s + (((a - s) / (2 |^ n)) * (( len G) - 2))) by EUCLID: 52

      .= (s + (((a - s) / (2 |^ n)) * (((2 |^ n) + 3) - 2))) by JORDAN8:def 1

      .= ((s + (((a - s) / (2 |^ n)) * (2 |^ n))) + ((a - s) / (2 |^ n)))

      .= ((s + (a - s)) + ((a - s) / (2 |^ n))) by A7, XCMPLX_1: 87

      .= (a + ((a - s) / (2 |^ n)));

    end;

    theorem :: JORDAN10:7

    

     Th7: i < j implies ( N-bound ( L~ ( Cage (C,j)))) < ( N-bound ( L~ ( Cage (C,i))))

    proof

      assume

       A1: i < j;

      defpred P[ Nat] means i < $1 implies ( N-bound ( L~ ( Cage (C,$1)))) < ( N-bound ( L~ ( Cage (C,i))));

      

       A2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A3: P[n];

        set j = (n + 1), a = ( N-bound C), s = ( S-bound C);

        

         A4: ((a + ((a - s) / (2 |^ j))) - (a + ((a - s) / (2 |^ n)))) = (( 0 + ((a - s) / (2 |^ j))) - ((a - s) / (2 |^ n)))

        .= (((a - s) / ((2 |^ n) * 2)) - (((a - s) / (2 |^ n)) / (2 / 2))) by NEWTON: 6

        .= (((a - s) / ((2 |^ n) * 2)) - (((a - s) * 2) / ((2 |^ n) * 2))) by XCMPLX_1: 84

        .= (((a - s) - ((2 * a) - (2 * s))) / ((2 |^ n) * 2)) by XCMPLX_1: 120

        .= ((s - a) / ((2 |^ n) * 2));

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

        then

         A5: ((2 |^ n) * 2) > ( 0 * 2) by XREAL_1: 68;

        

         A6: ( N-bound ( L~ ( Cage (C,n)))) = (a + ((a - s) / (2 |^ n))) & ( N-bound ( L~ ( Cage (C,j)))) = (a + ((a - s) / (2 |^ j))) by Th6;

        (s - a) < 0 by SPRECT_1: 32, XREAL_1: 49;

        then 0 > ((a + ((a - s) / (2 |^ j))) - (a + ((a - s) / (2 |^ n)))) by A5, A4, XREAL_1: 141;

        then

         A7: ( N-bound ( L~ ( Cage (C,(n + 1))))) < ( N-bound ( L~ ( Cage (C,n)))) by A6, XREAL_1: 48;

        assume i < (n + 1);

        then i <= n by NAT_1: 13;

        hence thesis by A3, A7, XXREAL_0: 1, XXREAL_0: 2;

      end;

      

       A8: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A8, A2);

      hence thesis by A1;

    end;

    registration

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

      cluster ( Cl ( RightComp ( Cage (C,n)))) -> compact;

      coherence by GOBRD14: 32;

    end

    theorem :: JORDAN10:8

    

     Th8: ( N-min C) in ( RightComp ( Cage (C,n)))

    proof

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

      consider k be Nat such that

       A1: 1 <= k and

       A2: (k + 1) <= ( len G) and

       A3: (f /. 1) = (G * (k,( width G))) & (f /. 2) = (G * ((k + 1),( width G))) and

       A4: ( N-min C) in ( cell (G,k,(( width G) -' 1))) and ( N-min C) <> (G * (k,(( width G) -' 1))) by JORDAN9:def 1;

      

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

      

       A6: 1 <= (k + 1) by NAT_1: 11;

      then

       A7: 1 <= ( len G) by A2, XXREAL_0: 2;

      then

       A8: [(k + 1), ( len G)] in ( Indices G) by A2, A5, A6, MATRIX_0: 30;

      ( L~ f) <> {} ;

      then

       A9: f is_sequence_on G & (1 + 1) <= ( len f) by GOBRD14: 2, JORDAN9:def 1;

      then ( right_cell (f,1,G)) is closed by GOBRD13: 30;

      then ( Fr ( right_cell (f,1,G))) = (( right_cell (f,1,G)) \ ( Int ( right_cell (f,1,G)))) by TOPS_1: 43;

      then

       A10: (( Fr ( right_cell (f,1,G))) \/ ( Int ( right_cell (f,1,G)))) = ( right_cell (f,1,G)) by TOPS_1: 16, XBOOLE_1: 45;

      

       A11: k < ( len G) by A2, NAT_1: 13;

      then [k, ( len G)] in ( Indices G) by A1, A5, A7, MATRIX_0: 30;

      then

       A12: ( cell (G,k,(( len G) -' 1))) = ( right_cell (f,1,G)) by A3, A9, A5, A8, GOBRD13: 24;

      

       A13: ( Int ( right_cell (f,1))) c= ( RightComp f) by GOBOARD9:def 2;

      ( Int ( right_cell (f,1,G))) c= ( Int ( right_cell (f,1))) by A9, GOBRD13: 33, TOPS_1: 19;

      then

       A14: ( Int ( cell (G,k,(( len G) -' 1)))) c= ( RightComp f) by A12, A13;

      ( RightComp f) misses ( L~ f) by SPRECT_3: 25;

      then

       A15: (( RightComp f) /\ ( L~ f)) = {} ;

      

       A16: ( Fr ( cell (G,k,(( len G) -' 1)))) c= (( RightComp f) \/ ( L~ f))

      proof

        let q be object;

        assume

         A17: q in ( Fr ( cell (G,k,(( len G) -' 1))));

        then

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

        4 <= ( len G) by JORDAN8: 10;

        then (4 - 1) <= (( len G) - 1) by XREAL_1: 13;

        then 0 <= (( len G) - 1) by XXREAL_0: 2;

        then

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

        

         A19: (( len G) - 1) < (( len G) - 0 ) by XREAL_1: 15;

        then ( Int ( cell (G,k,(( len G) -' 1)))) <> {} by A5, A11, A18, GOBOARD9: 14;

        then

        consider p be object such that

         A20: p in ( Int ( cell (G,k,(( len G) -' 1)))) by XBOOLE_0:def 1;

        reconsider p as Point of ( TOP-REAL 2) by A20;

        per cases ;

          suppose q in ( L~ f);

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose

           A21: not q in ( L~ f);

          

           A22: ( LSeg (p,s)) c= (( L~ f) ` )

          proof

            3 <= (( len G) -' 1) by GOBRD14: 7;

            then

             A23: 1 <= (( len G) -' 1) by XXREAL_0: 2;

            then

             A24: ( Int ( cell (G,k,(( len G) -' 1)))) = { |[x, y]| where x,y be Real : ((G * (k,1)) `1 ) < x & x < ((G * ((k + 1),1)) `1 ) & ((G * (1,(( len G) -' 1))) `2 ) < y & y < ((G * (1,((( len G) -' 1) + 1))) `2 ) } by A1, A5, A11, A18, A19, GOBOARD6: 26;

            

             A25: ( cell (G,k,(( len G) -' 1))) = { |[m, o]| where m,o be Real : ((G * (k,1)) `1 ) <= m & m <= ((G * ((k + 1),1)) `1 ) & ((G * (1,(( len G) -' 1))) `2 ) <= o & o <= ((G * (1,((( len G) -' 1) + 1))) `2 ) } by A1, A5, A11, A18, A19, A23, GOBRD11: 32;

            ( Fr ( cell (G,k,(( len G) -' 1)))) c= ( cell (G,k,(( len G) -' 1))) by A9, A12, GOBRD13: 30, TOPS_1: 35;

            then q in ( cell (G,k,(( len G) -' 1))) by A17;

            then

            consider m,o be Real such that

             A26: s = |[m, o]| and

             A27: ((G * (k,1)) `1 ) <= m and

             A28: m <= ((G * ((k + 1),1)) `1 ) and

             A29: ((G * (1,(( len G) -' 1))) `2 ) <= o and

             A30: o <= ((G * (1,((( len G) -' 1) + 1))) `2 ) by A25;

            

             A31: (s `2 ) = o by A26, EUCLID: 52;

            consider x,y be Real such that

             A32: p = |[x, y]| and

             A33: ((G * (k,1)) `1 ) < x and

             A34: x < ((G * ((k + 1),1)) `1 ) and

             A35: ((G * (1,(( len G) -' 1))) `2 ) < y and

             A36: y < ((G * (1,((( len G) -' 1) + 1))) `2 ) by A20, A24;

            

             A37: (p `1 ) = x by A32, EUCLID: 52;

            let a be object;

            assume

             A38: a in ( LSeg (p,s));

            then

            reconsider b = a as Point of ( TOP-REAL 2);

            

             A39: b = |[(b `1 ), (b `2 )]| by EUCLID: 53;

            

             A40: (p `2 ) = y by A32, EUCLID: 52;

            

             A41: (s `1 ) = m by A26, EUCLID: 52;

            now

              per cases ;

                case b = s;

                hence thesis by A21, SUBSET_1: 29;

              end;

                case

                 A42: b <> s;

                now

                  per cases by XXREAL_0: 1;

                    case

                     A43: (s `1 ) < (p `1 ) & (s `2 ) < (p `2 );

                    then (s `2 ) < (b `2 ) by A38, A42, TOPREAL6: 30;

                    then

                     A44: ((G * (1,(( len G) -' 1))) `2 ) < (b `2 ) by A29, A31, XXREAL_0: 2;

                    (b `1 ) <= (p `1 ) by A38, A43, TOPREAL6: 29;

                    then

                     A45: (b `1 ) < ((G * ((k + 1),1)) `1 ) by A34, A37, XXREAL_0: 2;

                    (b `2 ) <= (p `2 ) by A38, A43, TOPREAL6: 30;

                    then

                     A46: (b `2 ) < ((G * (1,((( len G) -' 1) + 1))) `2 ) by A36, A40, XXREAL_0: 2;

                    (s `1 ) < (b `1 ) by A38, A42, A43, TOPREAL6: 29;

                    then ((G * (k,1)) `1 ) < (b `1 ) by A27, A41, XXREAL_0: 2;

                    hence b in ( Int ( cell (G,k,(( len G) -' 1)))) by A24, A39, A45, A44, A46;

                  end;

                    case

                     A47: (s `1 ) < (p `1 ) & (s `2 ) > (p `2 );

                    then (b `2 ) < (s `2 ) by A38, A42, TOPREAL6: 30;

                    then

                     A48: (b `2 ) < ((G * (1,((( len G) -' 1) + 1))) `2 ) by A30, A31, XXREAL_0: 2;

                    (b `1 ) <= (p `1 ) by A38, A47, TOPREAL6: 29;

                    then

                     A49: (b `1 ) < ((G * ((k + 1),1)) `1 ) by A34, A37, XXREAL_0: 2;

                    (p `2 ) <= (b `2 ) by A38, A47, TOPREAL6: 30;

                    then

                     A50: ((G * (1,(( len G) -' 1))) `2 ) < (b `2 ) by A35, A40, XXREAL_0: 2;

                    (s `1 ) < (b `1 ) by A38, A42, A47, TOPREAL6: 29;

                    then ((G * (k,1)) `1 ) < (b `1 ) by A27, A41, XXREAL_0: 2;

                    hence b in ( Int ( cell (G,k,(( len G) -' 1)))) by A24, A39, A49, A50, A48;

                  end;

                    case

                     A51: (s `1 ) < (p `1 ) & (s `2 ) = (p `2 );

                    then (b `1 ) <= (p `1 ) by A38, TOPREAL6: 29;

                    then

                     A52: (b `1 ) < ((G * ((k + 1),1)) `1 ) by A34, A37, XXREAL_0: 2;

                    (s `1 ) < (b `1 ) by A38, A42, A51, TOPREAL6: 29;

                    then

                     A53: ((G * (k,1)) `1 ) < (b `1 ) by A27, A41, XXREAL_0: 2;

                    (p `2 ) = (b `2 ) by A38, A51, GOBOARD7: 6;

                    hence b in ( Int ( cell (G,k,(( len G) -' 1)))) by A24, A39, A35, A36, A40, A53, A52;

                  end;

                    case

                     A54: (s `1 ) > (p `1 ) & (s `2 ) < (p `2 );

                    then (s `2 ) < (b `2 ) by A38, A42, TOPREAL6: 30;

                    then

                     A55: ((G * (1,(( len G) -' 1))) `2 ) < (b `2 ) by A29, A31, XXREAL_0: 2;

                    (b `1 ) >= (p `1 ) by A38, A54, TOPREAL6: 29;

                    then

                     A56: ((G * (k,1)) `1 ) < (b `1 ) by A33, A37, XXREAL_0: 2;

                    (b `2 ) <= (p `2 ) by A38, A54, TOPREAL6: 30;

                    then

                     A57: (b `2 ) < ((G * (1,((( len G) -' 1) + 1))) `2 ) by A36, A40, XXREAL_0: 2;

                    (s `1 ) > (b `1 ) by A38, A42, A54, TOPREAL6: 29;

                    then (b `1 ) < ((G * ((k + 1),1)) `1 ) by A28, A41, XXREAL_0: 2;

                    hence b in ( Int ( cell (G,k,(( len G) -' 1)))) by A24, A39, A56, A55, A57;

                  end;

                    case

                     A58: (s `1 ) > (p `1 ) & (s `2 ) > (p `2 );

                    then (s `2 ) > (b `2 ) by A38, A42, TOPREAL6: 30;

                    then

                     A59: (b `2 ) < ((G * (1,((( len G) -' 1) + 1))) `2 ) by A30, A31, XXREAL_0: 2;

                    (b `1 ) >= (p `1 ) by A38, A58, TOPREAL6: 29;

                    then

                     A60: ((G * (k,1)) `1 ) < (b `1 ) by A33, A37, XXREAL_0: 2;

                    (b `2 ) >= (p `2 ) by A38, A58, TOPREAL6: 30;

                    then

                     A61: ((G * (1,(( len G) -' 1))) `2 ) < (b `2 ) by A35, A40, XXREAL_0: 2;

                    (s `1 ) > (b `1 ) by A38, A42, A58, TOPREAL6: 29;

                    then (b `1 ) < ((G * ((k + 1),1)) `1 ) by A28, A41, XXREAL_0: 2;

                    hence b in ( Int ( cell (G,k,(( len G) -' 1)))) by A24, A39, A60, A61, A59;

                  end;

                    case

                     A62: (s `1 ) > (p `1 ) & (s `2 ) = (p `2 );

                    then (b `1 ) >= (p `1 ) by A38, TOPREAL6: 29;

                    then

                     A63: ((G * (k,1)) `1 ) < (b `1 ) by A33, A37, XXREAL_0: 2;

                    (s `1 ) > (b `1 ) by A38, A42, A62, TOPREAL6: 29;

                    then

                     A64: (b `1 ) < ((G * ((k + 1),1)) `1 ) by A28, A41, XXREAL_0: 2;

                    (b `2 ) = (p `2 ) by A38, A62, GOBOARD7: 6;

                    hence b in ( Int ( cell (G,k,(( len G) -' 1)))) by A24, A39, A35, A36, A40, A63, A64;

                  end;

                    case

                     A65: (s `1 ) = (p `1 ) & (s `2 ) > (p `2 );

                    then (b `2 ) >= (p `2 ) by A38, TOPREAL6: 30;

                    then

                     A66: ((G * (1,(( len G) -' 1))) `2 ) < (b `2 ) by A35, A40, XXREAL_0: 2;

                    (s `2 ) > (b `2 ) by A38, A42, A65, TOPREAL6: 30;

                    then

                     A67: (b `2 ) < ((G * (1,((( len G) -' 1) + 1))) `2 ) by A30, A31, XXREAL_0: 2;

                    (b `1 ) = (p `1 ) by A38, A65, GOBOARD7: 5;

                    hence b in ( Int ( cell (G,k,(( len G) -' 1)))) by A24, A39, A33, A34, A37, A66, A67;

                  end;

                    case

                     A68: (s `1 ) = (p `1 ) & (s `2 ) < (p `2 );

                    then (b `2 ) <= (p `2 ) by A38, TOPREAL6: 30;

                    then

                     A69: (b `2 ) < ((G * (1,((( len G) -' 1) + 1))) `2 ) by A36, A40, XXREAL_0: 2;

                    (s `2 ) < (b `2 ) by A38, A42, A68, TOPREAL6: 30;

                    then

                     A70: ((G * (1,(( len G) -' 1))) `2 ) < (b `2 ) by A29, A31, XXREAL_0: 2;

                    (b `1 ) = (p `1 ) by A38, A68, GOBOARD7: 5;

                    hence b in ( Int ( cell (G,k,(( len G) -' 1)))) by A24, A39, A33, A34, A37, A70, A69;

                  end;

                    case (s `1 ) = (p `1 ) & (s `2 ) = (p `2 );

                    then p = s by TOPREAL3: 6;

                    then ( LSeg (p,s)) = {p} by RLTOPSP1: 70;

                    hence b in ( Int ( cell (G,k,(( len G) -' 1)))) by A20, A38, TARSKI:def 1;

                  end;

                end;

                then not b in ( L~ f) by A15, A14, XBOOLE_0:def 4;

                hence thesis by SUBSET_1: 29;

              end;

            end;

            hence thesis;

          end;

          

           A71: s in ( LSeg (p,s)) by RLTOPSP1: 68;

          now

            take a = p;

            thus a in {p} & a in ( LSeg (p,s)) by RLTOPSP1: 68, TARSKI:def 1;

          end;

          then

           A72: {p} meets ( LSeg (p,s)) by XBOOLE_0: 3;

          ( RightComp f) is_a_component_of (( L~ f) ` ) & {p} c= ( RightComp f) by A14, A20, GOBOARD9:def 2, ZFMISC_1: 31;

          then ( LSeg (p,s)) c= ( RightComp f) by A22, A72, GOBOARD9: 4;

          hence thesis by A71, XBOOLE_0:def 3;

        end;

      end;

      C misses ( L~ f) by Th5;

      then ( N-min C) in C & (C /\ ( L~ f)) = {} by SPRECT_1: 11;

      then

       A73: not ( N-min C) in ( L~ f) by XBOOLE_0:def 4;

      ( RightComp f) c= (( RightComp f) \/ ( L~ f)) by XBOOLE_1: 7;

      then ( Int ( cell (G,k,(( len G) -' 1)))) c= (( RightComp f) \/ ( L~ f)) by A14;

      then ( right_cell (f,1,G)) c= (( RightComp f) \/ ( L~ f)) by A12, A16, A10, XBOOLE_1: 8;

      hence thesis by A73, A4, A5, A12, XBOOLE_0:def 3;

    end;

    theorem :: JORDAN10:9

    

     Th9: C meets ( RightComp ( Cage (C,n)))

    proof

      ( N-min C) in C & ( N-min C) in ( RightComp ( Cage (C,n))) by Th8, SPRECT_1: 11;

      then (C /\ ( RightComp ( Cage (C,n)))) <> {} by XBOOLE_0:def 4;

      hence thesis;

    end;

    theorem :: JORDAN10:10

    

     Th10: C misses ( LeftComp ( Cage (C,n)))

    proof

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

      assume

       A1: C meets ( LeftComp f);

      ( RightComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 2;

      then

       A2: ex R be Subset of (( TOP-REAL 2) | (( L~ f) ` )) st R = ( RightComp f) & R is a_component by CONNSP_1:def 6;

      C misses ( L~ f) by Th5;

      then

       A3: (C /\ ( L~ f)) = {} ;

      C c= the carrier of (( TOP-REAL 2) | (( L~ f) ` ))

      proof

        let c be object;

        assume

         A4: c in C;

        then not c in ( L~ f) by A3, XBOOLE_0:def 4;

        then c in (( L~ f) ` ) by A4, SUBSET_1: 29;

        hence thesis by PRE_TOPC: 8;

      end;

      then

      reconsider C1 = C as Subset of (( TOP-REAL 2) | (( L~ f) ` ));

      ( LeftComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 1;

      then

       A5: ex L be Subset of (( TOP-REAL 2) | (( L~ f) ` )) st L = ( LeftComp f) & L is a_component by CONNSP_1:def 6;

      C meets ( RightComp f) & C1 is connected by Th9, CONNSP_1: 23;

      hence contradiction by A1, A5, A2, JORDAN2C: 92, SPRECT_4: 6;

    end;

    theorem :: JORDAN10:11

    

     Th11: C c= ( RightComp ( Cage (C,n)))

    proof

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

      let c be object;

      assume

       A1: c in C;

      C misses ( L~ f) by Th5;

      then (C /\ ( L~ f)) = {} ;

      then

       A2: not c in ( L~ f) by A1, XBOOLE_0:def 4;

      C misses ( LeftComp f) by Th10;

      then (C /\ ( LeftComp f)) = {} ;

      then not c in ( LeftComp f) by A1, XBOOLE_0:def 4;

      hence thesis by A1, A2, GOBRD14: 18;

    end;

    theorem :: JORDAN10:12

    

     Th12: C c= ( BDD ( L~ ( Cage (C,n))))

    proof

      C c= ( RightComp ( Cage (C,n))) & ( RightComp ( Cage (C,n))) c= ( BDD ( L~ ( Cage (C,n)))) by Th11, GOBRD14: 35, JORDAN2C: 22;

      hence thesis;

    end;

    theorem :: JORDAN10:13

    

     Th13: ( UBD ( L~ ( Cage (C,n)))) c= ( UBD C)

    proof

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

      

       A1: ( UBD C) = ( union { B where B be Subset of ( TOP-REAL 2) : B is_outside_component_of C }) by JORDAN2C:def 5;

      let x be object;

      

       A2: ( UBD ( L~ f)) = ( union { B where B be Subset of ( TOP-REAL 2) : B is_outside_component_of ( L~ f) }) by JORDAN2C:def 5;

      assume x in ( UBD ( L~ f));

      then

      consider L be set such that

       A3: x in L and

       A4: L in { B where B be Subset of ( TOP-REAL 2) : B is_outside_component_of ( L~ f) } by A2, TARSKI:def 4;

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

       A5: L = B and

       A6: B is_outside_component_of ( L~ f) by A4;

      reconsider B1 = B as Subset of ( Euclid 2) by TOPREAL3: 8;

      

       A7: B1 misses ( RightComp f) by A6, GOBRD14: 35, JORDAN2C: 118;

      then

       A8: (B1 /\ ( RightComp f)) = {} ;

      the carrier of (( TOP-REAL 2) | (C ` )) = (C ` ) by PRE_TOPC: 8;

      then

      reconsider P1 = ( Component_of ( Down (B,(C ` )))) as Subset of ( TOP-REAL 2) by XBOOLE_1: 1;

      B is_a_component_of (( L~ f) ` ) by A6, JORDAN2C:def 3;

      then

      consider B2 be Subset of (( TOP-REAL 2) | (( L~ f) ` )) such that

       A9: B2 = B and

       A10: B2 is a_component by CONNSP_1:def 6;

      B2 is connected by A10, CONNSP_1:def 5;

      then

       A11: B is connected by A9, CONNSP_1: 23;

      

       A12: C c= ( RightComp f) by Th11;

      then not x in C by A3, A5, A8, XBOOLE_0:def 4;

      then x in (C ` ) by A3, A5, XBOOLE_0:def 5;

      then

       A13: x in (B /\ (C ` )) by A3, A5, XBOOLE_0:def 4;

       not B is bounded by A6, JORDAN2C:def 3;

      then

       A14: not B1 is bounded by JORDAN2C: 11;

      B1 misses C by A7, Th11, XBOOLE_1: 63;

      then P1 is_outside_component_of C by A11, A14, JORDAN2C: 63;

      then

       A15: P1 in { W where W be Subset of ( TOP-REAL 2) : W is_outside_component_of C };

      B c= (C ` )

      proof

        let a be object;

        assume

         A16: a in B;

        then not a in C by A12, A8, XBOOLE_0:def 4;

        hence thesis by A16, XBOOLE_0:def 5;

      end;

      then ( Down (B,(C ` ))) = B by XBOOLE_1: 28;

      then ( Down (B,(C ` ))) c= ( Component_of ( Down (B,(C ` )))) by A11, CONNSP_1: 46, CONNSP_3: 1;

      hence thesis by A1, A13, A15, TARSKI:def 4;

    end;

    definition

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

      :: JORDAN10:def1

      func UBD-Family C -> set equals the set of all ( UBD ( L~ ( Cage (C,n)))) where n be Nat;

      coherence ;

      :: JORDAN10:def2

      func BDD-Family C -> set equals the set of all ( Cl ( BDD ( L~ ( Cage (C,n))))) where n be Nat;

      coherence ;

    end

    definition

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

      :: original: UBD-Family

      redefine

      func UBD-Family C -> Subset-Family of ( TOP-REAL 2) ;

      coherence

      proof

         the set of all ( UBD ( L~ ( Cage (C,i)))) where i be Nat c= ( bool the carrier of ( TOP-REAL 2))

        proof

          let x be object;

          assume x in the set of all ( UBD ( L~ ( Cage (C,i)))) where i be Nat;

          then ex i be Nat st x = ( UBD ( L~ ( Cage (C,i))));

          hence thesis;

        end;

        hence thesis;

      end;

      :: original: BDD-Family

      redefine

      func BDD-Family C -> Subset-Family of ( TOP-REAL 2) ;

      coherence

      proof

         the set of all ( Cl ( BDD ( L~ ( Cage (C,i))))) where i be Nat c= ( bool the carrier of ( TOP-REAL 2))

        proof

          let x be object;

          assume x in the set of all ( Cl ( BDD ( L~ ( Cage (C,i))))) where i be Nat;

          then ex i be Nat st x = ( Cl ( BDD ( L~ ( Cage (C,i)))));

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

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

      cluster ( UBD-Family C) -> non empty;

      coherence

      proof

        ( UBD ( L~ ( Cage (C, 0 )))) in ( UBD-Family C);

        hence thesis;

      end;

      cluster ( BDD-Family C) -> non empty;

      coherence

      proof

        ( Cl ( BDD ( L~ ( Cage (C, 0 ))))) in ( BDD-Family C);

        hence thesis;

      end;

    end

    theorem :: JORDAN10:14

    

     Th14: ( union ( UBD-Family C)) = ( UBD C)

    proof

      

       A1: ( UBD ( L~ ( Cage (C, 0 )))) c= ( UBD C) & ( UBD ( L~ ( Cage (C, 0 )))) = ( LeftComp ( Cage (C, 0 ))) by Th13, GOBRD14: 36;

      for X be set st X in ( UBD-Family C) holds X c= ( UBD C)

      proof

        let X be set;

        assume X in ( UBD-Family C);

        then ex n st X = ( UBD ( L~ ( Cage (C,n))));

        hence thesis by Th13;

      end;

      hence ( union ( UBD-Family C)) c= ( UBD C) by ZFMISC_1: 76;

      let x be object such that

       A2: x in ( UBD C);

      ( UBD C) = ( union { B where B be Subset of ( TOP-REAL 2) : B is_outside_component_of C }) by JORDAN2C:def 5;

      then

      consider A be set such that

       A3: x in A and

       A4: A in { B where B be Subset of ( TOP-REAL 2) : B is_outside_component_of C } by A2, TARSKI:def 4;

      ex B be Subset of ( TOP-REAL 2) st A = B & B is_outside_component_of C by A4;

      then

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

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

       A5: (q `2 ) > ( N-bound ( L~ ( Cage (C, 0 )))) and

       A6: p <> q by TOPREAL6: 33;

      (( Cage (C, 0 )) /. 1) = ( N-min ( L~ ( Cage (C, 0 )))) by JORDAN9: 32;

      then q in ( LeftComp ( Cage (C, 0 ))) by A5, JORDAN2C: 113;

      then

      consider P such that

       A7: P is_S-P_arc_joining (p,q) and

       A8: P c= ( UBD C) by A2, A6, A1, TOPREAL4: 29;

      consider f be FinSequence of ( TOP-REAL 2) such that

       A9: f is being_S-Seq and

       A10: P = ( L~ f) and

       A11: p = (f /. 1) and q = (f /. ( len f)) by A7, TOPREAL4:def 1;

      reconsider f as being_S-Seq FinSequence of ( TOP-REAL 2) by A9;

      2 <= ( len f) by NAT_D: 60;

      then

       A12: x in P by A10, A11, JORDAN3: 1;

      ( L~ f) is non empty & the TopStruct of ( TOP-REAL 2) = ( TopSpaceMetr ( Euclid 2)) by EUCLID:def 8;

      then

      reconsider P1 = P, C1 = C as non empty compact Subset of ( TopSpaceMetr ( Euclid 2)) by A10, COMPTS_1: 23;

      set d = ( min_dist_min (P1,C1));

      ( UBD C) is_outside_component_of C by JORDAN2C: 68;

      then ( UBD C) is_a_component_of (C ` ) by JORDAN2C:def 3;

      then C misses ( UBD C) by JORDAN2C: 117;

      then P misses C by A8, XBOOLE_1: 63;

      then d > 0 by JGRAPH_1: 38;

      then (d / 2) > 0 by XREAL_1: 139;

      then

      consider n such that 1 < n and

       A13: ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (1,2)))) < (d / 2) & ( dist ((( Gauge (C,n)) * (1,1)),(( Gauge (C,n)) * (2,1)))) < (d / 2) by GOBRD14: 11;

      set G = ( Gauge (C,n)), g = ( Cage (C,n));

      

       A14: ( UBD ( L~ g)) in ( UBD-Family C);

       A15:

      now

        assume (( L~ g) /\ P) <> {} ;

        then

        consider a be object such that

         A16: a in (( L~ g) /\ P) by XBOOLE_0:def 1;

        a in ( L~ g) by A16, XBOOLE_0:def 4;

        then

        consider i be Nat such that

         A17: 1 <= i & (i + 1) <= ( len g) and

         A18: a in ( LSeg (g,i)) by SPPOL_2: 13;

        ( right_cell (g,i,G)) meets C by A17, JORDAN9: 31;

        then

        consider c be object such that

         A19: c in (( right_cell (g,i,G)) /\ C) by XBOOLE_0: 4;

        reconsider c as Point of ( Euclid 2) by A19, TOPREAL3: 8;

        reconsider a9 = a as Point of ( Euclid 2) by A16, TOPREAL3: 8;

        

         A20: c in C by A19, XBOOLE_0:def 4;

        reconsider c9 = c as Point of ( TOP-REAL 2) by A19;

        

         A21: g is_sequence_on G by JORDAN9:def 1;

        then

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

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

         A23: (g /. i) = (G * (i1,j1)) and

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

         A25: (g /. (i + 1)) = (G * (i2,j2)) and

         A26: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A17, JORDAN8: 3;

        (( left_cell (g,i,G)) /\ ( right_cell (g,i,G))) = ( LSeg (g,i)) by A17, A21, GOBRD13: 29;

        then

         A27: a in ( right_cell (g,i,G)) by A18, XBOOLE_0:def 4;

        a in P by A16, XBOOLE_0:def 4;

        then

         A28: ( dist (a9,c)) >= d by A20, WEIERSTR: 34;

        reconsider A = a as Point of ( TOP-REAL 2) by A16;

        set e = ( E-bound C), w = ( W-bound C), p = ( N-bound C), s = ( S-bound C);

        

         A29: 4 <= ( len G) by JORDAN8: 10;

        then

         A30: 1 <= ( len G) by XXREAL_0: 2;

        

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

        then

         A32: 1 <= ( width G) by A29, XXREAL_0: 2;

        

         A33: [1, 1] in ( Indices G) by A31, A30, MATRIX_0: 30;

        

         A34: c in ( right_cell (g,i,G)) by A19, XBOOLE_0:def 4;

        now

          per cases by A26;

            case

             A35: i1 = i2 & (j1 + 1) = j2;

            then

             A36: i1 < ( len G) by A17, A22, A23, A24, A25, Th1;

            then

             A37: (i1 + 1) <= ( len G) by NAT_1: 13;

            

             A38: 1 <= i1 by A22, MATRIX_0: 32;

            then 1 <= (i1 + 1) by NAT_1: 13;

            then

             A39: [(i1 + 1), 1] in ( Indices G) by A32, A37, MATRIX_0: 30;

             [i1, 1] in ( Indices G) by A32, A38, A36, MATRIX_0: 30;

            then

             A40: ( dist ((G * (i1,1)),(G * ((i1 + 1),1)))) = (((G * ((i1 + 1),1)) `1 ) - ((G * (i1,1)) `1 )) & ( dist ((G * (i1,1)),(G * ((i1 + 1),1)))) = ((e - w) / (2 |^ n)) by A39, GOBRD14: 5, GOBRD14: 10;

            

             A41: (j1 + 1) <= ( width G) by A24, A35, MATRIX_0: 32;

            then

             A42: j1 < ( width G) by NAT_1: 13;

            

             A43: 1 <= j1 by A22, MATRIX_0: 32;

            then 1 <= (j1 + 1) by NAT_1: 13;

            then

             A44: [1, (j1 + 1)] in ( Indices G) by A30, A41, MATRIX_0: 30;

            

             A45: ( right_cell (g,i,G)) = ( cell (G,i1,j1)) by A17, A21, A22, A23, A24, A25, A35, GOBRD13: 22

            .= { |[r, t]| where r,t be Real : ((G * (i1,1)) `1 ) <= r & r <= ((G * ((i1 + 1),1)) `1 ) & ((G * (1,j1)) `2 ) <= t & t <= ((G * (1,(j1 + 1))) `2 ) } by A38, A36, A43, A42, GOBRD11: 32;

            then

            consider aa,ab be Real such that

             A46: a = |[aa, ab]| and

             A47: ((G * (i1,1)) `1 ) <= aa & aa <= ((G * ((i1 + 1),1)) `1 ) & ((G * (1,j1)) `2 ) <= ab & ab <= ((G * (1,(j1 + 1))) `2 ) by A27;

            

             A48: (A `1 ) = aa & (A `2 ) = ab by A46, EUCLID: 52;

             [1, j1] in ( Indices G) by A30, A43, A42, MATRIX_0: 30;

            then

             A49: ( dist ((G * (1,j1)),(G * (1,(j1 + 1))))) = (((G * (1,(j1 + 1))) `2 ) - ((G * (1,j1)) `2 )) & ( dist ((G * (1,j1)),(G * (1,(j1 + 1))))) = ((p - s) / (2 |^ n)) by A44, GOBRD14: 6, GOBRD14: 9;

            consider r,t be Real such that

             A50: c = |[r, t]| and

             A51: ((G * (i1,1)) `1 ) <= r & r <= ((G * ((i1 + 1),1)) `1 ) & ((G * (1,j1)) `2 ) <= t & t <= ((G * (1,(j1 + 1))) `2 ) by A34, A45;

            (c9 `1 ) = r & (c9 `2 ) = t by A50, EUCLID: 52;

            hence ( dist (A,c9)) <= (((p - s) / (2 |^ n)) + ((e - w) / (2 |^ n))) by A51, A47, A48, A49, A40, TOPREAL6: 95;

          end;

            case

             A52: (i1 + 1) = i2 & j1 = j2;

            then

             A53: (i1 + 1) <= ( len G) by A24, MATRIX_0: 32;

            then

             A54: i1 < ( len G) by NAT_1: 13;

            

             A55: 1 <= i1 by A22, MATRIX_0: 32;

            then 1 <= (i1 + 1) by NAT_1: 13;

            then

             A56: [(i1 + 1), 1] in ( Indices G) by A32, A53, MATRIX_0: 30;

             [i1, 1] in ( Indices G) by A32, A55, A54, MATRIX_0: 30;

            then

             A57: ( dist ((G * (i1,1)),(G * ((i1 + 1),1)))) = (((G * ((i1 + 1),1)) `1 ) - ((G * (i1,1)) `1 )) & ( dist ((G * (i1,1)),(G * ((i1 + 1),1)))) = ((e - w) / (2 |^ n)) by A56, GOBRD14: 5, GOBRD14: 10;

            

             A58: j2 <= ( width G) by A24, MATRIX_0: 32;

            j2 > 1 by A17, A22, A23, A24, A25, A52, Th3;

            then

             A59: (j2 - 1) > 0 by XREAL_1: 50;

            then

             A60: (j2 - 1) = (j2 -' 1) by XREAL_0:def 2;

            then

             A61: 1 <= (j2 -' 1) by A59, NAT_1: 14;

            (( width G) - 1) < (( width G) - 0 ) by XREAL_1: 15;

            then

             A62: (j2 -' 1) < ( width G) by A60, A58, XREAL_1: 15;

            then

             A63: [1, (j2 -' 1)] in ( Indices G) by A30, A61, MATRIX_0: 30;

            

             A64: ( right_cell (g,i,G)) = ( cell (G,i1,(j2 -' 1))) by A17, A21, A22, A23, A24, A25, A52, GOBRD13: 24

            .= { |[r, t]| where r,t be Real : ((G * (i1,1)) `1 ) <= r & r <= ((G * ((i1 + 1),1)) `1 ) & ((G * (1,(j2 -' 1))) `2 ) <= t & t <= ((G * (1,((j2 -' 1) + 1))) `2 ) } by A55, A54, A61, A62, GOBRD11: 32;

            then

            consider aa,ab be Real such that

             A65: a = |[aa, ab]| and

             A66: ((G * (i1,1)) `1 ) <= aa & aa <= ((G * ((i1 + 1),1)) `1 ) & ((G * (1,(j2 -' 1))) `2 ) <= ab & ab <= ((G * (1,((j2 -' 1) + 1))) `2 ) by A27;

            

             A67: (A `1 ) = aa & (A `2 ) = ab by A65, EUCLID: 52;

            1 <= ((j2 -' 1) + 1) by A61, NAT_1: 13;

            then [1, ((j2 -' 1) + 1)] in ( Indices G) by A30, A60, A58, MATRIX_0: 30;

            then

             A68: ( dist ((G * (1,(j2 -' 1))),(G * (1,((j2 -' 1) + 1))))) = (((G * (1,((j2 -' 1) + 1))) `2 ) - ((G * (1,(j2 -' 1))) `2 )) & ( dist ((G * (1,(j2 -' 1))),(G * (1,((j2 -' 1) + 1))))) = ((p - s) / (2 |^ n)) by A63, GOBRD14: 6, GOBRD14: 9;

            consider r,t be Real such that

             A69: c = |[r, t]| and

             A70: ((G * (i1,1)) `1 ) <= r & r <= ((G * ((i1 + 1),1)) `1 ) & ((G * (1,(j2 -' 1))) `2 ) <= t & t <= ((G * (1,((j2 -' 1) + 1))) `2 ) by A34, A64;

            (c9 `1 ) = r & (c9 `2 ) = t by A69, EUCLID: 52;

            hence ( dist (A,c9)) <= (((p - s) / (2 |^ n)) + ((e - w) / (2 |^ n))) by A70, A66, A67, A68, A57, TOPREAL6: 95;

          end;

            case

             A71: i1 = (i2 + 1) & j1 = j2;

            

             A72: 1 <= (j1 + 1) by NAT_1: 12;

            

             A73: j1 < ( width G) by A17, A22, A23, A24, A25, A71, Th4;

            then (j1 + 1) <= ( width G) by NAT_1: 13;

            then

             A74: [1, (j1 + 1)] in ( Indices G) by A30, A72, MATRIX_0: 30;

            

             A75: 1 <= j1 by A22, MATRIX_0: 32;

            then [1, j1] in ( Indices G) by A30, A73, MATRIX_0: 30;

            then

             A76: ( dist ((G * (1,j1)),(G * (1,(j1 + 1))))) = (((G * (1,(j1 + 1))) `2 ) - ((G * (1,j1)) `2 )) & ( dist ((G * (1,j1)),(G * (1,(j1 + 1))))) = ((p - s) / (2 |^ n)) by A74, GOBRD14: 6, GOBRD14: 9;

            

             A77: (i2 + 1) <= ( len G) by A22, A71, MATRIX_0: 32;

            then

             A78: i2 < ( len G) by NAT_1: 13;

            

             A79: 1 <= i2 by A24, MATRIX_0: 32;

            then 1 <= (i2 + 1) by NAT_1: 13;

            then

             A80: [(i2 + 1), 1] in ( Indices G) by A32, A77, MATRIX_0: 30;

            

             A81: ( right_cell (g,i,G)) = ( cell (G,i2,j1)) by A17, A21, A22, A23, A24, A25, A71, GOBRD13: 26

            .= { |[r, t]| where r,t be Real : ((G * (i2,1)) `1 ) <= r & r <= ((G * ((i2 + 1),1)) `1 ) & ((G * (1,j1)) `2 ) <= t & t <= ((G * (1,(j1 + 1))) `2 ) } by A79, A78, A75, A73, GOBRD11: 32;

            then

            consider aa,ab be Real such that

             A82: a = |[aa, ab]| and

             A83: ((G * (i2,1)) `1 ) <= aa & aa <= ((G * ((i2 + 1),1)) `1 ) & ((G * (1,j1)) `2 ) <= ab & ab <= ((G * (1,(j1 + 1))) `2 ) by A27;

            

             A84: (A `1 ) = aa & (A `2 ) = ab by A82, EUCLID: 52;

             [i2, 1] in ( Indices G) by A32, A79, A78, MATRIX_0: 30;

            then

             A85: ( dist ((G * (i2,1)),(G * ((i2 + 1),1)))) = (((G * ((i2 + 1),1)) `1 ) - ((G * (i2,1)) `1 )) & ( dist ((G * (i2,1)),(G * ((i2 + 1),1)))) = ((e - w) / (2 |^ n)) by A80, GOBRD14: 5, GOBRD14: 10;

            consider r,t be Real such that

             A86: c = |[r, t]| and

             A87: ((G * (i2,1)) `1 ) <= r & r <= ((G * ((i2 + 1),1)) `1 ) & ((G * (1,j1)) `2 ) <= t & t <= ((G * (1,(j1 + 1))) `2 ) by A34, A81;

            (c9 `1 ) = r & (c9 `2 ) = t by A86, EUCLID: 52;

            hence ( dist (A,c9)) <= (((p - s) / (2 |^ n)) + ((e - w) / (2 |^ n))) by A87, A83, A84, A76, A85, TOPREAL6: 95;

          end;

            case

             A88: i1 = i2 & j1 = (j2 + 1);

            then

             A89: (j2 + 1) <= ( width G) by A22, MATRIX_0: 32;

            then

             A90: j2 < ( width G) by NAT_1: 13;

            

             A91: 1 <= j2 by A24, MATRIX_0: 32;

            then 1 <= (j2 + 1) by NAT_1: 13;

            then

             A92: [1, (j2 + 1)] in ( Indices G) by A30, A89, MATRIX_0: 30;

             [1, j2] in ( Indices G) by A30, A91, A90, MATRIX_0: 30;

            then

             A93: ( dist ((G * (1,j2)),(G * (1,(j2 + 1))))) = (((G * (1,(j2 + 1))) `2 ) - ((G * (1,j2)) `2 )) & ( dist ((G * (1,j2)),(G * (1,(j2 + 1))))) = ((p - s) / (2 |^ n)) by A92, GOBRD14: 6, GOBRD14: 9;

            

             A94: i1 <= ( len G) by A22, MATRIX_0: 32;

            i1 > 1 by A17, A22, A23, A24, A25, A88, Th2;

            then

             A95: (i1 - 1) > 0 by XREAL_1: 50;

            then

             A96: (i1 - 1) = (i1 -' 1) by XREAL_0:def 2;

            then

             A97: 1 <= (i1 -' 1) by A95, NAT_1: 14;

            (( len G) - 1) < (( len G) - 0 ) by XREAL_1: 15;

            then

             A98: (i1 -' 1) < ( len G) by A96, A94, XREAL_1: 15;

            then

             A99: [(i1 -' 1), 1] in ( Indices G) by A32, A97, MATRIX_0: 30;

            

             A100: ( right_cell (g,i,G)) = ( cell (G,(i1 -' 1),j2)) by A17, A21, A22, A23, A24, A25, A88, GOBRD13: 28

            .= { |[r, t]| where r,t be Real : ((G * ((i1 -' 1),1)) `1 ) <= r & r <= ((G * (((i1 -' 1) + 1),1)) `1 ) & ((G * (1,j2)) `2 ) <= t & t <= ((G * (1,(j2 + 1))) `2 ) } by A97, A98, A91, A90, GOBRD11: 32;

            then

            consider aa,ab be Real such that

             A101: a = |[aa, ab]| and

             A102: ((G * ((i1 -' 1),1)) `1 ) <= aa & aa <= ((G * (((i1 -' 1) + 1),1)) `1 ) & ((G * (1,j2)) `2 ) <= ab & ab <= ((G * (1,(j2 + 1))) `2 ) by A27;

            

             A103: (A `1 ) = aa & (A `2 ) = ab by A101, EUCLID: 52;

            1 <= ((i1 -' 1) + 1) by A97, NAT_1: 13;

            then [((i1 -' 1) + 1), 1] in ( Indices G) by A32, A96, A94, MATRIX_0: 30;

            then

             A104: ( dist ((G * ((i1 -' 1),1)),(G * (((i1 -' 1) + 1),1)))) = (((G * (((i1 -' 1) + 1),1)) `1 ) - ((G * ((i1 -' 1),1)) `1 )) & ( dist ((G * ((i1 -' 1),1)),(G * (((i1 -' 1) + 1),1)))) = ((e - w) / (2 |^ n)) by A99, GOBRD14: 5, GOBRD14: 10;

            consider r,t be Real such that

             A105: c = |[r, t]| and

             A106: ((G * ((i1 -' 1),1)) `1 ) <= r & r <= ((G * (((i1 -' 1) + 1),1)) `1 ) & ((G * (1,j2)) `2 ) <= t & t <= ((G * (1,(j2 + 1))) `2 ) by A34, A100;

            (c9 `1 ) = r & (c9 `2 ) = t by A105, EUCLID: 52;

            hence ( dist (A,c9)) <= (((p - s) / (2 |^ n)) + ((e - w) / (2 |^ n))) by A106, A102, A103, A93, A104, TOPREAL6: 95;

          end;

        end;

        then

         A107: ( dist (a9,c)) <= (((p - s) / (2 |^ n)) + ((e - w) / (2 |^ n))) by TOPREAL6:def 1;

        (1 + 1) <= ( len G) by A29, XXREAL_0: 2;

        then [(1 + 1), 1] in ( Indices G) by A32, MATRIX_0: 30;

        then

         A108: ( dist ((G * (1,1)),(G * ((1 + 1),1)))) = ((e - w) / (2 |^ n)) by A33, GOBRD14: 10;

        (1 + 1) <= ( width G) by A31, A29, XXREAL_0: 2;

        then [1, (1 + 1)] in ( Indices G) by A30, MATRIX_0: 30;

        then ( dist ((G * (1,1)),(G * (1,(1 + 1))))) = ((p - s) / (2 |^ n)) by A33, GOBRD14: 9;

        then (((p - s) / (2 |^ n)) + ((e - w) / (2 |^ n))) < ((d / 2) + (d / 2)) by A13, A108, XREAL_1: 8;

        hence contradiction by A28, A107, XXREAL_0: 2;

      end;

      

       A109: P c= (( L~ g) ` )

      proof

        let a be object;

        assume

         A110: a in P;

        then not a in ( L~ g) by A15, XBOOLE_0:def 4;

        hence thesis by A110, SUBSET_1: 29;

      end;

       0 < n or 0 = n;

      then ( N-bound ( L~ ( Cage (C, 0 )))) >= ( N-bound ( L~ g)) by Th7;

      then (g /. 1) = ( N-min ( L~ g)) & (q `2 ) > ( N-bound ( L~ g)) by A5, JORDAN9: 32, XXREAL_0: 2;

      then q in ( LeftComp g) by JORDAN2C: 113;

      then q in ( UBD ( L~ g)) by GOBRD14: 36;

      then

       A111: {q} c= ( UBD ( L~ g)) by ZFMISC_1: 31;

      

       A112: P is_an_arc_of (p,q) by A7, TOPREAL4: 2;

      now

        take a = q;

        thus a in {q} & a in P by A112, TARSKI:def 1, TOPREAL1: 1;

      end;

      then

       A113: {q} meets P by XBOOLE_0: 3;

      ( UBD ( L~ g)) is_outside_component_of ( L~ g) by JORDAN2C: 68;

      then ex E be Subset of (( TOP-REAL 2) | (( L~ g) ` )) st E = ( UBD ( L~ g)) & E is a_component & not E is bounded Subset of ( Euclid 2) by JORDAN2C: 14;

      then ( UBD ( L~ g)) is_a_component_of (( L~ g) ` ) by CONNSP_1:def 6;

      then P c= ( UBD ( L~ g)) by A109, A112, A111, A113, GOBOARD9: 4, JORDAN6: 10;

      hence thesis by A12, A14, TARSKI:def 4;

    end;

    theorem :: JORDAN10:15

    

     Th15: C c= ( meet ( BDD-Family C))

    proof

      for Z be set st Z in ( BDD-Family C) holds C c= Z

      proof

        let Z be set;

        assume Z in ( BDD-Family C);

        then

        consider k be Nat such that

         A1: Z = ( Cl ( BDD ( L~ ( Cage (C,k)))));

        C c= ( BDD ( L~ ( Cage (C,k)))) & ( BDD ( L~ ( Cage (C,k)))) c= ( Cl ( BDD ( L~ ( Cage (C,k))))) by Th12, PRE_TOPC: 18;

        hence thesis by A1;

      end;

      hence thesis by SETFAM_1: 5;

    end;

    theorem :: JORDAN10:16

    

     Th16: ( BDD C) misses ( LeftComp ( Cage (C,n)))

    proof

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

      assume (( BDD C) /\ ( LeftComp f)) <> {} ;

      then

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

       A1: x in (( BDD C) /\ ( LeftComp f)) by SUBSET_1: 4;

      ( BDD C) misses ( UBD C) by JORDAN2C: 24;

      then

       A2: (( BDD C) /\ ( UBD C)) = {} ;

      x in ( BDD C) by A1, XBOOLE_0:def 4;

      then not x in ( UBD C) by A2, XBOOLE_0:def 4;

      then

       A3: not x in ( union ( UBD-Family C)) by Th14;

      

       A4: x in ( LeftComp f) by A1, XBOOLE_0:def 4;

      ( UBD ( L~ f)) in the set of all ( UBD ( L~ ( Cage (C,k)))) where k be Nat;

      then not x in ( UBD ( L~ f)) by A3, TARSKI:def 4;

      hence contradiction by A4, GOBRD14: 36;

    end;

    theorem :: JORDAN10:17

    

     Th17: ( BDD C) c= ( RightComp ( Cage (C,n)))

    proof

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

      let x be object;

      ( LeftComp f) is_outside_component_of ( L~ f) by GOBRD14: 34;

      then

       A1: ( UBD ( L~ f)) = ( union { E where E be Subset of ( TOP-REAL 2) : E is_outside_component_of ( L~ f) }) & ( LeftComp f) in { E where E be Subset of ( TOP-REAL 2) : E is_outside_component_of ( L~ f) } by JORDAN2C:def 5;

      assume

       A2: x in ( BDD C);

       A3:

      now

        assume x in ( Cl ( LeftComp f));

        then ( BDD C) meets ( LeftComp f) by A2, PRE_TOPC:def 7;

        hence contradiction by Th16;

      end;

      ( BDD C) misses ( UBD C) by JORDAN2C: 24;

      then (( BDD C) /\ ( UBD C)) = {} ;

      then not x in ( UBD C) by A2, XBOOLE_0:def 4;

      then

       A4: not x in ( union ( UBD-Family C)) by Th14;

      ( UBD ( L~ f)) in the set of all ( UBD ( L~ ( Cage (C,k)))) where k be Nat;

      then not x in ( UBD ( L~ ( Cage (C,n)))) by A4, TARSKI:def 4;

      then

       A5: not x in ( LeftComp f) by A1, TARSKI:def 4;

      ( L~ f) = (( Cl ( LeftComp f)) \ ( LeftComp f)) by GOBRD14: 20;

      then not x in ( L~ f) by A3, XBOOLE_0:def 5;

      hence thesis by A2, A5, GOBRD14: 18;

    end;

    theorem :: JORDAN10:18

    

     Th18: P is_inside_component_of C implies P misses ( L~ ( Cage (C,n)))

    proof

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

      assume P is_inside_component_of C;

      then

       A1: P c= ( BDD C) by JORDAN2C: 22;

      assume (P /\ ( L~ f)) <> {} ;

      then

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

       A2: x in (P /\ ( L~ f)) by SUBSET_1: 4;

      x in P by A2, XBOOLE_0:def 4;

      then

       A3: x in ( BDD C) by A1;

      

       A4: ( BDD C) c= ( RightComp f) by Th17;

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

      hence contradiction by A3, A4, GOBRD14: 18;

    end;

    theorem :: JORDAN10:19

    

     Th19: ( BDD C) misses ( L~ ( Cage (C,n)))

    proof

      assume not thesis;

      then

      consider x be object such that

       A1: x in (( BDD C) /\ ( L~ ( Cage (C,n)))) by XBOOLE_0: 4;

      

       A2: x in ( L~ ( Cage (C,n))) by A1, XBOOLE_0:def 4;

      ( BDD C) = ( union { B where B be Subset of ( TOP-REAL 2) : B is_inside_component_of C }) & x in ( BDD C) by A1, JORDAN2C:def 4, XBOOLE_0:def 4;

      then

      consider Z be set such that

       A3: x in Z and

       A4: Z in { B where B be Subset of ( TOP-REAL 2) : B is_inside_component_of C } by TARSKI:def 4;

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

       A5: Z = B and

       A6: B is_inside_component_of C by A4;

      B misses ( L~ ( Cage (C,n))) by A6, Th18;

      then (B /\ ( L~ ( Cage (C,n)))) = {} ;

      hence thesis by A3, A5, A2, XBOOLE_0:def 4;

    end;

    theorem :: JORDAN10:20

    

     Th20: ( COMPLEMENT ( UBD-Family C)) = ( BDD-Family C)

    proof

      for P be Subset of ( TOP-REAL 2) holds P in ( BDD-Family C) iff (P ` ) in ( UBD-Family C)

      proof

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

        thus P in ( BDD-Family C) implies (P ` ) in ( UBD-Family C)

        proof

          assume P in ( BDD-Family C);

          then

          consider k such that

           A1: P = ( Cl ( BDD ( L~ ( Cage (C,k)))));

          P = ( Cl ( RightComp ( Cage (C,k)))) by A1, GOBRD14: 37;

          then

           A2: P = (( RightComp ( Cage (C,k))) \/ ( L~ ( Cage (C,k)))) by GOBRD14: 21;

          ((P ` ) /\ (( LeftComp ( Cage (C,k))) ` )) = ((P \/ ( LeftComp ( Cage (C,k)))) ` ) by XBOOLE_1: 53

          .= (( [#] the carrier of ( TOP-REAL 2)) ` ) by A2, GOBRD14: 15

          .= ( {} the carrier of ( TOP-REAL 2)) by XBOOLE_1: 37;

          then

           A3: (P ` ) misses (( LeftComp ( Cage (C,k))) ` );

          ( L~ ( Cage (C,k))) misses ( LeftComp ( Cage (C,k))) & ( RightComp ( Cage (C,k))) misses ( LeftComp ( Cage (C,k))) by GOBRD14: 14, SPRECT_3: 26;

          then P misses ( LeftComp ( Cage (C,k))) by A2, XBOOLE_1: 70;

          then (P ` ) = ( LeftComp ( Cage (C,k))) by A3, SUBSET_1: 25;

          then (P ` ) = ( UBD ( L~ ( Cage (C,k)))) by GOBRD14: 36;

          hence thesis;

        end;

        assume (P ` ) in ( UBD-Family C);

        then

        consider k such that

         A4: (P ` ) = ( UBD ( L~ ( Cage (C,k))));

        

         A5: (P ` ) = ( LeftComp ( Cage (C,k))) by A4, GOBRD14: 36;

        then (P ` ) misses ( RightComp ( Cage (C,k))) & (P ` ) misses ( L~ ( Cage (C,k))) by GOBRD14: 14, SPRECT_3: 26;

        then (P ` ) misses (( RightComp ( Cage (C,k))) \/ ( L~ ( Cage (C,k)))) by XBOOLE_1: 70;

        then

         A6: (P ` ) misses ( Cl ( RightComp ( Cage (C,k)))) by GOBRD14: 21;

        (((P ` ) ` ) /\ (( Cl ( RightComp ( Cage (C,k)))) ` )) = (((P ` ) \/ ( Cl ( RightComp ( Cage (C,k))))) ` ) by XBOOLE_1: 53

        .= (((P ` ) \/ (( RightComp ( Cage (C,k))) \/ ( L~ ( Cage (C,k))))) ` ) by GOBRD14: 21

        .= (( [#] the carrier of ( TOP-REAL 2)) ` ) by A5, GOBRD14: 15

        .= ( {} the carrier of ( TOP-REAL 2)) by XBOOLE_1: 37;

        then ((P ` ) ` ) misses (( Cl ( RightComp ( Cage (C,k)))) ` );

        then ((P ` ) ` ) = ( Cl ( RightComp ( Cage (C,k)))) by A6, SUBSET_1: 25;

        then P = ( Cl ( BDD ( L~ ( Cage (C,k))))) by GOBRD14: 37;

        hence thesis;

      end;

      hence thesis by SETFAM_1:def 7;

    end;

    theorem :: JORDAN10:21

    ( meet ( BDD-Family C)) = (C \/ ( BDD C))

    proof

      thus ( meet ( BDD-Family C)) c= (C \/ ( BDD C))

      proof

        let x be object;

        assume

         A1: x in ( meet ( BDD-Family C));

        ( COMPLEMENT ( UBD-Family C)) = ( BDD-Family C) by Th20;

        then (( [#] the carrier of ( TOP-REAL 2)) \ ( union ( UBD-Family C))) = ( meet ( BDD-Family C)) by SETFAM_1: 33;

        then not x in ( union ( UBD-Family C)) by A1, XBOOLE_0:def 5;

        then

         A2: not x in ( UBD C) by Th14;

        per cases ;

          suppose

           A3: not x in C;

          

           A4: (( BDD C) \/ ( UBD C)) = (C ` ) by JORDAN2C: 27;

          x in (C ` ) by A1, A3, SUBSET_1: 29;

          then x in ( BDD C) by A2, A4, XBOOLE_0:def 3;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose x in C;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      ( BDD C) misses ( UBD C) by JORDAN2C: 24;

      then

       A5: (( BDD C) /\ ( UBD C)) = {} ;

      

       A6: ( BDD C) c= ( meet ( BDD-Family C))

      proof

        let x be object;

        assume

         A7: x in ( BDD C);

        then not x in ( UBD C) by A5, XBOOLE_0:def 4;

        then

         A8: not x in ( union ( UBD-Family C)) by Th14;

        for Y be set st Y in ( BDD-Family C) holds x in Y

        proof

          let Y be set;

          assume Y in ( BDD-Family C);

          then

          consider n such that

           A9: Y = ( Cl ( BDD ( L~ ( Cage (C,n))))) and not contradiction;

          ( LeftComp ( Cage (C,n))) is_outside_component_of ( L~ ( Cage (C,n))) by GOBRD14: 34;

          then

           A10: ( LeftComp ( Cage (C,n))) in { B where B be Subset of ( TOP-REAL 2) : B is_outside_component_of ( L~ ( Cage (C,n))) };

          ( BDD C) misses ( L~ ( Cage (C,n))) by Th19;

          then (( BDD C) /\ ( L~ ( Cage (C,n)))) = {} ;

          then

           A11: not x in ( L~ ( Cage (C,n))) by A7, XBOOLE_0:def 4;

          ( RightComp ( Cage (C,n))) is_inside_component_of ( L~ ( Cage (C,n))) by GOBRD14: 35;

          then

           A12: ( RightComp ( Cage (C,n))) in { B where B be Subset of ( TOP-REAL 2) : B is_inside_component_of ( L~ ( Cage (C,n))) };

          ( UBD ( L~ ( Cage (C,n)))) in ( UBD-Family C);

          then ( UBD ( L~ ( Cage (C,n)))) = ( union { B where B be Subset of ( TOP-REAL 2) : B is_outside_component_of ( L~ ( Cage (C,n))) }) & not x in ( UBD ( L~ ( Cage (C,n)))) by A8, JORDAN2C:def 5, TARSKI:def 4;

          then not x in ( LeftComp ( Cage (C,n))) by A10, TARSKI:def 4;

          then ( BDD ( L~ ( Cage (C,n)))) = ( union { B where B be Subset of ( TOP-REAL 2) : B is_inside_component_of ( L~ ( Cage (C,n))) }) & x in ( RightComp ( Cage (C,n))) by A7, A11, GOBRD14: 18, JORDAN2C:def 4;

          then

           A13: x in ( BDD ( L~ ( Cage (C,n)))) by A12, TARSKI:def 4;

          ( BDD ( L~ ( Cage (C,n)))) c= ( Cl ( BDD ( L~ ( Cage (C,n))))) by PRE_TOPC: 18;

          hence thesis by A9, A13;

        end;

        hence thesis by SETFAM_1:def 1;

      end;

      C c= ( meet ( BDD-Family C)) by Th15;

      hence thesis by A6, XBOOLE_1: 8;

    end;