gobrd11.miz



    begin

    reserve i,j,k for Nat,

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

x for set,

GX for non empty TopSpace;

    

     Lm1: ( sqrt 2) > 0 by SQUARE_1: 25;

    theorem :: GOBRD11:1

    

     Th1: for A be Subset of GX, p be Point of GX st p in A & A is connected holds A c= ( Component_of p)

    proof

      let A be Subset of GX, p be Point of GX;

      consider F be Subset-Family of GX such that

       A1: for B be Subset of GX holds B in F iff B is connected & p in B and

       A2: ( union F) = ( Component_of p) by CONNSP_1:def 7;

      assume p in A & A is connected;

      then

       A3: A in F by A1;

      A c= ( union F) by A3, TARSKI:def 4;

      hence thesis by A2;

    end;

    theorem :: GOBRD11:2

    for A,B,C be Subset of GX st C is a_component & A c= C & B is connected & ( Cl A) meets ( Cl B) holds B c= C

    proof

      let A,B,C be Subset of GX;

      assume that

       A1: C is a_component and

       A2: A c= C and

       A3: B is connected and

       A4: (( Cl A) /\ ( Cl B)) <> {} ;

      consider p be Point of GX such that

       A5: p in (( Cl A) /\ ( Cl B)) by A4, SUBSET_1: 4;

      reconsider C9 = C as Subset of GX;

      C9 is closed by A1, CONNSP_1: 33;

      then ( Cl C) = C by PRE_TOPC: 22;

      then

       A6: ( Cl A) c= C by A2, PRE_TOPC: 19;

      p in ( Cl A) by A5, XBOOLE_0:def 4;

      then

       A7: ( Component_of p) = C9 by A1, A6, CONNSP_1: 41;

      p in ( Cl B) by A5, XBOOLE_0:def 4;

      then

       A8: ( Cl B) c= ( Component_of p) by A3, Th1, CONNSP_1: 19;

      B c= ( Cl B) by PRE_TOPC: 18;

      hence thesis by A7, A8;

    end;

    reserve GZ for non empty TopSpace;

    theorem :: GOBRD11:3

    for A,B be Subset of GZ st A is a_component & B is a_component holds (A \/ B) is a_union_of_components of GZ

    proof

      let A,B be Subset of GZ;

       {A, B} c= ( bool the carrier of GZ)

      proof

        let x be object;

        assume x in {A, B};

        then x = A or x = B by TARSKI:def 2;

        hence thesis;

      end;

      then

      reconsider F2 = {A, B} as Subset-Family of GZ;

      reconsider F = F2 as Subset-Family of GZ;

      assume A is a_component & B is a_component;

      then

       A1: for B1 be Subset of GZ st B1 in F holds B1 is a_component by TARSKI:def 2;

      (A \/ B) = ( union F) by ZFMISC_1: 75;

      hence thesis by A1, CONNSP_3:def 2;

    end;

    theorem :: GOBRD11:4

    for B1,B2,V be Subset of GX holds ( Down ((B1 \/ B2),V)) = (( Down (B1,V)) \/ ( Down (B2,V)))

    proof

      let B1,B2,V be Subset of GX;

      

       A1: ( Down (B2,V)) = (B2 /\ V) by CONNSP_3:def 5;

      ( Down ((B1 \/ B2),V)) = ((B1 \/ B2) /\ V) & ( Down (B1,V)) = (B1 /\ V) by CONNSP_3:def 5;

      hence thesis by A1, XBOOLE_1: 23;

    end;

    theorem :: GOBRD11:5

    for B1,B2,V be Subset of GX holds ( Down ((B1 /\ B2),V)) = (( Down (B1,V)) /\ ( Down (B2,V)))

    proof

      let B1,B2,V be Subset of GX;

      ( Down ((B1 /\ B2),V)) = ((B1 /\ B2) /\ V) by CONNSP_3:def 5;

      

      then

       A1: ( Down ((B1 /\ B2),V)) = (B1 /\ (B2 /\ (V /\ V))) by XBOOLE_1: 16

      .= (B1 /\ ((B2 /\ V) /\ V)) by XBOOLE_1: 16

      .= ((B1 /\ V) /\ (B2 /\ V)) by XBOOLE_1: 16;

      ( Down (B1,V)) = (B1 /\ V) by CONNSP_3:def 5;

      hence thesis by A1, CONNSP_3:def 5;

    end;

    reserve f for non constant standard special_circular_sequence,

G for non empty-yielding Matrix of ( TOP-REAL 2);

    theorem :: GOBRD11:6

    

     Th6: (( L~ f) ` ) <> {}

    proof

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

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

      hence thesis;

    end;

    registration

      let f;

      cluster (( L~ f) ` ) -> non empty;

      coherence by Th6;

    end

    

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

    theorem :: GOBRD11:7

    for f holds the carrier of ( TOP-REAL 2) = ( union { ( cell (( GoB f),i,j)) : i <= ( len ( GoB f)) & j <= ( width ( GoB f)) })

    proof

      let f;

      set j1 = ( len ( GoB f)), j2 = ( width ( GoB f));

      thus the carrier of ( TOP-REAL 2) c= ( union { ( cell (( GoB f),i,j)) : i <= j1 & j <= j2 })

      proof

        let x be object;

        assume x in the carrier of ( TOP-REAL 2);

        then

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

        set r = (p `1 );

         A1:

        now

          assume that

           A2: not r < ((( GoB f) * (1,1)) `1 ) and

           A3: not ((( GoB f) * (( len ( GoB f)),1)) `1 ) <= r;

          now

            reconsider l = ( len ( GoB f)) as Nat;

            defpred P[ Nat] means $1 = 0 or (1 <= $1 & $1 < ( len ( GoB f)) implies ((( GoB f) * (($1 + 1),1)) `1 ) <= r);

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

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

            then

             A4: ((1 + 1) - 1) <= (l - 1) by XREAL_1: 9;

            assume

             A5: not ex j st 1 <= j & j < ( len ( GoB f)) & ((( GoB f) * (j,1)) `1 ) <= r & r < ((( GoB f) * ((j + 1),1)) `1 );

            

             A6: for k holds P[k] implies P[(k + 1)]

            proof

              let k;

              assume

               A7: k = 0 or (1 <= k & k < ( len ( GoB f)) implies ((( GoB f) * ((k + 1),1)) `1 ) <= r);

              1 <= (k + 1) & (k + 1) < ( len ( GoB f)) implies ((( GoB f) * (((k + 1) + 1),1)) `1 ) <= r

              proof

                assume

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

                now

                  assume

                   A9: r < ((( GoB f) * (((k + 1) + 1),1)) `1 );

                  then k <> 0 by A2, A5, GOBOARD7: 32;

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

                  hence contradiction by A5, A7, A8, A9, XREAL_1: 145;

                end;

                hence thesis;

              end;

              hence thesis;

            end;

            

             A10: P[ 0 ];

            

             A11: for j holds P[j] from NAT_1:sch 2( A10, A6);

            

             A12: (l - 1) < ((l - 1) + 1) by XREAL_1: 29;

            then

            reconsider l1 = (l - 1) as Nat by A4, SPPOL_1: 2;

             0 < l1 by A4;

            hence contradiction by A3, A11, A4, A12;

          end;

          hence ex j st 1 <= j & j < ( len ( GoB f)) & ((( GoB f) * (j,1)) `1 ) <= r & r < ((( GoB f) * ((j + 1),1)) `1 );

        end;

        now

          per cases by A1;

            case

             A13: r < ((( GoB f) * (1,1)) `1 );

            reconsider G = ( GoB f) as Go-board;

            1 <= ( width G) by GOBOARD7: 33;

            then

             A14: ( v_strip (G, 0 )) = { |[r1, s]| where r1,s be Real : r1 <= ((G * (1,1)) `1 ) } by GOBOARD5: 10;

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

            then p in ( v_strip (( GoB f), 0 )) by A14, EUCLID: 53;

            hence ex j0 be Nat st j0 <= j1 & x in ( v_strip (( GoB f),j0));

          end;

            case

             A15: ((( GoB f) * (( len ( GoB f)),1)) `1 ) <= r;

            reconsider G = ( GoB f) as Go-board;

            1 <= ( width G) by GOBOARD7: 33;

            then

             A16: ( v_strip (G,( len G))) = { |[r1, s]| where r1,s be Real : ((G * (( len G),1)) `1 ) <= r1 } by GOBOARD5: 9;

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

            then p in ( v_strip (( GoB f),( len ( GoB f)))) by A16, EUCLID: 53;

            hence ex j0 be Nat st j0 <= j1 & x in ( v_strip (( GoB f),j0));

          end;

            case

             A17: ex j st 1 <= j & j < ( len ( GoB f)) & ((( GoB f) * (j,1)) `1 ) <= r & r < ((( GoB f) * ((j + 1),1)) `1 );

            reconsider G = ( GoB f) as Go-board;

            consider j such that

             A18: 1 <= j and

             A19: j < ( len ( GoB f)) and

             A20: ((( GoB f) * (j,1)) `1 ) <= r & r < ((( GoB f) * ((j + 1),1)) `1 ) by A17;

            

             A21: |[r, (p `2 )]| in { |[r1, s]| where r1,s be Real : ((G * (j,1)) `1 ) <= r1 & r1 <= ((G * ((j + 1),1)) `1 ) } by A20;

            1 <= ( width G) by GOBOARD7: 33;

            then ( v_strip (G,j)) = { |[r1, s]| where r1,s be Real : ((G * (j,1)) `1 ) <= r1 & r1 <= ((G * ((j + 1),1)) `1 ) } by A18, A19, GOBOARD5: 8;

            then p in ( v_strip (( GoB f),j)) by A21, EUCLID: 53;

            hence ex j0 be Nat st j0 <= j1 & x in ( v_strip (( GoB f),j0)) by A19;

          end;

        end;

        then

        consider j0 be Nat such that

         A22: j0 <= j1 and

         A23: x in ( v_strip (( GoB f),j0));

        set s = (p `2 );

         A24:

        now

          assume that

           A25: not s < ((( GoB f) * (1,1)) `2 ) and

           A26: not ((( GoB f) * (1,( width ( GoB f)))) `2 ) <= s;

          now

            reconsider l = ( width ( GoB f)) as Nat;

            defpred P[ Nat] means $1 = 0 or (1 <= $1 & $1 < ( width ( GoB f)) implies ((( GoB f) * (1,($1 + 1))) `2 ) <= s);

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

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

            then

             A27: ((1 + 1) - 1) <= (l - 1) by XREAL_1: 9;

            assume

             A28: not ex j st 1 <= j & j < ( width ( GoB f)) & ((( GoB f) * (1,j)) `2 ) <= s & s < ((( GoB f) * (1,(j + 1))) `2 );

            

             A29: for k holds P[k] implies P[(k + 1)]

            proof

              let k;

              assume

               A30: k = 0 or (1 <= k & k < ( width ( GoB f)) implies ((( GoB f) * (1,(k + 1))) `2 ) <= s);

              1 <= (k + 1) & (k + 1) < ( width ( GoB f)) implies ((( GoB f) * (1,((k + 1) + 1))) `2 ) <= s

              proof

                assume

                 A31: 1 <= (k + 1) & (k + 1) < ( width ( GoB f));

                now

                  assume

                   A32: s < ((( GoB f) * (1,((k + 1) + 1))) `2 );

                  then k <> 0 by A25, A28, GOBOARD7: 33;

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

                  hence contradiction by A28, A30, A31, A32, XREAL_1: 145;

                end;

                hence thesis;

              end;

              hence thesis;

            end;

            

             A33: P[ 0 ];

            

             A34: for j holds P[j] from NAT_1:sch 2( A33, A29);

            

             A35: (l - 1) < ((l - 1) + 1) by XREAL_1: 29;

            then

            reconsider l1 = (l - 1) as Nat by A27, SPPOL_1: 2;

             0 < l1 by A27;

            hence contradiction by A26, A34, A27, A35;

          end;

          hence ex j st 1 <= j & j < ( width ( GoB f)) & ((( GoB f) * (1,j)) `2 ) <= s & s < ((( GoB f) * (1,(j + 1))) `2 );

        end;

        now

          per cases by A24;

            case

             A36: s < ((( GoB f) * (1,1)) `2 );

            reconsider G = ( GoB f) as Go-board;

            1 <= ( len G) by GOBOARD7: 32;

            then

             A37: ( h_strip (G, 0 )) = { |[r1, s1]| : s1 <= ((G * (1,1)) `2 ) } by GOBOARD5: 7;

             |[r, s]| in { |[r1, s1]| : s1 <= ((( GoB f) * (1,1)) `2 ) } by A36;

            then p in ( h_strip (( GoB f), 0 )) by A37, EUCLID: 53;

            hence ex i0 be Nat st i0 <= j2 & x in ( h_strip (( GoB f),i0));

          end;

            case

             A38: ((( GoB f) * (1,( width ( GoB f)))) `2 ) <= s;

            reconsider G = ( GoB f) as Go-board;

            1 <= ( len G) by GOBOARD7: 32;

            then

             A39: ( h_strip (G,( width G))) = { |[r1, s1]| : ((G * (1,( width G))) `2 ) <= s1 } by GOBOARD5: 6;

             |[r, s]| in { |[r1, s1]| : ((( GoB f) * (1,( width G))) `2 ) <= s1 } by A38;

            then p in ( h_strip (( GoB f),( width ( GoB f)))) by A39, EUCLID: 53;

            hence ex i0 be Nat st i0 <= j2 & x in ( h_strip (( GoB f),i0));

          end;

            case

             A40: ex j st 1 <= j & j < ( width ( GoB f)) & ((( GoB f) * (1,j)) `2 ) <= s & s < ((( GoB f) * (1,(j + 1))) `2 );

            reconsider G = ( GoB f) as Go-board;

            consider j such that

             A41: 1 <= j and

             A42: j < ( width ( GoB f)) and

             A43: ((( GoB f) * (1,j)) `2 ) <= s & s < ((( GoB f) * (1,(j + 1))) `2 ) by A40;

            

             A44: |[r, s]| in { |[r1, s1]| : ((G * (1,j)) `2 ) <= s1 & s1 <= ((G * (1,(j + 1))) `2 ) } by A43;

            1 <= ( len G) by GOBOARD7: 32;

            then ( h_strip (G,j)) = { |[r1, s1]| : ((G * (1,j)) `2 ) <= s1 & s1 <= ((G * (1,(j + 1))) `2 ) } by A41, A42, GOBOARD5: 5;

            then p in ( h_strip (( GoB f),j)) by A44, EUCLID: 53;

            hence ex i0 be Nat st i0 <= j2 & x in ( h_strip (( GoB f),i0)) by A42;

          end;

        end;

        then

        consider i0 be Nat such that

         A45: i0 <= j2 and

         A46: x in ( h_strip (( GoB f),i0));

        reconsider X0 = ( cell (( GoB f),j0,i0)) as set;

        x in (( v_strip (( GoB f),j0)) /\ ( h_strip (( GoB f),i0))) by A23, A46, XBOOLE_0:def 4;

        then

         A47: x in X0 by GOBOARD5:def 3;

        X0 in { ( cell (( GoB f),i,j)) : i <= j1 & j <= j2 } by A22, A45;

        hence thesis by A47, TARSKI:def 4;

      end;

      let x be object;

      assume x in ( union { ( cell (( GoB f),i,j)) : i <= j1 & j <= j2 });

      then

      consider X0 be set such that

       A48: x in X0 & X0 in { ( cell (( GoB f),i,j)) : i <= j1 & j <= j2 } by TARSKI:def 4;

      ex i, j st X0 = ( cell (( GoB f),i,j)) & i <= j1 & j <= j2 by A48;

      hence thesis by A48;

    end;

    

     Lm3: for s1 holds { |[tb, sb]| where tb,sb be Real : sb >= s1 } is Subset of ( TOP-REAL 2)

    proof

      let s1;

      { |[tb, sb]| where tb,sb be Real : sb >= s1 } c= ( REAL 2)

      proof

        let y be object;

        assume y in { |[tb, sb]| where tb,sb be Real : sb >= s1 };

        then ex t7,s7 be Real st |[t7, s7]| = y & s7 >= s1;

        hence thesis by Lm2;

      end;

      hence thesis by EUCLID: 22;

    end;

    

     Lm4: for s1 holds { |[tb, sb]| where tb,sb be Real : sb > s1 } is Subset of ( TOP-REAL 2)

    proof

      let s1;

      { |[tb, sb]| where tb,sb be Real : sb > s1 } c= ( REAL 2)

      proof

        let y be object;

        assume y in { |[tb, sb]| where tb,sb be Real : sb > s1 };

        then ex t7,s7 be Real st |[t7, s7]| = y & s7 > s1;

        hence thesis by Lm2;

      end;

      hence thesis by EUCLID: 22;

    end;

    

     Lm5: for s1 holds { |[tb, sb]| where tb,sb be Real : sb <= s1 } is Subset of ( TOP-REAL 2)

    proof

      let s1;

      { |[tb, sb]| where tb,sb be Real : sb <= s1 } c= ( REAL 2)

      proof

        let y be object;

        assume y in { |[tb, sb]| where tb,sb be Real : sb <= s1 };

        then ex t7,s7 be Real st |[t7, s7]| = y & s7 <= s1;

        hence thesis by Lm2;

      end;

      hence thesis by EUCLID: 22;

    end;

    

     Lm6: for s1 holds { |[tb, sb]| where tb,sb be Real : sb < s1 } is Subset of ( TOP-REAL 2)

    proof

      let s1;

      { |[tb, sb]| where tb,sb be Real : sb < s1 } c= ( REAL 2)

      proof

        let y be object;

        assume y in { |[tb, sb]| where tb,sb be Real : sb < s1 };

        then ex t7,s7 be Real st |[t7, s7]| = y & s7 < s1;

        hence thesis by Lm2;

      end;

      hence thesis by EUCLID: 22;

    end;

    

     Lm7: for s1 holds { |[sb, tb]| where sb,tb be Real : sb <= s1 } is Subset of ( TOP-REAL 2)

    proof

      let s1;

      { |[sb, tb]| where sb,tb be Real : sb <= s1 } c= ( REAL 2)

      proof

        let y be object;

        assume y in { |[sb, tb]| where sb,tb be Real : sb <= s1 };

        then ex s7,t7 be Real st |[s7, t7]| = y & s7 <= s1;

        hence thesis by Lm2;

      end;

      hence thesis by EUCLID: 22;

    end;

    

     Lm8: for s1 holds { |[sb, tb]| : sb < s1 } is Subset of ( TOP-REAL 2)

    proof

      let s1;

      { |[sb, tb]| : sb < s1 } c= ( REAL 2)

      proof

        let y be object;

        assume y in { |[sb, tb]| : sb < s1 };

        then ex s7,t7 be Real st |[s7, t7]| = y & s7 < s1;

        hence thesis by Lm2;

      end;

      hence thesis by EUCLID: 22;

    end;

    

     Lm9: for s1 holds { |[sb, tb]| : sb >= s1 } is Subset of ( TOP-REAL 2)

    proof

      let s1;

      { |[sb, tb]| : sb >= s1 } c= ( REAL 2)

      proof

        let y be object;

        assume y in { |[sb, tb]| : sb >= s1 };

        then ex s7,t7 be Real st |[s7, t7]| = y & s7 >= s1;

        hence thesis by Lm2;

      end;

      hence thesis by EUCLID: 22;

    end;

    

     Lm10: for s1 holds { |[sb, tb]| where sb,tb be Real : sb > s1 } is Subset of ( TOP-REAL 2)

    proof

      let s1;

      { |[sb, tb]| where sb,tb be Real : sb > s1 } c= ( REAL 2)

      proof

        let y be object;

        assume y in { |[sb, tb]| where sb,tb be Real : sb > s1 };

        then ex s7,t7 be Real st |[s7, t7]| = y & s7 > s1;

        hence thesis by Lm2;

      end;

      hence thesis by EUCLID: 22;

    end;

    theorem :: GOBRD11:8

    

     Th8: for P1,P2 be Subset of ( TOP-REAL 2) st P1 = { |[r, s]| : s <= s1 } & P2 = { |[r2, s2]| : s2 > s1 } holds P1 = (P2 ` )

    proof

      let P1,P2 be Subset of ( TOP-REAL 2);

      assume

       A1: P1 = { |[r, s]| : s <= s1 } & P2 = { |[r2, s2]| : s2 > s1 };

      

       A2: (P2 ` ) c= P1

      proof

        let x be object;

        assume

         A3: x in (P2 ` );

        then

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

        

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

        x in (the carrier of ( TOP-REAL 2) \ P2) by A3, SUBSET_1:def 4;

        then not x in P2 by XBOOLE_0:def 5;

        then (p `2 ) <= s1 by A1, A4;

        hence thesis by A1, A4;

      end;

      P1 c= (P2 ` )

      proof

        let x be object;

        assume

         A5: x in P1;

        then ex r, s st |[r, s]| = x & s <= s1 by A1;

        then for r2, s2 holds not ( |[r2, s2]| = x & s2 > s1) by SPPOL_2: 1;

        then not x in P2 by A1;

        then x in (the carrier of ( TOP-REAL 2) \ P2) by A5, XBOOLE_0:def 5;

        hence thesis by SUBSET_1:def 4;

      end;

      hence thesis by A2;

    end;

    theorem :: GOBRD11:9

    

     Th9: for P1,P2 be Subset of ( TOP-REAL 2) st P1 = { |[r, s]| : s >= s1 } & P2 = { |[r2, s2]| : s2 < s1 } holds P1 = (P2 ` )

    proof

      let P1,P2 be Subset of ( TOP-REAL 2);

      assume

       A1: P1 = { |[r, s]| : s >= s1 } & P2 = { |[r2, s2]| : s2 < s1 };

      

       A2: (P2 ` ) c= P1

      proof

        let x be object;

        assume

         A3: x in (P2 ` );

        then

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

        

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

        x in (the carrier of ( TOP-REAL 2) \ P2) by A3, SUBSET_1:def 4;

        then not x in P2 by XBOOLE_0:def 5;

        then (p `2 ) >= s1 by A1, A4;

        hence thesis by A1, A4;

      end;

      P1 c= (P2 ` )

      proof

        let x be object;

        assume

         A5: x in P1;

        then ex r, s st |[r, s]| = x & s >= s1 by A1;

        then not ex r2, s2 st |[r2, s2]| = x & s2 < s1 by SPPOL_2: 1;

        then not x in P2 by A1;

        then x in (the carrier of ( TOP-REAL 2) \ P2) by A5, XBOOLE_0:def 5;

        hence thesis by SUBSET_1:def 4;

      end;

      hence thesis by A2;

    end;

    theorem :: GOBRD11:10

    

     Th10: for P1,P2 be Subset of ( TOP-REAL 2) st P1 = { |[s, r]| where s,r be Real : s >= s1 } & P2 = { |[s2, r2]| where s2,r2 be Real : s2 < s1 } holds P1 = (P2 ` )

    proof

      let P1,P2 be Subset of ( TOP-REAL 2);

      assume

       A1: P1 = { |[s, r]| where s,r be Real : s >= s1 } & P2 = { |[s2, r2]| where s2,r2 be Real : s2 < s1 };

      

       A2: (P2 ` ) c= P1

      proof

        let x be object;

        assume

         A3: x in (P2 ` );

        then

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

        

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

        x in (the carrier of ( TOP-REAL 2) \ P2) by A3, SUBSET_1:def 4;

        then not x in P2 by XBOOLE_0:def 5;

        then (p `1 ) >= s1 by A1, A4;

        hence thesis by A1, A4;

      end;

      P1 c= (P2 ` )

      proof

        let x be object;

        assume

         A5: x in P1;

        then ex s, r st |[s, r]| = x & s >= s1 by A1;

        then not ex s2, r2 st |[s2, r2]| = x & s2 < s1 by SPPOL_2: 1;

        then not x in P2 by A1;

        then x in (the carrier of ( TOP-REAL 2) \ P2) by A5, XBOOLE_0:def 5;

        hence thesis by SUBSET_1:def 4;

      end;

      hence thesis by A2;

    end;

    theorem :: GOBRD11:11

    

     Th11: for P1,P2 be Subset of ( TOP-REAL 2) st P1 = { |[s, r]| where s,r be Real : s <= s1 } & P2 = { |[s2, r2]| where s2,r2 be Real : s2 > s1 } holds P1 = (P2 ` )

    proof

      let P1,P2 be Subset of ( TOP-REAL 2);

      assume

       A1: P1 = { |[s, r]| where s,r be Real : s <= s1 } & P2 = { |[s2, r2]| where s2,r2 be Real : s2 > s1 };

      

       A2: (P2 ` ) c= P1

      proof

        let x be object;

        assume

         A3: x in (P2 ` );

        then

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

        

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

        x in (the carrier of ( TOP-REAL 2) \ P2) by A3, SUBSET_1:def 4;

        then not x in P2 by XBOOLE_0:def 5;

        then (p `1 ) <= s1 by A1, A4;

        hence thesis by A1, A4;

      end;

      P1 c= (P2 ` )

      proof

        let x be object;

        assume

         A5: x in P1;

        then ex s, r st |[s, r]| = x & s <= s1 by A1;

        then not ex s2, r2 st |[s2, r2]| = x & s2 > s1 by SPPOL_2: 1;

        then not x in { |[s2, r2]| where s2,r2 be Real : s2 > s1 };

        then x in (the carrier of ( TOP-REAL 2) \ P2) by A1, A5, XBOOLE_0:def 5;

        hence thesis by SUBSET_1:def 4;

      end;

      hence thesis by A2;

    end;

    theorem :: GOBRD11:12

    

     Th12: for P be Subset of ( TOP-REAL 2), s1 st P = { |[r, s]| : s <= s1 } holds P is closed

    proof

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

      reconsider P1 = { |[r, s]| where r,s be Real : s > s1 } as Subset of ( TOP-REAL 2) by Lm4;

      assume P = { |[r, s]| : s <= s1 };

      then

       A1: P = (P1 ` ) by Th8;

      P1 is open by JORDAN1: 22;

      hence thesis by A1, TOPS_1: 4;

    end;

    theorem :: GOBRD11:13

    

     Th13: for P be Subset of ( TOP-REAL 2), s1 st P = { |[r, s]| : s1 <= s } holds P is closed

    proof

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

      reconsider P1 = { |[r, s]| : s1 > s } as Subset of ( TOP-REAL 2) by Lm6;

      assume P = { |[r, s]| : s1 <= s };

      then

       A1: P = (P1 ` ) by Th9;

      P1 is open by JORDAN1: 23;

      hence thesis by A1, TOPS_1: 4;

    end;

    theorem :: GOBRD11:14

    

     Th14: for P be Subset of ( TOP-REAL 2), s1 st P = { |[s, r]| where s,r be Real : s <= s1 } holds P is closed

    proof

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

      reconsider P1 = { |[s, r]| where s,r be Real : s > s1 } as Subset of ( TOP-REAL 2) by Lm10;

      assume P = { |[s, r]| where s,r be Real : s <= s1 };

      then

       A1: P = (P1 ` ) by Th11;

      P1 is open by JORDAN1: 20;

      hence thesis by A1, TOPS_1: 4;

    end;

    theorem :: GOBRD11:15

    

     Th15: for P be Subset of ( TOP-REAL 2), s1 st P = { |[s, r]| where s,r be Real : s1 <= s } holds P is closed

    proof

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

      reconsider P1 = { |[s, r]| where s,r be Real : s < s1 } as Subset of ( TOP-REAL 2) by Lm8;

      assume P = { |[s, r]| where s,r be Real : s >= s1 };

      then

       A1: P = (P1 ` ) by Th10;

      P1 is open by JORDAN1: 21;

      hence thesis by A1, TOPS_1: 4;

    end;

    theorem :: GOBRD11:16

    

     Th16: for G be Matrix of ( TOP-REAL 2) holds ( h_strip (G,j)) is closed

    proof

      let G be Matrix of ( TOP-REAL 2);

      now

        per cases ;

          case

           A1: j < 1;

           A2:

          now

            assume j >= ( width G);

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

            hence thesis by Th13;

          end;

          now

            assume j < ( width G);

            then ( h_strip (G,j)) = { |[r, s]| : s <= ((G * (1,(j + 1))) `2 ) } by A1, GOBOARD5:def 2;

            hence thesis by Th12;

          end;

          hence thesis by A2;

        end;

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

          then

           A3: ( h_strip (G,j)) = { |[r, s]| : ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) } by GOBOARD5:def 2;

          reconsider P2 = { |[r1, s1]| : s1 <= ((G * (1,(j + 1))) `2 ) } as Subset of ( TOP-REAL 2) by Lm5;

          reconsider P1 = { |[r1, s1]| : ((G * (1,j)) `2 ) <= s1 } as Subset of ( TOP-REAL 2) by Lm3;

          

           A4: { |[r, s]| : ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) } = ({ |[r1, s1]| : ((G * (1,j)) `2 ) <= s1 } /\ { |[r2, s2]| : s2 <= ((G * (1,(j + 1))) `2 ) })

          proof

            

             A5: ({ |[r1, s1]| : ((G * (1,j)) `2 ) <= s1 } /\ { |[r2, s2]| : s2 <= ((G * (1,(j + 1))) `2 ) }) c= { |[r, s]| : ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) }

            proof

              let x be object;

              assume

               A6: x in ({ |[r1, s1]| : ((G * (1,j)) `2 ) <= s1 } /\ { |[r2, s2]| : s2 <= ((G * (1,(j + 1))) `2 ) });

              then

               A7: x in { |[r1, s1]| : ((G * (1,j)) `2 ) <= s1 } by XBOOLE_0:def 4;

              x in { |[r2, s2]| : s2 <= ((G * (1,(j + 1))) `2 ) } by A6, XBOOLE_0:def 4;

              then

              consider r2, s2 such that

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

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

              consider r1, s1 such that

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

               A11: ((G * (1,j)) `2 ) <= s1 by A7;

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

              hence thesis by A10, A11, A9;

            end;

            

             A12: { |[r, s]| : ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) } c= { |[r1, s1]| : ((G * (1,j)) `2 ) <= s1 }

            proof

              let x be object;

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

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

              hence thesis;

            end;

            { |[r, s]| : ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) } c= { |[r1, s1]| : s1 <= ((G * (1,(j + 1))) `2 ) }

            proof

              let x be object;

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

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

              hence thesis;

            end;

            then { |[r, s]| : ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) } c= ({ |[r1, s1]| : ((G * (1,j)) `2 ) <= s1 } /\ { |[r2, s2]| : s2 <= ((G * (1,(j + 1))) `2 ) }) by A12, XBOOLE_1: 19;

            hence thesis by A5;

          end;

          P1 is closed & P2 is closed by Th12, Th13;

          hence thesis by A3, A4, TOPS_1: 8;

        end;

          case j >= ( width G);

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

          hence thesis by Th13;

        end;

      end;

      hence thesis;

    end;

    theorem :: GOBRD11:17

    

     Th17: for G be Matrix of ( TOP-REAL 2) holds ( v_strip (G,j)) is closed

    proof

      let G be Matrix of ( TOP-REAL 2);

      now

        per cases ;

          case

           A1: j < 1;

           A2:

          now

            assume j >= ( len G);

            then ( v_strip (G,j)) = { |[s, r]| where s,r be Real : ((G * (j,1)) `1 ) <= s } by GOBOARD5:def 1;

            hence thesis by Th15;

          end;

          now

            assume j < ( len G);

            then ( v_strip (G,j)) = { |[s, r]| where s,r be Real : s <= ((G * ((j + 1),1)) `1 ) } by A1, GOBOARD5:def 1;

            hence thesis by Th14;

          end;

          hence thesis by A2;

        end;

          case 1 <= j & j < ( len G);

          then

           A3: ( v_strip (G,j)) = { |[s, r]| where s,r be Real : ((G * (j,1)) `1 ) <= s & s <= ((G * ((j + 1),1)) `1 ) } by GOBOARD5:def 1;

          reconsider P2 = { |[s1, r1]| where s1,r1 be Real : s1 <= ((G * ((j + 1),1)) `1 ) } as Subset of ( TOP-REAL 2) by Lm7;

          reconsider P1 = { |[s1, r1]| where s1,r1 be Real : ((G * (j,1)) `1 ) <= s1 } as Subset of ( TOP-REAL 2) by Lm9;

          

           A4: { |[s, r]| where s,r be Real : ((G * (j,1)) `1 ) <= s & s <= ((G * ((j + 1),1)) `1 ) } = ({ |[s1, r1]| where s1,r1 be Real : ((G * (j,1)) `1 ) <= s1 } /\ { |[s2, r2]| where s2,r2 be Real : s2 <= ((G * ((j + 1),1)) `1 ) })

          proof

            

             A5: ({ |[s1, r1]| where s1,r1 be Real : ((G * (j,1)) `1 ) <= s1 } /\ { |[s2, r2]| where s2,r2 be Real : s2 <= ((G * ((j + 1),1)) `1 ) }) c= { |[s, r]| where s,r be Real : ((G * (j,1)) `1 ) <= s & s <= ((G * ((j + 1),1)) `1 ) }

            proof

              let x be object;

              assume

               A6: x in ({ |[s1, r1]| where s1,r1 be Real : ((G * (j,1)) `1 ) <= s1 } /\ { |[s2, r2]| where s2,r2 be Real : s2 <= ((G * ((j + 1),1)) `1 ) });

              then

               A7: x in { |[s2, r2]| where s2,r2 be Real : s2 <= ((G * ((j + 1),1)) `1 ) } by XBOOLE_0:def 4;

              x in { |[s1, r1]| where s1,r1 be Real : ((G * (j,1)) `1 ) <= s1 } by A6, XBOOLE_0:def 4;

              then ex s1, r1 st |[s1, r1]| = x & ((G * (j,1)) `1 ) <= s1;

              then

              consider r1, s1 such that

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

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

              consider s2, r2 such that

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

               A11: s2 <= ((G * ((j + 1),1)) `1 ) by A7;

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

              hence thesis by A8, A9, A11;

            end;

            

             A12: { |[s, r]| where s,r be Real : ((G * (j,1)) `1 ) <= s & s <= ((G * ((j + 1),1)) `1 ) } c= { |[s1, r1]| where s1,r1 be Real : ((G * (j,1)) `1 ) <= s1 }

            proof

              let x be object;

              assume x in { |[s, r]| where s,r be Real : ((G * (j,1)) `1 ) <= s & s <= ((G * ((j + 1),1)) `1 ) };

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

              hence thesis;

            end;

            { |[s, r]| where s,r be Real : ((G * (j,1)) `1 ) <= s & s <= ((G * ((j + 1),1)) `1 ) } c= { |[s1, r1]| where s1,r1 be Real : s1 <= ((G * ((j + 1),1)) `1 ) }

            proof

              let x be object;

              assume x in { |[s, r]| where s,r be Real : ((G * (j,1)) `1 ) <= s & s <= ((G * ((j + 1),1)) `1 ) };

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

              hence thesis;

            end;

            then { |[s, r]| where s,r be Real : ((G * (j,1)) `1 ) <= s & s <= ((G * ((j + 1),1)) `1 ) } c= ({ |[s1, r1]| where s1,r1 be Real : ((G * (j,1)) `1 ) <= s1 } /\ { |[s2, r2]| where s2,r2 be Real : s2 <= ((G * ((j + 1),1)) `1 ) }) by A12, XBOOLE_1: 19;

            hence thesis by A5;

          end;

          P1 is closed & P2 is closed by Th14, Th15;

          hence thesis by A3, A4, TOPS_1: 8;

        end;

          case j >= ( len G);

          then ( v_strip (G,j)) = { |[s, r]| where s,r be Real : ((G * (j,1)) `1 ) <= s } by GOBOARD5:def 1;

          hence thesis by Th15;

        end;

      end;

      hence thesis;

    end;

    theorem :: GOBRD11:18

    

     Th18: G is X_equal-in-line implies ( v_strip (G, 0 )) = { |[r, s]| : r <= ((G * (1,1)) `1 ) }

    proof

       0 <> ( width G) by MATRIX_0:def 10;

      then

       A1: 1 <= ( width G) by NAT_1: 14;

      assume G is X_equal-in-line;

      hence thesis by A1, GOBOARD5: 10;

    end;

    theorem :: GOBRD11:19

    

     Th19: G is X_equal-in-line implies ( v_strip (G,( len G))) = { |[r, s]| : ((G * (( len G),1)) `1 ) <= r }

    proof

       0 <> ( width G) by MATRIX_0:def 10;

      then

       A1: 1 <= ( width G) by NAT_1: 14;

      assume G is X_equal-in-line;

      hence thesis by A1, GOBOARD5: 9;

    end;

    theorem :: GOBRD11:20

    

     Th20: G is X_equal-in-line & 1 <= i & i < ( len G) implies ( v_strip (G,i)) = { |[r, s]| : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) }

    proof

      assume

       A1: G is X_equal-in-line;

       0 <> ( width G) by MATRIX_0:def 10;

      then

       A2: 1 <= ( width G) by NAT_1: 14;

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

      hence thesis by A1, A2, GOBOARD5: 8;

    end;

    theorem :: GOBRD11:21

    

     Th21: G is Y_equal-in-column implies ( h_strip (G, 0 )) = { |[r, s]| : s <= ((G * (1,1)) `2 ) }

    proof

       0 <> ( len G) by MATRIX_0:def 10;

      then

       A1: 1 <= ( len G) by NAT_1: 14;

      assume G is Y_equal-in-column;

      hence thesis by A1, GOBOARD5: 7;

    end;

    theorem :: GOBRD11:22

    

     Th22: G is Y_equal-in-column implies ( h_strip (G,( width G))) = { |[r, s]| : ((G * (1,( width G))) `2 ) <= s }

    proof

       0 <> ( len G) by MATRIX_0:def 10;

      then

       A1: 1 <= ( len G) by NAT_1: 14;

      assume G is Y_equal-in-column;

      hence thesis by A1, GOBOARD5: 6;

    end;

    theorem :: GOBRD11:23

    

     Th23: G is Y_equal-in-column & 1 <= j & j < ( width G) implies ( h_strip (G,j)) = { |[r, s]| : ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) }

    proof

      assume

       A1: G is Y_equal-in-column;

       0 <> ( len G) by MATRIX_0:def 10;

      then

       A2: 1 <= ( len G) by NAT_1: 14;

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

      hence thesis by A1, A2, GOBOARD5: 5;

    end;

    reserve G for non empty-yielding X_equal-in-line Y_equal-in-column Matrix of ( TOP-REAL 2);

    theorem :: GOBRD11:24

    

     Th24: ( cell (G, 0 , 0 )) = { |[r, s]| : r <= ((G * (1,1)) `1 ) & s <= ((G * (1,1)) `2 ) }

    proof

      

       A1: ( cell (G, 0 , 0 )) = (( v_strip (G, 0 )) /\ ( h_strip (G, 0 ))) by GOBOARD5:def 3;

      

       A2: ( h_strip (G, 0 )) = { |[r, s]| : s <= ((G * (1,1)) `2 ) } by Th21;

      

       A3: ( v_strip (G, 0 )) = { |[r, s]| : r <= ((G * (1,1)) `1 ) } by Th18;

      thus ( cell (G, 0 , 0 )) c= { |[r, s]| : r <= ((G * (1,1)) `1 ) & s <= ((G * (1,1)) `2 ) }

      proof

        let x be object;

        assume

         A4: x in ( cell (G, 0 , 0 ));

        then x in ( v_strip (G, 0 )) by A1, XBOOLE_0:def 4;

        then

        consider r1, s1 such that

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

         A6: r1 <= ((G * (1,1)) `1 ) by A3;

        x in ( h_strip (G, 0 )) by A1, A4, XBOOLE_0:def 4;

        then

        consider r2, s2 such that

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

         A8: s2 <= ((G * (1,1)) `2 ) by A2;

        s1 = s2 by A5, A7, SPPOL_2: 1;

        hence thesis by A5, A6, A8;

      end;

      let x be object;

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

      then

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

      then

       A10: x in ( h_strip (G, 0 )) by A2;

      x in ( v_strip (G, 0 )) by A3, A9;

      hence thesis by A1, A10, XBOOLE_0:def 4;

    end;

    theorem :: GOBRD11:25

    

     Th25: ( cell (G, 0 ,( width G))) = { |[r, s]| : r <= ((G * (1,1)) `1 ) & ((G * (1,( width G))) `2 ) <= s }

    proof

      

       A1: ( cell (G, 0 ,( width G))) = (( v_strip (G, 0 )) /\ ( h_strip (G,( width G)))) by GOBOARD5:def 3;

      

       A2: ( h_strip (G,( width G))) = { |[r, s]| : ((G * (1,( width G))) `2 ) <= s } by Th22;

      

       A3: ( v_strip (G, 0 )) = { |[r, s]| : r <= ((G * (1,1)) `1 ) } by Th18;

      thus ( cell (G, 0 ,( width G))) c= { |[r, s]| : r <= ((G * (1,1)) `1 ) & ((G * (1,( width G))) `2 ) <= s }

      proof

        let x be object;

        assume

         A4: x in ( cell (G, 0 ,( width G)));

        then x in ( v_strip (G, 0 )) by A1, XBOOLE_0:def 4;

        then

        consider r1, s1 such that

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

         A6: r1 <= ((G * (1,1)) `1 ) by A3;

        x in ( h_strip (G,( width G))) by A1, A4, XBOOLE_0:def 4;

        then

        consider r2, s2 such that

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

         A8: ((G * (1,( width G))) `2 ) <= s2 by A2;

        s1 = s2 by A5, A7, SPPOL_2: 1;

        hence thesis by A5, A6, A8;

      end;

      let x be object;

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

      then

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

      then

       A10: x in ( h_strip (G,( width G))) by A2;

      x in ( v_strip (G, 0 )) by A3, A9;

      hence thesis by A1, A10, XBOOLE_0:def 4;

    end;

    theorem :: GOBRD11:26

    

     Th26: 1 <= j & j < ( width G) implies ( cell (G, 0 ,j)) = { |[r, s]| : r <= ((G * (1,1)) `1 ) & ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) }

    proof

      

       A1: ( cell (G, 0 ,j)) = (( v_strip (G, 0 )) /\ ( h_strip (G,j))) by GOBOARD5:def 3;

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

      then

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

      

       A3: ( v_strip (G, 0 )) = { |[r, s]| : r <= ((G * (1,1)) `1 ) } by Th18;

      thus ( cell (G, 0 ,j)) c= { |[r, s]| : r <= ((G * (1,1)) `1 ) & ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) }

      proof

        let x be object;

        assume

         A4: x in ( cell (G, 0 ,j));

        then x in ( v_strip (G, 0 )) by A1, XBOOLE_0:def 4;

        then

        consider r1, s1 such that

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

         A6: r1 <= ((G * (1,1)) `1 ) by A3;

        x in ( h_strip (G,j)) by A1, A4, XBOOLE_0:def 4;

        then

        consider r2, s2 such that

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

         A8: ((G * (1,j)) `2 ) <= s2 & s2 <= ((G * (1,(j + 1))) `2 ) by A2;

        s1 = s2 by A5, A7, SPPOL_2: 1;

        hence thesis by A5, A6, A8;

      end;

      let x be object;

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

      then

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

      then

       A10: x in ( h_strip (G,j)) by A2;

      x in ( v_strip (G, 0 )) by A3, A9;

      hence thesis by A1, A10, XBOOLE_0:def 4;

    end;

    theorem :: GOBRD11:27

    

     Th27: ( cell (G,( len G), 0 )) = { |[r, s]| : ((G * (( len G),1)) `1 ) <= r & s <= ((G * (1,1)) `2 ) }

    proof

      

       A1: ( cell (G,( len G), 0 )) = (( v_strip (G,( len G))) /\ ( h_strip (G, 0 ))) by GOBOARD5:def 3;

      

       A2: ( h_strip (G, 0 )) = { |[r, s]| : s <= ((G * (1,1)) `2 ) } by Th21;

      

       A3: ( v_strip (G,( len G))) = { |[r, s]| : ((G * (( len G),1)) `1 ) <= r } by Th19;

      thus ( cell (G,( len G), 0 )) c= { |[r, s]| : ((G * (( len G),1)) `1 ) <= r & s <= ((G * (1,1)) `2 ) }

      proof

        let x be object;

        assume

         A4: x in ( cell (G,( len G), 0 ));

        then x in ( v_strip (G,( len G))) by A1, XBOOLE_0:def 4;

        then

        consider r1, s1 such that

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

         A6: ((G * (( len G),1)) `1 ) <= r1 by A3;

        x in ( h_strip (G, 0 )) by A1, A4, XBOOLE_0:def 4;

        then

        consider r2, s2 such that

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

         A8: s2 <= ((G * (1,1)) `2 ) by A2;

        s1 = s2 by A5, A7, SPPOL_2: 1;

        hence thesis by A5, A6, A8;

      end;

      let x be object;

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

      then

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

      then

       A10: x in ( h_strip (G, 0 )) by A2;

      x in ( v_strip (G,( len G))) by A3, A9;

      hence thesis by A1, A10, XBOOLE_0:def 4;

    end;

    theorem :: GOBRD11:28

    

     Th28: ( cell (G,( len G),( width G))) = { |[r, s]| : ((G * (( len G),1)) `1 ) <= r & ((G * (1,( width G))) `2 ) <= s }

    proof

      

       A1: ( cell (G,( len G),( width G))) = (( v_strip (G,( len G))) /\ ( h_strip (G,( width G)))) by GOBOARD5:def 3;

      

       A2: ( h_strip (G,( width G))) = { |[r, s]| : ((G * (1,( width G))) `2 ) <= s } by Th22;

      

       A3: ( v_strip (G,( len G))) = { |[r, s]| : ((G * (( len G),1)) `1 ) <= r } by Th19;

      thus ( cell (G,( len G),( width G))) c= { |[r, s]| : ((G * (( len G),1)) `1 ) <= r & ((G * (1,( width G))) `2 ) <= s }

      proof

        let x be object;

        assume

         A4: x in ( cell (G,( len G),( width G)));

        then x in ( v_strip (G,( len G))) by A1, XBOOLE_0:def 4;

        then

        consider r1, s1 such that

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

         A6: ((G * (( len G),1)) `1 ) <= r1 by A3;

        x in ( h_strip (G,( width G))) by A1, A4, XBOOLE_0:def 4;

        then

        consider r2, s2 such that

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

         A8: ((G * (1,( width G))) `2 ) <= s2 by A2;

        s1 = s2 by A5, A7, SPPOL_2: 1;

        hence thesis by A5, A6, A8;

      end;

      let x be object;

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

      then

       A9: ex r, s st x = |[r, s]| & ((G * (( len G),1)) `1 ) <= r & ((G * (1,( width G))) `2 ) <= s;

      then

       A10: x in ( h_strip (G,( width G))) by A2;

      x in ( v_strip (G,( len G))) by A3, A9;

      hence thesis by A1, A10, XBOOLE_0:def 4;

    end;

    theorem :: GOBRD11:29

    

     Th29: 1 <= j & j < ( width G) implies ( cell (G,( len G),j)) = { |[r, s]| : ((G * (( len G),1)) `1 ) <= r & ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) }

    proof

      

       A1: ( cell (G,( len G),j)) = (( v_strip (G,( len G))) /\ ( h_strip (G,j))) by GOBOARD5:def 3;

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

      then

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

      

       A3: ( v_strip (G,( len G))) = { |[r, s]| : ((G * (( len G),1)) `1 ) <= r } by Th19;

      thus ( cell (G,( len G),j)) c= { |[r, s]| : ((G * (( len G),1)) `1 ) <= r & ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) }

      proof

        let x be object;

        assume

         A4: x in ( cell (G,( len G),j));

        then x in ( v_strip (G,( len G))) by A1, XBOOLE_0:def 4;

        then

        consider r1, s1 such that

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

         A6: ((G * (( len G),1)) `1 ) <= r1 by A3;

        x in ( h_strip (G,j)) by A1, A4, XBOOLE_0:def 4;

        then

        consider r2, s2 such that

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

         A8: ((G * (1,j)) `2 ) <= s2 & s2 <= ((G * (1,(j + 1))) `2 ) by A2;

        s1 = s2 by A5, A7, SPPOL_2: 1;

        hence thesis by A5, A6, A8;

      end;

      let x be object;

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

      then

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

      then

       A10: x in ( h_strip (G,j)) by A2;

      x in ( v_strip (G,( len G))) by A3, A9;

      hence thesis by A1, A10, XBOOLE_0:def 4;

    end;

    theorem :: GOBRD11:30

    

     Th30: 1 <= i & i < ( len G) implies ( cell (G,i, 0 )) = { |[r, s]| : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) & s <= ((G * (1,1)) `2 ) }

    proof

      

       A1: ( cell (G,i, 0 )) = (( v_strip (G,i)) /\ ( h_strip (G, 0 ))) by GOBOARD5:def 3;

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

      then

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

      

       A3: ( h_strip (G, 0 )) = { |[r, s]| : s <= ((G * (1,1)) `2 ) } by Th21;

      thus ( cell (G,i, 0 )) c= { |[r, s]| : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) & s <= ((G * (1,1)) `2 ) }

      proof

        let x be object;

        assume

         A4: x in ( cell (G,i, 0 ));

        then x in ( v_strip (G,i)) by A1, XBOOLE_0:def 4;

        then

        consider r1, s1 such that

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

         A6: ((G * (i,1)) `1 ) <= r1 & r1 <= ((G * ((i + 1),1)) `1 ) by A2;

        x in ( h_strip (G, 0 )) by A1, A4, XBOOLE_0:def 4;

        then

        consider r2, s2 such that

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

         A8: s2 <= ((G * (1,1)) `2 ) by A3;

        s1 = s2 by A5, A7, SPPOL_2: 1;

        hence thesis by A5, A6, A8;

      end;

      let x be object;

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

      then

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

      then

       A10: x in ( h_strip (G, 0 )) by A3;

      x in ( v_strip (G,i)) by A2, A9;

      hence thesis by A1, A10, XBOOLE_0:def 4;

    end;

    theorem :: GOBRD11:31

    

     Th31: 1 <= i & i < ( len G) implies ( cell (G,i,( width G))) = { |[r, s]| : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) & ((G * (1,( width G))) `2 ) <= s }

    proof

      

       A1: ( cell (G,i,( width G))) = (( v_strip (G,i)) /\ ( h_strip (G,( width G)))) by GOBOARD5:def 3;

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

      then

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

      

       A3: ( h_strip (G,( width G))) = { |[r, s]| : ((G * (1,( width G))) `2 ) <= s } by Th22;

      thus ( cell (G,i,( width G))) c= { |[r, s]| : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) & ((G * (1,( width G))) `2 ) <= s }

      proof

        let x be object;

        assume

         A4: x in ( cell (G,i,( width G)));

        then x in ( v_strip (G,i)) by A1, XBOOLE_0:def 4;

        then

        consider r1, s1 such that

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

         A6: ((G * (i,1)) `1 ) <= r1 & r1 <= ((G * ((i + 1),1)) `1 ) by A2;

        x in ( h_strip (G,( width G))) by A1, A4, XBOOLE_0:def 4;

        then

        consider r2, s2 such that

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

         A8: ((G * (1,( width G))) `2 ) <= s2 by A3;

        s1 = s2 by A5, A7, SPPOL_2: 1;

        hence thesis by A5, A6, A8;

      end;

      let x be object;

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

      then

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

      then

       A10: x in ( h_strip (G,( width G))) by A3;

      x in ( v_strip (G,i)) by A2, A9;

      hence thesis by A1, A10, XBOOLE_0:def 4;

    end;

    theorem :: GOBRD11:32

    

     Th32: 1 <= i & i < ( len G) & 1 <= j & j < ( width G) implies ( cell (G,i,j)) = { |[r, s]| : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) }

    proof

      assume that

       A1: 1 <= i & i < ( len G) and

       A2: 1 <= j & j < ( width G);

      

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

      

       A4: ( cell (G,i,j)) = (( v_strip (G,i)) /\ ( h_strip (G,j))) by GOBOARD5:def 3;

      

       A5: ( v_strip (G,i)) = { |[r, s]| : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) } by A1, Th20;

      thus ( cell (G,i,j)) c= { |[r, s]| : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) }

      proof

        let x be object;

        assume

         A6: x in ( cell (G,i,j));

        then x in ( v_strip (G,i)) by A4, XBOOLE_0:def 4;

        then

        consider r1, s1 such that

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

         A8: ((G * (i,1)) `1 ) <= r1 & r1 <= ((G * ((i + 1),1)) `1 ) by A5;

        x in ( h_strip (G,j)) by A4, A6, XBOOLE_0:def 4;

        then

        consider r2, s2 such that

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

         A10: ((G * (1,j)) `2 ) <= s2 & s2 <= ((G * (1,(j + 1))) `2 ) by A3;

        s1 = s2 by A7, A9, SPPOL_2: 1;

        hence thesis by A7, A8, A10;

      end;

      let x be object;

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

      then

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

      then

       A12: x in ( h_strip (G,j)) by A3;

      x in ( v_strip (G,i)) by A5, A11;

      hence thesis by A4, A12, XBOOLE_0:def 4;

    end;

    theorem :: GOBRD11:33

    

     Th33: for G be Matrix of ( TOP-REAL 2) holds ( cell (G,i,j)) is closed

    proof

      let G be Matrix of ( TOP-REAL 2);

      

       A1: ( v_strip (G,i)) is closed by Th17;

      ( cell (G,i,j)) = (( h_strip (G,j)) /\ ( v_strip (G,i))) & ( h_strip (G,j)) is closed by Th16, GOBOARD5:def 3;

      hence thesis by A1, TOPS_1: 8;

    end;

    theorem :: GOBRD11:34

    

     Th34: for G be non empty-yielding Matrix of ( TOP-REAL 2) holds 1 <= ( len G) & 1 <= ( width G)

    proof

      let G be non empty-yielding Matrix of ( TOP-REAL 2);

      ( not ( len G) = 0 ) & not ( width G) = 0 by MATRIX_0:def 10;

      hence thesis by NAT_1: 14;

    end;

    theorem :: GOBRD11:35

    for G be Go-board holds i <= ( len G) & j <= ( width G) implies ( cell (G,i,j)) = ( Cl ( Int ( cell (G,i,j))))

    proof

      let G be Go-board;

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

      assume

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

      

       A2: ( cell (G,i,j)) c= ( Cl Y)

      proof

        let x be object;

        assume

         A3: x in ( cell (G,i,j));

        then

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

        for G0 be Subset of ( TOP-REAL 2) st G0 is open holds p in G0 implies Y meets G0

        proof

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

          assume

           A4: G0 is open;

          now

            reconsider u = p as Point of ( Euclid 2) by EUCLID: 22;

            assume

             A5: p in G0;

            

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

            reconsider v = u as Element of ( REAL 2);

            

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

            then

            reconsider G00 = G0 as Subset of ( TopSpaceMetr ( Euclid 2));

            G00 is open by A4, A7, PRE_TOPC: 30;

            then

            consider r be Real such that

             A8: r > 0 and

             A9: ( Ball (u,r)) c= G00 by A5, TOPMETR: 15;

            reconsider r as Real;

            

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

            now

              per cases by A1, A10, A6, XXREAL_0: 1;

                case

                 A11: i = 0 & j = 0 ;

                then p in { |[r2, s2]| : r2 <= ((G * (1,1)) `1 ) & s2 <= ((G * (1,1)) `2 ) } by A3, Th24;

                then

                consider r2, s2 such that

                 A12: p = |[r2, s2]| and

                 A13: r2 <= ((G * (1,1)) `1 ) and

                 A14: s2 <= ((G * (1,1)) `2 );

                set r3 = (r2 - (r / 2)), s3 = (s2 - (r / 2));

                

                 A15: (r * (2 " )) > 0 by A8, XREAL_1: 129;

                then s3 < (s3 + (r / 2)) by XREAL_1: 29;

                then

                 A16: s3 < ((G * (1,1)) `2 ) by A14, XXREAL_0: 2;

                reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                r3 < (r3 + (r / 2)) by A15, XREAL_1: 29;

                then r3 < ((G * (1,1)) `1 ) by A13, XXREAL_0: 2;

                then u0 in { |[r1, s1]| : r1 < ((G * (1,1)) `1 ) & s1 < ((G * (1,1)) `2 ) } by A16;

                then

                 A17: u0 in Y by A11, GOBOARD6: 18;

                reconsider v0 = u0 as Element of ( REAL 2);

                

                 A18: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                then

                 A19: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                .= (((r / 2) * ( sqrt 2)) ^2 );

                then

                 A20: ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                

                 A21: (r2 - r3) = (r / 2) & (s2 - s3) = (r / 2);

                (p `1 ) = r2 & (p `2 ) = s2 by A12, EUCLID: 52;

                then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & (( Pitag_dist 2) . (v,v0)) < r by A18, A21, A19, A20, METRIC_1:def 1, TOPREAL3: 7;

                then u0 in ( Ball (u,r)) by METRIC_1: 11;

                hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A17, XBOOLE_0:def 4;

              end;

                case

                 A22: i = 0 & j = ( width G);

                then p in { |[r2, s2]| : r2 <= ((G * (1,1)) `1 ) & ((G * (1,( width G))) `2 ) <= s2 } by A3, Th25;

                then

                consider r2, s2 such that

                 A23: p = |[r2, s2]| and

                 A24: r2 <= ((G * (1,1)) `1 ) and

                 A25: ((G * (1,( width G))) `2 ) <= s2;

                set r3 = (r2 - (r / 2)), s3 = (s2 + (r / 2));

                

                 A26: (r * (2 " )) > 0 by A8, XREAL_1: 129;

                then s3 > s2 by XREAL_1: 29;

                then

                 A27: s3 > ((G * (1,( width G))) `2 ) by A25, XXREAL_0: 2;

                reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                r3 < (r3 + (r / 2)) by A26, XREAL_1: 29;

                then r3 < ((G * (1,1)) `1 ) by A24, XXREAL_0: 2;

                then u0 in { |[r1, s1]| : r1 < ((G * (1,1)) `1 ) & ((G * (1,( width G))) `2 ) < s1 } by A27;

                then

                 A28: u0 in Y by A22, GOBOARD6: 19;

                reconsider v0 = u0 as Element of ( REAL 2);

                

                 A29: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                then

                 A30: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                .= (((r / 2) * ( sqrt 2)) ^2 );

                then

                 A31: ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A8, A30, Lm1, METRIC_1:def 1, SQUARE_1: 22;

                (p `1 ) = r2 & (p `2 ) = s2 by A23, EUCLID: 52;

                then ( dist (u,u0)) < r by A29, A31, TOPREAL3: 7;

                then u0 in ( Ball (u,r)) by METRIC_1: 11;

                hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A28, XBOOLE_0:def 4;

              end;

                case

                 A32: i = 0 & 1 <= j & j < ( width G);

                then p in { |[r2, s2]| : r2 <= ((G * (1,1)) `1 ) & ((G * (1,j)) `2 ) <= s2 & s2 <= ((G * (1,(j + 1))) `2 ) } by A3, Th26;

                then

                consider r2, s2 such that

                 A33: p = |[r2, s2]| and

                 A34: r2 <= ((G * (1,1)) `1 ) and

                 A35: ((G * (1,j)) `2 ) <= s2 and

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

                now

                  per cases by A35, A36, XXREAL_0: 1;

                    case

                     A37: s2 = ((G * (1,j)) `2 );

                    

                     A38: (p `1 ) = r2 & (p `2 ) = s2 by A33, EUCLID: 52;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A39: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then

                     A40: ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    set rl = (((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 ));

                    set rm = ( min (r,rl));

                    set r3 = (r2 - (r / 2)), s3 = (s2 + (rm / 2));

                    set q0 = |[r3, s3]|;

                    

                     A41: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A42: 1 <= ( len G) by Th34;

                    j < (j + 1) & (j + 1) <= ( width G) by A32, NAT_1: 13;

                    then ((G * (1,j)) `2 ) < ((G * (1,(j + 1))) `2 ) by A32, A42, GOBOARD5: 4;

                    then

                     A43: rl > 0 by XREAL_1: 50;

                    then

                     A44: rm > 0 by A8, XXREAL_0: 21;

                    then s3 > s2 by XREAL_1: 29, XREAL_1: 139;

                    then

                     A45: s3 > ((G * (1,j)) `2 ) by A35, XXREAL_0: 2;

                    (rm / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then ((rm / 2) ^2 ) <= ((r / 2) ^2 ) by A44, SQUARE_1: 15;

                    then

                     A46: (((r / 2) ^2 ) + ((rm / 2) ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 7;

                     0 <= ((rm / 2) ^2 ) & 0 <= ((r / 2) ^2 ) by XREAL_1: 63;

                    then ( sqrt (((r / 2) ^2 ) + ((rm / 2) ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A46, SQUARE_1: 26;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A39, A40, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by A38, A41, TOPREAL3: 7;

                    then

                     A47: u0 in ( Ball (u,r)) by METRIC_1: 11;

                    (rm / 2) <= (rl / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A48: (((G * (1,j)) `2 ) + (rm / 2)) <= (((G * (1,j)) `2 ) + (rl / 2)) by XREAL_1: 6;

                    (r * (2 " )) > 0 by A8, XREAL_1: 129;

                    then r3 < (r3 + (r / 2)) by XREAL_1: 29;

                    then

                     A49: r3 < ((G * (1,1)) `1 ) by A34, XXREAL_0: 2;

                    (((G * (1,j)) `2 ) + ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) < ((((G * (1,j)) `2 ) + ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) + ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) by A43, XREAL_1: 29, XREAL_1: 139;

                    then s3 < ((G * (1,(j + 1))) `2 ) by A37, A48, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : r1 < ((G * (1,1)) `1 ) & ((G * (1,j)) `2 ) < s1 & s1 < ((G * (1,(j + 1))) `2 ) } by A49, A45;

                    then u0 in Y by A32, GOBOARD6: 20;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A47, XBOOLE_0:def 4;

                  end;

                    case

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

                    set r3 = (r2 - (r / 2)), s3 = s2;

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    (r * (2 " )) > 0 by A8, XREAL_1: 129;

                    then r3 < (r3 + (r / 2)) by XREAL_1: 29;

                    then r3 < ((G * (1,1)) `1 ) by A34, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : r1 < ((G * (1,1)) `1 ) & ((G * (1,j)) `2 ) < s1 & s1 < ((G * (1,(j + 1))) `2 ) } by A50;

                    then

                     A51: u0 in Y by A32, GOBOARD6: 20;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A52: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A53: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    

                     A54: ((r / 2) ^2 ) >= 0 by XREAL_1: 63;

                    then (((r / 2) ^2 ) + 0 ) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 6;

                    then

                     A55: ( sqrt (((r / 2) ^2 ) + ( 0 ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A54, SQUARE_1: 26;

                    

                     A56: (p `1 ) = r2 & (p `2 ) = s2 by A33, EUCLID: 52;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A53, A55, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by A56, A52, TOPREAL3: 7;

                    then u0 in ( Ball (u,r)) by METRIC_1: 11;

                    hence (Y /\ G0) <> {} by A9, A51, XBOOLE_0:def 4;

                  end;

                    case

                     A57: s2 = ((G * (1,(j + 1))) `2 );

                    

                     A58: (p `1 ) = r2 & (p `2 ) = s2 by A33, EUCLID: 52;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A59: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then

                     A60: ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    set rl = (((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 ));

                    set rm = ( min (r,rl));

                    set r3 = (r2 - (r / 2)), s3 = (s2 - (rm / 2));

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    

                     A61: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A62: 1 <= ( len G) by Th34;

                    j < (j + 1) & (j + 1) <= ( width G) by A32, NAT_1: 13;

                    then ((G * (1,j)) `2 ) < ((G * (1,(j + 1))) `2 ) by A32, A62, GOBOARD5: 4;

                    then

                     A63: rl > 0 by XREAL_1: 50;

                    then

                     A64: rm > 0 by A8, XXREAL_0: 21;

                    then s3 < (s3 + (rm / 2)) by XREAL_1: 29, XREAL_1: 139;

                    then

                     A65: s3 < ((G * (1,(j + 1))) `2 ) by A36, XXREAL_0: 2;

                    (rm / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then ((rm / 2) ^2 ) <= ((r / 2) ^2 ) by A64, SQUARE_1: 15;

                    then

                     A66: (((r / 2) ^2 ) + ((rm / 2) ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 7;

                     0 <= ((rm / 2) ^2 ) & 0 <= ((r / 2) ^2 ) by XREAL_1: 63;

                    then ( sqrt (((r / 2) ^2 ) + ((rm / 2) ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A66, SQUARE_1: 26;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A59, A60, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by A58, A61, TOPREAL3: 7;

                    then

                     A67: u0 in ( Ball (u,r)) by METRIC_1: 11;

                    (rm / 2) <= (rl / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A68: (((G * (1,(j + 1))) `2 ) - (rm / 2)) >= (((G * (1,(j + 1))) `2 ) - (rl / 2)) by XREAL_1: 10;

                    (r * (2 " )) > 0 by A8, XREAL_1: 129;

                    then r3 < (r3 + (r / 2)) by XREAL_1: 29;

                    then

                     A69: r3 < ((G * (1,1)) `1 ) by A34, XXREAL_0: 2;

                    (((G * (1,(j + 1))) `2 ) - ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) > ((((G * (1,(j + 1))) `2 ) - ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) - ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) by A63, XREAL_1: 44, XREAL_1: 139;

                    then s3 > ((G * (1,j)) `2 ) by A57, A68, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : r1 < ((G * (1,1)) `1 ) & ((G * (1,j)) `2 ) < s1 & s1 < ((G * (1,(j + 1))) `2 ) } by A69, A65;

                    then u0 in Y by A32, GOBOARD6: 20;

                    hence (Y /\ G0) <> {} by A9, A67, XBOOLE_0:def 4;

                  end;

                end;

                hence (Y /\ G0) <> ( {} ( TOP-REAL 2));

              end;

                case

                 A70: i = ( len G) & j = 0 ;

                then p in { |[r2, s2]| : r2 >= ((G * (( len G),1)) `1 ) & ((G * (1,1)) `2 ) >= s2 } by A3, Th27;

                then

                consider r2, s2 such that

                 A71: p = |[r2, s2]| and

                 A72: r2 >= ((G * (( len G),1)) `1 ) and

                 A73: ((G * (1,1)) `2 ) >= s2;

                set r3 = (r2 + (r / 2)), s3 = (s2 - (r / 2));

                

                 A74: (r * (2 " )) > 0 by A8, XREAL_1: 129;

                then r3 > r2 by XREAL_1: 29;

                then

                 A75: r3 > ((G * (( len G),1)) `1 ) by A72, XXREAL_0: 2;

                reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                s3 < (s3 + (r / 2)) by A74, XREAL_1: 29;

                then s3 < ((G * (1,1)) `2 ) by A73, XXREAL_0: 2;

                then u0 in { |[r1, s1]| : r1 > ((G * (( len G),1)) `1 ) & ((G * (1,1)) `2 ) > s1 } by A75;

                then

                 A76: u0 in Y by A70, GOBOARD6: 21;

                reconsider v0 = u0 as Element of ( REAL 2);

                

                 A77: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                then

                 A78: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                .= (((r / 2) * ( sqrt 2)) ^2 );

                then

                 A79: ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A8, A78, Lm1, METRIC_1:def 1, SQUARE_1: 22;

                (p `1 ) = r2 & (p `2 ) = s2 by A71, EUCLID: 52;

                then ( dist (u,u0)) < r by A77, A79, TOPREAL3: 7;

                then u0 in ( Ball (u,r)) by METRIC_1: 11;

                hence (Y /\ G0) <> {} by A9, A76, XBOOLE_0:def 4;

              end;

                case

                 A80: i = ( len G) & j = ( width G);

                (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                then

                 A81: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                .= (((r / 2) * ( sqrt 2)) ^2 );

                then

                 A82: ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                p in { |[r2, s2]| : ((G * (( len G),1)) `1 ) <= r2 & ((G * (1,( width G))) `2 ) <= s2 } by A3, A80, Th28;

                then

                consider r2, s2 such that

                 A83: p = |[r2, s2]| and

                 A84: ((G * (( len G),1)) `1 ) <= r2 and

                 A85: ((G * (1,( width G))) `2 ) <= s2;

                set r3 = (r2 + (r / 2)), s3 = (s2 + (r / 2));

                

                 A86: (r * (2 " )) > 0 by A8, XREAL_1: 129;

                then s2 < (s2 + (r / 2)) by XREAL_1: 29;

                then

                 A87: s3 > ((G * (1,( width G))) `2 ) by A85, XXREAL_0: 2;

                reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                r2 < (r2 + (r / 2)) by A86, XREAL_1: 29;

                then r3 > ((G * (( len G),1)) `1 ) by A84, XXREAL_0: 2;

                then u0 in { |[r1, s1]| : r1 > ((G * (( len G),1)) `1 ) & s1 > ((G * (1,( width G))) `2 ) } by A87;

                then

                 A88: u0 in Y by A80, GOBOARD6: 22;

                reconsider v0 = u0 as Element of ( REAL 2);

                

                 A89: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                

                 A90: (( - (r / 2)) ^2 ) = ((r / 2) ^2 ) & ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) by METRIC_1:def 1;

                

                 A91: (r2 - r3) = ( - (r / 2)) & (s2 - s3) = ( - (r / 2));

                (p `1 ) = r2 & (p `2 ) = s2 by A83, EUCLID: 52;

                then ( dist (u,u0)) < r by A89, A91, A90, A81, A82, TOPREAL3: 7;

                then u0 in ( Ball (u,r)) by METRIC_1: 11;

                hence (Y /\ G0) <> {} by A9, A88, XBOOLE_0:def 4;

              end;

                case

                 A92: i = ( len G) & 1 <= j & j < ( width G);

                then p in { |[r2, s2]| : r2 >= ((G * (( len G),1)) `1 ) & ((G * (1,j)) `2 ) <= s2 & s2 <= ((G * (1,(j + 1))) `2 ) } by A3, Th29;

                then

                consider r2, s2 such that

                 A93: p = |[r2, s2]| and

                 A94: r2 >= ((G * (( len G),1)) `1 ) and

                 A95: ((G * (1,j)) `2 ) <= s2 and

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

                now

                  per cases by A95, A96, XXREAL_0: 1;

                    case

                     A97: s2 = ((G * (1,j)) `2 );

                    

                     A98: (p `1 ) = r2 & (p `2 ) = s2 by A93, EUCLID: 52;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A99: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then

                     A100: ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    set rl = (((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 ));

                    set rm = ( min (r,rl));

                    set r3 = (r2 + (r / 2)), s3 = (s2 + (rm / 2));

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    

                     A101: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A102: 1 <= ( len G) by Th34;

                    j < (j + 1) & (j + 1) <= ( width G) by A92, NAT_1: 13;

                    then ((G * (1,j)) `2 ) < ((G * (1,(j + 1))) `2 ) by A92, A102, GOBOARD5: 4;

                    then

                     A103: rl > 0 by XREAL_1: 50;

                    then

                     A104: rm > 0 by A8, XXREAL_0: 21;

                    then s3 > s2 by XREAL_1: 29, XREAL_1: 139;

                    then

                     A105: s3 > ((G * (1,j)) `2 ) by A95, XXREAL_0: 2;

                    (rm / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then ((rm / 2) ^2 ) <= ((r / 2) ^2 ) by A104, SQUARE_1: 15;

                    then

                     A106: (((r / 2) ^2 ) + ((rm / 2) ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 7;

                     0 <= ((rm / 2) ^2 ) & 0 <= ((r / 2) ^2 ) by XREAL_1: 63;

                    then ( sqrt (((r / 2) ^2 ) + ((rm / 2) ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A106, SQUARE_1: 26;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A99, A100, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by A98, A101, TOPREAL3: 7;

                    then

                     A107: u0 in ( Ball (u,r)) by METRIC_1: 11;

                    (rm / 2) <= (rl / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A108: (((G * (1,j)) `2 ) + (rm / 2)) <= (((G * (1,j)) `2 ) + (rl / 2)) by XREAL_1: 6;

                    (r * (2 " )) > 0 by A8, XREAL_1: 129;

                    then r2 < (r2 + (r / 2)) by XREAL_1: 29;

                    then

                     A109: r3 > ((G * (( len G),1)) `1 ) by A94, XXREAL_0: 2;

                    (((G * (1,j)) `2 ) + ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) < ((((G * (1,j)) `2 ) + ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) + ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) by A103, XREAL_1: 29, XREAL_1: 139;

                    then s3 < ((G * (1,(j + 1))) `2 ) by A97, A108, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : r1 > ((G * (( len G),1)) `1 ) & ((G * (1,j)) `2 ) < s1 & s1 < ((G * (1,(j + 1))) `2 ) } by A109, A105;

                    then u0 in Y by A92, GOBOARD6: 23;

                    hence (Y /\ G0) <> {} by A9, A107, XBOOLE_0:def 4;

                  end;

                    case

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

                    set r3 = (r2 + (r / 2)), s3 = s2;

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    (r * (2 " )) > 0 by A8, XREAL_1: 129;

                    then r2 < (r2 + (r / 2)) by XREAL_1: 29;

                    then r3 > ((G * (( len G),1)) `1 ) by A94, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : r1 > ((G * (( len G),1)) `1 ) & ((G * (1,j)) `2 ) < s1 & s1 < ((G * (1,(j + 1))) `2 ) } by A110;

                    then

                     A111: u0 in Y by A92, GOBOARD6: 23;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A112: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A113: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    

                     A114: ((r / 2) ^2 ) >= 0 by XREAL_1: 63;

                    then (((r / 2) ^2 ) + 0 ) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 6;

                    then

                     A115: ( sqrt (((r / 2) ^2 ) + ( 0 ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A114, SQUARE_1: 26;

                    

                     A116: (p `1 ) = r2 & (p `2 ) = s2 by A93, EUCLID: 52;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A113, A115, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by A116, A112, TOPREAL3: 7;

                    then u0 in ( Ball (u,r)) by METRIC_1: 11;

                    hence (Y /\ G0) <> {} by A9, A111, XBOOLE_0:def 4;

                  end;

                    case

                     A117: s2 = ((G * (1,(j + 1))) `2 );

                    

                     A118: (p `1 ) = r2 & (p `2 ) = s2 by A93, EUCLID: 52;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A119: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then

                     A120: ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    set rl = (((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 ));

                    set rm = ( min (r,rl));

                    set r3 = (r2 + (r / 2)), s3 = (s2 - (rm / 2));

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    

                     A121: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A122: 1 <= ( len G) by Th34;

                    j < (j + 1) & (j + 1) <= ( width G) by A92, NAT_1: 13;

                    then ((G * (1,j)) `2 ) < ((G * (1,(j + 1))) `2 ) by A92, A122, GOBOARD5: 4;

                    then

                     A123: rl > 0 by XREAL_1: 50;

                    then

                     A124: rm > 0 by A8, XXREAL_0: 21;

                    then s3 < (s3 + (rm / 2)) by XREAL_1: 29, XREAL_1: 139;

                    then

                     A125: s3 < ((G * (1,(j + 1))) `2 ) by A96, XXREAL_0: 2;

                    (rm / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then ((rm / 2) ^2 ) <= ((r / 2) ^2 ) by A124, SQUARE_1: 15;

                    then

                     A126: (((r / 2) ^2 ) + ((rm / 2) ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 7;

                     0 <= ((rm / 2) ^2 ) & 0 <= ((r / 2) ^2 ) by XREAL_1: 63;

                    then ( sqrt (((r / 2) ^2 ) + ((rm / 2) ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A126, SQUARE_1: 26;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A119, A120, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by A118, A121, TOPREAL3: 7;

                    then

                     A127: u0 in ( Ball (u,r)) by METRIC_1: 11;

                    (rm / 2) <= (rl / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A128: (((G * (1,(j + 1))) `2 ) - (rm / 2)) >= (((G * (1,(j + 1))) `2 ) - (rl / 2)) by XREAL_1: 10;

                    (r * (2 " )) > 0 by A8, XREAL_1: 129;

                    then r2 < (r2 + (r / 2)) by XREAL_1: 29;

                    then

                     A129: r3 > ((G * (( len G),1)) `1 ) by A94, XXREAL_0: 2;

                    (((G * (1,(j + 1))) `2 ) - ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) > ((((G * (1,(j + 1))) `2 ) - ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) - ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) by A123, XREAL_1: 44, XREAL_1: 139;

                    then s3 > ((G * (1,j)) `2 ) by A117, A128, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : r1 > ((G * (( len G),1)) `1 ) & ((G * (1,j)) `2 ) < s1 & s1 < ((G * (1,(j + 1))) `2 ) } by A129, A125;

                    then u0 in Y by A92, GOBOARD6: 23;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A127, XBOOLE_0:def 4;

                  end;

                end;

                hence (Y /\ G0) <> ( {} ( TOP-REAL 2));

              end;

                case

                 A130: 1 <= i & i < ( len G) & j = 0 ;

                then p in { |[r2, s2]| : ((G * (i,1)) `1 ) <= r2 & r2 <= ((G * ((i + 1),1)) `1 ) & s2 <= ((G * (1,1)) `2 ) } by A3, Th30;

                then

                consider r2, s2 such that

                 A131: p = |[r2, s2]| and

                 A132: ((G * (i,1)) `1 ) <= r2 and

                 A133: r2 <= ((G * ((i + 1),1)) `1 ) and

                 A134: s2 <= ((G * (1,1)) `2 );

                now

                  per cases by A132, A133, XXREAL_0: 1;

                    case

                     A135: r2 = ((G * (i,1)) `1 );

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then

                     A136: ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    set sl = (((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 ));

                    set sm = ( min (r,sl));

                    set s3 = (s2 - (r / 2)), r3 = (r2 + (sm / 2));

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    

                     A137: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A138: 1 <= ( width G) by Th34;

                    i < (i + 1) & (i + 1) <= ( len G) by A130, NAT_1: 13;

                    then ((G * (i,1)) `1 ) < ((G * ((i + 1),1)) `1 ) by A130, A138, GOBOARD5: 3;

                    then

                     A139: sl > 0 by XREAL_1: 50;

                    then

                     A140: sm > 0 by A8, XXREAL_0: 21;

                    then r3 > r2 by XREAL_1: 29, XREAL_1: 139;

                    then

                     A141: r3 > ((G * (i,1)) `1 ) by A132, XXREAL_0: 2;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A142: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    (sm / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then ((sm / 2) ^2 ) <= ((r / 2) ^2 ) by A140, SQUARE_1: 15;

                    then

                     A143: (((r / 2) ^2 ) + ((sm / 2) ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 7;

                     0 <= ((sm / 2) ^2 ) & 0 <= ((r / 2) ^2 ) by XREAL_1: 63;

                    then

                     A144: ( sqrt (((r / 2) ^2 ) + ((sm / 2) ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A143, SQUARE_1: 26;

                    (p `1 ) = r2 & (p `2 ) = s2 by A131, EUCLID: 52;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt ((((p `1 ) - (q0 `1 )) ^2 ) + (((p `2 ) - (q0 `2 )) ^2 ))) < r by A144, A137, A142, A136, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by TOPREAL3: 7;

                    then

                     A145: u0 in ( Ball (u,r)) by METRIC_1: 11;

                    (sm / 2) <= (sl / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A146: (((G * (i,1)) `1 ) + (sm / 2)) <= (((G * (i,1)) `1 ) + (sl / 2)) by XREAL_1: 6;

                    (r * (2 " )) > 0 by A8, XREAL_1: 129;

                    then s3 < (s3 + (r / 2)) by XREAL_1: 29;

                    then

                     A147: s3 < ((G * (1,1)) `2 ) by A134, XXREAL_0: 2;

                    (((G * (i,1)) `1 ) + ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) < ((((G * (i,1)) `1 ) + ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) + ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) by A139, XREAL_1: 29, XREAL_1: 139;

                    then r3 < ((G * ((i + 1),1)) `1 ) by A135, A146, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : ((G * (i,1)) `1 ) < r1 & r1 < ((G * ((i + 1),1)) `1 ) & s1 < ((G * (1,1)) `2 ) } by A147, A141;

                    then u0 in Y by A130, GOBOARD6: 24;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A145, XBOOLE_0:def 4;

                  end;

                    case

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

                    set s3 = (s2 - (r / 2)), r3 = r2;

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    (r * (2 " )) > 0 by A8, XREAL_1: 129;

                    then s3 < (s3 + (r / 2)) by XREAL_1: 29;

                    then s3 < ((G * (1,1)) `2 ) by A134, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : ((G * (i,1)) `1 ) < r1 & r1 < ((G * ((i + 1),1)) `1 ) & s1 < ((G * (1,1)) `2 ) } by A148;

                    then

                     A149: u0 in Y by A130, GOBOARD6: 24;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A150: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A151: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    

                     A152: ((r / 2) ^2 ) >= 0 by XREAL_1: 63;

                    then (( 0 ^2 ) + ((r / 2) ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 6;

                    then

                     A153: ( sqrt (( 0 ^2 ) + ((r / 2) ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A152, SQUARE_1: 26;

                    

                     A154: (p `1 ) = r2 & (p `2 ) = s2 by A131, EUCLID: 52;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A151, A153, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by A154, A150, TOPREAL3: 7;

                    then u0 in ( Ball (u,r)) by METRIC_1: 11;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A149, XBOOLE_0:def 4;

                  end;

                    case

                     A155: r2 = ((G * ((i + 1),1)) `1 );

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then

                     A156: ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    set sl = (((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 ));

                    set sm = ( min (r,sl));

                    set s3 = (s2 - (r / 2)), r3 = (r2 - (sm / 2));

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    

                     A157: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A158: 1 <= ( width G) by Th34;

                    i < (i + 1) & (i + 1) <= ( len G) by A130, NAT_1: 13;

                    then ((G * (i,1)) `1 ) < ((G * ((i + 1),1)) `1 ) by A130, A158, GOBOARD5: 3;

                    then

                     A159: sl > 0 by XREAL_1: 50;

                    then

                     A160: sm > 0 by A8, XXREAL_0: 21;

                    then r3 < (r3 + (sm / 2)) by XREAL_1: 29, XREAL_1: 139;

                    then

                     A161: r3 < ((G * ((i + 1),1)) `1 ) by A133, XXREAL_0: 2;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A162: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    (sm / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then ((sm / 2) ^2 ) <= ((r / 2) ^2 ) by A160, SQUARE_1: 15;

                    then

                     A163: (((r / 2) ^2 ) + ((sm / 2) ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 7;

                     0 <= ((sm / 2) ^2 ) & 0 <= ((r / 2) ^2 ) by XREAL_1: 63;

                    then

                     A164: ( sqrt (((r / 2) ^2 ) + ((sm / 2) ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A163, SQUARE_1: 26;

                    (p `1 ) = r2 & (p `2 ) = s2 by A131, EUCLID: 52;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt ((((p `1 ) - (q0 `1 )) ^2 ) + (((p `2 ) - (q0 `2 )) ^2 ))) < r by A164, A157, A162, A156, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by TOPREAL3: 7;

                    then

                     A165: u0 in ( Ball (u,r)) by METRIC_1: 11;

                    (sm / 2) <= (sl / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A166: (((G * ((i + 1),1)) `1 ) - (sm / 2)) >= (((G * ((i + 1),1)) `1 ) - (sl / 2)) by XREAL_1: 10;

                    (r * (2 " )) > 0 by A8, XREAL_1: 129;

                    then s3 < (s3 + (r / 2)) by XREAL_1: 29;

                    then

                     A167: s3 < ((G * (1,1)) `2 ) by A134, XXREAL_0: 2;

                    (((G * ((i + 1),1)) `1 ) - ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) > ((((G * ((i + 1),1)) `1 ) - ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) - ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) by A159, XREAL_1: 44, XREAL_1: 139;

                    then r3 > ((G * (i,1)) `1 ) by A155, A166, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : ((G * (i,1)) `1 ) < r1 & r1 < ((G * ((i + 1),1)) `1 ) & s1 < ((G * (1,1)) `2 ) } by A167, A161;

                    then u0 in Y by A130, GOBOARD6: 24;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A165, XBOOLE_0:def 4;

                  end;

                end;

                hence (Y /\ G0) <> ( {} ( TOP-REAL 2));

              end;

                case

                 A168: 1 <= i & i < ( len G) & j = ( width G);

                then p in { |[r2, s2]| : ((G * (i,1)) `1 ) <= r2 & r2 <= ((G * ((i + 1),1)) `1 ) & s2 >= ((G * (1,( width G))) `2 ) } by A3, Th31;

                then

                consider r2, s2 such that

                 A169: p = |[r2, s2]| and

                 A170: ((G * (i,1)) `1 ) <= r2 and

                 A171: r2 <= ((G * ((i + 1),1)) `1 ) and

                 A172: s2 >= ((G * (1,( width G))) `2 );

                now

                  per cases by A170, A171, XXREAL_0: 1;

                    case

                     A173: r2 = ((G * (i,1)) `1 );

                    

                     A174: (p `1 ) = r2 & (p `2 ) = s2 by A169, EUCLID: 52;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A175: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then

                     A176: ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    set rl = (((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 ));

                    set rm = ( min (r,rl));

                    set s3 = (s2 + (r / 2)), r3 = (r2 + (rm / 2));

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    

                     A177: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A178: 1 <= ( width G) by Th34;

                    i < (i + 1) & (i + 1) <= ( len G) by A168, NAT_1: 13;

                    then ((G * (i,1)) `1 ) < ((G * ((i + 1),1)) `1 ) by A168, A178, GOBOARD5: 3;

                    then

                     A179: rl > 0 by XREAL_1: 50;

                    then

                     A180: rm > 0 by A8, XXREAL_0: 21;

                    then r3 > r2 by XREAL_1: 29, XREAL_1: 139;

                    then

                     A181: r3 > ((G * (i,1)) `1 ) by A170, XXREAL_0: 2;

                    (rm / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then ((rm / 2) ^2 ) <= ((r / 2) ^2 ) by A180, SQUARE_1: 15;

                    then

                     A182: (((r / 2) ^2 ) + ((rm / 2) ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 7;

                     0 <= ((rm / 2) ^2 ) & 0 <= ((r / 2) ^2 ) by XREAL_1: 63;

                    then ( sqrt (((r / 2) ^2 ) + ((rm / 2) ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A182, SQUARE_1: 26;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A175, A176, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by A174, A177, TOPREAL3: 7;

                    then

                     A183: u0 in ( Ball (u,r)) by METRIC_1: 11;

                    (rm / 2) <= (rl / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A184: (((G * (i,1)) `1 ) + (rm / 2)) <= (((G * (i,1)) `1 ) + (rl / 2)) by XREAL_1: 6;

                    (r * (2 " )) > 0 by A8, XREAL_1: 129;

                    then s2 < (s2 + (r / 2)) by XREAL_1: 29;

                    then

                     A185: s3 > ((G * (1,( width G))) `2 ) by A172, XXREAL_0: 2;

                    (((G * (i,1)) `1 ) + ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) < ((((G * (i,1)) `1 ) + ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) + ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) by A179, XREAL_1: 29, XREAL_1: 139;

                    then r3 < ((G * ((i + 1),1)) `1 ) by A173, A184, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : ((G * (i,1)) `1 ) < r1 & r1 < ((G * ((i + 1),1)) `1 ) & s1 > ((G * (1,( width G))) `2 ) } by A185, A181;

                    then u0 in Y by A168, GOBOARD6: 25;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A183, XBOOLE_0:def 4;

                  end;

                    case

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

                    set s3 = (s2 + (r / 2)), r3 = r2;

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    (r * (2 " )) > 0 by A8, XREAL_1: 129;

                    then s2 < s3 by XREAL_1: 29;

                    then s3 > ((G * (1,( width G))) `2 ) by A172, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : ((G * (i,1)) `1 ) < r1 & r1 < ((G * ((i + 1),1)) `1 ) & s1 > ((G * (1,( width G))) `2 ) } by A186;

                    then

                     A187: u0 in Y by A168, GOBOARD6: 25;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A188: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A189: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    

                     A190: ((r / 2) ^2 ) >= 0 by XREAL_1: 63;

                    then (((r / 2) ^2 ) + ( 0 ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 6;

                    then

                     A191: ( sqrt (((r / 2) ^2 ) + ( 0 ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A190, SQUARE_1: 26;

                    

                     A192: (p `1 ) = r2 & (p `2 ) = s2 by A169, EUCLID: 52;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A189, A191, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by A192, A188, TOPREAL3: 7;

                    then u0 in ( Ball (u,r)) by METRIC_1: 11;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A187, XBOOLE_0:def 4;

                  end;

                    case

                     A193: r2 = ((G * ((i + 1),1)) `1 );

                    

                     A194: (p `1 ) = r2 & (p `2 ) = s2 by A169, EUCLID: 52;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A195: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then

                     A196: ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    set rl = (((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 ));

                    set rm = ( min (r,rl));

                    set s3 = (s2 + (r / 2)), r3 = (r2 - (rm / 2));

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    

                     A197: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A198: 1 <= ( width G) by Th34;

                    i < (i + 1) & (i + 1) <= ( len G) by A168, NAT_1: 13;

                    then ((G * (i,1)) `1 ) < ((G * ((i + 1),1)) `1 ) by A168, A198, GOBOARD5: 3;

                    then

                     A199: rl > 0 by XREAL_1: 50;

                    then

                     A200: rm > 0 by A8, XXREAL_0: 21;

                    then r3 < (r3 + (rm / 2)) by XREAL_1: 29, XREAL_1: 139;

                    then

                     A201: r3 < ((G * ((i + 1),1)) `1 ) by A171, XXREAL_0: 2;

                    (rm / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then ((rm / 2) ^2 ) <= ((r / 2) ^2 ) by A200, SQUARE_1: 15;

                    then

                     A202: (((r / 2) ^2 ) + ((rm / 2) ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 7;

                     0 <= ((rm / 2) ^2 ) & 0 <= ((r / 2) ^2 ) by XREAL_1: 63;

                    then ( sqrt (((r / 2) ^2 ) + ((rm / 2) ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A202, SQUARE_1: 26;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A195, A196, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by A194, A197, TOPREAL3: 7;

                    then

                     A203: u0 in ( Ball (u,r)) by METRIC_1: 11;

                    (rm / 2) <= (rl / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A204: (((G * ((i + 1),1)) `1 ) - (rm / 2)) >= (((G * ((i + 1),1)) `1 ) - (rl / 2)) by XREAL_1: 10;

                    (r * (2 " )) > 0 by A8, XREAL_1: 129;

                    then s3 > s2 by XREAL_1: 29;

                    then

                     A205: s3 > ((G * (1,( width G))) `2 ) by A172, XXREAL_0: 2;

                    (((G * ((i + 1),1)) `1 ) - ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) > ((((G * ((i + 1),1)) `1 ) - ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) - ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) by A199, XREAL_1: 44, XREAL_1: 139;

                    then r3 > ((G * (i,1)) `1 ) by A193, A204, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : ((G * (i,1)) `1 ) < r1 & r1 < ((G * ((i + 1),1)) `1 ) & s1 > ((G * (1,( width G))) `2 ) } by A205, A201;

                    then u0 in Y by A168, GOBOARD6: 25;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A203, XBOOLE_0:def 4;

                  end;

                end;

                hence (Y /\ G0) <> ( {} ( TOP-REAL 2));

              end;

                case

                 A206: 1 <= i & i < ( len G) & 1 <= j & j < ( width G);

                then p in { |[r2, s2]| : ((G * (i,1)) `1 ) <= r2 & r2 <= ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) <= s2 & s2 <= ((G * (1,(j + 1))) `2 ) } by A3, Th32;

                then

                consider r2, s2 such that

                 A207: p = |[r2, s2]| and

                 A208: ((G * (i,1)) `1 ) <= r2 and

                 A209: r2 <= ((G * ((i + 1),1)) `1 ) and

                 A210: ((G * (1,j)) `2 ) <= s2 and

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

                now

                  per cases by A208, A209, A210, A211, XXREAL_0: 1;

                    case

                     A212: r2 = ((G * (i,1)) `1 ) & s2 = ((G * (1,j)) `2 );

                    set rl1 = (((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 ));

                    set rl = (((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 ));

                    set rm = ( min (r,rl));

                    set rm1 = ( min (r,rl1));

                    set r3 = (r2 + (rm1 / 2)), s3 = (s2 + (rm / 2));

                    

                     A213: 1 <= ( width G) by Th34;

                    i < (i + 1) & (i + 1) <= ( len G) by A206, NAT_1: 13;

                    then ((G * (i,1)) `1 ) < ((G * ((i + 1),1)) `1 ) by A206, A213, GOBOARD5: 3;

                    then

                     A214: rl1 > 0 by XREAL_1: 50;

                    then

                     A215: rm1 > 0 by A8, XXREAL_0: 21;

                    then r3 > r2 by XREAL_1: 29, XREAL_1: 139;

                    then

                     A216: r3 > ((G * (i,1)) `1 ) by A208, XXREAL_0: 2;

                    (rm1 / 2) <= (rl1 / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A217: (((G * (i,1)) `1 ) + (rm1 / 2)) <= (((G * (i,1)) `1 ) + (rl1 / 2)) by XREAL_1: 6;

                    (((G * (i,1)) `1 ) + ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) < ((((G * (i,1)) `1 ) + ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) + ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) by A214, XREAL_1: 29, XREAL_1: 139;

                    then

                     A218: r3 < ((G * ((i + 1),1)) `1 ) by A212, A217, XXREAL_0: 2;

                    (rm / 2) <= (rl / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A219: (((G * (1,j)) `2 ) + (rm / 2)) <= (((G * (1,j)) `2 ) + (rl / 2)) by XREAL_1: 6;

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    

                     A220: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A221: 1 <= ( len G) by Th34;

                    j < (j + 1) & (j + 1) <= ( width G) by A206, NAT_1: 13;

                    then ((G * (1,j)) `2 ) < ((G * (1,(j + 1))) `2 ) by A206, A221, GOBOARD5: 4;

                    then

                     A222: rl > 0 by XREAL_1: 50;

                    then

                     A223: rm > 0 by A8, XXREAL_0: 21;

                    then s3 > s2 by XREAL_1: 29, XREAL_1: 139;

                    then

                     A224: s3 > ((G * (1,j)) `2 ) by A210, XXREAL_0: 2;

                    (rm1 / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A225: ((rm1 / 2) ^2 ) <= ((r / 2) ^2 ) by A215, SQUARE_1: 15;

                    (rm / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then ((rm / 2) ^2 ) <= ((r / 2) ^2 ) by A223, SQUARE_1: 15;

                    then

                     A226: (((rm1 / 2) ^2 ) + ((rm / 2) ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by A225, XREAL_1: 7;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A227: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then

                     A228: ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    

                     A229: (p `1 ) = r2 & (p `2 ) = s2 by A207, EUCLID: 52;

                     0 <= ((rm / 2) ^2 ) & 0 <= ((rm1 / 2) ^2 ) by XREAL_1: 63;

                    then ( sqrt (((rm1 / 2) ^2 ) + ((rm / 2) ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A226, SQUARE_1: 26;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A227, A228, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by A229, A220, TOPREAL3: 7;

                    then

                     A230: u0 in ( Ball (u,r)) by METRIC_1: 11;

                    (((G * (1,j)) `2 ) + ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) < ((((G * (1,j)) `2 ) + ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) + ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) by A222, XREAL_1: 29, XREAL_1: 139;

                    then s3 < ((G * (1,(j + 1))) `2 ) by A212, A219, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : ((G * (i,1)) `1 ) < r1 & r1 < ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s1 & s1 < ((G * (1,(j + 1))) `2 ) } by A224, A216, A218;

                    then u0 in Y by A206, GOBOARD6: 26;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A230, XBOOLE_0:def 4;

                  end;

                    case

                     A231: r2 = ((G * (i,1)) `1 ) & ((G * (1,j)) `2 ) < s2 & s2 < ((G * (1,(j + 1))) `2 );

                    set s3 = s2;

                    set rl1 = (((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 ));

                    set rm1 = ( min (r,rl1));

                    set r3 = (r2 + (rm1 / 2));

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    

                     A232: 1 <= ( width G) by Th34;

                    i < (i + 1) & (i + 1) <= ( len G) by A206, NAT_1: 13;

                    then ((G * (i,1)) `1 ) < ((G * ((i + 1),1)) `1 ) by A206, A232, GOBOARD5: 3;

                    then

                     A233: rl1 > 0 by XREAL_1: 50;

                    then

                     A234: rm1 > 0 by A8, XXREAL_0: 21;

                    then

                     A235: r3 > r2 by XREAL_1: 29, XREAL_1: 139;

                    (rm1 / 2) <= (rl1 / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A236: (((G * (i,1)) `1 ) + (rm1 / 2)) <= (((G * (i,1)) `1 ) + (rl1 / 2)) by XREAL_1: 6;

                    (((G * (i,1)) `1 ) + ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) < ((((G * (i,1)) `1 ) + ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) + ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) by A233, XREAL_1: 29, XREAL_1: 139;

                    then r3 < ((G * ((i + 1),1)) `1 ) by A231, A236, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : ((G * (i,1)) `1 ) < r1 & r1 < ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s1 & s1 < ((G * (1,(j + 1))) `2 ) } by A231, A235;

                    then

                     A237: u0 in Y by A206, GOBOARD6: 26;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A238: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A239: 0 <= ((rm1 / 2) ^2 ) by XREAL_1: 63;

                    (rm1 / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then (((rm1 / 2) ^2 ) + ( 0 ^2 )) <= (((r / 2) ^2 ) + ( 0 ^2 )) by A234, SQUARE_1: 15;

                    then

                     A240: ( sqrt (((rm1 / 2) ^2 ) + ( 0 ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ( 0 ^2 ))) by A239, SQUARE_1: 26;

                    

                     A241: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    

                     A242: ((r / 2) ^2 ) >= 0 by XREAL_1: 63;

                    then (((r / 2) ^2 ) + ( 0 ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 6;

                    then

                     A243: ( sqrt (((r / 2) ^2 ) + ( 0 ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A242, SQUARE_1: 26;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    then ( sqrt (((r / 2) ^2 ) + ( 0 ^2 ))) < r by A238, A243, XXREAL_0: 2;

                    then

                     A244: ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A240, METRIC_1:def 1, XXREAL_0: 2;

                    (p `1 ) = r2 & (p `2 ) = s2 by A207, EUCLID: 52;

                    then ( dist (u,u0)) < r by A241, A244, TOPREAL3: 7;

                    then u0 in ( Ball (u,r)) by METRIC_1: 11;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A237, XBOOLE_0:def 4;

                  end;

                    case

                     A245: r2 = ((G * (i,1)) `1 ) & s2 = ((G * (1,(j + 1))) `2 );

                    set rl1 = (((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 ));

                    set rl = (((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 ));

                    set rm = ( min (r,rl));

                    set rm1 = ( min (r,rl1));

                    set r3 = (r2 + (rm1 / 2)), s3 = (s2 - (rm / 2));

                    

                     A246: 1 <= ( width G) by Th34;

                    i < (i + 1) & (i + 1) <= ( len G) by A206, NAT_1: 13;

                    then ((G * (i,1)) `1 ) < ((G * ((i + 1),1)) `1 ) by A206, A246, GOBOARD5: 3;

                    then

                     A247: rl1 > 0 by XREAL_1: 50;

                    then

                     A248: rm1 > 0 by A8, XXREAL_0: 21;

                    then r3 > r2 by XREAL_1: 29, XREAL_1: 139;

                    then

                     A249: r3 > ((G * (i,1)) `1 ) by A208, XXREAL_0: 2;

                    (rm1 / 2) <= (rl1 / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A250: (((G * (i,1)) `1 ) + (rm1 / 2)) <= (((G * (i,1)) `1 ) + (rl1 / 2)) by XREAL_1: 6;

                    (((G * (i,1)) `1 ) + ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) < ((((G * (i,1)) `1 ) + ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) + ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) by A247, XREAL_1: 29, XREAL_1: 139;

                    then

                     A251: r3 < ((G * ((i + 1),1)) `1 ) by A245, A250, XXREAL_0: 2;

                    (rm / 2) <= (rl / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A252: (((G * (1,(j + 1))) `2 ) - (rm / 2)) >= (((G * (1,(j + 1))) `2 ) - (rl / 2)) by XREAL_1: 13;

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    

                     A253: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A254: 1 <= ( len G) by Th34;

                    j < (j + 1) & (j + 1) <= ( width G) by A206, NAT_1: 13;

                    then ((G * (1,j)) `2 ) < ((G * (1,(j + 1))) `2 ) by A206, A254, GOBOARD5: 4;

                    then

                     A255: rl > 0 by XREAL_1: 50;

                    then

                     A256: rm > 0 by A8, XXREAL_0: 21;

                    then s3 < s2 by XREAL_1: 44, XREAL_1: 139;

                    then

                     A257: s3 < ((G * (1,(j + 1))) `2 ) by A211, XXREAL_0: 2;

                    (rm1 / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A258: ((rm1 / 2) ^2 ) <= ((r / 2) ^2 ) by A248, SQUARE_1: 15;

                    (rm / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then ((rm / 2) ^2 ) <= ((r / 2) ^2 ) by A256, SQUARE_1: 15;

                    then

                     A259: (((rm1 / 2) ^2 ) + ((rm / 2) ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by A258, XREAL_1: 7;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A260: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then

                     A261: ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    

                     A262: (p `1 ) = r2 & (p `2 ) = s2 by A207, EUCLID: 52;

                     0 <= ((rm / 2) ^2 ) & 0 <= ((rm1 / 2) ^2 ) by XREAL_1: 63;

                    then ( sqrt (((rm1 / 2) ^2 ) + ((rm / 2) ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A259, SQUARE_1: 26;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A260, A261, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by A262, A253, TOPREAL3: 7;

                    then

                     A263: u0 in ( Ball (u,r)) by METRIC_1: 11;

                    (((G * (1,(j + 1))) `2 ) - ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) > ((((G * (1,(j + 1))) `2 ) - ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) - ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) by A255, XREAL_1: 44, XREAL_1: 139;

                    then s3 > ((G * (1,j)) `2 ) by A245, A252, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : ((G * (i,1)) `1 ) < r1 & r1 < ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s1 & s1 < ((G * (1,(j + 1))) `2 ) } by A257, A249, A251;

                    then u0 in Y by A206, GOBOARD6: 26;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A263, XBOOLE_0:def 4;

                  end;

                    case

                     A264: ((G * (i,1)) `1 ) < r2 & r2 < ((G * ((i + 1),1)) `1 ) & s2 = ((G * (1,j)) `2 );

                    set r3 = r2;

                    set rl = (((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 ));

                    set rm = ( min (r,rl));

                    set s3 = (s2 + (rm / 2));

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    

                     A265: 1 <= ( len G) by Th34;

                    j < (j + 1) & (j + 1) <= ( width G) by A206, NAT_1: 13;

                    then ((G * (1,j)) `2 ) < ((G * (1,(j + 1))) `2 ) by A206, A265, GOBOARD5: 4;

                    then

                     A266: rl > 0 by XREAL_1: 50;

                    then

                     A267: rm > 0 by A8, XXREAL_0: 21;

                    then

                     A268: s3 > s2 by XREAL_1: 29, XREAL_1: 139;

                    (rm / 2) <= (rl / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A269: (((G * (1,j)) `2 ) + (rm / 2)) <= (((G * (1,j)) `2 ) + (rl / 2)) by XREAL_1: 6;

                    (((G * (1,j)) `2 ) + ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) < ((((G * (1,j)) `2 ) + ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) + ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) by A266, XREAL_1: 29, XREAL_1: 139;

                    then s3 < ((G * (1,(j + 1))) `2 ) by A264, A269, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : ((G * (i,1)) `1 ) < r1 & r1 < ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s1 & s1 < ((G * (1,(j + 1))) `2 ) } by A264, A268;

                    then

                     A270: u0 in Y by A206, GOBOARD6: 26;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A271: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A272: 0 <= ((rm / 2) ^2 ) by XREAL_1: 63;

                    (rm / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then (((rm / 2) ^2 ) + ( 0 ^2 )) <= (((r / 2) ^2 ) + ( 0 ^2 )) by A267, SQUARE_1: 15;

                    then

                     A273: ( sqrt (( 0 ^2 ) + ((rm / 2) ^2 ))) <= ( sqrt (( 0 ^2 ) + ((r / 2) ^2 ))) by A272, SQUARE_1: 26;

                    

                     A274: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    

                     A275: ((r / 2) ^2 ) >= 0 by XREAL_1: 63;

                    then (( 0 ^2 ) + ((r / 2) ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 6;

                    then

                     A276: ( sqrt (( 0 ^2 ) + ((r / 2) ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A275, SQUARE_1: 26;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    then ( sqrt (( 0 ^2 ) + ((r / 2) ^2 ))) < r by A271, A276, XXREAL_0: 2;

                    then

                     A277: ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A273, METRIC_1:def 1, XXREAL_0: 2;

                    (p `1 ) = r2 & (p `2 ) = s2 by A207, EUCLID: 52;

                    then ( dist (u,u0)) < r by A274, A277, TOPREAL3: 7;

                    then u0 in ( Ball (u,r)) by METRIC_1: 11;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A270, XBOOLE_0:def 4;

                  end;

                    case

                     A278: ((G * (i,1)) `1 ) < r2 & r2 < ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s2 & s2 < ((G * (1,(j + 1))) `2 );

                    set s3 = s2, r3 = r2;

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    

                     A279: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A8, METRIC_1:def 1, SQUARE_1: 22;

                    then ( dist (u,u0)) < r by A207, A279, TOPREAL3: 7;

                    then

                     A280: u0 in ( Ball (u,r)) by METRIC_1: 11;

                    u0 in { |[r1, s1]| : ((G * (i,1)) `1 ) < r1 & r1 < ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s1 & s1 < ((G * (1,(j + 1))) `2 ) } by A278;

                    then u0 in Y by A206, GOBOARD6: 26;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A280, XBOOLE_0:def 4;

                  end;

                    case

                     A281: ((G * (i,1)) `1 ) < r2 & r2 < ((G * ((i + 1),1)) `1 ) & s2 = ((G * (1,(j + 1))) `2 );

                    set r3 = r2;

                    set rl = (((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 ));

                    set rm = ( min (r,rl));

                    set s3 = (s2 - (rm / 2));

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    

                     A282: 1 <= ( len G) by Th34;

                    j < (j + 1) & (j + 1) <= ( width G) by A206, NAT_1: 13;

                    then ((G * (1,j)) `2 ) < ((G * (1,(j + 1))) `2 ) by A206, A282, GOBOARD5: 4;

                    then

                     A283: rl > 0 by XREAL_1: 50;

                    then

                     A284: rm > 0 by A8, XXREAL_0: 21;

                    then

                     A285: s3 < s2 by XREAL_1: 44, XREAL_1: 139;

                    (rm / 2) <= (rl / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A286: (((G * (1,(j + 1))) `2 ) - (rm / 2)) >= (((G * (1,(j + 1))) `2 ) - (rl / 2)) by XREAL_1: 13;

                    (((G * (1,(j + 1))) `2 ) - ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) > ((((G * (1,(j + 1))) `2 ) - ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) - ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) by A283, XREAL_1: 44, XREAL_1: 139;

                    then s3 > ((G * (1,j)) `2 ) by A281, A286, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : ((G * (i,1)) `1 ) < r1 & r1 < ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s1 & s1 < ((G * (1,(j + 1))) `2 ) } by A281, A285;

                    then

                     A287: u0 in Y by A206, GOBOARD6: 26;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A288: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A289: 0 <= ((rm / 2) ^2 ) by XREAL_1: 63;

                    (rm / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then (((rm / 2) ^2 ) + ( 0 ^2 )) <= (((r / 2) ^2 ) + ( 0 ^2 )) by A284, SQUARE_1: 15;

                    then

                     A290: ( sqrt (( 0 ^2 ) + ((rm / 2) ^2 ))) <= ( sqrt (( 0 ^2 ) + ((r / 2) ^2 ))) by A289, SQUARE_1: 26;

                    

                     A291: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    

                     A292: ((r / 2) ^2 ) >= 0 by XREAL_1: 63;

                    then ( 0 + ((r / 2) ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 6;

                    then

                     A293: ( sqrt (( 0 ^2 ) + ((r / 2) ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A292, SQUARE_1: 26;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    then ( sqrt (( 0 ^2 ) + ((r / 2) ^2 ))) < r by A288, A293, XXREAL_0: 2;

                    then

                     A294: ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A290, METRIC_1:def 1, XXREAL_0: 2;

                    (p `1 ) = r2 & (p `2 ) = s2 by A207, EUCLID: 52;

                    then ( dist (u,u0)) < r by A291, A294, TOPREAL3: 7;

                    then u0 in ( Ball (u,r)) by METRIC_1: 11;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A287, XBOOLE_0:def 4;

                  end;

                    case

                     A295: r2 = ((G * ((i + 1),1)) `1 ) & s2 = ((G * (1,j)) `2 );

                    set rl1 = (((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 ));

                    set rl = (((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 ));

                    set rm = ( min (r,rl));

                    set rm1 = ( min (r,rl1));

                    set r3 = (r2 - (rm1 / 2)), s3 = (s2 + (rm / 2));

                    

                     A296: 1 <= ( width G) by Th34;

                    i < (i + 1) & (i + 1) <= ( len G) by A206, NAT_1: 13;

                    then ((G * (i,1)) `1 ) < ((G * ((i + 1),1)) `1 ) by A206, A296, GOBOARD5: 3;

                    then

                     A297: rl1 > 0 by XREAL_1: 50;

                    then

                     A298: rm1 > 0 by A8, XXREAL_0: 21;

                    then r3 < r2 by XREAL_1: 44, XREAL_1: 139;

                    then

                     A299: r3 < ((G * ((i + 1),1)) `1 ) by A209, XXREAL_0: 2;

                    (rm1 / 2) <= (rl1 / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A300: (((G * ((i + 1),1)) `1 ) - (rm1 / 2)) >= (((G * ((i + 1),1)) `1 ) - (rl1 / 2)) by XREAL_1: 13;

                    (((G * ((i + 1),1)) `1 ) - ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) > ((((G * ((i + 1),1)) `1 ) - ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) - ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) by A297, XREAL_1: 44, XREAL_1: 139;

                    then

                     A301: r3 > ((G * (i,1)) `1 ) by A295, A300, XXREAL_0: 2;

                    (rm / 2) <= (rl / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A302: (((G * (1,j)) `2 ) + (rm / 2)) <= (((G * (1,j)) `2 ) + (rl / 2)) by XREAL_1: 6;

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    

                     A303: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A304: 1 <= ( len G) by Th34;

                    j < (j + 1) & (j + 1) <= ( width G) by A206, NAT_1: 13;

                    then ((G * (1,j)) `2 ) < ((G * (1,(j + 1))) `2 ) by A206, A304, GOBOARD5: 4;

                    then

                     A305: rl > 0 by XREAL_1: 50;

                    then

                     A306: rm > 0 by A8, XXREAL_0: 21;

                    then s3 > s2 by XREAL_1: 29, XREAL_1: 139;

                    then

                     A307: s3 > ((G * (1,j)) `2 ) by A210, XXREAL_0: 2;

                    (rm1 / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A308: ((rm1 / 2) ^2 ) <= ((r / 2) ^2 ) by A298, SQUARE_1: 15;

                    (rm / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then ((rm / 2) ^2 ) <= ((r / 2) ^2 ) by A306, SQUARE_1: 15;

                    then

                     A309: (((rm1 / 2) ^2 ) + ((rm / 2) ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by A308, XREAL_1: 7;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A310: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then

                     A311: ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    

                     A312: (p `1 ) = r2 & (p `2 ) = s2 by A207, EUCLID: 52;

                     0 <= ((rm / 2) ^2 ) & 0 <= ((rm1 / 2) ^2 ) by XREAL_1: 63;

                    then ( sqrt (((rm1 / 2) ^2 ) + ((rm / 2) ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A309, SQUARE_1: 26;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A310, A311, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by A312, A303, TOPREAL3: 7;

                    then

                     A313: u0 in ( Ball (u,r)) by METRIC_1: 11;

                    (((G * (1,j)) `2 ) + ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) < ((((G * (1,j)) `2 ) + ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) + ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) by A305, XREAL_1: 29, XREAL_1: 139;

                    then s3 < ((G * (1,(j + 1))) `2 ) by A295, A302, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : ((G * (i,1)) `1 ) < r1 & r1 < ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s1 & s1 < ((G * (1,(j + 1))) `2 ) } by A307, A299, A301;

                    then u0 in Y by A206, GOBOARD6: 26;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A313, XBOOLE_0:def 4;

                  end;

                    case

                     A314: r2 = ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s2 & s2 < ((G * (1,(j + 1))) `2 );

                    set s3 = s2;

                    set rl1 = (((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 ));

                    set rm1 = ( min (r,rl1));

                    set r3 = (r2 - (rm1 / 2));

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    

                     A315: 1 <= ( width G) by Th34;

                    i < (i + 1) & (i + 1) <= ( len G) by A206, NAT_1: 13;

                    then ((G * (i,1)) `1 ) < ((G * ((i + 1),1)) `1 ) by A206, A315, GOBOARD5: 3;

                    then

                     A316: rl1 > 0 by XREAL_1: 50;

                    then

                     A317: rm1 > 0 by A8, XXREAL_0: 21;

                    then

                     A318: r3 < r2 by XREAL_1: 44, XREAL_1: 139;

                    (rm1 / 2) <= (rl1 / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A319: (((G * ((i + 1),1)) `1 ) - (rm1 / 2)) >= (((G * ((i + 1),1)) `1 ) - (rl1 / 2)) by XREAL_1: 13;

                    (((G * ((i + 1),1)) `1 ) - ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) > ((((G * ((i + 1),1)) `1 ) - ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) - ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) by A316, XREAL_1: 44, XREAL_1: 139;

                    then r3 > ((G * (i,1)) `1 ) by A314, A319, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : ((G * (i,1)) `1 ) < r1 & r1 < ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s1 & s1 < ((G * (1,(j + 1))) `2 ) } by A314, A318;

                    then

                     A320: u0 in Y by A206, GOBOARD6: 26;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A321: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A322: 0 <= ((rm1 / 2) ^2 ) by XREAL_1: 63;

                    (rm1 / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then (( 0 ^2 ) + ((rm1 / 2) ^2 )) <= (( 0 ^2 ) + ((r / 2) ^2 )) by A317, SQUARE_1: 15;

                    then

                     A323: ( sqrt (((rm1 / 2) ^2 ) + ( 0 ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ( 0 ^2 ))) by A322, SQUARE_1: 26;

                    

                     A324: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    

                     A325: ((r / 2) ^2 ) >= 0 by XREAL_1: 63;

                    then (((r / 2) ^2 ) + 0 ) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by XREAL_1: 6;

                    then

                     A326: ( sqrt (((r / 2) ^2 ) + ( 0 ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A325, SQUARE_1: 26;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    then ( sqrt (((r / 2) ^2 ) + ( 0 ^2 ))) < r by A321, A326, XXREAL_0: 2;

                    then

                     A327: ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((r2 - r3) ^2 ) + ((s2 - s3) ^2 ))) < r by A323, METRIC_1:def 1, XXREAL_0: 2;

                    (p `1 ) = r2 & (p `2 ) = s2 by A207, EUCLID: 52;

                    then ( dist (u,u0)) < r by A324, A327, TOPREAL3: 7;

                    then u0 in ( Ball (u,r)) by METRIC_1: 11;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A320, XBOOLE_0:def 4;

                  end;

                    case

                     A328: r2 = ((G * ((i + 1),1)) `1 ) & s2 = ((G * (1,(j + 1))) `2 );

                    set rl1 = (((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 ));

                    set rl = (((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 ));

                    set rm = ( min (r,rl));

                    set rm1 = ( min (r,rl1));

                    set r3 = (r2 - (rm1 / 2)), s3 = (s2 - (rm / 2));

                    

                     A329: 1 <= ( width G) by Th34;

                    i < (i + 1) & (i + 1) <= ( len G) by A206, NAT_1: 13;

                    then ((G * (i,1)) `1 ) < ((G * ((i + 1),1)) `1 ) by A206, A329, GOBOARD5: 3;

                    then

                     A330: rl1 > 0 by XREAL_1: 50;

                    then

                     A331: rm1 > 0 by A8, XXREAL_0: 21;

                    then r3 < r2 by XREAL_1: 44, XREAL_1: 139;

                    then

                     A332: r3 < ((G * ((i + 1),1)) `1 ) by A209, XXREAL_0: 2;

                    (rm1 / 2) <= (rl1 / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A333: (((G * ((i + 1),1)) `1 ) - (rm1 / 2)) >= (((G * ((i + 1),1)) `1 ) - (rl1 / 2)) by XREAL_1: 13;

                    (((G * ((i + 1),1)) `1 ) - ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) > ((((G * ((i + 1),1)) `1 ) - ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) - ((((G * ((i + 1),1)) `1 ) - ((G * (i,1)) `1 )) / 2)) by A330, XREAL_1: 44, XREAL_1: 139;

                    then

                     A334: r3 > ((G * (i,1)) `1 ) by A328, A333, XXREAL_0: 2;

                    (rm / 2) <= (rl / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A335: (((G * (1,(j + 1))) `2 ) - (rm / 2)) >= (((G * (1,(j + 1))) `2 ) - (rl / 2)) by XREAL_1: 13;

                    (( sqrt 2) / 2) < 1 by Lm1, SQUARE_1: 21, XREAL_1: 189;

                    then

                     A336: (r * (( sqrt 2) / 2)) < (r * 1) by A8, XREAL_1: 68;

                    

                     A337: (p `1 ) = r2 & (p `2 ) = s2 by A207, EUCLID: 52;

                    (((r / 2) ^2 ) + ((r / 2) ^2 )) = (2 * ((r / 2) ^2 ))

                    .= ((( sqrt 2) ^2 ) * ((r / 2) ^2 )) by SQUARE_1:def 2

                    .= (((r / 2) * ( sqrt 2)) ^2 );

                    then

                     A338: ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) = (r * (( sqrt 2) / 2)) by A8, Lm1, SQUARE_1: 22;

                    

                     A339: 1 <= ( len G) by Th34;

                    (rm1 / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then

                     A340: ((rm1 / 2) ^2 ) <= ((r / 2) ^2 ) by A331, SQUARE_1: 15;

                    reconsider q0 = |[r3, s3]| as Point of ( TOP-REAL 2);

                    

                     A341: (q0 `1 ) = r3 & (q0 `2 ) = s3 by EUCLID: 52;

                    reconsider u0 = q0 as Point of ( Euclid 2) by EUCLID: 22;

                    reconsider v0 = u0 as Element of ( REAL 2);

                    

                     A342: (r2 - r3) = (rm1 / 2) & (s2 - s3) = (rm / 2);

                    j < (j + 1) & (j + 1) <= ( width G) by A206, NAT_1: 13;

                    then ((G * (1,j)) `2 ) < ((G * (1,(j + 1))) `2 ) by A206, A339, GOBOARD5: 4;

                    then

                     A343: rl > 0 by XREAL_1: 50;

                    then

                     A344: rm > 0 by A8, XXREAL_0: 21;

                    then s3 < s2 by XREAL_1: 44, XREAL_1: 139;

                    then

                     A345: s3 < ((G * (1,(j + 1))) `2 ) by A211, XXREAL_0: 2;

                    (rm / 2) <= (r / 2) by XREAL_1: 72, XXREAL_0: 17;

                    then ((rm / 2) ^2 ) <= ((r / 2) ^2 ) by A344, SQUARE_1: 15;

                    then

                     A346: (((rm1 / 2) ^2 ) + ((rm / 2) ^2 )) <= (((r / 2) ^2 ) + ((r / 2) ^2 )) by A340, XREAL_1: 7;

                     0 <= ((rm / 2) ^2 ) & 0 <= ((rm1 / 2) ^2 ) by XREAL_1: 63;

                    then ( sqrt (((rm1 / 2) ^2 ) + ((rm / 2) ^2 ))) <= ( sqrt (((r / 2) ^2 ) + ((r / 2) ^2 ))) by A346, SQUARE_1: 26;

                    then ( dist (u,u0)) = (( Pitag_dist 2) . (v,v0)) & ( sqrt (((rm1 / 2) ^2 ) + ((rm / 2) ^2 ))) < r by A336, A338, METRIC_1:def 1, XXREAL_0: 2;

                    then ( dist (u,u0)) < r by A337, A341, A342, TOPREAL3: 7;

                    then

                     A347: u0 in ( Ball (u,r)) by METRIC_1: 11;

                    (((G * (1,(j + 1))) `2 ) - ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) > ((((G * (1,(j + 1))) `2 ) - ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) - ((((G * (1,(j + 1))) `2 ) - ((G * (1,j)) `2 )) / 2)) by A343, XREAL_1: 44, XREAL_1: 139;

                    then s3 > ((G * (1,j)) `2 ) by A328, A335, XXREAL_0: 2;

                    then u0 in { |[r1, s1]| : ((G * (i,1)) `1 ) < r1 & r1 < ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s1 & s1 < ((G * (1,(j + 1))) `2 ) } by A345, A332, A334;

                    then u0 in Y by A206, GOBOARD6: 26;

                    hence (Y /\ G0) <> ( {} ( TOP-REAL 2)) by A9, A347, XBOOLE_0:def 4;

                  end;

                end;

                hence (Y /\ G0) <> ( {} ( TOP-REAL 2));

              end;

            end;

            hence (Y /\ G0) <> ( {} ( TOP-REAL 2));

          end;

          hence thesis;

        end;

        hence thesis by PRE_TOPC:def 7;

      end;

      ( Cl Y) c= ( Cl ( cell (G,i,j))) & ( cell (G,i,j)) is closed by Th33, PRE_TOPC: 19, TOPS_1: 16;

      then ( Cl Y) c= ( cell (G,i,j)) by PRE_TOPC: 22;

      hence thesis by A2;

    end;