gobrd12.miz



    begin

    reserve i,j,k,k1,k2,i1,i2,j1,j2 for Nat,

r,s for Real,

x for set,

f for non constant standard special_circular_sequence;

    

     Lm1: (( L~ f) ` ) = the carrier of (( TOP-REAL 2) | (( L~ f) ` ))

    proof

      (( L~ f) ` ) = ( [#] (( TOP-REAL 2) | (( L~ f) ` ))) by PRE_TOPC:def 5

      .= the carrier of (( TOP-REAL 2) | (( L~ f) ` ));

      hence thesis;

    end;

    

     Lm2: the carrier of ( TOP-REAL 2) = ( REAL 2) by EUCLID: 22;

    theorem :: GOBRD12:1

    

     Th1: for i, j st i <= ( len ( GoB f)) & j <= ( width ( GoB f)) holds ( Int ( cell (( GoB f),i,j))) c= (( L~ f) ` ) by GOBOARD7: 12, SUBSET_1: 23;

    theorem :: GOBRD12:2

    

     Th2: for i, j st i <= ( len ( GoB f)) & j <= ( width ( GoB f)) holds ( Cl ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` )))) = (( cell (( GoB f),i,j)) /\ (( L~ f) ` ))

    proof

      let i, j;

      reconsider V = ( Int ( cell (( GoB f),i,j))) as Subset of ( TOP-REAL 2);

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

      assume

       A1: i <= ( len ( GoB f)) & j <= ( width ( GoB f));

      then ( Cl ( Down (V,B))) = (( Cl V) /\ B) by Th1, CONNSP_3: 29;

      hence thesis by A1, GOBRD11: 35;

    end;

    theorem :: GOBRD12:3

    

     Th3: for i, j st i <= ( len ( GoB f)) & j <= ( width ( GoB f)) holds ( Cl ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` )))) is connected & ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` ))) = ( Int ( cell (( GoB f),i,j)))

    proof

      let i, j;

      assume

       A1: i <= ( len ( GoB f)) & j <= ( width ( GoB f));

      then ( Int ( cell (( GoB f),i,j))) is convex & ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` ))) = ( Int ( cell (( GoB f),i,j))) by Th1, GOBOARD9: 17, XBOOLE_1: 28;

      then ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` ))) is connected by CONNSP_1: 23;

      hence ( Cl ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` )))) is connected by CONNSP_1: 19;

      thus thesis by A1, Th1, XBOOLE_1: 28;

    end;

    

     Lm3: ( Cl ( Down (( LeftComp f),(( L~ f) ` )))) is connected & ( Down (( LeftComp f),(( L~ f) ` ))) = ( LeftComp f) & ( Down (( LeftComp f),(( L~ f) ` ))) is a_component

    proof

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

      then

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

      

       A2: the carrier of (( TOP-REAL 2) | (( L~ f) ` )) = (( L~ f) ` ) by PRE_TOPC: 8;

      then ( Down (( LeftComp f),(( L~ f) ` ))) = ( LeftComp f) by A1, XBOOLE_1: 28;

      then ( Down (( LeftComp f),(( L~ f) ` ))) is connected by A1, CONNSP_1:def 5;

      hence ( Cl ( Down (( LeftComp f),(( L~ f) ` )))) is connected by CONNSP_1: 19;

      thus thesis by A1, A2, XBOOLE_1: 28;

    end;

    

     Lm4: ( Cl ( Down (( RightComp f),(( L~ f) ` )))) is connected & ( Down (( RightComp f),(( L~ f) ` ))) = ( RightComp f) & ( Down (( RightComp f),(( L~ f) ` ))) is a_component

    proof

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

      then

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

      

       A2: the carrier of (( TOP-REAL 2) | (( L~ f) ` )) = (( L~ f) ` ) by PRE_TOPC: 8;

      then ( Down (( RightComp f),(( L~ f) ` ))) = ( RightComp f) by A1, XBOOLE_1: 28;

      then ( Down (( RightComp f),(( L~ f) ` ))) is connected by A1, CONNSP_1:def 5;

      hence ( Cl ( Down (( RightComp f),(( L~ f) ` )))) is connected by CONNSP_1: 19;

      thus thesis by A1, A2, XBOOLE_1: 28;

    end;

    theorem :: GOBRD12:4

    

     Th4: (( L~ f) ` ) = ( union { ( Cl ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` )))) : i <= ( len ( GoB f)) & j <= ( width ( GoB f)) })

    proof

      

       A1: the carrier of ( TOP-REAL 2) = ( union { ( cell (( GoB f),i,j)) : i <= ( len ( GoB f)) & j <= ( width ( GoB f)) }) by GOBRD11: 7;

      

       A2: (( L~ f) ` ) c= ( union { ( Cl ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` )))) : i <= ( len ( GoB f)) & j <= ( width ( GoB f)) })

      proof

        let x be object;

        assume

         A3: x in (( L~ f) ` );

        then

        consider Y be set such that

         A4: x in Y & Y in { ( cell (( GoB f),i,j)) : i <= ( len ( GoB f)) & j <= ( width ( GoB f)) } by A1, TARSKI:def 4;

        consider i, j such that

         A5: Y = ( cell (( GoB f),i,j)) and

         A6: i <= ( len ( GoB f)) & j <= ( width ( GoB f)) by A4;

        reconsider Y0 = ( Cl ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` )))) as set;

        x in (( cell (( GoB f),i,j)) /\ (( L~ f) ` )) by A3, A4, A5, XBOOLE_0:def 4;

        then

         A7: x in Y0 by A6, Th2;

        Y0 in { ( Cl ( Down (( Int ( cell (( GoB f),i1,j1))),(( L~ f) ` )))) : i1 <= ( len ( GoB f)) & j1 <= ( width ( GoB f)) } by A6;

        hence thesis by A7, TARSKI:def 4;

      end;

      ( union { ( Cl ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` )))) : i <= ( len ( GoB f)) & j <= ( width ( GoB f)) }) c= (( L~ f) ` )

      proof

        let x be object;

        assume x in ( union { ( Cl ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` )))) : i <= ( len ( GoB f)) & j <= ( width ( GoB f)) });

        then

        consider Y be set such that

         A8: x in Y & Y in { ( Cl ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` )))) : i <= ( len ( GoB f)) & j <= ( width ( GoB f)) } by TARSKI:def 4;

        consider i, j such that

         A9: Y = ( Cl ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` )))) and i <= ( len ( GoB f)) and j <= ( width ( GoB f)) by A8;

        ( Cl ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` )))) c= the carrier of (( TOP-REAL 2) | (( L~ f) ` ));

        then Y c= (( L~ f) ` ) by A9, Lm1;

        hence thesis by A8;

      end;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: GOBRD12:5

    

     Th5: (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) is a_union_of_components of (( TOP-REAL 2) | (( L~ f) ` )) & ( Down (( LeftComp f),(( L~ f) ` ))) = ( LeftComp f) & ( Down (( RightComp f),(( L~ f) ` ))) = ( RightComp f)

    proof

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

      then

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

       A1: B1 = ( LeftComp f) and

       A2: B1 is a_component by CONNSP_1:def 6;

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

      then

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

       A3: B2 = ( RightComp f) and

       A4: B2 is a_component by CONNSP_1:def 6;

      

       A5: B2 is Subset of (( L~ f) ` ) by Lm1;

      then

       A6: ( Down (( RightComp f),(( L~ f) ` ))) is a_component by A3, A4, XBOOLE_1: 28;

      

       A7: B1 is Subset of (( L~ f) ` ) by Lm1;

      then ( Down (( LeftComp f),(( L~ f) ` ))) is a_component by A1, A2, XBOOLE_1: 28;

      hence thesis by A1, A7, A3, A5, A6, GOBRD11: 3, XBOOLE_1: 28;

    end;

    

     Lm5: for i1, j1, i2, j2 st i1 <= ( len ( GoB f)) & j1 <= ( width ( GoB f)) & i2 <= ( len ( GoB f)) & j2 <= ( width ( GoB f)) & (i2 = (i1 + 1) or i1 = (i2 + 1)) & j1 = j2 holds ( Int ( cell (( GoB f),i1,j1))) c= (( LeftComp f) \/ ( RightComp f)) implies ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f))

    proof

      let i1, j1, i2, j2;

      assume that

       A1: i1 <= ( len ( GoB f)) and

       A2: j1 <= ( width ( GoB f)) and

       A3: i2 <= ( len ( GoB f)) and

       A4: j2 <= ( width ( GoB f)) and

       A5: i2 = (i1 + 1) or i1 = (i2 + 1) and

       A6: j1 = j2;

      now

        assume

         A7: ( Int ( cell (( GoB f),i1,j1))) c= (( LeftComp f) \/ ( RightComp f));

        now

          per cases by A5;

            case

             A8: i2 = (i1 + 1);

            now

              per cases ;

                case ex k st 1 <= k & (k + 1) <= ( len f) & j2 <> 0 & j2 <> ( width ( GoB f)) & ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * ((i1 + 1),j2)),(( GoB f) * ((i1 + 1),(j2 + 1)))));

                then

                consider k such that

                 A9: 1 <= k & (k + 1) <= ( len f) and

                 A10: j2 <> 0 and

                 A11: j2 <> ( width ( GoB f)) and

                 A12: ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * ((i1 + 1),j2)),(( GoB f) * ((i1 + 1),(j2 + 1)))));

                now

                  per cases by A12, SPPOL_1: 8;

                    case

                     A13: (f /. k) = (( GoB f) * ((i1 + 1),j2)) & (f /. (k + 1)) = (( GoB f) * ((i1 + 1),(j2 + 1)));

                    

                     A14: ( Int ( right_cell (f,k))) c= ( RightComp f) & ( RightComp f) c= (( LeftComp f) \/ ( RightComp f)) by A9, GOBOARD9: 25, XBOOLE_1: 7;

                    j2 < ( width ( GoB f)) by A4, A11, XXREAL_0: 1;

                    then

                     A15: (j2 + 1) <= ( width ( GoB f)) by NAT_1: 13;

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

                    then

                     A16: ( Indices ( GoB f)) = [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] & (i1 + 1) in ( dom ( GoB f)) by A3, A8, FINSEQ_3: 25, MATRIX_0:def 4;

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

                    then (j2 + 1) in ( Seg ( width ( GoB f))) by A15, FINSEQ_1: 1;

                    then

                     A17: [(i1 + 1), (j2 + 1)] in ( Indices ( GoB f)) by A16, ZFMISC_1: 87;

                    j2 >= ( 0 + 1) by A10, NAT_1: 13;

                    then j2 in ( Seg ( width ( GoB f))) by A4, FINSEQ_1: 1;

                    then [(i1 + 1), j2] in ( Indices ( GoB f)) by A16, ZFMISC_1: 87;

                    then ( right_cell (f,k)) = ( cell (( GoB f),(i1 + 1),j2)) by A9, A13, A17, GOBOARD5: 27;

                    hence ( Int ( cell (( GoB f),(i1 + 1),j2))) c= (( LeftComp f) \/ ( RightComp f)) by A14;

                  end;

                    case

                     A18: (f /. k) = (( GoB f) * ((i1 + 1),(j2 + 1))) & (f /. (k + 1)) = (( GoB f) * ((i1 + 1),j2));

                    

                     A19: ( Int ( left_cell (f,k))) c= ( LeftComp f) & ( LeftComp f) c= (( LeftComp f) \/ ( RightComp f)) by A9, GOBOARD9: 21, XBOOLE_1: 7;

                    j2 < ( width ( GoB f)) by A4, A11, XXREAL_0: 1;

                    then

                     A20: (j2 + 1) <= ( width ( GoB f)) by NAT_1: 13;

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

                    then

                     A21: ( Indices ( GoB f)) = [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] & (i1 + 1) in ( dom ( GoB f)) by A3, A8, FINSEQ_3: 25, MATRIX_0:def 4;

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

                    then (j2 + 1) in ( Seg ( width ( GoB f))) by A20, FINSEQ_1: 1;

                    then

                     A22: [(i1 + 1), (j2 + 1)] in ( Indices ( GoB f)) by A21, ZFMISC_1: 87;

                    j2 >= ( 0 + 1) by A10, NAT_1: 13;

                    then j2 in ( Seg ( width ( GoB f))) by A4, FINSEQ_1: 1;

                    then [(i1 + 1), j2] in ( Indices ( GoB f)) by A21, ZFMISC_1: 87;

                    then ( left_cell (f,k)) = ( cell (( GoB f),(i1 + 1),j2)) by A9, A18, A22, GOBOARD5: 30;

                    hence ( Int ( cell (( GoB f),(i1 + 1),j2))) c= (( LeftComp f) \/ ( RightComp f)) by A19;

                  end;

                end;

                hence ( Int ( cell (( GoB f),(i1 + 1),j2))) c= (( LeftComp f) \/ ( RightComp f));

              end;

                case

                 A23: not ex k st 1 <= k & (k + 1) <= ( len f) & j2 <> 0 & j2 <> ( width ( GoB f)) & ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * ((i1 + 1),j2)),(( GoB f) * ((i1 + 1),(j2 + 1)))));

                now

                  per cases by A23;

                    case

                     A24: j2 = 0 ;

                    reconsider p = |[((( GoB f) * ((i1 + 1),1)) `1 ), (((( GoB f) * ((i1 + 1),1)) `2 ) - 1)]| as Point of ( TOP-REAL 2);

                    

                     A25: 1 < ( width ( GoB f)) by GOBOARD7: 33;

                    

                     A26: 1 < ( len ( GoB f)) by GOBOARD7: 32;

                    reconsider P = {p} as Subset of ( TOP-REAL 2);

                    

                     A27: (p `2 ) < ((p `2 ) + 1) by XREAL_1: 29;

                    

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

                    then ((( GoB f) * ((i1 + 1),1)) `2 ) = ((( GoB f) * (1,1)) `2 ) by A3, A8, A25, GOBOARD5: 1;

                    then

                     A29: (p `2 ) = (((( GoB f) * (1,1)) `2 ) - 1) by EUCLID: 52;

                    p in { |[r, s]| : s <= ((( GoB f) * (1,1)) `2 ) }

                    proof

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

                      hence thesis by A29, A27;

                    end;

                    then

                     A30: p in ( h_strip (( GoB f),j2)) by A24, A26, GOBOARD5: 7;

                    (for q be Point of ( TOP-REAL 2) st q in P holds (q `2 ) < ((( GoB f) * (1,1)) `2 )) implies P misses ( L~ f) by GOBOARD8: 23;

                    then

                     A31: p in {p} & {p} c= (( L~ f) ` ) by A29, A27, SUBSET_1: 23, TARSKI:def 1;

                    then

                    reconsider p1 = p as Point of (( TOP-REAL 2) | (( L~ f) ` )) by PRE_TOPC: 8;

                    

                     A32: i1 = 0 or i1 >= ( 0 + 1) by NAT_1: 13;

                     A33:

                    now

                      per cases by A3, A8, A32, XXREAL_0: 1;

                        case

                         A34: i1 >= 1 & (i1 + 1) < ( len ( GoB f));

                        then

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

                        

                         A36: p in { |[r, s]| : ((( GoB f) * ((i1 + 1),1)) `1 ) <= r & r <= ((( GoB f) * (((i1 + 1) + 1),1)) `1 ) }

                        proof

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

                          then ((( GoB f) * ((i1 + 1),1)) `1 ) <= ((( GoB f) * (((i1 + 1) + 1),1)) `1 ) by A25, A28, A35, GOBOARD5: 3;

                          hence thesis;

                        end;

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

                        then p in ( v_strip (( GoB f),(i1 + 1))) by A25, A34, A36, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),(i1 + 1))) /\ ( h_strip (( GoB f),j2))) by A30, XBOOLE_0:def 4;

                        then

                         A37: p in ( cell (( GoB f),(i1 + 1),j2)) by GOBOARD5:def 3;

                        

                         A38: p in { |[r, s]| : ((( GoB f) * (i1,1)) `1 ) <= r & r <= ((( GoB f) * ((i1 + 1),1)) `1 ) }

                        proof

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

                          then ((( GoB f) * (i1,1)) `1 ) < ((( GoB f) * ((i1 + 1),1)) `1 ) by A25, A34, GOBOARD5: 3;

                          hence thesis;

                        end;

                        i1 < ( len ( GoB f)) by A34, NAT_1: 13;

                        then p in ( v_strip (( GoB f),i1)) by A25, A34, A38, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),i1)) /\ ( h_strip (( GoB f),j2))) by A30, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i1,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i1 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i1,j2)) /\ (( L~ f) ` )) by A31, A37, XBOOLE_0:def 4;

                      end;

                        case

                         A39: i1 >= 1 & (i1 + 1) = ( len ( GoB f));

                        

                         A40: i1 < (i1 + 1) by NAT_1: 13;

                        

                         A41: p in { |[r, s]| : ((( GoB f) * (i1,1)) `1 ) <= r & r <= ((( GoB f) * ((i1 + 1),1)) `1 ) }

                        proof

                          ((( GoB f) * (i1,1)) `1 ) < ((( GoB f) * ((i1 + 1),1)) `1 ) by A25, A39, A40, GOBOARD5: 3;

                          hence thesis;

                        end;

                        p in { |[r, s]| : ((( GoB f) * ((i1 + 1),1)) `1 ) <= r };

                        then p in ( v_strip (( GoB f),(i1 + 1))) by A25, A39, GOBOARD5: 9;

                        then p in (( v_strip (( GoB f),(i1 + 1))) /\ ( h_strip (( GoB f),j2))) by A30, XBOOLE_0:def 4;

                        then

                         A42: p in ( cell (( GoB f),(i1 + 1),j2)) by GOBOARD5:def 3;

                        i1 < ( len ( GoB f)) by A39, NAT_1: 13;

                        then p in ( v_strip (( GoB f),i1)) by A25, A39, A41, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),i1)) /\ ( h_strip (( GoB f),j2))) by A30, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i1,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i1 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i1,j2)) /\ (( L~ f) ` )) by A31, A42, XBOOLE_0:def 4;

                      end;

                        case

                         A43: i1 = 0 & (i1 + 1) < ( len ( GoB f));

                        then

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

                        p in { |[r, s]| : ((( GoB f) * ((i1 + 1),1)) `1 ) <= r & r <= ((( GoB f) * (((i1 + 1) + 1),1)) `1 ) }

                        proof

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

                          then ((( GoB f) * ((i1 + 1),1)) `1 ) <= ((( GoB f) * (((i1 + 1) + 1),1)) `1 ) by A25, A28, A44, GOBOARD5: 3;

                          hence thesis;

                        end;

                        then p in ( v_strip (( GoB f),(i1 + 1))) by A25, A43, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),(i1 + 1))) /\ ( h_strip (( GoB f),j2))) by A30, XBOOLE_0:def 4;

                        then

                         A45: p in ( cell (( GoB f),(i1 + 1),j2)) by GOBOARD5:def 3;

                        p in { |[r, s]| : r <= ((( GoB f) * (1,1)) `1 ) } by A43;

                        then p in ( v_strip (( GoB f),i1)) by A25, A43, GOBOARD5: 10;

                        then p in (( v_strip (( GoB f),i1)) /\ ( h_strip (( GoB f),j2))) by A30, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i1,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i1 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i1,j2)) /\ (( L~ f) ` )) by A31, A45, XBOOLE_0:def 4;

                      end;

                        case

                         A46: i1 = 0 & (i1 + 1) = ( len ( GoB f));

                        p in { |[r, s]| : ((( GoB f) * ((i1 + 1),1)) `1 ) <= r };

                        then p in ( v_strip (( GoB f),(i1 + 1))) by A25, A46, GOBOARD5: 9;

                        then p in (( v_strip (( GoB f),(i1 + 1))) /\ ( h_strip (( GoB f),j2))) by A30, XBOOLE_0:def 4;

                        then

                         A47: p in ( cell (( GoB f),(i1 + 1),j2)) by GOBOARD5:def 3;

                        p in { |[r, s]| : r <= ((( GoB f) * (1,1)) `1 ) } by A46;

                        then p in ( v_strip (( GoB f),i1)) by A25, A46, GOBOARD5: 10;

                        then p in (( v_strip (( GoB f),i1)) /\ ( h_strip (( GoB f),j2))) by A30, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i1,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i1 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i1,j2)) /\ (( L~ f) ` )) by A31, A47, XBOOLE_0:def 4;

                      end;

                    end;

                    then p in ( Cl ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` )))) by A4, Th2;

                    then

                     A48: ( Cl ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` )))) c= ( Component_of p1) by A3, A4, A8, Th3, GOBRD11: 1;

                    ( Down (( RightComp f),(( L~ f) ` ))) is closed by Lm4, CONNSP_1: 33;

                    then

                     A49: ( Cl ( Down (( RightComp f),(( L~ f) ` )))) = ( Down (( RightComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    ( Down (( LeftComp f),(( L~ f) ` ))) is closed by Lm3, CONNSP_1: 33;

                    then

                     A50: ( Cl ( Down (( LeftComp f),(( L~ f) ` )))) = ( Down (( LeftComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) = ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by GOBRD11: 4;

                    then

                     A51: ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) = (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A50, A49, PRE_TOPC: 20;

                    

                     A52: ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` ))) c= ( Cl ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` )))) & ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` ))) = ( Int ( cell (( GoB f),(i1 + 1),j2))) by A3, A4, A8, Th3, PRE_TOPC: 18;

                    

                     A53: ( Down (( LeftComp f),(( L~ f) ` ))) = ( LeftComp f) & ( Down (( RightComp f),(( L~ f) ` ))) = ( RightComp f) by Th5;

                    ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` ))) c= (( LeftComp f) \/ ( RightComp f)) by A1, A2, A6, A7, Th3;

                    then ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` ))) c= ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by A53, GOBRD11: 4;

                    then

                     A54: ( Cl ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` )))) c= ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) by PRE_TOPC: 19;

                    p in ( Cl ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` )))) by A1, A4, A33, Th2;

                    then ( Component_of p1) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A54, A51, Th5, CONNSP_3: 21;

                    then ( Cl ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` )))) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A48;

                    hence ( Int ( cell (( GoB f),(i1 + 1),j2))) c= (( LeftComp f) \/ ( RightComp f)) by A53, A52;

                  end;

                    case

                     A55: j2 = ( width ( GoB f));

                    reconsider p = |[((( GoB f) * ((i1 + 1),( width ( GoB f)))) `1 ), (((( GoB f) * ((i1 + 1),( width ( GoB f)))) `2 ) + 1)]| as Point of ( TOP-REAL 2);

                    

                     A56: 1 < ( width ( GoB f)) by GOBOARD7: 33;

                    reconsider P = {p} as Subset of ( TOP-REAL 2);

                    

                     A57: (for q be Point of ( TOP-REAL 2) st q in P holds ((( GoB f) * (1,( width ( GoB f)))) `2 ) < (q `2 )) implies P misses ( L~ f) by GOBOARD8: 24;

                    

                     A58: 1 < ( len ( GoB f)) by GOBOARD7: 32;

                    

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

                    then ((( GoB f) * ((i1 + 1),( width ( GoB f)))) `2 ) = ((( GoB f) * (1,( width ( GoB f)))) `2 ) by A3, A8, A56, GOBOARD5: 1;

                    then

                     A60: (p `2 ) = (((( GoB f) * (1,( width ( GoB f)))) `2 ) + 1) by EUCLID: 52;

                    then

                     A61: ((( GoB f) * (1,( width ( GoB f)))) `2 ) < (p `2 ) by XREAL_1: 29;

                    p in { |[r, s]| : ((( GoB f) * (1,( width ( GoB f)))) `2 ) <= s }

                    proof

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

                      hence thesis by A61;

                    end;

                    then

                     A62: p in ( h_strip (( GoB f),j2)) by A55, A58, GOBOARD5: 6;

                    ((( GoB f) * (1,( width ( GoB f)))) `2 ) < (((( GoB f) * (1,( width ( GoB f)))) `2 ) + 1) by XREAL_1: 29;

                    then

                     A63: p in {p} & {p} c= (( L~ f) ` ) by A60, A57, SUBSET_1: 23, TARSKI:def 1;

                    then

                    reconsider p1 = p as Point of (( TOP-REAL 2) | (( L~ f) ` )) by PRE_TOPC: 8;

                    

                     A64: i1 = 0 or i1 >= ( 0 + 1) by NAT_1: 13;

                     A65:

                    now

                      per cases by A3, A8, A64, XXREAL_0: 1;

                        case

                         A66: i1 >= 1 & (i1 + 1) < ( len ( GoB f));

                        then

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

                        

                         A68: p in { |[r, s]| : ((( GoB f) * ((i1 + 1),( width ( GoB f)))) `1 ) <= r & r <= ((( GoB f) * (((i1 + 1) + 1),( width ( GoB f)))) `1 ) }

                        proof

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

                          then ((( GoB f) * ((i1 + 1),( width ( GoB f)))) `1 ) <= ((( GoB f) * (((i1 + 1) + 1),( width ( GoB f)))) `1 ) by A56, A59, A67, GOBOARD5: 3;

                          hence thesis;

                        end;

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

                        then p in ( v_strip (( GoB f),(i1 + 1))) by A56, A66, A68, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),(i1 + 1))) /\ ( h_strip (( GoB f),j2))) by A62, XBOOLE_0:def 4;

                        then

                         A69: p in ( cell (( GoB f),(i1 + 1),j2)) by GOBOARD5:def 3;

                        

                         A70: p in { |[r, s]| : ((( GoB f) * (i1,( width ( GoB f)))) `1 ) <= r & r <= ((( GoB f) * ((i1 + 1),( width ( GoB f)))) `1 ) }

                        proof

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

                          then ((( GoB f) * (i1,( width ( GoB f)))) `1 ) < ((( GoB f) * ((i1 + 1),( width ( GoB f)))) `1 ) by A56, A66, GOBOARD5: 3;

                          hence thesis;

                        end;

                        i1 < ( len ( GoB f)) by A66, NAT_1: 13;

                        then p in ( v_strip (( GoB f),i1)) by A56, A66, A70, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),i1)) /\ ( h_strip (( GoB f),j2))) by A62, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i1,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i1 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i1,j2)) /\ (( L~ f) ` )) by A63, A69, XBOOLE_0:def 4;

                      end;

                        case

                         A71: i1 >= 1 & (i1 + 1) = ( len ( GoB f));

                        

                         A72: i1 < (i1 + 1) by NAT_1: 13;

                        

                         A73: p in { |[r, s]| : ((( GoB f) * (i1,( width ( GoB f)))) `1 ) <= r & r <= ((( GoB f) * ((i1 + 1),( width ( GoB f)))) `1 ) }

                        proof

                          ((( GoB f) * (i1,( width ( GoB f)))) `1 ) < ((( GoB f) * ((i1 + 1),( width ( GoB f)))) `1 ) by A56, A71, A72, GOBOARD5: 3;

                          hence thesis;

                        end;

                        p in { |[r, s]| : ((( GoB f) * ((i1 + 1),( width ( GoB f)))) `1 ) <= r };

                        then p in ( v_strip (( GoB f),(i1 + 1))) by A56, A71, GOBOARD5: 9;

                        then p in (( v_strip (( GoB f),(i1 + 1))) /\ ( h_strip (( GoB f),j2))) by A62, XBOOLE_0:def 4;

                        then

                         A74: p in ( cell (( GoB f),(i1 + 1),j2)) by GOBOARD5:def 3;

                        i1 < ( len ( GoB f)) by A71, NAT_1: 13;

                        then p in ( v_strip (( GoB f),i1)) by A56, A71, A73, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),i1)) /\ ( h_strip (( GoB f),j2))) by A62, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i1,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i1 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i1,j2)) /\ (( L~ f) ` )) by A63, A74, XBOOLE_0:def 4;

                      end;

                        case

                         A75: i1 = 0 & (i1 + 1) < ( len ( GoB f));

                        then

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

                        p in { |[r, s]| : ((( GoB f) * ((i1 + 1),( width ( GoB f)))) `1 ) <= r & r <= ((( GoB f) * (((i1 + 1) + 1),( width ( GoB f)))) `1 ) }

                        proof

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

                          then ((( GoB f) * ((i1 + 1),( width ( GoB f)))) `1 ) <= ((( GoB f) * (((i1 + 1) + 1),( width ( GoB f)))) `1 ) by A56, A59, A76, GOBOARD5: 3;

                          hence thesis;

                        end;

                        then p in ( v_strip (( GoB f),(i1 + 1))) by A56, A75, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),(i1 + 1))) /\ ( h_strip (( GoB f),j2))) by A62, XBOOLE_0:def 4;

                        then

                         A77: p in ( cell (( GoB f),(i1 + 1),j2)) by GOBOARD5:def 3;

                        p in { |[r, s]| : r <= ((( GoB f) * (1,( width ( GoB f)))) `1 ) } by A75;

                        then p in ( v_strip (( GoB f),i1)) by A56, A75, GOBOARD5: 10;

                        then p in (( v_strip (( GoB f),i1)) /\ ( h_strip (( GoB f),j2))) by A62, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i1,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i1 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i1,j2)) /\ (( L~ f) ` )) by A63, A77, XBOOLE_0:def 4;

                      end;

                        case i1 = 0 & (i1 + 1) = ( len ( GoB f));

                        hence contradiction by GOBOARD7: 32;

                      end;

                    end;

                    then p in ( Cl ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` )))) by A4, Th2;

                    then

                     A78: ( Cl ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` )))) c= ( Component_of p1) by A3, A4, A8, Th3, GOBRD11: 1;

                    ( Down (( RightComp f),(( L~ f) ` ))) is closed by Lm4, CONNSP_1: 33;

                    then

                     A79: ( Cl ( Down (( RightComp f),(( L~ f) ` )))) = ( Down (( RightComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    ( Down (( LeftComp f),(( L~ f) ` ))) is closed by Lm3, CONNSP_1: 33;

                    then

                     A80: ( Cl ( Down (( LeftComp f),(( L~ f) ` )))) = ( Down (( LeftComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) = ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by GOBRD11: 4;

                    then

                     A81: ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) = (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A80, A79, PRE_TOPC: 20;

                    

                     A82: ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` ))) c= ( Cl ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` )))) & ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` ))) = ( Int ( cell (( GoB f),(i1 + 1),j2))) by A3, A4, A8, Th3, PRE_TOPC: 18;

                    

                     A83: ( Down (( LeftComp f),(( L~ f) ` ))) = ( LeftComp f) & ( Down (( RightComp f),(( L~ f) ` ))) = ( RightComp f) by Th5;

                    ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` ))) c= (( LeftComp f) \/ ( RightComp f)) by A1, A2, A6, A7, Th3;

                    then ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` ))) c= ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by A83, GOBRD11: 4;

                    then

                     A84: ( Cl ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` )))) c= ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) by PRE_TOPC: 19;

                    p in ( Cl ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` )))) by A1, A4, A65, Th2;

                    then ( Component_of p1) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A84, A81, Th5, CONNSP_3: 21;

                    then ( Cl ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` )))) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A78;

                    hence ( Int ( cell (( GoB f),(i1 + 1),j2))) c= (( LeftComp f) \/ ( RightComp f)) by A83, A82;

                  end;

                    case

                     A85: j2 <> 0 & j2 <> ( width ( GoB f)) & not ex k st 1 <= k & (k + 1) <= ( len f) & ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * ((i1 + 1),j2)),(( GoB f) * ((i1 + 1),(j2 + 1)))));

                    then

                     A86: j2 < ( width ( GoB f)) by A4, XXREAL_0: 1;

                    then

                     A87: (j2 + 1) <= ( width ( GoB f)) by NAT_1: 13;

                    for k st 1 <= k & (k + 1) <= ( len f) holds ( LSeg ((( GoB f) * ((i1 + 1),j2)),(( GoB f) * ((i1 + 1),(j2 + 1))))) <> ( LSeg (f,k))

                    proof

                      let k;

                      assume

                       A88: 1 <= k & (k + 1) <= ( len f);

                      then ( LSeg (f,k)) = ( LSeg ((f /. k),(f /. (k + 1)))) by TOPREAL1:def 3;

                      hence thesis by A85, A88;

                    end;

                    then

                     A89: 1 <= (i1 + 1) & (i1 + 1) <= ( len ( GoB f)) & 1 <= j2 & (j2 + 1) <= ( width ( GoB f)) implies not ((1 / 2) * ((( GoB f) * ((i1 + 1),j2)) + (( GoB f) * ((i1 + 1),(j2 + 1))))) in ( L~ f) by GOBOARD7: 39;

                    reconsider p = ((1 / 2) * ((( GoB f) * ((i1 + 1),j2)) + (( GoB f) * ((i1 + 1),(j2 + 1))))) as Point of ( TOP-REAL 2);

                    

                     A90: (p `2 ) = ((1 / 2) * (((( GoB f) * ((i1 + 1),j2)) + (( GoB f) * ((i1 + 1),(j2 + 1)))) `2 )) by TOPREAL3: 4

                    .= ((1 / 2) * (((( GoB f) * ((i1 + 1),j2)) `2 ) + ((( GoB f) * ((i1 + 1),(j2 + 1))) `2 ))) by TOPREAL3: 2;

                    reconsider P = {p} as Subset of ( TOP-REAL 2);

                    

                     A91: 1 < ( width ( GoB f)) by GOBOARD7: 33;

                    ( Down (( RightComp f),(( L~ f) ` ))) is closed by Lm4, CONNSP_1: 33;

                    then

                     A92: ( Cl ( Down (( RightComp f),(( L~ f) ` )))) = ( Down (( RightComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    ( Down (( LeftComp f),(( L~ f) ` ))) is closed by Lm3, CONNSP_1: 33;

                    then

                     A93: ( Cl ( Down (( LeftComp f),(( L~ f) ` )))) = ( Down (( LeftComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) = ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by GOBRD11: 4;

                    then

                     A94: ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) = (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A93, A92, PRE_TOPC: 20;

                    

                     A95: ( Down (( LeftComp f),(( L~ f) ` ))) = ( LeftComp f) & ( Down (( RightComp f),(( L~ f) ` ))) = ( RightComp f) by Th5;

                    ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` ))) c= (( LeftComp f) \/ ( RightComp f)) by A1, A2, A6, A7, Th3;

                    then ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` ))) c= ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by A95, GOBRD11: 4;

                    then

                     A96: ( Cl ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` )))) c= ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) by PRE_TOPC: 19;

                    

                     A97: ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` ))) c= ( Cl ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` )))) & ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` ))) = ( Int ( cell (( GoB f),(i1 + 1),j2))) by A3, A4, A8, Th3, PRE_TOPC: 18;

                    

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

                    

                     A99: ( 0 + 1) <= j2 by A85, NAT_1: 13;

                    then

                     A100: 1 < (j2 + 1) by NAT_1: 13;

                    (for x be object st x in P holds not x in ( L~ f)) implies P misses ( L~ f) by XBOOLE_0: 3;

                    then

                     A101: p in {p} & {p} c= (( L~ f) ` ) by A3, A8, A99, A86, A89, NAT_1: 13, SUBSET_1: 23, TARSKI:def 1;

                    then

                    reconsider p1 = p as Point of (( TOP-REAL 2) | (( L~ f) ` )) by PRE_TOPC: 8;

                    

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

                    (p `1 ) = ((1 / 2) * (((( GoB f) * ((i1 + 1),j2)) + (( GoB f) * ((i1 + 1),(j2 + 1)))) `1 )) by TOPREAL3: 4

                    .= ((1 / 2) * (((( GoB f) * ((i1 + 1),j2)) `1 ) + ((( GoB f) * ((i1 + 1),(j2 + 1))) `1 ))) by TOPREAL3: 2;

                    then

                     A103: p = |[((1 / 2) * (((( GoB f) * ((i1 + 1),j2)) `1 ) + ((( GoB f) * ((i1 + 1),(j2 + 1))) `1 ))), ((1 / 2) * (((( GoB f) * ((i1 + 1),j2)) `2 ) + ((( GoB f) * ((i1 + 1),(j2 + 1))) `2 )))]| by A90, EUCLID: 53;

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

                    then

                     A104: ((( GoB f) * ((i1 + 1),j2)) `2 ) < ((( GoB f) * ((i1 + 1),(j2 + 1))) `2 ) by A3, A8, A99, A87, A102, GOBOARD5: 4;

                    then (((( GoB f) * ((i1 + 1),j2)) `2 ) + ((( GoB f) * ((i1 + 1),(j2 + 1))) `2 )) < (((( GoB f) * ((i1 + 1),(j2 + 1))) `2 ) + ((( GoB f) * ((i1 + 1),(j2 + 1))) `2 )) by XREAL_1: 8;

                    then

                     A105: ((((( GoB f) * ((i1 + 1),j2)) `2 ) + ((( GoB f) * ((i1 + 1),(j2 + 1))) `2 )) / 2) < ((((( GoB f) * ((i1 + 1),(j2 + 1))) `2 ) + ((( GoB f) * ((i1 + 1),(j2 + 1))) `2 )) / 2) by XREAL_1: 74;

                    (((( GoB f) * ((i1 + 1),j2)) `2 ) + ((( GoB f) * ((i1 + 1),j2)) `2 )) < (((( GoB f) * ((i1 + 1),j2)) `2 ) + ((( GoB f) * ((i1 + 1),(j2 + 1))) `2 )) by A104, XREAL_1: 8;

                    then

                     A106: ((((( GoB f) * ((i1 + 1),j2)) `2 ) + ((( GoB f) * ((i1 + 1),j2)) `2 )) / 2) < ((((( GoB f) * ((i1 + 1),j2)) `2 ) + ((( GoB f) * ((i1 + 1),(j2 + 1))) `2 )) / 2) by XREAL_1: 74;

                    p in { |[r, s]| : ((( GoB f) * ((i1 + 1),j2)) `2 ) <= s & s <= ((( GoB f) * ((i1 + 1),(j2 + 1))) `2 ) }

                    proof

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

                      hence thesis by A90, A106, A105;

                    end;

                    then

                     A107: p in ( h_strip (( GoB f),j2)) by A3, A8, A99, A86, A98, GOBOARD5: 5;

                    

                     A108: i1 = 0 or i1 >= ( 0 + 1) by NAT_1: 13;

                     A109:

                    now

                      per cases by A3, A8, A108, XXREAL_0: 1;

                        case

                         A110: i1 >= 1 & (i1 + 1) < ( len ( GoB f));

                        then

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

                        

                         A112: p in { |[r, s]| : ((( GoB f) * ((i1 + 1),1)) `1 ) <= r & r <= ((( GoB f) * (((i1 + 1) + 1),1)) `1 ) }

                        proof

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

                          then

                           A113: ((( GoB f) * ((i1 + 1),1)) `1 ) < ((( GoB f) * (((i1 + 1) + 1),1)) `1 ) by A91, A102, A111, GOBOARD5: 3;

                          ((( GoB f) * ((i1 + 1),j2)) `1 ) = ((( GoB f) * ((i1 + 1),1)) `1 ) & ((( GoB f) * ((i1 + 1),(j2 + 1))) `1 ) = ((( GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5: 2;

                          hence thesis by A103, A113;

                        end;

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

                        then p in ( v_strip (( GoB f),(i1 + 1))) by A91, A110, A112, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),(i1 + 1))) /\ ( h_strip (( GoB f),j2))) by A107, XBOOLE_0:def 4;

                        then

                         A114: p in ( cell (( GoB f),(i1 + 1),j2)) by GOBOARD5:def 3;

                        

                         A115: p in { |[r, s]| : ((( GoB f) * (i1,1)) `1 ) <= r & r <= ((( GoB f) * ((i1 + 1),1)) `1 ) }

                        proof

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

                          then

                           A116: ((( GoB f) * (i1,1)) `1 ) < ((( GoB f) * ((i1 + 1),1)) `1 ) by A91, A110, GOBOARD5: 3;

                          ((( GoB f) * ((i1 + 1),j2)) `1 ) = ((( GoB f) * ((i1 + 1),1)) `1 ) & ((( GoB f) * ((i1 + 1),(j2 + 1))) `1 ) = ((( GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5: 2;

                          hence thesis by A103, A116;

                        end;

                        i1 < ( len ( GoB f)) by A110, NAT_1: 13;

                        then p in ( v_strip (( GoB f),i1)) by A91, A110, A115, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),i1)) /\ ( h_strip (( GoB f),j2))) by A107, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i1,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i1 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i1,j2)) /\ (( L~ f) ` )) by A101, A114, XBOOLE_0:def 4;

                      end;

                        case

                         A117: i1 >= 1 & (i1 + 1) = ( len ( GoB f));

                        

                         A118: i1 < (i1 + 1) by NAT_1: 13;

                        p in { |[r, s]| : ((( GoB f) * (i1,1)) `1 ) <= r & r <= ((( GoB f) * ((i1 + 1),1)) `1 ) }

                        proof

                          

                           A119: ((( GoB f) * (i1,1)) `1 ) < ((( GoB f) * ((i1 + 1),1)) `1 ) by A91, A117, A118, GOBOARD5: 3;

                          ((( GoB f) * ((i1 + 1),j2)) `1 ) = ((( GoB f) * ((i1 + 1),1)) `1 ) & ((( GoB f) * ((i1 + 1),(j2 + 1))) `1 ) = ((( GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5: 2;

                          hence thesis by A103, A119;

                        end;

                        then p in ( v_strip (( GoB f),i1)) by A91, A117, A118, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),i1)) /\ ( h_strip (( GoB f),j2))) by A107, XBOOLE_0:def 4;

                        then

                         A120: p in ( cell (( GoB f),i1,j2)) by GOBOARD5:def 3;

                        p in { |[r, s]| : ((( GoB f) * ((i1 + 1),1)) `1 ) <= r }

                        proof

                          ((( GoB f) * ((i1 + 1),j2)) `1 ) = ((( GoB f) * ((i1 + 1),1)) `1 ) & ((( GoB f) * ((i1 + 1),(j2 + 1))) `1 ) = ((( GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5: 2;

                          hence thesis by A103;

                        end;

                        then p in ( v_strip (( GoB f),(i1 + 1))) by A91, A117, GOBOARD5: 9;

                        then p in (( v_strip (( GoB f),(i1 + 1))) /\ ( h_strip (( GoB f),j2))) by A107, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),(i1 + 1),j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i1 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i1,j2)) /\ (( L~ f) ` )) by A101, A120, XBOOLE_0:def 4;

                      end;

                        case

                         A121: i1 = 0 & (i1 + 1) < ( len ( GoB f));

                        then

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

                        p in { |[r, s]| : ((( GoB f) * ((i1 + 1),1)) `1 ) <= r & r <= ((( GoB f) * (((i1 + 1) + 1),1)) `1 ) }

                        proof

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

                          then

                           A123: ((( GoB f) * ((i1 + 1),1)) `1 ) < ((( GoB f) * (((i1 + 1) + 1),1)) `1 ) by A91, A102, A122, GOBOARD5: 3;

                          ((( GoB f) * ((i1 + 1),j2)) `1 ) = ((( GoB f) * ((i1 + 1),1)) `1 ) & ((( GoB f) * ((i1 + 1),(j2 + 1))) `1 ) = ((( GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5: 2;

                          hence thesis by A103, A123;

                        end;

                        then p in ( v_strip (( GoB f),(i1 + 1))) by A91, A121, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),(i1 + 1))) /\ ( h_strip (( GoB f),j2))) by A107, XBOOLE_0:def 4;

                        then

                         A124: p in ( cell (( GoB f),(i1 + 1),j2)) by GOBOARD5:def 3;

                        p in { |[r, s]| : r <= ((( GoB f) * (1,1)) `1 ) }

                        proof

                          ((( GoB f) * ((i1 + 1),j2)) `1 ) = ((( GoB f) * ((i1 + 1),1)) `1 ) & ((( GoB f) * ((i1 + 1),(j2 + 1))) `1 ) = ((( GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5: 2;

                          hence thesis by A103, A121;

                        end;

                        then p in ( v_strip (( GoB f),i1)) by A91, A121, GOBOARD5: 10;

                        then p in (( v_strip (( GoB f),i1)) /\ ( h_strip (( GoB f),j2))) by A107, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i1,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i1 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i1,j2)) /\ (( L~ f) ` )) by A101, A124, XBOOLE_0:def 4;

                      end;

                        case i1 = 0 & (i1 + 1) = ( len ( GoB f));

                        hence contradiction by GOBOARD7: 32;

                      end;

                    end;

                    then p in ( Cl ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` )))) by A4, Th2;

                    then

                     A125: ( Cl ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` )))) c= ( Component_of p1) by A3, A4, A8, Th3, GOBRD11: 1;

                    p in ( Cl ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` )))) by A1, A4, A109, Th2;

                    then ( Component_of p1) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A96, A94, Th5, CONNSP_3: 21;

                    then ( Cl ( Down (( Int ( cell (( GoB f),(i1 + 1),j2))),(( L~ f) ` )))) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A125;

                    hence ( Int ( cell (( GoB f),(i1 + 1),j2))) c= (( LeftComp f) \/ ( RightComp f)) by A95, A97;

                  end;

                end;

                hence ( Int ( cell (( GoB f),(i1 + 1),j2))) c= (( LeftComp f) \/ ( RightComp f));

              end;

            end;

            hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f)) by A8;

          end;

            case

             A126: i1 = (i2 + 1);

            then i2 < i1 by NAT_1: 13;

            then

             A127: (i1 -' 1) < i1 by A126, NAT_D: 34;

            

             A128: i2 < (i2 + 1) by NAT_1: 13;

            

             A129: 1 <= ((i1 -' 1) + 1) by NAT_1: 11;

            

             A130: (i2 + 1) < ((i2 + 1) + 1) by NAT_1: 13;

            

             A131: 1 <= i1 & (i1 -' 1) = (i1 - 1) by A126, NAT_1: 11, XREAL_0:def 2;

            

             A132: 1 <= (i2 + 1) by NAT_1: 11;

            

             A133: (i1 -' 1) = i2 by A126, NAT_D: 34;

            now

              per cases ;

                case ex k st 1 <= k & (k + 1) <= ( len f) & j2 <> 0 & j2 <> ( width ( GoB f)) & ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * ((i2 + 1),j2)),(( GoB f) * ((i2 + 1),(j2 + 1)))));

                then

                consider k such that

                 A134: 1 <= k & (k + 1) <= ( len f) and

                 A135: j2 <> 0 and

                 A136: j2 <> ( width ( GoB f)) and

                 A137: ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * (((i1 -' 1) + 1),j2)),(( GoB f) * (((i1 -' 1) + 1),(j2 + 1))))) by A133;

                now

                  per cases by A137, SPPOL_1: 8;

                    case

                     A138: (f /. k) = (( GoB f) * (((i1 -' 1) + 1),j2)) & (f /. (k + 1)) = (( GoB f) * (((i1 -' 1) + 1),(j2 + 1)));

                    

                     A139: ( Int ( left_cell (f,k))) c= ( LeftComp f) & ( LeftComp f) c= (( LeftComp f) \/ ( RightComp f)) by A134, GOBOARD9: 21, XBOOLE_1: 7;

                    j2 < ( width ( GoB f)) by A4, A136, XXREAL_0: 1;

                    then

                     A140: (j2 + 1) <= ( width ( GoB f)) by NAT_1: 13;

                    (i1 -' 1) < ( len ( GoB f)) by A1, A127, XXREAL_0: 2;

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

                    then

                     A141: ( Indices ( GoB f)) = [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] & ((i1 -' 1) + 1) in ( dom ( GoB f)) by A129, FINSEQ_3: 25, MATRIX_0:def 4;

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

                    then (j2 + 1) in ( Seg ( width ( GoB f))) by A140, FINSEQ_1: 1;

                    then

                     A142: [((i1 -' 1) + 1), (j2 + 1)] in ( Indices ( GoB f)) by A141, ZFMISC_1: 87;

                    j2 >= ( 0 + 1) by A135, NAT_1: 13;

                    then j2 in ( Seg ( width ( GoB f))) by A4, FINSEQ_1: 1;

                    then [((i1 -' 1) + 1), j2] in ( Indices ( GoB f)) by A141, ZFMISC_1: 87;

                    then ( left_cell (f,k)) = ( cell (( GoB f),(i1 -' 1),j2)) by A134, A138, A142, GOBOARD5: 27;

                    hence ( Int ( cell (( GoB f),(i1 -' 1),j2))) c= (( LeftComp f) \/ ( RightComp f)) by A139;

                  end;

                    case

                     A143: (f /. k) = (( GoB f) * (((i1 -' 1) + 1),(j2 + 1))) & (f /. (k + 1)) = (( GoB f) * (((i1 -' 1) + 1),j2));

                    

                     A144: ( Int ( right_cell (f,k))) c= ( RightComp f) & ( RightComp f) c= (( LeftComp f) \/ ( RightComp f)) by A134, GOBOARD9: 25, XBOOLE_1: 7;

                    j2 < ( width ( GoB f)) by A4, A136, XXREAL_0: 1;

                    then

                     A145: (j2 + 1) <= ( width ( GoB f)) by NAT_1: 13;

                    

                     A146: ( Indices ( GoB f)) = [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] & ((i1 -' 1) + 1) in ( dom ( GoB f)) by A1, A131, FINSEQ_3: 25, MATRIX_0:def 4;

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

                    then (j2 + 1) in ( Seg ( width ( GoB f))) by A145, FINSEQ_1: 1;

                    then

                     A147: [((i1 -' 1) + 1), (j2 + 1)] in ( Indices ( GoB f)) by A146, ZFMISC_1: 87;

                    j2 >= ( 0 + 1) by A135, NAT_1: 13;

                    then j2 in ( Seg ( width ( GoB f))) by A4, FINSEQ_1: 1;

                    then [((i1 -' 1) + 1), j2] in ( Indices ( GoB f)) by A146, ZFMISC_1: 87;

                    then ( right_cell (f,k)) = ( cell (( GoB f),(i1 -' 1),j2)) by A134, A143, A147, GOBOARD5: 30;

                    hence ( Int ( cell (( GoB f),(i1 -' 1),j2))) c= (( LeftComp f) \/ ( RightComp f)) by A144;

                  end;

                end;

                hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f)) by A126, NAT_D: 34;

              end;

                case

                 A148: not ex k st 1 <= k & (k + 1) <= ( len f) & j2 <> 0 & j2 <> ( width ( GoB f)) & ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * ((i2 + 1),j2)),(( GoB f) * ((i2 + 1),(j2 + 1)))));

                now

                  per cases by A148;

                    case

                     A149: j2 = 0 ;

                    reconsider p = |[((( GoB f) * ((i2 + 1),1)) `1 ), (((( GoB f) * ((i2 + 1),1)) `2 ) - 1)]| as Point of ( TOP-REAL 2);

                    

                     A150: 1 < ( width ( GoB f)) by GOBOARD7: 33;

                    

                     A151: 1 < ( len ( GoB f)) by GOBOARD7: 32;

                    reconsider P = {p} as Subset of ( TOP-REAL 2);

                    

                     A152: (p `2 ) < ((p `2 ) + 1) by XREAL_1: 29;

                    

                     A153: 1 <= (i2 + 1) by NAT_1: 11;

                    then ((( GoB f) * ((i2 + 1),1)) `2 ) = ((( GoB f) * (1,1)) `2 ) by A1, A126, A150, GOBOARD5: 1;

                    then

                     A154: (p `2 ) = (((( GoB f) * (1,1)) `2 ) - 1) by EUCLID: 52;

                    p in { |[r, s]| : s <= ((( GoB f) * (1,1)) `2 ) }

                    proof

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

                      hence thesis by A154, A152;

                    end;

                    then

                     A155: p in ( h_strip (( GoB f),j2)) by A149, A151, GOBOARD5: 7;

                    (for q be Point of ( TOP-REAL 2) st q in P holds (q `2 ) < ((( GoB f) * (1,1)) `2 )) implies P misses ( L~ f) by GOBOARD8: 23;

                    then

                     A156: p in {p} & {p} c= (( L~ f) ` ) by A154, A152, SUBSET_1: 23, TARSKI:def 1;

                    then

                    reconsider p1 = p as Point of (( TOP-REAL 2) | (( L~ f) ` )) by PRE_TOPC: 8;

                     A157:

                    now

                      per cases by A1, A126, XXREAL_0: 1;

                        case

                         A158: (i2 + 1) < ( len ( GoB f)) & i2 > 0 ;

                        then

                         A159: ((i2 + 1) + 1) <= ( len ( GoB f)) by NAT_1: 13;

                        

                         A160: p in { |[r, s]| : ((( GoB f) * ((i2 + 1),1)) `1 ) <= r & r <= ((( GoB f) * (((i2 + 1) + 1),1)) `1 ) }

                        proof

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

                          then ((( GoB f) * ((i2 + 1),1)) `1 ) <= ((( GoB f) * (((i2 + 1) + 1),1)) `1 ) by A150, A153, A159, GOBOARD5: 3;

                          hence thesis;

                        end;

                        

                         A161: ( 0 + 1) <= i2 by A158, NAT_1: 13;

                        

                         A162: p in { |[r, s]| : ((( GoB f) * (i2,1)) `1 ) <= r & r <= ((( GoB f) * ((i2 + 1),1)) `1 ) }

                        proof

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

                          then ((( GoB f) * (i2,1)) `1 ) < ((( GoB f) * ((i2 + 1),1)) `1 ) by A1, A126, A150, A161, GOBOARD5: 3;

                          hence thesis;

                        end;

                        i2 < ( len ( GoB f)) by A158, NAT_1: 13;

                        then p in ( v_strip (( GoB f),i2)) by A150, A161, A162, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),i2)) /\ ( h_strip (( GoB f),j2))) by A155, XBOOLE_0:def 4;

                        then

                         A163: p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

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

                        then p in ( v_strip (( GoB f),(i2 + 1))) by A150, A158, A160, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),(i2 + 1))) /\ ( h_strip (( GoB f),j2))) by A155, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),(i2 + 1),j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i2 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A156, A163, XBOOLE_0:def 4;

                      end;

                        case

                         A164: (i2 + 1) < ( len ( GoB f)) & i2 = 0 ;

                        

                         A165: (i2 + 1) < ((i2 + 1) + 1) by NAT_1: 13;

                        

                         A166: ((i2 + 1) + 1) <= ( len ( GoB f)) by A164, NAT_1: 13;

                        p in { |[r, s]| : ((( GoB f) * ((i2 + 1),1)) `1 ) <= r & r <= ((( GoB f) * (((i2 + 1) + 1),1)) `1 ) }

                        proof

                          ((( GoB f) * ((i2 + 1),1)) `1 ) < ((( GoB f) * (((i2 + 1) + 1),1)) `1 ) by A132, A150, A166, A165, GOBOARD5: 3;

                          hence thesis;

                        end;

                        then p in ( v_strip (( GoB f),(i2 + 1))) by A150, A164, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),(i2 + 1))) /\ ( h_strip (( GoB f),j2))) by A155, XBOOLE_0:def 4;

                        then

                         A167: p in ( cell (( GoB f),(i2 + 1),j2)) by GOBOARD5:def 3;

                        p in { |[r, s]| : r <= ((( GoB f) * ((i2 + 1),1)) `1 ) };

                        then p in ( v_strip (( GoB f),i2)) by A150, A164, GOBOARD5: 10;

                        then p in (( v_strip (( GoB f),i2)) /\ ( h_strip (( GoB f),j2))) by A155, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i2 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A156, A167, XBOOLE_0:def 4;

                      end;

                        case

                         A168: (i2 + 1) = ( len ( GoB f)) & i2 > 0 ;

                        then

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

                        

                         A170: p in { |[r, s]| : ((( GoB f) * (i2,1)) `1 ) <= r & r <= ((( GoB f) * ((i2 + 1),1)) `1 ) }

                        proof

                          ((( GoB f) * (i2,1)) `1 ) < ((( GoB f) * ((i2 + 1),1)) `1 ) by A128, A150, A168, A169, GOBOARD5: 3;

                          hence thesis;

                        end;

                        p in { |[r, s]| : ((( GoB f) * ((i2 + 1),1)) `1 ) <= r };

                        then p in ( v_strip (( GoB f),(i2 + 1))) by A150, A168, GOBOARD5: 9;

                        then p in (( v_strip (( GoB f),(i2 + 1))) /\ ( h_strip (( GoB f),j2))) by A155, XBOOLE_0:def 4;

                        then

                         A171: p in ( cell (( GoB f),(i2 + 1),j2)) by GOBOARD5:def 3;

                        i2 < ( len ( GoB f)) by A168, NAT_1: 13;

                        then p in ( v_strip (( GoB f),i2)) by A150, A169, A170, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),i2)) /\ ( h_strip (( GoB f),j2))) by A155, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i2 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A156, A171, XBOOLE_0:def 4;

                      end;

                        case

                         A172: (i2 + 1) = ( len ( GoB f)) & i2 = 0 ;

                        p in { |[r, s]| : ((( GoB f) * ((i2 + 1),1)) `1 ) <= r };

                        then p in ( v_strip (( GoB f),(i2 + 1))) by A150, A172, GOBOARD5: 9;

                        then p in (( v_strip (( GoB f),(i2 + 1))) /\ ( h_strip (( GoB f),j2))) by A155, XBOOLE_0:def 4;

                        then

                         A173: p in ( cell (( GoB f),(i2 + 1),j2)) by GOBOARD5:def 3;

                        p in { |[r, s]| : r <= ((( GoB f) * (1,1)) `1 ) } by A172;

                        then p in ( v_strip (( GoB f),i2)) by A150, A172, GOBOARD5: 10;

                        then p in (( v_strip (( GoB f),i2)) /\ ( h_strip (( GoB f),j2))) by A155, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i2 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A156, A173, XBOOLE_0:def 4;

                      end;

                    end;

                    then p in ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) by A3, A4, Th2;

                    then

                     A174: ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) c= ( Component_of p1) by A3, A4, Th3, GOBRD11: 1;

                    ( Down (( RightComp f),(( L~ f) ` ))) is closed by Lm4, CONNSP_1: 33;

                    then

                     A175: ( Cl ( Down (( RightComp f),(( L~ f) ` )))) = ( Down (( RightComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    ( Down (( LeftComp f),(( L~ f) ` ))) is closed by Lm3, CONNSP_1: 33;

                    then

                     A176: ( Cl ( Down (( LeftComp f),(( L~ f) ` )))) = ( Down (( LeftComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    

                     A177: ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` ))) c= ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) & ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` ))) = ( Int ( cell (( GoB f),i2,j2))) by A3, A4, Th3, PRE_TOPC: 18;

                    (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) = ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by GOBRD11: 4;

                    then

                     A178: ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) = (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A176, A175, PRE_TOPC: 20;

                    

                     A179: ( Down (( LeftComp f),(( L~ f) ` ))) = ( LeftComp f) & ( Down (( RightComp f),(( L~ f) ` ))) = ( RightComp f) by Th5;

                    ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` ))) c= (( LeftComp f) \/ ( RightComp f)) by A1, A2, A6, A7, Th3;

                    then ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` ))) c= ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by A179, GOBRD11: 4;

                    then

                     A180: ( Cl ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` )))) c= ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) by PRE_TOPC: 19;

                    p in ( Cl ( Down (( Int ( cell (( GoB f),(i2 + 1),j2))),(( L~ f) ` )))) by A4, A157, Th2;

                    then ( Component_of p1) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A126, A180, A178, Th5, CONNSP_3: 21;

                    then ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A174;

                    hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f)) by A179, A177;

                  end;

                    case

                     A181: j2 = ( width ( GoB f));

                    reconsider p = |[((( GoB f) * ((i2 + 1),( width ( GoB f)))) `1 ), (((( GoB f) * ((i2 + 1),( width ( GoB f)))) `2 ) + 1)]| as Point of ( TOP-REAL 2);

                    

                     A182: 1 < ( width ( GoB f)) by GOBOARD7: 33;

                    reconsider P = {p} as Subset of ( TOP-REAL 2);

                    

                     A183: (for q be Point of ( TOP-REAL 2) st q in P holds ((( GoB f) * (1,( width ( GoB f)))) `2 ) < (q `2 )) implies P misses ( L~ f) by GOBOARD8: 24;

                    

                     A184: 1 < ( len ( GoB f)) by GOBOARD7: 32;

                    

                     A185: 1 <= (i2 + 1) by NAT_1: 11;

                    then ((( GoB f) * ((i2 + 1),( width ( GoB f)))) `2 ) = ((( GoB f) * (1,( width ( GoB f)))) `2 ) by A1, A126, A182, GOBOARD5: 1;

                    then

                     A186: (p `2 ) = (((( GoB f) * (1,( width ( GoB f)))) `2 ) + 1) by EUCLID: 52;

                    p in { |[r, s]| : ((( GoB f) * (1,( width ( GoB f)))) `2 ) <= s }

                    proof

                      p = |[(p `1 ), (p `2 )]| & ((( GoB f) * (1,( width ( GoB f)))) `2 ) <= (p `2 ) by A186, EUCLID: 53, XREAL_1: 29;

                      hence thesis;

                    end;

                    then

                     A187: p in ( h_strip (( GoB f),j2)) by A181, A184, GOBOARD5: 6;

                    ((( GoB f) * (1,( width ( GoB f)))) `2 ) < (((( GoB f) * (1,( width ( GoB f)))) `2 ) + 1) by XREAL_1: 29;

                    then

                     A188: p in {p} & {p} c= (( L~ f) ` ) by A186, A183, SUBSET_1: 23, TARSKI:def 1;

                    then

                    reconsider p1 = p as Point of (( TOP-REAL 2) | (( L~ f) ` )) by PRE_TOPC: 8;

                     A189:

                    now

                      per cases by A1, A126, XXREAL_0: 1;

                        case

                         A190: (i2 + 1) < ( len ( GoB f)) & i2 > 0 ;

                        then

                         A191: ((i2 + 1) + 1) <= ( len ( GoB f)) by NAT_1: 13;

                        

                         A192: p in { |[r, s]| : ((( GoB f) * ((i2 + 1),( width ( GoB f)))) `1 ) <= r & r <= ((( GoB f) * (((i2 + 1) + 1),( width ( GoB f)))) `1 ) }

                        proof

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

                          then ((( GoB f) * ((i2 + 1),( width ( GoB f)))) `1 ) <= ((( GoB f) * (((i2 + 1) + 1),( width ( GoB f)))) `1 ) by A182, A185, A191, GOBOARD5: 3;

                          hence thesis;

                        end;

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

                        then p in ( v_strip (( GoB f),(i2 + 1))) by A182, A190, A192, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),(i2 + 1))) /\ ( h_strip (( GoB f),j2))) by A187, XBOOLE_0:def 4;

                        then

                         A193: p in ( cell (( GoB f),(i2 + 1),j2)) by GOBOARD5:def 3;

                        

                         A194: ( 0 + 1) <= i2 by A190, NAT_1: 13;

                        

                         A195: i2 < (i2 + 1) by NAT_1: 13;

                        

                         A196: p in { |[r, s]| : ((( GoB f) * (i2,( width ( GoB f)))) `1 ) <= r & r <= ((( GoB f) * ((i2 + 1),( width ( GoB f)))) `1 ) }

                        proof

                          ((( GoB f) * (i2,( width ( GoB f)))) `1 ) < ((( GoB f) * ((i2 + 1),( width ( GoB f)))) `1 ) by A1, A126, A182, A194, A195, GOBOARD5: 3;

                          hence thesis;

                        end;

                        i2 < ( len ( GoB f)) by A190, NAT_1: 13;

                        then p in ( v_strip (( GoB f),i2)) by A182, A194, A196, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),i2)) /\ ( h_strip (( GoB f),j2))) by A187, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i2 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A188, A193, XBOOLE_0:def 4;

                      end;

                        case

                         A197: (i2 + 1) < ( len ( GoB f)) & i2 = 0 ;

                        then

                         A198: ((i2 + 1) + 1) <= ( len ( GoB f)) by NAT_1: 13;

                        p in { |[r, s]| : ((( GoB f) * ((i2 + 1),( width ( GoB f)))) `1 ) <= r & r <= ((( GoB f) * (((i2 + 1) + 1),( width ( GoB f)))) `1 ) }

                        proof

                          ((( GoB f) * ((i2 + 1),( width ( GoB f)))) `1 ) < ((( GoB f) * (((i2 + 1) + 1),( width ( GoB f)))) `1 ) by A132, A130, A182, A198, GOBOARD5: 3;

                          hence thesis;

                        end;

                        then p in ( v_strip (( GoB f),(i2 + 1))) by A182, A197, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),(i2 + 1))) /\ ( h_strip (( GoB f),j2))) by A187, XBOOLE_0:def 4;

                        then

                         A199: p in ( cell (( GoB f),(i2 + 1),j2)) by GOBOARD5:def 3;

                        p in { |[r, s]| : r <= ((( GoB f) * (1,( width ( GoB f)))) `1 ) } by A197;

                        then p in ( v_strip (( GoB f),i2)) by A182, A197, GOBOARD5: 10;

                        then p in (( v_strip (( GoB f),i2)) /\ ( h_strip (( GoB f),j2))) by A187, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i2 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A188, A199, XBOOLE_0:def 4;

                      end;

                        case

                         A200: (i2 + 1) = ( len ( GoB f)) & i2 > 0 ;

                        then

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

                        

                         A202: p in { |[r, s]| : ((( GoB f) * (i2,( width ( GoB f)))) `1 ) <= r & r <= ((( GoB f) * ((i2 + 1),( width ( GoB f)))) `1 ) }

                        proof

                          ((( GoB f) * (i2,( width ( GoB f)))) `1 ) <= ((( GoB f) * ((i2 + 1),( width ( GoB f)))) `1 ) by A128, A182, A200, A201, GOBOARD5: 3;

                          hence thesis;

                        end;

                        p in { |[r, s]| : ((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) `1 ) <= r } by A200;

                        then p in ( v_strip (( GoB f),(i2 + 1))) by A182, A200, GOBOARD5: 9;

                        then p in (( v_strip (( GoB f),(i2 + 1))) /\ ( h_strip (( GoB f),j2))) by A187, XBOOLE_0:def 4;

                        then

                         A203: p in ( cell (( GoB f),(i2 + 1),j2)) by GOBOARD5:def 3;

                        i2 < ( len ( GoB f)) by A200, NAT_1: 13;

                        then p in ( v_strip (( GoB f),i2)) by A182, A201, A202, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),i2)) /\ ( h_strip (( GoB f),j2))) by A187, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i2 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A188, A203, XBOOLE_0:def 4;

                      end;

                        case (i2 + 1) = ( len ( GoB f)) & i2 = 0 ;

                        hence contradiction by GOBOARD7: 32;

                      end;

                    end;

                    then p in ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) by A3, A4, Th2;

                    then

                     A204: ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) c= ( Component_of p1) by A3, A4, Th3, GOBRD11: 1;

                    ( Down (( RightComp f),(( L~ f) ` ))) is closed by Lm4, CONNSP_1: 33;

                    then

                     A205: ( Cl ( Down (( RightComp f),(( L~ f) ` )))) = ( Down (( RightComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    ( Down (( LeftComp f),(( L~ f) ` ))) is closed by Lm3, CONNSP_1: 33;

                    then

                     A206: ( Cl ( Down (( LeftComp f),(( L~ f) ` )))) = ( Down (( LeftComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    

                     A207: ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` ))) c= ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) & ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` ))) = ( Int ( cell (( GoB f),i2,j2))) by A3, A4, Th3, PRE_TOPC: 18;

                    (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) = ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by GOBRD11: 4;

                    then

                     A208: ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) = (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A206, A205, PRE_TOPC: 20;

                    

                     A209: ( Down (( LeftComp f),(( L~ f) ` ))) = ( LeftComp f) & ( Down (( RightComp f),(( L~ f) ` ))) = ( RightComp f) by Th5;

                    ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` ))) c= (( LeftComp f) \/ ( RightComp f)) by A1, A2, A6, A7, Th3;

                    then ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` ))) c= ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by A209, GOBRD11: 4;

                    then

                     A210: ( Cl ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` )))) c= ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) by PRE_TOPC: 19;

                    p in ( Cl ( Down (( Int ( cell (( GoB f),(i2 + 1),j2))),(( L~ f) ` )))) by A4, A189, Th2;

                    then ( Component_of p1) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A126, A210, A208, Th5, CONNSP_3: 21;

                    then ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A204;

                    hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f)) by A209, A207;

                  end;

                    case

                     A211: j2 <> 0 & j2 <> ( width ( GoB f)) & not ex k st 1 <= k & (k + 1) <= ( len f) & ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * ((i2 + 1),j2)),(( GoB f) * ((i2 + 1),(j2 + 1)))));

                    then

                     A212: j2 < ( width ( GoB f)) by A4, XXREAL_0: 1;

                    then

                     A213: (j2 + 1) <= ( width ( GoB f)) by NAT_1: 13;

                    for k st 1 <= k & (k + 1) <= ( len f) holds ( LSeg ((( GoB f) * ((i2 + 1),j2)),(( GoB f) * ((i2 + 1),(j2 + 1))))) <> ( LSeg (f,k))

                    proof

                      let k;

                      assume

                       A214: 1 <= k & (k + 1) <= ( len f);

                      then ( LSeg (f,k)) = ( LSeg ((f /. k),(f /. (k + 1)))) by TOPREAL1:def 3;

                      hence thesis by A211, A214;

                    end;

                    then

                     A215: 1 <= (i2 + 1) & (i2 + 1) <= ( len ( GoB f)) & 1 <= j2 & (j2 + 1) <= ( width ( GoB f)) implies not ((1 / 2) * ((( GoB f) * ((i2 + 1),j2)) + (( GoB f) * ((i2 + 1),(j2 + 1))))) in ( L~ f) by GOBOARD7: 39;

                    reconsider p = ((1 / 2) * ((( GoB f) * ((i2 + 1),j2)) + (( GoB f) * ((i2 + 1),(j2 + 1))))) as Point of ( TOP-REAL 2);

                    

                     A216: (p `2 ) = ((1 / 2) * (((( GoB f) * ((i2 + 1),j2)) + (( GoB f) * ((i2 + 1),(j2 + 1)))) `2 )) by TOPREAL3: 4

                    .= ((1 / 2) * (((( GoB f) * ((i2 + 1),j2)) `2 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 ))) by TOPREAL3: 2;

                    reconsider P = {p} as Subset of ( TOP-REAL 2);

                    

                     A217: 1 < ( width ( GoB f)) by GOBOARD7: 33;

                    ( Down (( RightComp f),(( L~ f) ` ))) is closed by Lm4, CONNSP_1: 33;

                    then

                     A218: ( Cl ( Down (( RightComp f),(( L~ f) ` )))) = ( Down (( RightComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    ( Down (( LeftComp f),(( L~ f) ` ))) is closed by Lm3, CONNSP_1: 33;

                    then

                     A219: ( Cl ( Down (( LeftComp f),(( L~ f) ` )))) = ( Down (( LeftComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) = ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by GOBRD11: 4;

                    then

                     A220: ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) = (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A219, A218, PRE_TOPC: 20;

                    

                     A221: 1 <= (i2 + 1) by NAT_1: 11;

                    (p `1 ) = ((1 / 2) * (((( GoB f) * ((i2 + 1),j2)) + (( GoB f) * ((i2 + 1),(j2 + 1)))) `1 )) by TOPREAL3: 4

                    .= ((1 / 2) * (((( GoB f) * ((i2 + 1),j2)) `1 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 ))) by TOPREAL3: 2;

                    then

                     A222: p = |[((1 / 2) * (((( GoB f) * ((i2 + 1),j2)) `1 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 ))), ((1 / 2) * (((( GoB f) * ((i2 + 1),j2)) `2 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 )))]| by A216, EUCLID: 53;

                    

                     A223: ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` ))) c= ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) & ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` ))) = ( Int ( cell (( GoB f),i2,j2))) by A3, A4, Th3, PRE_TOPC: 18;

                    

                     A224: ( Down (( LeftComp f),(( L~ f) ` ))) = ( LeftComp f) & ( Down (( RightComp f),(( L~ f) ` ))) = ( RightComp f) by Th5;

                    ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` ))) c= (( LeftComp f) \/ ( RightComp f)) by A1, A2, A6, A7, Th3;

                    then ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` ))) c= ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by A224, GOBRD11: 4;

                    then

                     A225: ( Cl ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` )))) c= ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) by PRE_TOPC: 19;

                    

                     A226: ( 0 + 1) <= j2 by A211, NAT_1: 13;

                    then

                     A227: 1 < (j2 + 1) by NAT_1: 13;

                    (for x be object st x in P holds not x in ( L~ f)) implies P misses ( L~ f) by XBOOLE_0: 3;

                    then

                     A228: p in {p} & {p} c= (( L~ f) ` ) by A1, A126, A226, A212, A215, NAT_1: 13, SUBSET_1: 23, TARSKI:def 1;

                    then

                    reconsider p1 = p as Point of (( TOP-REAL 2) | (( L~ f) ` )) by PRE_TOPC: 8;

                    

                     A229: 1 <= (1 + i2) by NAT_1: 11;

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

                    then

                     A230: ((( GoB f) * ((i2 + 1),j2)) `2 ) < ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 ) by A1, A126, A226, A213, A229, GOBOARD5: 4;

                    then (((( GoB f) * ((i2 + 1),j2)) `2 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 )) < (((( GoB f) * ((i2 + 1),(j2 + 1))) `2 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 )) by XREAL_1: 8;

                    then

                     A231: ((((( GoB f) * ((i2 + 1),j2)) `2 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 )) / 2) < ((((( GoB f) * ((i2 + 1),(j2 + 1))) `2 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 )) / 2) by XREAL_1: 74;

                    (((( GoB f) * ((i2 + 1),j2)) `2 ) + ((( GoB f) * ((i2 + 1),j2)) `2 )) < (((( GoB f) * ((i2 + 1),j2)) `2 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 )) by A230, XREAL_1: 8;

                    then

                     A232: ((((( GoB f) * ((i2 + 1),j2)) `2 ) + ((( GoB f) * ((i2 + 1),j2)) `2 )) / 2) < ((((( GoB f) * ((i2 + 1),j2)) `2 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 )) / 2) by XREAL_1: 74;

                    p in { |[r, s]| : ((( GoB f) * ((i2 + 1),j2)) `2 ) <= s & s <= ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 ) }

                    proof

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

                      hence thesis by A216, A232, A231;

                    end;

                    then

                     A233: p in ( h_strip (( GoB f),j2)) by A1, A126, A226, A212, A221, GOBOARD5: 5;

                    

                     A234: i2 = 0 or i2 >= ( 0 + 1) by NAT_1: 13;

                     A235:

                    now

                      per cases by A1, A126, A234, XXREAL_0: 1;

                        case

                         A236: i2 >= 1 & (i2 + 1) < ( len ( GoB f));

                        then

                         A237: ((i2 + 1) + 1) <= ( len ( GoB f)) by NAT_1: 13;

                        

                         A238: p in { |[r, s]| : ((( GoB f) * ((i2 + 1),1)) `1 ) <= r & r <= ((( GoB f) * (((i2 + 1) + 1),1)) `1 ) }

                        proof

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

                          then

                           A239: ((( GoB f) * ((i2 + 1),1)) `1 ) < ((( GoB f) * (((i2 + 1) + 1),1)) `1 ) by A217, A229, A237, GOBOARD5: 3;

                          ((( GoB f) * ((i2 + 1),j2)) `1 ) = ((( GoB f) * ((i2 + 1),1)) `1 ) & ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 ) = ((( GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5: 2;

                          hence thesis by A222, A239;

                        end;

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

                        then p in ( v_strip (( GoB f),(i2 + 1))) by A217, A236, A238, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),(i2 + 1))) /\ ( h_strip (( GoB f),j2))) by A233, XBOOLE_0:def 4;

                        then

                         A240: p in ( cell (( GoB f),(i2 + 1),j2)) by GOBOARD5:def 3;

                        

                         A241: p in { |[r, s]| : ((( GoB f) * (i2,1)) `1 ) <= r & r <= ((( GoB f) * ((i2 + 1),1)) `1 ) }

                        proof

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

                          then

                           A242: ((( GoB f) * (i2,1)) `1 ) < ((( GoB f) * ((i2 + 1),1)) `1 ) by A217, A236, GOBOARD5: 3;

                          ((( GoB f) * ((i2 + 1),j2)) `1 ) = ((( GoB f) * ((i2 + 1),1)) `1 ) & ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 ) = ((( GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5: 2;

                          hence thesis by A222, A242;

                        end;

                        i2 < ( len ( GoB f)) by A236, NAT_1: 13;

                        then p in ( v_strip (( GoB f),i2)) by A217, A236, A241, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),i2)) /\ ( h_strip (( GoB f),j2))) by A233, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i2 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A228, A240, XBOOLE_0:def 4;

                      end;

                        case

                         A243: i2 >= 1 & (i2 + 1) = ( len ( GoB f));

                        

                         A244: i2 < (i2 + 1) by NAT_1: 13;

                        p in { |[r, s]| : ((( GoB f) * (i2,1)) `1 ) <= r & r <= ((( GoB f) * ((i2 + 1),1)) `1 ) }

                        proof

                          

                           A245: ((( GoB f) * (i2,1)) `1 ) < ((( GoB f) * ((i2 + 1),1)) `1 ) by A217, A243, A244, GOBOARD5: 3;

                          ((( GoB f) * ((i2 + 1),j2)) `1 ) = ((( GoB f) * ((i2 + 1),1)) `1 ) & ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 ) = ((( GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5: 2;

                          hence thesis by A222, A245;

                        end;

                        then p in ( v_strip (( GoB f),i2)) by A217, A243, A244, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),i2)) /\ ( h_strip (( GoB f),j2))) by A233, XBOOLE_0:def 4;

                        then

                         A246: p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        p in { |[r, s]| : ((( GoB f) * ((i2 + 1),1)) `1 ) <= r }

                        proof

                          ((( GoB f) * ((i2 + 1),j2)) `1 ) = ((( GoB f) * ((i2 + 1),1)) `1 ) & ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 ) = ((( GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5: 2;

                          hence thesis by A222;

                        end;

                        then p in ( v_strip (( GoB f),(i2 + 1))) by A217, A243, GOBOARD5: 9;

                        then p in (( v_strip (( GoB f),(i2 + 1))) /\ ( h_strip (( GoB f),j2))) by A233, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),(i2 + 1),j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i2 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A228, A246, XBOOLE_0:def 4;

                      end;

                        case

                         A247: i2 = 0 & (i2 + 1) < ( len ( GoB f));

                        then

                         A248: ((i2 + 1) + 1) <= ( len ( GoB f)) by NAT_1: 13;

                        p in { |[r, s]| : ((( GoB f) * ((i2 + 1),1)) `1 ) <= r & r <= ((( GoB f) * (((i2 + 1) + 1),1)) `1 ) }

                        proof

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

                          then

                           A249: ((( GoB f) * ((i2 + 1),1)) `1 ) < ((( GoB f) * (((i2 + 1) + 1),1)) `1 ) by A217, A229, A248, GOBOARD5: 3;

                          ((( GoB f) * ((i2 + 1),j2)) `1 ) = ((( GoB f) * ((i2 + 1),1)) `1 ) & ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 ) = ((( GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5: 2;

                          hence thesis by A222, A249;

                        end;

                        then p in ( v_strip (( GoB f),i1)) by A126, A217, A247, GOBOARD5: 8;

                        then p in (( v_strip (( GoB f),(i2 + 1))) /\ ( h_strip (( GoB f),j2))) by A126, A233, XBOOLE_0:def 4;

                        then

                         A250: p in ( cell (( GoB f),(i2 + 1),j2)) by GOBOARD5:def 3;

                        p in { |[r, s]| : r <= ((( GoB f) * (1,1)) `1 ) }

                        proof

                          ((( GoB f) * ((i2 + 1),j2)) `1 ) = ((( GoB f) * ((i2 + 1),1)) `1 ) & ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 ) = ((( GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5: 2;

                          hence thesis by A222, A247;

                        end;

                        then p in ( v_strip (( GoB f),i2)) by A217, A247, GOBOARD5: 10;

                        then p in (( v_strip (( GoB f),i2)) /\ ( h_strip (( GoB f),j2))) by A233, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),(i2 + 1),j2)) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A228, A250, XBOOLE_0:def 4;

                      end;

                        case i2 = 0 & (i2 + 1) = ( len ( GoB f));

                        hence contradiction by GOBOARD7: 32;

                      end;

                    end;

                    then p in ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) by A3, A4, Th2;

                    then

                     A251: ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) c= ( Component_of p1) by A3, A4, Th3, GOBRD11: 1;

                    p in ( Cl ( Down (( Int ( cell (( GoB f),i1,j2))),(( L~ f) ` )))) by A4, A126, A235, Th2;

                    then ( Component_of p1) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A225, A220, Th5, CONNSP_3: 21;

                    then ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A251;

                    hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f)) by A224, A223;

                  end;

                end;

                hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f));

              end;

            end;

            hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f));

          end;

        end;

        hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f));

      end;

      hence thesis;

    end;

    

     Lm6: for i1, j1, i2, j2 st i1 <= ( len ( GoB f)) & j1 <= ( width ( GoB f)) & i2 <= ( len ( GoB f)) & j2 <= ( width ( GoB f)) & (j2 = (j1 + 1) or j1 = (j2 + 1)) & i1 = i2 holds ( Int ( cell (( GoB f),i1,j1))) c= (( LeftComp f) \/ ( RightComp f)) implies ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f))

    proof

      let i1, j1, i2, j2;

      assume that

       A1: i1 <= ( len ( GoB f)) and

       A2: j1 <= ( width ( GoB f)) and

       A3: i2 <= ( len ( GoB f)) and

       A4: j2 <= ( width ( GoB f)) and

       A5: j2 = (j1 + 1) or j1 = (j2 + 1) and

       A6: i1 = i2;

      now

        assume

         A7: ( Int ( cell (( GoB f),i1,j1))) c= (( LeftComp f) \/ ( RightComp f));

        now

          per cases by A5;

            case

             A8: j2 = (j1 + 1);

            now

              per cases ;

                case ex k st 1 <= k & (k + 1) <= ( len f) & i2 <> 0 & i2 <> ( len ( GoB f)) & ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * (i2,(j1 + 1))),(( GoB f) * ((i2 + 1),(j1 + 1)))));

                then

                consider k such that

                 A9: 1 <= k & (k + 1) <= ( len f) and

                 A10: i2 <> 0 and

                 A11: i2 <> ( len ( GoB f)) and

                 A12: ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * (i2,(j1 + 1))),(( GoB f) * ((i2 + 1),(j1 + 1)))));

                now

                  per cases by A12, SPPOL_1: 8;

                    case

                     A13: (f /. k) = (( GoB f) * (i2,(j1 + 1))) & (f /. (k + 1)) = (( GoB f) * ((i2 + 1),(j1 + 1)));

                    

                     A14: ( Int ( left_cell (f,k))) c= ( LeftComp f) & ( LeftComp f) c= (( LeftComp f) \/ ( RightComp f)) by A9, GOBOARD9: 21, XBOOLE_1: 7;

                    i2 < ( len ( GoB f)) by A3, A11, XXREAL_0: 1;

                    then

                     A15: (i2 + 1) <= ( len ( GoB f)) by NAT_1: 13;

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

                    then

                     A16: ( Indices ( GoB f)) = [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] & (j1 + 1) in ( Seg ( width ( GoB f))) by A4, A8, FINSEQ_1: 1, MATRIX_0:def 4;

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

                    then (i2 + 1) in ( dom ( GoB f)) by A15, FINSEQ_3: 25;

                    then

                     A17: [(i2 + 1), (j1 + 1)] in ( Indices ( GoB f)) by A16, ZFMISC_1: 87;

                    i2 >= ( 0 + 1) by A10, NAT_1: 13;

                    then i2 in ( dom ( GoB f)) by A3, FINSEQ_3: 25;

                    then [i2, (j1 + 1)] in ( Indices ( GoB f)) by A16, ZFMISC_1: 87;

                    then ( left_cell (f,k)) = ( cell (( GoB f),i2,(j1 + 1))) by A9, A13, A17, GOBOARD5: 28;

                    hence ( Int ( cell (( GoB f),i2,(j1 + 1)))) c= (( LeftComp f) \/ ( RightComp f)) by A14;

                  end;

                    case

                     A18: (f /. k) = (( GoB f) * ((i2 + 1),(j1 + 1))) & (f /. (k + 1)) = (( GoB f) * (i2,(j1 + 1)));

                    

                     A19: ( Int ( right_cell (f,k))) c= ( RightComp f) & ( RightComp f) c= (( LeftComp f) \/ ( RightComp f)) by A9, GOBOARD9: 25, XBOOLE_1: 7;

                    i2 < ( len ( GoB f)) by A3, A11, XXREAL_0: 1;

                    then

                     A20: (i2 + 1) <= ( len ( GoB f)) by NAT_1: 13;

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

                    then

                     A21: ( Indices ( GoB f)) = [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] & (j1 + 1) in ( Seg ( width ( GoB f))) by A4, A8, FINSEQ_1: 1, MATRIX_0:def 4;

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

                    then (i2 + 1) in ( dom ( GoB f)) by A20, FINSEQ_3: 25;

                    then

                     A22: [(i2 + 1), (j1 + 1)] in ( Indices ( GoB f)) by A21, ZFMISC_1: 87;

                    i2 >= ( 0 + 1) by A10, NAT_1: 13;

                    then i2 in ( dom ( GoB f)) by A3, FINSEQ_3: 25;

                    then [i2, (j1 + 1)] in ( Indices ( GoB f)) by A21, ZFMISC_1: 87;

                    then ( right_cell (f,k)) = ( cell (( GoB f),i2,(j1 + 1))) by A9, A18, A22, GOBOARD5: 29;

                    hence ( Int ( cell (( GoB f),i2,(j1 + 1)))) c= (( LeftComp f) \/ ( RightComp f)) by A19;

                  end;

                end;

                hence ( Int ( cell (( GoB f),i2,(j1 + 1)))) c= (( LeftComp f) \/ ( RightComp f));

              end;

                case

                 A23: not ex k st 1 <= k & (k + 1) <= ( len f) & i2 <> 0 & i2 <> ( len ( GoB f)) & ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * (i2,(j1 + 1))),(( GoB f) * ((i2 + 1),(j1 + 1)))));

                now

                  per cases by A23;

                    case

                     A24: i2 = 0 ;

                    reconsider p = |[(((( GoB f) * (1,(j1 + 1))) `1 ) - 1), ((( GoB f) * (1,(j1 + 1))) `2 )]| as Point of ( TOP-REAL 2);

                    

                     A25: 1 < ( len ( GoB f)) by GOBOARD7: 32;

                    

                     A26: 1 < ( width ( GoB f)) by GOBOARD7: 33;

                    reconsider P = {p} as Subset of ( TOP-REAL 2);

                    

                     A27: (p `1 ) < ((p `1 ) + 1) by XREAL_1: 29;

                    

                     A28: 1 <= (1 + j1) by NAT_1: 11;

                    then ((( GoB f) * (1,(j1 + 1))) `1 ) = ((( GoB f) * (1,1)) `1 ) by A4, A8, A25, GOBOARD5: 2;

                    then

                     A29: (p `1 ) = (((( GoB f) * (1,1)) `1 ) - 1) by EUCLID: 52;

                    p in { |[s, r]| where s,r be Real : s <= ((( GoB f) * (1,1)) `1 ) }

                    proof

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

                      hence thesis by A29, A27;

                    end;

                    then

                     A30: p in ( v_strip (( GoB f),i2)) by A24, A26, GOBOARD5: 10;

                    (for q be Point of ( TOP-REAL 2) st q in P holds (q `1 ) < ((( GoB f) * (1,1)) `1 )) implies P misses ( L~ f) by GOBOARD8: 21;

                    then

                     A31: p in {p} & {p} c= (( L~ f) ` ) by A29, A27, SUBSET_1: 23, TARSKI:def 1;

                    then

                    reconsider p1 = p as Point of (( TOP-REAL 2) | (( L~ f) ` )) by PRE_TOPC: 8;

                    

                     A32: j1 = 0 or j1 >= ( 0 + 1) by NAT_1: 13;

                     A33:

                    now

                      per cases by A4, A8, A32, XXREAL_0: 1;

                        case

                         A34: j1 >= 1 & (j1 + 1) < ( width ( GoB f));

                        then

                         A35: ((j1 + 1) + 1) <= ( width ( GoB f)) by NAT_1: 13;

                        

                         A36: p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,(j1 + 1))) `2 ) <= r & r <= ((( GoB f) * (1,((j1 + 1) + 1))) `2 ) }

                        proof

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

                          then ((( GoB f) * (1,(j1 + 1))) `2 ) <= ((( GoB f) * (1,((j1 + 1) + 1))) `2 ) by A25, A28, A35, GOBOARD5: 4;

                          hence thesis;

                        end;

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

                        then p in ( h_strip (( GoB f),(j1 + 1))) by A25, A34, A36, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),(j1 + 1))) /\ ( v_strip (( GoB f),i2))) by A30, XBOOLE_0:def 4;

                        then

                         A37: p in ( cell (( GoB f),i2,(j1 + 1))) by GOBOARD5:def 3;

                        

                         A38: p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,j1)) `2 ) <= r & r <= ((( GoB f) * (1,(j1 + 1))) `2 ) }

                        proof

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

                          then ((( GoB f) * (1,j1)) `2 ) < ((( GoB f) * (1,(j1 + 1))) `2 ) by A25, A34, GOBOARD5: 4;

                          hence thesis;

                        end;

                        j1 < ( width ( GoB f)) by A34, NAT_1: 13;

                        then p in ( h_strip (( GoB f),j1)) by A25, A34, A38, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),j1)) /\ ( v_strip (( GoB f),i2))) by A30, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j1)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j1 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j1)) /\ (( L~ f) ` )) by A31, A37, XBOOLE_0:def 4;

                      end;

                        case

                         A39: j1 >= 1 & (j1 + 1) = ( width ( GoB f));

                        

                         A40: j1 < (j1 + 1) by NAT_1: 13;

                        

                         A41: p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,j1)) `2 ) <= r & r <= ((( GoB f) * (1,(j1 + 1))) `2 ) }

                        proof

                          ((( GoB f) * (1,j1)) `2 ) < ((( GoB f) * (1,(j1 + 1))) `2 ) by A25, A39, A40, GOBOARD5: 4;

                          hence thesis;

                        end;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,(j1 + 1))) `2 ) <= r };

                        then p in ( h_strip (( GoB f),(j1 + 1))) by A25, A39, GOBOARD5: 6;

                        then p in (( h_strip (( GoB f),(j1 + 1))) /\ ( v_strip (( GoB f),i2))) by A30, XBOOLE_0:def 4;

                        then

                         A42: p in ( cell (( GoB f),i2,(j1 + 1))) by GOBOARD5:def 3;

                        j1 < ( width ( GoB f)) by A39, NAT_1: 13;

                        then p in ( h_strip (( GoB f),j1)) by A25, A39, A41, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),j1)) /\ ( v_strip (( GoB f),i2))) by A30, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j1)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j1 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j1)) /\ (( L~ f) ` )) by A31, A42, XBOOLE_0:def 4;

                      end;

                        case

                         A43: j1 = 0 & (j1 + 1) < ( width ( GoB f));

                        then

                         A44: ((j1 + 1) + 1) <= ( width ( GoB f)) by NAT_1: 13;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,(j1 + 1))) `2 ) <= r & r <= ((( GoB f) * (1,((j1 + 1) + 1))) `2 ) }

                        proof

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

                          then ((( GoB f) * (1,(j1 + 1))) `2 ) <= ((( GoB f) * (1,((j1 + 1) + 1))) `2 ) by A25, A28, A44, GOBOARD5: 4;

                          hence thesis;

                        end;

                        then p in ( h_strip (( GoB f),(j1 + 1))) by A25, A43, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),(j1 + 1))) /\ ( v_strip (( GoB f),i2))) by A30, XBOOLE_0:def 4;

                        then

                         A45: p in ( cell (( GoB f),i2,(j1 + 1))) by GOBOARD5:def 3;

                        p in { |[s, r]| where s,r be Real : r <= ((( GoB f) * (1,1)) `2 ) } by A43;

                        then p in ( h_strip (( GoB f),j1)) by A25, A43, GOBOARD5: 7;

                        then p in (( h_strip (( GoB f),j1)) /\ ( v_strip (( GoB f),i2))) by A30, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j1)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j1 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j1)) /\ (( L~ f) ` )) by A31, A45, XBOOLE_0:def 4;

                      end;

                        case

                         A46: j1 = 0 & (j1 + 1) = ( width ( GoB f));

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,(j1 + 1))) `2 ) <= r };

                        then p in ( h_strip (( GoB f),(j1 + 1))) by A25, A46, GOBOARD5: 6;

                        then p in (( h_strip (( GoB f),(j1 + 1))) /\ ( v_strip (( GoB f),i2))) by A30, XBOOLE_0:def 4;

                        then

                         A47: p in ( cell (( GoB f),i2,(j1 + 1))) by GOBOARD5:def 3;

                        p in { |[s, r]| where s,r be Real : r <= ((( GoB f) * (1,1)) `2 ) } by A46;

                        then p in ( h_strip (( GoB f),j1)) by A25, A46, GOBOARD5: 7;

                        then p in (( h_strip (( GoB f),j1)) /\ ( v_strip (( GoB f),i2))) by A30, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j1)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j1 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j1)) /\ (( L~ f) ` )) by A31, A47, XBOOLE_0:def 4;

                      end;

                    end;

                    then p in ( Cl ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` )))) by A3, Th2;

                    then

                     A48: ( Cl ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` )))) c= ( Component_of p1) by A3, A4, A8, Th3, GOBRD11: 1;

                    ( Down (( RightComp f),(( L~ f) ` ))) is closed by Lm4, CONNSP_1: 33;

                    then

                     A49: ( Cl ( Down (( RightComp f),(( L~ f) ` )))) = ( Down (( RightComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    ( Down (( LeftComp f),(( L~ f) ` ))) is closed by Lm3, CONNSP_1: 33;

                    then

                     A50: ( Cl ( Down (( LeftComp f),(( L~ f) ` )))) = ( Down (( LeftComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) = ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by GOBRD11: 4;

                    then

                     A51: ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) = (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A50, A49, PRE_TOPC: 20;

                    

                     A52: ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` ))) c= ( Cl ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` )))) & ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` ))) = ( Int ( cell (( GoB f),i2,(j1 + 1)))) by A3, A4, A8, Th3, PRE_TOPC: 18;

                    

                     A53: ( Down (( LeftComp f),(( L~ f) ` ))) = ( LeftComp f) & ( Down (( RightComp f),(( L~ f) ` ))) = ( RightComp f) by Th5;

                    ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` ))) c= (( LeftComp f) \/ ( RightComp f)) by A1, A2, A6, A7, Th3;

                    then ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` ))) c= ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by A53, GOBRD11: 4;

                    then

                     A54: ( Cl ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` )))) c= ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) by PRE_TOPC: 19;

                    p in ( Cl ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` )))) by A2, A3, A33, Th2;

                    then ( Component_of p1) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A54, A51, Th5, CONNSP_3: 21;

                    then ( Cl ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` )))) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A48;

                    hence ( Int ( cell (( GoB f),i2,(j1 + 1)))) c= (( LeftComp f) \/ ( RightComp f)) by A53, A52;

                  end;

                    case

                     A55: i2 = ( len ( GoB f));

                    reconsider p = |[(((( GoB f) * (( len ( GoB f)),(j1 + 1))) `1 ) + 1), ((( GoB f) * (( len ( GoB f)),(j1 + 1))) `2 )]| as Point of ( TOP-REAL 2);

                    

                     A56: 1 < ( len ( GoB f)) by GOBOARD7: 32;

                    reconsider P = {p} as Subset of ( TOP-REAL 2);

                    

                     A57: (for q be Point of ( TOP-REAL 2) st q in P holds ((( GoB f) * (( len ( GoB f)),1)) `1 ) < (q `1 )) implies P misses ( L~ f) by GOBOARD8: 22;

                    

                     A58: 1 < ( width ( GoB f)) by GOBOARD7: 33;

                    

                     A59: 1 <= (1 + j1) by NAT_1: 11;

                    then ((( GoB f) * (( len ( GoB f)),(j1 + 1))) `1 ) = ((( GoB f) * (( len ( GoB f)),1)) `1 ) by A4, A8, A56, GOBOARD5: 2;

                    then

                     A60: (p `1 ) = (((( GoB f) * (( len ( GoB f)),1)) `1 ) + 1) by EUCLID: 52;

                    then

                     A61: ((( GoB f) * (( len ( GoB f)),1)) `1 ) < (p `1 ) by XREAL_1: 29;

                    p in { |[s, r]| where s,r be Real : ((( GoB f) * (( len ( GoB f)),1)) `1 ) <= s }

                    proof

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

                      hence thesis by A61;

                    end;

                    then

                     A62: p in ( v_strip (( GoB f),i2)) by A55, A58, GOBOARD5: 9;

                    ((( GoB f) * (( len ( GoB f)),1)) `1 ) < (((( GoB f) * (( len ( GoB f)),1)) `1 ) + 1) by XREAL_1: 29;

                    then

                     A63: p in {p} & {p} c= (( L~ f) ` ) by A60, A57, SUBSET_1: 23, TARSKI:def 1;

                    then

                    reconsider p1 = p as Point of (( TOP-REAL 2) | (( L~ f) ` )) by PRE_TOPC: 8;

                    

                     A64: j1 = 0 or j1 >= ( 0 + 1) by NAT_1: 13;

                     A65:

                    now

                      per cases by A4, A8, A64, XXREAL_0: 1;

                        case

                         A66: j1 >= 1 & (j1 + 1) < ( width ( GoB f));

                        then

                         A67: ((j1 + 1) + 1) <= ( width ( GoB f)) by NAT_1: 13;

                        

                         A68: p in { |[s, r]| where s,r be Real : ((( GoB f) * (( len ( GoB f)),(j1 + 1))) `2 ) <= r & r <= ((( GoB f) * (( len ( GoB f)),((j1 + 1) + 1))) `2 ) }

                        proof

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

                          then ((( GoB f) * (( len ( GoB f)),(j1 + 1))) `2 ) <= ((( GoB f) * (( len ( GoB f)),((j1 + 1) + 1))) `2 ) by A56, A59, A67, GOBOARD5: 4;

                          hence thesis;

                        end;

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

                        then p in ( h_strip (( GoB f),(j1 + 1))) by A56, A66, A68, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),(j1 + 1))) /\ ( v_strip (( GoB f),i2))) by A62, XBOOLE_0:def 4;

                        then

                         A69: p in ( cell (( GoB f),i2,(j1 + 1))) by GOBOARD5:def 3;

                        

                         A70: p in { |[s, r]| where s,r be Real : ((( GoB f) * (( len ( GoB f)),j1)) `2 ) <= r & r <= ((( GoB f) * (( len ( GoB f)),(j1 + 1))) `2 ) }

                        proof

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

                          then ((( GoB f) * (( len ( GoB f)),j1)) `2 ) < ((( GoB f) * (( len ( GoB f)),(j1 + 1))) `2 ) by A56, A66, GOBOARD5: 4;

                          hence thesis;

                        end;

                        j1 < ( width ( GoB f)) by A66, NAT_1: 13;

                        then p in ( h_strip (( GoB f),j1)) by A56, A66, A70, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),j1)) /\ ( v_strip (( GoB f),i2))) by A62, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j1)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j1 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j1)) /\ (( L~ f) ` )) by A63, A69, XBOOLE_0:def 4;

                      end;

                        case

                         A71: j1 >= 1 & (j1 + 1) = ( width ( GoB f));

                        

                         A72: j1 < (j1 + 1) by NAT_1: 13;

                        

                         A73: p in { |[s, r]| where s,r be Real : ((( GoB f) * (( len ( GoB f)),j1)) `2 ) <= r & r <= ((( GoB f) * (( len ( GoB f)),(j1 + 1))) `2 ) }

                        proof

                          ((( GoB f) * (( len ( GoB f)),j1)) `2 ) < ((( GoB f) * (( len ( GoB f)),(j1 + 1))) `2 ) by A56, A71, A72, GOBOARD5: 4;

                          hence thesis;

                        end;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (( len ( GoB f)),(j1 + 1))) `2 ) <= r };

                        then p in ( h_strip (( GoB f),(j1 + 1))) by A56, A71, GOBOARD5: 6;

                        then p in (( h_strip (( GoB f),(j1 + 1))) /\ ( v_strip (( GoB f),i2))) by A62, XBOOLE_0:def 4;

                        then

                         A74: p in ( cell (( GoB f),i2,(j1 + 1))) by GOBOARD5:def 3;

                        j1 < ( width ( GoB f)) by A71, NAT_1: 13;

                        then p in ( h_strip (( GoB f),j1)) by A56, A71, A73, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),j1)) /\ ( v_strip (( GoB f),i2))) by A62, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j1)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j1 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j1)) /\ (( L~ f) ` )) by A63, A74, XBOOLE_0:def 4;

                      end;

                        case

                         A75: j1 = 0 & (j1 + 1) < ( width ( GoB f));

                        then

                         A76: ((j1 + 1) + 1) <= ( width ( GoB f)) by NAT_1: 13;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (( len ( GoB f)),(j1 + 1))) `2 ) <= r & r <= ((( GoB f) * (( len ( GoB f)),((j1 + 1) + 1))) `2 ) }

                        proof

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

                          then ((( GoB f) * (( len ( GoB f)),(j1 + 1))) `2 ) <= ((( GoB f) * (( len ( GoB f)),((j1 + 1) + 1))) `2 ) by A56, A59, A76, GOBOARD5: 4;

                          hence thesis;

                        end;

                        then p in ( h_strip (( GoB f),(j1 + 1))) by A56, A75, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),(j1 + 1))) /\ ( v_strip (( GoB f),i2))) by A62, XBOOLE_0:def 4;

                        then

                         A77: p in ( cell (( GoB f),i2,(j1 + 1))) by GOBOARD5:def 3;

                        p in { |[s, r]| where s,r be Real : r <= ((( GoB f) * (( len ( GoB f)),1)) `2 ) } by A75;

                        then p in ( h_strip (( GoB f),j1)) by A56, A75, GOBOARD5: 7;

                        then p in (( h_strip (( GoB f),j1)) /\ ( v_strip (( GoB f),i2))) by A62, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j1)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j1 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j1)) /\ (( L~ f) ` )) by A63, A77, XBOOLE_0:def 4;

                      end;

                        case j1 = 0 & (j1 + 1) = ( width ( GoB f));

                        hence contradiction by GOBOARD7: 33;

                      end;

                    end;

                    then p in ( Cl ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` )))) by A3, Th2;

                    then

                     A78: ( Cl ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` )))) c= ( Component_of p1) by A3, A4, A8, Th3, GOBRD11: 1;

                    ( Down (( RightComp f),(( L~ f) ` ))) is closed by Lm4, CONNSP_1: 33;

                    then

                     A79: ( Cl ( Down (( RightComp f),(( L~ f) ` )))) = ( Down (( RightComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    ( Down (( LeftComp f),(( L~ f) ` ))) is closed by Lm3, CONNSP_1: 33;

                    then

                     A80: ( Cl ( Down (( LeftComp f),(( L~ f) ` )))) = ( Down (( LeftComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) = ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by GOBRD11: 4;

                    then

                     A81: ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) = (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A80, A79, PRE_TOPC: 20;

                    

                     A82: ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` ))) c= ( Cl ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` )))) & ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` ))) = ( Int ( cell (( GoB f),i2,(j1 + 1)))) by A3, A4, A8, Th3, PRE_TOPC: 18;

                    

                     A83: ( Down (( LeftComp f),(( L~ f) ` ))) = ( LeftComp f) & ( Down (( RightComp f),(( L~ f) ` ))) = ( RightComp f) by Th5;

                    ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` ))) c= (( LeftComp f) \/ ( RightComp f)) by A1, A2, A6, A7, Th3;

                    then ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` ))) c= ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by A83, GOBRD11: 4;

                    then

                     A84: ( Cl ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` )))) c= ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) by PRE_TOPC: 19;

                    p in ( Cl ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` )))) by A2, A3, A65, Th2;

                    then ( Component_of p1) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A84, A81, Th5, CONNSP_3: 21;

                    then ( Cl ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` )))) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A78;

                    hence ( Int ( cell (( GoB f),i2,(j1 + 1)))) c= (( LeftComp f) \/ ( RightComp f)) by A83, A82;

                  end;

                    case

                     A85: i2 <> 0 & i2 <> ( len ( GoB f)) & not ex k st 1 <= k & (k + 1) <= ( len f) & ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * (i2,(j1 + 1))),(( GoB f) * ((i2 + 1),(j1 + 1)))));

                    then

                     A86: i2 < ( len ( GoB f)) by A3, XXREAL_0: 1;

                    then

                     A87: (i2 + 1) <= ( len ( GoB f)) by NAT_1: 13;

                    for k st 1 <= k & (k + 1) <= ( len f) holds ( LSeg ((( GoB f) * (i2,(j1 + 1))),(( GoB f) * ((i2 + 1),(j1 + 1))))) <> ( LSeg (f,k))

                    proof

                      let k;

                      assume

                       A88: 1 <= k & (k + 1) <= ( len f);

                      then ( LSeg (f,k)) = ( LSeg ((f /. k),(f /. (k + 1)))) by TOPREAL1:def 3;

                      hence thesis by A85, A88;

                    end;

                    then

                     A89: 1 <= (j1 + 1) & (j1 + 1) <= ( width ( GoB f)) & 1 <= i2 & (i2 + 1) <= ( len ( GoB f)) implies not ((1 / 2) * ((( GoB f) * (i2,(j1 + 1))) + (( GoB f) * ((i2 + 1),(j1 + 1))))) in ( L~ f) by GOBOARD7: 40;

                    reconsider p = ((1 / 2) * ((( GoB f) * (i2,(j1 + 1))) + (( GoB f) * ((i2 + 1),(j1 + 1))))) as Point of ( TOP-REAL 2);

                    

                     A90: (p `1 ) = ((1 / 2) * (((( GoB f) * (i2,(j1 + 1))) + (( GoB f) * ((i2 + 1),(j1 + 1)))) `1 )) by TOPREAL3: 4

                    .= ((1 / 2) * (((( GoB f) * (i2,(j1 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j1 + 1))) `1 ))) by TOPREAL3: 2;

                    reconsider P = {p} as Subset of ( TOP-REAL 2);

                    

                     A91: 1 < ( len ( GoB f)) by GOBOARD7: 32;

                    ( Down (( RightComp f),(( L~ f) ` ))) is closed by Lm4, CONNSP_1: 33;

                    then

                     A92: ( Cl ( Down (( RightComp f),(( L~ f) ` )))) = ( Down (( RightComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    ( Down (( LeftComp f),(( L~ f) ` ))) is closed by Lm3, CONNSP_1: 33;

                    then

                     A93: ( Cl ( Down (( LeftComp f),(( L~ f) ` )))) = ( Down (( LeftComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) = ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by GOBRD11: 4;

                    then

                     A94: ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) = (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A93, A92, PRE_TOPC: 20;

                    

                     A95: ( Down (( LeftComp f),(( L~ f) ` ))) = ( LeftComp f) & ( Down (( RightComp f),(( L~ f) ` ))) = ( RightComp f) by Th5;

                    ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` ))) c= (( LeftComp f) \/ ( RightComp f)) by A1, A2, A6, A7, Th3;

                    then ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` ))) c= ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by A95, GOBRD11: 4;

                    then

                     A96: ( Cl ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` )))) c= ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) by PRE_TOPC: 19;

                    

                     A97: ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` ))) c= ( Cl ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` )))) & ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` ))) = ( Int ( cell (( GoB f),i2,(j1 + 1)))) by A3, A4, A8, Th3, PRE_TOPC: 18;

                    

                     A98: 1 <= (j1 + 1) by NAT_1: 11;

                    

                     A99: ( 0 + 1) <= i2 by A85, NAT_1: 13;

                    then

                     A100: 1 < (i2 + 1) by NAT_1: 13;

                    (for x be object st x in P holds not x in ( L~ f)) implies P misses ( L~ f) by XBOOLE_0: 3;

                    then

                     A101: p in {p} & {p} c= (( L~ f) ` ) by A4, A8, A99, A86, A89, NAT_1: 13, SUBSET_1: 23, TARSKI:def 1;

                    then

                    reconsider p1 = p as Point of (( TOP-REAL 2) | (( L~ f) ` )) by PRE_TOPC: 8;

                    

                     A102: 1 <= (1 + j1) by NAT_1: 11;

                    (p `2 ) = ((1 / 2) * (((( GoB f) * (i2,(j1 + 1))) + (( GoB f) * ((i2 + 1),(j1 + 1)))) `2 )) by TOPREAL3: 4

                    .= ((1 / 2) * (((( GoB f) * (i2,(j1 + 1))) `2 ) + ((( GoB f) * ((i2 + 1),(j1 + 1))) `2 ))) by TOPREAL3: 2;

                    then

                     A103: p = |[((1 / 2) * (((( GoB f) * (i2,(j1 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j1 + 1))) `1 ))), ((1 / 2) * (((( GoB f) * (i2,(j1 + 1))) `2 ) + ((( GoB f) * ((i2 + 1),(j1 + 1))) `2 )))]| by A90, EUCLID: 53;

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

                    then

                     A104: ((( GoB f) * (i2,(j1 + 1))) `1 ) < ((( GoB f) * ((i2 + 1),(j1 + 1))) `1 ) by A4, A8, A99, A87, A102, GOBOARD5: 3;

                    then (((( GoB f) * (i2,(j1 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j1 + 1))) `1 )) < (((( GoB f) * ((i2 + 1),(j1 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j1 + 1))) `1 )) by XREAL_1: 8;

                    then

                     A105: ((((( GoB f) * (i2,(j1 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j1 + 1))) `1 )) / 2) < ((((( GoB f) * ((i2 + 1),(j1 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j1 + 1))) `1 )) / 2) by XREAL_1: 74;

                    (((( GoB f) * (i2,(j1 + 1))) `1 ) + ((( GoB f) * (i2,(j1 + 1))) `1 )) < (((( GoB f) * (i2,(j1 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j1 + 1))) `1 )) by A104, XREAL_1: 8;

                    then

                     A106: ((((( GoB f) * (i2,(j1 + 1))) `1 ) + ((( GoB f) * (i2,(j1 + 1))) `1 )) / 2) < ((((( GoB f) * (i2,(j1 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j1 + 1))) `1 )) / 2) by XREAL_1: 74;

                    p in { |[s, r]| where s,r be Real : ((( GoB f) * (i2,(j1 + 1))) `1 ) <= s & s <= ((( GoB f) * ((i2 + 1),(j1 + 1))) `1 ) }

                    proof

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

                      hence thesis by A90, A106, A105;

                    end;

                    then

                     A107: p in ( v_strip (( GoB f),i2)) by A4, A8, A99, A86, A98, GOBOARD5: 8;

                    

                     A108: j1 = 0 or j1 >= ( 0 + 1) by NAT_1: 13;

                     A109:

                    now

                      per cases by A4, A8, A108, XXREAL_0: 1;

                        case

                         A110: j1 >= 1 & (j1 + 1) < ( width ( GoB f));

                        then

                         A111: ((j1 + 1) + 1) <= ( width ( GoB f)) by NAT_1: 13;

                        

                         A112: p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,(j1 + 1))) `2 ) <= r & r <= ((( GoB f) * (1,((j1 + 1) + 1))) `2 ) }

                        proof

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

                          then

                           A113: ((( GoB f) * (1,(j1 + 1))) `2 ) < ((( GoB f) * (1,((j1 + 1) + 1))) `2 ) by A91, A102, A111, GOBOARD5: 4;

                          ((( GoB f) * (i2,(j1 + 1))) `2 ) = ((( GoB f) * (1,(j1 + 1))) `2 ) & ((( GoB f) * ((i2 + 1),(j1 + 1))) `2 ) = ((( GoB f) * (1,(j1 + 1))) `2 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5: 1;

                          hence thesis by A103, A113;

                        end;

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

                        then p in ( h_strip (( GoB f),(j1 + 1))) by A91, A110, A112, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),(j1 + 1))) /\ ( v_strip (( GoB f),i2))) by A107, XBOOLE_0:def 4;

                        then

                         A114: p in ( cell (( GoB f),i2,(j1 + 1))) by GOBOARD5:def 3;

                        

                         A115: p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,j1)) `2 ) <= r & r <= ((( GoB f) * (1,(j1 + 1))) `2 ) }

                        proof

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

                          then

                           A116: ((( GoB f) * (1,j1)) `2 ) < ((( GoB f) * (1,(j1 + 1))) `2 ) by A91, A110, GOBOARD5: 4;

                          ((( GoB f) * (i2,(j1 + 1))) `2 ) = ((( GoB f) * (1,(j1 + 1))) `2 ) & ((( GoB f) * ((i2 + 1),(j1 + 1))) `2 ) = ((( GoB f) * (1,(j1 + 1))) `2 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5: 1;

                          hence thesis by A103, A116;

                        end;

                        j1 < ( width ( GoB f)) by A110, NAT_1: 13;

                        then p in ( h_strip (( GoB f),j1)) by A91, A110, A115, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),j1)) /\ ( v_strip (( GoB f),i2))) by A107, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j1)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j1 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j1)) /\ (( L~ f) ` )) by A101, A114, XBOOLE_0:def 4;

                      end;

                        case

                         A117: j1 >= 1 & (j1 + 1) = ( width ( GoB f));

                        

                         A118: j1 < (j1 + 1) by NAT_1: 13;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,j1)) `2 ) <= r & r <= ((( GoB f) * (1,(j1 + 1))) `2 ) }

                        proof

                          

                           A119: ((( GoB f) * (1,j1)) `2 ) < ((( GoB f) * (1,(j1 + 1))) `2 ) by A91, A117, A118, GOBOARD5: 4;

                          ((( GoB f) * (i2,(j1 + 1))) `2 ) = ((( GoB f) * (1,(j1 + 1))) `2 ) & ((( GoB f) * ((i2 + 1),(j1 + 1))) `2 ) = ((( GoB f) * (1,(j1 + 1))) `2 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5: 1;

                          hence thesis by A103, A119;

                        end;

                        then p in ( h_strip (( GoB f),j1)) by A91, A117, A118, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),j1)) /\ ( v_strip (( GoB f),i2))) by A107, XBOOLE_0:def 4;

                        then

                         A120: p in ( cell (( GoB f),i2,j1)) by GOBOARD5:def 3;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,(j1 + 1))) `2 ) <= r }

                        proof

                          ((( GoB f) * (i2,(j1 + 1))) `2 ) = ((( GoB f) * (1,(j1 + 1))) `2 ) & ((( GoB f) * ((i2 + 1),(j1 + 1))) `2 ) = ((( GoB f) * (1,(j1 + 1))) `2 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5: 1;

                          hence thesis by A103;

                        end;

                        then p in ( h_strip (( GoB f),(j1 + 1))) by A91, A117, GOBOARD5: 6;

                        then p in (( h_strip (( GoB f),(j1 + 1))) /\ ( v_strip (( GoB f),i2))) by A107, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,(j1 + 1))) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j1 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j1)) /\ (( L~ f) ` )) by A101, A120, XBOOLE_0:def 4;

                      end;

                        case

                         A121: j1 = 0 & (j1 + 1) < ( width ( GoB f));

                        then

                         A122: ((j1 + 1) + 1) <= ( width ( GoB f)) by NAT_1: 13;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,(j1 + 1))) `2 ) <= r & r <= ((( GoB f) * (1,((j1 + 1) + 1))) `2 ) }

                        proof

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

                          then

                           A123: ((( GoB f) * (1,(j1 + 1))) `2 ) < ((( GoB f) * (1,((j1 + 1) + 1))) `2 ) by A91, A102, A122, GOBOARD5: 4;

                          ((( GoB f) * (i2,(j1 + 1))) `2 ) = ((( GoB f) * (1,(j1 + 1))) `2 ) & ((( GoB f) * ((i2 + 1),(j1 + 1))) `2 ) = ((( GoB f) * (1,(j1 + 1))) `2 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5: 1;

                          hence thesis by A103, A123;

                        end;

                        then p in ( h_strip (( GoB f),(j1 + 1))) by A91, A121, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),(j1 + 1))) /\ ( v_strip (( GoB f),i2))) by A107, XBOOLE_0:def 4;

                        then

                         A124: p in ( cell (( GoB f),i2,(j1 + 1))) by GOBOARD5:def 3;

                        p in { |[s, r]| where s,r be Real : r <= ((( GoB f) * (1,1)) `2 ) }

                        proof

                          ((( GoB f) * (i2,(j1 + 1))) `2 ) = ((( GoB f) * (1,(j1 + 1))) `2 ) & ((( GoB f) * ((i2 + 1),(j1 + 1))) `2 ) = ((( GoB f) * (1,(j1 + 1))) `2 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5: 1;

                          hence thesis by A103, A121;

                        end;

                        then p in ( h_strip (( GoB f),j1)) by A91, A121, GOBOARD5: 7;

                        then p in (( h_strip (( GoB f),j1)) /\ ( v_strip (( GoB f),i2))) by A107, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j1)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j1 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j1)) /\ (( L~ f) ` )) by A101, A124, XBOOLE_0:def 4;

                      end;

                        case j1 = 0 & (j1 + 1) = ( width ( GoB f));

                        hence contradiction by GOBOARD7: 33;

                      end;

                    end;

                    then p in ( Cl ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` )))) by A3, Th2;

                    then

                     A125: ( Cl ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` )))) c= ( Component_of p1) by A3, A4, A8, Th3, GOBRD11: 1;

                    p in ( Cl ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` )))) by A2, A3, A109, Th2;

                    then ( Component_of p1) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A96, A94, Th5, CONNSP_3: 21;

                    then ( Cl ( Down (( Int ( cell (( GoB f),i2,(j1 + 1)))),(( L~ f) ` )))) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A125;

                    hence ( Int ( cell (( GoB f),i2,(j1 + 1)))) c= (( LeftComp f) \/ ( RightComp f)) by A95, A97;

                  end;

                end;

                hence ( Int ( cell (( GoB f),i2,(j1 + 1)))) c= (( LeftComp f) \/ ( RightComp f));

              end;

            end;

            hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f)) by A8;

          end;

            case

             A126: j1 = (j2 + 1);

            then j2 < j1 by NAT_1: 13;

            then

             A127: (j1 -' 1) < j1 by A126, NAT_D: 34;

            

             A128: j2 < (j2 + 1) by NAT_1: 13;

            

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

            

             A130: (j2 + 1) < ((j2 + 1) + 1) by NAT_1: 13;

            

             A131: 1 <= j1 & (j1 -' 1) = (j1 - 1) by A126, NAT_1: 11, XREAL_0:def 2;

            

             A132: 1 <= (j2 + 1) by NAT_1: 11;

            

             A133: (j1 -' 1) = j2 by A126, NAT_D: 34;

            now

              per cases ;

                case ex k st 1 <= k & (k + 1) <= ( len f) & i2 <> 0 & i2 <> ( len ( GoB f)) & ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * (i2,(j2 + 1))),(( GoB f) * ((i2 + 1),(j2 + 1)))));

                then

                consider k such that

                 A134: 1 <= k & (k + 1) <= ( len f) and

                 A135: i2 <> 0 and

                 A136: i2 <> ( len ( GoB f)) and

                 A137: ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * (i2,((j1 -' 1) + 1))),(( GoB f) * ((i2 + 1),((j1 -' 1) + 1))))) by A133;

                now

                  per cases by A137, SPPOL_1: 8;

                    case

                     A138: (f /. k) = (( GoB f) * (i2,((j1 -' 1) + 1))) & (f /. (k + 1)) = (( GoB f) * ((i2 + 1),((j1 -' 1) + 1)));

                    

                     A139: ( Int ( right_cell (f,k))) c= ( RightComp f) & ( RightComp f) c= (( LeftComp f) \/ ( RightComp f)) by A134, GOBOARD9: 25, XBOOLE_1: 7;

                    i2 < ( len ( GoB f)) by A3, A136, XXREAL_0: 1;

                    then

                     A140: (i2 + 1) <= ( len ( GoB f)) by NAT_1: 13;

                    (j1 -' 1) < ( width ( GoB f)) by A2, A127, XXREAL_0: 2;

                    then ((j1 -' 1) + 1) <= ( width ( GoB f)) by NAT_1: 13;

                    then

                     A141: ( Indices ( GoB f)) = [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] & ((j1 -' 1) + 1) in ( Seg ( width ( GoB f))) by A129, FINSEQ_1: 1, MATRIX_0:def 4;

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

                    then (i2 + 1) in ( dom ( GoB f)) by A140, FINSEQ_3: 25;

                    then

                     A142: [(i2 + 1), ((j1 -' 1) + 1)] in ( Indices ( GoB f)) by A141, ZFMISC_1: 87;

                    i2 >= ( 0 + 1) by A135, NAT_1: 13;

                    then i2 in ( dom ( GoB f)) by A3, FINSEQ_3: 25;

                    then [i2, ((j1 -' 1) + 1)] in ( Indices ( GoB f)) by A141, ZFMISC_1: 87;

                    then ( right_cell (f,k)) = ( cell (( GoB f),i2,(j1 -' 1))) by A134, A138, A142, GOBOARD5: 28;

                    hence ( Int ( cell (( GoB f),i2,(j1 -' 1)))) c= (( LeftComp f) \/ ( RightComp f)) by A139;

                  end;

                    case

                     A143: (f /. k) = (( GoB f) * ((i2 + 1),((j1 -' 1) + 1))) & (f /. (k + 1)) = (( GoB f) * (i2,((j1 -' 1) + 1)));

                    

                     A144: ( Int ( left_cell (f,k))) c= ( LeftComp f) & ( LeftComp f) c= (( LeftComp f) \/ ( RightComp f)) by A134, GOBOARD9: 21, XBOOLE_1: 7;

                    i2 < ( len ( GoB f)) by A3, A136, XXREAL_0: 1;

                    then

                     A145: (i2 + 1) <= ( len ( GoB f)) by NAT_1: 13;

                    

                     A146: ( Indices ( GoB f)) = [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] & ((j1 -' 1) + 1) in ( Seg ( width ( GoB f))) by A2, A131, FINSEQ_1: 1, MATRIX_0:def 4;

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

                    then (i2 + 1) in ( dom ( GoB f)) by A145, FINSEQ_3: 25;

                    then

                     A147: [(i2 + 1), ((j1 -' 1) + 1)] in ( Indices ( GoB f)) by A146, ZFMISC_1: 87;

                    i2 >= ( 0 + 1) by A135, NAT_1: 13;

                    then i2 in ( dom ( GoB f)) by A3, FINSEQ_3: 25;

                    then [i2, ((j1 -' 1) + 1)] in ( Indices ( GoB f)) by A146, ZFMISC_1: 87;

                    then ( left_cell (f,k)) = ( cell (( GoB f),i2,(j1 -' 1))) by A134, A143, A147, GOBOARD5: 29;

                    hence ( Int ( cell (( GoB f),i2,(j1 -' 1)))) c= (( LeftComp f) \/ ( RightComp f)) by A144;

                  end;

                end;

                hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f)) by A126, NAT_D: 34;

              end;

                case

                 A148: not ex k st 1 <= k & (k + 1) <= ( len f) & i2 <> 0 & i2 <> ( len ( GoB f)) & ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * (i2,(j2 + 1))),(( GoB f) * ((i2 + 1),(j2 + 1)))));

                now

                  per cases by A148;

                    case

                     A149: i2 = 0 ;

                    reconsider p = |[(((( GoB f) * (1,(j2 + 1))) `1 ) - 1), ((( GoB f) * (1,(j2 + 1))) `2 )]| as Point of ( TOP-REAL 2);

                    

                     A150: 1 < ( len ( GoB f)) by GOBOARD7: 32;

                    

                     A151: 1 < ( width ( GoB f)) by GOBOARD7: 33;

                    reconsider P = {p} as Subset of ( TOP-REAL 2);

                    

                     A152: (p `1 ) < ((p `1 ) + 1) by XREAL_1: 29;

                    

                     A153: 1 <= (j2 + 1) by NAT_1: 11;

                    then ((( GoB f) * (1,(j2 + 1))) `1 ) = ((( GoB f) * (1,1)) `1 ) by A2, A126, A150, GOBOARD5: 2;

                    then

                     A154: (p `1 ) = (((( GoB f) * (1,1)) `1 ) - 1) by EUCLID: 52;

                    p in { |[s, r]| where s,r be Real : s <= ((( GoB f) * (1,1)) `1 ) }

                    proof

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

                      hence thesis by A154, A152;

                    end;

                    then

                     A155: p in ( v_strip (( GoB f),i2)) by A149, A151, GOBOARD5: 10;

                    (for q be Point of ( TOP-REAL 2) st q in P holds (q `1 ) < ((( GoB f) * (1,1)) `1 )) implies P misses ( L~ f) by GOBOARD8: 21;

                    then

                     A156: p in {p} & {p} c= (( L~ f) ` ) by A154, A152, SUBSET_1: 23, TARSKI:def 1;

                    then

                    reconsider p1 = p as Point of (( TOP-REAL 2) | (( L~ f) ` )) by PRE_TOPC: 8;

                     A157:

                    now

                      per cases by A2, A126, XXREAL_0: 1;

                        case

                         A158: (j2 + 1) < ( width ( GoB f)) & j2 > 0 ;

                        then

                         A159: ((j2 + 1) + 1) <= ( width ( GoB f)) by NAT_1: 13;

                        

                         A160: p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,(j2 + 1))) `2 ) <= r & r <= ((( GoB f) * (1,((j2 + 1) + 1))) `2 ) }

                        proof

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

                          then ((( GoB f) * (1,(j2 + 1))) `2 ) <= ((( GoB f) * (1,((j2 + 1) + 1))) `2 ) by A150, A153, A159, GOBOARD5: 4;

                          hence thesis;

                        end;

                        

                         A161: ( 0 + 1) <= j2 by A158, NAT_1: 13;

                        

                         A162: p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,j2)) `2 ) <= r & r <= ((( GoB f) * (1,(j2 + 1))) `2 ) }

                        proof

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

                          then ((( GoB f) * (1,j2)) `2 ) < ((( GoB f) * (1,(j2 + 1))) `2 ) by A2, A126, A150, A161, GOBOARD5: 4;

                          hence thesis;

                        end;

                        j2 < ( width ( GoB f)) by A158, NAT_1: 13;

                        then p in ( h_strip (( GoB f),j2)) by A150, A161, A162, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),j2)) /\ ( v_strip (( GoB f),i2))) by A155, XBOOLE_0:def 4;

                        then

                         A163: p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

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

                        then p in ( h_strip (( GoB f),(j2 + 1))) by A150, A158, A160, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),(j2 + 1))) /\ ( v_strip (( GoB f),i2))) by A155, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,(j2 + 1))) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j2 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A156, A163, XBOOLE_0:def 4;

                      end;

                        case

                         A164: (j2 + 1) < ( width ( GoB f)) & j2 = 0 ;

                        

                         A165: (j2 + 1) < ((j2 + 1) + 1) by NAT_1: 13;

                        

                         A166: ((j2 + 1) + 1) <= ( width ( GoB f)) by A164, NAT_1: 13;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,(j2 + 1))) `2 ) <= r & r <= ((( GoB f) * (1,((j2 + 1) + 1))) `2 ) }

                        proof

                          ((( GoB f) * (1,(j2 + 1))) `2 ) < ((( GoB f) * (1,((j2 + 1) + 1))) `2 ) by A132, A150, A166, A165, GOBOARD5: 4;

                          hence thesis;

                        end;

                        then p in ( h_strip (( GoB f),(j2 + 1))) by A150, A164, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),(j2 + 1))) /\ ( v_strip (( GoB f),i2))) by A155, XBOOLE_0:def 4;

                        then

                         A167: p in ( cell (( GoB f),i2,(j2 + 1))) by GOBOARD5:def 3;

                        p in { |[s, r]| where s,r be Real : r <= ((( GoB f) * (1,(j2 + 1))) `2 ) };

                        then p in ( h_strip (( GoB f),j2)) by A150, A164, GOBOARD5: 7;

                        then p in (( h_strip (( GoB f),j2)) /\ ( v_strip (( GoB f),i2))) by A155, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j2 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A156, A167, XBOOLE_0:def 4;

                      end;

                        case

                         A168: (j2 + 1) = ( width ( GoB f)) & j2 > 0 ;

                        then

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

                        

                         A170: p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,j2)) `2 ) <= r & r <= ((( GoB f) * (1,(j2 + 1))) `2 ) }

                        proof

                          ((( GoB f) * (1,j2)) `2 ) < ((( GoB f) * (1,(j2 + 1))) `2 ) by A128, A150, A168, A169, GOBOARD5: 4;

                          hence thesis;

                        end;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,(j2 + 1))) `2 ) <= r };

                        then p in ( h_strip (( GoB f),(j2 + 1))) by A150, A168, GOBOARD5: 6;

                        then p in (( h_strip (( GoB f),(j2 + 1))) /\ ( v_strip (( GoB f),i2))) by A155, XBOOLE_0:def 4;

                        then

                         A171: p in ( cell (( GoB f),i2,(j2 + 1))) by GOBOARD5:def 3;

                        j2 < ( width ( GoB f)) by A168, NAT_1: 13;

                        then p in ( h_strip (( GoB f),j2)) by A150, A169, A170, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),j2)) /\ ( v_strip (( GoB f),i2))) by A155, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j2 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A156, A171, XBOOLE_0:def 4;

                      end;

                        case

                         A172: (j2 + 1) = ( width ( GoB f)) & j2 = 0 ;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,(j2 + 1))) `2 ) <= r };

                        then p in ( h_strip (( GoB f),(j2 + 1))) by A150, A172, GOBOARD5: 6;

                        then p in (( h_strip (( GoB f),(j2 + 1))) /\ ( v_strip (( GoB f),i2))) by A155, XBOOLE_0:def 4;

                        then

                         A173: p in ( cell (( GoB f),i2,(j2 + 1))) by GOBOARD5:def 3;

                        p in { |[s, r]| where s,r be Real : r <= ((( GoB f) * (1,1)) `2 ) } by A172;

                        then p in ( h_strip (( GoB f),j2)) by A150, A172, GOBOARD5: 7;

                        then p in (( h_strip (( GoB f),j2)) /\ ( v_strip (( GoB f),i2))) by A155, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j2 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A156, A173, XBOOLE_0:def 4;

                      end;

                    end;

                    then p in ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) by A3, A4, Th2;

                    then

                     A174: ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) c= ( Component_of p1) by A3, A4, Th3, GOBRD11: 1;

                    ( Down (( RightComp f),(( L~ f) ` ))) is closed by Lm4, CONNSP_1: 33;

                    then

                     A175: ( Cl ( Down (( RightComp f),(( L~ f) ` )))) = ( Down (( RightComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    ( Down (( LeftComp f),(( L~ f) ` ))) is closed by Lm3, CONNSP_1: 33;

                    then

                     A176: ( Cl ( Down (( LeftComp f),(( L~ f) ` )))) = ( Down (( LeftComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    

                     A177: ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` ))) c= ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) & ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` ))) = ( Int ( cell (( GoB f),i2,j2))) by A3, A4, Th3, PRE_TOPC: 18;

                    (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) = ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by GOBRD11: 4;

                    then

                     A178: ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) = (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A176, A175, PRE_TOPC: 20;

                    

                     A179: ( Down (( LeftComp f),(( L~ f) ` ))) = ( LeftComp f) & ( Down (( RightComp f),(( L~ f) ` ))) = ( RightComp f) by Th5;

                    ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` ))) c= (( LeftComp f) \/ ( RightComp f)) by A1, A2, A6, A7, Th3;

                    then ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` ))) c= ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by A179, GOBRD11: 4;

                    then

                     A180: ( Cl ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` )))) c= ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) by PRE_TOPC: 19;

                    p in ( Cl ( Down (( Int ( cell (( GoB f),i2,(j2 + 1)))),(( L~ f) ` )))) by A3, A157, Th2;

                    then ( Component_of p1) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A126, A180, A178, Th5, CONNSP_3: 21;

                    then ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A174;

                    hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f)) by A179, A177;

                  end;

                    case

                     A181: i2 = ( len ( GoB f));

                    reconsider p = |[(((( GoB f) * (( len ( GoB f)),(j2 + 1))) `1 ) + 1), ((( GoB f) * (( len ( GoB f)),(j2 + 1))) `2 )]| as Point of ( TOP-REAL 2);

                    

                     A182: 1 < ( len ( GoB f)) by GOBOARD7: 32;

                    reconsider P = {p} as Subset of ( TOP-REAL 2);

                    

                     A183: (for q be Point of ( TOP-REAL 2) st q in P holds ((( GoB f) * (( len ( GoB f)),1)) `1 ) < (q `1 )) implies P misses ( L~ f) by GOBOARD8: 22;

                    

                     A184: 1 < ( width ( GoB f)) by GOBOARD7: 33;

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

                    then ((( GoB f) * (( len ( GoB f)),(j2 + 1))) `1 ) = ((( GoB f) * (( len ( GoB f)),1)) `1 ) by A2, A126, A182, GOBOARD5: 2;

                    then

                     A185: (p `1 ) = (((( GoB f) * (( len ( GoB f)),1)) `1 ) + 1) by EUCLID: 52;

                    then

                     A186: ((( GoB f) * (( len ( GoB f)),1)) `1 ) < (p `1 ) by XREAL_1: 29;

                    p in { |[s, r]| where s,r be Real : ((( GoB f) * (( len ( GoB f)),1)) `1 ) <= s }

                    proof

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

                      hence thesis by A186;

                    end;

                    then

                     A187: p in ( v_strip (( GoB f),i2)) by A181, A184, GOBOARD5: 9;

                    ((( GoB f) * (( len ( GoB f)),1)) `1 ) < (((( GoB f) * (( len ( GoB f)),1)) `1 ) + 1) by XREAL_1: 29;

                    then

                     A188: p in {p} & {p} c= (( L~ f) ` ) by A185, A183, SUBSET_1: 23, TARSKI:def 1;

                    then

                    reconsider p1 = p as Point of (( TOP-REAL 2) | (( L~ f) ` )) by PRE_TOPC: 8;

                     A189:

                    now

                      per cases by A2, A126, XXREAL_0: 1;

                        case

                         A190: (j2 + 1) < ( width ( GoB f)) & j2 > 0 ;

                        then

                         A191: ((j2 + 1) + 1) <= ( width ( GoB f)) by NAT_1: 13;

                        

                         A192: p in { |[s, r]| where s,r be Real : ((( GoB f) * (( len ( GoB f)),(j2 + 1))) `2 ) <= r & r <= ((( GoB f) * (( len ( GoB f)),((j2 + 1) + 1))) `2 ) }

                        proof

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

                          then ((( GoB f) * (( len ( GoB f)),(j2 + 1))) `2 ) <= ((( GoB f) * (( len ( GoB f)),((j2 + 1) + 1))) `2 ) by A132, A182, A191, GOBOARD5: 4;

                          hence thesis;

                        end;

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

                        then p in ( h_strip (( GoB f),(j2 + 1))) by A182, A190, A192, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),(j2 + 1))) /\ ( v_strip (( GoB f),i2))) by A187, XBOOLE_0:def 4;

                        then

                         A193: p in ( cell (( GoB f),i2,(j2 + 1))) by GOBOARD5:def 3;

                        

                         A194: ( 0 + 1) <= j2 by A190, NAT_1: 13;

                        

                         A195: j2 < (j2 + 1) by NAT_1: 13;

                        

                         A196: p in { |[s, r]| where s,r be Real : ((( GoB f) * (( len ( GoB f)),j2)) `2 ) <= r & r <= ((( GoB f) * (( len ( GoB f)),(j2 + 1))) `2 ) }

                        proof

                          ((( GoB f) * (( len ( GoB f)),j2)) `2 ) < ((( GoB f) * (( len ( GoB f)),(j2 + 1))) `2 ) by A2, A126, A182, A194, A195, GOBOARD5: 4;

                          hence thesis;

                        end;

                        j2 < ( width ( GoB f)) by A190, NAT_1: 13;

                        then p in ( h_strip (( GoB f),j2)) by A182, A194, A196, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),j2)) /\ ( v_strip (( GoB f),i2))) by A187, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j2 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A188, A193, XBOOLE_0:def 4;

                      end;

                        case

                         A197: (j2 + 1) < ( width ( GoB f)) & j2 = 0 ;

                        then

                         A198: ((j2 + 1) + 1) <= ( width ( GoB f)) by NAT_1: 13;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (( len ( GoB f)),(j2 + 1))) `2 ) <= r & r <= ((( GoB f) * (( len ( GoB f)),((j2 + 1) + 1))) `2 ) }

                        proof

                          ((( GoB f) * (( len ( GoB f)),(j2 + 1))) `2 ) < ((( GoB f) * (( len ( GoB f)),((j2 + 1) + 1))) `2 ) by A132, A130, A182, A198, GOBOARD5: 4;

                          hence thesis;

                        end;

                        then p in ( h_strip (( GoB f),(j2 + 1))) by A182, A197, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),(j2 + 1))) /\ ( v_strip (( GoB f),i2))) by A187, XBOOLE_0:def 4;

                        then

                         A199: p in ( cell (( GoB f),i2,(j2 + 1))) by GOBOARD5:def 3;

                        p in { |[s, r]| where s,r be Real : r <= ((( GoB f) * (( len ( GoB f)),1)) `2 ) } by A197;

                        then p in ( h_strip (( GoB f),j2)) by A182, A197, GOBOARD5: 7;

                        then p in (( h_strip (( GoB f),j2)) /\ ( v_strip (( GoB f),i2))) by A187, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j2 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A188, A199, XBOOLE_0:def 4;

                      end;

                        case

                         A200: (j2 + 1) = ( width ( GoB f)) & j2 > 0 ;

                        then

                         A201: ( 0 + 1) <= j2 & j2 < ( width ( GoB f)) by NAT_1: 13;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (( len ( GoB f)),j2)) `2 ) <= r & r <= ((( GoB f) * (( len ( GoB f)),(j2 + 1))) `2 ) }

                        proof

                          ((( GoB f) * (( len ( GoB f)),j2)) `2 ) <= ((( GoB f) * (( len ( GoB f)),(j2 + 1))) `2 ) by A182, A200, A201, GOBOARD5: 4;

                          hence thesis;

                        end;

                        then p in ( h_strip (( GoB f),j2)) by A182, A201, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),j2)) /\ ( v_strip (( GoB f),i2))) by A187, XBOOLE_0:def 4;

                        then

                         A202: p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) `2 ) <= r } by A200;

                        then p in ( h_strip (( GoB f),(j2 + 1))) by A182, A200, GOBOARD5: 6;

                        then p in (( h_strip (( GoB f),(j2 + 1))) /\ ( v_strip (( GoB f),i2))) by A187, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,(j2 + 1))) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j2 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A188, A202, XBOOLE_0:def 4;

                      end;

                        case (j2 + 1) = ( width ( GoB f)) & j2 = 0 ;

                        hence contradiction by GOBOARD7: 33;

                      end;

                    end;

                    then p in ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) by A3, A4, Th2;

                    then

                     A203: ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) c= ( Component_of p1) by A3, A4, Th3, GOBRD11: 1;

                    ( Down (( RightComp f),(( L~ f) ` ))) is closed by Lm4, CONNSP_1: 33;

                    then

                     A204: ( Cl ( Down (( RightComp f),(( L~ f) ` )))) = ( Down (( RightComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    ( Down (( LeftComp f),(( L~ f) ` ))) is closed by Lm3, CONNSP_1: 33;

                    then

                     A205: ( Cl ( Down (( LeftComp f),(( L~ f) ` )))) = ( Down (( LeftComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    

                     A206: ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` ))) c= ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) & ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` ))) = ( Int ( cell (( GoB f),i2,j2))) by A3, A4, Th3, PRE_TOPC: 18;

                    (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) = ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by GOBRD11: 4;

                    then

                     A207: ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) = (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A205, A204, PRE_TOPC: 20;

                    

                     A208: ( Down (( LeftComp f),(( L~ f) ` ))) = ( LeftComp f) & ( Down (( RightComp f),(( L~ f) ` ))) = ( RightComp f) by Th5;

                    ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` ))) c= (( LeftComp f) \/ ( RightComp f)) by A1, A2, A6, A7, Th3;

                    then ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` ))) c= ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by A208, GOBRD11: 4;

                    then

                     A209: ( Cl ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` )))) c= ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) by PRE_TOPC: 19;

                    p in ( Cl ( Down (( Int ( cell (( GoB f),i2,(j2 + 1)))),(( L~ f) ` )))) by A3, A189, Th2;

                    then ( Component_of p1) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A126, A209, A207, Th5, CONNSP_3: 21;

                    then ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A203;

                    hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f)) by A208, A206;

                  end;

                    case

                     A210: i2 <> 0 & i2 <> ( len ( GoB f)) & not ex k st 1 <= k & (k + 1) <= ( len f) & ( LSeg ((f /. k),(f /. (k + 1)))) = ( LSeg ((( GoB f) * (i2,(j2 + 1))),(( GoB f) * ((i2 + 1),(j2 + 1)))));

                    then

                     A211: i2 < ( len ( GoB f)) by A3, XXREAL_0: 1;

                    then

                     A212: (i2 + 1) <= ( len ( GoB f)) by NAT_1: 13;

                    for k st 1 <= k & (k + 1) <= ( len f) holds ( LSeg ((( GoB f) * (i2,(j2 + 1))),(( GoB f) * ((i2 + 1),(j2 + 1))))) <> ( LSeg (f,k))

                    proof

                      let k;

                      assume

                       A213: 1 <= k & (k + 1) <= ( len f);

                      then ( LSeg (f,k)) = ( LSeg ((f /. k),(f /. (k + 1)))) by TOPREAL1:def 3;

                      hence thesis by A210, A213;

                    end;

                    then

                     A214: 1 <= (j2 + 1) & (j2 + 1) <= ( width ( GoB f)) & 1 <= i2 & (i2 + 1) <= ( len ( GoB f)) implies not ((1 / 2) * ((( GoB f) * (i2,(j2 + 1))) + (( GoB f) * ((i2 + 1),(j2 + 1))))) in ( L~ f) by GOBOARD7: 40;

                    reconsider p = ((1 / 2) * ((( GoB f) * (i2,(j2 + 1))) + (( GoB f) * ((i2 + 1),(j2 + 1))))) as Point of ( TOP-REAL 2);

                    

                     A215: (p `1 ) = ((1 / 2) * (((( GoB f) * (i2,(j2 + 1))) + (( GoB f) * ((i2 + 1),(j2 + 1)))) `1 )) by TOPREAL3: 4

                    .= ((1 / 2) * (((( GoB f) * (i2,(j2 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 ))) by TOPREAL3: 2;

                    reconsider P = {p} as Subset of ( TOP-REAL 2);

                    

                     A216: 1 < ( len ( GoB f)) by GOBOARD7: 32;

                    ( Down (( RightComp f),(( L~ f) ` ))) is closed by Lm4, CONNSP_1: 33;

                    then

                     A217: ( Cl ( Down (( RightComp f),(( L~ f) ` )))) = ( Down (( RightComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    ( Down (( LeftComp f),(( L~ f) ` ))) is closed by Lm3, CONNSP_1: 33;

                    then

                     A218: ( Cl ( Down (( LeftComp f),(( L~ f) ` )))) = ( Down (( LeftComp f),(( L~ f) ` ))) by PRE_TOPC: 22;

                    (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) = ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by GOBRD11: 4;

                    then

                     A219: ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) = (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A218, A217, PRE_TOPC: 20;

                    

                     A220: 1 <= (j2 + 1) by NAT_1: 11;

                    

                     A221: ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` ))) c= ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) & ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` ))) = ( Int ( cell (( GoB f),i2,j2))) by A3, A4, Th3, PRE_TOPC: 18;

                    

                     A222: ( Down (( LeftComp f),(( L~ f) ` ))) = ( LeftComp f) & ( Down (( RightComp f),(( L~ f) ` ))) = ( RightComp f) by Th5;

                    ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` ))) c= (( LeftComp f) \/ ( RightComp f)) by A1, A2, A6, A7, Th3;

                    then ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` ))) c= ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` ))) by A222, GOBRD11: 4;

                    then

                     A223: ( Cl ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` )))) c= ( Cl ( Down ((( LeftComp f) \/ ( RightComp f)),(( L~ f) ` )))) by PRE_TOPC: 19;

                    

                     A224: ( 0 + 1) <= i2 by A210, NAT_1: 13;

                    then

                     A225: 1 < (i2 + 1) by NAT_1: 13;

                    (for x be object st x in P holds not x in ( L~ f)) implies P misses ( L~ f) by XBOOLE_0: 3;

                    then

                     A226: p in {p} & {p} c= (( L~ f) ` ) by A2, A126, A224, A211, A214, NAT_1: 13, SUBSET_1: 23, TARSKI:def 1;

                    then

                    reconsider p1 = p as Point of (( TOP-REAL 2) | (( L~ f) ` )) by PRE_TOPC: 8;

                    

                     A227: 1 <= (1 + j2) by NAT_1: 11;

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

                    then

                     A228: ((( GoB f) * (i2,(j2 + 1))) `1 ) < ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 ) by A2, A126, A224, A212, A220, GOBOARD5: 3;

                    then (((( GoB f) * (i2,(j2 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 )) < (((( GoB f) * ((i2 + 1),(j2 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 )) by XREAL_1: 8;

                    then

                     A229: ((((( GoB f) * (i2,(j2 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 )) / 2) < ((((( GoB f) * ((i2 + 1),(j2 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 )) / 2) by XREAL_1: 74;

                    (((( GoB f) * (i2,(j2 + 1))) `1 ) + ((( GoB f) * (i2,(j2 + 1))) `1 )) < (((( GoB f) * (i2,(j2 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 )) by A228, XREAL_1: 8;

                    then

                     A230: ((((( GoB f) * (i2,(j2 + 1))) `1 ) + ((( GoB f) * (i2,(j2 + 1))) `1 )) / 2) < ((((( GoB f) * (i2,(j2 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 )) / 2) by XREAL_1: 74;

                    p in { |[s, r]| where s,r be Real : ((( GoB f) * (i2,(j2 + 1))) `1 ) <= s & s <= ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 ) }

                    proof

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

                      hence thesis by A215, A230, A229;

                    end;

                    then

                     A231: p in ( v_strip (( GoB f),i2)) by A2, A126, A224, A211, A227, GOBOARD5: 8;

                    (p `2 ) = ((1 / 2) * (((( GoB f) * (i2,(j2 + 1))) + (( GoB f) * ((i2 + 1),(j2 + 1)))) `2 )) by TOPREAL3: 4

                    .= ((1 / 2) * (((( GoB f) * (i2,(j2 + 1))) `2 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 ))) by TOPREAL3: 2;

                    then

                     A232: p = |[((1 / 2) * (((( GoB f) * (i2,(j2 + 1))) `1 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `1 ))), ((1 / 2) * (((( GoB f) * (i2,(j2 + 1))) `2 ) + ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 )))]| by A215, EUCLID: 53;

                    

                     A233: j2 = 0 or j2 >= ( 0 + 1) by NAT_1: 13;

                     A234:

                    now

                      per cases by A2, A126, A233, XXREAL_0: 1;

                        case

                         A235: j2 >= 1 & (j2 + 1) < ( width ( GoB f));

                        then

                         A236: ((j2 + 1) + 1) <= ( width ( GoB f)) by NAT_1: 13;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,(j2 + 1))) `2 ) <= r & r <= ((( GoB f) * (1,((j2 + 1) + 1))) `2 ) }

                        proof

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

                          then

                           A237: ((( GoB f) * (1,(j2 + 1))) `2 ) < ((( GoB f) * (1,((j2 + 1) + 1))) `2 ) by A216, A220, A236, GOBOARD5: 4;

                          ((( GoB f) * (i2,(j2 + 1))) `2 ) = ((( GoB f) * (1,(j2 + 1))) `2 ) & ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 ) = ((( GoB f) * (1,(j2 + 1))) `2 ) by A2, A3, A126, A224, A212, A220, A225, GOBOARD5: 1;

                          hence thesis by A232, A237;

                        end;

                        then p in ( h_strip (( GoB f),(j2 + 1))) by A216, A227, A235, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),(j2 + 1))) /\ ( v_strip (( GoB f),i2))) by A231, XBOOLE_0:def 4;

                        then

                         A238: p in ( cell (( GoB f),i2,(j2 + 1))) by GOBOARD5:def 3;

                        

                         A239: p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,j2)) `2 ) <= r & r <= ((( GoB f) * (1,(j2 + 1))) `2 ) }

                        proof

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

                          then

                           A240: ((( GoB f) * (1,j2)) `2 ) < ((( GoB f) * (1,(j2 + 1))) `2 ) by A216, A235, GOBOARD5: 4;

                          ((( GoB f) * (i2,(j2 + 1))) `2 ) = ((( GoB f) * (1,(j2 + 1))) `2 ) & ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 ) = ((( GoB f) * (1,(j2 + 1))) `2 ) by A2, A3, A126, A224, A212, A220, A225, GOBOARD5: 1;

                          hence thesis by A232, A240;

                        end;

                        j2 < ( width ( GoB f)) by A235, NAT_1: 13;

                        then p in ( h_strip (( GoB f),j2)) by A216, A235, A239, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),j2)) /\ ( v_strip (( GoB f),i2))) by A231, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j2 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A226, A238, XBOOLE_0:def 4;

                      end;

                        case

                         A241: j2 >= 1 & (j2 + 1) = ( width ( GoB f));

                        

                         A242: j2 < (j2 + 1) by NAT_1: 13;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,j2)) `2 ) <= r & r <= ((( GoB f) * (1,(j2 + 1))) `2 ) }

                        proof

                          

                           A243: ((( GoB f) * (1,j2)) `2 ) < ((( GoB f) * (1,(j2 + 1))) `2 ) by A216, A241, A242, GOBOARD5: 4;

                          ((( GoB f) * (i2,(j2 + 1))) `2 ) = ((( GoB f) * (1,(j2 + 1))) `2 ) & ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 ) = ((( GoB f) * (1,(j2 + 1))) `2 ) by A2, A3, A126, A224, A212, A220, A225, GOBOARD5: 1;

                          hence thesis by A232, A243;

                        end;

                        then p in ( h_strip (( GoB f),j2)) by A216, A241, A242, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),j2)) /\ ( v_strip (( GoB f),i2))) by A231, XBOOLE_0:def 4;

                        then

                         A244: p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,(j2 + 1))) `2 ) <= r }

                        proof

                          ((( GoB f) * (i2,(j2 + 1))) `2 ) = ((( GoB f) * (1,(j2 + 1))) `2 ) & ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 ) = ((( GoB f) * (1,(j2 + 1))) `2 ) by A2, A3, A126, A224, A212, A220, A225, GOBOARD5: 1;

                          hence thesis by A232;

                        end;

                        then p in ( h_strip (( GoB f),(j2 + 1))) by A216, A241, GOBOARD5: 6;

                        then p in (( h_strip (( GoB f),(j2 + 1))) /\ ( v_strip (( GoB f),i2))) by A231, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,(j2 + 1))) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j2 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A226, A244, XBOOLE_0:def 4;

                      end;

                        case

                         A245: j2 = 0 & (j2 + 1) < ( width ( GoB f));

                        then

                         A246: ((j2 + 1) + 1) <= ( width ( GoB f)) by NAT_1: 13;

                        p in { |[s, r]| where s,r be Real : ((( GoB f) * (1,(j2 + 1))) `2 ) <= r & r <= ((( GoB f) * (1,((j2 + 1) + 1))) `2 ) }

                        proof

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

                          then

                           A247: ((( GoB f) * (1,(j2 + 1))) `2 ) < ((( GoB f) * (1,((j2 + 1) + 1))) `2 ) by A216, A220, A246, GOBOARD5: 4;

                          ((( GoB f) * (i2,(j2 + 1))) `2 ) = ((( GoB f) * (1,(j2 + 1))) `2 ) & ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 ) = ((( GoB f) * (1,(j2 + 1))) `2 ) by A2, A3, A126, A224, A212, A220, A225, GOBOARD5: 1;

                          hence thesis by A232, A247;

                        end;

                        then p in ( h_strip (( GoB f),j1)) by A126, A216, A245, GOBOARD5: 5;

                        then p in (( h_strip (( GoB f),(j2 + 1))) /\ ( v_strip (( GoB f),i2))) by A126, A231, XBOOLE_0:def 4;

                        then

                         A248: p in ( cell (( GoB f),i2,(j2 + 1))) by GOBOARD5:def 3;

                        p in { |[s, r]| where s,r be Real : r <= ((( GoB f) * (1,1)) `2 ) }

                        proof

                          ((( GoB f) * (i2,(j2 + 1))) `2 ) = ((( GoB f) * (1,(j2 + 1))) `2 ) & ((( GoB f) * ((i2 + 1),(j2 + 1))) `2 ) = ((( GoB f) * (1,(j2 + 1))) `2 ) by A2, A3, A126, A224, A212, A220, A225, GOBOARD5: 1;

                          hence thesis by A232, A245;

                        end;

                        then p in ( h_strip (( GoB f),j2)) by A216, A245, GOBOARD5: 7;

                        then p in (( h_strip (( GoB f),j2)) /\ ( v_strip (( GoB f),i2))) by A231, XBOOLE_0:def 4;

                        then p in ( cell (( GoB f),i2,j2)) by GOBOARD5:def 3;

                        hence p in (( cell (( GoB f),i2,(j2 + 1))) /\ (( L~ f) ` )) & p in (( cell (( GoB f),i2,j2)) /\ (( L~ f) ` )) by A226, A248, XBOOLE_0:def 4;

                      end;

                        case j2 = 0 & (j2 + 1) = ( width ( GoB f));

                        hence contradiction by GOBOARD7: 33;

                      end;

                    end;

                    then p in ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) by A3, A4, Th2;

                    then

                     A249: ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) c= ( Component_of p1) by A3, A4, Th3, GOBRD11: 1;

                    p in ( Cl ( Down (( Int ( cell (( GoB f),i2,j1))),(( L~ f) ` )))) by A3, A126, A234, Th2;

                    then ( Component_of p1) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A223, A219, Th5, CONNSP_3: 21;

                    then ( Cl ( Down (( Int ( cell (( GoB f),i2,j2))),(( L~ f) ` )))) c= (( Down (( LeftComp f),(( L~ f) ` ))) \/ ( Down (( RightComp f),(( L~ f) ` )))) by A249;

                    hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f)) by A222, A221;

                  end;

                end;

                hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f));

              end;

            end;

            hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f));

          end;

        end;

        hence ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f));

      end;

      hence thesis;

    end;

    theorem :: GOBRD12:6

    

     Th6: for i1, j1, i2, j2 st i1 <= ( len ( GoB f)) & j1 <= ( width ( GoB f)) & i2 <= ( len ( GoB f)) & j2 <= ( width ( GoB f)) & (i1,j1,i2,j2) are_adjacent holds ( Int ( cell (( GoB f),i1,j1))) c= (( LeftComp f) \/ ( RightComp f)) iff ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f))

    proof

      let i1, j1, i2, j2;

      assume that

       A1: i1 <= ( len ( GoB f)) & j1 <= ( width ( GoB f)) and

       A2: i2 <= ( len ( GoB f)) and

       A3: j2 <= ( width ( GoB f)) and

       A4: (i1,j1,i2,j2) are_adjacent ;

      

       A5: (i1,i2) are_adjacent & j1 = j2 or i1 = i2 & (j1,j2) are_adjacent by A4, GOBRD10:def 2;

      now

        per cases by A5, GOBRD10:def 1;

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

          hence thesis by A1, A2, Lm5;

        end;

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

          hence thesis by A1, A3, Lm6;

        end;

      end;

      hence thesis;

    end;

    theorem :: GOBRD12:7

    

     Th7: for F1,F2 be FinSequence of NAT st ( len F1) = ( len F2) & (ex i st i in ( dom F1) & ( Int ( cell (( GoB f),(F1 /. i),(F2 /. i)))) c= (( LeftComp f) \/ ( RightComp f))) & (for i, k1, k2 st i in ( dom F1) & k1 = (F1 . i) & k2 = (F2 . i) holds k1 <= ( len ( GoB f)) & k2 <= ( width ( GoB f))) holds for i st i in ( dom F1) holds ( Int ( cell (( GoB f),(F1 /. i),(F2 /. i)))) c= (( LeftComp f) \/ ( RightComp f))

    proof

      let F1,F2 be FinSequence of NAT ;

      assume that

       A1: ( len F1) = ( len F2) and

       A2: ex i st i in ( dom F1) & ( Int ( cell (( GoB f),(F1 /. i),(F2 /. i)))) c= (( LeftComp f) \/ ( RightComp f)) and

       A3: for i, k1, k2 st i in ( dom F1) & k1 = (F1 . i) & k2 = (F2 . i) holds k1 <= ( len ( GoB f)) & k2 <= ( width ( GoB f));

      consider i1 such that

       A4: i1 in ( dom F1) and

       A5: ( Int ( cell (( GoB f),(F1 /. i1),(F2 /. i1)))) c= (( LeftComp f) \/ ( RightComp f)) by A2;

      reconsider kw1 = (F1 /. i1), kw2 = (F2 /. i1) as Element of NAT ;

      reconsider k1 = (kw1 + 1), k2 = (kw2 + 1) as Element of NAT ;

      ( dom F1) = ( Seg ( len F1)) by FINSEQ_1:def 3;

      then ( dom F1) = ( dom F2) by A1, FINSEQ_1:def 3;

      then

       A6: (F2 /. i1) = (F2 . i1) by A4, PARTFUN1:def 6;

      

       A7: (F1 /. i1) = (F1 . i1) by A4, PARTFUN1:def 6;

      then kw1 <= ( len ( GoB f)) by A3, A4, A6;

      then

       A8: k1 <= (( len ( GoB f)) + 1) by XREAL_1: 6;

      kw2 <= ( width ( GoB f)) by A3, A4, A7, A6;

      then

       A9: k2 <= (( width ( GoB f)) + 1) by XREAL_1: 6;

      

       A10: (k1 -' 1) = (F1 /. i1) & (k2 -' 1) = (F2 /. i1) by NAT_D: 34;

      set n = ( len ( GoB f)), m = ( width ( GoB f));

      defpred P[ Nat, Nat, set] means $3 = ( Int ( cell (( GoB f),($1 -' 1),($2 -' 1))));

      reconsider F = (( LeftComp f) \/ ( RightComp f)) as Subset of ( REAL 2) by EUCLID: 22;

      

       A11: for i,j be Nat st [i, j] in [:( Seg (( len ( GoB f)) + 1)), ( Seg (( width ( GoB f)) + 1)):] holds ex x be Subset of ( REAL 2) st P[i, j, x] by Lm2;

      ex Mm be Matrix of (( len ( GoB f)) + 1), (( width ( GoB f)) + 1), ( bool ( REAL 2)) st for i,j be Nat st [i, j] in ( Indices Mm) holds P[i, j, (Mm * (i,j))] from MATRIX_0:sch 2( A11);

      then

      consider Mm be Matrix of (( len ( GoB f)) + 1), (( width ( GoB f)) + 1), ( bool ( REAL 2)) such that

       A12: for i,j be Nat st [i, j] in ( Indices Mm) holds (Mm * (i,j)) = ( Int ( cell (( GoB f),(i -' 1),(j -' 1))));

      

       A13: ( len Mm) = (( len ( GoB f)) + 1) by MATRIX_0:def 2;

      then

       A14: ( dom Mm) = ( Seg (( len ( GoB f)) + 1)) by FINSEQ_1:def 3;

      

       A15: ( Seg (( width ( GoB f)) + 1)) = ( Seg ( width Mm)) by A13, MATRIX_0: 20;

      

       A16: (( width ( GoB f)) + 1) = ( width Mm) by A13, MATRIX_0: 20;

      

       A17: for i1,j1,i2,j2 be Element of NAT st i1 in ( Seg (( len ( GoB f)) + 1)) & i2 in ( Seg (( len ( GoB f)) + 1)) & j1 in ( Seg (( width ( GoB f)) + 1)) & j2 in ( Seg (( width ( GoB f)) + 1)) & (i1,j1,i2,j2) are_adjacent holds (Mm * (i1,j1)) c= (( LeftComp f) \/ ( RightComp f)) iff (Mm * (i2,j2)) c= (( LeftComp f) \/ ( RightComp f))

      proof

        let i1,j1,i2,j2 be Element of NAT ;

        assume that

         A18: i1 in ( Seg (( len ( GoB f)) + 1)) and

         A19: i2 in ( Seg (( len ( GoB f)) + 1)) and

         A20: j1 in ( Seg (( width ( GoB f)) + 1)) and

         A21: j2 in ( Seg (( width ( GoB f)) + 1)) and

         A22: (i1,j1,i2,j2) are_adjacent ;

        

         A23: 1 <= i2 by A19, FINSEQ_1: 1;

        then 0 <= (i2 - 1) by XREAL_1: 48;

        then

         A24: (i2 -' 1) = (i2 - 1) by XREAL_0:def 2;

         [i2, j2] in [:( dom Mm), ( Seg ( width Mm)):] by A14, A15, A19, A21, ZFMISC_1: 87;

        then [i2, j2] in ( Indices Mm) by MATRIX_0:def 4;

        then

         A25: (Mm * (i2,j2)) = ( Int ( cell (( GoB f),(i2 -' 1),(j2 -' 1)))) by A12;

        reconsider ii1 = (i1 -' 1), ii2 = (i2 -' 1), jj1 = (j1 -' 1), jj2 = (j2 -' 1) as Element of NAT ;

        

         A26: 1 <= i1 by A18, FINSEQ_1: 1;

        then 0 <= (i1 - 1) by XREAL_1: 48;

        then

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

         [i1, j1] in [:( dom Mm), ( Seg ( width Mm)):] by A14, A16, A18, A20, ZFMISC_1: 87;

        then [i1, j1] in ( Indices Mm) by MATRIX_0:def 4;

        then

         A28: (Mm * (i1,j1)) = ( Int ( cell (( GoB f),(i1 -' 1),(j1 -' 1)))) by A12;

        

         A29: 1 <= j2 by A21, FINSEQ_1: 1;

        then 0 <= (j2 - 1) by XREAL_1: 48;

        then

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

        i2 <= (( len ( GoB f)) + 1) by A19, FINSEQ_1: 1;

        then

         A31: (i2 -' 1) <= ((( len ( GoB f)) + 1) - 1) by A24, XREAL_1: 9;

        

         A32: 1 <= j1 by A20, FINSEQ_1: 1;

        then 0 <= (j1 - 1) by XREAL_1: 48;

        then

         A33: (j1 -' 1) = (j1 - 1) by XREAL_0:def 2;

        j2 <= (( width ( GoB f)) + 1) by A21, FINSEQ_1: 1;

        then

         A34: (j2 -' 1) <= ((( width ( GoB f)) + 1) - 1) by A30, XREAL_1: 9;

        j1 <= (( width ( GoB f)) + 1) by A20, FINSEQ_1: 1;

        then

         A35: (j1 -' 1) <= ((( width ( GoB f)) + 1) - 1) by A33, XREAL_1: 9;

        i1 <= (( len ( GoB f)) + 1) by A18, FINSEQ_1: 1;

        then

         A36: (i1 -' 1) <= ((( len ( GoB f)) + 1) - 1) by A27, XREAL_1: 9;

        (ii1,jj1,ii2,jj2) are_adjacent by A22, A26, A23, A32, A29, GOBRD10: 4;

        hence thesis by A36, A31, A35, A34, A28, A25, Th6;

      end;

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

      then

       A37: k2 in ( Seg (m + 1)) by A9, FINSEQ_1: 1;

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

      then

       A38: k1 in ( Seg (n + 1)) by A8, FINSEQ_1: 1;

      then [k1, k2] in [:( dom Mm), ( Seg ( width Mm)):] by A37, A14, A15, ZFMISC_1: 87;

      then [k1, k2] in ( Indices Mm) by MATRIX_0:def 4;

      then (Mm * (k1,k2)) c= (( LeftComp f) \/ ( RightComp f)) by A5, A12, A10;

      then

       A39: for i,j be Element of NAT st i in ( Seg (n + 1)) & j in ( Seg (m + 1)) holds (Mm * (i,j)) c= F by A38, A37, A17, GOBRD10: 8;

      thus for i st i in ( dom F1) holds ( Int ( cell (( GoB f),(F1 /. i),(F2 /. i)))) c= (( LeftComp f) \/ ( RightComp f))

      proof

        let i;

        assume

         A40: i in ( dom F1);

        reconsider kx1 = (F1 /. i), kx2 = (F2 /. i) as Element of NAT ;

        reconsider kk1 = (kx1 + 1), kk2 = (kx2 + 1) as Element of NAT ;

        ( dom F1) = ( Seg ( len F1)) by FINSEQ_1:def 3;

        then ( dom F1) = ( dom F2) by A1, FINSEQ_1:def 3;

        then

         A41: (F2 /. i) = (F2 . i) by A40, PARTFUN1:def 6;

        

         A42: (F1 /. i) = (F1 . i) by A40, PARTFUN1:def 6;

        then kx1 <= ( len ( GoB f)) by A3, A40, A41;

        then

         A43: kk1 <= (( len ( GoB f)) + 1) by XREAL_1: 6;

        kx2 <= ( width ( GoB f)) by A3, A40, A42, A41;

        then

         A44: kk2 <= (( width ( GoB f)) + 1) by XREAL_1: 6;

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

        then

         A45: kk2 in ( Seg (( width ( GoB f)) + 1)) by A44, FINSEQ_1: 1;

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

        then

         A46: kk1 in ( Seg (( len ( GoB f)) + 1)) by A43, FINSEQ_1: 1;

        

         A47: ( len Mm) = (( len ( GoB f)) + 1) by MATRIX_0:def 2;

        ( dom Mm) = ( Seg (( len ( GoB f)) + 1)) & ( Seg (( width ( GoB f)) + 1)) = ( Seg ( width Mm)) by A47, FINSEQ_1:def 3, MATRIX_0: 20;

        then [kk1, kk2] in [:( dom Mm), ( Seg ( width Mm)):] by A46, A45, ZFMISC_1: 87;

        then

         A48: [kk1, kk2] in ( Indices Mm) by MATRIX_0:def 4;

        

         A49: (kk1 -' 1) = (F1 /. i) & (kk2 -' 1) = (F2 /. i) by NAT_D: 34;

        (Mm * (kk1,kk2)) c= (( LeftComp f) \/ ( RightComp f)) by A39, A46, A45;

        hence thesis by A12, A49, A48;

      end;

    end;

    theorem :: GOBRD12:8

    

     Th8: ex i, j st i <= ( len ( GoB f)) & j <= ( width ( GoB f)) & ( Int ( cell (( GoB f),i,j))) c= (( LeftComp f) \/ ( RightComp f))

    proof

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

      then

       A1: (ex i, j st i <= ( len ( GoB f)) & j <= ( width ( GoB f)) & ( cell (( GoB f),i,j)) = ( left_cell (f,1))) & ( Int ( left_cell (f,1))) c= ( LeftComp f) by GOBOARD9: 11, GOBOARD9: 21;

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

      hence thesis by A1, XBOOLE_1: 1;

    end;

    theorem :: GOBRD12:9

    

     Th9: for i, j st i <= ( len ( GoB f)) & j <= ( width ( GoB f)) holds ( Int ( cell (( GoB f),i,j))) c= (( LeftComp f) \/ ( RightComp f))

    proof

      let i, j;

      set n = ( len ( GoB f)), m = ( width ( GoB f));

      consider i2, j2 such that

       A1: i2 <= n & j2 <= m and

       A2: ( Int ( cell (( GoB f),i2,j2))) c= (( LeftComp f) \/ ( RightComp f)) by Th8;

      

       A3: i in NAT & j in NAT & i2 in NAT & j2 in NAT & n in NAT & m in NAT by ORDINAL1:def 12;

      assume i <= ( len ( GoB f)) & j <= ( width ( GoB f));

      then

      consider fs1,fs2 be FinSequence of NAT such that

       A4: for k,k1,k2 be Element of NAT st k in ( dom fs1) & k1 = (fs1 . k) & k2 = (fs2 . k) holds k1 <= n & k2 <= m and

       A5: (fs1 . 1) = i and

       A6: (fs1 . ( len fs1)) = i2 and

       A7: (fs2 . 1) = j and

       A8: (fs2 . ( len fs2)) = j2 and

       A9: ( len fs1) = ( len fs2) and

       A10: ( len fs1) = (((((i -' i2) + (i2 -' i)) + (j -' j2)) + (j2 -' j)) + 1) and for k be Element of NAT st 1 <= k & k < ( len fs1) holds ((fs1 /. k),(fs2 /. k),(fs1 /. (k + 1)),(fs2 /. (k + 1))) are_adjacent by A1, GOBRD10: 7, A3;

      

       A11: for k,k1,k2 be Nat st k in ( dom fs1) & k1 = (fs1 . k) & k2 = (fs2 . k) holds k1 <= n & k2 <= m

      proof

        let k,k1,k2 be Nat;

        k in NAT & k1 in NAT & k2 in NAT by ORDINAL1:def 12;

        hence thesis by A4;

      end;

      

       A12: 1 <= (1 + ((((i -' i2) + (i2 -' i)) + (j -' j2)) + (j2 -' j))) by NAT_1: 12;

      then

       A13: 1 in ( dom fs1) by A10, FINSEQ_3: 25;

      then

       A14: (fs1 /. 1) = i by A5, PARTFUN1:def 6;

      

       A15: 1 <= (1 + ((((i -' i2) + (i2 -' i)) + (j -' j2)) + (j2 -' j))) by NAT_1: 12;

      then ( len fs2) in ( dom fs2) by A9, A10, FINSEQ_3: 25;

      then

       A16: j2 = (fs2 /. ( len fs1)) by A8, A9, PARTFUN1:def 6;

      1 in ( dom fs2) by A9, A10, A12, FINSEQ_3: 25;

      then

       A17: (fs2 /. 1) = j by A7, PARTFUN1:def 6;

      

       A18: ( len fs1) in ( dom fs1) by A10, A15, FINSEQ_3: 25;

      then i2 = (fs1 /. ( len fs1)) by A6, PARTFUN1:def 6;

      hence thesis by A2, A9, A18, A16, A13, A14, A17, Th7, A11;

    end;

    ::$Notion-Name

    theorem :: GOBRD12:10

    (( L~ f) ` ) = (( LeftComp f) \/ ( RightComp f))

    proof

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

      then

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

       A1: B1 = ( LeftComp f) and B1 is a_component by CONNSP_1:def 6;

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

      then

       A2: ( LeftComp f) c= (( L~ f) ` ) by A1, Lm1;

      ( union { ( Cl ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` )))) : i <= ( len ( GoB f)) & j <= ( width ( GoB f)) }) c= (( LeftComp f) \/ ( RightComp f))

      proof

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

        then

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

         A3: B2 = ( RightComp f) and

         A4: B2 is a_component by CONNSP_1:def 6;

        ( Cl B2) = (( Cl ( RightComp f)) /\ ( [#] (( TOP-REAL 2) | (( L~ f) ` )))) by A3, PRE_TOPC: 17;

        then

         A5: ( Cl B2) = (( Cl ( RightComp f)) /\ (( L~ f) ` )) by PRE_TOPC:def 5;

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

        B2 is closed by A4, CONNSP_1: 33;

        then

         A6: (( Cl ( RightComp f)) /\ (( L~ f) ` )) = ( RightComp f) by A3, A5, PRE_TOPC: 22;

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

        then

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

         A7: B1 = ( LeftComp f) and

         A8: B1 is a_component by CONNSP_1:def 6;

        ( Cl B1) = (( Cl ( LeftComp f)) /\ ( [#] (( TOP-REAL 2) | (( L~ f) ` )))) by A7, PRE_TOPC: 17;

        then

         A9: ( Cl B1) = (( Cl ( LeftComp f)) /\ (( L~ f) ` )) by PRE_TOPC:def 5;

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

        B1 is closed by A8, CONNSP_1: 33;

        then

         A10: ((( Cl ( LeftComp f)) \/ ( Cl ( RightComp f))) /\ (( L~ f) ` )) = ((( Cl ( LeftComp f)) /\ (( L~ f) ` )) \/ (( Cl ( RightComp f)) /\ (( L~ f) ` ))) & (( Cl ( LeftComp f)) /\ (( L~ f) ` )) = ( LeftComp f) by A7, A9, PRE_TOPC: 22, XBOOLE_1: 23;

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

        let x be object;

        

         A11: ( Cl (( LeftComp f) \/ ( RightComp f))) = (( Cl ( LeftComp f)) \/ ( Cl ( RightComp f))) by PRE_TOPC: 20;

        assume x in ( union { ( Cl ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` )))) : i <= ( len ( GoB f)) & j <= ( width ( GoB f)) });

        then

        consider y be set such that

         A12: x in y & y in { ( Cl ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` )))) : i <= ( len ( GoB f)) & j <= ( width ( GoB f)) } by TARSKI:def 4;

        consider i, j such that

         A13: y = ( Cl ( Down (( Int ( cell (( GoB f),i,j))),(( L~ f) ` )))) and

         A14: i <= ( len ( GoB f)) & j <= ( width ( GoB f)) by A12;

        ( Cl ( Int ( cell (( GoB f),i,j)))) c= ( Cl (( LeftComp f) \/ ( RightComp f))) by A14, Th9, PRE_TOPC: 19;

        then

         A15: (( Cl ( Int ( cell (( GoB f),i,j)))) /\ (( L~ f) ` )) c= ((( Cl ( LeftComp f)) \/ ( Cl ( RightComp f))) /\ (( L~ f) ` )) by A11, XBOOLE_1: 26;

        reconsider P = ( Int ( cell (( GoB f),i,j))) as Subset of ( TOP-REAL 2);

        ( Cl ( Down (P,Q))) = (( Cl P) /\ Q) by A14, Th1, CONNSP_3: 29;

        hence thesis by A12, A13, A15, A10, A6;

      end;

      then

       A16: (( L~ f) ` ) c= (( LeftComp f) \/ ( RightComp f)) by Th4;

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

      then

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

       A17: B1 = ( RightComp f) and B1 is a_component by CONNSP_1:def 6;

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

      then B1 c= (( L~ f) ` ) by Lm1;

      then (( LeftComp f) \/ ( RightComp f)) c= (( L~ f) ` ) by A2, A17, XBOOLE_1: 8;

      hence thesis by A16, XBOOLE_0:def 10;

    end;