jordan14.miz



    begin

    theorem :: JORDAN14:1

    

     Th1: for f be non constant standard special_circular_sequence holds ( BDD ( L~ f)) = ( RightComp f) or ( BDD ( L~ f)) = ( LeftComp f)

    proof

      let f be non constant standard special_circular_sequence;

      ( BDD ( L~ f)) is_inside_component_of ( L~ f) by JORDAN2C: 108;

      then ( BDD ( L~ f)) is_a_component_of (( L~ f) ` ) by JORDAN2C:def 2;

      hence thesis by JORDAN1H: 24;

    end;

    theorem :: JORDAN14:2

    for f be non constant standard special_circular_sequence holds ( UBD ( L~ f)) = ( RightComp f) or ( UBD ( L~ f)) = ( LeftComp f)

    proof

      let f be non constant standard special_circular_sequence;

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

      then ( UBD ( L~ f)) is_a_component_of (( L~ f) ` ) by JORDAN2C:def 3;

      hence thesis by JORDAN1H: 24;

    end;

    theorem :: JORDAN14:3

    for G be Go-board holds for f be FinSequence of ( TOP-REAL 2) holds for k be Nat holds 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G implies ( left_cell (f,k,G)) is closed

    proof

      let G be Go-board;

      let f be FinSequence of ( TOP-REAL 2);

      let k be Nat;

      assume that

       A1: 1 <= k and

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

       A3: f is_sequence_on G;

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

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

       A5: (f /. k) = (G * (i1,j1)) and

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

       A7: (f /. (k + 1)) = (G * (i2,j2)) and

       A8: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A1, A2, A3, JORDAN8: 3;

      i1 = i2 & (j1 + 1) = j2 & ( left_cell (f,k,G)) = ( cell (G,(i1 -' 1),j1)) or (i1 + 1) = i2 & j1 = j2 & ( left_cell (f,k,G)) = ( cell (G,i1,j1)) or i1 = (i2 + 1) & j1 = j2 & ( left_cell (f,k,G)) = ( cell (G,i2,(j2 -' 1))) or i1 = i2 & j1 = (j2 + 1) & ( left_cell (f,k,G)) = ( cell (G,i1,j2)) by A1, A2, A3, A4, A5, A6, A7, A8, GOBRD13:def 3;

      hence thesis by GOBRD11: 33;

    end;

    theorem :: JORDAN14:4

    

     Th4: for G be Go-board holds for p be Point of ( TOP-REAL 2) holds for i,j be Nat st 1 <= i & (i + 1) <= ( len G) & 1 <= j & (j + 1) <= ( width G) holds p in ( Int ( cell (G,i,j))) iff ((G * (i,j)) `1 ) < (p `1 ) & (p `1 ) < ((G * ((i + 1),j)) `1 ) & ((G * (i,j)) `2 ) < (p `2 ) & (p `2 ) < ((G * (i,(j + 1))) `2 )

    proof

      let G be Go-board;

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

      let i,j be Nat;

      assume that

       A1: 1 <= i and

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

       A3: 1 <= j and

       A4: (j + 1) <= ( width G);

      set Z = { |[r, s]| where r,s be Real : ((G * (i,1)) `1 ) < r & r < ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s & s < ((G * (1,(j + 1))) `2 ) };

      

       A5: j < ( width G) by A4, NAT_1: 13;

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

      then

       A6: ((G * ((i + 1),1)) `1 ) = ((G * ((i + 1),j)) `1 ) by A2, A3, A5, GOBOARD5: 2;

      

       A7: i < ( len G) by A2, NAT_1: 13;

      then

       A8: ((G * (1,j)) `2 ) = ((G * (i,j)) `2 ) by A1, A3, A5, GOBOARD5: 1;

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

      then

       A9: ((G * (1,(j + 1))) `2 ) = ((G * (i,(j + 1))) `2 ) by A1, A4, A7, GOBOARD5: 1;

      

       A10: ((G * (i,1)) `1 ) = ((G * (i,j)) `1 ) by A1, A3, A7, A5, GOBOARD5: 2;

      thus p in ( Int ( cell (G,i,j))) implies ((G * (i,j)) `1 ) < (p `1 ) & (p `1 ) < ((G * ((i + 1),j)) `1 ) & ((G * (i,j)) `2 ) < (p `2 ) & (p `2 ) < ((G * (i,(j + 1))) `2 )

      proof

        assume p in ( Int ( cell (G,i,j)));

        then p in Z by A1, A3, A7, A5, GOBOARD6: 26;

        then ex r,s be Real st p = |[r, s]| & ((G * (i,1)) `1 ) < r & r < ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s & s < ((G * (1,(j + 1))) `2 );

        hence thesis by A10, A6, A8, A9, EUCLID: 52;

      end;

      assume that

       A11: ((G * (i,j)) `1 ) < (p `1 ) and

       A12: (p `1 ) < ((G * ((i + 1),j)) `1 ) and

       A13: ((G * (i,j)) `2 ) < (p `2 ) and

       A14: (p `2 ) < ((G * (i,(j + 1))) `2 );

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

      then p in Z by A10, A6, A8, A9, A11, A12, A13, A14;

      hence thesis by A1, A3, A7, A5, GOBOARD6: 26;

    end;

    theorem :: JORDAN14:5

    

     Th5: for f be non constant standard special_circular_sequence holds ( BDD ( L~ f)) is connected

    proof

      let f be non constant standard special_circular_sequence;

      ( BDD ( L~ f)) = ( RightComp f) or ( BDD ( L~ f)) = ( LeftComp f) by Th1;

      hence thesis;

    end;

    registration

      let f be non constant standard special_circular_sequence;

      cluster ( BDD ( L~ f)) -> connected;

      coherence by Th5;

    end

    definition

      let C be Simple_closed_curve;

      let n be Nat;

      :: JORDAN14:def1

      func SpanStart (C,n) -> Point of ( TOP-REAL 2) equals (( Gauge (C,n)) * (( X-SpanStart (C,n)),( Y-SpanStart (C,n))));

      coherence ;

    end

    theorem :: JORDAN14:6

    

     Th6: for C be Simple_closed_curve holds for n be Nat st n is_sufficiently_large_for C holds ( SpanStart (C,n)) in ( BDD C)

    proof

      let C be Simple_closed_curve;

      let n be Nat;

      

       A1: 1 <= (( X-SpanStart (C,n)) -' 1) by JORDAN1H: 50;

      

       A2: (( X-SpanStart (C,n)) -' 1) < ( len ( Gauge (C,n))) by JORDAN1H: 50;

      assume

       A3: n is_sufficiently_large_for C;

      then

       A4: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n)))) c= ( BDD C) by JORDAN11: 6;

      

       A5: ( Y-SpanStart (C,n)) <= ( width ( Gauge (C,n))) by A3, JORDAN11: 7;

      1 < ( Y-SpanStart (C,n)) by A3, JORDAN11: 7;

      then ( LSeg ((( Gauge (C,n)) * ((( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n)))),(( Gauge (C,n)) * (((( X-SpanStart (C,n)) -' 1) + 1),( Y-SpanStart (C,n)))))) c= ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n)))) by A1, A2, A5, GOBOARD5: 22;

      then

       A6: ( LSeg ((( Gauge (C,n)) * ((( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n)))),(( Gauge (C,n)) * (((( X-SpanStart (C,n)) -' 1) + 1),( Y-SpanStart (C,n)))))) c= ( BDD C) by A4;

      

       A7: 2 < ( X-SpanStart (C,n)) by JORDAN1H: 49;

      (( Gauge (C,n)) * (((( X-SpanStart (C,n)) -' 1) + 1),( Y-SpanStart (C,n)))) in ( LSeg ((( Gauge (C,n)) * ((( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n)))),(( Gauge (C,n)) * (((( X-SpanStart (C,n)) -' 1) + 1),( Y-SpanStart (C,n)))))) by RLTOPSP1: 68;

      then (( Gauge (C,n)) * (((( X-SpanStart (C,n)) -' 1) + 1),( Y-SpanStart (C,n)))) in ( BDD C) by A6;

      hence thesis by A7, XREAL_1: 235, XXREAL_0: 2;

    end;

    theorem :: JORDAN14:7

    

     Th7: for C be Simple_closed_curve holds for n,k be Nat st n is_sufficiently_large_for C holds 1 <= k & (k + 1) <= ( len ( Span (C,n))) implies ( right_cell (( Span (C,n)),k,( Gauge (C,n)))) misses C & ( left_cell (( Span (C,n)),k,( Gauge (C,n)))) meets C

    proof

      let C be Simple_closed_curve;

      let n,k be Nat;

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

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

      defpred P[ Nat] means for m be Nat st 1 <= m & (m + 1) <= ( len (f | $1)) holds ( right_cell ((f | $1),m,G)) misses C & ( left_cell ((f | $1),m,G)) meets C;

      

       A1: (f | ( len f)) = f by FINSEQ_1: 58;

      assume

       A2: n is_sufficiently_large_for C;

      then

       A3: f is_sequence_on G by JORDAN13:def 1;

      

       A4: (f /. 2) = (G * ((( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n)))) by A2, JORDAN13:def 1;

      

       A5: (f /. 1) = (G * (( X-SpanStart (C,n)),( Y-SpanStart (C,n)))) by A2, JORDAN13:def 1;

      

       A6: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A7: for m be Nat st 1 <= m & (m + 1) <= ( len (f | k)) holds ( right_cell ((f | k),m,G)) misses C & ( left_cell ((f | k),m,G)) meets C;

        

         A8: (f | (k + 1)) is_sequence_on G by A3, GOBOARD1: 22;

        

         A9: (f | k) is_sequence_on G by A3, GOBOARD1: 22;

        per cases ;

          suppose

           A10: k >= ( len f);

          then

           A11: (f | (k + 1)) = f by FINSEQ_1: 58, NAT_1: 12;

          (f | k) = f by A10, FINSEQ_1: 58;

          hence thesis by A7, A11;

        end;

          suppose

           A12: k < ( len f);

          let m be Nat;

          assume that

           A13: 1 <= m and

           A14: (m + 1) <= ( len (f | (k + 1)));

          

           A15: (k + 1) <= ( len f) by A12, NAT_1: 13;

          then

           A16: ( len (f | (k + 1))) = (k + 1) by FINSEQ_1: 59;

          

           A17: ( len (f | k)) = k by A12, FINSEQ_1: 59;

          now

            per cases by NAT_1: 25;

              suppose

               A18: k = 0 ;

              1 <= (m + 1) by NAT_1: 12;

              then (m + 1) = ( 0 + 1) by A14, A18, XXREAL_0: 1;

              hence thesis by A13;

            end;

              suppose

               A19: k = 1;

              set j = ( Y-SpanStart (C,n));

              set i = ( X-SpanStart (C,n));

              

               A20: (f | (k + 1)) = <*(G * (i,j)), (G * ((i -' 1),j))*> by A5, A4, A15, A19, FINSEQ_5: 81;

              then

               A21: ((f | (k + 1)) /. 1) = (G * (i,j)) by FINSEQ_4: 17;

              (1 + 1) <= (m + 1) by A13, XREAL_1: 6;

              then

               A22: (m + 1) = (1 + 1) by A16, A14, A19, XXREAL_0: 1;

              

               A23: [(i -' 1), j] in ( Indices G) by A2, JORDAN11: 9;

              

               A24: [i, j] in ( Indices G) by A2, JORDAN11: 8;

              (i -' 1) <= i by NAT_D: 35;

              then

               A25: (i + 1) <> (i -' 1) by NAT_1: 13;

              

               A26: j <> (j + 1);

              

               A27: ((f | (k + 1)) /. 2) = (G * ((i -' 1),j)) by A20, FINSEQ_4: 17;

              then ( right_cell ((f | (k + 1)),m,G)) = ( cell (G,(i -' 1),j)) by A8, A14, A21, A24, A23, A22, A26, A25, GOBRD13:def 2;

              hence ( right_cell ((f | (k + 1)),m,G)) misses C by A2, JORDAN11: 11;

              ( left_cell ((f | (k + 1)),m,G)) = ( cell (G,(i -' 1),(j -' 1))) by A8, A14, A21, A27, A24, A23, A22, A26, A25, GOBRD13:def 3;

              hence ( left_cell ((f | (k + 1)),m,G)) meets C by A2, JORDAN11: 10;

            end;

              suppose

               A28: k > 1;

              

               A29: ( len (f | k)) <= ( len f) by FINSEQ_5: 16;

              

               A30: 1 <= (( len (f | k)) -' 1) by A17, A28, NAT_D: 49;

              

               A31: ((( len (f | k)) -' 1) + 1) = ( len (f | k)) by A17, A28, XREAL_1: 235;

              then

               A32: ((( len (f | k)) -' 1) + (1 + 1)) = (( len (f | k)) + 1);

              now

                per cases ;

                  suppose

                   A33: (m + 1) = ( len (f | (k + 1)));

                  ( left_cell ((f | k),(( len (f | k)) -' 1),G)) meets C by A7, A30, A31;

                  then

                   A34: ( left_cell (f,(( len (f | k)) -' 1),G)) meets C by A3, A17, A30, A31, A29, GOBRD13: 31;

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

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

                   A36: (f /. (( len (f | k)) -' 1)) = (G * (i1,j1)) and

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

                   A38: (f /. ( len (f | k))) = (G * (i2,j2)) and i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A3, A12, A17, A30, A31, JORDAN8: 3;

                  1 <= i2 by A37, MATRIX_0: 32;

                  then

                   A39: ((i2 -' 1) + 1) = i2 by XREAL_1: 235;

                  

                   A40: 1 <= j2 by A37, MATRIX_0: 32;

                  then

                   A41: ((j2 -' 1) + 1) = j2 by XREAL_1: 235;

                  ( right_cell ((f | k),(( len (f | k)) -' 1),G)) misses C by A7, A30, A31;

                  then

                   A42: ( right_cell (f,(( len (f | k)) -' 1),G)) misses C by A3, A17, A30, A31, A29, GOBRD13: 31;

                  now

                    per cases ;

                      suppose

                       A43: ( front_right_cell (f,(( len (f | k)) -' 1),G)) misses C & ( front_left_cell (f,(( len (f | k)) -' 1),G)) misses C;

                      then

                       A44: f turns_left ((( len (f | k)) -' 1),G) by A2, A15, A17, A30, A32, JORDAN13:def 1;

                      now

                        per cases by A31, A35, A36, A37, A38, A44, GOBRD13:def 7;

                          suppose that

                           A45: i1 = i2 & (j1 + 1) = j2 and

                           A46: [(i2 -' 1), j2] in ( Indices G) and

                           A47: (f /. ((( len (f | k)) -' 1) + 2)) = (G * ((i2 -' 1),j2));

                          ( cell (G,(i1 -' 1),(j1 + 1))) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A43, A45, GOBRD13: 34;

                          then ( right_cell (f,m,G)) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A45, A46, A47, GOBRD13: 26;

                          hence ( right_cell ((f | (k + 1)),m,G)) misses C by A3, A15, A16, A13, A33, GOBRD13: 31;

                          

                           A48: ((j1 + 1) -' 1) = j1 by NAT_D: 34;

                          ( cell (G,(i1 -' 1),j1)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A45, GOBRD13: 21;

                          then ( left_cell (f,m,G)) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A45, A46, A47, A48, GOBRD13: 25;

                          hence ( left_cell ((f | (k + 1)),m,G)) meets C by A3, A15, A16, A13, A33, GOBRD13: 31;

                        end;

                          suppose that

                           A49: (i1 + 1) = i2 & j1 = j2 and

                           A50: [i2, (j2 + 1)] in ( Indices G) and

                           A51: (f /. ((( len (f | k)) -' 1) + 2)) = (G * (i2,(j2 + 1)));

                          ( cell (G,i2,j2)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A43, A49, GOBRD13: 36;

                          then ( right_cell (f,m,G)) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A50, A51, GOBRD13: 22;

                          hence ( right_cell ((f | (k + 1)),m,G)) misses C by A3, A15, A16, A13, A33, GOBRD13: 31;

                          

                           A52: ((i1 + 1) -' 1) = i1 by NAT_D: 34;

                          ( cell (G,i1,j2)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A49, GOBRD13: 23;

                          then ( left_cell (f,m,G)) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A49, A50, A51, A52, GOBRD13: 21;

                          hence ( left_cell ((f | (k + 1)),m,G)) meets C by A3, A15, A16, A13, A33, GOBRD13: 31;

                        end;

                          suppose that

                           A53: i1 = (i2 + 1) & j1 = j2 and

                           A54: [i2, (j2 -' 1)] in ( Indices G) and

                           A55: (f /. ((( len (f | k)) -' 1) + 2)) = (G * (i2,(j2 -' 1)));

                          ( cell (G,(i2 -' 1),(j2 -' 1))) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A43, A53, GOBRD13: 38;

                          then ( right_cell (f,m,G)) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A54, A55, GOBRD13: 28;

                          hence ( right_cell ((f | (k + 1)),m,G)) misses C by A3, A15, A16, A13, A33, GOBRD13: 31;

                          ( cell (G,i2,(j2 -' 1))) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A53, GOBRD13: 25;

                          then ( left_cell (f,m,G)) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A54, A55, GOBRD13: 27;

                          hence ( left_cell ((f | (k + 1)),m,G)) meets C by A3, A15, A16, A13, A33, GOBRD13: 31;

                        end;

                          suppose that

                           A56: i1 = i2 & j1 = (j2 + 1) and

                           A57: [(i2 + 1), j2] in ( Indices G) and

                           A58: (f /. ((( len (f | k)) -' 1) + 2)) = (G * ((i2 + 1),j2));

                          ( cell (G,i1,(j2 -' 1))) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A43, A56, GOBRD13: 40;

                          then ( right_cell (f,m,G)) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A56, A57, A58, GOBRD13: 24;

                          hence ( right_cell ((f | (k + 1)),m,G)) misses C by A3, A15, A16, A13, A33, GOBRD13: 31;

                          ( cell (G,i1,j2)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A56, GOBRD13: 27;

                          then ( left_cell (f,m,G)) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A56, A57, A58, GOBRD13: 23;

                          hence ( left_cell ((f | (k + 1)),m,G)) meets C by A3, A15, A16, A13, A33, GOBRD13: 31;

                        end;

                      end;

                      hence thesis;

                    end;

                      suppose

                       A59: ( front_right_cell (f,(( len (f | k)) -' 1),G)) misses C & ( front_left_cell (f,(( len (f | k)) -' 1),G)) meets C;

                      then

                       A60: f goes_straight ((( len (f | k)) -' 1),G) by A2, A15, A17, A30, A32, JORDAN13:def 1;

                      now

                        per cases by A31, A35, A36, A37, A38, A60, GOBRD13:def 8;

                          suppose that

                           A61: i1 = i2 & (j1 + 1) = j2 and

                           A62: [i2, (j2 + 1)] in ( Indices G) and

                           A63: (f /. ((( len (f | k)) -' 1) + 2)) = (G * (i2,(j2 + 1)));

                          ( cell (G,i1,(j1 + 1))) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A59, A61, GOBRD13: 35;

                          then ( right_cell (f,m,G)) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A61, A62, A63, GOBRD13: 22;

                          hence ( right_cell ((f | (k + 1)),m,G)) misses C by A3, A15, A16, A13, A33, GOBRD13: 31;

                          ( cell (G,(i2 -' 1),j2)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A61, GOBRD13: 34;

                          then ( left_cell (f,m,G)) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A62, A63, GOBRD13: 21;

                          hence ( left_cell ((f | (k + 1)),m,G)) meets C by A3, A15, A16, A13, A33, GOBRD13: 31;

                        end;

                          suppose that

                           A64: (i1 + 1) = i2 & j1 = j2 and

                           A65: [(i2 + 1), j2] in ( Indices G) and

                           A66: (f /. ((( len (f | k)) -' 1) + 2)) = (G * ((i2 + 1),j2));

                          ( cell (G,(i1 + 1),(j1 -' 1))) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A59, A64, GOBRD13: 37;

                          then ( right_cell (f,m,G)) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A64, A65, A66, GOBRD13: 24;

                          hence ( right_cell ((f | (k + 1)),m,G)) misses C by A3, A15, A16, A13, A33, GOBRD13: 31;

                          ( cell (G,(i1 + 1),j1)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A64, GOBRD13: 36;

                          then ( left_cell (f,m,G)) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A64, A65, A66, GOBRD13: 23;

                          hence ( left_cell ((f | (k + 1)),m,G)) meets C by A3, A15, A16, A13, A33, GOBRD13: 31;

                        end;

                          suppose that

                           A67: i1 = (i2 + 1) & j1 = j2 and

                           A68: [(i2 -' 1), j2] in ( Indices G) and

                           A69: (f /. ((( len (f | k)) -' 1) + 2)) = (G * ((i2 -' 1),j2));

                          ( cell (G,(i2 -' 1),j2)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A59, A67, GOBRD13: 39;

                          then ( right_cell (f,m,G)) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A68, A69, GOBRD13: 26;

                          hence ( right_cell ((f | (k + 1)),m,G)) misses C by A3, A15, A16, A13, A33, GOBRD13: 31;

                          ( cell (G,(i2 -' 1),(j2 -' 1))) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A67, GOBRD13: 38;

                          then ( left_cell (f,m,G)) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A68, A69, GOBRD13: 25;

                          hence ( left_cell ((f | (k + 1)),m,G)) meets C by A3, A15, A16, A13, A33, GOBRD13: 31;

                        end;

                          suppose that

                           A70: i1 = i2 & j1 = (j2 + 1) and

                           A71: [i2, (j2 -' 1)] in ( Indices G) and

                           A72: (f /. ((( len (f | k)) -' 1) + 2)) = (G * (i2,(j2 -' 1)));

                          

                           A73: ((j2 -' 1) + 1) = j2 by A40, XREAL_1: 235;

                          ( cell (G,(i2 -' 1),(j2 -' 1))) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A59, A70, GOBRD13: 41;

                          then ( right_cell (f,m,G)) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A71, A72, A73, GOBRD13: 28;

                          hence ( right_cell ((f | (k + 1)),m,G)) misses C by A3, A15, A16, A13, A33, GOBRD13: 31;

                          ( cell (G,i2,(j2 -' 1))) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A70, GOBRD13: 40;

                          then ( left_cell (f,m,G)) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A71, A72, GOBRD13: 27;

                          hence ( left_cell ((f | (k + 1)),m,G)) meets C by A3, A15, A16, A13, A33, GOBRD13: 31;

                        end;

                      end;

                      hence thesis;

                    end;

                      suppose

                       A74: ( front_right_cell (f,(( len (f | k)) -' 1),G)) meets C;

                      then

                       A75: f turns_right ((( len (f | k)) -' 1),G) by A2, A15, A17, A30, A32, JORDAN13:def 1;

                      now

                        per cases by A31, A35, A36, A37, A38, A75, GOBRD13:def 6;

                          suppose that

                           A76: i1 = i2 & (j1 + 1) = j2 and

                           A77: [(i2 + 1), j2] in ( Indices G) and

                           A78: (f /. ((( len (f | k)) -' 1) + 2)) = (G * ((i2 + 1),j2));

                          

                           A79: ((j1 + 1) -' 1) = j1 by NAT_D: 34;

                          ( cell (G,i1,j1)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A42, A76, GOBRD13: 22;

                          then ( right_cell (f,m,G)) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A76, A77, A78, A79, GOBRD13: 24;

                          hence ( right_cell ((f | (k + 1)),m,G)) misses C by A3, A15, A16, A13, A33, GOBRD13: 31;

                          ( cell (G,i2,j2)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A76, GOBRD13: 35;

                          then ( left_cell (f,m,G)) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A77, A78, GOBRD13: 23;

                          hence ( left_cell ((f | (k + 1)),m,G)) meets C by A3, A15, A16, A13, A33, GOBRD13: 31;

                        end;

                          suppose that

                           A80: (i1 + 1) = i2 & j1 = j2 and

                           A81: [i2, (j2 -' 1)] in ( Indices G) and

                           A82: (f /. ((( len (f | k)) -' 1) + 2)) = (G * (i2,(j2 -' 1)));

                          

                           A83: ((i1 + 1) -' 1) = i1 by NAT_D: 34;

                          ( cell (G,i1,(j1 -' 1))) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A42, A80, GOBRD13: 24;

                          then ( right_cell (f,m,G)) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A80, A81, A82, A83, GOBRD13: 28;

                          hence ( right_cell ((f | (k + 1)),m,G)) misses C by A3, A15, A16, A13, A33, GOBRD13: 31;

                          ( cell (G,i2,(j2 -' 1))) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A80, GOBRD13: 37;

                          then ( left_cell (f,m,G)) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A81, A82, GOBRD13: 27;

                          hence ( left_cell ((f | (k + 1)),m,G)) meets C by A3, A15, A16, A13, A33, GOBRD13: 31;

                        end;

                          suppose that

                           A84: i1 = (i2 + 1) & j1 = j2 and

                           A85: [i2, (j2 + 1)] in ( Indices G) and

                           A86: (f /. ((( len (f | k)) -' 1) + 2)) = (G * (i2,(j2 + 1)));

                          ( cell (G,i2,j2)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A42, A84, GOBRD13: 26;

                          then ( right_cell (f,m,G)) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A85, A86, GOBRD13: 22;

                          hence ( right_cell ((f | (k + 1)),m,G)) misses C by A3, A15, A16, A13, A33, GOBRD13: 31;

                          ( cell (G,(i2 -' 1),j2)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A84, GOBRD13: 39;

                          then ( left_cell (f,m,G)) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A85, A86, GOBRD13: 21;

                          hence ( left_cell ((f | (k + 1)),m,G)) meets C by A3, A15, A16, A13, A33, GOBRD13: 31;

                        end;

                          suppose that

                           A87: i1 = i2 & j1 = (j2 + 1) and

                           A88: [(i2 -' 1), j2] in ( Indices G) and

                           A89: (f /. ((( len (f | k)) -' 1) + 2)) = (G * ((i2 -' 1),j2));

                          ( cell (G,(i2 -' 1),j2)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A42, A87, GOBRD13: 28;

                          then ( right_cell (f,m,G)) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A88, A89, GOBRD13: 26;

                          hence ( right_cell ((f | (k + 1)),m,G)) misses C by A3, A15, A16, A13, A33, GOBRD13: 31;

                          ( cell (G,(i2 -' 1),(j2 -' 1))) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A87, GOBRD13: 41;

                          then ( left_cell (f,m,G)) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A88, A89, GOBRD13: 25;

                          hence ( left_cell ((f | (k + 1)),m,G)) meets C by A3, A15, A16, A13, A33, GOBRD13: 31;

                        end;

                      end;

                      hence thesis;

                    end;

                  end;

                  hence thesis;

                end;

                  suppose (m + 1) <> ( len (f | (k + 1)));

                  then (m + 1) < ( len (f | (k + 1))) by A14, XXREAL_0: 1;

                  then

                   A90: (m + 1) <= ( len (f | k)) by A16, A17, NAT_1: 13;

                  then

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

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

                   A92: ((f | k) /. m) = (G * (i1,j1)) and

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

                   A94: ((f | k) /. (m + 1)) = (G * (i2,j2)) and

                   A95: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A9, A13, JORDAN8: 3;

                  

                   A96: ( right_cell ((f | k),m,G)) misses C by A7, A13, A90;

                  

                   A97: (f | (k + 1)) = ((f | k) ^ <*(f /. (k + 1))*>) by A15, FINSEQ_5: 82;

                  1 <= (m + 1) by NAT_1: 12;

                  then (m + 1) in ( dom (f | k)) by A90, FINSEQ_3: 25;

                  then

                   A98: ((f | (k + 1)) /. (m + 1)) = (G * (i2,j2)) by A94, A97, FINSEQ_4: 68;

                  

                   A99: ( left_cell ((f | k),m,G)) meets C by A7, A13, A90;

                  m <= ( len (f | k)) by A90, NAT_1: 13;

                  then m in ( dom (f | k)) by A13, FINSEQ_3: 25;

                  then

                   A100: ((f | (k + 1)) /. m) = (G * (i1,j1)) by A92, A97, FINSEQ_4: 68;

                  now

                    per cases by A95;

                      suppose

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

                      then

                       A102: ( left_cell ((f | k),m,G)) = ( cell (G,(i1 -' 1),j1)) by A9, A13, A90, A91, A92, A93, A94, GOBRD13: 21;

                      ( right_cell ((f | k),m,G)) = ( cell (G,i1,j1)) by A9, A13, A90, A91, A92, A93, A94, A101, GOBRD13: 22;

                      hence thesis by A8, A13, A14, A91, A93, A96, A99, A100, A98, A101, A102, GOBRD13: 21, GOBRD13: 22;

                    end;

                      suppose

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

                      then

                       A104: ( left_cell ((f | k),m,G)) = ( cell (G,i1,j1)) by A9, A13, A90, A91, A92, A93, A94, GOBRD13: 23;

                      ( right_cell ((f | k),m,G)) = ( cell (G,i1,(j1 -' 1))) by A9, A13, A90, A91, A92, A93, A94, A103, GOBRD13: 24;

                      hence thesis by A8, A13, A14, A91, A93, A96, A99, A100, A98, A103, A104, GOBRD13: 23, GOBRD13: 24;

                    end;

                      suppose

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

                      then

                       A106: ( left_cell ((f | k),m,G)) = ( cell (G,i2,(j2 -' 1))) by A9, A13, A90, A91, A92, A93, A94, GOBRD13: 25;

                      ( right_cell ((f | k),m,G)) = ( cell (G,i2,j2)) by A9, A13, A90, A91, A92, A93, A94, A105, GOBRD13: 26;

                      hence thesis by A8, A13, A14, A91, A93, A96, A99, A100, A98, A105, A106, GOBRD13: 25, GOBRD13: 26;

                    end;

                      suppose

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

                      then

                       A108: ( left_cell ((f | k),m,G)) = ( cell (G,i1,j2)) by A9, A13, A90, A91, A92, A93, A94, GOBRD13: 27;

                      ( right_cell ((f | k),m,G)) = ( cell (G,(i2 -' 1),j2)) by A9, A13, A90, A91, A92, A93, A94, A107, GOBRD13: 28;

                      hence thesis by A8, A13, A14, A91, A93, A96, A99, A100, A98, A107, A108, GOBRD13: 27, GOBRD13: 28;

                    end;

                  end;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

      end;

      

       A109: P[ 0 ] by CARD_1: 27;

      for k be Nat holds P[k] from NAT_1:sch 2( A109, A6);

      hence thesis by A1;

    end;

    theorem :: JORDAN14:8

    

     Th8: for C be Simple_closed_curve holds for n be Nat st n is_sufficiently_large_for C holds C misses ( L~ ( Span (C,n)))

    proof

      let C be Simple_closed_curve;

      let n be Nat;

      assume

       A1: n is_sufficiently_large_for C;

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

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

      assume not thesis;

      then

      consider c be object such that

       A2: c in C and

       A3: 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

       A4: c in Z and

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

      consider i be Nat such that

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

       A7: 1 <= i and

       A8: (i + 1) <= ( len f) by A5;

      f is_sequence_on G by A1, JORDAN13:def 1;

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

      then

       A9: c in ( right_cell (f,i,G)) by A4, A6, XBOOLE_0:def 4;

      ( right_cell (f,i,G)) misses C by A1, A7, A8, Th7;

      hence contradiction by A2, A9, XBOOLE_0: 3;

    end;

    registration

      let C be Simple_closed_curve;

      let n be Nat;

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

      coherence by GOBRD14: 32;

    end

    theorem :: JORDAN14:9

    

     Th9: for C be Simple_closed_curve holds for n be Nat st n is_sufficiently_large_for C holds C meets ( LeftComp ( Span (C,n)))

    proof

      let C be Simple_closed_curve;

      let n be Nat;

      assume

       A1: n is_sufficiently_large_for C;

      then

       A2: ( Span (C,n)) is_sequence_on ( Gauge (C,n)) by JORDAN13:def 1;

      

       A3: (1 + 1) <= ( len ( Span (C,n))) by GOBOARD7: 34, XXREAL_0: 2;

      then ( left_cell (( Span (C,n)),1,( Gauge (C,n)))) meets C by A1, Th7;

      then (( left_cell (( Span (C,n)),1,( Gauge (C,n)))) \ ( L~ ( Span (C,n)))) meets C by A1, Th8, XBOOLE_1: 84;

      hence thesis by A3, A2, JORDAN9: 27, XBOOLE_1: 63;

    end;

    theorem :: JORDAN14:10

    

     Th10: for C be Simple_closed_curve holds for n be Nat st n is_sufficiently_large_for C holds C misses ( RightComp ( Span (C,n)))

    proof

      let C be Simple_closed_curve;

      let n be Nat;

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

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

      then

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

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

      then

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

      assume

       A3: n is_sufficiently_large_for C;

      then

       A4: C misses ( L~ f) by Th8;

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

      proof

        let c be object;

        assume

         A5: c in C;

        then not c in ( L~ f) by A4, XBOOLE_0: 3;

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

        hence thesis by PRE_TOPC: 8;

      end;

      then

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

      assume

       A6: C meets ( RightComp f);

      

       A7: C1 is connected by CONNSP_1: 23;

      C meets ( LeftComp f) by A3, Th9;

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

    end;

    theorem :: JORDAN14:11

    

     Th11: for C be Simple_closed_curve holds for n be Nat st n is_sufficiently_large_for C holds C c= ( LeftComp ( Span (C,n)))

    proof

      let C be Simple_closed_curve;

      let n be Nat;

      assume

       A1: n is_sufficiently_large_for C;

      let c be object;

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

      assume

       A2: c in C;

      C misses ( L~ f) by A1, Th8;

      then

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

      C misses ( RightComp f) by A1, Th10;

      then not c in ( RightComp f) by A2, XBOOLE_0: 3;

      hence thesis by A2, A3, GOBRD14: 18;

    end;

    theorem :: JORDAN14:12

    

     Th12: for C be Simple_closed_curve holds for n be Nat st n is_sufficiently_large_for C holds C c= ( UBD ( L~ ( Span (C,n))))

    proof

      let C be Simple_closed_curve;

      let n be Nat;

      assume n is_sufficiently_large_for C;

      then

       A1: C c= ( LeftComp ( Span (C,n))) by Th11;

      ( LeftComp ( Span (C,n))) c= ( UBD ( L~ ( Span (C,n)))) by GOBRD14: 34, JORDAN2C: 23;

      hence thesis by A1;

    end;

    theorem :: JORDAN14:13

    

     Th13: for C be Simple_closed_curve holds for n be Nat st n is_sufficiently_large_for C holds ( BDD ( L~ ( Span (C,n)))) c= ( BDD C)

    proof

      let C be Simple_closed_curve;

      let n be Nat;

      assume that

       A1: n is_sufficiently_large_for C and

       A2: not ( BDD ( L~ ( Span (C,n)))) c= ( BDD C);

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

      

       A3: ( Cl ( BDD ( L~ f))) = ( Cl ( RightComp f)) by GOBRD14: 37

      .= (( RightComp f) \/ ( L~ f)) by GOBRD14: 21;

      ( len f) >= 1 by GOBOARD7: 34, XXREAL_0: 2;

      then

       A4: 1 in ( dom f) by FINSEQ_3: 25;

      ( len f) > 4 by GOBOARD7: 34;

      then (f /. 1) in ( L~ f) by A4, GOBOARD1: 1, XXREAL_0: 2;

      then ( SpanStart (C,n)) in ( L~ f) by A1, JORDAN13:def 1;

      then

       A5: ( SpanStart (C,n)) in ( Cl ( BDD ( L~ f))) by A3, XBOOLE_0:def 3;

      ( SpanStart (C,n)) in ( BDD C) by A1, Th6;

      then

       A6: ( BDD ( L~ f)) meets ( BDD C) by A5, PRE_TOPC:def 7;

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

      then

       A7: (( BDD C),( UBD C)) are_separated by TSEP_1: 37;

      ( BDD ( L~ f)) misses ( UBD ( L~ f)) by JORDAN2C: 24;

      then C misses ( BDD ( L~ f)) by A1, Th12, XBOOLE_1: 63;

      then

       A8: ( BDD ( L~ f)) c= (C ` ) by SUBSET_1: 23;

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

      then ( BDD ( L~ f)) c= ( UBD C) by A2, A8, A7, CONNSP_1: 16;

      then ( BDD C) meets ( UBD C) by A6, XBOOLE_1: 63;

      hence contradiction by JORDAN2C: 24;

    end;

    theorem :: JORDAN14:14

    

     Th14: for C be Simple_closed_curve holds for n be Nat st n is_sufficiently_large_for C holds ( UBD C) c= ( UBD ( L~ ( Span (C,n))))

    proof

      let C be Simple_closed_curve;

      let n be Nat;

      assume

       A1: n is_sufficiently_large_for C;

      let x be object;

      

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

      assume

       A3: x in ( UBD C);

      then

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

      

       A4: ( Cl ( BDD ( L~ ( Span (C,n))))) c= ( Cl ( BDD C)) by A1, Th13, PRE_TOPC: 19;

       A5:

      now

        assume x in ( L~ ( Span (C,n)));

        then p in (( RightComp ( Span (C,n))) \/ ( L~ ( Span (C,n)))) by XBOOLE_0:def 3;

        then p in ( Cl ( RightComp ( Span (C,n)))) by GOBRD14: 21;

        then p in ( Cl ( BDD ( L~ ( Span (C,n))))) by GOBRD14: 37;

        hence contradiction by A4, A2, A3, PRE_TOPC:def 7;

      end;

      ( BDD ( L~ ( Span (C,n)))) c= ( BDD C) by A1, Th13;

      then not x in ( BDD ( L~ ( Span (C,n)))) by A2, A3, XBOOLE_0: 3;

      then not x in ( RightComp ( Span (C,n))) by GOBRD14: 37;

      then p in ( LeftComp ( Span (C,n))) by A5, GOBRD14: 17;

      hence thesis by GOBRD14: 36;

    end;

    theorem :: JORDAN14:15

    for C be Simple_closed_curve holds for n be Nat st n is_sufficiently_large_for C holds ( RightComp ( Span (C,n))) c= ( BDD C)

    proof

      let C be Simple_closed_curve;

      let n be Nat;

      assume n is_sufficiently_large_for C;

      then ( BDD ( L~ ( Span (C,n)))) c= ( BDD C) by Th13;

      hence thesis by GOBRD14: 37;

    end;

    theorem :: JORDAN14:16

    

     Th16: for C be Simple_closed_curve holds for n be Nat st n is_sufficiently_large_for C holds ( UBD C) c= ( LeftComp ( Span (C,n)))

    proof

      let C be Simple_closed_curve;

      let n be Nat;

      assume n is_sufficiently_large_for C;

      then ( UBD C) c= ( UBD ( L~ ( Span (C,n)))) by Th14;

      hence thesis by GOBRD14: 36;

    end;

    theorem :: JORDAN14:17

    

     Th17: for C be Simple_closed_curve holds for n be Nat st n is_sufficiently_large_for C holds ( UBD C) misses ( BDD ( L~ ( Span (C,n))))

    proof

      let C be Simple_closed_curve;

      let n be Nat;

      assume that

       A1: n is_sufficiently_large_for C and

       A2: ( UBD C) meets ( BDD ( L~ ( Span (C,n))));

      ( UBD ( L~ ( Span (C,n)))) meets ( BDD ( L~ ( Span (C,n)))) by A1, A2, Th14, XBOOLE_1: 63;

      hence contradiction by JORDAN2C: 24;

    end;

    theorem :: JORDAN14:18

    for C be Simple_closed_curve holds for n be Nat st n is_sufficiently_large_for C holds ( UBD C) misses ( RightComp ( Span (C,n)))

    proof

      let C be Simple_closed_curve;

      let n be Nat;

      assume n is_sufficiently_large_for C;

      then ( UBD C) misses ( BDD ( L~ ( Span (C,n)))) by Th17;

      hence thesis by GOBRD14: 37;

    end;

    theorem :: JORDAN14:19

    

     Th19: for C be Simple_closed_curve holds for P be Subset of ( TOP-REAL 2) holds for n be Nat st n is_sufficiently_large_for C holds P is_outside_component_of C implies P misses ( L~ ( Span (C,n)))

    proof

      let C be Simple_closed_curve;

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

      let n be Nat;

      assume that

       A1: n is_sufficiently_large_for C and

       A2: P is_outside_component_of C and

       A3: P meets ( L~ ( Span (C,n)));

      

       A4: ( UBD C) c= ( LeftComp ( Span (C,n))) by A1, Th16;

      consider x be object such that

       A5: x in P and

       A6: x in ( L~ ( Span (C,n))) by A3, XBOOLE_0: 3;

      P c= ( UBD C) by A2, JORDAN2C: 23;

      then x in ( UBD C) by A5;

      hence contradiction by A6, A4, GOBRD14: 17;

    end;

    theorem :: JORDAN14:20

    

     Th20: for C be Simple_closed_curve holds for n be Nat st n is_sufficiently_large_for C holds ( UBD C) misses ( L~ ( Span (C,n)))

    proof

      let C be Simple_closed_curve;

      let n be Nat;

      assume

       A1: n is_sufficiently_large_for C;

      assume ( UBD C) meets ( L~ ( Span (C,n)));

      then

      consider x be object such that

       A2: x in ( UBD C) and

       A3: x in ( L~ ( Span (C,n))) by XBOOLE_0: 3;

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

      then

      consider Z be set such that

       A4: x in Z and

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

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

       A6: Z = B and

       A7: B is_outside_component_of C by A5;

      B misses ( L~ ( Span (C,n))) by A1, A7, Th19;

      hence thesis by A3, A4, A6, XBOOLE_0: 3;

    end;

    theorem :: JORDAN14:21

    

     Th21: for C be Simple_closed_curve holds for n be Nat st n is_sufficiently_large_for C holds ( L~ ( Span (C,n))) c= ( BDD C)

    proof

      let C be Simple_closed_curve;

      let n be Nat;

      assume

       A1: n is_sufficiently_large_for C;

      then C misses ( L~ ( Span (C,n))) by Th8;

      then ( L~ ( Span (C,n))) c= (C ` ) by SUBSET_1: 23;

      then

       A2: ( L~ ( Span (C,n))) c= (( BDD C) \/ ( UBD C)) by JORDAN2C: 27;

      ( UBD C) misses ( L~ ( Span (C,n))) by A1, Th20;

      hence thesis by A2, XBOOLE_1: 73;

    end;

    theorem :: JORDAN14:22

    

     Th22: for C be Simple_closed_curve holds for i,j,k,n be Nat st n is_sufficiently_large_for C & 1 <= k & k <= ( len ( Span (C,n))) & [i, j] in ( Indices ( Gauge (C,n))) & (( Span (C,n)) /. k) = (( Gauge (C,n)) * (i,j)) holds i > 1

    proof

      let C be Simple_closed_curve;

      let i,j,k,n be Nat;

      assume that

       A1: n is_sufficiently_large_for C and

       A2: 1 <= k and

       A3: k <= ( len ( Span (C,n))) and

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

       A5: (( Span (C,n)) /. k) = (( Gauge (C,n)) * (i,j));

      

       A6: ( len ( Span (C,n))) > 4 by GOBOARD7: 34;

      ( SpanStart (C,n)) in ( BDD C) by A1, Th6;

      then

       A7: ( W-bound C) <= ( W-bound ( BDD C)) by JORDAN1C: 6;

      

       A8: j <= ( width ( Gauge (C,n))) by A4, MATRIX_0: 32;

      k in ( dom ( Span (C,n))) by A2, A3, FINSEQ_3: 25;

      then (( Span (C,n)) /. k) in ( L~ ( Span (C,n))) by A6, GOBOARD1: 1, XXREAL_0: 2;

      then

       A9: ( W-bound ( L~ ( Span (C,n)))) <= ((( Gauge (C,n)) * (i,j)) `1 ) by A5, PSCOMP_1: 24;

      

       A10: ( BDD C) c= ( Cl ( BDD C)) by PRE_TOPC: 18;

      

       A11: ( BDD C) is bounded by JORDAN2C: 106;

      then

       A12: ( Cl ( BDD C)) is compact by TOPREAL6: 79;

      ( SpanStart (C,n)) in ( BDD C) by A1, Th6;

      then

       A13: ( W-bound ( BDD C)) = ( W-bound ( Cl ( BDD C))) by A11, TOPREAL6: 85;

      ( L~ ( Span (C,n))) c= ( BDD C) by A1, Th21;

      then ( W-bound ( L~ ( Span (C,n)))) >= ( W-bound ( Cl ( BDD C))) by A12, A10, PSCOMP_1: 69, XBOOLE_1: 1;

      then

       A14: ( W-bound ( BDD C)) <= ((( Gauge (C,n)) * (i,j)) `1 ) by A13, A9, XXREAL_0: 2;

      ( len ( Gauge (C,n))) >= 4 by JORDAN8: 10;

      then

       A15: ( len ( Gauge (C,n))) >= 2 by XXREAL_0: 2;

      

       A16: 1 <= i by A4, MATRIX_0: 32;

      

       A17: 1 <= j by A4, MATRIX_0: 32;

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

      then ((( Gauge (C,n)) * (2,j)) `1 ) = ( W-bound C) by A17, A8, JORDAN8: 11;

      then ((( Gauge (C,n)) * (2,j)) `1 ) <= ((( Gauge (C,n)) * (i,j)) `1 ) by A7, A14, XXREAL_0: 2;

      then i >= (1 + 1) by A16, A17, A8, A15, GOBOARD5: 3;

      hence thesis by NAT_1: 13;

    end;

    theorem :: JORDAN14:23

    

     Th23: for C be Simple_closed_curve holds for i,j,k,n be Nat st n is_sufficiently_large_for C & 1 <= k & k <= ( len ( Span (C,n))) & [i, j] in ( Indices ( Gauge (C,n))) & (( Span (C,n)) /. k) = (( Gauge (C,n)) * (i,j)) holds i < ( len ( Gauge (C,n)))

    proof

      let C be Simple_closed_curve;

      let i,j,k,n be Nat;

      assume that

       A1: n is_sufficiently_large_for C and

       A2: 1 <= k and

       A3: k <= ( len ( Span (C,n))) and

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

       A5: (( Span (C,n)) /. k) = (( Gauge (C,n)) * (i,j));

      

       A6: ( len ( Span (C,n))) > 4 by GOBOARD7: 34;

      ( SpanStart (C,n)) in ( BDD C) by A1, Th6;

      then

       A7: ( E-bound C) >= ( E-bound ( BDD C)) by JORDAN1C: 7;

      

       A8: 1 <= j by A4, MATRIX_0: 32;

      k in ( dom ( Span (C,n))) by A2, A3, FINSEQ_3: 25;

      then (( Span (C,n)) /. k) in ( L~ ( Span (C,n))) by A6, GOBOARD1: 1, XXREAL_0: 2;

      then

       A9: ( E-bound ( L~ ( Span (C,n)))) >= ((( Gauge (C,n)) * (i,j)) `1 ) by A5, PSCOMP_1: 24;

      

       A10: ( BDD C) c= ( Cl ( BDD C)) by PRE_TOPC: 18;

      

       A11: ( BDD C) is bounded by JORDAN2C: 106;

      then

       A12: ( Cl ( BDD C)) is compact by TOPREAL6: 79;

      ( SpanStart (C,n)) in ( BDD C) by A1, Th6;

      then

       A13: ( E-bound ( BDD C)) = ( E-bound ( Cl ( BDD C))) by A11, TOPREAL6: 86;

      ( L~ ( Span (C,n))) c= ( BDD C) by A1, Th21;

      then ( E-bound ( L~ ( Span (C,n)))) <= ( E-bound ( Cl ( BDD C))) by A12, A10, PSCOMP_1: 67, XBOOLE_1: 1;

      then

       A14: ( E-bound ( BDD C)) >= ((( Gauge (C,n)) * (i,j)) `1 ) by A13, A9, XXREAL_0: 2;

      

       A15: ( len ( Gauge (C,n))) >= 4 by JORDAN8: 10;

      then ( len ( Gauge (C,n))) >= (1 + 1) by XXREAL_0: 2;

      then

       A16: (( len ( Gauge (C,n))) - 1) >= 1 by XREAL_1: 19;

      

       A17: (( len ( Gauge (C,n))) -' 1) >= 1 by A16, XREAL_0:def 2;

      

       A18: j <= ( width ( Gauge (C,n))) by A4, MATRIX_0: 32;

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

      then ((( Gauge (C,n)) * ((( len ( Gauge (C,n))) -' 1),j)) `1 ) = ( E-bound C) by A8, A18, JORDAN8: 12;

      then

       A19: ((( Gauge (C,n)) * ((( len ( Gauge (C,n))) -' 1),j)) `1 ) >= ((( Gauge (C,n)) * (i,j)) `1 ) by A7, A14, XXREAL_0: 2;

      i <= ( len ( Gauge (C,n))) by A4, MATRIX_0: 32;

      then i <= (( len ( Gauge (C,n))) -' 1) by A8, A18, A17, A19, GOBOARD5: 3;

      then i < ((( len ( Gauge (C,n))) -' 1) + 1) by NAT_1: 13;

      hence thesis by A15, XREAL_1: 235, XXREAL_0: 2;

    end;

    theorem :: JORDAN14:24

    

     Th24: for C be Simple_closed_curve holds for i,j,k,n be Nat st n is_sufficiently_large_for C & 1 <= k & k <= ( len ( Span (C,n))) & [i, j] in ( Indices ( Gauge (C,n))) & (( Span (C,n)) /. k) = (( Gauge (C,n)) * (i,j)) holds j > 1

    proof

      let C be Simple_closed_curve;

      let i,j,k,n be Nat;

      assume that

       A1: n is_sufficiently_large_for C and

       A2: 1 <= k and

       A3: k <= ( len ( Span (C,n))) and

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

       A5: (( Span (C,n)) /. k) = (( Gauge (C,n)) * (i,j));

      

       A6: ( len ( Span (C,n))) > 4 by GOBOARD7: 34;

      ( SpanStart (C,n)) in ( BDD C) by A1, Th6;

      then

       A7: ( S-bound C) <= ( S-bound ( BDD C)) by JORDAN1C: 8;

      

       A8: i <= ( len ( Gauge (C,n))) by A4, MATRIX_0: 32;

      k in ( dom ( Span (C,n))) by A2, A3, FINSEQ_3: 25;

      then (( Span (C,n)) /. k) in ( L~ ( Span (C,n))) by A6, GOBOARD1: 1, XXREAL_0: 2;

      then

       A9: ( S-bound ( L~ ( Span (C,n)))) <= ((( Gauge (C,n)) * (i,j)) `2 ) by A5, PSCOMP_1: 24;

      

       A10: ( BDD C) c= ( Cl ( BDD C)) by PRE_TOPC: 18;

      

       A11: ( BDD C) is bounded by JORDAN2C: 106;

      then

       A12: ( Cl ( BDD C)) is compact by TOPREAL6: 79;

      ( SpanStart (C,n)) in ( BDD C) by A1, Th6;

      then

       A13: ( S-bound ( BDD C)) = ( S-bound ( Cl ( BDD C))) by A11, TOPREAL6: 88;

      ( L~ ( Span (C,n))) c= ( BDD C) by A1, Th21;

      then ( S-bound ( L~ ( Span (C,n)))) >= ( S-bound ( Cl ( BDD C))) by A12, A10, PSCOMP_1: 68, XBOOLE_1: 1;

      then

       A14: ( S-bound ( BDD C)) <= ((( Gauge (C,n)) * (i,j)) `2 ) by A13, A9, XXREAL_0: 2;

      ( len ( Gauge (C,n))) >= 4 by JORDAN8: 10;

      then

       A15: ( len ( Gauge (C,n))) >= 2 by XXREAL_0: 2;

      

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

      

       A17: 1 <= i by A4, MATRIX_0: 32;

      then ((( Gauge (C,n)) * (i,2)) `2 ) = ( S-bound C) by A8, JORDAN8: 13;

      then

       A18: ((( Gauge (C,n)) * (i,2)) `2 ) <= ((( Gauge (C,n)) * (i,j)) `2 ) by A7, A14, XXREAL_0: 2;

      1 <= j by A4, MATRIX_0: 32;

      then j >= (1 + 1) by A17, A8, A16, A15, A18, GOBOARD5: 4;

      hence thesis by NAT_1: 13;

    end;

    theorem :: JORDAN14:25

    

     Th25: for C be Simple_closed_curve holds for i,j,k,n be Nat st n is_sufficiently_large_for C & 1 <= k & k <= ( len ( Span (C,n))) & [i, j] in ( Indices ( Gauge (C,n))) & (( Span (C,n)) /. k) = (( Gauge (C,n)) * (i,j)) holds j < ( width ( Gauge (C,n)))

    proof

      let C be Simple_closed_curve;

      let i,j,k,n be Nat;

      assume that

       A1: n is_sufficiently_large_for C and

       A2: 1 <= k and

       A3: k <= ( len ( Span (C,n))) and

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

       A5: (( Span (C,n)) /. k) = (( Gauge (C,n)) * (i,j));

      

       A6: ( len ( Span (C,n))) > 4 by GOBOARD7: 34;

      k in ( dom ( Span (C,n))) by A2, A3, FINSEQ_3: 25;

      then (( Span (C,n)) /. k) in ( L~ ( Span (C,n))) by A6, GOBOARD1: 1, XXREAL_0: 2;

      then

       A7: ( N-bound ( L~ ( Span (C,n)))) >= ((( Gauge (C,n)) * (i,j)) `2 ) by A5, PSCOMP_1: 24;

      

       A8: ( BDD C) c= ( Cl ( BDD C)) by PRE_TOPC: 18;

      

       A9: ( BDD C) is bounded by JORDAN2C: 106;

      then

       A10: ( Cl ( BDD C)) is compact by TOPREAL6: 79;

      ( SpanStart (C,n)) in ( BDD C) by A1, Th6;

      then

       A11: ( N-bound ( BDD C)) = ( N-bound ( Cl ( BDD C))) by A9, TOPREAL6: 87;

      ( L~ ( Span (C,n))) c= ( BDD C) by A1, Th21;

      then ( N-bound ( L~ ( Span (C,n)))) <= ( N-bound ( Cl ( BDD C))) by A10, A8, PSCOMP_1: 66, XBOOLE_1: 1;

      then

       A12: ( N-bound ( BDD C)) >= ((( Gauge (C,n)) * (i,j)) `2 ) by A11, A7, XXREAL_0: 2;

      

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

      

       A14: ( len ( Gauge (C,n))) >= 4 by JORDAN8: 10;

      then ( len ( Gauge (C,n))) >= (1 + 1) by XXREAL_0: 2;

      then

       A15: (( len ( Gauge (C,n))) - 1) >= 1 by XREAL_1: 19;

      ( SpanStart (C,n)) in ( BDD C) by A1, Th6;

      then

       A16: ( N-bound C) >= ( N-bound ( BDD C)) by JORDAN1C: 9;

      

       A17: i <= ( len ( Gauge (C,n))) by A4, MATRIX_0: 32;

      

       A18: 1 <= i by A4, MATRIX_0: 32;

      then ((( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))) `2 ) = ( N-bound C) by A17, JORDAN8: 14;

      then

       A19: ((( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))) `2 ) >= ((( Gauge (C,n)) * (i,j)) `2 ) by A16, A12, XXREAL_0: 2;

      

       A20: (( len ( Gauge (C,n))) -' 1) >= 1 by A15, XREAL_0:def 2;

      j <= ( width ( Gauge (C,n))) by A4, MATRIX_0: 32;

      then j <= (( len ( Gauge (C,n))) -' 1) by A18, A17, A20, A19, GOBOARD5: 4;

      then j < ((( len ( Gauge (C,n))) -' 1) + 1) by NAT_1: 13;

      hence thesis by A13, A14, XREAL_1: 235, XXREAL_0: 2;

    end;

    theorem :: JORDAN14:26

    for C be Simple_closed_curve holds for n be Nat st n is_sufficiently_large_for C holds ( Y-SpanStart (C,n)) < ( width ( Gauge (C,n)))

    proof

      let C be Simple_closed_curve;

      let n be Nat;

      

       A1: ( len ( Span (C,n))) > 1 by GOBOARD7: 34, XXREAL_0: 2;

      assume

       A2: n is_sufficiently_large_for C;

      then

       A3: (( Span (C,n)) /. 1) = (( Gauge (C,n)) * (( X-SpanStart (C,n)),( Y-SpanStart (C,n)))) by JORDAN13:def 1;

       [( X-SpanStart (C,n)), ( Y-SpanStart (C,n))] in ( Indices ( Gauge (C,n))) by A2, JORDAN11: 8;

      hence thesis by A2, A1, A3, Th25;

    end;

    theorem :: JORDAN14:27

    

     Th27: for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for n,m be Nat st m >= n & n >= 1 holds ( X-SpanStart (C,m)) = (((2 |^ (m -' n)) * (( X-SpanStart (C,n)) - 2)) + 2)

    proof

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

      let n,m be Nat;

      

       A1: ( X-SpanStart (C,n)) = ((2 |^ (n -' 1)) + 2) by JORDAN1H:def 2;

      assume

       A2: m >= n;

      assume

       A3: n >= 1;

      

      then ((m -' n) + (n -' 1)) = ((m -' n) + (n - 1)) by XREAL_1: 233

      .= (((m -' n) + n) - 1)

      .= (m - 1) by A2, XREAL_1: 235

      .= (m -' 1) by A2, A3, XREAL_1: 233, XXREAL_0: 2;

      then (2 |^ (m -' 1)) = ((2 |^ (m -' n)) * (( X-SpanStart (C,n)) - 2)) by A1, NEWTON: 8;

      hence thesis by JORDAN1H:def 2;

    end;

    theorem :: JORDAN14:28

    

     Th28: for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for n,m be Nat st n <= m & n is_sufficiently_large_for C holds m is_sufficiently_large_for C

    proof

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

      let n,m be Nat;

      assume that

       A1: n <= m and

       A2: n is_sufficiently_large_for C;

      consider j be Nat such that

       A3: j < ( width ( Gauge (C,n))) and

       A4: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),j)) c= ( BDD C) by A2, JORDAN1H:def 3;

      set iin = ( X-SpanStart (C,n));

      set iim = ( X-SpanStart (C,m));

      n >= 1 by A2, JORDAN1H: 51;

      then

       A5: iim = (((2 |^ (m -' n)) * (iin - 2)) + 2) by A1, Th27;

      

       A6: j > 1

      proof

        

         A7: (( X-SpanStart (C,n)) -' 1) <= ( len ( Gauge (C,n))) by JORDAN1H: 50;

        assume

         A8: j <= 1;

        per cases by A8, NAT_1: 25;

          suppose

           A9: j = 0 ;

          ( width ( Gauge (C,n))) >= 0 ;

          then

           A10: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1), 0 )) is non empty by A7, JORDAN1A: 24;

          ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1), 0 )) c= ( UBD C) by A7, JORDAN1A: 49;

          hence contradiction by A4, A9, A10, JORDAN2C: 24, XBOOLE_1: 68;

        end;

          suppose

           A11: j = 1;

          set i1 = ( X-SpanStart (C,n));

          

           A12: (i1 -' 1) <= i1 by NAT_D: 44;

          i1 < ( len ( Gauge (C,n))) by JORDAN1H: 49;

          then

           A13: (i1 -' 1) < ( len ( Gauge (C,n))) by A12, XXREAL_0: 2;

          ( BDD C) c= (C ` ) by JORDAN2C: 25;

          then

           A14: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),1)) c= (C ` ) by A4, A11;

          ( UBD C) is_outside_component_of C by JORDAN2C: 68;

          then

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

          ( width ( Gauge (C,n))) <> 0 by MATRIX_0:def 10;

          then

           A16: ( 0 + 1) <= ( width ( Gauge (C,n))) by NAT_1: 14;

          then

           A17: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),1)) is non empty by A7, JORDAN1A: 24;

          

           A18: 1 <= (i1 -' 1) by JORDAN1H: 50;

           0 < ( width ( Gauge (C,n))) by A16;

          then (( cell (( Gauge (C,n)),(i1 -' 1), 0 )) /\ ( cell (( Gauge (C,n)),(i1 -' 1),( 0 + 1)))) = ( LSeg ((( Gauge (C,n)) * ((i1 -' 1),( 0 + 1))),(( Gauge (C,n)) * (((i1 -' 1) + 1),( 0 + 1))))) by A13, A18, GOBOARD5: 26;

          then

           A19: ( cell (( Gauge (C,n)),(i1 -' 1), 0 )) meets ( cell (( Gauge (C,n)),(i1 -' 1),( 0 + 1))) by XBOOLE_0:def 7;

          ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1), 0 )) c= ( UBD C) by A7, JORDAN1A: 49;

          then ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),1)) c= ( UBD C) by A16, A13, A19, A15, A14, GOBOARD9: 4, JORDAN1A: 25;

          hence contradiction by A4, A11, A17, JORDAN2C: 24, XBOOLE_1: 68;

        end;

      end;

      then (((2 |^ (m -' n)) * (j - 2)) + 2) > 1 by A1, A3, JORDAN1A: 32;

      then

      reconsider j1 = (((2 |^ (m -' n)) * (j - 2)) + 2) as Element of NAT by INT_1: 3;

      iin > 2 by JORDAN1H: 49;

      then

       A20: iin >= (2 + 1) by NAT_1: 13;

      

       A21: (j + 1) < ( width ( Gauge (C,n)))

      proof

        assume (j + 1) >= ( width ( Gauge (C,n)));

        then

         A22: (j + 1) > ( width ( Gauge (C,n))) or (j + 1) = ( width ( Gauge (C,n))) by XXREAL_0: 1;

        

         A23: (( X-SpanStart (C,n)) -' 1) <= ( len ( Gauge (C,n))) by JORDAN1H: 50;

        per cases by A3, A22, NAT_1: 13;

          suppose

           A24: j = ( width ( Gauge (C,n)));

          

           A25: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),( width ( Gauge (C,n))))) c= ( UBD C) by A23, JORDAN1A: 50;

          ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),j)) is non empty by A23, A24, JORDAN1A: 24;

          hence contradiction by A4, A24, A25, JORDAN2C: 24, XBOOLE_1: 68;

        end;

          suppose (j + 1) = ( width ( Gauge (C,n)));

          then

           A26: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),(( width ( Gauge (C,n))) -' 1))) c= ( BDD C) by A4, NAT_D: 34;

          ( BDD C) c= (C ` ) by JORDAN2C: 25;

          then

           A27: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),(( width ( Gauge (C,n))) -' 1))) c= (C ` ) by A26;

          

           A28: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),( width ( Gauge (C,n))))) c= ( UBD C) by A23, JORDAN1A: 50;

          set i1 = ( X-SpanStart (C,n));

          

           A29: (i1 -' 1) <= i1 by NAT_D: 44;

          i1 < ( len ( Gauge (C,n))) by JORDAN1H: 49;

          then

           A30: (i1 -' 1) < ( len ( Gauge (C,n))) by A29, XXREAL_0: 2;

          ( UBD C) is_outside_component_of C by JORDAN2C: 68;

          then

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

          (( width ( Gauge (C,n))) -' 1) <= ( width ( Gauge (C,n))) by NAT_D: 44;

          then

           A32: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),(( width ( Gauge (C,n))) -' 1))) is non empty by A23, JORDAN1A: 24;

          

           A33: (( width ( Gauge (C,n))) - 1) < ( width ( Gauge (C,n))) by XREAL_1: 146;

          

           A34: 1 <= (i1 -' 1) by JORDAN1H: 50;

          

           A35: ( width ( Gauge (C,n))) <> 0 by MATRIX_0:def 10;

          then ((( width ( Gauge (C,n))) -' 1) + 1) = ( width ( Gauge (C,n))) by NAT_1: 14, XREAL_1: 235;

          then (( cell (( Gauge (C,n)),(i1 -' 1),( width ( Gauge (C,n))))) /\ ( cell (( Gauge (C,n)),(i1 -' 1),(( width ( Gauge (C,n))) -' 1)))) = ( LSeg ((( Gauge (C,n)) * ((i1 -' 1),( width ( Gauge (C,n))))),(( Gauge (C,n)) * (((i1 -' 1) + 1),( width ( Gauge (C,n))))))) by A30, A33, A34, GOBOARD5: 26;

          then

           A36: ( cell (( Gauge (C,n)),(i1 -' 1),( width ( Gauge (C,n))))) meets ( cell (( Gauge (C,n)),(i1 -' 1),(( width ( Gauge (C,n))) -' 1))) by XBOOLE_0:def 7;

          (( width ( Gauge (C,n))) -' 1) < ( width ( Gauge (C,n))) by A35, A33, NAT_1: 14, XREAL_1: 233;

          then ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),(( width ( Gauge (C,n))) -' 1))) c= ( UBD C) by A28, A30, A36, A31, A27, GOBOARD9: 4, JORDAN1A: 25;

          hence contradiction by A26, A32, JORDAN2C: 24, XBOOLE_1: 68;

        end;

      end;

      iin < ( len ( Gauge (C,n))) by JORDAN1H: 49;

      then ( cell (( Gauge (C,m)),(iim -' 1),j1)) c= ( cell (( Gauge (C,n)),(iin -' 1),j)) by A1, A5, A20, A6, A21, JORDAN1A: 48;

      then

       A37: ( cell (( Gauge (C,m)),(( X-SpanStart (C,m)) -' 1),j1)) c= ( BDD C) by A4;

      j1 < ( width ( Gauge (C,m))) by A1, A3, A6, JORDAN1A: 32;

      hence thesis by A37, JORDAN1H:def 3;

    end;

    theorem :: JORDAN14:29

    

     Th29: for G be Go-board holds for f be FinSequence of ( TOP-REAL 2) holds for i,j be Nat holds f is_sequence_on G & f is special & i <= ( len G) & j <= ( width G) implies (( cell (G,i,j)) \ ( L~ f)) is connected

    proof

      let G be Go-board;

      let f be FinSequence of ( TOP-REAL 2);

      let i,j be Nat;

      assume that

       A1: f is_sequence_on G and

       A2: f is special and

       A3: i <= ( len G) and

       A4: j <= ( width G);

      ( Int ( cell (G,i,j))) misses ( L~ f) by A1, A2, A3, A4, JORDAN9: 14;

      then

       A5: ( Int ( cell (G,i,j))) c= (( L~ f) ` ) by SUBSET_1: 23;

      (( cell (G,i,j)) \ ( L~ f)) c= ( cell (G,i,j)) by XBOOLE_1: 36;

      then

       A6: (( cell (G,i,j)) \ ( L~ f)) c= ( Cl ( Int ( cell (G,i,j)))) by A3, A4, GOBRD11: 35;

      

       A7: ( Int ( cell (G,i,j))) c= ( cell (G,i,j)) by TOPS_1: 16;

      

       A8: ( Int ( cell (G,i,j))) is convex by A3, A4, GOBOARD9: 17;

      (( cell (G,i,j)) \ ( L~ f)) = (( cell (G,i,j)) /\ (( L~ f) ` )) by SUBSET_1: 13;

      then ( Int ( cell (G,i,j))) c= (( cell (G,i,j)) \ ( L~ f)) by A5, A7, XBOOLE_1: 19;

      hence thesis by A6, A8, CONNSP_1: 18;

    end;

    theorem :: JORDAN14:30

    

     Th30: for C be Simple_closed_curve holds for n,k be Nat st n is_sufficiently_large_for C & ( Y-SpanStart (C,n)) <= k & k <= (((2 |^ (n -' ( ApproxIndex C))) * (( Y-InitStart C) -' 2)) + 2) holds (( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),k)) \ ( L~ ( Span (C,n)))) c= ( BDD ( L~ ( Span (C,n))))

    proof

      let C be Simple_closed_curve;

      let n,k be Nat;

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

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

      set AI = ( ApproxIndex C);

      set YI = ( Y-InitStart C);

      set XS = ( X-SpanStart (C,n));

      set YS = ( Y-SpanStart (C,n));

      assume that

       A1: n is_sufficiently_large_for C and

       A2: YS <= k and

       A3: k <= (((2 |^ (n -' AI)) * (YI -' 2)) + 2);

      

       A4: f is_sequence_on G by A1, JORDAN13:def 1;

      reconsider ro = (k - YS) as Element of NAT by A2, INT_1: 5;

      

       A5: ro <= ((((2 |^ (n -' AI)) * (YI -' 2)) + 2) - YS) by A3, XREAL_1: 9;

      

       A6: k = (YS + ro);

      defpred P[ Nat] means $1 <= ((((2 |^ (n -' AI)) * (YI -' 2)) + 2) - YS) implies (( cell (G,(XS -' 1),(YS + $1))) \ ( L~ f)) c= ( BDD ( L~ f));

      

       A7: 1 <= (XS -' 1) by JORDAN1H: 50;

      XS > 2 by JORDAN1H: 49;

      then

       A8: ((XS -' 1) + 1) = XS by XREAL_1: 235, XXREAL_0: 2;

      

       A9: (XS -' 1) < ( len G) by JORDAN1H: 50;

      

       A10: for t be Nat st P[t] holds P[(t + 1)]

      proof

        let t be Nat;

        assume

         A11: t <= ((((2 |^ (n -' AI)) * (YI -' 2)) + 2) - YS) implies (( cell (G,(XS -' 1),(YS + t))) \ ( L~ f)) c= ( BDD ( L~ f));

        set Ls = ( LSeg ((G * ((XS -' 1),(YS + (t + 1)))),(G * (XS,(YS + (t + 1))))));

        

         A12: t < (t + 1) by NAT_1: 13;

        set p = ((1 / 2) * ((G * ((XS -' 1),(YS + (t + 1)))) + (G * (XS,(YS + (t + 1))))));

        

         A13: (( cell (G,(XS -' 1),(YS + (t + 1)))) \ ( L~ f)) c= (( L~ f) ` )

        proof

          let y be object;

          assume

           A14: y in (( cell (G,(XS -' 1),(YS + (t + 1)))) \ ( L~ f));

          then not y in ( L~ f) by XBOOLE_0:def 5;

          hence thesis by A14, SUBSET_1: 29;

        end;

        

         A15: p in Ls by RLTOPSP1: 69;

        

         A16: ((YS + t) + 1) = (YS + (t + 1));

        then

         A17: 1 <= (YS + (t + 1)) by NAT_1: 11;

        

         A18: YI > 1 by JORDAN11: 2;

        then YI >= ((1 + 1) + 0 ) by NAT_1: 13;

        then (YI - 2) >= 0 by XREAL_1: 19;

        then

         A19: (YI -' 2) = (YI - 2) by XREAL_0:def 2;

        assume

         A20: (t + 1) <= ((((2 |^ (n -' AI)) * (YI -' 2)) + 2) - YS);

        then

         A21: ((t + 1) + YS) <= (((2 |^ (n -' AI)) * (YI -' 2)) + 2) by XREAL_1: 19;

        assume not (( cell (G,(XS -' 1),(YS + (t + 1)))) \ ( L~ f)) c= ( BDD ( L~ f));

        then

        consider x be object such that

         A22: x in (( cell (G,(XS -' 1),(YS + (t + 1)))) \ ( L~ f)) and

         A23: not x in ( BDD ( L~ f));

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

        then x in (( L~ f) ` ) by A22, SUBSET_1: 29;

        then x in (( BDD ( L~ f)) \/ ( UBD ( L~ f))) by JORDAN2C: 27;

        then x in ( UBD ( L~ f)) by A23, XBOOLE_0:def 3;

        then

         A24: (( cell (G,(XS -' 1),(YS + (t + 1)))) \ ( L~ f)) meets ( UBD ( L~ f)) by A22, XBOOLE_0: 3;

        

         A25: YI < ( width ( Gauge (C,AI))) by JORDAN11:def 2;

        AI <= n by A1, JORDAN11:def 1;

        then (((2 |^ (n -' AI)) * (YI - 2)) + 2) < ( width ( Gauge (C,n))) by A18, A25, JORDAN1A: 32;

        then

         A26: ((YS + t) + 1) <= ( width G) by A19, A21, XXREAL_0: 2;

        

         A27: ((YS + t) + 1) <= (((2 |^ (n -' AI)) * (YI -' 2)) + 2) by A21;

         A28:

        now

          

           A29: YS <= (YS + (t + 1)) by NAT_1: 11;

          

           A30: XS < ( len G) by JORDAN1H: 49;

          assume p in ( L~ f);

          then

          consider i be Nat such that

           A31: 1 <= i and

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

           A33: p in ( LSeg (f,i)) by SPPOL_2: 13;

          

           A34: ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A31, A32, TOPREAL1:def 3;

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

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

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

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

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

           A39: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A4, A31, A32, JORDAN8: 3;

          

           A40: 1 <= i1 by A35, MATRIX_0: 32;

          

           A41: i2 <= ( len G) by A37, MATRIX_0: 32;

          

           A42: 1 <= i2 by A37, MATRIX_0: 32;

          

           A43: j1 <= ( width G) by A35, MATRIX_0: 32;

          

           A44: 1 <= j2 by A37, MATRIX_0: 32;

          

           A45: i1 <= ( len G) by A35, MATRIX_0: 32;

          

           A46: j2 <= ( width G) by A37, MATRIX_0: 32;

          

           A47: 1 <= j1 by A35, MATRIX_0: 32;

          per cases by A39;

            suppose i1 = i2 & (j1 + 1) = j2;

            hence contradiction by A7, A8, A26, A17, A33, A34, A36, A38, A40, A45, A47, A46, A30, GOBOARD7: 27;

          end;

            suppose

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

            then

             A49: (YS + (t + 1)) = j1 by A7, A8, A26, A17, A33, A34, A36, A38, A40, A47, A43, A41, A30, GOBOARD7: 26;

            

             A50: ( cell (G,(XS -' 1),(YS + (t + 1)))) c= ( BDD C) by A1, A21, A29, JORDAN11:def 3;

            

             A51: ( left_cell (f,i,G)) = ( cell (G,i1,j1)) by A4, A31, A32, A35, A36, A37, A38, A48, GOBRD13: 23;

            (XS -' 1) = i1 by A7, A8, A26, A17, A33, A34, A36, A38, A40, A47, A43, A41, A30, A48, GOBOARD7: 26;

            then ( cell (G,(XS -' 1),(YS + (t + 1)))) meets C by A1, A31, A32, A49, A51, Th7;

            hence contradiction by A50, JORDAN1A: 7, XBOOLE_1: 63;

          end;

            suppose

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

            then

             A53: ( left_cell (f,i,G)) = ( cell (G,i2,(j2 -' 1))) by A4, A31, A32, A35, A36, A37, A38, GOBRD13: 25;

            

             A54: (YS + (t + 1)) = j2 by A7, A8, A26, A17, A33, A34, A36, A38, A45, A47, A43, A42, A30, A52, GOBOARD7: 26;

            (XS -' 1) = i2 by A7, A8, A26, A17, A33, A34, A36, A38, A45, A47, A43, A42, A30, A52, GOBOARD7: 26;

            then ( cell (G,(XS -' 1),((YS + (t + 1)) -' 1))) meets C by A1, A31, A32, A54, A53, Th7;

            then

             A55: ( cell (G,(XS -' 1),(YS + t))) meets C by A16, NAT_D: 34;

            

             A56: YS <= (YS + t) by NAT_1: 11;

            (YS + t) <= (((2 |^ (n -' AI)) * (YI -' 2)) + 2) by A27, NAT_1: 13;

            then ( cell (G,(XS -' 1),(YS + t))) c= ( BDD C) by A1, A56, JORDAN11:def 3;

            hence contradiction by A55, JORDAN1A: 7, XBOOLE_1: 63;

          end;

            suppose i1 = i2 & j1 = (j2 + 1);

            hence contradiction by A7, A8, A26, A17, A33, A34, A36, A38, A40, A45, A43, A44, A30, GOBOARD7: 27;

          end;

        end;

        (YS + t) < ( width G) by A26, NAT_1: 13;

        then Ls c= ( cell (G,(XS -' 1),(YS + t))) by A7, A9, A8, A16, GOBOARD5: 21;

        then

         A57: p in (( cell (G,(XS -' 1),(YS + t))) \ ( L~ f)) by A28, A15, XBOOLE_0:def 5;

        Ls c= ( cell (G,(XS -' 1),(YS + (t + 1)))) by A7, A9, A8, A26, A17, GOBOARD5: 22;

        then

         A58: p in (( cell (G,(XS -' 1),(YS + (t + 1)))) \ ( L~ f)) by A28, A15, XBOOLE_0:def 5;

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

        then ( UBD ( L~ f)) is_a_component_of (( L~ f) ` ) by GOBRD14: 36;

        then (( cell (G,(XS -' 1),(YS + (t + 1)))) \ ( L~ f)) c= ( UBD ( L~ f)) by A4, A9, A26, A24, A13, Th29, GOBOARD9: 4;

        then ( BDD ( L~ f)) meets ( UBD ( L~ f)) by A11, A20, A12, A57, A58, XBOOLE_0: 3, XXREAL_0: 2;

        hence contradiction by JORDAN2C: 24;

      end;

      

       A59: P[ 0 ]

      proof

        assume 0 <= ((((2 |^ (n -' AI)) * (YI -' 2)) + 2) - YS);

        

         A60: (f /. (1 + 1)) = (G * ((XS -' 1),YS)) by A1, JORDAN13:def 1;

        

         A61: [XS, YS] in ( Indices ( Gauge (C,n))) by A1, JORDAN11: 8;

        

         A62: [(XS -' 1), YS] in ( Indices ( Gauge (C,n))) by A1, JORDAN11: 9;

        

         A63: ( len f) >= (1 + 1) by GOBOARD7: 34, XXREAL_0: 2;

        then

         A64: (( right_cell (f,1,G)) \ ( L~ f)) c= ( RightComp f) by A4, JORDAN9: 27;

        (f /. 1) = (G * (XS,YS)) by A1, JORDAN13:def 1;

        then ( right_cell (f,1,G)) = ( cell (G,(XS -' 1),YS)) by A4, A8, A63, A60, A61, A62, GOBRD13: 26;

        hence thesis by A64, GOBRD14: 37;

      end;

      for t be Nat holds P[t] from NAT_1:sch 2( A59, A10);

      hence thesis by A6, A5;

    end;

    theorem :: JORDAN14:31

    

     Th31: for C be Subset of ( TOP-REAL 2) holds for n,m,i be Nat st m <= n & 1 < i & (i + 1) < ( len ( Gauge (C,m))) holds ((((2 |^ (n -' m)) * (i - 2)) + 2) + 1) < ( len ( Gauge (C,n)))

    proof

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

      let n,m,i be Nat;

      assume that

       A1: m <= n and

       A2: 1 < i and

       A3: (i + 1) < ( len ( Gauge (C,m)));

      (1 + 1) <= i by A2, NAT_1: 13;

      then

      reconsider i2 = (i - 2) as Element of NAT by INT_1: 5;

      

       A4: (2 |^ (n -' m)) > 0 by NEWTON: 83;

      ( len ( Gauge (C,m))) = ((2 |^ m) + (2 + 1)) by JORDAN8:def 1

      .= (((2 |^ m) + 2) + 1);

      then i < ((2 |^ m) + 2) by A3, XREAL_1: 7;

      then i2 < (2 |^ m) by XREAL_1: 19;

      then ((2 |^ (n -' m)) * i2) < ((2 |^ (n -' m)) * (2 |^ m)) by A4, XREAL_1: 68;

      then ((2 |^ (n -' m)) * i2) < (2 |^ ((n -' m) + m)) by NEWTON: 8;

      then ((2 |^ (n -' m)) * i2) < (2 |^ n) by A1, XREAL_1: 235;

      then (((2 |^ (n -' m)) * i2) + 2) < ((2 |^ n) + 2) by XREAL_1: 8;

      then ((((2 |^ (n -' m)) * (i - 2)) + 2) + 1) < (((2 |^ n) + 2) + 1) by XREAL_1: 8;

      then ((((2 |^ (n -' m)) * (i - 2)) + 2) + 1) < ((2 |^ n) + (1 + 2));

      hence thesis by JORDAN8:def 1;

    end;

    theorem :: JORDAN14:32

    

     Th32: for C be Simple_closed_curve holds for n,m be Nat st n is_sufficiently_large_for C & n <= m holds ( RightComp ( Span (C,n))) meets ( RightComp ( Span (C,m)))

    proof

      let C be Simple_closed_curve;

      let n,m be Nat;

      assume that

       A1: n is_sufficiently_large_for C and

       A2: n <= m;

      set i1 = ( X-SpanStart (C,m));

      set G1 = ( Gauge (C,m));

      set YI = ( Y-InitStart C);

      set AI = ( ApproxIndex C);

      

       A3: m is_sufficiently_large_for C by A1, A2, Th28;

      then

       A4: AI <= m by JORDAN11:def 1;

      set i = ( X-SpanStart (C,n));

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

      

       A5: 1 <= (i1 -' 1) by JORDAN1H: 50;

      set j1 = ( Y-SpanStart (C,m));

      set f1 = ( Span (C,m));

      j1 <= (((2 |^ (m -' AI)) * (YI -' 2)) + 2) by A3, JORDAN11: 5;

      then

       A6: (( cell (G1,(i1 -' 1),(((2 |^ (m -' AI)) * (YI -' 2)) + 2))) \ ( L~ f1)) c= ( BDD ( L~ f1)) by A1, A2, Th28, Th30;

      

       A7: i < ( len G) by JORDAN1H: 49;

      then (i + 1) <= ( len G) by NAT_1: 13;

      then

       A8: i <= (( len G) - 1) by XREAL_1: 19;

      set XSAI = ( X-SpanStart (C,AI));

      set p2 = (( Gauge (C,AI)) * (XSAI,YI));

      

       A9: 1 < XSAI by JORDAN1H: 49, XXREAL_0: 2;

      

       A10: (YI + 1) < ( width ( Gauge (C,AI))) by JORDAN11: 3;

      then

       A11: YI < ( width ( Gauge (C,AI))) by NAT_1: 13;

      set j4 = (((2 |^ (n -' AI)) * (YI -' 2)) + 2);

      

       A12: i1 < ( len G1) by JORDAN1H: 49;

      set j = ( Y-SpanStart (C,n));

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

      j <= (((2 |^ (n -' AI)) * (YI -' 2)) + 2) by A1, JORDAN11: 5;

      then

       A13: (( cell (G,(i -' 1),(((2 |^ (n -' AI)) * (YI -' 2)) + 2))) \ ( L~ f)) c= ( BDD ( L~ f)) by A1, Th30;

      

       A14: ( Int ( cell (G,(i -' 1),j4))) c= ( cell (G,(i -' 1),j4)) by TOPS_1: 16;

      

       A15: 2 < i by JORDAN1H: 49;

      then

       A16: ((i -' 1) + 1) = i by XREAL_1: 235, XXREAL_0: 2;

      then

       A17: (i -' 1) >= (1 + 1) by A15, NAT_1: 13;

      set j3 = (((2 |^ (m -' AI)) * (YI -' 2)) + 2);

      

       A18: i < ( len G) by JORDAN1H: 49;

      

       A19: YI > 1 by JORDAN11: 2;

      then YI >= ((1 + 1) + 0 ) by NAT_1: 13;

      then

       A20: (YI - 2) >= 0 by XREAL_1: 19;

      then

       A21: (((2 |^ (n -' AI)) * (YI -' 2)) + 2) = (((2 |^ (n -' AI)) * (YI - 2)) + 2) by XREAL_0:def 2;

      

       A22: (((2 |^ (m -' AI)) * (YI -' 2)) + 2) = (((2 |^ (m -' AI)) * (YI - 2)) + 2) by A20, XREAL_0:def 2;

      then

       A23: 1 < (((2 |^ (m -' AI)) * (YI -' 2)) + 2) by A4, A11, A19, JORDAN1A: 32;

      set p3 = ((1 / 2) * ((G1 * ((i1 -' 1),j3)) + (G1 * (i1,(j3 + 1)))));

      

       A24: (i1 -' 1) < ( len G1) by JORDAN1H: 50;

      

       A25: (((2 |^ (m -' AI)) * (YI -' 2)) + 2) < ( width G1) by A4, A11, A19, A22, JORDAN1A: 32;

      then

       A26: (j3 + 1) <= ( width G1) by NAT_1: 13;

      2 < i1 by JORDAN1H: 49;

      then

       A27: ((i1 -' 1) + 1) = i1 by XREAL_1: 235, XXREAL_0: 2;

      then

       A28: p3 in ( Int ( cell (G1,(i1 -' 1),j3))) by A12, A23, A5, A26, GOBOARD6: 31;

      then

       A29: ((G1 * ((i1 -' 1),j3)) `2 ) < (p3 `2 ) by A12, A23, A27, A5, A26, Th4;

      

       A30: (p3 `2 ) < ((G1 * ((i1 -' 1),(j3 + 1))) `2 ) by A12, A23, A27, A5, A26, A28, Th4;

      

       A31: ((G1 * ((i1 -' 1),j3)) `1 ) < (p3 `1 ) by A12, A23, A27, A5, A26, A28, Th4;

      

       A32: 1 < i1 by JORDAN1H: 49, XXREAL_0: 2;

      

      then

       A33: ((G1 * (i1,j3)) `2 ) = ((G1 * (1,j3)) `2 ) by A12, A23, A25, GOBOARD5: 1

      .= ((G1 * ((i1 -' 1),j3)) `2 ) by A23, A25, A5, A24, GOBOARD5: 1;

      

       A34: (j3 + 1) >= 1 by NAT_1: 11;

      

      then

       A35: ((G1 * (i1,(j3 + 1))) `2 ) = ((G1 * (1,(j3 + 1))) `2 ) by A12, A32, A26, GOBOARD5: 1

      .= ((G1 * ((i1 -' 1),(j3 + 1))) `2 ) by A5, A24, A26, A34, GOBOARD5: 1;

      

       A36: 1 <= (i -' 1) by JORDAN1H: 50;

      

       A37: AI <= n by A1, JORDAN11:def 1;

      then

       A38: 1 < (((2 |^ (n -' AI)) * (YI -' 2)) + 2) by A11, A19, A21, JORDAN1A: 32;

      (YI + 1) < ( len ( Gauge (C,AI))) by A10, JORDAN8:def 1;

      then ((((2 |^ (n -' AI)) * (YI -' 2)) + 2) + 1) < ( len G) by A37, A21, Th31, JORDAN11: 2;

      then (((((2 |^ (n -' AI)) * (YI -' 2)) + 2) + 1) + 1) <= ( len G) by NAT_1: 13;

      then

       A39: (j4 + 1) <= (( len G) - 1) by XREAL_1: 19;

      

       A40: (i -' 1) < ( len G) by JORDAN1H: 50;

      then ((i -' 1) + 1) <= ( len G) by NAT_1: 13;

      then

       A41: (i -' 1) <= (( len G) - 1) by XREAL_1: 19;

      

       A42: (((2 |^ (n -' AI)) * (YI -' 2)) + 2) < ( width G) by A37, A11, A19, A21, JORDAN1A: 32;

      then

       A43: (j4 + 1) <= ( width G) by NAT_1: 13;

      j4 < ( len G) by A42, JORDAN8:def 1;

      then (j4 + 1) <= ( len G) by NAT_1: 13;

      then

       A44: j4 <= (( len G) - 1) by XREAL_1: 19;

      

       A45: XSAI < ( len ( Gauge (C,AI))) by JORDAN1H: 49;

      i1 = (((2 |^ (m -' AI)) * (XSAI - 2)) + 2) by A1, A2, Th28, JORDAN11: 4;

      then

       A46: p2 = (G1 * (i1,(((2 |^ (m -' AI)) * (YI -' 2)) + 2))) by A4, A9, A45, A11, A19, A22, JORDAN1A: 33;

      

       A47: i = (((2 |^ (n -' AI)) * (XSAI - 2)) + 2) by A1, JORDAN11: 4;

      then

       A48: p2 = (G * (i,(((2 |^ (n -' AI)) * (YI -' 2)) + 2))) by A37, A9, A45, A11, A19, A21, JORDAN1A: 33;

      

       A49: 1 < i by JORDAN1H: 49, XXREAL_0: 2;

      

      then ((G * (i,j4)) `2 ) = ((G * (1,j4)) `2 ) by A18, A38, A42, GOBOARD5: 1

      .= ((G * ((i -' 1),j4)) `2 ) by A38, A42, A36, A40, GOBOARD5: 1;

      then

       A50: ((G * ((i -' 1),j4)) `2 ) < (p3 `2 ) by A47, A37, A9, A45, A11, A19, A21, A46, A29, A33, JORDAN1A: 33;

      (p3 `1 ) < ((G1 * (i1,j3)) `1 ) by A12, A23, A27, A5, A26, A28, Th4;

      then

       A51: (p3 `1 ) < ((G * (i,j4)) `1 ) by A47, A37, A9, A45, A11, A19, A21, A46, JORDAN1A: 33;

      j4 >= (1 + 1) by A38, NAT_1: 13;

      then ex c,d be Nat st 2 <= c & c <= (( len G1) - 1) & 2 <= d & d <= (( len G1) - 1) & [c, d] in ( Indices G1) & (G * ((i -' 1),j4)) = (G1 * (c,d)) & c = (2 + ((2 |^ (m -' n)) * ((i -' 1) -' 2))) & d = (2 + ((2 |^ (m -' n)) * (j4 -' 2))) by A2, A17, A41, A44, GOBRD14: 8;

      then (G * ((i -' 1),j4)) in { (G1 * (ii,jj)) where ii,jj be Nat : [ii, jj] in ( Indices G1) };

      then (G * ((i -' 1),j4)) in ( Values G1) by MATRIX_0: 39;

      then ((G * ((i -' 1),j4)) `1 ) <= ((G1 * ((i1 -' 1),j3)) `1 ) by A48, A46, A49, A18, A38, A42, A12, A32, A23, A25, GOBRD13: 14;

      then

       A52: ((G * ((i -' 1),j4)) `1 ) < (p3 `1 ) by A31, XXREAL_0: 2;

      (j4 + 1) > (1 + 1) by A38, XREAL_1: 6;

      then ex c,d be Nat st 2 <= c & c <= (( len G1) - 1) & 2 <= d & d <= (( len G1) - 1) & [c, d] in ( Indices G1) & (G * (i,(j4 + 1))) = (G1 * (c,d)) & c = (2 + ((2 |^ (m -' n)) * (i -' 2))) & d = (2 + ((2 |^ (m -' n)) * ((j4 + 1) -' 2))) by A2, A15, A8, A39, GOBRD14: 8;

      then (G * (i,(j4 + 1))) in { (G1 * (ii,jj)) where ii,jj be Nat : [ii, jj] in ( Indices G1) };

      then (G * (i,(j4 + 1))) in ( Values G1) by MATRIX_0: 39;

      then

       A53: ((G1 * (i1,(j3 + 1))) `2 ) <= ((G * (i,(j4 + 1))) `2 ) by A48, A46, A49, A18, A38, A42, A12, A32, A23, A25, GOBRD13: 15;

      

       A54: (j4 + 1) >= 1 by NAT_1: 11;

      

      then ((G * (i,(j4 + 1))) `2 ) = ((G * (1,(j4 + 1))) `2 ) by A49, A18, A43, GOBOARD5: 1

      .= ((G * ((i -' 1),(j4 + 1))) `2 ) by A36, A40, A43, A54, GOBOARD5: 1;

      then (p3 `2 ) < ((G * ((i -' 1),(j4 + 1))) `2 ) by A30, A35, A53, XXREAL_0: 2;

      then

       A55: p3 in ( Int ( cell (G,(i -' 1),j4))) by A7, A38, A16, A36, A52, A51, A43, A50, Th4;

      f is_sequence_on G by A1, JORDAN13:def 1;

      then ( Int ( cell (G,(i -' 1),j4))) misses ( L~ f) by A42, A40, JORDAN9: 14;

      then not p3 in ( L~ f) by A55, XBOOLE_0: 3;

      then p3 in (( cell (G,(i -' 1),j4)) \ ( L~ f)) by A55, A14, XBOOLE_0:def 5;

      then p3 in ( BDD ( L~ f)) by A13;

      then

       A56: p3 in ( RightComp ( Span (C,n))) by GOBRD14: 37;

      f1 is_sequence_on G1 by A3, JORDAN13:def 1;

      then ( Int ( cell (G1,(i1 -' 1),j3))) misses ( L~ f1) by A25, A24, JORDAN9: 14;

      then

       A57: not p3 in ( L~ f1) by A28, XBOOLE_0: 3;

      ( Int ( cell (G1,(i1 -' 1),j3))) c= ( cell (G1,(i1 -' 1),j3)) by TOPS_1: 16;

      then p3 in (( cell (G1,(i1 -' 1),j3)) \ ( L~ f1)) by A28, A57, XBOOLE_0:def 5;

      then p3 in ( BDD ( L~ f1)) by A6;

      then p3 in ( RightComp ( Span (C,m))) by GOBRD14: 37;

      hence thesis by A56, XBOOLE_0: 3;

    end;

    theorem :: JORDAN14:33

    

     Th33: for G be Go-board holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on G & f is special holds for i,j be Nat st i <= ( len G) & j <= ( width G) holds ( Int ( cell (G,i,j))) c= (( L~ f) ` ) by JORDAN9: 14, SUBSET_1: 23;

    theorem :: JORDAN14:34

    

     Th34: for C be Simple_closed_curve holds for n,m be Nat st n is_sufficiently_large_for C & n <= m holds ( L~ ( Span (C,m))) c= ( Cl ( LeftComp ( Span (C,n))))

    proof

      let C be Simple_closed_curve;

      let i,j be Nat;

      assume that

       A1: i is_sufficiently_large_for C and

       A2: i <= j and

       A3: not ( L~ ( Span (C,j))) c= ( Cl ( LeftComp ( Span (C,i))));

      

       A4: j is_sufficiently_large_for C by A1, A2, Th28;

      then

       A5: ( Span (C,j)) is_sequence_on ( Gauge (C,j)) by JORDAN13:def 1;

      set G = ( Gauge (C,j));

      set f = ( Span (C,j));

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

       A6: p in ( L~ ( Span (C,j))) and

       A7: not p in ( Cl ( LeftComp ( Span (C,i)))) by A3;

      consider i1 be Nat such that

       A8: 1 <= i1 and

       A9: (i1 + 1) <= ( len ( Span (C,j))) and

       A10: p in ( LSeg (( Span (C,j)),i1)) by A6, SPPOL_2: 13;

      

       A11: i1 < ( len ( Span (C,j))) by A9, NAT_1: 13;

      

       A12: ( Span (C,i)) is_sequence_on ( Gauge (C,i)) by A1, JORDAN13:def 1;

      now

        ex i2,j2 be Nat st 1 <= i2 & (i2 + 1) <= ( len ( Gauge (C,i))) & 1 <= j2 & (j2 + 1) <= ( width ( Gauge (C,i))) & ( left_cell (( Span (C,j)),i1,G)) c= ( cell (( Gauge (C,i)),i2,j2))

        proof

          

           A13: 1 <= (i1 + 1) by NAT_1: 11;

          then

           A14: (i1 + 1) in ( dom f) by A9, FINSEQ_3: 25;

          then

          consider i5,j5 be Nat such that

           A15: [i5, j5] in ( Indices ( Gauge (C,j))) and

           A16: (f /. (i1 + 1)) = (( Gauge (C,j)) * (i5,j5)) by A5, GOBOARD1:def 9;

          

           A17: 1 <= i5 by A15, MATRIX_0: 32;

          

           A18: j5 <= ( width ( Gauge (C,j))) by A15, MATRIX_0: 32;

          

           A19: i5 <= ( len ( Gauge (C,j))) by A15, MATRIX_0: 32;

          

           A20: 1 <= j5 by A15, MATRIX_0: 32;

          

           A21: i1 in ( dom f) by A8, A11, FINSEQ_3: 25;

          then

          consider i4,j4 be Nat such that

           A22: [i4, j4] in ( Indices ( Gauge (C,j))) and

           A23: (f /. i1) = (( Gauge (C,j)) * (i4,j4)) by A5, GOBOARD1:def 9;

          

           A24: 1 <= i4 by A22, MATRIX_0: 32;

          ( |.(i4 - i5).| + |.(j4 - j5).|) = 1 by A5, A21, A22, A23, A14, A15, A16, GOBOARD1:def 9;

          then

           A25: |.(i4 - i5).| = 1 & j4 = j5 or |.(j4 - j5).| = 1 & i4 = i5 by SEQM_3: 42;

          

           A26: 1 <= j4 by A22, MATRIX_0: 32;

          ( left_cell (f,i1,G)) = ( left_cell (f,i1,G));

          then

           A27: i4 = i5 & (j4 + 1) = j5 & ( left_cell (f,i1,G)) = ( cell (G,(i4 -' 1),j4)) or (i4 + 1) = i5 & j4 = j5 & ( left_cell (f,i1,G)) = ( cell (G,i4,j4)) or i4 = (i5 + 1) & j4 = j5 & ( left_cell (f,i1,G)) = ( cell (G,i5,(j5 -' 1))) or i4 = i5 & j4 = (j5 + 1) & ( left_cell (f,i1,G)) = ( cell (G,i4,j5)) by A5, A8, A9, A22, A23, A15, A16, GOBRD13:def 3;

          

           A28: j4 <= ( width ( Gauge (C,j))) by A22, MATRIX_0: 32;

          

           A29: i4 <= ( len ( Gauge (C,j))) by A22, MATRIX_0: 32;

          per cases by A25, SEQM_3: 41;

            suppose

             A30: i4 = i5 & (j4 + 1) = j5;

            1 < i4 by A1, A2, A8, A11, A22, A23, Th22, Th28;

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

            then

             A31: 1 <= (i4 -' 1) by JORDAN5B: 2;

            ((i4 -' 1) + 1) = i4 by A24, XREAL_1: 235;

            hence thesis by A2, A29, A26, A18, A27, A30, A31, JORDAN1H: 38;

          end;

            suppose

             A32: (i4 + 1) = i5 & j4 = j5;

            j4 < ( width ( Gauge (C,j))) by A1, A2, A8, A11, A22, A23, Th25, Th28;

            then (j4 + 1) <= ( width ( Gauge (C,j))) by NAT_1: 13;

            hence thesis by A2, A24, A26, A19, A27, A32, JORDAN1H: 38;

          end;

            suppose

             A33: i4 = (i5 + 1) & j4 = j5;

            1 < j5 by A1, A2, A9, A13, A15, A16, Th24, Th28;

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

            then

             A34: 1 <= (j5 -' 1) by JORDAN5B: 2;

            ((j5 -' 1) + 1) = j5 by A20, XREAL_1: 235;

            hence thesis by A2, A29, A17, A18, A27, A33, A34, JORDAN1H: 38;

          end;

            suppose

             A35: i4 = i5 & j4 = (j5 + 1);

            i4 < ( len ( Gauge (C,j))) by A1, A2, A8, A11, A22, A23, Th23, Th28;

            then (i4 + 1) <= ( len ( Gauge (C,j))) by NAT_1: 13;

            hence thesis by A2, A24, A28, A20, A27, A35, JORDAN1H: 38;

          end;

        end;

        then

        consider i2,j2 be Nat such that 1 <= i2 and

         A36: (i2 + 1) <= ( len ( Gauge (C,i))) and 1 <= j2 and

         A37: (j2 + 1) <= ( width ( Gauge (C,i))) and

         A38: ( left_cell (( Span (C,j)),i1,G)) c= ( cell (( Gauge (C,i)),i2,j2));

        

         A39: j2 < ( width ( Gauge (C,i))) by A37, NAT_1: 13;

        

         A40: ( LeftComp ( Span (C,i))) is_a_component_of (( L~ ( Span (C,i))) ` ) by GOBOARD9:def 1;

        

         A41: (( Cl ( RightComp ( Span (C,i)))) \/ ( LeftComp ( Span (C,i)))) = ((( L~ ( Span (C,i))) \/ ( RightComp ( Span (C,i)))) \/ ( LeftComp ( Span (C,i)))) by GOBRD14: 21

        .= the carrier of ( TOP-REAL 2) by GOBRD14: 15;

        assume not ( left_cell (( Span (C,j)),i1,G)) c= ( Cl ( RightComp ( Span (C,i))));

        then not ( cell (( Gauge (C,i)),i2,j2)) c= ( Cl ( RightComp ( Span (C,i)))) by A38;

        then

         A42: ( cell (( Gauge (C,i)),i2,j2)) meets ( LeftComp ( Span (C,i))) by A41, XBOOLE_1: 73;

        

         A43: i2 < ( len ( Gauge (C,i))) by A36, NAT_1: 13;

        then ( cell (( Gauge (C,i)),i2,j2)) = ( Cl ( Int ( cell (( Gauge (C,i)),i2,j2)))) by A39, GOBRD11: 35;

        then

         A44: ( Int ( cell (( Gauge (C,i)),i2,j2))) meets ( LeftComp ( Span (C,i))) by A42, TSEP_1: 36;

        

         A45: ( Int ( left_cell (( Span (C,j)),i1,G))) c= ( Int ( cell (( Gauge (C,i)),i2,j2))) by A38, TOPS_1: 19;

        

         A46: ( Int ( cell (( Gauge (C,i)),i2,j2))) is convex by A43, A39, GOBOARD9: 17;

        ( Int ( cell (( Gauge (C,i)),i2,j2))) c= (( L~ ( Span (C,i))) ` ) by A12, A43, A39, Th33;

        then ( Int ( cell (( Gauge (C,i)),i2,j2))) c= ( LeftComp ( Span (C,i))) by A44, A40, A46, GOBOARD9: 4;

        then ( Int ( left_cell (( Span (C,j)),i1,G))) c= ( LeftComp ( Span (C,i))) by A45;

        then ( Cl ( Int ( left_cell (( Span (C,j)),i1,G)))) c= ( Cl ( LeftComp ( Span (C,i)))) by PRE_TOPC: 19;

        then

         A47: ( left_cell (( Span (C,j)),i1,G)) c= ( Cl ( LeftComp ( Span (C,i)))) by A5, A8, A9, JORDAN9: 11;

        ( LSeg (( Span (C,j)),i1)) c= ( left_cell (( Span (C,j)),i1,G)) by A5, A8, A9, JORDAN1H: 20;

        then ( LSeg (( Span (C,j)),i1)) c= ( Cl ( LeftComp ( Span (C,i)))) by A47;

        hence contradiction by A7, A10;

      end;

      then

       A48: C meets ( Cl ( RightComp ( Span (C,i)))) by A4, A8, A9, Th7, XBOOLE_1: 63;

      

       A49: ( Cl ( RightComp ( Span (C,i)))) = (( RightComp ( Span (C,i))) \/ ( L~ ( Span (C,i)))) by GOBRD14: 21;

      C misses ( L~ ( Span (C,i))) by A1, Th8;

      then

       A50: C meets ( RightComp ( Span (C,i))) by A48, A49, XBOOLE_1: 70;

      C meets C;

      then

       A51: C meets ( LeftComp ( Span (C,i))) by A1, Th11, XBOOLE_1: 63;

      reconsider D = (( L~ ( Span (C,i))) ` ) as Subset of ( TOP-REAL 2);

      D = (( RightComp ( Span (C,i))) \/ ( LeftComp ( Span (C,i)))) by GOBRD12: 10;

      then

       A52: ( LeftComp ( Span (C,i))) c= D by XBOOLE_1: 7;

      C c= ( LeftComp ( Span (C,i))) by A1, Th11;

      then

       A53: C c= D by A52;

      

       A54: ( LeftComp ( Span (C,i))) is_a_component_of D by GOBOARD9:def 1;

      ( RightComp ( Span (C,i))) is_a_component_of D by GOBOARD9:def 2;

      hence contradiction by A50, A53, A54, A51, JORDAN9: 1, SPRECT_4: 6;

    end;

    theorem :: JORDAN14:35

    

     Th35: for C be Simple_closed_curve holds for n,m be Nat st n is_sufficiently_large_for C & n <= m holds ( RightComp ( Span (C,n))) c= ( RightComp ( Span (C,m)))

    proof

      let C be Simple_closed_curve;

      let n,m be Nat;

      assume that

       A1: n is_sufficiently_large_for C and

       A2: n <= m;

      

       A3: ( L~ ( Span (C,n))) misses ( RightComp ( Span (C,n))) by SPRECT_3: 25;

      

       A4: ( RightComp ( Span (C,n))) misses ( LeftComp ( Span (C,n))) by GOBRD14: 14;

      ( Cl ( LeftComp ( Span (C,n)))) = (( LeftComp ( Span (C,n))) \/ ( L~ ( Span (C,n)))) by GOBRD14: 22;

      then ( Cl ( LeftComp ( Span (C,n)))) misses ( RightComp ( Span (C,n))) by A3, A4, XBOOLE_1: 70;

      then ( L~ ( Span (C,m))) misses ( RightComp ( Span (C,n))) by A1, A2, Th34, XBOOLE_1: 63;

      then

       A5: ( RightComp ( Span (C,n))) c= (( L~ ( Span (C,m))) ` ) by SUBSET_1: 23;

      

       A6: ( RightComp ( Span (C,m))) is_a_component_of (( L~ ( Span (C,m))) ` ) by GOBOARD9:def 2;

      ( RightComp ( Span (C,n))) meets ( RightComp ( Span (C,m))) by A1, A2, Th32;

      hence thesis by A6, A5, GOBOARD9: 4;

    end;

    theorem :: JORDAN14:36

    for C be Simple_closed_curve holds for n,m be Nat st n is_sufficiently_large_for C & n <= m holds ( LeftComp ( Span (C,m))) c= ( LeftComp ( Span (C,n)))

    proof

      let C be Simple_closed_curve;

      let n,m be Nat;

      assume that

       A1: n is_sufficiently_large_for C and

       A2: n <= m;

      

       A3: (( Cl ( RightComp ( Span (C,n)))) ` ) = ( LeftComp ( Span (C,n))) by JORDAN1H: 43;

      

       A4: (( Cl ( RightComp ( Span (C,m)))) ` ) = ( LeftComp ( Span (C,m))) by JORDAN1H: 43;

      ( Cl ( RightComp ( Span (C,n)))) c= ( Cl ( RightComp ( Span (C,m)))) by A1, A2, Th35, PRE_TOPC: 19;

      hence thesis by A3, A4, SUBSET_1: 12;

    end;