goboard9.miz



    begin

    reserve f for non constant standard special_circular_sequence,

i,j,k,i1,i2,j1,j2 for Nat,

r,s,r1,s1,r2,s2 for Real,

p,q for Point of ( TOP-REAL 2),

G for Go-board;

    theorem :: GOBOARD9:1

    

     Th1: for GX be TopSpace, A1,A2,B be Subset of GX st A1 is_a_component_of B & A2 is_a_component_of B holds A1 = A2 or A1 misses A2

    proof

      let GX be TopSpace, A1,A2,B be Subset of GX;

      assume A1 is_a_component_of B;

      then

       A1: ex B1 be Subset of (GX | B) st B1 = A1 & B1 is a_component by CONNSP_1:def 6;

      assume A2 is_a_component_of B;

      then ex B2 be Subset of (GX | B) st B2 = A2 & B2 is a_component by CONNSP_1:def 6;

      hence thesis by A1, CONNSP_1: 35;

    end;

    theorem :: GOBOARD9:2

    

     Th2: for GX be TopSpace, A,B be Subset of GX, AA be Subset of (GX | B) st A = AA holds (GX | A) = ((GX | B) | AA)

    proof

      let GX be TopSpace, A,B be Subset of GX;

      let AA be Subset of (GX | B);

      assume

       A1: A = AA;

      the carrier of (GX | A) = ( [#] (GX | A))

      .= A by PRE_TOPC:def 5;

      then

      reconsider GY = (GX | A) as strict SubSpace of (GX | B) by A1, TSEP_1: 4;

      ( [#] GY) = AA by A1, PRE_TOPC:def 5;

      hence thesis by PRE_TOPC:def 5;

    end;

    theorem :: GOBOARD9:3

    

     Th3: for GX be non empty TopSpace, A,B be non empty Subset of GX st A c= B & A is connected holds ex C be Subset of GX st C is_a_component_of B & A c= C

    proof

      let GX be non empty TopSpace, A,B be non empty Subset of GX such that

       A1: A c= B and

       A2: A is connected;

      consider p be object such that

       A3: p in A by XBOOLE_0:def 1;

      

       A4: B = ( [#] (GX | B)) by PRE_TOPC:def 5

      .= the carrier of (GX | B);

      then

      reconsider p as Point of (GX | B) by A1, A3;

      reconsider C = ( Component_of p) as Subset of GX by PRE_TOPC: 11;

      take C;

      

       A5: ( Component_of p) is a_component by CONNSP_1: 40;

      hence C is_a_component_of B by CONNSP_1:def 6;

      reconsider AA = A as Subset of (GX | B) by A1, A4;

      (GX | A) is connected by A2, CONNSP_1:def 3;

      then ((GX | B) | AA) is connected by Th2;

      then

       A6: AA is connected by CONNSP_1:def 3;

      p in ( Component_of p) by CONNSP_1: 38;

      then (AA /\ ( Component_of p)) <> ( {} (GX | B)) by A3, XBOOLE_0:def 4;

      then AA meets ( Component_of p);

      hence thesis by A5, A6, CONNSP_1: 36;

    end;

    theorem :: GOBOARD9:4

    

     Th4: for GX be non empty TopSpace, A,B,C,D be Subset of GX st B is connected & C is_a_component_of D & A c= C & A meets B & B c= D holds B c= C

    proof

      let GX be non empty TopSpace, A,B,C,D be Subset of GX such that

       A1: B is connected and

       A2: C is_a_component_of D and

       A3: A c= C and

       A4: A meets B and

       A5: B c= D;

      

       A6: A <> {} by A4;

      

       A7: B <> {} by A4;

      reconsider A, B as non empty Subset of GX by A4;

      reconsider C, D as non empty Subset of GX by A3, A5, A6, A7, XBOOLE_1: 3;

      consider CC be Subset of GX such that

       A8: CC is_a_component_of D and

       A9: B c= CC by A1, A5, Th3;

      

       A10: A meets CC by A4, A9, XBOOLE_1: 63;

      

       A11: ex C1 be Subset of (GX | D) st C1 = C & C1 is a_component by A2, CONNSP_1:def 6;

      ex CC1 be Subset of (GX | D) st CC1 = CC & CC1 is a_component by A8, CONNSP_1:def 6;

      hence thesis by A3, A9, A10, A11, CONNSP_1: 35, XBOOLE_1: 63;

    end;

    registration

      cluster convex non empty for Subset of ( TOP-REAL 2);

      existence

      proof

        set p = the Point of ( TOP-REAL 2);

        take ( LSeg (p,p));

        thus thesis;

      end;

    end

    ::$Canceled

    theorem :: GOBOARD9:6

    

     Th5: for P,Q be convex Subset of ( TOP-REAL 2) holds (P /\ Q) is convex

    proof

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

      let p, q;

      assume that

       A1: p in (P /\ Q) and

       A2: q in (P /\ Q);

      

       A3: p in P by A1, XBOOLE_0:def 4;

      q in P by A2, XBOOLE_0:def 4;

      then

       A4: ( LSeg (p,q)) c= P by A3, JORDAN1:def 1;

      

       A5: p in Q by A1, XBOOLE_0:def 4;

      q in Q by A2, XBOOLE_0:def 4;

      then ( LSeg (p,q)) c= Q by A5, JORDAN1:def 1;

      hence thesis by A4, XBOOLE_1: 19;

    end;

    theorem :: GOBOARD9:7

    

     Th6: for f be FinSequence of ( TOP-REAL 2) holds ( Rev ( X_axis f)) = ( X_axis ( Rev f))

    proof

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

      

       A1: ( len ( Rev ( X_axis f))) = ( len ( X_axis f)) by FINSEQ_5:def 3

      .= ( len f) by GOBOARD1:def 1

      .= ( len ( Rev f)) by FINSEQ_5:def 3;

      ( len ( X_axis f)) = ( len f) by GOBOARD1:def 1;

      then

       A2: ( dom ( X_axis f)) = ( dom f) by FINSEQ_3: 29;

      

       A3: ( len f) = ( len ( Rev f)) by FINSEQ_5:def 3;

      now

        let k such that

         A4: k in ( dom ( Rev ( X_axis f)));

        set l = ((( len f) + 1) -' k);

        

         A5: k <= ( len f) by A1, A3, A4, FINSEQ_3: 25;

        ( len f) < (( len f) + 1) by NAT_1: 13;

        then

         A6: (l + k) = (( len f) + 1) by A5, XREAL_1: 235, XXREAL_0: 2;

        

         A7: ( Rev ( Rev ( X_axis f))) = ( X_axis f);

        then

         A8: l in ( dom ( X_axis f)) by A1, A3, A4, A6, FINSEQ_5: 59;

        

        thus (( Rev ( X_axis f)) . k) = (( Rev ( X_axis f)) /. k) by A4, PARTFUN1:def 6

        .= (( X_axis f) /. l) by A1, A3, A4, A6, A7, FINSEQ_5: 66

        .= (( X_axis f) . l) by A8, PARTFUN1:def 6

        .= ((f /. l) `1 ) by A8, GOBOARD1:def 1

        .= ((( Rev f) /. k) `1 ) by A1, A2, A3, A4, A6, A7, FINSEQ_5: 59, FINSEQ_5: 66;

      end;

      hence thesis by A1, GOBOARD1:def 1;

    end;

    theorem :: GOBOARD9:8

    

     Th7: for f be FinSequence of ( TOP-REAL 2) holds ( Rev ( Y_axis f)) = ( Y_axis ( Rev f))

    proof

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

      

       A1: ( len ( Rev ( Y_axis f))) = ( len ( Y_axis f)) by FINSEQ_5:def 3

      .= ( len f) by GOBOARD1:def 2

      .= ( len ( Rev f)) by FINSEQ_5:def 3;

      ( len ( Y_axis f)) = ( len f) by GOBOARD1:def 2;

      then

       A2: ( dom ( Y_axis f)) = ( dom f) by FINSEQ_3: 29;

      

       A3: ( len f) = ( len ( Rev f)) by FINSEQ_5:def 3;

      now

        let k such that

         A4: k in ( dom ( Rev ( Y_axis f)));

        set l = ((( len f) + 1) -' k);

        

         A5: k <= ( len f) by A1, A3, A4, FINSEQ_3: 25;

        ( len f) < (( len f) + 1) by NAT_1: 13;

        then

         A6: (l + k) = (( len f) + 1) by A5, XREAL_1: 235, XXREAL_0: 2;

        

         A7: ( Rev ( Rev ( Y_axis f))) = ( Y_axis f);

        then

         A8: l in ( dom ( Y_axis f)) by A1, A3, A4, A6, FINSEQ_5: 59;

        

        thus (( Rev ( Y_axis f)) . k) = (( Rev ( Y_axis f)) /. k) by A4, PARTFUN1:def 6

        .= (( Y_axis f) /. l) by A1, A3, A4, A6, A7, FINSEQ_5: 66

        .= (( Y_axis f) . l) by A8, PARTFUN1:def 6

        .= ((f /. l) `2 ) by A8, GOBOARD1:def 2

        .= ((( Rev f) /. k) `2 ) by A1, A2, A3, A4, A6, A7, FINSEQ_5: 59, FINSEQ_5: 66;

      end;

      hence thesis by A1, GOBOARD1:def 2;

    end;

    

     Lm1: for f,ff be non empty FinSequence of ( TOP-REAL 2) st ff = ( Rev f) holds ( GoB ff) = ( GoB f)

    proof

      let f,ff be non empty FinSequence of ( TOP-REAL 2);

      assume

       A1: ff = ( Rev f);

      then

       A2: ( Rev ( X_axis f)) = ( X_axis ff) by Th6;

      

       A3: ( rng ( Incr ( X_axis ff))) = ( rng ( X_axis ff)) by SEQ_4:def 21

      .= ( rng ( X_axis f)) by A2, FINSEQ_5: 57;

      ( len ( Incr ( X_axis ff))) = ( card ( rng ( X_axis ff))) by SEQ_4:def 21

      .= ( card ( rng ( X_axis f))) by A2, FINSEQ_5: 57;

      then

       A4: ( Incr ( X_axis f)) = ( Incr ( X_axis ff)) by A3, SEQ_4:def 21;

      

       A5: ( Rev ( Y_axis f)) = ( Y_axis ff) by A1, Th7;

      

       A6: ( rng ( Incr ( Y_axis ff))) = ( rng ( Y_axis ff)) by SEQ_4:def 21

      .= ( rng ( Y_axis f)) by A5, FINSEQ_5: 57;

      ( len ( Incr ( Y_axis ff))) = ( card ( rng ( Y_axis ff))) by SEQ_4:def 21

      .= ( card ( rng ( Y_axis f))) by A5, FINSEQ_5: 57;

      then ( Incr ( Y_axis f)) = ( Incr ( Y_axis ff)) by A6, SEQ_4:def 21;

      

      hence ( GoB ff) = ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) by A4, GOBOARD2:def 2

      .= ( GoB f) by GOBOARD2:def 2;

    end;

    registration

      cluster non constant for FinSequence;

      existence

      proof

        take <*1, 2*>, 1, 2;

        

         A1: 1 in {1, 2} by TARSKI:def 2;

        2 in {1, 2} by TARSKI:def 2;

        hence 1 in ( dom <*1, 2*>) & 2 in ( dom <*1, 2*>) by A1, FINSEQ_1: 2, FINSEQ_1: 89;

        ( <*1, 2*> . 1) = 1 by FINSEQ_1: 44;

        hence thesis by FINSEQ_1: 44;

      end;

    end

    registration

      let f be non constant FinSequence;

      cluster ( Rev f) -> non constant;

      coherence

      proof

        consider i, j such that

         A1: i in ( dom f) and

         A2: j in ( dom f) and

         A3: (f . i) <> (f . j) by SEQM_3:def 10;

        

         A4: i <= ( len f) by A1, FINSEQ_3: 25;

        j <= ( len f) by A2, FINSEQ_3: 25;

        then

        reconsider k1 = (( len f) - i), l1 = (( len f) - j) as Element of NAT by A4, INT_1: 5;

        take k = (k1 + 1), l = (l1 + 1);

        (k + i) = (( len f) + 1);

        hence k in ( dom ( Rev f)) by A1, FINSEQ_5: 59;

        

        then

         A5: (( Rev f) . k) = (f . ((( len f) - k) + 1)) by FINSEQ_5:def 3

        .= (f . ( 0 + i));

        (l + j) = (( len f) + 1);

        hence l in ( dom ( Rev f)) by A2, FINSEQ_5: 59;

        

        then (( Rev f) . l) = (f . ((( len f) - l) + 1)) by FINSEQ_5:def 3

        .= (f . ( 0 + j));

        hence thesis by A3, A5;

      end;

    end

    definition

      let f be standard special_circular_sequence;

      :: original: Rev

      redefine

      func Rev f -> standard special_circular_sequence ;

      coherence

      proof

        reconsider ff = ( Rev f) as non empty FinSequence of ( TOP-REAL 2);

        

         A1: ( Rev ff) = f;

        

         A2: ( GoB ff) = ( GoB f) by Lm1;

        

         A3: f is_sequence_on ( GoB f) by GOBOARD5:def 5;

        

         A4: ( len f) = ( len ff) by FINSEQ_5:def 3;

        

         A5: ff is standard

        proof

          hereby

            let k such that

             A6: k in ( dom ff);

            set l = ((( len f) + 1) -' k);

            

             A7: k <= ( len f) by A4, A6, FINSEQ_3: 25;

            ( len f) < (( len f) + 1) by NAT_1: 13;

            then

             A8: (l + k) = (( len f) + 1) by A7, XREAL_1: 235, XXREAL_0: 2;

            then l in ( dom f) by A1, A4, A6, FINSEQ_5: 59;

            then

            consider i, j such that

             A9: [i, j] in ( Indices ( GoB f)) and

             A10: (f /. l) = (( GoB f) * (i,j)) by A3;

            take i, j;

            thus [i, j] in ( Indices ( GoB ff)) by A9, Lm1;

            thus (ff /. k) = (( GoB ff) * (i,j)) by A1, A2, A4, A6, A8, A10, FINSEQ_5: 66;

          end;

          let k such that

           A11: k in ( dom ff) and

           A12: (k + 1) in ( dom ff);

          set l = ((( len f) + 1) -' (k + 1));

          k <= ( len f) by A4, A11, FINSEQ_3: 25;

          then (k + 1) <= (( len f) + 1) by XREAL_1: 6;

          then

           A13: (l + (k + 1)) = (( len f) + 1) by XREAL_1: 235;

          then

           A14: l in ( dom f) by A1, A4, A12, FINSEQ_5: 59;

          

           A15: ((l + 1) + k) = (( len f) + 1) by A13;

          then

           A16: (l + 1) in ( dom f) by A1, A4, A11, FINSEQ_5: 59;

          let i1, j1, i2, j2 such that

           A17: [i1, j1] in ( Indices ( GoB ff)) and

           A18: [i2, j2] in ( Indices ( GoB ff)) and

           A19: (ff /. k) = (( GoB ff) * (i1,j1)) and

           A20: (ff /. (k + 1)) = (( GoB ff) * (i2,j2));

          

           A21: |.(i2 - i1).| = |.( - (i1 - i2)).|

          .= |.(i1 - i2).| by COMPLEX1: 52;

          

           A22: |.(j2 - j1).| = |.( - (j1 - j2)).|

          .= |.(j1 - j2).| by COMPLEX1: 52;

          

           A23: (f /. l) = (( GoB f) * (i2,j2)) by A1, A2, A4, A12, A13, A20, FINSEQ_5: 66;

          (f /. (l + 1)) = (( GoB f) * (i1,j1)) by A1, A2, A4, A11, A15, A19, FINSEQ_5: 66;

          hence ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A2, A3, A14, A16, A17, A18, A21, A22, A23;

        end;

        

         A24: (ff /. 1) = (f /. ( len f)) by FINSEQ_5: 65

        .= (f /. 1) by FINSEQ_6:def 1

        .= (ff /. ( len ff)) by A4, FINSEQ_5: 65;

        ff is s.c.c.

        proof

          let i, j such that

           A25: (i + 1) < j and

           A26: i > 1 & j < ( len ff) or (j + 1) < ( len ff);

          set k = (( len f) -' i), l = (( len f) -' j);

          

           A27: j <= ( len f) by A4, A26, NAT_1: 13;

          then

           A28: (l + j) = ( len f) by XREAL_1: 235;

          i < j by A25, NAT_1: 13;

          then

           A29: (k + i) = ( len f) by A27, XREAL_1: 235, XXREAL_0: 2;

          then ((i + 1) + k) = ((l + 1) + j) by A28;

          then ((l + 1) + j) < (j + k) by A25, XREAL_1: 6;

          then

           A30: (l + 1) < k by XREAL_1: 6;

          

           A31: (j + 1) <= ( len f) by A4, A26, NAT_1: 13;

          per cases by A31, NAT_1: 14, XXREAL_0: 1;

            suppose (j + 1) = ( len f);

            then (k + 1) < ( len f) by A26, A29, FINSEQ_5:def 3, XREAL_1: 6;

            then ( LSeg (f,k)) misses ( LSeg (f,l)) by A30, GOBOARD5:def 4;

            then

             A32: (( LSeg (f,k)) /\ ( LSeg (f,l))) = {} ;

            ( LSeg (f,k)) = ( LSeg (ff,i)) by A29, SPPOL_2: 2;

            hence (( LSeg (ff,i)) /\ ( LSeg (ff,j))) = {} by A28, A32, SPPOL_2: 2;

          end;

            suppose that

             A33: i >= 1 and

             A34: (j + 1) < ( len f);

            

             A35: l > 1 by A28, A34, XREAL_1: 6;

            (k + 1) <= ( len f) by A29, A33, XREAL_1: 6;

            then k < ( len f) by NAT_1: 13;

            then ( LSeg (f,k)) misses ( LSeg (f,l)) by A30, A35, GOBOARD5:def 4;

            then

             A36: (( LSeg (f,k)) /\ ( LSeg (f,l))) = {} ;

            ( LSeg (f,k)) = ( LSeg (ff,i)) by A29, SPPOL_2: 2;

            hence (( LSeg (ff,i)) /\ ( LSeg (ff,j))) = {} by A28, A36, SPPOL_2: 2;

          end;

            suppose i = 0 ;

            then ( LSeg (ff,i)) = {} by TOPREAL1:def 3;

            hence (( LSeg (ff,i)) /\ ( LSeg (ff,j))) = {} ;

          end;

        end;

        hence thesis by A5, A24, FINSEQ_6:def 1, SPPOL_2: 28, SPPOL_2: 40;

      end;

    end

    theorem :: GOBOARD9:9

    

     Th8: i >= 1 & j >= 1 & (i + j) = ( len f) implies ( left_cell (f,i)) = ( right_cell (( Rev f),j))

    proof

      assume that

       A1: i >= 1 and

       A2: j >= 1 and

       A3: (i + j) = ( len f);

      

       A4: (i + 1) <= ( len f) by A2, A3, XREAL_1: 6;

      ( len f) = ( len ( Rev f)) by FINSEQ_5:def 3;

      then

       A5: (j + 1) <= ( len ( Rev f)) by A1, A3, XREAL_1: 6;

      

       A6: ( GoB ( Rev f)) = ( GoB f) by Lm1;

      now

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

         A7: [i1, j1] in ( Indices ( GoB f)) and

         A8: [i2, j2] in ( Indices ( GoB f)) and

         A9: (f /. i) = (( GoB f) * (i1,j1)) and

         A10: (f /. (i + 1)) = (( GoB f) * (i2,j2));

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

        then

         A11: (i + 1) in ( dom f) by A4, FINSEQ_3: 25;

        ((i + 1) + j) = (( len f) + 1) by A3;

        then

         A12: (( Rev f) /. j) = (( GoB f) * (i2,j2)) by A10, A11, FINSEQ_5: 66;

        i <= ( len f) by A4, NAT_1: 13;

        then

         A13: i in ( dom f) by A1, FINSEQ_3: 25;

        ((j + 1) + i) = (( len f) + 1) by A3;

        then

         A14: (( Rev f) /. (j + 1)) = (( GoB f) * (i1,j1)) by A9, A13, FINSEQ_5: 66;

        1 <= i1 by A7, MATRIX_0: 32;

        then

         A15: ((i1 -' 1) + 1) = i1 by XREAL_1: 235;

        1 <= j1 by A7, MATRIX_0: 32;

        then

         A16: ((j1 -' 1) + 1) = j1 by XREAL_1: 235;

        reconsider i19 = i1, i29 = i2, j19 = j1, j29 = j2 as Element of REAL by XREAL_0:def 1;

        f is_sequence_on ( GoB f) by GOBOARD5:def 5;

        then ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A7, A8, A9, A10, A11, A13;

        then

         A17: |.(i19 - i29).| = 1 & j1 = j2 or |.(j19 - j29).| = 1 & i1 = i2 by SEQM_3: 42;

        per cases by A17, SEQM_3: 41;

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

          hence ( right_cell (( Rev f),j)) = ( cell (( GoB f),(i1 -' 1),j1)) by A2, A5, A6, A7, A8, A12, A14, A15, GOBOARD5: 30;

        end;

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

          hence ( right_cell (( Rev f),j)) = ( cell (( GoB f),i1,j1)) by A2, A5, A6, A7, A8, A12, A14, A16, GOBOARD5: 29;

        end;

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

          hence ( right_cell (( Rev f),j)) = ( cell (( GoB f),i2,(j2 -' 1))) by A2, A5, A6, A7, A8, A12, A14, A16, GOBOARD5: 28;

        end;

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

          hence ( right_cell (( Rev f),j)) = ( cell (( GoB f),i1,j2)) by A2, A5, A6, A7, A8, A12, A14, A15, GOBOARD5: 27;

        end;

      end;

      hence thesis by A1, A4, GOBOARD5:def 7;

    end;

    theorem :: GOBOARD9:10

    

     Th9: i >= 1 & j >= 1 & (i + j) = ( len f) implies ( left_cell (( Rev f),i)) = ( right_cell (f,j))

    proof

      

       A1: ( len ( Rev f)) = ( len f) by FINSEQ_5:def 3;

      ( Rev ( Rev f)) = f;

      hence thesis by A1, Th8;

    end;

    theorem :: GOBOARD9:11

    

     Th10: 1 <= k & (k + 1) <= ( len f) implies ex i, j st i <= ( len ( GoB f)) & j <= ( width ( GoB f)) & ( cell (( GoB f),i,j)) = ( left_cell (f,k))

    proof

      assume that

       A1: 1 <= k and

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

      

       A3: f is_sequence_on ( GoB f) by GOBOARD5:def 5;

      k <= ( len f) by A2, NAT_1: 13;

      then

       A4: k in ( dom f) by A1, FINSEQ_3: 25;

      then

      consider i1,j1 be Nat such that

       A5: [i1, j1] in ( Indices ( GoB f)) and

       A6: (f /. k) = (( GoB f) * (i1,j1)) by A3;

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

      then

       A7: (k + 1) in ( dom f) by A2, FINSEQ_3: 25;

      then

      consider i2,j2 be Nat such that

       A8: [i2, j2] in ( Indices ( GoB f)) and

       A9: (f /. (k + 1)) = (( GoB f) * (i2,j2)) by A3;

      1 <= i1 by A5, MATRIX_0: 32;

      then

       A10: ((i1 -' 1) + 1) = i1 by XREAL_1: 235;

      1 <= j1 by A5, MATRIX_0: 32;

      then

       A11: ((j1 -' 1) + 1) = j1 by XREAL_1: 235;

      reconsider i19 = i1, i29 = i2, j19 = j1, j29 = j2 as Element of REAL by XREAL_0:def 1;

      ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A3, A4, A5, A6, A7, A8, A9;

      then

       A12: |.(i19 - i29).| = 1 & j1 = j2 or |.(j19 - j29).| = 1 & i1 = i2 by SEQM_3: 42;

      

       A13: i1 <= ( len ( GoB f)) by A5, MATRIX_0: 32;

      

       A14: j1 <= ( width ( GoB f)) by A5, MATRIX_0: 32;

      per cases by A12, SEQM_3: 41;

        suppose

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

        take (i1 -' 1), j1;

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

        hence (i1 -' 1) <= ( len ( GoB f)) by A13, XXREAL_0: 2;

        thus j1 <= ( width ( GoB f)) by A5, MATRIX_0: 32;

        thus thesis by A1, A2, A5, A6, A8, A9, A10, A15, GOBOARD5: 27;

      end;

        suppose

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

        take i1, j1;

        thus i1 <= ( len ( GoB f)) by A5, MATRIX_0: 32;

        thus j1 <= ( width ( GoB f)) by A5, MATRIX_0: 32;

        thus thesis by A1, A2, A5, A6, A8, A9, A11, A16, GOBOARD5: 28;

      end;

        suppose

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

        take i2, (j1 -' 1);

        thus i2 <= ( len ( GoB f)) by A8, MATRIX_0: 32;

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

        hence (j1 -' 1) <= ( width ( GoB f)) by A14, XXREAL_0: 2;

        thus thesis by A1, A2, A5, A6, A8, A9, A11, A17, GOBOARD5: 29;

      end;

        suppose

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

        take i1, j2;

        thus i1 <= ( len ( GoB f)) by A5, MATRIX_0: 32;

        thus j2 <= ( width ( GoB f)) by A8, MATRIX_0: 32;

        thus thesis by A1, A2, A5, A6, A8, A9, A10, A18, GOBOARD5: 30;

      end;

    end;

    theorem :: GOBOARD9:12

    

     Th11: j <= ( width G) implies ( Int ( h_strip (G,j))) is convex

    proof

      assume

       A1: j <= ( width G);

      per cases by A1, NAT_1: 14, XXREAL_0: 1;

        suppose j = 0 ;

        then ( Int ( h_strip (G,j))) = { |[r, s]| : s < ((G * (1,1)) `2 ) } by GOBOARD6: 15;

        hence thesis by JORDAN1: 17;

      end;

        suppose j = ( width G);

        then ( Int ( h_strip (G,j))) = { |[r, s]| : ((G * (1,( width G))) `2 ) < s } by GOBOARD6: 16;

        hence thesis by JORDAN1: 15;

      end;

        suppose 1 <= j & j < ( width G);

        then

         A2: ( Int ( h_strip (G,j))) = { |[r, s]| : ((G * (1,j)) `2 ) < s & s < ((G * (1,(j + 1))) `2 ) } by GOBOARD6: 17;

        

         A3: { |[r, s]| : ((G * (1,j)) `2 ) < s } c= the carrier of ( TOP-REAL 2)

        proof

          let x be object;

          assume x in { |[r, s]| : ((G * (1,j)) `2 ) < s };

          then ex r, s st x = |[r, s]| & ((G * (1,j)) `2 ) < s;

          hence thesis;

        end;

        { |[r, s]| : s < ((G * (1,(j + 1))) `2 ) } c= the carrier of ( TOP-REAL 2)

        proof

          let x be object;

          assume x in { |[r, s]| : s < ((G * (1,(j + 1))) `2 ) };

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

          hence thesis;

        end;

        then

        reconsider P = { |[r, s]| : ((G * (1,j)) `2 ) < s }, Q = { |[r, s]| : s < ((G * (1,(j + 1))) `2 ) } as Subset of ( TOP-REAL 2) by A3;

        

         A4: ( Int ( h_strip (G,j))) = (P /\ Q)

        proof

          hereby

            let x be object;

            assume x in ( Int ( h_strip (G,j)));

            then

             A5: ex r, s st x = |[r, s]| & ((G * (1,j)) `2 ) < s & s < ((G * (1,(j + 1))) `2 ) by A2;

            then

             A6: x in P;

            x in Q by A5;

            hence x in (P /\ Q) by A6, XBOOLE_0:def 4;

          end;

          let x be object;

          assume

           A7: x in (P /\ Q);

          then x in P by XBOOLE_0:def 4;

          then

          consider r1, s1 such that

           A8: x = |[r1, s1]| and

           A9: ((G * (1,j)) `2 ) < s1;

          x in Q by A7, XBOOLE_0:def 4;

          then

          consider r2, s2 such that

           A10: x = |[r2, s2]| and

           A11: s2 < ((G * (1,(j + 1))) `2 );

          s1 = s2 by A8, A10, SPPOL_2: 1;

          hence thesis by A2, A8, A9, A11;

        end;

        

         A12: P is convex by JORDAN1: 15;

        Q is convex by JORDAN1: 17;

        hence thesis by A4, A12, Th5;

      end;

    end;

    theorem :: GOBOARD9:13

    

     Th12: i <= ( len G) implies ( Int ( v_strip (G,i))) is convex

    proof

      assume

       A1: i <= ( len G);

      per cases by A1, NAT_1: 14, XXREAL_0: 1;

        suppose i = 0 ;

        then ( Int ( v_strip (G,i))) = { |[r, s]| : r < ((G * (1,1)) `1 ) } by GOBOARD6: 12;

        hence thesis by JORDAN1: 13;

      end;

        suppose i = ( len G);

        then ( Int ( v_strip (G,i))) = { |[r, s]| : ((G * (( len G),1)) `1 ) < r } by GOBOARD6: 13;

        hence thesis by JORDAN1: 11;

      end;

        suppose 1 <= i & i < ( len G);

        then

         A2: ( Int ( v_strip (G,i))) = { |[r, s]| : ((G * (i,1)) `1 ) < r & r < ((G * ((i + 1),1)) `1 ) } by GOBOARD6: 14;

        

         A3: { |[r, s]| : ((G * (i,1)) `1 ) < r } c= the carrier of ( TOP-REAL 2)

        proof

          let x be object;

          assume x in { |[r, s]| : ((G * (i,1)) `1 ) < r };

          then ex r, s st x = |[r, s]| & ((G * (i,1)) `1 ) < r;

          hence thesis;

        end;

        { |[r, s]| : r < ((G * ((i + 1),1)) `1 ) } c= the carrier of ( TOP-REAL 2)

        proof

          let x be object;

          assume x in { |[r, s]| : r < ((G * ((i + 1),1)) `1 ) };

          then ex r, s st x = |[r, s]| & r < ((G * ((i + 1),1)) `1 );

          hence thesis;

        end;

        then

        reconsider P = { |[r, s]| : ((G * (i,1)) `1 ) < r }, Q = { |[r, s]| : r < ((G * ((i + 1),1)) `1 ) } as Subset of ( TOP-REAL 2) by A3;

        

         A4: ( Int ( v_strip (G,i))) = (P /\ Q)

        proof

          hereby

            let x be object;

            assume x in ( Int ( v_strip (G,i)));

            then

             A5: ex r, s st x = |[r, s]| & ((G * (i,1)) `1 ) < r & r < ((G * ((i + 1),1)) `1 ) by A2;

            then

             A6: x in P;

            x in Q by A5;

            hence x in (P /\ Q) by A6, XBOOLE_0:def 4;

          end;

          let x be object;

          assume

           A7: x in (P /\ Q);

          then x in P by XBOOLE_0:def 4;

          then

          consider r1, s1 such that

           A8: x = |[r1, s1]| and

           A9: ((G * (i,1)) `1 ) < r1;

          x in Q by A7, XBOOLE_0:def 4;

          then

          consider r2, s2 such that

           A10: x = |[r2, s2]| and

           A11: r2 < ((G * ((i + 1),1)) `1 );

          r1 = r2 by A8, A10, SPPOL_2: 1;

          hence thesis by A2, A8, A9, A11;

        end;

        

         A12: P is convex by JORDAN1: 11;

        Q is convex by JORDAN1: 13;

        hence thesis by A4, A12, Th5;

      end;

    end;

    theorem :: GOBOARD9:14

    

     Th13: i <= ( len G) & j <= ( width G) implies ( Int ( cell (G,i,j))) <> {}

    proof

      assume that

       A1: i <= ( len G) and

       A2: j <= ( width G);

      

       A3: j = ( width G) or j < ( width G) by A2, XXREAL_0: 1;

      

       A4: i = ( len G) or i < ( len G) by A1, XXREAL_0: 1;

      set p = the Point of ( TOP-REAL 2);

      per cases by A3, A4, NAT_1: 13, NAT_1: 14;

        suppose 1 <= i & (i + 1) <= ( len G) & 1 <= j & (j + 1) <= ( width G);

        then ( LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),p)) meets ( Int ( cell (G,i,j))) by GOBOARD6: 82;

        hence thesis;

      end;

        suppose 1 <= i & (i + 1) <= ( len G) & j = ( width G);

        then ( LSeg (p,(((1 / 2) * ((G * (i,j)) + (G * ((i + 1),j)))) + |[ 0 , 1]|))) meets ( Int ( cell (G,i,j))) by GOBOARD6: 83;

        hence thesis;

      end;

        suppose 1 <= i & (i + 1) <= ( len G) & j = 0 ;

        then ( LSeg ((((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1))))) - |[ 0 , 1]|),p)) meets ( Int ( cell (G,i,j))) by GOBOARD6: 84;

        hence thesis;

      end;

        suppose 1 <= j & (j + 1) <= ( width G) & i = 0 ;

        then ( LSeg ((((1 / 2) * ((G * ((i + 1),j)) + (G * ((i + 1),(j + 1))))) - |[1, 0 ]|),p)) meets ( Int ( cell (G,i,j))) by GOBOARD6: 85;

        hence thesis;

      end;

        suppose 1 <= j & (j + 1) <= ( width G) & i = ( len G);

        then ( LSeg (p,(((1 / 2) * ((G * (i,j)) + (G * (i,(j + 1))))) + |[1, 0 ]|))) meets ( Int ( cell (G,i,j))) by GOBOARD6: 86;

        hence thesis;

      end;

        suppose i = 0 & j = 0 ;

        then ( LSeg (p,((G * ((i + 1),(j + 1))) - |[1, 1]|))) meets ( Int ( cell (G,i,j))) by GOBOARD6: 87;

        hence thesis;

      end;

        suppose i = ( len G) & j = ( width G);

        then ( LSeg (p,((G * (i,j)) + |[1, 1]|))) meets ( Int ( cell (G,i,j))) by GOBOARD6: 88;

        hence thesis;

      end;

        suppose i = 0 & j = ( width G);

        then ( LSeg (p,((G * ((i + 1),j)) + |[( - 1), 1]|))) meets ( Int ( cell (G,i,j))) by GOBOARD6: 89;

        hence thesis;

      end;

        suppose i = ( len G) & j = 0 ;

        then ( LSeg (p,((G * (i,(j + 1))) + |[1, ( - 1)]|))) meets ( Int ( cell (G,i,j))) by GOBOARD6: 90;

        hence thesis;

      end;

    end;

    theorem :: GOBOARD9:15

    

     Th14: 1 <= k & (k + 1) <= ( len f) implies ( Int ( left_cell (f,k))) <> {}

    proof

      assume that

       A1: 1 <= k and

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

      ex i, j st i <= ( len ( GoB f)) & j <= ( width ( GoB f)) & ( cell (( GoB f),i,j)) = ( left_cell (f,k)) by A1, A2, Th10;

      hence thesis by Th13;

    end;

    theorem :: GOBOARD9:16

    

     Th15: 1 <= k & (k + 1) <= ( len f) implies ( Int ( right_cell (f,k))) <> {}

    proof

      assume that

       A1: 1 <= k and

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

      

       A3: ( len f) = ( len ( Rev f)) by FINSEQ_5:def 3;

      k <= ( len f) by A2, NAT_1: 13;

      then

       A4: ((( len f) -' k) + k) = ( len f) by XREAL_1: 235;

      then

       A5: ((( len f) -' k) + 1) <= ( len f) by A1, XREAL_1: 6;

      

       A6: (( len f) -' k) >= 1 by A2, A4, XREAL_1: 6;

      then ( right_cell (f,k)) = ( left_cell (( Rev f),(( len f) -' k))) by A1, A4, Th9;

      hence thesis by A3, A5, A6, Th14;

    end;

    theorem :: GOBOARD9:17

    

     Th16: i <= ( len G) & j <= ( width G) implies ( Int ( cell (G,i,j))) is convex

    proof

      assume that

       A1: i <= ( len G) and

       A2: j <= ( width G);

      set P = ( Int ( cell (G,i,j)));

      

       A3: P = (( Int ( v_strip (G,i))) /\ ( Int ( h_strip (G,j)))) by TOPS_1: 17;

      

       A4: ( Int ( v_strip (G,i))) is convex by A1, Th12;

      ( Int ( h_strip (G,j))) is convex by A2, Th11;

      hence thesis by A3, A4, Th5;

    end;

    ::$Canceled

    theorem :: GOBOARD9:19

    

     Th17: 1 <= k & (k + 1) <= ( len f) implies ( Int ( left_cell (f,k))) is convex

    proof

      assume that

       A1: 1 <= k and

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

      ex i, j st i <= ( len ( GoB f)) & j <= ( width ( GoB f)) & ( cell (( GoB f),i,j)) = ( left_cell (f,k)) by A1, A2, Th10;

      hence thesis by Th16;

    end;

    theorem :: GOBOARD9:20

    

     Th18: 1 <= k & (k + 1) <= ( len f) implies ( Int ( right_cell (f,k))) is convex

    proof

      assume that

       A1: 1 <= k and

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

      

       A3: ( len f) = ( len ( Rev f)) by FINSEQ_5:def 3;

      k <= ( len f) by A2, NAT_1: 13;

      then

       A4: ((( len f) -' k) + k) = ( len f) by XREAL_1: 235;

      then

       A5: ((( len f) -' k) + 1) <= ( len f) by A1, XREAL_1: 6;

      

       A6: (( len f) -' k) >= 1 by A2, A4, XREAL_1: 6;

      then ( right_cell (f,k)) = ( left_cell (( Rev f),(( len f) -' k))) by A1, A4, Th9;

      hence thesis by A3, A5, A6, Th17;

    end;

    definition

      let f;

      

       A1: (1 + 1) < ( len f) by GOBOARD7: 34, XXREAL_0: 2;

      then

       A2: ( Int ( left_cell (f,1))) <> {} by Th14;

      

       A3: ( Int ( right_cell (f,1))) <> {} by A1, Th15;

      :: GOBOARD9:def1

      func LeftComp f -> Subset of ( TOP-REAL 2) means

      : Def1: it is_a_component_of (( L~ f) ` ) & ( Int ( left_cell (f,1))) c= it ;

      existence

      proof

        

         A4: ( Int ( left_cell (f,1))) is convex by A1, Th17;

        ( Int ( left_cell (f,1))) misses ( L~ f) by A1, GOBOARD8: 37;

        then

         A5: ( Int ( left_cell (f,1))) c= (( L~ f) ` ) by SUBSET_1: 23;

        then (( L~ f) ` ) <> {} by A1, Th14, XBOOLE_1: 3;

        hence thesis by A2, A4, A5, Th3;

      end;

      uniqueness by A2, Th1, XBOOLE_1: 67;

      :: GOBOARD9:def2

      func RightComp f -> Subset of ( TOP-REAL 2) means

      : Def2: it is_a_component_of (( L~ f) ` ) & ( Int ( right_cell (f,1))) c= it ;

      existence

      proof

        

         A6: ( Int ( right_cell (f,1))) is convex by A1, Th18;

        ( Int ( right_cell (f,1))) misses ( L~ f) by A1, GOBOARD8: 38;

        then

         A7: ( Int ( right_cell (f,1))) c= (( L~ f) ` ) by SUBSET_1: 23;

        then (( L~ f) ` ) <> {} by A1, Th15, XBOOLE_1: 3;

        hence thesis by A3, A6, A7, Th3;

      end;

      uniqueness by A3, Th1, XBOOLE_1: 67;

    end

    theorem :: GOBOARD9:21

    

     Th19: for k st 1 <= k & (k + 1) <= ( len f) holds ( Int ( left_cell (f,k))) c= ( LeftComp f)

    proof

      defpred P[ Nat] means 1 <= $1 & ($1 + 1) <= ( len f) implies ( Int ( left_cell (f,$1))) c= ( LeftComp f);

      

       A1: P[ 0 ];

       A2:

      now

        let k such that

         A3: P[k];

        thus P[(k + 1)]

        proof

          assume that

           A4: 1 <= (k + 1) and

           A5: ((k + 1) + 1) <= ( len f);

          per cases by NAT_1: 14;

            suppose k = 0 ;

            hence thesis by Def1;

          end;

            suppose

             A6: k >= 1;

            

             A7: (k + 1) <= ( len f) by A5, NAT_1: 13;

            

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

            then k <= ( len f) by A7, XXREAL_0: 2;

            then

             A9: k in ( dom f) by A6, FINSEQ_3: 25;

            then

            consider i0,j0 be Nat such that

             A10: [i0, j0] in ( Indices ( GoB f)) and

             A11: (f /. k) = (( GoB f) * (i0,j0)) by GOBOARD2: 14;

            

             A12: (k + 1) in ( dom f) by A4, A7, FINSEQ_3: 25;

            then

            consider i1,j1 be Nat such that

             A13: [i1, j1] in ( Indices ( GoB f)) and

             A14: (f /. (k + 1)) = (( GoB f) * (i1,j1)) by GOBOARD2: 14;

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

            then

             A15: ((k + 1) + 1) in ( dom f) by A5, FINSEQ_3: 25;

            then

            consider i2,j2 be Nat such that

             A16: [i2, j2] in ( Indices ( GoB f)) and

             A17: (f /. ((k + 1) + 1)) = (( GoB f) * (i2,j2)) by GOBOARD2: 14;

            

             A18: 1 <= i0 by A10, MATRIX_0: 32;

            

             A19: i0 <= ( len ( GoB f)) by A10, MATRIX_0: 32;

            

             A20: 1 <= i1 by A13, MATRIX_0: 32;

            

             A21: i1 <= ( len ( GoB f)) by A13, MATRIX_0: 32;

            

             A22: 1 <= i2 by A16, MATRIX_0: 32;

            

             A23: i2 <= ( len ( GoB f)) by A16, MATRIX_0: 32;

            

             A24: 1 <= j0 by A10, MATRIX_0: 32;

            

             A25: j0 <= ( width ( GoB f)) by A10, MATRIX_0: 32;

            

             A26: 1 <= j1 by A13, MATRIX_0: 32;

            

             A27: j1 <= ( width ( GoB f)) by A13, MATRIX_0: 32;

            

             A28: 1 <= j2 by A16, MATRIX_0: 32;

            

             A29: j2 <= ( width ( GoB f)) by A16, MATRIX_0: 32;

            

             A30: i0 = i1 or j0 = j1 by A9, A10, A11, A12, A13, A14, GOBOARD2: 11;

            

             A31: i1 = i2 or j1 = j2 by A12, A13, A14, A15, A16, A17, GOBOARD2: 11;

            reconsider i19 = i1, i09 = i0, i29 = i2, j19 = j1, j09 = j0, j29 = j2 as Element of REAL by XREAL_0:def 1;

            

             A32: f is_sequence_on ( GoB f) by GOBOARD5:def 5;

            then ( |.(i0 - i1).| + |.(j0 - j1).|) = 1 by A9, A10, A11, A12, A13, A14;

            then

             A33: |.(i09 - i19).| = 1 & j0 = j1 or |.(j09 - j19).| = 1 & i0 = i1 by SEQM_3: 42;

            then

             A34: i0 = i1 or i0 = (i1 + 1) or (i0 + 1) = i1 by SEQM_3: 41;

            ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A12, A13, A14, A15, A16, A17, A32;

            then

             A35: |.(i19 - i29).| = 1 & j1 = j2 or |.(j19 - j29).| = 1 & i1 = i2 by SEQM_3: 42;

            then

             A36: i1 = i2 or i1 = (i2 + 1) or (i1 + 1) = i2 by SEQM_3: 41;

            

             A37: j0 = j1 or j0 = (j1 + 1) or (j0 + 1) = j1 by A33, SEQM_3: 41;

            

             A38: j1 = j2 or j1 = (j2 + 1) or (j1 + 1) = j2 by A35, SEQM_3: 41;

             A39:

            now

              assume that

               A40: i0 = i2 and

               A41: j0 = j2;

               A42:

              now

                assume k <= 1;

                then

                 A43: k = 1 by A6, XXREAL_0: 1;

                assume ((k + 1) + 1) >= ( len f);

                then ((k + 1) + 1) = ( len f) by A5, XXREAL_0: 1;

                hence contradiction by A43, GOBOARD7: 34;

              end;

              

               A44: k < ((k + 1) + 1) by A8, NAT_1: 13;

              per cases by A42;

                suppose k > 1;

                hence contradiction by A5, A11, A17, A40, A41, A44, GOBOARD7: 37;

              end;

                suppose ((k + 1) + 1) < ( len f);

                hence contradiction by A6, A11, A17, A40, A41, A44, GOBOARD7: 36;

              end;

            end;

            i1 >= 1 by A13, MATRIX_0: 32;

            then

             A45: i1 = ((i1 -' 1) + 1) by XREAL_1: 235;

            j1 >= 1 by A13, MATRIX_0: 32;

            then

             A46: j1 = ((j1 -' 1) + 1) by XREAL_1: 235;

            then (j1 -' 1) <= j1 by NAT_1: 11;

            then

             A47: (j1 -' 1) <= ( width ( GoB f)) by A27, XXREAL_0: 2;

            ( len ( GoB f)) > 1 by GOBOARD7: 32;

            then

             A48: ((( len ( GoB f)) -' 1) + 1) = ( len ( GoB f)) by XREAL_1: 235;

            ( width ( GoB f)) >= 1 by GOBOARD7: 33;

            then

             A49: ((( width ( GoB f)) -' 1) + 1) = ( width ( GoB f)) by XREAL_1: 235;

            

             A50: ((k + 1) + 1) = (k + (1 + 1));

            

             A51: ((i0 + 1) + 1) = (i0 + (1 + 1));

            

             A52: ((i2 + 1) + 1) = (i2 + (1 + 1));

            

             A53: ((j0 + 1) + 1) = (j0 + (1 + 1));

            

             A54: ((j2 + 1) + 1) = (j2 + (1 + 1));

            

             A55: ( LeftComp f) is_a_component_of (( L~ f) ` ) by Def1;

            

             A56: ( 0 + 1) = 1;

            now

              per cases by A9, A11, A12, A14, A15, A17, A34, A36, A37, A38, A39, GOBOARD7: 29;

                suppose that

                 A57: i0 = (i1 + 1) and

                 A58: i1 = (i2 + 1) and

                 A59: j0 = 1;

                

                 A60: ( left_cell (f,k)) = ( cell (( GoB f),i1, 0 )) by A6, A7, A10, A11, A13, A14, A30, A56, A57, A59, GOBOARD5: 29;

                ( 0 + 1) = j2 by A30, A31, A57, A58, A59;

                then

                 A61: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i2, 0 )) by A4, A5, A13, A14, A16, A17, A30, A57, A58, A59, GOBOARD5: 29;

                

                 A62: ( LSeg ((((1 / 2) * ((( GoB f) * (i1,1)) + (( GoB f) * (i0,1)))) - |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i2,1)) + (( GoB f) * (i1,1)))) - |[ 0 , 1]|))) meets ( Int ( cell (( GoB f),i1, 0 ))) by A19, A20, A57, GOBOARD6: 84;

                ( LSeg ((((1 / 2) * ((( GoB f) * (i1,1)) + (( GoB f) * (i0,1)))) - |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i2,1)) + (( GoB f) * (i1,1)))) - |[ 0 , 1]|))) misses ( L~ f) by A19, A22, A52, A57, A58, GOBOARD8: 25;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (i1,1)) + (( GoB f) * (i0,1)))) - |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i2,1)) + (( GoB f) * (i1,1)))) - |[ 0 , 1]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A63: ( LSeg ((((1 / 2) * ((( GoB f) * (i1,1)) + (( GoB f) * (i0,1)))) - |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i2,1)) + (( GoB f) * (i1,1)))) - |[ 0 , 1]|))) c= ( LeftComp f) by A3, A5, A6, A55, A60, A62, Th4, NAT_1: 13;

                

                 A64: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A61, A63, A21, A22, A58, Th4, A64, GOBOARD6: 84;

              end;

                suppose that

                 A65: i0 = (i1 + 1) and

                 A66: i1 = (i2 + 1) and

                 A67: j0 <> 1;

                

                 A68: ( left_cell (f,k)) = ( cell (( GoB f),i1,(j1 -' 1))) by A6, A7, A10, A11, A13, A14, A30, A46, A65, GOBOARD5: 29;

                1 < j0 by A24, A67, XXREAL_0: 1;

                then

                 A69: 1 <= (j0 -' 1) by A30, A46, A65, NAT_1: 13;

                

                 A70: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i2,(j1 -' 1))) by A4, A5, A13, A14, A16, A17, A31, A46, A66, GOBOARD5: 29;

                

                 A71: ( LSeg (((1 / 2) * ((( GoB f) * (i1,(j0 -' 1))) + (( GoB f) * (i0,j0)))),((1 / 2) * ((( GoB f) * (i2,(j0 -' 1))) + (( GoB f) * (i1,j0)))))) meets ( Int ( cell (( GoB f),i1,(j1 -' 1)))) by A19, A20, A27, A30, A46, A65, A69, GOBOARD6: 82;

                ( LSeg (((1 / 2) * ((( GoB f) * (i1,(j0 -' 1))) + (( GoB f) * (i0,j0)))),((1 / 2) * ((( GoB f) * (i2,(j0 -' 1))) + (( GoB f) * (i1,j0)))))) misses ( L~ f) by A5, A6, A11, A14, A17, A19, A22, A25, A30, A31, A46, A50, A52, A65, A66, A69, GOBOARD8: 11;

                then ( LSeg (((1 / 2) * ((( GoB f) * (i1,(j0 -' 1))) + (( GoB f) * (i0,j0)))),((1 / 2) * ((( GoB f) * (i2,(j0 -' 1))) + (( GoB f) * (i1,j0)))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A72: ( LSeg (((1 / 2) * ((( GoB f) * (i1,(j0 -' 1))) + (( GoB f) * (i0,j0)))),((1 / 2) * ((( GoB f) * (i2,(j0 -' 1))) + (( GoB f) * (i1,j0)))))) c= ( LeftComp f) by A3, A5, A6, A55, A68, A71, Th4, NAT_1: 13;

                

                 A73: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A30, A55, A65, A66, A70, A72, A21, A22, A25, A46, A69, Th4, A73, GOBOARD6: 82;

              end;

                suppose that

                 A74: i0 = (i1 + 1) and

                 A75: j1 = (j2 + 1);

                ( left_cell (f,k)) = ( cell (( GoB f),i1,j2)) by A6, A7, A10, A11, A13, A14, A30, A74, A75, GOBOARD5: 29

                .= ( left_cell (f,(k + 1))) by A4, A5, A13, A14, A16, A17, A31, A45, A75, GOBOARD5: 30;

                hence thesis by A3, A5, A6, NAT_1: 13;

              end;

                suppose that

                 A76: j0 = (j1 + 1) and

                 A77: i1 = (i2 + 1) and

                 A78: i0 = ( len ( GoB f)) and

                 A79: j1 = 1;

                

                 A80: ( left_cell (f,k)) = ( cell (( GoB f),i0,j1)) by A6, A7, A10, A11, A13, A14, A30, A45, A76, GOBOARD5: 30;

                

                 A81: ( LSeg (((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),1)) + (( GoB f) * (( len ( GoB f)),2)))) + |[1, 0 ]|))) meets ( Int ( cell (( GoB f),i0,j1))) by A25, A76, A78, A79, GOBOARD6: 86;

                ( LSeg (((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),1)) + (( GoB f) * (( len ( GoB f)),2)))) + |[1, 0 ]|))) misses ( L~ f) by GOBOARD8: 35;

                then ( LSeg (((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),1)) + (( GoB f) * (( len ( GoB f)),2)))) + |[1, 0 ]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A82: ( LSeg (((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),1)) + (( GoB f) * (( len ( GoB f)),2)))) + |[1, 0 ]|))) c= ( LeftComp f) by A3, A5, A6, A55, A80, A81, Th4, NAT_1: 13;

                

                 A83: ( Int ( cell (( GoB f),i1, 0 ))) is convex by A21, A26, A27, Th16;

                ( Int ( cell (( GoB f),i1, 0 ))) misses ( L~ f) by A21, A26, A27, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),i1, 0 ))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A84: ( Int ( cell (( GoB f),i1, 0 ))) c= ( LeftComp f) by A55, A82, A30, A76, A78, Th4, A83, GOBOARD6: 90;

                

                 A85: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i2, 0 )) by A4, A5, A13, A14, A16, A17, A31, A46, A77, A79, GOBOARD5: 29;

                

                 A86: ( LSeg ((((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),1)) + (( GoB f) * (( len ( GoB f)),1)))) - |[ 0 , 1]|),((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|))) meets ( Int ( cell (( GoB f),i1, 0 ))) by A30, A76, A78, GOBOARD6: 90;

                ( LSeg ((((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),1)) + (( GoB f) * (( len ( GoB f)),1)))) - |[ 0 , 1]|),((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|))) misses ( L~ f) by GOBOARD8: 27;

                then ( LSeg ((((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),1)) + (( GoB f) * (( len ( GoB f)),1)))) - |[ 0 , 1]|),((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A87: ( LSeg ((((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),1)) + (( GoB f) * (( len ( GoB f)),1)))) - |[ 0 , 1]|),((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|))) c= ( LeftComp f) by A55, A84, A86, Th4;

                

                 A88: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A85, A87, A22, A30, A45, A76, A77, A78, Th4, A88, GOBOARD6: 84;

              end;

                suppose that

                 A89: j0 = (j1 + 1) and

                 A90: i1 = (i2 + 1) and

                 A91: i0 <> ( len ( GoB f)) and

                 A92: j1 = 1;

                

                 A93: ( left_cell (f,k)) = ( cell (( GoB f),i0,j1)) by A6, A7, A10, A11, A13, A14, A30, A45, A89, GOBOARD5: 30;

                ( len ( GoB f)) > i0 by A19, A91, XXREAL_0: 1;

                then

                 A94: ( len ( GoB f)) >= (i0 + 1) by NAT_1: 13;

                

                 A95: ( LSeg ((((1 / 2) * ((( GoB f) * (i0,1)) + (( GoB f) * ((i0 + 1),1)))) - |[ 0 , 1]|),((1 / 2) * ((( GoB f) * (i1,1)) + (( GoB f) * ((i1 + 1),(1 + 1))))))) meets ( Int ( cell (( GoB f),i0,j1))) by A20, A25, A30, A89, A92, A94, GOBOARD6: 82;

                ( LSeg ((((1 / 2) * ((( GoB f) * (i0,1)) + (( GoB f) * ((i0 + 1),1)))) - |[ 0 , 1]|),((1 / 2) * ((( GoB f) * (i1,1)) + (( GoB f) * ((i1 + 1),2)))))) misses ( L~ f) by A5, A6, A11, A14, A17, A22, A30, A31, A50, A52, A89, A90, A92, A94, GOBOARD8: 8;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (i0,1)) + (( GoB f) * ((i0 + 1),1)))) - |[ 0 , 1]|),((1 / 2) * ((( GoB f) * (i1,1)) + (( GoB f) * ((i1 + 1),2)))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A96: ( LSeg ((((1 / 2) * ((( GoB f) * (i0,1)) + (( GoB f) * ((i0 + 1),1)))) - |[ 0 , 1]|),((1 / 2) * ((( GoB f) * (i1,1)) + (( GoB f) * ((i1 + 1),2)))))) c= ( LeftComp f) by A3, A5, A6, A55, A93, A95, Th4, NAT_1: 13;

                

                 A97: ( Int ( cell (( GoB f),i1, 0 ))) is convex by A21, A26, A27, Th16;

                ( Int ( cell (( GoB f),i1, 0 ))) misses ( L~ f) by A21, A26, A27, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),i1, 0 ))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A98: ( Int ( cell (( GoB f),i1, 0 ))) c= ( LeftComp f) by A55, A96, A20, A30, A89, A94, Th4, A97, GOBOARD6: 84;

                

                 A99: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i2, 0 )) by A4, A5, A13, A14, A16, A17, A31, A46, A90, A92, GOBOARD5: 29;

                

                 A100: ( LSeg ((((1 / 2) * ((( GoB f) * (i2,1)) + (( GoB f) * ((i2 + 1),1)))) - |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * ((i2 + 1),1)) + (( GoB f) * ((i2 + 2),1)))) - |[ 0 , 1]|))) meets ( Int ( cell (( GoB f),i1, 0 ))) by A20, A30, A89, A90, A94, GOBOARD6: 84;

                ( LSeg ((((1 / 2) * ((( GoB f) * (i2,1)) + (( GoB f) * ((i2 + 1),1)))) - |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * ((i2 + 1),1)) + (( GoB f) * ((i2 + 2),1)))) - |[ 0 , 1]|))) misses ( L~ f) by A22, A30, A89, A90, A94, GOBOARD8: 25;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (i2,1)) + (( GoB f) * ((i2 + 1),1)))) - |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * ((i2 + 1),1)) + (( GoB f) * ((i2 + 2),1)))) - |[ 0 , 1]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A101: ( LSeg ((((1 / 2) * ((( GoB f) * (i2,1)) + (( GoB f) * ((i2 + 1),1)))) - |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * ((i2 + 1),1)) + (( GoB f) * ((i2 + 2),1)))) - |[ 0 , 1]|))) c= ( LeftComp f) by A55, A98, A100, Th4;

                

                 A102: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A99, A101, A21, A22, A90, Th4, A102, GOBOARD6: 84;

              end;

                suppose that

                 A103: j0 = (j1 + 1) and

                 A104: i1 = (i2 + 1) and

                 A105: i0 = ( len ( GoB f)) and

                 A106: j1 <> 1;

                

                 A107: ( left_cell (f,k)) = ( cell (( GoB f),i0,j1)) by A6, A7, A10, A11, A13, A14, A30, A45, A103, GOBOARD5: 30;

                1 < j1 by A26, A106, XXREAL_0: 1;

                then

                 A108: 1 <= (j1 -' 1) by A46, NAT_1: 13;

                

                 A109: (j1 + 1) = ((j1 -' 1) + (1 + 1)) by A46;

                

                 A110: ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j1 -' 1))) + (( GoB f) * (( len ( GoB f)),j1)))) + |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),j1)) + (( GoB f) * (( len ( GoB f)),(j1 + 1))))) + |[1, 0 ]|))) meets ( Int ( cell (( GoB f),i0,j1))) by A25, A26, A103, A105, GOBOARD6: 86;

                ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j1 -' 1))) + (( GoB f) * (( len ( GoB f)),j1)))) + |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),j1)) + (( GoB f) * (( len ( GoB f)),(j1 + 1))))) + |[1, 0 ]|))) misses ( L~ f) by A25, A46, A103, A108, A109, GOBOARD8: 34;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j1 -' 1))) + (( GoB f) * (( len ( GoB f)),j1)))) + |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),j1)) + (( GoB f) * (( len ( GoB f)),(j1 + 1))))) + |[1, 0 ]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A111: ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j1 -' 1))) + (( GoB f) * (( len ( GoB f)),j1)))) + |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),j1)) + (( GoB f) * (( len ( GoB f)),(j1 + 1))))) + |[1, 0 ]|))) c= ( LeftComp f) by A3, A5, A6, A55, A107, A110, Th4, NAT_1: 13;

                j1 > 1 by A26, A106, XXREAL_0: 1;

                then

                 A112: 1 <= (j1 -' 1) by A46, NAT_1: 13;

                

                 A113: ( Int ( cell (( GoB f),i1,(j1 -' 1)))) is convex by A21, A47, Th16;

                ( Int ( cell (( GoB f),i1,(j1 -' 1)))) misses ( L~ f) by A21, A47, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),i1,(j1 -' 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A114: ( Int ( cell (( GoB f),i1,(j1 -' 1)))) c= ( LeftComp f) by A55, A111, A27, A30, A46, A103, A105, Th4, A113, A112, GOBOARD6: 86;

                

                 A115: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i2,(j1 -' 1))) by A4, A5, A13, A14, A16, A17, A31, A46, A104, GOBOARD5: 29;

                

                 A116: ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),(j1 -' 1))) + (( GoB f) * (i1,j1)))),(((1 / 2) * ((( GoB f) * (i1,(j1 -' 1))) + (( GoB f) * (i1,j1)))) + |[1, 0 ]|))) meets ( Int ( cell (( GoB f),i1,(j1 -' 1)))) by A27, A30, A46, A103, A105, A108, GOBOARD6: 86;

                

                 A117: (i1 -' 1) = i2 by A104, NAT_D: 34;

                then ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),(j1 -' 1))) + (( GoB f) * (i1,j1)))),(((1 / 2) * ((( GoB f) * (i1,(j1 -' 1))) + (( GoB f) * (i1,j1)))) + |[1, 0 ]|))) misses ( L~ f) by A5, A6, A11, A14, A17, A25, A30, A31, A46, A50, A103, A104, A105, A108, A109, GOBOARD8: 19;

                then ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),(j1 -' 1))) + (( GoB f) * (i1,j1)))),(((1 / 2) * ((( GoB f) * (i1,(j1 -' 1))) + (( GoB f) * (i1,j1)))) + |[1, 0 ]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A118: ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),(j1 -' 1))) + (( GoB f) * (i1,j1)))),(((1 / 2) * ((( GoB f) * (i1,(j1 -' 1))) + (( GoB f) * (i1,j1)))) + |[1, 0 ]|))) c= ( LeftComp f) by A55, A114, A116, Th4;

                

                 A119: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A115, A118, A21, A22, A27, A46, A104, A108, A117, Th4, A119, GOBOARD6: 82;

              end;

                suppose that

                 A120: j0 = (j1 + 1) and

                 A121: i1 = (i2 + 1) and

                 A122: i0 <> ( len ( GoB f)) and

                 A123: j1 <> 1;

                

                 A124: ( left_cell (f,k)) = ( cell (( GoB f),i0,j1)) by A6, A7, A10, A11, A13, A14, A30, A45, A120, GOBOARD5: 30;

                1 < j1 by A26, A123, XXREAL_0: 1;

                then

                 A125: 1 <= (j1 -' 1) by A46, NAT_1: 13;

                ( len ( GoB f)) > i0 by A19, A122, XXREAL_0: 1;

                then

                 A126: ( len ( GoB f)) >= (i0 + 1) by NAT_1: 13;

                

                 A127: (j1 + 1) = ((j1 -' 1) + (1 + 1)) by A46;

                

                 A128: ( LSeg (((1 / 2) * ((( GoB f) * (i0,(j1 -' 1))) + (( GoB f) * ((i0 + 1),j1)))),((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * ((i1 + 1),(j1 + 1))))))) meets ( Int ( cell (( GoB f),i0,j1))) by A20, A25, A26, A30, A120, A126, GOBOARD6: 82;

                ( LSeg (((1 / 2) * ((( GoB f) * (i0,(j1 -' 1))) + (( GoB f) * ((i0 + 1),j1)))),((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * ((i1 + 1),(j1 + 1))))))) misses ( L~ f) by A5, A6, A11, A14, A17, A22, A25, A30, A31, A46, A50, A52, A120, A121, A125, A126, A127, GOBOARD8: 5;

                then ( LSeg (((1 / 2) * ((( GoB f) * (i0,(j1 -' 1))) + (( GoB f) * ((i0 + 1),j1)))),((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * ((i1 + 1),(j1 + 1))))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A129: ( LSeg (((1 / 2) * ((( GoB f) * (i0,(j1 -' 1))) + (( GoB f) * ((i0 + 1),j1)))),((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * ((i1 + 1),(j1 + 1))))))) c= ( LeftComp f) by A3, A5, A6, A55, A124, A128, Th4, NAT_1: 13;

                j1 > 1 by A26, A123, XXREAL_0: 1;

                then

                 A130: 1 <= (j1 -' 1) by A46, NAT_1: 13;

                

                 A131: ( Int ( cell (( GoB f),i1,(j1 -' 1)))) is convex by A21, A47, Th16;

                ( Int ( cell (( GoB f),i1,(j1 -' 1)))) misses ( L~ f) by A21, A47, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),i1,(j1 -' 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A132: ( Int ( cell (( GoB f),i1,(j1 -' 1)))) c= ( LeftComp f) by A30, A55, A120, A129, A20, A27, A46, A126, Th4, A131, A130, GOBOARD6: 82;

                

                 A133: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i2,(j1 -' 1))) by A4, A5, A13, A14, A16, A17, A31, A46, A121, GOBOARD5: 29;

                

                 A134: ( LSeg (((1 / 2) * ((( GoB f) * (i1,(j1 -' 1))) + (( GoB f) * ((i1 + 1),j1)))),((1 / 2) * ((( GoB f) * (i2,(j1 -' 1))) + (( GoB f) * (i1,j1)))))) meets ( Int ( cell (( GoB f),i1,(j1 -' 1)))) by A20, A27, A30, A46, A120, A125, A126, GOBOARD6: 82;

                i1 < ( len ( GoB f)) by A21, A30, A120, A122, XXREAL_0: 1;

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

                then ( LSeg (((1 / 2) * ((( GoB f) * (i1,(j1 -' 1))) + (( GoB f) * ((i1 + 1),j1)))),((1 / 2) * ((( GoB f) * (i2,(j1 -' 1))) + (( GoB f) * (i1,j1)))))) misses ( L~ f) by A5, A6, A11, A14, A17, A22, A25, A30, A31, A46, A50, A52, A120, A121, A125, A127, GOBOARD8: 13;

                then ( LSeg (((1 / 2) * ((( GoB f) * (i1,(j1 -' 1))) + (( GoB f) * ((i1 + 1),j1)))),((1 / 2) * ((( GoB f) * (i2,(j1 -' 1))) + (( GoB f) * (i1,j1)))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A135: ( LSeg (((1 / 2) * ((( GoB f) * (i1,(j1 -' 1))) + (( GoB f) * ((i1 + 1),j1)))),((1 / 2) * ((( GoB f) * (i2,(j1 -' 1))) + (( GoB f) * (i1,j1)))))) c= ( LeftComp f) by A55, A132, A134, Th4;

                

                 A136: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A121, A133, A135, A21, A22, A27, A46, A125, Th4, A136, GOBOARD6: 82;

              end;

                suppose that

                 A137: j0 = (j1 + 1) and

                 A138: j1 = (j2 + 1) and

                 A139: i0 = ( len ( GoB f));

                

                 A140: ( left_cell (f,k)) = ( cell (( GoB f),( len ( GoB f)),j1)) by A6, A7, A10, A11, A13, A14, A30, A48, A137, A139, GOBOARD5: 30;

                

                 A141: ( left_cell (f,(k + 1))) = ( cell (( GoB f),( len ( GoB f)),j2)) by A4, A5, A13, A14, A16, A17, A30, A31, A48, A137, A138, A139, GOBOARD5: 30;

                

                 A142: ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),j2)) + (( GoB f) * (( len ( GoB f)),(j2 + 1))))) + |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j2 + 1))) + (( GoB f) * (( len ( GoB f)),(j2 + 2))))) + |[1, 0 ]|))) meets ( Int ( cell (( GoB f),( len ( GoB f)),j1))) by A25, A26, A137, A138, GOBOARD6: 86;

                ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),j2)) + (( GoB f) * (( len ( GoB f)),(j2 + 1))))) + |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j2 + 1))) + (( GoB f) * (( len ( GoB f)),(j2 + 2))))) + |[1, 0 ]|))) misses ( L~ f) by A25, A28, A137, A138, GOBOARD8: 34;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),j2)) + (( GoB f) * (( len ( GoB f)),(j2 + 1))))) + |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j2 + 1))) + (( GoB f) * (( len ( GoB f)),(j2 + 2))))) + |[1, 0 ]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A143: ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),j2)) + (( GoB f) * (( len ( GoB f)),(j2 + 1))))) + |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j2 + 1))) + (( GoB f) * (( len ( GoB f)),(j2 + 2))))) + |[1, 0 ]|))) c= ( LeftComp f) by A3, A5, A6, A55, A140, A142, Th4, NAT_1: 13;

                

                 A144: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A141, A143, A27, A28, A138, Th4, A144, GOBOARD6: 86;

              end;

                suppose that

                 A145: j0 = (j1 + 1) and

                 A146: j1 = (j2 + 1) and

                 A147: i0 <> ( len ( GoB f));

                

                 A148: ( left_cell (f,k)) = ( cell (( GoB f),i0,j1)) by A6, A7, A10, A11, A13, A14, A30, A45, A145, GOBOARD5: 30;

                ( len ( GoB f)) > i0 by A19, A147, XXREAL_0: 1;

                then

                 A149: ( len ( GoB f)) >= (i0 + 1) by NAT_1: 13;

                

                 A150: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i1,j2)) by A4, A5, A13, A14, A16, A17, A31, A45, A146, GOBOARD5: 30;

                

                 A151: ( LSeg (((1 / 2) * ((( GoB f) * (i0,j2)) + (( GoB f) * ((i0 + 1),(j2 + 1))))),((1 / 2) * ((( GoB f) * (i1,(j2 + 1))) + (( GoB f) * ((i1 + 1),(j2 + 2))))))) meets ( Int ( cell (( GoB f),i0,j1))) by A20, A25, A26, A30, A145, A146, A149, GOBOARD6: 82;

                ( LSeg (((1 / 2) * ((( GoB f) * (i0,j2)) + (( GoB f) * ((i0 + 1),(j2 + 1))))),((1 / 2) * ((( GoB f) * (i1,(j2 + 1))) + (( GoB f) * ((i1 + 1),(j2 + 2))))))) misses ( L~ f) by A5, A6, A11, A14, A17, A18, A25, A28, A30, A31, A50, A145, A146, A149, GOBOARD8: 4;

                then ( LSeg (((1 / 2) * ((( GoB f) * (i0,j2)) + (( GoB f) * ((i0 + 1),(j2 + 1))))),((1 / 2) * ((( GoB f) * (i1,(j2 + 1))) + (( GoB f) * ((i1 + 1),(j2 + 2))))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A152: ( LSeg (((1 / 2) * ((( GoB f) * (i0,j2)) + (( GoB f) * ((i0 + 1),(j2 + 1))))),((1 / 2) * ((( GoB f) * (i1,(j2 + 1))) + (( GoB f) * ((i1 + 1),(j2 + 2))))))) c= ( LeftComp f) by A3, A5, A6, A55, A148, A151, Th4, NAT_1: 13;

                

                 A153: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A150, A152, A20, A27, A28, A30, A145, A146, A149, Th4, A153, GOBOARD6: 82;

              end;

                suppose that

                 A154: (i0 + 1) = i1 and

                 A155: j1 = (j2 + 1) and

                 A156: i1 = ( len ( GoB f)) and

                 A157: j0 = ( width ( GoB f));

                

                 A158: ( left_cell (f,k)) = ( cell (( GoB f),i0,j1)) by A6, A7, A10, A11, A13, A14, A30, A46, A154, GOBOARD5: 28;

                

                 A159: ( LSeg ((((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * (i1,j0)))) + |[ 0 , 1]|),((( GoB f) * (i1,j0)) + |[1, 1]|))) meets ( Int ( cell (( GoB f),i0,j1))) by A18, A21, A30, A154, A157, GOBOARD6: 83;

                ( LSeg ((((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * (i1,j0)))) + |[ 0 , 1]|),((( GoB f) * (i1,j0)) + |[1, 1]|))) misses ( L~ f) by A48, A154, A156, A157, GOBOARD8: 30;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * (i1,j0)))) + |[ 0 , 1]|),((( GoB f) * (i1,j0)) + |[1, 1]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A160: ( LSeg ((((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * (i1,j0)))) + |[ 0 , 1]|),((( GoB f) * (i1,j0)) + |[1, 1]|))) c= ( LeftComp f) by A3, A5, A6, A55, A158, A159, Th4, NAT_1: 13;

                

                 A161: ( Int ( cell (( GoB f),i1,j1))) is convex by A21, A27, Th16;

                ( Int ( cell (( GoB f),i1,j1))) misses ( L~ f) by A21, A27, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),i1,j1))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A162: ( Int ( cell (( GoB f),i1,j1))) c= ( LeftComp f) by A55, A160, A30, A154, A156, A157, Th4, A161, GOBOARD6: 88;

                

                 A163: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i1,j2)) by A4, A5, A13, A14, A16, A17, A31, A45, A155, GOBOARD5: 30;

                

                 A164: ( LSeg ((((1 / 2) * ((( GoB f) * (i1,j2)) + (( GoB f) * (i1,j1)))) + |[1, 0 ]|),((( GoB f) * (i1,j1)) + |[1, 1]|))) meets ( Int ( cell (( GoB f),i1,j1))) by A30, A154, A156, A157, GOBOARD6: 88;

                ( LSeg ((((1 / 2) * ((( GoB f) * (i1,j2)) + (( GoB f) * (i1,j1)))) + |[1, 0 ]|),((( GoB f) * (i1,j1)) + |[1, 1]|))) misses ( L~ f) by A30, A49, A154, A155, A156, A157, GOBOARD8: 36;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (i1,j2)) + (( GoB f) * (i1,j1)))) + |[1, 0 ]|),((( GoB f) * (i1,j1)) + |[1, 1]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A165: ( LSeg ((((1 / 2) * ((( GoB f) * (i1,j2)) + (( GoB f) * (i1,j1)))) + |[1, 0 ]|),((( GoB f) * (i1,j1)) + |[1, 1]|))) c= ( LeftComp f) by A55, A162, A164, Th4;

                

                 A166: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A163, A165, A27, A28, A155, A156, Th4, A166, GOBOARD6: 86;

              end;

                suppose that

                 A167: (i0 + 1) = i1 and

                 A168: j1 = (j2 + 1) and

                 A169: i1 <> ( len ( GoB f)) and

                 A170: j0 = ( width ( GoB f));

                

                 A171: ( left_cell (f,k)) = ( cell (( GoB f),i0,j1)) by A6, A7, A10, A11, A13, A14, A30, A46, A167, GOBOARD5: 28;

                ( len ( GoB f)) > i1 by A21, A169, XXREAL_0: 1;

                then

                 A172: (i1 + 1) <= ( len ( GoB f)) by NAT_1: 13;

                

                 A173: ( LSeg ((((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * ((i0 + 1),j0)))) + |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * ((i0 + 1),j0)) + (( GoB f) * ((i0 + 2),j0)))) + |[ 0 , 1]|))) meets ( Int ( cell (( GoB f),i0,j1))) by A18, A21, A30, A167, A170, GOBOARD6: 83;

                ( LSeg ((((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * ((i0 + 1),j0)))) + |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * ((i0 + 1),j0)) + (( GoB f) * ((i0 + 2),j0)))) + |[ 0 , 1]|))) misses ( L~ f) by A18, A167, A170, A172, GOBOARD8: 28;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * ((i0 + 1),j0)))) + |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * ((i0 + 1),j0)) + (( GoB f) * ((i0 + 2),j0)))) + |[ 0 , 1]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A174: ( LSeg ((((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * ((i0 + 1),j0)))) + |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * ((i0 + 1),j0)) + (( GoB f) * ((i0 + 2),j0)))) + |[ 0 , 1]|))) c= ( LeftComp f) by A3, A5, A6, A55, A171, A173, Th4, NAT_1: 13;

                

                 A175: ( Int ( cell (( GoB f),i1,j1))) is convex by A21, A27, Th16;

                ( Int ( cell (( GoB f),i1,j1))) misses ( L~ f) by A21, A27, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),i1,j1))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A176: ( Int ( cell (( GoB f),i1,j1))) c= ( LeftComp f) by A55, A174, A20, A30, A167, A170, A172, Th4, A175, GOBOARD6: 83;

                

                 A177: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i1,j2)) by A4, A5, A13, A14, A16, A17, A31, A45, A168, GOBOARD5: 30;

                

                 A178: ( LSeg (((1 / 2) * ((( GoB f) * ((i0 + 1),j2)) + (( GoB f) * ((i1 + 1),j0)))),(((1 / 2) * ((( GoB f) * ((i0 + 1),j0)) + (( GoB f) * ((i1 + 1),j0)))) + |[ 0 , 1]|))) meets ( Int ( cell (( GoB f),i1,j1))) by A20, A30, A167, A170, A172, GOBOARD6: 83;

                ( LSeg (((1 / 2) * ((( GoB f) * ((i0 + 1),j2)) + (( GoB f) * ((i1 + 1),j0)))),(((1 / 2) * ((( GoB f) * ((i0 + 1),j0)) + (( GoB f) * ((i1 + 1),j0)))) + |[ 0 , 1]|))) misses ( L~ f) by A5, A6, A11, A14, A17, A18, A30, A31, A49, A50, A51, A167, A168, A170, A172, GOBOARD8: 10;

                then ( LSeg (((1 / 2) * ((( GoB f) * ((i0 + 1),j2)) + (( GoB f) * ((i1 + 1),j0)))),(((1 / 2) * ((( GoB f) * ((i0 + 1),j0)) + (( GoB f) * ((i1 + 1),j0)))) + |[ 0 , 1]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A179: ( LSeg (((1 / 2) * ((( GoB f) * ((i0 + 1),j2)) + (( GoB f) * ((i1 + 1),j0)))),(((1 / 2) * ((( GoB f) * ((i0 + 1),j0)) + (( GoB f) * ((i1 + 1),j0)))) + |[ 0 , 1]|))) c= ( LeftComp f) by A55, A176, A178, Th4;

                

                 A180: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A177, A179, A20, A28, A30, A167, A168, A170, A172, Th4, A180, GOBOARD6: 82;

              end;

                suppose that

                 A181: (i0 + 1) = i1 and

                 A182: j1 = (j2 + 1) and

                 A183: i1 = ( len ( GoB f)) and

                 A184: j0 <> ( width ( GoB f));

                

                 A185: ( left_cell (f,k)) = ( cell (( GoB f),i0,j1)) by A6, A7, A10, A11, A13, A14, A30, A46, A181, GOBOARD5: 28;

                ( width ( GoB f)) > j0 by A25, A184, XXREAL_0: 1;

                then

                 A186: ( width ( GoB f)) >= (j0 + 1) by NAT_1: 13;

                

                 A187: ( LSeg (((1 / 2) * ((( GoB f) * (i0,j1)) + (( GoB f) * (i1,(j1 + 1))))),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i1,(j1 + 1))))) + |[1, 0 ]|))) meets ( Int ( cell (( GoB f),i0,j1))) by A18, A21, A26, A30, A181, A186, GOBOARD6: 82;

                ( LSeg (((1 / 2) * ((( GoB f) * (i0,j1)) + (( GoB f) * (i1,(j1 + 1))))),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i1,(j1 + 1))))) + |[1, 0 ]|))) misses ( L~ f) by A5, A6, A11, A14, A17, A28, A30, A31, A48, A50, A54, A181, A182, A183, A186, GOBOARD8: 20;

                then ( LSeg (((1 / 2) * ((( GoB f) * (i0,j1)) + (( GoB f) * (i1,(j1 + 1))))),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i1,(j1 + 1))))) + |[1, 0 ]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A188: ( LSeg (((1 / 2) * ((( GoB f) * (i0,j1)) + (( GoB f) * (i1,(j1 + 1))))),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i1,(j1 + 1))))) + |[1, 0 ]|))) c= ( LeftComp f) by A3, A5, A6, A55, A185, A187, Th4, NAT_1: 13;

                

                 A189: ( Int ( cell (( GoB f),i1,j1))) is convex by A21, A27, Th16;

                ( Int ( cell (( GoB f),i1,j1))) misses ( L~ f) by A21, A27, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),i1,j1))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A190: ( Int ( cell (( GoB f),i1,j1))) c= ( LeftComp f) by A55, A188, A26, A30, A181, A183, A186, Th4, A189, GOBOARD6: 86;

                

                 A191: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i1,j2)) by A4, A5, A13, A14, A16, A17, A31, A45, A182, GOBOARD5: 30;

                

                 A192: ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),j2)) + (( GoB f) * (( len ( GoB f)),j1)))) + |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),j1)) + (( GoB f) * (( len ( GoB f)),(j1 + 1))))) + |[1, 0 ]|))) meets ( Int ( cell (( GoB f),i1,j1))) by A26, A30, A181, A183, A186, GOBOARD6: 86;

                ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),j2)) + (( GoB f) * (( len ( GoB f)),j1)))) + |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),j1)) + (( GoB f) * (( len ( GoB f)),(j1 + 1))))) + |[1, 0 ]|))) misses ( L~ f) by A28, A30, A54, A181, A182, A186, GOBOARD8: 34;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),j2)) + (( GoB f) * (( len ( GoB f)),j1)))) + |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),j1)) + (( GoB f) * (( len ( GoB f)),(j1 + 1))))) + |[1, 0 ]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A193: ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),j2)) + (( GoB f) * (( len ( GoB f)),j1)))) + |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),j1)) + (( GoB f) * (( len ( GoB f)),(j1 + 1))))) + |[1, 0 ]|))) c= ( LeftComp f) by A55, A190, A192, Th4;

                

                 A194: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A191, A193, A27, A28, A182, A183, Th4, A194, GOBOARD6: 86;

              end;

                suppose that

                 A195: (i0 + 1) = i1 and

                 A196: j1 = (j2 + 1) and

                 A197: i1 <> ( len ( GoB f)) and

                 A198: j0 <> ( width ( GoB f));

                

                 A199: ( left_cell (f,k)) = ( cell (( GoB f),i0,j1)) by A6, A7, A10, A11, A13, A14, A30, A46, A195, GOBOARD5: 28;

                ( len ( GoB f)) > i1 by A21, A197, XXREAL_0: 1;

                then

                 A200: (i1 + 1) <= ( len ( GoB f)) by NAT_1: 13;

                ( width ( GoB f)) > j0 by A25, A198, XXREAL_0: 1;

                then

                 A201: ( width ( GoB f)) >= (j0 + 1) by NAT_1: 13;

                

                 A202: ( LSeg (((1 / 2) * ((( GoB f) * (i0,(j2 + 1))) + (( GoB f) * ((i0 + 1),(j1 + 1))))),((1 / 2) * ((( GoB f) * ((i0 + 1),(j2 + 1))) + (( GoB f) * ((i1 + 1),(j1 + 1))))))) meets ( Int ( cell (( GoB f),i0,j1))) by A18, A21, A26, A30, A195, A196, A201, GOBOARD6: 82;

                ( LSeg (((1 / 2) * ((( GoB f) * (i0,(j2 + 1))) + (( GoB f) * ((i0 + 1),(j1 + 1))))),((1 / 2) * ((( GoB f) * ((i0 + 1),(j2 + 1))) + (( GoB f) * ((i1 + 1),(j1 + 1))))))) misses ( L~ f) by A5, A6, A11, A14, A17, A18, A28, A30, A31, A50, A51, A54, A195, A196, A200, A201, GOBOARD8: 16;

                then ( LSeg (((1 / 2) * ((( GoB f) * (i0,(j2 + 1))) + (( GoB f) * ((i0 + 1),(j1 + 1))))),((1 / 2) * ((( GoB f) * ((i0 + 1),(j2 + 1))) + (( GoB f) * ((i1 + 1),(j1 + 1))))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A203: ( LSeg (((1 / 2) * ((( GoB f) * (i0,(j2 + 1))) + (( GoB f) * ((i0 + 1),(j1 + 1))))),((1 / 2) * ((( GoB f) * ((i0 + 1),(j2 + 1))) + (( GoB f) * ((i1 + 1),(j1 + 1))))))) c= ( LeftComp f) by A3, A5, A6, A55, A199, A202, Th4, NAT_1: 13;

                

                 A204: ( Int ( cell (( GoB f),i1,j1))) is convex by A21, A27, Th16;

                ( Int ( cell (( GoB f),i1,j1))) misses ( L~ f) by A21, A27, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),i1,j1))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A205: ( Int ( cell (( GoB f),i1,j1))) c= ( LeftComp f) by A55, A203, A20, A26, A30, A195, A196, A200, A201, Th4, A204, GOBOARD6: 82;

                

                 A206: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i1,j2)) by A4, A5, A13, A14, A16, A17, A31, A45, A196, GOBOARD5: 30;

                

                 A207: ( LSeg (((1 / 2) * ((( GoB f) * ((i0 + 1),j2)) + (( GoB f) * ((i1 + 1),(j2 + 1))))),((1 / 2) * ((( GoB f) * ((i0 + 1),(j2 + 1))) + (( GoB f) * ((i1 + 1),(j1 + 1))))))) meets ( Int ( cell (( GoB f),i1,j1))) by A20, A26, A30, A195, A196, A200, A201, GOBOARD6: 82;

                ( LSeg (((1 / 2) * ((( GoB f) * ((i0 + 1),j2)) + (( GoB f) * ((i1 + 1),(j2 + 1))))),((1 / 2) * ((( GoB f) * ((i0 + 1),(j2 + 1))) + (( GoB f) * ((i1 + 1),(j1 + 1))))))) misses ( L~ f) by A5, A6, A11, A14, A17, A18, A28, A30, A31, A50, A51, A54, A195, A196, A200, A201, GOBOARD8: 6;

                then ( LSeg (((1 / 2) * ((( GoB f) * ((i0 + 1),j2)) + (( GoB f) * ((i1 + 1),(j2 + 1))))),((1 / 2) * ((( GoB f) * ((i0 + 1),(j2 + 1))) + (( GoB f) * ((i1 + 1),(j1 + 1))))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A208: ( LSeg (((1 / 2) * ((( GoB f) * ((i0 + 1),j2)) + (( GoB f) * ((i1 + 1),(j2 + 1))))),((1 / 2) * ((( GoB f) * ((i0 + 1),(j2 + 1))) + (( GoB f) * ((i1 + 1),(j1 + 1))))))) c= ( LeftComp f) by A55, A205, A207, Th4;

                

                 A209: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A206, A208, A20, A27, A28, A195, A196, A200, Th4, A209, GOBOARD6: 82;

              end;

                suppose that

                 A210: (j0 + 1) = j1 and

                 A211: i1 = (i2 + 1);

                ( left_cell (f,k)) = ( cell (( GoB f),i2,j0)) by A6, A7, A10, A11, A13, A14, A30, A210, A211, GOBOARD5: 27

                .= ( left_cell (f,(k + 1))) by A4, A5, A13, A14, A16, A17, A31, A210, A211, GOBOARD5: 29;

                hence thesis by A3, A5, A6, NAT_1: 13;

              end;

                suppose that

                 A212: i0 = (i1 + 1) and

                 A213: (j1 + 1) = j2 and

                 A214: i1 = 1 and

                 A215: j1 = 1;

                

                 A216: ( left_cell (f,k)) = ( cell (( GoB f),i1,(j1 -' 1))) by A6, A7, A10, A11, A13, A14, A30, A46, A212, GOBOARD5: 29;

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

                then

                 A217: (i1 -' 1) <= ( len ( GoB f)) by A21, XXREAL_0: 2;

                

                 A218: (j1 -' 1) = 0 by A215, XREAL_1: 232;

                

                 A219: (i1 -' 1) = 0 by A214, XREAL_1: 232;

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

                then

                 A220: (j1 -' 1) <= ( width ( GoB f)) by A27, XXREAL_0: 2;

                

                 A221: ( LSeg (((( GoB f) * (i1,j1)) - |[1, 1]|),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i0,j1)))) - |[ 0 , 1]|))) meets ( Int ( cell (( GoB f),i1,(j1 -' 1)))) by A19, A20, A212, A215, A218, GOBOARD6: 84;

                ( LSeg (((( GoB f) * (i1,j1)) - |[1, 1]|),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i0,j1)))) - |[ 0 , 1]|))) misses ( L~ f) by A212, A214, A215, GOBOARD8: 26;

                then ( LSeg (((( GoB f) * (i1,j1)) - |[1, 1]|),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i0,j1)))) - |[ 0 , 1]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A222: ( LSeg (((( GoB f) * (i1,j1)) - |[1, 1]|),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i0,j1)))) - |[ 0 , 1]|))) c= ( LeftComp f) by A3, A5, A6, A55, A216, A221, Th4, NAT_1: 13;

                

                 A223: ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) is convex by A217, A220, Th16;

                ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) misses ( L~ f) by A217, A220, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A224: ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) c= ( LeftComp f) by A55, A222, A214, A215, A218, Th4, A223, GOBOARD6: 87;

                

                 A225: ( left_cell (f,(k + 1))) = ( cell (( GoB f),(i1 -' 1),j1)) by A4, A5, A13, A14, A16, A17, A31, A45, A213, GOBOARD5: 27;

                

                 A226: ( LSeg (((( GoB f) * (i1,j1)) - |[1, 1]|),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i1,j2)))) - |[1, 0 ]|))) meets ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) by A214, A215, A218, GOBOARD6: 87;

                ( LSeg (((( GoB f) * (i1,j1)) - |[1, 1]|),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i1,j2)))) - |[1, 0 ]|))) misses ( L~ f) by A213, A214, A215, GOBOARD8: 32;

                then ( LSeg (((( GoB f) * (i1,j1)) - |[1, 1]|),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i1,j2)))) - |[1, 0 ]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A227: ( LSeg (((( GoB f) * (i1,j1)) - |[1, 1]|),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i1,j2)))) - |[1, 0 ]|))) c= ( LeftComp f) by A55, A224, A226, Th4;

                

                 A228: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A225, A227, A26, A29, A213, A214, A219, Th4, A228, GOBOARD6: 85;

              end;

                suppose that

                 A229: i0 = (i1 + 1) and

                 A230: (j1 + 1) = j2 and

                 A231: i1 <> 1 and

                 A232: j1 = 1;

                

                 A233: ( left_cell (f,k)) = ( cell (( GoB f),i1,(j1 -' 1))) by A6, A7, A10, A11, A13, A14, A30, A46, A229, GOBOARD5: 29;

                1 < i1 by A20, A231, XXREAL_0: 1;

                then

                 A234: 1 <= (i1 -' 1) by A45, NAT_1: 13;

                

                 A235: ((i1 -' 1) + (1 + 1)) = i0 by A45, A229;

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

                then

                 A236: (i1 -' 1) <= ( len ( GoB f)) by A21, XXREAL_0: 2;

                

                 A237: (j1 -' 1) = 0 by A232, XREAL_1: 232;

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

                then

                 A238: (j1 -' 1) <= ( width ( GoB f)) by A27, XXREAL_0: 2;

                

                 A239: ( LSeg ((((1 / 2) * ((( GoB f) * ((i1 -' 1),1)) + (( GoB f) * (i1,1)))) - |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i1,1)) + (( GoB f) * (i0,1)))) - |[ 0 , 1]|))) meets ( Int ( cell (( GoB f),i1,(j1 -' 1)))) by A19, A20, A229, A237, GOBOARD6: 84;

                ( LSeg ((((1 / 2) * ((( GoB f) * ((i1 -' 1),1)) + (( GoB f) * (i1,1)))) - |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i1,1)) + (( GoB f) * (i0,1)))) - |[ 0 , 1]|))) misses ( L~ f) by A19, A45, A234, A235, GOBOARD8: 25;

                then ( LSeg ((((1 / 2) * ((( GoB f) * ((i1 -' 1),1)) + (( GoB f) * (i1,1)))) - |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i1,1)) + (( GoB f) * (i0,1)))) - |[ 0 , 1]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A240: ( LSeg ((((1 / 2) * ((( GoB f) * ((i1 -' 1),1)) + (( GoB f) * (i1,1)))) - |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i1,1)) + (( GoB f) * (i0,1)))) - |[ 0 , 1]|))) c= ( LeftComp f) by A3, A5, A6, A55, A233, A239, Th4, NAT_1: 13;

                

                 A241: ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) is convex by A236, A238, Th16;

                ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) misses ( L~ f) by A236, A238, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A242: ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) c= ( LeftComp f) by A55, A240, A21, A45, A234, A237, Th4, A241, GOBOARD6: 84;

                

                 A243: ( left_cell (f,(k + 1))) = ( cell (( GoB f),(i1 -' 1),j1)) by A4, A5, A13, A14, A16, A17, A31, A45, A230, GOBOARD5: 27;

                

                 A244: ( LSeg ((((1 / 2) * ((( GoB f) * ((i1 -' 1),1)) + (( GoB f) * (i1,1)))) - |[ 0 , 1]|),((1 / 2) * ((( GoB f) * ((i1 -' 1),1)) + (( GoB f) * (i1,2)))))) meets ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) by A21, A45, A234, A237, GOBOARD6: 84;

                ( LSeg ((((1 / 2) * ((( GoB f) * ((i1 -' 1),1)) + (( GoB f) * (i1,1)))) - |[ 0 , 1]|),((1 / 2) * ((( GoB f) * ((i1 -' 1),1)) + (( GoB f) * (i1,2)))))) misses ( L~ f) by A5, A6, A11, A14, A17, A19, A30, A31, A45, A50, A230, A232, A234, A235, GOBOARD8: 7;

                then ( LSeg ((((1 / 2) * ((( GoB f) * ((i1 -' 1),1)) + (( GoB f) * (i1,1)))) - |[ 0 , 1]|),((1 / 2) * ((( GoB f) * ((i1 -' 1),1)) + (( GoB f) * (i1,2)))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A245: ( LSeg ((((1 / 2) * ((( GoB f) * ((i1 -' 1),1)) + (( GoB f) * (i1,1)))) - |[ 0 , 1]|),((1 / 2) * ((( GoB f) * ((i1 -' 1),1)) + (( GoB f) * (i1,2)))))) c= ( LeftComp f) by A55, A242, A244, Th4;

                

                 A246: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A243, A245, A21, A29, A45, A230, A232, A234, Th4, A246, GOBOARD6: 82;

              end;

                suppose that

                 A247: i0 = (i1 + 1) and

                 A248: (j1 + 1) = j2 and

                 A249: i1 = 1 and

                 A250: j1 <> 1;

                

                 A251: ( left_cell (f,k)) = ( cell (( GoB f),i1,(j1 -' 1))) by A6, A7, A10, A11, A13, A14, A30, A46, A247, GOBOARD5: 29;

                1 < j0 by A24, A30, A247, A250, XXREAL_0: 1;

                then

                 A252: 1 <= (j0 -' 1) by A30, A46, A247, NAT_1: 13;

                

                 A253: ((j0 -' 1) + (1 + 1)) = j2 by A30, A46, A247, A248;

                

                 A254: ( LSeg ((((1 / 2) * ((( GoB f) * (1,(j1 -' 1))) + (( GoB f) * (1,((j1 -' 1) + 1))))) - |[1, 0 ]|),((1 / 2) * ((( GoB f) * (1,(j1 -' 1))) + (( GoB f) * (2,((j1 -' 1) + 1))))))) meets ( Int ( cell (( GoB f),i1,(j1 -' 1)))) by A19, A27, A30, A46, A247, A249, A252, GOBOARD6: 82;

                ( LSeg ((((1 / 2) * ((( GoB f) * (1,(j1 -' 1))) + (( GoB f) * (1,((j1 -' 1) + 1))))) - |[1, 0 ]|),((1 / 2) * ((( GoB f) * (1,(j1 -' 1))) + (( GoB f) * (2,((j1 -' 1) + 1))))))) misses ( L~ f) by A5, A6, A11, A14, A17, A29, A30, A31, A46, A50, A247, A248, A249, A252, A253, GOBOARD8: 17;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (1,(j1 -' 1))) + (( GoB f) * (1,((j1 -' 1) + 1))))) - |[1, 0 ]|),((1 / 2) * ((( GoB f) * (1,(j1 -' 1))) + (( GoB f) * (2,((j1 -' 1) + 1))))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A255: ( LSeg ((((1 / 2) * ((( GoB f) * (1,(j1 -' 1))) + (( GoB f) * (1,((j1 -' 1) + 1))))) - |[1, 0 ]|),((1 / 2) * ((( GoB f) * (1,(j1 -' 1))) + (( GoB f) * (2,((j1 -' 1) + 1))))))) c= ( LeftComp f) by A3, A5, A6, A55, A251, A254, Th4, NAT_1: 13;

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

                then

                 A256: (i1 -' 1) <= ( len ( GoB f)) by A21, XXREAL_0: 2;

                

                 A257: (i1 -' 1) = 0 by A249, XREAL_1: 232;

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

                then

                 A258: (j1 -' 1) <= ( width ( GoB f)) by A27, XXREAL_0: 2;

                

                 A259: ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) is convex by A256, A258, Th16;

                ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) misses ( L~ f) by A256, A258, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A260: ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) c= ( LeftComp f) by A30, A55, A247, A255, A27, A46, A252, A257, Th4, A259, GOBOARD6: 85;

                

                 A261: ( left_cell (f,(k + 1))) = ( cell (( GoB f),(i1 -' 1),j1)) by A4, A5, A13, A14, A16, A17, A31, A45, A248, GOBOARD5: 27;

                

                 A262: ( LSeg ((((1 / 2) * ((( GoB f) * (1,(j1 -' 1))) + (( GoB f) * (1,((j1 -' 1) + 1))))) - |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (1,((j1 -' 1) + 1))) + (( GoB f) * (1,((j1 -' 1) + 2))))) - |[1, 0 ]|))) meets ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) by A27, A30, A46, A247, A252, A257, GOBOARD6: 85;

                ( LSeg ((((1 / 2) * ((( GoB f) * (1,(j1 -' 1))) + (( GoB f) * (1,((j1 -' 1) + 1))))) - |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (1,((j1 -' 1) + 1))) + (( GoB f) * (1,((j1 -' 1) + 2))))) - |[1, 0 ]|))) misses ( L~ f) by A29, A30, A46, A247, A248, A252, GOBOARD8: 31;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (1,(j1 -' 1))) + (( GoB f) * (1,((j1 -' 1) + 1))))) - |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (1,((j1 -' 1) + 1))) + (( GoB f) * (1,((j1 -' 1) + 2))))) - |[1, 0 ]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A263: ( LSeg ((((1 / 2) * ((( GoB f) * (1,(j1 -' 1))) + (( GoB f) * (1,((j1 -' 1) + 1))))) - |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (1,((j1 -' 1) + 1))) + (( GoB f) * (1,((j1 -' 1) + 2))))) - |[1, 0 ]|))) c= ( LeftComp f) by A55, A260, A262, Th4;

                

                 A264: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A261, A263, A26, A29, A46, A248, A257, Th4, A264, GOBOARD6: 85;

              end;

                suppose that

                 A265: i0 = (i1 + 1) and

                 A266: (j1 + 1) = j2 and

                 A267: i1 <> 1 and

                 A268: j1 <> 1;

                

                 A269: ( left_cell (f,k)) = ( cell (( GoB f),i1,(j1 -' 1))) by A6, A7, A10, A11, A13, A14, A30, A46, A265, GOBOARD5: 29;

                1 < j0 by A24, A30, A265, A268, XXREAL_0: 1;

                then

                 A270: 1 <= (j0 -' 1) by A30, A46, A265, NAT_1: 13;

                1 < i1 by A20, A267, XXREAL_0: 1;

                then

                 A271: 1 <= (i1 -' 1) by A45, NAT_1: 13;

                

                 A272: ((i1 -' 1) + (1 + 1)) = i0 by A45, A265;

                

                 A273: ((j0 -' 1) + (1 + 1)) = j2 by A30, A46, A265, A266;

                

                 A274: ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),(j0 -' 1))) + (( GoB f) * (i1,j1)))),((1 / 2) * ((( GoB f) * (i1,(j0 -' 1))) + (( GoB f) * (i0,j1)))))) meets ( Int ( cell (( GoB f),i1,(j1 -' 1)))) by A19, A20, A27, A30, A46, A265, A270, GOBOARD6: 82;

                ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),(j0 -' 1))) + (( GoB f) * (i1,j1)))),((1 / 2) * ((( GoB f) * (i1,(j0 -' 1))) + (( GoB f) * (i0,j1)))))) misses ( L~ f) by A5, A6, A11, A14, A17, A19, A29, A30, A31, A45, A46, A50, A266, A270, A271, A272, A273, GOBOARD8: 12;

                then ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),(j0 -' 1))) + (( GoB f) * (i1,j1)))),((1 / 2) * ((( GoB f) * (i1,(j0 -' 1))) + (( GoB f) * (i0,j1)))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A275: ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),(j0 -' 1))) + (( GoB f) * (i1,j1)))),((1 / 2) * ((( GoB f) * (i1,(j0 -' 1))) + (( GoB f) * (i0,j1)))))) c= ( LeftComp f) by A3, A5, A6, A55, A269, A274, Th4, NAT_1: 13;

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

                then

                 A276: (i1 -' 1) <= ( len ( GoB f)) by A21, XXREAL_0: 2;

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

                then

                 A277: (j1 -' 1) <= ( width ( GoB f)) by A27, XXREAL_0: 2;

                

                 A278: ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) is convex by A276, A277, Th16;

                ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) misses ( L~ f) by A276, A277, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A279: ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) c= ( LeftComp f) by A30, A55, A265, A275, A21, A27, A45, A46, A270, A271, Th4, A278, GOBOARD6: 82;

                

                 A280: ( left_cell (f,(k + 1))) = ( cell (( GoB f),(i1 -' 1),j1)) by A4, A5, A13, A14, A16, A17, A31, A45, A266, GOBOARD5: 27;

                

                 A281: ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),(j1 -' 1))) + (( GoB f) * (i1,j1)))),((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,j2)))))) meets ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) by A21, A27, A30, A45, A46, A265, A270, A271, GOBOARD6: 82;

                ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),(j1 -' 1))) + (( GoB f) * (i1,j1)))),((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,j2)))))) misses ( L~ f) by A5, A6, A11, A14, A17, A19, A29, A30, A31, A45, A46, A50, A266, A270, A271, A272, A273, GOBOARD8: 2;

                then ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),(j1 -' 1))) + (( GoB f) * (i1,j1)))),((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,j2)))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A282: ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),(j1 -' 1))) + (( GoB f) * (i1,j1)))),((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,j2)))))) c= ( LeftComp f) by A55, A279, A281, Th4;

                

                 A283: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A280, A282, A21, A26, A29, A45, A266, A271, Th4, A283, GOBOARD6: 82;

              end;

                suppose that

                 A284: j0 = (j1 + 1) and

                 A285: (i1 + 1) = i2;

                ( left_cell (f,k)) = ( cell (( GoB f),i0,j1)) by A6, A7, A10, A11, A13, A14, A30, A45, A284, GOBOARD5: 30

                .= ( left_cell (f,(k + 1))) by A4, A5, A13, A14, A16, A17, A30, A31, A46, A284, A285, GOBOARD5: 28;

                hence thesis by A3, A5, A6, NAT_1: 13;

              end;

                suppose that

                 A286: (i0 + 1) = i1 and

                 A287: (i1 + 1) = i2 and

                 A288: j0 = ( width ( GoB f));

                

                 A289: ( left_cell (f,k)) = ( cell (( GoB f),i0,( width ( GoB f)))) by A6, A7, A10, A11, A13, A14, A30, A49, A286, A288, GOBOARD5: 28;

                

                 A290: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i1,( width ( GoB f)))) by A4, A5, A13, A14, A16, A17, A30, A31, A49, A286, A287, A288, GOBOARD5: 28;

                

                 A291: ( LSeg ((((1 / 2) * ((( GoB f) * (i0,( width ( GoB f)))) + (( GoB f) * ((i0 + 1),( width ( GoB f)))))) + |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i1,( width ( GoB f)))) + (( GoB f) * ((i1 + 1),( width ( GoB f)))))) + |[ 0 , 1]|))) meets ( Int ( cell (( GoB f),i0,( width ( GoB f))))) by A18, A21, A286, GOBOARD6: 83;

                ( LSeg ((((1 / 2) * ((( GoB f) * (i0,( width ( GoB f)))) + (( GoB f) * ((i0 + 1),( width ( GoB f)))))) + |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i1,( width ( GoB f)))) + (( GoB f) * ((i1 + 1),( width ( GoB f)))))) + |[ 0 , 1]|))) misses ( L~ f) by A18, A23, A51, A286, A287, GOBOARD8: 28;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (i0,( width ( GoB f)))) + (( GoB f) * ((i0 + 1),( width ( GoB f)))))) + |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i1,( width ( GoB f)))) + (( GoB f) * ((i1 + 1),( width ( GoB f)))))) + |[ 0 , 1]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A292: ( LSeg ((((1 / 2) * ((( GoB f) * (i0,( width ( GoB f)))) + (( GoB f) * ((i0 + 1),( width ( GoB f)))))) + |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i1,( width ( GoB f)))) + (( GoB f) * ((i1 + 1),( width ( GoB f)))))) + |[ 0 , 1]|))) c= ( LeftComp f) by A3, A5, A6, A55, A289, A291, Th4, NAT_1: 13;

                

                 A293: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A290, A292, A20, A23, A287, Th4, A293, GOBOARD6: 83;

              end;

                suppose that

                 A294: (i0 + 1) = i1 and

                 A295: (i1 + 1) = i2 and

                 A296: j0 <> ( width ( GoB f));

                

                 A297: ( left_cell (f,k)) = ( cell (( GoB f),i0,j1)) by A6, A7, A10, A11, A13, A14, A30, A46, A294, GOBOARD5: 28;

                ( width ( GoB f)) > j0 by A25, A296, XXREAL_0: 1;

                then

                 A298: ( width ( GoB f)) >= (j0 + 1) by NAT_1: 13;

                

                 A299: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i1,j1)) by A4, A5, A13, A14, A16, A17, A31, A46, A295, GOBOARD5: 28;

                

                 A300: ( LSeg (((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * ((i0 + 1),(j0 + 1))))),((1 / 2) * ((( GoB f) * (i1,j0)) + (( GoB f) * ((i1 + 1),(j0 + 1))))))) meets ( Int ( cell (( GoB f),i0,j1))) by A18, A21, A26, A30, A294, A298, GOBOARD6: 82;

                ( LSeg (((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * ((i0 + 1),(j0 + 1))))),((1 / 2) * ((( GoB f) * (i1,j0)) + (( GoB f) * ((i1 + 1),(j0 + 1))))))) misses ( L~ f) by A5, A6, A11, A14, A17, A18, A23, A24, A30, A31, A50, A51, A294, A295, A298, GOBOARD8: 14;

                then ( LSeg (((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * ((i0 + 1),(j0 + 1))))),((1 / 2) * ((( GoB f) * (i1,j0)) + (( GoB f) * ((i1 + 1),(j0 + 1))))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A301: ( LSeg (((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * ((i0 + 1),(j0 + 1))))),((1 / 2) * ((( GoB f) * (i1,j0)) + (( GoB f) * ((i1 + 1),(j0 + 1))))))) c= ( LeftComp f) by A3, A5, A6, A55, A297, A300, Th4, NAT_1: 13;

                

                 A302: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A299, A301, A20, A23, A24, A30, A294, A295, A298, Th4, A302, GOBOARD6: 82;

              end;

                suppose that

                 A303: (i0 + 1) = i1 and

                 A304: (j1 + 1) = j2;

                ( left_cell (f,k)) = ( cell (( GoB f),i0,j1)) by A6, A7, A10, A11, A13, A14, A30, A46, A303, GOBOARD5: 28

                .= ( left_cell (f,(k + 1))) by A4, A5, A13, A14, A16, A17, A31, A303, A304, GOBOARD5: 27;

                hence thesis by A3, A5, A6, NAT_1: 13;

              end;

                suppose that

                 A305: (j0 + 1) = j1 and

                 A306: (i1 + 1) = i2 and

                 A307: i0 = 1 and

                 A308: j1 = ( width ( GoB f));

                

                 A309: ( left_cell (f,k)) = ( cell (( GoB f),(i1 -' 1),j0)) by A6, A7, A10, A11, A13, A14, A30, A45, A305, GOBOARD5: 27;

                

                 A310: (i0 -' 1) = 0 by A307, XREAL_1: 232;

                

                 A311: (j1 -' 1) = j0 by A305, NAT_D: 34;

                

                 A312: ( LSeg ((((1 / 2) * ((( GoB f) * (1,j0)) + (( GoB f) * (1,j1)))) - |[1, 0 ]|),((( GoB f) * (1,j1)) + |[( - 1), 1]|))) meets ( Int ( cell (( GoB f),(i1 -' 1),j0))) by A24, A27, A30, A305, A310, GOBOARD6: 85;

                ( LSeg ((((1 / 2) * ((( GoB f) * (1,j0)) + (( GoB f) * (1,j1)))) - |[1, 0 ]|),((( GoB f) * (1,j1)) + |[( - 1), 1]|))) misses ( L~ f) by A308, A311, GOBOARD8: 33;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (1,j0)) + (( GoB f) * (1,j1)))) - |[1, 0 ]|),((( GoB f) * (1,j1)) + |[( - 1), 1]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A313: ( LSeg ((((1 / 2) * ((( GoB f) * (1,j0)) + (( GoB f) * (1,j1)))) - |[1, 0 ]|),((( GoB f) * (1,j1)) + |[( - 1), 1]|))) c= ( LeftComp f) by A3, A5, A6, A55, A309, A312, Th4, NAT_1: 13;

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

                then

                 A314: (i1 -' 1) <= ( len ( GoB f)) by A21, XXREAL_0: 2;

                

                 A315: ( Int ( cell (( GoB f),(i1 -' 1),j1))) is convex by A27, A314, Th16;

                ( Int ( cell (( GoB f),(i1 -' 1),j1))) misses ( L~ f) by A27, A314, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),(i1 -' 1),j1))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A316: ( Int ( cell (( GoB f),(i1 -' 1),j1))) c= ( LeftComp f) by A30, A55, A305, A313, A308, A310, Th4, A315, GOBOARD6: 89;

                

                 A317: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i1,j1)) by A4, A5, A13, A14, A16, A17, A31, A305, A306, GOBOARD5: 28;

                

                 A318: ( LSeg (((( GoB f) * (1,j1)) + |[( - 1), 1]|),(((1 / 2) * ((( GoB f) * (1,j1)) + (( GoB f) * (2,j1)))) + |[ 0 , 1]|))) meets ( Int ( cell (( GoB f),(i1 -' 1),j1))) by A30, A305, A308, A310, GOBOARD6: 89;

                ( LSeg (((( GoB f) * (1,j1)) + |[( - 1), 1]|),(((1 / 2) * ((( GoB f) * (1,j1)) + (( GoB f) * (2,j1)))) + |[ 0 , 1]|))) misses ( L~ f) by A308, GOBOARD8: 29;

                then ( LSeg (((( GoB f) * (1,j1)) + |[( - 1), 1]|),(((1 / 2) * ((( GoB f) * (1,j1)) + (( GoB f) * (2,j1)))) + |[ 0 , 1]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A319: ( LSeg (((( GoB f) * (1,j1)) + |[( - 1), 1]|),(((1 / 2) * ((( GoB f) * (1,j1)) + (( GoB f) * (2,j1)))) + |[ 0 , 1]|))) c= ( LeftComp f) by A55, A316, A318, Th4;

                

                 A320: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A317, A319, A23, A30, A305, A306, A307, A308, Th4, A320, GOBOARD6: 83;

              end;

                suppose that

                 A321: (j0 + 1) = j1 and

                 A322: (i1 + 1) = i2 and

                 A323: i0 <> 1 and

                 A324: j1 = ( width ( GoB f));

                

                 A325: ( left_cell (f,k)) = ( cell (( GoB f),(i1 -' 1),j0)) by A6, A7, A10, A11, A13, A14, A30, A45, A321, GOBOARD5: 27;

                1 < i0 by A18, A323, XXREAL_0: 1;

                then

                 A326: 1 <= (i0 -' 1) by A30, A45, A321, NAT_1: 13;

                

                 A327: (j1 -' 1) = j0 by A321, NAT_D: 34;

                

                 A328: ((i1 -' 1) + (1 + 1)) = i2 by A45, A322;

                

                 A329: ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),j0)) + (( GoB f) * (i1,j1)))),(((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,j1)))) + |[ 0 , 1]|))) meets ( Int ( cell (( GoB f),(i1 -' 1),j0))) by A21, A24, A27, A30, A45, A321, A326, GOBOARD6: 82;

                ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),j0)) + (( GoB f) * (i1,j1)))),(((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,j1)))) + |[ 0 , 1]|))) misses ( L~ f) by A5, A6, A11, A14, A17, A23, A30, A31, A45, A50, A321, A324, A326, A327, A328, GOBOARD8: 9;

                then ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),j0)) + (( GoB f) * (i1,j1)))),(((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,j1)))) + |[ 0 , 1]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A330: ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),j0)) + (( GoB f) * (i1,j1)))),(((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,j1)))) + |[ 0 , 1]|))) c= ( LeftComp f) by A3, A5, A6, A55, A325, A329, Th4, NAT_1: 13;

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

                then

                 A331: (i1 -' 1) <= ( len ( GoB f)) by A21, XXREAL_0: 2;

                

                 A332: ( Int ( cell (( GoB f),(i1 -' 1),j1))) is convex by A27, A331, Th16;

                ( Int ( cell (( GoB f),(i1 -' 1),j1))) misses ( L~ f) by A27, A331, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),(i1 -' 1),j1))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A333: ( Int ( cell (( GoB f),(i1 -' 1),j1))) c= ( LeftComp f) by A30, A55, A321, A330, A19, A45, A324, A326, Th4, A332, GOBOARD6: 83;

                

                 A334: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i1,j1)) by A4, A5, A13, A14, A16, A17, A31, A321, A322, GOBOARD5: 28;

                

                 A335: ( LSeg ((((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,j1)))) + |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i2,j1)))) + |[ 0 , 1]|))) meets ( Int ( cell (( GoB f),(i1 -' 1),j1))) by A21, A30, A45, A321, A324, A326, GOBOARD6: 83;

                ( LSeg ((((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,j1)))) + |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i2,j1)))) + |[ 0 , 1]|))) misses ( L~ f) by A23, A30, A45, A321, A324, A326, A328, GOBOARD8: 28;

                then ( LSeg ((((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,j1)))) + |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i2,j1)))) + |[ 0 , 1]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A336: ( LSeg ((((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,j1)))) + |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i2,j1)))) + |[ 0 , 1]|))) c= ( LeftComp f) by A55, A333, A335, Th4;

                

                 A337: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A334, A336, A20, A23, A322, A324, Th4, A337, GOBOARD6: 83;

              end;

                suppose that

                 A338: (j0 + 1) = j1 and

                 A339: (i1 + 1) = i2 and

                 A340: i0 = 1 and

                 A341: j1 <> ( width ( GoB f));

                

                 A342: ( left_cell (f,k)) = ( cell (( GoB f),(i1 -' 1),j0)) by A6, A7, A10, A11, A13, A14, A30, A45, A338, GOBOARD5: 27;

                ( width ( GoB f)) > j1 by A27, A341, XXREAL_0: 1;

                then

                 A343: ( width ( GoB f)) >= (j1 + 1) by NAT_1: 13;

                

                 A344: (i0 -' 1) = 0 by A340, XREAL_1: 232;

                

                 A345: ( LSeg ((((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * (i0,j1)))) - |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (i0,j1)) + (( GoB f) * (i0,(j1 + 1))))) - |[1, 0 ]|))) meets ( Int ( cell (( GoB f),(i1 -' 1),j0))) by A24, A27, A30, A338, A340, A344, GOBOARD6: 85;

                ( LSeg ((((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * (i0,j1)))) - |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (i0,j1)) + (( GoB f) * (i0,(j1 + 1))))) - |[1, 0 ]|))) misses ( L~ f) by A24, A53, A338, A340, A343, GOBOARD8: 31;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * (i0,j1)))) - |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (i0,j1)) + (( GoB f) * (i0,(j1 + 1))))) - |[1, 0 ]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A346: ( LSeg ((((1 / 2) * ((( GoB f) * (i0,j0)) + (( GoB f) * (i0,j1)))) - |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (i0,j1)) + (( GoB f) * (i0,(j1 + 1))))) - |[1, 0 ]|))) c= ( LeftComp f) by A3, A5, A6, A55, A342, A345, Th4, NAT_1: 13;

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

                then

                 A347: (i1 -' 1) <= ( len ( GoB f)) by A21, XXREAL_0: 2;

                

                 A348: ( Int ( cell (( GoB f),(i1 -' 1),j1))) is convex by A27, A347, Th16;

                ( Int ( cell (( GoB f),(i1 -' 1),j1))) misses ( L~ f) by A27, A347, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),(i1 -' 1),j1))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A349: ( Int ( cell (( GoB f),(i1 -' 1),j1))) c= ( LeftComp f) by A30, A55, A338, A346, A26, A340, A343, A344, Th4, A348, GOBOARD6: 85;

                

                 A350: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i1,j1)) by A4, A5, A13, A14, A16, A17, A31, A338, A339, GOBOARD5: 28;

                

                 A351: ( LSeg ((((1 / 2) * ((( GoB f) * (i1,(j0 + 1))) + (( GoB f) * (i1,(j0 + 2))))) - |[1, 0 ]|),((1 / 2) * ((( GoB f) * (i1,(j0 + 1))) + (( GoB f) * (i2,(j0 + 2))))))) meets ( Int ( cell (( GoB f),(i1 -' 1),j1))) by A26, A30, A338, A340, A343, A344, GOBOARD6: 85;

                ( LSeg ((((1 / 2) * ((( GoB f) * (i1,(j0 + 1))) + (( GoB f) * (i1,(j0 + 2))))) - |[1, 0 ]|),((1 / 2) * ((( GoB f) * (i1,(j0 + 1))) + (( GoB f) * (i2,(j0 + 2))))))) misses ( L~ f) by A5, A6, A11, A14, A17, A24, A30, A31, A50, A338, A339, A340, A343, GOBOARD8: 18;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (i1,(j0 + 1))) + (( GoB f) * (i1,(j0 + 2))))) - |[1, 0 ]|),((1 / 2) * ((( GoB f) * (i1,(j0 + 1))) + (( GoB f) * (i2,(j0 + 2))))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A352: ( LSeg ((((1 / 2) * ((( GoB f) * (i1,(j0 + 1))) + (( GoB f) * (i1,(j0 + 2))))) - |[1, 0 ]|),((1 / 2) * ((( GoB f) * (i1,(j0 + 1))) + (( GoB f) * (i2,(j0 + 2))))))) c= ( LeftComp f) by A55, A349, A351, Th4;

                

                 A353: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A350, A352, A20, A23, A26, A338, A339, A343, Th4, A353, GOBOARD6: 82;

              end;

                suppose that

                 A354: (j0 + 1) = j1 and

                 A355: (i1 + 1) = i2 and

                 A356: i0 <> 1 and

                 A357: j1 <> ( width ( GoB f));

                

                 A358: ( left_cell (f,k)) = ( cell (( GoB f),(i1 -' 1),j0)) by A6, A7, A10, A11, A13, A14, A30, A45, A354, GOBOARD5: 27;

                1 < i0 by A18, A356, XXREAL_0: 1;

                then

                 A359: 1 <= (i0 -' 1) by A30, A45, A354, NAT_1: 13;

                ( width ( GoB f)) > j1 by A27, A357, XXREAL_0: 1;

                then

                 A360: ( width ( GoB f)) >= (j1 + 1) by NAT_1: 13;

                

                 A361: ((i1 -' 1) + (1 + 1)) = i2 by A45, A355;

                

                 A362: ( LSeg (((1 / 2) * ((( GoB f) * ((i0 -' 1),j0)) + (( GoB f) * (i0,j1)))),((1 / 2) * ((( GoB f) * ((i0 -' 1),j1)) + (( GoB f) * (i0,(j1 + 1))))))) meets ( Int ( cell (( GoB f),(i1 -' 1),j0))) by A21, A24, A27, A30, A45, A354, A359, GOBOARD6: 82;

                ( LSeg (((1 / 2) * ((( GoB f) * ((i0 -' 1),j0)) + (( GoB f) * (i0,j1)))),((1 / 2) * ((( GoB f) * ((i0 -' 1),j1)) + (( GoB f) * (i0,(j1 + 1))))))) misses ( L~ f) by A5, A6, A11, A14, A17, A23, A24, A30, A31, A45, A50, A53, A354, A359, A360, A361, GOBOARD8: 3;

                then ( LSeg (((1 / 2) * ((( GoB f) * ((i0 -' 1),j0)) + (( GoB f) * (i0,j1)))),((1 / 2) * ((( GoB f) * ((i0 -' 1),j1)) + (( GoB f) * (i0,(j1 + 1))))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A363: ( LSeg (((1 / 2) * ((( GoB f) * ((i0 -' 1),j0)) + (( GoB f) * (i0,j1)))),((1 / 2) * ((( GoB f) * ((i0 -' 1),j1)) + (( GoB f) * (i0,(j1 + 1))))))) c= ( LeftComp f) by A3, A5, A6, A55, A358, A362, Th4, NAT_1: 13;

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

                then

                 A364: (i1 -' 1) <= ( len ( GoB f)) by A21, XXREAL_0: 2;

                

                 A365: ( Int ( cell (( GoB f),(i1 -' 1),j1))) is convex by A27, A364, Th16;

                ( Int ( cell (( GoB f),(i1 -' 1),j1))) misses ( L~ f) by A27, A364, GOBOARD7: 12;

                then ( Int ( cell (( GoB f),(i1 -' 1),j1))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A366: ( Int ( cell (( GoB f),(i1 -' 1),j1))) c= ( LeftComp f) by A30, A55, A354, A363, A19, A26, A45, A359, A360, Th4, A365, GOBOARD6: 82;

                

                 A367: ( left_cell (f,(k + 1))) = ( cell (( GoB f),i1,j1)) by A4, A5, A13, A14, A16, A17, A31, A354, A355, GOBOARD5: 28;

                

                 A368: ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,(j1 + 1))))),((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i2,(j1 + 1))))))) meets ( Int ( cell (( GoB f),(i1 -' 1),j1))) by A21, A26, A30, A45, A354, A359, A360, GOBOARD6: 82;

                ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,(j1 + 1))))),((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i2,(j1 + 1))))))) misses ( L~ f) by A5, A6, A11, A14, A17, A23, A24, A30, A31, A45, A50, A53, A354, A359, A360, A361, GOBOARD8: 15;

                then ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,(j1 + 1))))),((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i2,(j1 + 1))))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A369: ( LSeg (((1 / 2) * ((( GoB f) * ((i1 -' 1),j1)) + (( GoB f) * (i1,(j1 + 1))))),((1 / 2) * ((( GoB f) * (i1,j1)) + (( GoB f) * (i2,(j1 + 1))))))) c= ( LeftComp f) by A55, A366, A368, Th4;

                

                 A370: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A367, A369, A20, A23, A26, A355, A360, Th4, A370, GOBOARD6: 82;

              end;

                suppose that

                 A371: (j0 + 1) = j1 and

                 A372: (j1 + 1) = j2 and

                 A373: i0 = 1;

                

                 A374: ( left_cell (f,k)) = ( cell (( GoB f), 0 ,j0)) by A6, A7, A10, A11, A13, A14, A30, A56, A371, A373, GOBOARD5: 27;

                

                 A375: ( left_cell (f,(k + 1))) = ( cell (( GoB f), 0 ,j1)) by A4, A5, A13, A14, A16, A17, A30, A31, A56, A371, A372, A373, GOBOARD5: 27;

                

                 A376: ( LSeg ((((1 / 2) * ((( GoB f) * (1,j0)) + (( GoB f) * (1,j1)))) - |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (1,j1)) + (( GoB f) * (1,j2)))) - |[1, 0 ]|))) meets ( Int ( cell (( GoB f), 0 ,j0))) by A24, A27, A371, GOBOARD6: 85;

                ( LSeg ((((1 / 2) * ((( GoB f) * (1,j0)) + (( GoB f) * (1,j1)))) - |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (1,j1)) + (( GoB f) * (1,j2)))) - |[1, 0 ]|))) misses ( L~ f) by A24, A29, A53, A371, A372, GOBOARD8: 31;

                then ( LSeg ((((1 / 2) * ((( GoB f) * (1,j0)) + (( GoB f) * (1,j1)))) - |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (1,j1)) + (( GoB f) * (1,j2)))) - |[1, 0 ]|))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A377: ( LSeg ((((1 / 2) * ((( GoB f) * (1,j0)) + (( GoB f) * (1,j1)))) - |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (1,j1)) + (( GoB f) * (1,j2)))) - |[1, 0 ]|))) c= ( LeftComp f) by A3, A5, A6, A55, A374, A376, Th4, NAT_1: 13;

                

                 A378: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A55, A375, A377, A26, A29, A372, Th4, A378, GOBOARD6: 85;

              end;

                suppose that

                 A379: (j0 + 1) = j1 and

                 A380: (j1 + 1) = j2 and

                 A381: i0 <> 1;

                

                 A382: ( left_cell (f,k)) = ( cell (( GoB f),(i1 -' 1),j0)) by A6, A7, A10, A11, A13, A14, A30, A45, A379, GOBOARD5: 27;

                1 < i0 by A18, A381, XXREAL_0: 1;

                then

                 A383: 1 <= (i0 -' 1) by A30, A45, A379, NAT_1: 13;

                

                 A384: ( left_cell (f,(k + 1))) = ( cell (( GoB f),(i1 -' 1),j1)) by A4, A5, A13, A14, A16, A17, A31, A45, A380, GOBOARD5: 27;

                

                 A385: ( LSeg (((1 / 2) * ((( GoB f) * ((i0 -' 1),j0)) + (( GoB f) * (i0,j1)))),((1 / 2) * ((( GoB f) * ((i0 -' 1),j1)) + (( GoB f) * (i0,j2)))))) meets ( Int ( cell (( GoB f),(i1 -' 1),j0))) by A21, A24, A27, A30, A45, A379, A383, GOBOARD6: 82;

                ( LSeg (((1 / 2) * ((( GoB f) * ((i0 -' 1),j0)) + (( GoB f) * (i0,j1)))),((1 / 2) * ((( GoB f) * ((i0 -' 1),j1)) + (( GoB f) * (i0,j2)))))) misses ( L~ f) by A5, A6, A11, A14, A17, A19, A24, A29, A30, A31, A45, A50, A53, A379, A380, A383, GOBOARD8: 1;

                then ( LSeg (((1 / 2) * ((( GoB f) * ((i0 -' 1),j0)) + (( GoB f) * (i0,j1)))),((1 / 2) * ((( GoB f) * ((i0 -' 1),j1)) + (( GoB f) * (i0,j2)))))) c= (( L~ f) ` ) by SUBSET_1: 23;

                then

                 A386: ( LSeg (((1 / 2) * ((( GoB f) * ((i0 -' 1),j0)) + (( GoB f) * (i0,j1)))),((1 / 2) * ((( GoB f) * ((i0 -' 1),j1)) + (( GoB f) * (i0,j2)))))) c= ( LeftComp f) by A3, A5, A6, A55, A382, A385, Th4, NAT_1: 13;

                

                 A387: ( Int ( left_cell (f,(k + 1)))) is convex by A4, A5, Th17;

                ( Int ( left_cell (f,(k + 1)))) misses ( L~ f) by A4, A5, GOBOARD8: 37;

                then ( Int ( left_cell (f,(k + 1)))) c= (( L~ f) ` ) by SUBSET_1: 23;

                hence thesis by A30, A55, A379, A384, A386, A19, A26, A29, A45, A380, A383, Th4, A387, GOBOARD6: 82;

              end;

            end;

            hence thesis;

          end;

        end;

      end;

      thus for k holds P[k] from NAT_1:sch 2( A1, A2);

    end;

    theorem :: GOBOARD9:22

    ( GoB ( Rev f)) = ( GoB f) by Lm1;

    theorem :: GOBOARD9:23

    

     Th21: ( RightComp f) = ( LeftComp ( Rev f))

    proof

      ( LeftComp ( Rev f)) is_a_component_of (( L~ ( Rev f)) ` ) by Def1;

      then

       A1: ( LeftComp ( Rev f)) is_a_component_of (( L~ f) ` ) by SPPOL_2: 22;

      

       A2: ( len f) >= 4 by GOBOARD7: 34;

      

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

      

       A4: ((( len f) -' 1) + 1) = ( len f) by A2, XREAL_1: 235, XXREAL_0: 2;

      then

       A5: 1 <= (( len f) -' 1) by A3, XREAL_1: 6;

      

       A6: ((( len f) -' 1) + 1) <= ( len ( Rev f)) by A4, FINSEQ_5:def 3;

      ( right_cell (f,1)) = ( left_cell (( Rev f),(( len f) -' 1))) by A4, A5, Th9;

      then ( Int ( right_cell (f,1))) c= ( LeftComp ( Rev f)) by A5, A6, Th19;

      hence thesis by A1, Def2;

    end;

    theorem :: GOBOARD9:24

    ( RightComp ( Rev f)) = ( LeftComp f)

    proof

      ( Rev ( Rev f)) = f;

      hence thesis by Th21;

    end;

    theorem :: GOBOARD9:25

    for k st 1 <= k & (k + 1) <= ( len f) holds ( Int ( right_cell (f,k))) c= ( RightComp f)

    proof

      let k such that

       A1: 1 <= k and

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

      

       A3: ( len f) = ( len ( Rev f)) by FINSEQ_5:def 3;

      k <= ( len f) by A2, NAT_1: 13;

      then

       A4: ((( len f) -' k) + k) = ( len f) by XREAL_1: 235;

      then

       A5: 1 <= (( len f) -' k) by A2, XREAL_1: 6;

      

       A6: ((( len f) -' k) + 1) <= ( len f) by A1, A4, XREAL_1: 6;

      

       A7: ( right_cell (f,k)) = ( left_cell (( Rev f),(( len f) -' k))) by A1, A4, A5, Th9;

      ( RightComp f) = ( LeftComp ( Rev f)) by Th21;

      hence thesis by A3, A5, A6, A7, Th19;

    end;