:: GOBRD11 semantic presentation begin Lm1: sqrt 2 > 0 by SQUARE_1:25; theorem Th1: :: GOBRD11:1 for GX being non empty TopSpace for A being Subset of GX for p being Point of GX st p in A & A is connected holds A c= Component_of p proof let GX be non empty TopSpace; ::_thesis: for A being Subset of GX for p being Point of GX st p in A & A is connected holds A c= Component_of p let A be Subset of GX; ::_thesis: for p being Point of GX st p in A & A is connected holds A c= Component_of p let p be Point of GX; ::_thesis: ( p in A & A is connected implies A c= Component_of p ) consider F being Subset-Family of GX such that A1: for B being 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 ) ; ::_thesis: A c= Component_of p then A3: A in F by A1; A c= union F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in union F ) thus ( not x in A or x in union F ) by A3, TARSKI:def_4; ::_thesis: verum end; hence A c= Component_of p by A2; ::_thesis: verum end; theorem :: GOBRD11:2 for GX being non empty TopSpace for A, B, C being 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 GX be non empty TopSpace; ::_thesis: for A, B, C being Subset of GX st C is a_component & A c= C & B is connected & Cl A meets Cl B holds B c= C let A, B, C be Subset of GX; ::_thesis: ( C is a_component & A c= C & B is connected & Cl A meets Cl B implies B c= C ) assume that A1: C is a_component and A2: A c= C and A3: B is connected and A4: (Cl A) /\ (Cl B) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: B c= C consider p being 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 B c= C by A7, A8, XBOOLE_1:1; ::_thesis: verum end; theorem :: GOBRD11:3 for GZ being non empty TopSpace for A, B being Subset of GZ st A is a_component & B is a_component holds A \/ B is a_union_of_components of GZ proof let GZ be non empty TopSpace; ::_thesis: for A, B being Subset of GZ st A is a_component & B is a_component holds A \/ B is a_union_of_components of GZ let A, B be Subset of GZ; ::_thesis: ( A is a_component & B is a_component implies A \/ B is a_union_of_components of GZ ) {A,B} c= bool the carrier of GZ proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {A,B} or x in bool the carrier of GZ ) assume x in {A,B} ; ::_thesis: x in bool the carrier of GZ then ( x = A or x = B ) by TARSKI:def_2; hence x in bool the carrier of GZ ; ::_thesis: verum 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 ) ; ::_thesis: A \/ B is a_union_of_components of GZ then A1: for B1 being 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 A \/ B is a_union_of_components of GZ by A1, CONNSP_3:def_2; ::_thesis: verum end; theorem :: GOBRD11:4 for GX being non empty TopSpace for B1, B2, V being Subset of GX holds Down ((B1 \/ B2),V) = (Down (B1,V)) \/ (Down (B2,V)) proof let GX be non empty TopSpace; ::_thesis: for B1, B2, V being Subset of GX holds Down ((B1 \/ B2),V) = (Down (B1,V)) \/ (Down (B2,V)) let B1, B2, V be Subset of GX; ::_thesis: Down ((B1 \/ B2),V) = (Down (B1,V)) \/ (Down (B2,V)) 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 Down ((B1 \/ B2),V) = (Down (B1,V)) \/ (Down (B2,V)) by A1, XBOOLE_1:23; ::_thesis: verum end; theorem :: GOBRD11:5 for GX being non empty TopSpace for B1, B2, V being Subset of GX holds Down ((B1 /\ B2),V) = (Down (B1,V)) /\ (Down (B2,V)) proof let GX be non empty TopSpace; ::_thesis: for B1, B2, V being Subset of GX holds Down ((B1 /\ B2),V) = (Down (B1,V)) /\ (Down (B2,V)) let B1, B2, V be Subset of GX; ::_thesis: Down ((B1 /\ B2),V) = (Down (B1,V)) /\ (Down (B2,V)) 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 Down ((B1 /\ B2),V) = (Down (B1,V)) /\ (Down (B2,V)) by A1, CONNSP_3:def_5; ::_thesis: verum end; theorem Th6: :: GOBRD11:6 for f being non constant standard special_circular_sequence holds (L~ f) ` <> {} proof let f be non constant standard special_circular_sequence; ::_thesis: (L~ f) ` <> {} 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 (L~ f) ` <> {} ; ::_thesis: verum end; registration let f be non constant standard special_circular_sequence; cluster(L~ f) ` -> non empty ; coherence not (L~ f) ` is empty by Th6; end; Lm2: the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22; theorem :: GOBRD11:7 for f being non constant standard special_circular_sequence holds the carrier of (TOP-REAL 2) = union { (cell ((GoB f),i,j)) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } proof let f be non constant standard special_circular_sequence; ::_thesis: the carrier of (TOP-REAL 2) = union { (cell ((GoB f),i,j)) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } set j1 = len (GoB f); set j2 = width (GoB f); thus the carrier of (TOP-REAL 2) c= union { (cell ((GoB f),i,j)) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } :: according to XBOOLE_0:def_10 ::_thesis: union { (cell ((GoB f),i,j)) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (TOP-REAL 2) or x in union { (cell ((GoB f),i,j)) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } ) assume x in the carrier of (TOP-REAL 2) ; ::_thesis: x in union { (cell ((GoB f),i,j)) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } then reconsider p = x as Point of (TOP-REAL 2) ; set r = p `1 ; A1: now__::_thesis:_(_not_p_`1_<_((GoB_f)_*_(1,1))_`1_&_not_((GoB_f)_*_((len_(GoB_f)),1))_`1_<=_p_`1_implies_ex_j_being_Element_of_NAT_st_ (_1_<=_j_&_j_<_len_(GoB_f)_&_((GoB_f)_*_(j,1))_`1_<=_p_`1_&_p_`1_<_((GoB_f)_*_((j_+_1),1))_`1_)_) assume that A2: not p `1 < ((GoB f) * (1,1)) `1 and A3: not ((GoB f) * ((len (GoB f)),1)) `1 <= p `1 ; ::_thesis: ex j being Element of NAT st ( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) now__::_thesis:_ex_j_being_Element_of_NAT_st_ (_1_<=_j_&_j_<_len_(GoB_f)_&_((GoB_f)_*_(j,1))_`1_<=_p_`1_&_p_`1_<_((GoB_f)_*_((j_+_1),1))_`1_) reconsider l = len (GoB f) as Element of NAT ; defpred S1[ Element of NAT ] means not ( not \$1 = 0 & 1 <= \$1 & \$1 < len (GoB f) & not ((GoB f) * ((\$1 + 1),1)) `1 <= p `1 ); 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: for j being Element of NAT holds ( not 1 <= j or not j < len (GoB f) or not ((GoB f) * (j,1)) `1 <= p `1 or not p `1 < ((GoB f) * ((j + 1),1)) `1 ) ; ::_thesis: contradiction A6: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A7: not ( not k = 0 & 1 <= k & k < len (GoB f) & not ((GoB f) * ((k + 1),1)) `1 <= p `1 ) ; ::_thesis: S1[k + 1] ( 1 <= k + 1 & k + 1 < len (GoB f) implies ((GoB f) * (((k + 1) + 1),1)) `1 <= p `1 ) proof assume A8: ( 1 <= k + 1 & k + 1 < len (GoB f) ) ; ::_thesis: ((GoB f) * (((k + 1) + 1),1)) `1 <= p `1 now__::_thesis:_not_p_`1_<_((GoB_f)_*_(((k_+_1)_+_1),1))_`1 A9: 0 <= k by NAT_1:2; assume A10: p `1 < ((GoB f) * (((k + 1) + 1),1)) `1 ; ::_thesis: contradiction then k <> 0 by A2, A5, GOBOARD7:32; then 0 + 1 <= k by A9, NAT_1:13; hence contradiction by A5, A7, A8, A10, XREAL_1:145; ::_thesis: verum end; hence ((GoB f) * (((k + 1) + 1),1)) `1 <= p `1 ; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A11: S1[ 0 ] ; A12: for j being Element of NAT holds S1[j] from NAT_1:sch_1(A11, A6); A13: l - 1 < (l - 1) + 1 by XREAL_1:29; then reconsider l1 = l - 1 as Element of NAT by A4, SPPOL_1:2; 0 < l1 by A4; hence contradiction by A3, A12, A4, A13; ::_thesis: verum end; hence ex j being Element of NAT st ( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) ; ::_thesis: verum end; now__::_thesis:_(_(_p_`1_<_((GoB_f)_*_(1,1))_`1_&_ex_j0_being_Element_of_NAT_st_ (_j0_<=_len_(GoB_f)_&_x_in_v_strip_((GoB_f),j0)_)_)_or_(_((GoB_f)_*_((len_(GoB_f)),1))_`1_<=_p_`1_&_ex_j0_being_Element_of_NAT_st_ (_j0_<=_len_(GoB_f)_&_x_in_v_strip_((GoB_f),j0)_)_)_or_(_ex_j_being_Element_of_NAT_st_ (_1_<=_j_&_j_<_len_(GoB_f)_&_((GoB_f)_*_(j,1))_`1_<=_p_`1_&_p_`1_<_((GoB_f)_*_((j_+_1),1))_`1_)_&_ex_j0_being_Element_of_NAT_st_ (_j0_<=_len_(GoB_f)_&_x_in_v_strip_((GoB_f),j0)_)_)_) percases ( p `1 < ((GoB f) * (1,1)) `1 or ((GoB f) * ((len (GoB f)),1)) `1 <= p `1 or ex j being Element of NAT st ( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) ) by A1; caseA14: p `1 < ((GoB f) * (1,1)) `1 ; ::_thesis: ex j0 being Element of NAT st ( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) reconsider G = GoB f as Go-board ; 1 <= width G by GOBOARD7:33; then A15: v_strip (G,0) = { |[r1,s]| where r1, s is Real : r1 <= (G * (1,1)) `1 } by GOBOARD5:10; |[(p `1),(p `2)]| in { |[r1,s]| where r1, s is Real : r1 <= ((GoB f) * (1,1)) `1 } by A14; then p in v_strip ((GoB f),0) by A15, EUCLID:53; hence ex j0 being Element of NAT st ( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) by NAT_1:2; ::_thesis: verum end; caseA16: ((GoB f) * ((len (GoB f)),1)) `1 <= p `1 ; ::_thesis: ex j0 being Element of NAT st ( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) reconsider G = GoB f as Go-board ; 1 <= width G by GOBOARD7:33; then A17: v_strip (G,(len G)) = { |[r1,s]| where r1, s is Real : (G * ((len G),1)) `1 <= r1 } by GOBOARD5:9; |[(p `1),(p `2)]| in { |[r1,s]| where r1, s is Real : ((GoB f) * ((len G),1)) `1 <= r1 } by A16; then p in v_strip ((GoB f),(len (GoB f))) by A17, EUCLID:53; hence ex j0 being Element of NAT st ( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) ; ::_thesis: verum end; caseA18: ex j being Element of NAT st ( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) ; ::_thesis: ex j0 being Element of NAT st ( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) reconsider G = GoB f as Go-board ; consider j being Element of NAT such that A19: 1 <= j and A20: j < len (GoB f) and A21: ( ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) by A18; A22: |[(p `1),(p `2)]| in { |[r1,s]| where r1, s is Real : ( (G * (j,1)) `1 <= r1 & r1 <= (G * ((j + 1),1)) `1 ) } by A21; 1 <= width G by GOBOARD7:33; then v_strip (G,j) = { |[r1,s]| where r1, s is Real : ( (G * (j,1)) `1 <= r1 & r1 <= (G * ((j + 1),1)) `1 ) } by A19, A20, GOBOARD5:8; then p in v_strip ((GoB f),j) by A22, EUCLID:53; hence ex j0 being Element of NAT st ( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) by A20; ::_thesis: verum end; end; end; then consider j0 being Element of NAT such that A23: j0 <= len (GoB f) and A24: x in v_strip ((GoB f),j0) ; set s = p `2 ; A25: now__::_thesis:_(_not_p_`2_<_((GoB_f)_*_(1,1))_`2_&_not_((GoB_f)_*_(1,(width_(GoB_f))))_`2_<=_p_`2_implies_ex_j_being_Element_of_NAT_st_ (_1_<=_j_&_j_<_width_(GoB_f)_&_((GoB_f)_*_(1,j))_`2_<=_p_`2_&_p_`2_<_((GoB_f)_*_(1,(j_+_1)))_`2_)_) assume that A26: not p `2 < ((GoB f) * (1,1)) `2 and A27: not ((GoB f) * (1,(width (GoB f)))) `2 <= p `2 ; ::_thesis: ex j being Element of NAT st ( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) now__::_thesis:_ex_j_being_Element_of_NAT_st_ (_1_<=_j_&_j_<_width_(GoB_f)_&_((GoB_f)_*_(1,j))_`2_<=_p_`2_&_p_`2_<_((GoB_f)_*_(1,(j_+_1)))_`2_) reconsider l = width (GoB f) as Element of NAT ; defpred S1[ Element of NAT ] means not ( not \$1 = 0 & 1 <= \$1 & \$1 < width (GoB f) & not ((GoB f) * (1,(\$1 + 1))) `2 <= p `2 ); 1 < width (GoB f) by GOBOARD7:33; then 1 + 1 <= width (GoB f) by NAT_1:13; then A28: (1 + 1) - 1 <= l - 1 by XREAL_1:9; assume A29: for j being Element of NAT holds ( not 1 <= j or not j < width (GoB f) or not ((GoB f) * (1,j)) `2 <= p `2 or not p `2 < ((GoB f) * (1,(j + 1))) `2 ) ; ::_thesis: contradiction A30: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A31: not ( not k = 0 & 1 <= k & k < width (GoB f) & not ((GoB f) * (1,(k + 1))) `2 <= p `2 ) ; ::_thesis: S1[k + 1] ( 1 <= k + 1 & k + 1 < width (GoB f) implies ((GoB f) * (1,((k + 1) + 1))) `2 <= p `2 ) proof assume A32: ( 1 <= k + 1 & k + 1 < width (GoB f) ) ; ::_thesis: ((GoB f) * (1,((k + 1) + 1))) `2 <= p `2 now__::_thesis:_not_p_`2_<_((GoB_f)_*_(1,((k_+_1)_+_1)))_`2 A33: 0 <= k by NAT_1:2; assume A34: p `2 < ((GoB f) * (1,((k + 1) + 1))) `2 ; ::_thesis: contradiction then k <> 0 by A26, A29, GOBOARD7:33; then 0 + 1 <= k by A33, NAT_1:13; hence contradiction by A29, A31, A32, A34, XREAL_1:145; ::_thesis: verum end; hence ((GoB f) * (1,((k + 1) + 1))) `2 <= p `2 ; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A35: S1[ 0 ] ; A36: for j being Element of NAT holds S1[j] from NAT_1:sch_1(A35, A30); A37: l - 1 < (l - 1) + 1 by XREAL_1:29; then reconsider l1 = l - 1 as Element of NAT by A28, SPPOL_1:2; 0 < l1 by A28; hence contradiction by A27, A36, A28, A37; ::_thesis: verum end; hence ex j being Element of NAT st ( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) ; ::_thesis: verum end; now__::_thesis:_(_(_p_`2_<_((GoB_f)_*_(1,1))_`2_&_ex_i0_being_Element_of_NAT_st_ (_i0_<=_width_(GoB_f)_&_x_in_h_strip_((GoB_f),i0)_)_)_or_(_((GoB_f)_*_(1,(width_(GoB_f))))_`2_<=_p_`2_&_ex_i0_being_Element_of_NAT_st_ (_i0_<=_width_(GoB_f)_&_x_in_h_strip_((GoB_f),i0)_)_)_or_(_ex_j_being_Element_of_NAT_st_ (_1_<=_j_&_j_<_width_(GoB_f)_&_((GoB_f)_*_(1,j))_`2_<=_p_`2_&_p_`2_<_((GoB_f)_*_(1,(j_+_1)))_`2_)_&_ex_i0_being_Element_of_NAT_st_ (_i0_<=_width_(GoB_f)_&_x_in_h_strip_((GoB_f),i0)_)_)_) percases ( p `2 < ((GoB f) * (1,1)) `2 or ((GoB f) * (1,(width (GoB f)))) `2 <= p `2 or ex j being Element of NAT st ( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) ) by A25; caseA38: p `2 < ((GoB f) * (1,1)) `2 ; ::_thesis: ex i0 being Element of NAT st ( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) reconsider G = GoB f as Go-board ; 1 <= len G by GOBOARD7:32; then A39: h_strip (G,0) = { |[r1,s1]| where r1, s1 is Real : s1 <= (G * (1,1)) `2 } by GOBOARD5:7; |[(p `1),(p `2)]| in { |[r1,s1]| where r1, s1 is Real : s1 <= ((GoB f) * (1,1)) `2 } by A38; then p in h_strip ((GoB f),0) by A39, EUCLID:53; hence ex i0 being Element of NAT st ( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) by NAT_1:2; ::_thesis: verum end; caseA40: ((GoB f) * (1,(width (GoB f)))) `2 <= p `2 ; ::_thesis: ex i0 being Element of NAT st ( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) reconsider G = GoB f as Go-board ; 1 <= len G by GOBOARD7:32; then A41: h_strip (G,(width G)) = { |[r1,s1]| where r1, s1 is Real : (G * (1,(width G))) `2 <= s1 } by GOBOARD5:6; |[(p `1),(p `2)]| in { |[r1,s1]| where r1, s1 is Real : ((GoB f) * (1,(width G))) `2 <= s1 } by A40; then p in h_strip ((GoB f),(width (GoB f))) by A41, EUCLID:53; hence ex i0 being Element of NAT st ( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) ; ::_thesis: verum end; caseA42: ex j being Element of NAT st ( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) ; ::_thesis: ex i0 being Element of NAT st ( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) reconsider G = GoB f as Go-board ; consider j being Element of NAT such that A43: 1 <= j and A44: j < width (GoB f) and A45: ( ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) by A42; A46: |[(p `1),(p `2)]| in { |[r1,s1]| where r1, s1 is Real : ( (G * (1,j)) `2 <= s1 & s1 <= (G * (1,(j + 1))) `2 ) } by A45; 1 <= len G by GOBOARD7:32; then h_strip (G,j) = { |[r1,s1]| where r1, s1 is Real : ( (G * (1,j)) `2 <= s1 & s1 <= (G * (1,(j + 1))) `2 ) } by A43, A44, GOBOARD5:5; then p in h_strip ((GoB f),j) by A46, EUCLID:53; hence ex i0 being Element of NAT st ( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) by A44; ::_thesis: verum end; end; end; then consider i0 being Element of NAT such that A47: i0 <= width (GoB f) and A48: 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 A24, A48, XBOOLE_0:def_4; then A49: x in X0 by GOBOARD5:def_3; X0 in { (cell ((GoB f),i,j)) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } by A23, A47; hence x in union { (cell ((GoB f),i,j)) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } by A49, TARSKI:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { (cell ((GoB f),i,j)) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } or x in the carrier of (TOP-REAL 2) ) assume x in union { (cell ((GoB f),i,j)) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } ; ::_thesis: x in the carrier of (TOP-REAL 2) then consider X0 being set such that A50: ( x in X0 & X0 in { (cell ((GoB f),i,j)) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } ) by TARSKI:def_4; ex i, j being Element of NAT st ( X0 = cell ((GoB f),i,j) & i <= len (GoB f) & j <= width (GoB f) ) by A50; hence x in the carrier of (TOP-REAL 2) by A50; ::_thesis: verum end; Lm3: for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb >= s1 } is Subset of (TOP-REAL 2) proof let s1 be Real; ::_thesis: { |[tb,sb]| where tb, sb is Real : sb >= s1 } is Subset of (TOP-REAL 2) { |[tb,sb]| where tb, sb is Real : sb >= s1 } c= REAL 2 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { |[tb,sb]| where tb, sb is Real : sb >= s1 } or y in REAL 2 ) assume y in { |[tb,sb]| where tb, sb is Real : sb >= s1 } ; ::_thesis: y in REAL 2 then ex t7, s7 being Real st ( |[t7,s7]| = y & s7 >= s1 ) ; hence y in REAL 2 by Lm2; ::_thesis: verum end; hence { |[tb,sb]| where tb, sb is Real : sb >= s1 } is Subset of (TOP-REAL 2) by EUCLID:22; ::_thesis: verum end; Lm4: for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb > s1 } is Subset of (TOP-REAL 2) proof let s1 be Real; ::_thesis: { |[tb,sb]| where tb, sb is Real : sb > s1 } is Subset of (TOP-REAL 2) { |[tb,sb]| where tb, sb is Real : sb > s1 } c= REAL 2 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { |[tb,sb]| where tb, sb is Real : sb > s1 } or y in REAL 2 ) assume y in { |[tb,sb]| where tb, sb is Real : sb > s1 } ; ::_thesis: y in REAL 2 then ex t7, s7 being Real st ( |[t7,s7]| = y & s7 > s1 ) ; hence y in REAL 2 by Lm2; ::_thesis: verum end; hence { |[tb,sb]| where tb, sb is Real : sb > s1 } is Subset of (TOP-REAL 2) by EUCLID:22; ::_thesis: verum end; Lm5: for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb <= s1 } is Subset of (TOP-REAL 2) proof let s1 be Real; ::_thesis: { |[tb,sb]| where tb, sb is Real : sb <= s1 } is Subset of (TOP-REAL 2) { |[tb,sb]| where tb, sb is Real : sb <= s1 } c= REAL 2 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { |[tb,sb]| where tb, sb is Real : sb <= s1 } or y in REAL 2 ) assume y in { |[tb,sb]| where tb, sb is Real : sb <= s1 } ; ::_thesis: y in REAL 2 then ex t7, s7 being Real st ( |[t7,s7]| = y & s7 <= s1 ) ; hence y in REAL 2 by Lm2; ::_thesis: verum end; hence { |[tb,sb]| where tb, sb is Real : sb <= s1 } is Subset of (TOP-REAL 2) by EUCLID:22; ::_thesis: verum end; Lm6: for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb < s1 } is Subset of (TOP-REAL 2) proof let s1 be Real; ::_thesis: { |[tb,sb]| where tb, sb is Real : sb < s1 } is Subset of (TOP-REAL 2) { |[tb,sb]| where tb, sb is Real : sb < s1 } c= REAL 2 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { |[tb,sb]| where tb, sb is Real : sb < s1 } or y in REAL 2 ) assume y in { |[tb,sb]| where tb, sb is Real : sb < s1 } ; ::_thesis: y in REAL 2 then ex t7, s7 being Real st ( |[t7,s7]| = y & s7 < s1 ) ; hence y in REAL 2 by Lm2; ::_thesis: verum end; hence { |[tb,sb]| where tb, sb is Real : sb < s1 } is Subset of (TOP-REAL 2) by EUCLID:22; ::_thesis: verum end; Lm7: for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb <= s1 } is Subset of (TOP-REAL 2) proof let s1 be Real; ::_thesis: { |[sb,tb]| where sb, tb is Real : sb <= s1 } is Subset of (TOP-REAL 2) { |[sb,tb]| where sb, tb is Real : sb <= s1 } c= REAL 2 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { |[sb,tb]| where sb, tb is Real : sb <= s1 } or y in REAL 2 ) assume y in { |[sb,tb]| where sb, tb is Real : sb <= s1 } ; ::_thesis: y in REAL 2 then ex s7, t7 being Real st ( |[s7,t7]| = y & s7 <= s1 ) ; hence y in REAL 2 by Lm2; ::_thesis: verum end; hence { |[sb,tb]| where sb, tb is Real : sb <= s1 } is Subset of (TOP-REAL 2) by EUCLID:22; ::_thesis: verum end; Lm8: for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb < s1 } is Subset of (TOP-REAL 2) proof let s1 be Real; ::_thesis: { |[sb,tb]| where sb, tb is Real : sb < s1 } is Subset of (TOP-REAL 2) { |[sb,tb]| where sb, tb is Real : sb < s1 } c= REAL 2 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { |[sb,tb]| where sb, tb is Real : sb < s1 } or y in REAL 2 ) assume y in { |[sb,tb]| where sb, tb is Real : sb < s1 } ; ::_thesis: y in REAL 2 then ex s7, t7 being Real st ( |[s7,t7]| = y & s7 < s1 ) ; hence y in REAL 2 by Lm2; ::_thesis: verum end; hence { |[sb,tb]| where sb, tb is Real : sb < s1 } is Subset of (TOP-REAL 2) by EUCLID:22; ::_thesis: verum end; Lm9: for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb >= s1 } is Subset of (TOP-REAL 2) proof let s1 be Real; ::_thesis: { |[sb,tb]| where sb, tb is Real : sb >= s1 } is Subset of (TOP-REAL 2) { |[sb,tb]| where sb, tb is Real : sb >= s1 } c= REAL 2 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { |[sb,tb]| where sb, tb is Real : sb >= s1 } or y in REAL 2 ) assume y in { |[sb,tb]| where sb, tb is Real : sb >= s1 } ; ::_thesis: y in REAL 2 then ex s7, t7 being Real st ( |[s7,t7]| = y & s7 >= s1 ) ; hence y in REAL 2 by Lm2; ::_thesis: verum end; hence { |[sb,tb]| where sb, tb is Real : sb >= s1 } is Subset of (TOP-REAL 2) by EUCLID:22; ::_thesis: verum end; Lm10: for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb > s1 } is Subset of (TOP-REAL 2) proof let s1 be Real; ::_thesis: { |[sb,tb]| where sb, tb is Real : sb > s1 } is Subset of (TOP-REAL 2) { |[sb,tb]| where sb, tb is Real : sb > s1 } c= REAL 2 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { |[sb,tb]| where sb, tb is Real : sb > s1 } or y in REAL 2 ) assume y in { |[sb,tb]| where sb, tb is Real : sb > s1 } ; ::_thesis: y in REAL 2 then ex s7, t7 being Real st ( |[s7,t7]| = y & s7 > s1 ) ; hence y in REAL 2 by Lm2; ::_thesis: verum end; hence { |[sb,tb]| where sb, tb is Real : sb > s1 } is Subset of (TOP-REAL 2) by EUCLID:22; ::_thesis: verum end; theorem Th8: :: GOBRD11:8 for s1 being Real for P1, P2 being Subset of (TOP-REAL 2) st P1 = { |[r,s]| where r, s is Real : s <= s1 } & P2 = { |[r2,s2]| where r2, s2 is Real : s2 > s1 } holds P1 = P2 ` proof let s1 be Real; ::_thesis: for P1, P2 being Subset of (TOP-REAL 2) st P1 = { |[r,s]| where r, s is Real : s <= s1 } & P2 = { |[r2,s2]| where r2, s2 is Real : s2 > s1 } holds P1 = P2 ` let P1, P2 be Subset of (TOP-REAL 2); ::_thesis: ( P1 = { |[r,s]| where r, s is Real : s <= s1 } & P2 = { |[r2,s2]| where r2, s2 is Real : s2 > s1 } implies P1 = P2 ` ) assume A1: ( P1 = { |[r,s]| where r, s is Real : s <= s1 } & P2 = { |[r2,s2]| where r2, s2 is Real : s2 > s1 } ) ; ::_thesis: P1 = P2 ` A2: P2 ` c= P1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P2 ` or x in P1 ) assume A3: x in P2 ` ; ::_thesis: x in P1 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 x in P1 by A1, A4; ::_thesis: verum end; P1 c= P2 ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P1 or x in P2 ` ) assume A5: x in P1 ; ::_thesis: x in P2 ` then ex r, s being Real st ( |[r,s]| = x & s <= s1 ) by A1; then for r2, s2 being Real holds ( not |[r2,s2]| = x or not 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 x in P2 ` by SUBSET_1:def_4; ::_thesis: verum end; hence P1 = P2 ` by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th9: :: GOBRD11:9 for s1 being Real for P1, P2 being Subset of (TOP-REAL 2) st P1 = { |[r,s]| where r, s is Real : s >= s1 } & P2 = { |[r2,s2]| where r2, s2 is Real : s2 < s1 } holds P1 = P2 ` proof let s1 be Real; ::_thesis: for P1, P2 being Subset of (TOP-REAL 2) st P1 = { |[r,s]| where r, s is Real : s >= s1 } & P2 = { |[r2,s2]| where r2, s2 is Real : s2 < s1 } holds P1 = P2 ` let P1, P2 be Subset of (TOP-REAL 2); ::_thesis: ( P1 = { |[r,s]| where r, s is Real : s >= s1 } & P2 = { |[r2,s2]| where r2, s2 is Real : s2 < s1 } implies P1 = P2 ` ) assume A1: ( P1 = { |[r,s]| where r, s is Real : s >= s1 } & P2 = { |[r2,s2]| where r2, s2 is Real : s2 < s1 } ) ; ::_thesis: P1 = P2 ` A2: P2 ` c= P1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P2 ` or x in P1 ) assume A3: x in P2 ` ; ::_thesis: x in P1 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 x in P1 by A1, A4; ::_thesis: verum end; P1 c= P2 ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P1 or x in P2 ` ) assume A5: x in P1 ; ::_thesis: x in P2 ` then ex r, s being Real st ( |[r,s]| = x & s >= s1 ) by A1; then for r2, s2 being Real holds ( not |[r2,s2]| = x or not 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 x in P2 ` by SUBSET_1:def_4; ::_thesis: verum end; hence P1 = P2 ` by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th10: :: GOBRD11:10 for s1 being Real for P1, P2 being Subset of (TOP-REAL 2) st P1 = { |[s,r]| where s, r is Real : s >= s1 } & P2 = { |[s2,r2]| where s2, r2 is Real : s2 < s1 } holds P1 = P2 ` proof let s1 be Real; ::_thesis: for P1, P2 being Subset of (TOP-REAL 2) st P1 = { |[s,r]| where s, r is Real : s >= s1 } & P2 = { |[s2,r2]| where s2, r2 is Real : s2 < s1 } holds P1 = P2 ` let P1, P2 be Subset of (TOP-REAL 2); ::_thesis: ( P1 = { |[s,r]| where s, r is Real : s >= s1 } & P2 = { |[s2,r2]| where s2, r2 is Real : s2 < s1 } implies P1 = P2 ` ) assume A1: ( P1 = { |[s,r]| where s, r is Real : s >= s1 } & P2 = { |[s2,r2]| where s2, r2 is Real : s2 < s1 } ) ; ::_thesis: P1 = P2 ` A2: P2 ` c= P1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P2 ` or x in P1 ) assume A3: x in P2 ` ; ::_thesis: x in P1 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 x in P1 by A1, A4; ::_thesis: verum end; P1 c= P2 ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P1 or x in P2 ` ) assume A5: x in P1 ; ::_thesis: x in P2 ` then ex s, r being Real st ( |[s,r]| = x & s >= s1 ) by A1; then for s2, r2 being Real holds ( not |[s2,r2]| = x or not 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 x in P2 ` by SUBSET_1:def_4; ::_thesis: verum end; hence P1 = P2 ` by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th11: :: GOBRD11:11 for s1 being Real for P1, P2 being Subset of (TOP-REAL 2) st P1 = { |[s,r]| where s, r is Real : s <= s1 } & P2 = { |[s2,r2]| where s2, r2 is Real : s2 > s1 } holds P1 = P2 ` proof let s1 be Real; ::_thesis: for P1, P2 being Subset of (TOP-REAL 2) st P1 = { |[s,r]| where s, r is Real : s <= s1 } & P2 = { |[s2,r2]| where s2, r2 is Real : s2 > s1 } holds P1 = P2 ` let P1, P2 be Subset of (TOP-REAL 2); ::_thesis: ( P1 = { |[s,r]| where s, r is Real : s <= s1 } & P2 = { |[s2,r2]| where s2, r2 is Real : s2 > s1 } implies P1 = P2 ` ) assume A1: ( P1 = { |[s,r]| where s, r is Real : s <= s1 } & P2 = { |[s2,r2]| where s2, r2 is Real : s2 > s1 } ) ; ::_thesis: P1 = P2 ` A2: P2 ` c= P1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P2 ` or x in P1 ) assume A3: x in P2 ` ; ::_thesis: x in P1 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 x in P1 by A1, A4; ::_thesis: verum end; P1 c= P2 ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P1 or x in P2 ` ) assume A5: x in P1 ; ::_thesis: x in P2 ` then ex s, r being Real st ( |[s,r]| = x & s <= s1 ) by A1; then for s2, r2 being Real holds ( not |[s2,r2]| = x or not s2 > s1 ) by SPPOL_2:1; then not x in { |[s2,r2]| where s2, r2 is Real : s2 > s1 } ; then x in the carrier of (TOP-REAL 2) \ P2 by A1, A5, XBOOLE_0:def_5; hence x in P2 ` by SUBSET_1:def_4; ::_thesis: verum end; hence P1 = P2 ` by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th12: :: GOBRD11:12 for P being Subset of (TOP-REAL 2) for s1 being Real st P = { |[r,s]| where r, s is Real : s <= s1 } holds P is closed proof let P be Subset of (TOP-REAL 2); ::_thesis: for s1 being Real st P = { |[r,s]| where r, s is Real : s <= s1 } holds P is closed let s1 be Real; ::_thesis: ( P = { |[r,s]| where r, s is Real : s <= s1 } implies P is closed ) reconsider P1 = { |[r,s]| where r, s is Real : s > s1 } as Subset of (TOP-REAL 2) by Lm4; assume P = { |[r,s]| where r, s is Real : s <= s1 } ; ::_thesis: P is closed then A1: P = P1 ` by Th8; P1 is open by JORDAN1:22; hence P is closed by A1, TOPS_1:4; ::_thesis: verum end; theorem Th13: :: GOBRD11:13 for P being Subset of (TOP-REAL 2) for s1 being Real st P = { |[r,s]| where r, s is Real : s1 <= s } holds P is closed proof let P be Subset of (TOP-REAL 2); ::_thesis: for s1 being Real st P = { |[r,s]| where r, s is Real : s1 <= s } holds P is closed let s1 be Real; ::_thesis: ( P = { |[r,s]| where r, s is Real : s1 <= s } implies P is closed ) reconsider P1 = { |[r,s]| where r, s is Real : s1 > s } as Subset of (TOP-REAL 2) by Lm6; assume P = { |[r,s]| where r, s is Real : s1 <= s } ; ::_thesis: P is closed then A1: P = P1 ` by Th9; P1 is open by JORDAN1:23; hence P is closed by A1, TOPS_1:4; ::_thesis: verum end; theorem Th14: :: GOBRD11:14 for P being Subset of (TOP-REAL 2) for s1 being Real st P = { |[s,r]| where s, r is Real : s <= s1 } holds P is closed proof let P be Subset of (TOP-REAL 2); ::_thesis: for s1 being Real st P = { |[s,r]| where s, r is Real : s <= s1 } holds P is closed let s1 be Real; ::_thesis: ( P = { |[s,r]| where s, r is Real : s <= s1 } implies P is closed ) reconsider P1 = { |[s,r]| where s, r is Real : s > s1 } as Subset of (TOP-REAL 2) by Lm10; assume P = { |[s,r]| where s, r is Real : s <= s1 } ; ::_thesis: P is closed then A1: P = P1 ` by Th11; P1 is open by JORDAN1:20; hence P is closed by A1, TOPS_1:4; ::_thesis: verum end; theorem Th15: :: GOBRD11:15 for P being Subset of (TOP-REAL 2) for s1 being Real st P = { |[s,r]| where s, r is Real : s1 <= s } holds P is closed proof let P be Subset of (TOP-REAL 2); ::_thesis: for s1 being Real st P = { |[s,r]| where s, r is Real : s1 <= s } holds P is closed let s1 be Real; ::_thesis: ( P = { |[s,r]| where s, r is Real : s1 <= s } implies P is closed ) reconsider P1 = { |[s,r]| where s, r is Real : s < s1 } as Subset of (TOP-REAL 2) by Lm8; assume P = { |[s,r]| where s, r is Real : s >= s1 } ; ::_thesis: P is closed then A1: P = P1 ` by Th10; P1 is open by JORDAN1:21; hence P is closed by A1, TOPS_1:4; ::_thesis: verum end; theorem Th16: :: GOBRD11:16 for j being Element of NAT for G being Matrix of (TOP-REAL 2) holds h_strip (G,j) is closed proof let j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) holds h_strip (G,j) is closed let G be Matrix of (TOP-REAL 2); ::_thesis: h_strip (G,j) is closed now__::_thesis:_(_(_j_<_1_&_h_strip_(G,j)_is_closed_)_or_(_1_<=_j_&_j_<_width_G_&_h_strip_(G,j)_is_closed_)_or_(_j_>=_width_G_&_h_strip_(G,j)_is_closed_)_) percases ( j < 1 or ( 1 <= j & j < width G ) or j >= width G ) ; caseA1: j < 1 ; ::_thesis: h_strip (G,j) is closed A2: now__::_thesis:_(_j_>=_width_G_implies_h_strip_(G,j)_is_closed_) assume j >= width G ; ::_thesis: h_strip (G,j) is closed then h_strip (G,j) = { |[r,s]| where r, s is Real : (G * (1,j)) `2 <= s } by GOBOARD5:def_2; hence h_strip (G,j) is closed by Th13; ::_thesis: verum end; now__::_thesis:_(_j_<_width_G_implies_h_strip_(G,j)_is_closed_) assume j < width G ; ::_thesis: h_strip (G,j) is closed then h_strip (G,j) = { |[r,s]| where r, s is Real : s <= (G * (1,(j + 1))) `2 } by A1, GOBOARD5:def_2; hence h_strip (G,j) is closed by Th12; ::_thesis: verum end; hence h_strip (G,j) is closed by A2; ::_thesis: verum end; case ( 1 <= j & j < width G ) ; ::_thesis: h_strip (G,j) is closed then A3: h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by GOBOARD5:def_2; reconsider P2 = { |[r1,s1]| where r1, s1 is Real : s1 <= (G * (1,(j + 1))) `2 } as Subset of (TOP-REAL 2) by Lm5; reconsider P1 = { |[r1,s1]| where r1, s1 is Real : (G * (1,j)) `2 <= s1 } as Subset of (TOP-REAL 2) by Lm3; A4: { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } = { |[r1,s1]| where r1, s1 is Real : (G * (1,j)) `2 <= s1 } /\ { |[r2,s2]| where r2, s2 is Real : s2 <= (G * (1,(j + 1))) `2 } proof A5: { |[r1,s1]| where r1, s1 is Real : (G * (1,j)) `2 <= s1 } /\ { |[r2,s2]| where r2, s2 is Real : s2 <= (G * (1,(j + 1))) `2 } c= { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r1,s1]| where r1, s1 is Real : (G * (1,j)) `2 <= s1 } /\ { |[r2,s2]| where r2, s2 is Real : s2 <= (G * (1,(j + 1))) `2 } or x in { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } ) assume A6: x in { |[r1,s1]| where r1, s1 is Real : (G * (1,j)) `2 <= s1 } /\ { |[r2,s2]| where r2, s2 is Real : s2 <= (G * (1,(j + 1))) `2 } ; ::_thesis: x in { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } then A7: x in { |[r1,s1]| where r1, s1 is Real : (G * (1,j)) `2 <= s1 } by XBOOLE_0:def_4; x in { |[r2,s2]| where r2, s2 is Real : s2 <= (G * (1,(j + 1))) `2 } by A6, XBOOLE_0:def_4; then consider r2, s2 being Real such that A8: |[r2,s2]| = x and A9: s2 <= (G * (1,(j + 1))) `2 ; consider r1, s1 being Real such that A10: |[r1,s1]| = x and A11: (G * (1,j)) `2 <= s1 by A7; s1 = s2 by A10, A8, SPPOL_2:1; hence x in { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by A10, A11, A9; ::_thesis: verum end; A12: { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } c= { |[r1,s1]| where r1, s1 is Real : (G * (1,j)) `2 <= s1 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } or x in { |[r1,s1]| where r1, s1 is Real : (G * (1,j)) `2 <= s1 } ) assume x in { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } ; ::_thesis: x in { |[r1,s1]| where r1, s1 is Real : (G * (1,j)) `2 <= s1 } then ex r, s being Real st ( x = |[r,s]| & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) ; hence x in { |[r1,s1]| where r1, s1 is Real : (G * (1,j)) `2 <= s1 } ; ::_thesis: verum end; { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } c= { |[r1,s1]| where r1, s1 is Real : s1 <= (G * (1,(j + 1))) `2 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } or x in { |[r1,s1]| where r1, s1 is Real : s1 <= (G * (1,(j + 1))) `2 } ) assume x in { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } ; ::_thesis: x in { |[r1,s1]| where r1, s1 is Real : s1 <= (G * (1,(j + 1))) `2 } then ex r, s being Real st ( x = |[r,s]| & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) ; hence x in { |[r1,s1]| where r1, s1 is Real : s1 <= (G * (1,(j + 1))) `2 } ; ::_thesis: verum end; then { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } c= { |[r1,s1]| where r1, s1 is Real : (G * (1,j)) `2 <= s1 } /\ { |[r2,s2]| where r2, s2 is Real : s2 <= (G * (1,(j + 1))) `2 } by A12, XBOOLE_1:19; hence { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } = { |[r1,s1]| where r1, s1 is Real : (G * (1,j)) `2 <= s1 } /\ { |[r2,s2]| where r2, s2 is Real : s2 <= (G * (1,(j + 1))) `2 } by A5, XBOOLE_0:def_10; ::_thesis: verum end; ( P1 is closed & P2 is closed ) by Th12, Th13; hence h_strip (G,j) is closed by A3, A4, TOPS_1:8; ::_thesis: verum end; case j >= width G ; ::_thesis: h_strip (G,j) is closed then h_strip (G,j) = { |[r,s]| where r, s is Real : (G * (1,j)) `2 <= s } by GOBOARD5:def_2; hence h_strip (G,j) is closed by Th13; ::_thesis: verum end; end; end; hence h_strip (G,j) is closed ; ::_thesis: verum end; theorem Th17: :: GOBRD11:17 for j being Element of NAT for G being Matrix of (TOP-REAL 2) holds v_strip (G,j) is closed proof let j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) holds v_strip (G,j) is closed let G be Matrix of (TOP-REAL 2); ::_thesis: v_strip (G,j) is closed now__::_thesis:_(_(_j_<_1_&_v_strip_(G,j)_is_closed_)_or_(_1_<=_j_&_j_<_len_G_&_v_strip_(G,j)_is_closed_)_or_(_j_>=_len_G_&_v_strip_(G,j)_is_closed_)_) percases ( j < 1 or ( 1 <= j & j < len G ) or j >= len G ) ; caseA1: j < 1 ; ::_thesis: v_strip (G,j) is closed A2: now__::_thesis:_(_j_>=_len_G_implies_v_strip_(G,j)_is_closed_) assume j >= len G ; ::_thesis: v_strip (G,j) is closed then v_strip (G,j) = { |[s,r]| where s, r is Real : (G * (j,1)) `1 <= s } by GOBOARD5:def_1; hence v_strip (G,j) is closed by Th15; ::_thesis: verum end; now__::_thesis:_(_j_<_len_G_implies_v_strip_(G,j)_is_closed_) assume j < len G ; ::_thesis: v_strip (G,j) is closed then v_strip (G,j) = { |[s,r]| where s, r is Real : s <= (G * ((j + 1),1)) `1 } by A1, GOBOARD5:def_1; hence v_strip (G,j) is closed by Th14; ::_thesis: verum end; hence v_strip (G,j) is closed by A2; ::_thesis: verum end; case ( 1 <= j & j < len G ) ; ::_thesis: v_strip (G,j) is closed then A3: v_strip (G,j) = { |[s,r]| where s, r is Real : ( (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) } by GOBOARD5:def_1; reconsider P2 = { |[s1,r1]| where s1, r1 is Real : s1 <= (G * ((j + 1),1)) `1 } as Subset of (TOP-REAL 2) by Lm7; reconsider P1 = { |[s1,r1]| where s1, r1 is Real : (G * (j,1)) `1 <= s1 } as Subset of (TOP-REAL 2) by Lm9; A4: { |[s,r]| where s, r is Real : ( (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) } = { |[s1,r1]| where s1, r1 is Real : (G * (j,1)) `1 <= s1 } /\ { |[s2,r2]| where s2, r2 is Real : s2 <= (G * ((j + 1),1)) `1 } proof A5: { |[s1,r1]| where s1, r1 is Real : (G * (j,1)) `1 <= s1 } /\ { |[s2,r2]| where s2, r2 is Real : s2 <= (G * ((j + 1),1)) `1 } c= { |[s,r]| where s, r is Real : ( (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[s1,r1]| where s1, r1 is Real : (G * (j,1)) `1 <= s1 } /\ { |[s2,r2]| where s2, r2 is Real : s2 <= (G * ((j + 1),1)) `1 } or x in { |[s,r]| where s, r is Real : ( (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) } ) assume A6: x in { |[s1,r1]| where s1, r1 is Real : (G * (j,1)) `1 <= s1 } /\ { |[s2,r2]| where s2, r2 is Real : s2 <= (G * ((j + 1),1)) `1 } ; ::_thesis: x in { |[s,r]| where s, r is Real : ( (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) } then A7: x in { |[s2,r2]| where s2, r2 is Real : s2 <= (G * ((j + 1),1)) `1 } by XBOOLE_0:def_4; x in { |[s1,r1]| where s1, r1 is Real : (G * (j,1)) `1 <= s1 } by A6, XBOOLE_0:def_4; then ex s1, r1 being Real st ( |[s1,r1]| = x & (G * (j,1)) `1 <= s1 ) ; then consider r1, s1 being Real such that A8: |[s1,r1]| = x and A9: (G * (j,1)) `1 <= s1 ; consider s2, r2 being Real 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 x in { |[s,r]| where s, r is Real : ( (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) } by A8, A9, A11; ::_thesis: verum end; A12: { |[s,r]| where s, r is Real : ( (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) } c= { |[s1,r1]| where s1, r1 is Real : (G * (j,1)) `1 <= s1 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[s,r]| where s, r is Real : ( (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) } or x in { |[s1,r1]| where s1, r1 is Real : (G * (j,1)) `1 <= s1 } ) assume x in { |[s,r]| where s, r is Real : ( (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) } ; ::_thesis: x in { |[s1,r1]| where s1, r1 is Real : (G * (j,1)) `1 <= s1 } then ex s, r being Real st ( x = |[s,r]| & (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) ; hence x in { |[s1,r1]| where s1, r1 is Real : (G * (j,1)) `1 <= s1 } ; ::_thesis: verum end; { |[s,r]| where s, r is Real : ( (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) } c= { |[s1,r1]| where s1, r1 is Real : s1 <= (G * ((j + 1),1)) `1 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[s,r]| where s, r is Real : ( (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) } or x in { |[s1,r1]| where s1, r1 is Real : s1 <= (G * ((j + 1),1)) `1 } ) assume x in { |[s,r]| where s, r is Real : ( (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) } ; ::_thesis: x in { |[s1,r1]| where s1, r1 is Real : s1 <= (G * ((j + 1),1)) `1 } then ex s, r being Real st ( x = |[s,r]| & (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) ; hence x in { |[s1,r1]| where s1, r1 is Real : s1 <= (G * ((j + 1),1)) `1 } ; ::_thesis: verum end; then { |[s,r]| where s, r is Real : ( (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) } c= { |[s1,r1]| where s1, r1 is Real : (G * (j,1)) `1 <= s1 } /\ { |[s2,r2]| where s2, r2 is Real : s2 <= (G * ((j + 1),1)) `1 } by A12, XBOOLE_1:19; hence { |[s,r]| where s, r is Real : ( (G * (j,1)) `1 <= s & s <= (G * ((j + 1),1)) `1 ) } = { |[s1,r1]| where s1, r1 is Real : (G * (j,1)) `1 <= s1 } /\ { |[s2,r2]| where s2, r2 is Real : s2 <= (G * ((j + 1),1)) `1 } by A5, XBOOLE_0:def_10; ::_thesis: verum end; ( P1 is closed & P2 is closed ) by Th14, Th15; hence v_strip (G,j) is closed by A3, A4, TOPS_1:8; ::_thesis: verum end; case j >= len G ; ::_thesis: v_strip (G,j) is closed then v_strip (G,j) = { |[s,r]| where s, r is Real : (G * (j,1)) `1 <= s } by GOBOARD5:def_1; hence v_strip (G,j) is closed by Th15; ::_thesis: verum end; end; end; hence v_strip (G,j) is closed ; ::_thesis: verum end; theorem Th18: :: GOBRD11:18 for G being V21() Matrix of (TOP-REAL 2) st G is X_equal-in-line holds v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,1)) `1 } proof let G be V21() Matrix of (TOP-REAL 2); ::_thesis: ( G is X_equal-in-line implies v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,1)) `1 } ) 0 <> width G by GOBOARD1:def_3; then A1: 1 <= width G by NAT_1:14; assume G is X_equal-in-line ; ::_thesis: v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,1)) `1 } hence v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,1)) `1 } by A1, GOBOARD5:10; ::_thesis: verum end; theorem Th19: :: GOBRD11:19 for G being V21() Matrix of (TOP-REAL 2) st G is X_equal-in-line holds v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r } proof let G be V21() Matrix of (TOP-REAL 2); ::_thesis: ( G is X_equal-in-line implies v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r } ) 0 <> width G by GOBOARD1:def_3; then A1: 1 <= width G by NAT_1:14; assume G is X_equal-in-line ; ::_thesis: v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r } hence v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r } by A1, GOBOARD5:9; ::_thesis: verum end; theorem Th20: :: GOBRD11:20 for i being Element of NAT for G being V21() Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= i & i < len G holds v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } proof let i be Element of NAT ; ::_thesis: for G being V21() Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= i & i < len G holds v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } let G be V21() Matrix of (TOP-REAL 2); ::_thesis: ( G is X_equal-in-line & 1 <= i & i < len G implies v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } ) assume A1: G is X_equal-in-line ; ::_thesis: ( not 1 <= i or not i < len G or v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } ) 0 <> width G by GOBOARD1:def_3; then A2: 1 <= width G by NAT_1:14; assume ( 1 <= i & i < len G ) ; ::_thesis: v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } hence v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } by A1, A2, GOBOARD5:8; ::_thesis: verum end; theorem Th21: :: GOBRD11:21 for G being V21() Matrix of (TOP-REAL 2) st G is Y_equal-in-column holds h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (1,1)) `2 } proof let G be V21() Matrix of (TOP-REAL 2); ::_thesis: ( G is Y_equal-in-column implies h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (1,1)) `2 } ) 0 <> len G by GOBOARD1:def_3; then A1: 1 <= len G by NAT_1:14; assume G is Y_equal-in-column ; ::_thesis: h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (1,1)) `2 } hence h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (1,1)) `2 } by A1, GOBOARD5:7; ::_thesis: verum end; theorem Th22: :: GOBRD11:22 for G being V21() Matrix of (TOP-REAL 2) st G is Y_equal-in-column holds h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s } proof let G be V21() Matrix of (TOP-REAL 2); ::_thesis: ( G is Y_equal-in-column implies h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s } ) 0 <> len G by GOBOARD1:def_3; then A1: 1 <= len G by NAT_1:14; assume G is Y_equal-in-column ; ::_thesis: h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s } hence h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s } by A1, GOBOARD5:6; ::_thesis: verum end; theorem Th23: :: GOBRD11:23 for j being Element of NAT for G being V21() Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j < width G holds h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } proof let j be Element of NAT ; ::_thesis: for G being V21() Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j < width G holds h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } let G be V21() Matrix of (TOP-REAL 2); ::_thesis: ( G is Y_equal-in-column & 1 <= j & j < width G implies h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } ) assume A1: G is Y_equal-in-column ; ::_thesis: ( not 1 <= j or not j < width G or h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } ) 0 <> len G by GOBOARD1:def_3; then A2: 1 <= len G by NAT_1:14; assume ( 1 <= j & j < width G ) ; ::_thesis: h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } hence h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by A1, A2, GOBOARD5:5; ::_thesis: verum end; theorem Th24: :: GOBRD11:24 for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) holds cell (G,0,0) = { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & s <= (G * (1,1)) `2 ) } proof let G be V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2); ::_thesis: cell (G,0,0) = { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & s <= (G * (1,1)) `2 ) } A1: cell (G,0,0) = (v_strip (G,0)) /\ (h_strip (G,0)) by GOBOARD5:def_3; A2: h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (1,1)) `2 } by Th21; A3: v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,1)) `1 } by Th18; thus cell (G,0,0) c= { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & s <= (G * (1,1)) `2 ) } :: according to XBOOLE_0:def_10 ::_thesis: { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & s <= (G * (1,1)) `2 ) } c= cell (G,0,0) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cell (G,0,0) or x in { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & s <= (G * (1,1)) `2 ) } ) assume A4: x in cell (G,0,0) ; ::_thesis: x in { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & s <= (G * (1,1)) `2 ) } then x in v_strip (G,0) by A1, XBOOLE_0:def_4; then consider r1, s1 being Real 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 being Real such that A7: x = |[r2,s2]| and A8: s2 <= (G * (1,1)) `2 by A2; s1 = s2 by A5, A7, SPPOL_2:1; hence x in { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & s <= (G * (1,1)) `2 ) } by A5, A6, A8; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & s <= (G * (1,1)) `2 ) } or x in cell (G,0,0) ) assume x in { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & s <= (G * (1,1)) `2 ) } ; ::_thesis: x in cell (G,0,0) then A9: ex r, s being Real 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 x in cell (G,0,0) by A1, A10, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th25: :: GOBRD11:25 for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) holds cell (G,0,(width G)) = { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= s ) } proof let G be V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2); ::_thesis: cell (G,0,(width G)) = { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= s ) } 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]| where r, s is Real : (G * (1,(width G))) `2 <= s } by Th22; A3: v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,1)) `1 } by Th18; thus cell (G,0,(width G)) c= { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= s ) } :: according to XBOOLE_0:def_10 ::_thesis: { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= s ) } c= cell (G,0,(width G)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cell (G,0,(width G)) or x in { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= s ) } ) assume A4: x in cell (G,0,(width G)) ; ::_thesis: x in { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= s ) } then x in v_strip (G,0) by A1, XBOOLE_0:def_4; then consider r1, s1 being Real 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 being Real 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 x in { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= s ) } by A5, A6, A8; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= s ) } or x in cell (G,0,(width G)) ) assume x in { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= s ) } ; ::_thesis: x in cell (G,0,(width G)) then A9: ex r, s being Real 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 x in cell (G,0,(width G)) by A1, A10, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th26: :: GOBRD11:26 for j being Element of NAT for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= j & j < width G holds cell (G,0,j) = { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } proof let j be Element of NAT ; ::_thesis: for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= j & j < width G holds cell (G,0,j) = { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } let G be V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2); ::_thesis: ( 1 <= j & j < width G implies cell (G,0,j) = { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } ) A1: cell (G,0,j) = (v_strip (G,0)) /\ (h_strip (G,j)) by GOBOARD5:def_3; assume ( 1 <= j & j < width G ) ; ::_thesis: cell (G,0,j) = { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } then A2: h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by Th23; A3: v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,1)) `1 } by Th18; thus cell (G,0,j) c= { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } :: according to XBOOLE_0:def_10 ::_thesis: { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } c= cell (G,0,j) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cell (G,0,j) or x in { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } ) assume A4: x in cell (G,0,j) ; ::_thesis: x in { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } then x in v_strip (G,0) by A1, XBOOLE_0:def_4; then consider r1, s1 being Real 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 being Real 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 x in { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by A5, A6, A8; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } or x in cell (G,0,j) ) assume x in { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } ; ::_thesis: x in cell (G,0,j) then A9: ex r, s being Real 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 x in cell (G,0,j) by A1, A10, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th27: :: GOBRD11:27 for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) holds cell (G,(len G),0) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & s <= (G * (1,1)) `2 ) } proof let G be V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2); ::_thesis: cell (G,(len G),0) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & s <= (G * (1,1)) `2 ) } 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]| where r, s is Real : s <= (G * (1,1)) `2 } by Th21; A3: v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r } by Th19; thus cell (G,(len G),0) c= { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & s <= (G * (1,1)) `2 ) } :: according to XBOOLE_0:def_10 ::_thesis: { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & s <= (G * (1,1)) `2 ) } c= cell (G,(len G),0) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cell (G,(len G),0) or x in { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & s <= (G * (1,1)) `2 ) } ) assume A4: x in cell (G,(len G),0) ; ::_thesis: x in { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & s <= (G * (1,1)) `2 ) } then x in v_strip (G,(len G)) by A1, XBOOLE_0:def_4; then consider r1, s1 being Real 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 being Real such that A7: x = |[r2,s2]| and A8: s2 <= (G * (1,1)) `2 by A2; s1 = s2 by A5, A7, SPPOL_2:1; hence x in { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & s <= (G * (1,1)) `2 ) } by A5, A6, A8; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & s <= (G * (1,1)) `2 ) } or x in cell (G,(len G),0) ) assume x in { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & s <= (G * (1,1)) `2 ) } ; ::_thesis: x in cell (G,(len G),0) then A9: ex r, s being Real 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 x in cell (G,(len G),0) by A1, A10, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th28: :: GOBRD11:28 for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) holds cell (G,(len G),(width G)) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,(width G))) `2 <= s ) } proof let G be V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2); ::_thesis: cell (G,(len G),(width G)) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,(width G))) `2 <= s ) } 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]| where r, s is Real : (G * (1,(width G))) `2 <= s } by Th22; A3: v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r } by Th19; thus cell (G,(len G),(width G)) c= { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,(width G))) `2 <= s ) } :: according to XBOOLE_0:def_10 ::_thesis: { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,(width G))) `2 <= s ) } c= cell (G,(len G),(width G)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cell (G,(len G),(width G)) or x in { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,(width G))) `2 <= s ) } ) assume A4: x in cell (G,(len G),(width G)) ; ::_thesis: x in { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,(width G))) `2 <= s ) } then x in v_strip (G,(len G)) by A1, XBOOLE_0:def_4; then consider r1, s1 being Real 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 being Real 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 x in { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,(width G))) `2 <= s ) } by A5, A6, A8; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,(width G))) `2 <= s ) } or x in cell (G,(len G),(width G)) ) assume x in { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,(width G))) `2 <= s ) } ; ::_thesis: x in cell (G,(len G),(width G)) then A9: ex r, s being Real 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 x in cell (G,(len G),(width G)) by A1, A10, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th29: :: GOBRD11:29 for j being Element of NAT for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= j & j < width G holds cell (G,(len G),j) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } proof let j be Element of NAT ; ::_thesis: for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= j & j < width G holds cell (G,(len G),j) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } let G be V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2); ::_thesis: ( 1 <= j & j < width G implies cell (G,(len G),j) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } ) 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 ) ; ::_thesis: cell (G,(len G),j) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } then A2: h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by Th23; A3: v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r } by Th19; thus cell (G,(len G),j) c= { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } :: according to XBOOLE_0:def_10 ::_thesis: { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } c= cell (G,(len G),j) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cell (G,(len G),j) or x in { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } ) assume A4: x in cell (G,(len G),j) ; ::_thesis: x in { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } then x in v_strip (G,(len G)) by A1, XBOOLE_0:def_4; then consider r1, s1 being Real 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 being Real 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 x in { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by A5, A6, A8; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } or x in cell (G,(len G),j) ) assume x in { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } ; ::_thesis: x in cell (G,(len G),j) then A9: ex r, s being Real 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 x in cell (G,(len G),j) by A1, A10, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th30: :: GOBRD11:30 for i being Element of NAT for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= i & i < len G holds cell (G,i,0) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & s <= (G * (1,1)) `2 ) } proof let i be Element of NAT ; ::_thesis: for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= i & i < len G holds cell (G,i,0) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & s <= (G * (1,1)) `2 ) } let G be V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2); ::_thesis: ( 1 <= i & i < len G implies cell (G,i,0) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & s <= (G * (1,1)) `2 ) } ) A1: cell (G,i,0) = (v_strip (G,i)) /\ (h_strip (G,0)) by GOBOARD5:def_3; assume ( 1 <= i & i < len G ) ; ::_thesis: cell (G,i,0) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & s <= (G * (1,1)) `2 ) } then A2: v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } by Th20; A3: h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (1,1)) `2 } by Th21; thus cell (G,i,0) c= { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & s <= (G * (1,1)) `2 ) } :: according to XBOOLE_0:def_10 ::_thesis: { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & s <= (G * (1,1)) `2 ) } c= cell (G,i,0) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cell (G,i,0) or x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & s <= (G * (1,1)) `2 ) } ) assume A4: x in cell (G,i,0) ; ::_thesis: x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & s <= (G * (1,1)) `2 ) } then x in v_strip (G,i) by A1, XBOOLE_0:def_4; then consider r1, s1 being Real 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 being Real such that A7: x = |[r2,s2]| and A8: s2 <= (G * (1,1)) `2 by A3; s1 = s2 by A5, A7, SPPOL_2:1; hence x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & s <= (G * (1,1)) `2 ) } by A5, A6, A8; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & s <= (G * (1,1)) `2 ) } or x in cell (G,i,0) ) assume x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & s <= (G * (1,1)) `2 ) } ; ::_thesis: x in cell (G,i,0) then A9: ex r, s being Real 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 x in cell (G,i,0) by A1, A10, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th31: :: GOBRD11:31 for i being Element of NAT for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= i & i < len G holds cell (G,i,(width G)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 <= s ) } proof let i be Element of NAT ; ::_thesis: for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= i & i < len G holds cell (G,i,(width G)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 <= s ) } let G be V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2); ::_thesis: ( 1 <= i & i < len G implies cell (G,i,(width G)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 <= s ) } ) 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 ) ; ::_thesis: cell (G,i,(width G)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 <= s ) } then A2: v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } by Th20; A3: h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s } by Th22; thus cell (G,i,(width G)) c= { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 <= s ) } :: according to XBOOLE_0:def_10 ::_thesis: { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 <= s ) } c= cell (G,i,(width G)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cell (G,i,(width G)) or x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 <= s ) } ) assume A4: x in cell (G,i,(width G)) ; ::_thesis: x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 <= s ) } then x in v_strip (G,i) by A1, XBOOLE_0:def_4; then consider r1, s1 being Real 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 being Real 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 x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 <= s ) } by A5, A6, A8; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 <= s ) } or x in cell (G,i,(width G)) ) assume x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 <= s ) } ; ::_thesis: x in cell (G,i,(width G)) then A9: ex r, s being Real 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 x in cell (G,i,(width G)) by A1, A10, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th32: :: GOBRD11:32 for i, j being Element of NAT for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= i & i < len G & 1 <= j & j < width G holds cell (G,i,j) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } proof let i, j be Element of NAT ; ::_thesis: for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= i & i < len G & 1 <= j & j < width G holds cell (G,i,j) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } let G be V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2); ::_thesis: ( 1 <= i & i < len G & 1 <= j & j < width G implies cell (G,i,j) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } ) assume that A1: ( 1 <= i & i < len G ) and A2: ( 1 <= j & j < width G ) ; ::_thesis: cell (G,i,j) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } A3: h_strip (G,j) = { |[r,s]| where r, s is Real : ( (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]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } by A1, Th20; thus cell (G,i,j) c= { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } :: according to XBOOLE_0:def_10 ::_thesis: { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } c= cell (G,i,j) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cell (G,i,j) or x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } ) assume A6: x in cell (G,i,j) ; ::_thesis: x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } then x in v_strip (G,i) by A4, XBOOLE_0:def_4; then consider r1, s1 being Real 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 being Real 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 x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by A7, A8, A10; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } or x in cell (G,i,j) ) assume x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } ; ::_thesis: x in cell (G,i,j) then A11: ex r, s being Real 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 x in cell (G,i,j) by A4, A12, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th33: :: GOBRD11:33 for i, j being Element of NAT for G being Matrix of (TOP-REAL 2) holds cell (G,i,j) is closed proof let i, j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) holds cell (G,i,j) is closed let G be Matrix of (TOP-REAL 2); ::_thesis: cell (G,i,j) is closed 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 cell (G,i,j) is closed by A1, TOPS_1:8; ::_thesis: verum end; theorem Th34: :: GOBRD11:34 for G being V21() Matrix of (TOP-REAL 2) holds ( 1 <= len G & 1 <= width G ) proof let G be V21() Matrix of (TOP-REAL 2); ::_thesis: ( 1 <= len G & 1 <= width G ) ( not len G = 0 & not width G = 0 ) by GOBOARD1:def_3; hence ( 1 <= len G & 1 <= width G ) by NAT_1:14; ::_thesis: verum end; theorem :: GOBRD11:35 for i, j being Element of NAT for G being Go-board st i <= len G & j <= width G holds cell (G,i,j) = Cl (Int (cell (G,i,j))) proof let i, j be Element of NAT ; ::_thesis: for G being Go-board st i <= len G & j <= width G holds cell (G,i,j) = Cl (Int (cell (G,i,j))) let G be Go-board; ::_thesis: ( i <= len G & j <= width G implies cell (G,i,j) = Cl (Int (cell (G,i,j))) ) set Y = Int (cell (G,i,j)); assume A1: ( i <= len G & j <= width G ) ; ::_thesis: cell (G,i,j) = Cl (Int (cell (G,i,j))) A2: cell (G,i,j) c= Cl (Int (cell (G,i,j))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cell (G,i,j) or x in Cl (Int (cell (G,i,j))) ) assume A3: x in cell (G,i,j) ; ::_thesis: x in Cl (Int (cell (G,i,j))) then reconsider p = x as Point of (TOP-REAL 2) ; for G0 being Subset of (TOP-REAL 2) st G0 is open & p in G0 holds Int (cell (G,i,j)) meets G0 proof let G0 be Subset of (TOP-REAL 2); ::_thesis: ( G0 is open & p in G0 implies Int (cell (G,i,j)) meets G0 ) assume A4: G0 is open ; ::_thesis: ( not p in G0 or Int (cell (G,i,j)) meets G0 ) now__::_thesis:_(_p_in_G0_implies_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_) reconsider u = p as Point of (Euclid 2) by EUCLID:22; assume A5: p in G0 ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) j >= 0 by NAT_1:2; then A6: ( j = 0 or 0 + 1 <= j ) by NAT_1:13; reconsider v = u as Element of REAL 2 ; A7: TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2), the topology 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 being real number such that A8: r > 0 and A9: Ball (u,r) c= G00 by A5, TOPMETR:15; reconsider r = r as Real by XREAL_0:def_1; i >= 0 by NAT_1:2; then A10: ( i = 0 or 0 + 1 <= i ) by NAT_1:13; now__::_thesis:_(_(_i_=_0_&_j_=_0_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_i_=_0_&_j_=_width_G_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_i_=_0_&_1_<=_j_&_j_<_width_G_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_i_=_len_G_&_j_=_0_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_)_or_(_i_=_len_G_&_j_=_width_G_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_)_or_(_i_=_len_G_&_1_<=_j_&_j_<_width_G_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_1_<=_i_&_i_<_len_G_&_j_=_0_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_1_<=_i_&_i_<_len_G_&_j_=_width_G_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_1_<=_i_&_i_<_len_G_&_1_<=_j_&_j_<_width_G_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_) percases ( ( i = 0 & j = 0 ) or ( i = 0 & j = width G ) or ( i = 0 & 1 <= j & j < width G ) or ( i = len G & j = 0 ) or ( i = len G & j = width G ) or ( i = len G & 1 <= j & j < width G ) or ( 1 <= i & i < len G & j = 0 ) or ( 1 <= i & i < len G & j = width G ) or ( 1 <= i & i < len G & 1 <= j & j < width G ) ) by A1, A10, A6, XXREAL_0:1; caseA11: ( i = 0 & j = 0 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) then p in { |[r2,s2]| where r2, s2 is Real : ( r2 <= (G * (1,1)) `1 & s2 <= (G * (1,1)) `2 ) } by A3, Th24; then consider r2, s2 being Real 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); set s3 = s2 - (r / 2); A15: r * (2 ") > 0 by A8, XREAL_1:129; then s2 - (r / 2) < (s2 - (r / 2)) + (r / 2) by XREAL_1:29; then A16: s2 - (r / 2) < (G * (1,1)) `2 by A14, XXREAL_0:2; reconsider q0 = |[(r2 - (r / 2)),(s2 - (r / 2))]| as Point of (TOP-REAL 2) ; reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22; r2 - (r / 2) < (r2 - (r / 2)) + (r / 2) by A15, XREAL_1:29; then r2 - (r / 2) < (G * (1,1)) `1 by A13, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 < (G * (1,1)) `1 & s1 < (G * (1,1)) `2 ) } by A16; then A17: u0 in Int (cell (G,i,j)) by A11, GOBOARD6:18; reconsider v0 = u0 as Element of REAL 2 ; A18: ( q0 `1 = r2 - (r / 2) & q0 `2 = s2 - (r / 2) ) 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 - (r2 - (r / 2)) = r / 2 & s2 - (s2 - (r / 2)) = 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 (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A17, XBOOLE_0:def_4; ::_thesis: verum end; caseA22: ( i = 0 & j = width G ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) then p in { |[r2,s2]| where r2, s2 is Real : ( r2 <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= s2 ) } by A3, Th25; then consider r2, s2 being Real 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); set s3 = s2 + (r / 2); A26: r * (2 ") > 0 by A8, XREAL_1:129; then s2 + (r / 2) > s2 by XREAL_1:29; then A27: s2 + (r / 2) > (G * (1,(width G))) `2 by A25, XXREAL_0:2; reconsider q0 = |[(r2 - (r / 2)),(s2 + (r / 2))]| as Point of (TOP-REAL 2) ; reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22; r2 - (r / 2) < (r2 - (r / 2)) + (r / 2) by A26, XREAL_1:29; then r2 - (r / 2) < (G * (1,1)) `1 by A24, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 < (G * (1,1)) `1 & (G * (1,(width G))) `2 < s1 ) } by A27; then A28: u0 in Int (cell (G,i,j)) by A22, GOBOARD6:19; reconsider v0 = u0 as Element of REAL 2 ; A29: ( q0 `1 = r2 - (r / 2) & q0 `2 = s2 + (r / 2) ) 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 - (r2 - (r / 2))) ^2) + ((s2 - (s2 + (r / 2))) ^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 (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A28, XBOOLE_0:def_4; ::_thesis: verum end; caseA32: ( i = 0 & 1 <= j & j < width G ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) then p in { |[r2,s2]| where r2, s2 is Real : ( r2 <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s2 & s2 <= (G * (1,(j + 1))) `2 ) } by A3, Th26; then consider r2, s2 being Real 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__::_thesis:_(_(_s2_=_(G_*_(1,j))_`2_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_(G_*_(1,j))_`2_<_s2_&_s2_<_(G_*_(1,(j_+_1)))_`2_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_)_or_(_s2_=_(G_*_(1,(j_+_1)))_`2_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_)_) percases ( s2 = (G * (1,j)) `2 or ( (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) or s2 = (G * (1,(j + 1))) `2 ) by A35, A36, XXREAL_0:1; caseA37: s2 = (G * (1,j)) `2 ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 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,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))); set r3 = r2 - (r / 2); set s3 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2); set q0 = |[(r2 - (r / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]|; A41: ( |[(r2 - (r / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| `1 = r2 - (r / 2) & |[(r2 - (r / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| `2 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) by EUCLID:52; reconsider u0 = |[(r2 - (r / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| 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: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50; then A44: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21; then s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > s2 by XREAL_1:29, XREAL_1:139; then A45: s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A35, XXREAL_0:2; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A44, SQUARE_1:15; then A46: ((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7; ( 0 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63; then sqrt (((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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 - (r2 - (r / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^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; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17; then A48: ((G * (1,j)) `2) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) <= ((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by XREAL_1:6; r * (2 ") > 0 by A8, XREAL_1:129; then r2 - (r / 2) < (r2 - (r / 2)) + (r / 2) by XREAL_1:29; then A49: r2 - (r / 2) < (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 s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A37, A48, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 < (G * (1,1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A49, A45; then u0 in Int (cell (G,i,j)) by A32, GOBOARD6:20; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A47, XBOOLE_0:def_4; ::_thesis: verum end; caseA50: ( (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} set r3 = r2 - (r / 2); set s3 = s2; reconsider q0 = |[(r2 - (r / 2)),s2]| 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 - (r / 2) < (r2 - (r / 2)) + (r / 2) by XREAL_1:29; then r2 - (r / 2) < (G * (1,1)) `1 by A34, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 < (G * (1,1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A50; then A51: u0 in Int (cell (G,i,j)) by A32, GOBOARD6:20; reconsider v0 = u0 as Element of REAL 2 ; A52: ( q0 `1 = r2 - (r / 2) & q0 `2 = s2 ) 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 - (r2 - (r / 2))) ^2) + ((s2 - s2) ^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 (Int (cell (G,i,j))) /\ G0 <> {} by A9, A51, XBOOLE_0:def_4; ::_thesis: verum end; caseA57: s2 = (G * (1,(j + 1))) `2 ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} 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,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))); set r3 = r2 - (r / 2); set s3 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2); reconsider q0 = |[(r2 - (r / 2)),(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ; A61: ( q0 `1 = r2 - (r / 2) & q0 `2 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) 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: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50; then A64: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21; then s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) by XREAL_1:29, XREAL_1:139; then A65: s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A36, XXREAL_0:2; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A64, SQUARE_1:15; then A66: ((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7; ( 0 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63; then sqrt (((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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 - (r2 - (r / 2))) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^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; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17; then A68: ((G * (1,(j + 1))) `2) - ((min (r,(((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) by XREAL_1:10; r * (2 ") > 0 by A8, XREAL_1:129; then r2 - (r / 2) < (r2 - (r / 2)) + (r / 2) by XREAL_1:29; then A69: r2 - (r / 2) < (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 s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A57, A68, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 < (G * (1,1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A69, A65; then u0 in Int (cell (G,i,j)) by A32, GOBOARD6:20; hence (Int (cell (G,i,j))) /\ G0 <> {} by A9, A67, XBOOLE_0:def_4; ::_thesis: verum end; end; end; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ; ::_thesis: verum end; caseA70: ( i = len G & j = 0 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} then p in { |[r2,s2]| where r2, s2 is Real : ( r2 >= (G * ((len G),1)) `1 & (G * (1,1)) `2 >= s2 ) } by A3, Th27; then consider r2, s2 being Real 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); set s3 = s2 - (r / 2); A74: r * (2 ") > 0 by A8, XREAL_1:129; then r2 + (r / 2) > r2 by XREAL_1:29; then A75: r2 + (r / 2) > (G * ((len G),1)) `1 by A72, XXREAL_0:2; reconsider q0 = |[(r2 + (r / 2)),(s2 - (r / 2))]| as Point of (TOP-REAL 2) ; reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22; s2 - (r / 2) < (s2 - (r / 2)) + (r / 2) by A74, XREAL_1:29; then s2 - (r / 2) < (G * (1,1)) `2 by A73, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 > (G * ((len G),1)) `1 & (G * (1,1)) `2 > s1 ) } by A75; then A76: u0 in Int (cell (G,i,j)) by A70, GOBOARD6:21; reconsider v0 = u0 as Element of REAL 2 ; A77: ( q0 `1 = r2 + (r / 2) & q0 `2 = s2 - (r / 2) ) 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 - (r2 + (r / 2))) ^2) + ((s2 - (s2 - (r / 2))) ^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 (Int (cell (G,i,j))) /\ G0 <> {} by A9, A76, XBOOLE_0:def_4; ::_thesis: verum end; caseA80: ( i = len G & j = width G ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (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]| where r2, s2 is Real : ( (G * ((len G),1)) `1 <= r2 & (G * (1,(width G))) `2 <= s2 ) } by A3, A80, Th28; then consider r2, s2 being Real 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); set s3 = s2 + (r / 2); A86: r * (2 ") > 0 by A8, XREAL_1:129; then s2 < s2 + (r / 2) by XREAL_1:29; then A87: s2 + (r / 2) > (G * (1,(width G))) `2 by A85, XXREAL_0:2; reconsider q0 = |[(r2 + (r / 2)),(s2 + (r / 2))]| 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 r2 + (r / 2) > (G * ((len G),1)) `1 by A84, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 > (G * ((len G),1)) `1 & s1 > (G * (1,(width G))) `2 ) } by A87; then A88: u0 in Int (cell (G,i,j)) by A80, GOBOARD6:22; reconsider v0 = u0 as Element of REAL 2 ; A89: ( q0 `1 = r2 + (r / 2) & q0 `2 = s2 + (r / 2) ) 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 - (r2 + (r / 2)) = - (r / 2) & s2 - (s2 + (r / 2)) = - (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 (Int (cell (G,i,j))) /\ G0 <> {} by A9, A88, XBOOLE_0:def_4; ::_thesis: verum end; caseA92: ( i = len G & 1 <= j & j < width G ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) then p in { |[r2,s2]| where r2, s2 is Real : ( r2 >= (G * ((len G),1)) `1 & (G * (1,j)) `2 <= s2 & s2 <= (G * (1,(j + 1))) `2 ) } by A3, Th29; then consider r2, s2 being Real 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__::_thesis:_(_(_s2_=_(G_*_(1,j))_`2_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_)_or_(_(G_*_(1,j))_`2_<_s2_&_s2_<_(G_*_(1,(j_+_1)))_`2_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_)_or_(_s2_=_(G_*_(1,(j_+_1)))_`2_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_) percases ( s2 = (G * (1,j)) `2 or ( (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) or s2 = (G * (1,(j + 1))) `2 ) by A95, A96, XXREAL_0:1; caseA97: s2 = (G * (1,j)) `2 ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} 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,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))); set r3 = r2 + (r / 2); set s3 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2); reconsider q0 = |[(r2 + (r / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ; A101: ( q0 `1 = r2 + (r / 2) & q0 `2 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) 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: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50; then A104: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21; then s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > s2 by XREAL_1:29, XREAL_1:139; then A105: s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A95, XXREAL_0:2; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A104, SQUARE_1:15; then A106: ((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7; ( 0 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63; then sqrt (((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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 - (r2 + (r / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^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; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17; then A108: ((G * (1,j)) `2) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) <= ((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by XREAL_1:6; r * (2 ") > 0 by A8, XREAL_1:129; then r2 < r2 + (r / 2) by XREAL_1:29; then A109: r2 + (r / 2) > (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 s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A97, A108, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 > (G * ((len G),1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A109, A105; then u0 in Int (cell (G,i,j)) by A92, GOBOARD6:23; hence (Int (cell (G,i,j))) /\ G0 <> {} by A9, A107, XBOOLE_0:def_4; ::_thesis: verum end; caseA110: ( (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} set r3 = r2 + (r / 2); set s3 = s2; reconsider q0 = |[(r2 + (r / 2)),s2]| 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 r2 + (r / 2) > (G * ((len G),1)) `1 by A94, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 > (G * ((len G),1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A110; then A111: u0 in Int (cell (G,i,j)) by A92, GOBOARD6:23; reconsider v0 = u0 as Element of REAL 2 ; A112: ( q0 `1 = r2 + (r / 2) & q0 `2 = s2 ) 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 - (r2 + (r / 2))) ^2) + ((s2 - s2) ^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 (Int (cell (G,i,j))) /\ G0 <> {} by A9, A111, XBOOLE_0:def_4; ::_thesis: verum end; caseA117: s2 = (G * (1,(j + 1))) `2 ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 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,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))); set r3 = r2 + (r / 2); set s3 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2); reconsider q0 = |[(r2 + (r / 2)),(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ; A121: ( q0 `1 = r2 + (r / 2) & q0 `2 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) 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: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50; then A124: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21; then s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) by XREAL_1:29, XREAL_1:139; then A125: s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A96, XXREAL_0:2; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A124, SQUARE_1:15; then A126: ((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7; ( 0 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63; then sqrt (((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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 - (r2 + (r / 2))) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^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; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17; then A128: ((G * (1,(j + 1))) `2) - ((min (r,(((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) by XREAL_1:10; r * (2 ") > 0 by A8, XREAL_1:129; then r2 < r2 + (r / 2) by XREAL_1:29; then A129: r2 + (r / 2) > (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 s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A117, A128, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 > (G * ((len G),1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A129, A125; then u0 in Int (cell (G,i,j)) by A92, GOBOARD6:23; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A127, XBOOLE_0:def_4; ::_thesis: verum end; end; end; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ; ::_thesis: verum end; caseA130: ( 1 <= i & i < len G & j = 0 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) then p in { |[r2,s2]| where r2, s2 is Real : ( (G * (i,1)) `1 <= r2 & r2 <= (G * ((i + 1),1)) `1 & s2 <= (G * (1,1)) `2 ) } by A3, Th30; then consider r2, s2 being Real 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__::_thesis:_(_(_r2_=_(G_*_(i,1))_`1_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_(G_*_(i,1))_`1_<_r2_&_r2_<_(G_*_((i_+_1),1))_`1_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_r2_=_(G_*_((i_+_1),1))_`1_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_) percases ( r2 = (G * (i,1)) `1 or ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 ) or r2 = (G * ((i + 1),1)) `1 ) by A132, A133, XXREAL_0:1; caseA135: r2 = (G * (i,1)) `1 ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ((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,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))); set s3 = s2 - (r / 2); set r3 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2); reconsider q0 = |[(r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 - (r / 2))]| as Point of (TOP-REAL 2) ; A137: ( q0 `1 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 - (r / 2) ) 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: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50; then A140: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21; then r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > r2 by XREAL_1:29, XREAL_1:139; then A141: r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (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; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A140, SQUARE_1:15; then A143: ((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7; ( 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63; then A144: sqrt (((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 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; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17; then A146: ((G * (i,1)) `1) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) <= ((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by XREAL_1:6; r * (2 ") > 0 by A8, XREAL_1:129; then s2 - (r / 2) < (s2 - (r / 2)) + (r / 2) by XREAL_1:29; then A147: s2 - (r / 2) < (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 r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A135, A146, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & s1 < (G * (1,1)) `2 ) } by A147, A141; then u0 in Int (cell (G,i,j)) by A130, GOBOARD6:24; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A145, XBOOLE_0:def_4; ::_thesis: verum end; caseA148: ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) set s3 = s2 - (r / 2); set r3 = r2; reconsider q0 = |[r2,(s2 - (r / 2))]| 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 - (r / 2) < (s2 - (r / 2)) + (r / 2) by XREAL_1:29; then s2 - (r / 2) < (G * (1,1)) `2 by A134, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & s1 < (G * (1,1)) `2 ) } by A148; then A149: u0 in Int (cell (G,i,j)) by A130, GOBOARD6:24; reconsider v0 = u0 as Element of REAL 2 ; A150: ( q0 `1 = r2 & q0 `2 = s2 - (r / 2) ) 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 - r2) ^2) + ((s2 - (s2 - (r / 2))) ^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 (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A149, XBOOLE_0:def_4; ::_thesis: verum end; caseA155: r2 = (G * ((i + 1),1)) `1 ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ((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,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))); set s3 = s2 - (r / 2); set r3 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2); reconsider q0 = |[(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 - (r / 2))]| as Point of (TOP-REAL 2) ; A157: ( q0 `1 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 - (r / 2) ) 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: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50; then A160: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21; then r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) by XREAL_1:29, XREAL_1:139; then A161: r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (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; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A160, SQUARE_1:15; then A163: ((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7; ( 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63; then A164: sqrt (((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 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; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17; then A166: ((G * ((i + 1),1)) `1) - ((min (r,(((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) by XREAL_1:10; r * (2 ") > 0 by A8, XREAL_1:129; then s2 - (r / 2) < (s2 - (r / 2)) + (r / 2) by XREAL_1:29; then A167: s2 - (r / 2) < (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 r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A155, A166, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & s1 < (G * (1,1)) `2 ) } by A167, A161; then u0 in Int (cell (G,i,j)) by A130, GOBOARD6:24; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A165, XBOOLE_0:def_4; ::_thesis: verum end; end; end; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ; ::_thesis: verum end; caseA168: ( 1 <= i & i < len G & j = width G ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) then p in { |[r2,s2]| where r2, s2 is Real : ( (G * (i,1)) `1 <= r2 & r2 <= (G * ((i + 1),1)) `1 & s2 >= (G * (1,(width G))) `2 ) } by A3, Th31; then consider r2, s2 being Real 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__::_thesis:_(_(_r2_=_(G_*_(i,1))_`1_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_(G_*_(i,1))_`1_<_r2_&_r2_<_(G_*_((i_+_1),1))_`1_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_r2_=_(G_*_((i_+_1),1))_`1_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_) percases ( r2 = (G * (i,1)) `1 or ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 ) or r2 = (G * ((i + 1),1)) `1 ) by A170, A171, XXREAL_0:1; caseA173: r2 = (G * (i,1)) `1 ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) 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,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))); set s3 = s2 + (r / 2); set r3 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2); reconsider q0 = |[(r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 + (r / 2))]| as Point of (TOP-REAL 2) ; A177: ( q0 `1 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 + (r / 2) ) 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: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50; then A180: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21; then r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > r2 by XREAL_1:29, XREAL_1:139; then A181: r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A170, XXREAL_0:2; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A180, SQUARE_1:15; then A182: ((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7; ( 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63; then sqrt (((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 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 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + (r / 2))) ^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; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17; then A184: ((G * (i,1)) `1) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) <= ((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by XREAL_1:6; r * (2 ") > 0 by A8, XREAL_1:129; then s2 < s2 + (r / 2) by XREAL_1:29; then A185: s2 + (r / 2) > (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 r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A173, A184, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & s1 > (G * (1,(width G))) `2 ) } by A185, A181; then u0 in Int (cell (G,i,j)) by A168, GOBOARD6:25; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A183, XBOOLE_0:def_4; ::_thesis: verum end; caseA186: ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) set s3 = s2 + (r / 2); set r3 = r2; reconsider q0 = |[r2,(s2 + (r / 2))]| 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 < s2 + (r / 2) by XREAL_1:29; then s2 + (r / 2) > (G * (1,(width G))) `2 by A172, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & s1 > (G * (1,(width G))) `2 ) } by A186; then A187: u0 in Int (cell (G,i,j)) by A168, GOBOARD6:25; reconsider v0 = u0 as Element of REAL 2 ; A188: ( q0 `1 = r2 & q0 `2 = s2 + (r / 2) ) 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 - r2) ^2) + ((s2 - (s2 + (r / 2))) ^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 (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A187, XBOOLE_0:def_4; ::_thesis: verum end; caseA193: r2 = (G * ((i + 1),1)) `1 ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) 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,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))); set s3 = s2 + (r / 2); set r3 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2); reconsider q0 = |[(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 + (r / 2))]| as Point of (TOP-REAL 2) ; A197: ( q0 `1 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 + (r / 2) ) 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: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50; then A200: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21; then r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) by XREAL_1:29, XREAL_1:139; then A201: r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A171, XXREAL_0:2; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A200, SQUARE_1:15; then A202: ((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7; ( 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63; then sqrt (((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 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 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + (r / 2))) ^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; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17; then A204: ((G * ((i + 1),1)) `1) - ((min (r,(((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) by XREAL_1:10; r * (2 ") > 0 by A8, XREAL_1:129; then s2 + (r / 2) > s2 by XREAL_1:29; then A205: s2 + (r / 2) > (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 r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A193, A204, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & s1 > (G * (1,(width G))) `2 ) } by A205, A201; then u0 in Int (cell (G,i,j)) by A168, GOBOARD6:25; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A203, XBOOLE_0:def_4; ::_thesis: verum end; end; end; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ; ::_thesis: verum end; caseA206: ( 1 <= i & i < len G & 1 <= j & j < width G ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) then p in { |[r2,s2]| where r2, s2 is Real : ( (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 being Real 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__::_thesis:_(_(_r2_=_(G_*_(i,1))_`1_&_s2_=_(G_*_(1,j))_`2_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_r2_=_(G_*_(i,1))_`1_&_(G_*_(1,j))_`2_<_s2_&_s2_<_(G_*_(1,(j_+_1)))_`2_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_r2_=_(G_*_(i,1))_`1_&_s2_=_(G_*_(1,(j_+_1)))_`2_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_(G_*_(i,1))_`1_<_r2_&_r2_<_(G_*_((i_+_1),1))_`1_&_s2_=_(G_*_(1,j))_`2_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_(G_*_(i,1))_`1_<_r2_&_r2_<_(G_*_((i_+_1),1))_`1_&_(G_*_(1,j))_`2_<_s2_&_s2_<_(G_*_(1,(j_+_1)))_`2_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_(G_*_(i,1))_`1_<_r2_&_r2_<_(G_*_((i_+_1),1))_`1_&_s2_=_(G_*_(1,(j_+_1)))_`2_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_r2_=_(G_*_((i_+_1),1))_`1_&_s2_=_(G_*_(1,j))_`2_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_r2_=_(G_*_((i_+_1),1))_`1_&_(G_*_(1,j))_`2_<_s2_&_s2_<_(G_*_(1,(j_+_1)))_`2_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_or_(_r2_=_(G_*_((i_+_1),1))_`1_&_s2_=_(G_*_(1,(j_+_1)))_`2_&_(Int_(cell_(G,i,j)))_/\_G0_<>_{}_(TOP-REAL_2)_)_) percases ( ( r2 = (G * (i,1)) `1 & s2 = (G * (1,j)) `2 ) or ( r2 = (G * (i,1)) `1 & (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) or ( r2 = (G * (i,1)) `1 & s2 = (G * (1,(j + 1))) `2 ) or ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & s2 = (G * (1,j)) `2 ) or ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) or ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & s2 = (G * (1,(j + 1))) `2 ) or ( r2 = (G * ((i + 1),1)) `1 & s2 = (G * (1,j)) `2 ) or ( r2 = (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) or ( r2 = (G * ((i + 1),1)) `1 & s2 = (G * (1,(j + 1))) `2 ) ) by A208, A209, A210, A211, XXREAL_0:1; caseA212: ( r2 = (G * (i,1)) `1 & s2 = (G * (1,j)) `2 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 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,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))); set rm1 = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))); set r3 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2); set s3 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50; then A215: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21; then r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > r2 by XREAL_1:29, XREAL_1:139; then A216: r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A208, XXREAL_0:2; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17; then A217: ((G * (i,1)) `1) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) <= ((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 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: r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A212, A217, XXREAL_0:2; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17; then A219: ((G * (1,j)) `2) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) <= ((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by XREAL_1:6; reconsider q0 = |[(r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ; A220: ( q0 `1 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) 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: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50; then A223: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21; then s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > s2 by XREAL_1:29, XREAL_1:139; then A224: s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A210, XXREAL_0:2; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then A225: ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A215, SQUARE_1:15; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A223, SQUARE_1:15; then A226: (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 ) by XREAL_1:63; then sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^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 s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A212, A219, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( (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 Int (cell (G,i,j)) by A206, GOBOARD6:26; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A230, XBOOLE_0:def_4; ::_thesis: verum end; caseA231: ( r2 = (G * (i,1)) `1 & (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) set s3 = s2; set rl1 = ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1); set rm1 = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))); set r3 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2); reconsider q0 = |[(r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),s2]| 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: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50; then A234: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21; then A235: r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > r2 by XREAL_1:29, XREAL_1:139; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17; then A236: ((G * (i,1)) `1) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) <= ((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 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 r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A231, A236, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( (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 Int (cell (G,i,j)) 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 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 by XREAL_1:63; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (0 ^2) <= ((r / 2) ^2) + (0 ^2) by A234, SQUARE_1:15; then A240: sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (0 ^2)) <= sqrt (((r / 2) ^2) + (0 ^2)) by A239, SQUARE_1:26; A241: ( q0 `1 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 ) 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 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - s2) ^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 (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A237, XBOOLE_0:def_4; ::_thesis: verum end; caseA245: ( r2 = (G * (i,1)) `1 & s2 = (G * (1,(j + 1))) `2 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 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,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))); set rm1 = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))); set r3 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2); set s3 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50; then A248: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21; then r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > r2 by XREAL_1:29, XREAL_1:139; then A249: r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A208, XXREAL_0:2; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17; then A250: ((G * (i,1)) `1) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) <= ((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 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: r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A245, A250, XXREAL_0:2; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17; then A252: ((G * (1,(j + 1))) `2) - ((min (r,(((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) by XREAL_1:13; reconsider q0 = |[(r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ; A253: ( q0 `1 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) 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: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50; then A256: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21; then s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < s2 by XREAL_1:44, XREAL_1:139; then A257: s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A211, XXREAL_0:2; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then A258: ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A248, SQUARE_1:15; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A256, SQUARE_1:15; then A259: (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 ) by XREAL_1:63; then sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^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 s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A245, A252, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( (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 Int (cell (G,i,j)) by A206, GOBOARD6:26; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A263, XBOOLE_0:def_4; ::_thesis: verum end; caseA264: ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & s2 = (G * (1,j)) `2 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) set r3 = r2; set rl = ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2); set rm = min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))); set s3 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2); reconsider q0 = |[r2,(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| 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: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50; then A267: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21; then A268: s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > s2 by XREAL_1:29, XREAL_1:139; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17; then A269: ((G * (1,j)) `2) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) <= ((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 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 s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A264, A269, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( (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 Int (cell (G,i,j)) 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 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 by XREAL_1:63; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) + (0 ^2) <= ((r / 2) ^2) + (0 ^2) by A267, SQUARE_1:15; then A273: sqrt ((0 ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) <= sqrt ((0 ^2) + ((r / 2) ^2)) by A272, SQUARE_1:26; A274: ( q0 `1 = r2 & q0 `2 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) 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 - r2) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^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 (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A270, XBOOLE_0:def_4; ::_thesis: verum end; caseA278: ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) set s3 = s2; set r3 = r2; reconsider q0 = |[r2,s2]| as Point of (TOP-REAL 2) ; A279: ( q0 `1 = r2 & q0 `2 = s2 ) 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 - r2) ^2) + ((s2 - s2) ^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]| where r1, s1 is Real : ( (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 Int (cell (G,i,j)) by A206, GOBOARD6:26; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A280, XBOOLE_0:def_4; ::_thesis: verum end; caseA281: ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & s2 = (G * (1,(j + 1))) `2 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) set r3 = r2; set rl = ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2); set rm = min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))); set s3 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2); reconsider q0 = |[r2,(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| 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: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50; then A284: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21; then A285: s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < s2 by XREAL_1:44, XREAL_1:139; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17; then A286: ((G * (1,(j + 1))) `2) - ((min (r,(((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) 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 s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A281, A286, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( (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 Int (cell (G,i,j)) 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 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 by XREAL_1:63; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) + (0 ^2) <= ((r / 2) ^2) + (0 ^2) by A284, SQUARE_1:15; then A290: sqrt ((0 ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) <= sqrt ((0 ^2) + ((r / 2) ^2)) by A289, SQUARE_1:26; A291: ( q0 `1 = r2 & q0 `2 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) 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 - r2) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^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 (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A287, XBOOLE_0:def_4; ::_thesis: verum end; caseA295: ( r2 = (G * ((i + 1),1)) `1 & s2 = (G * (1,j)) `2 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 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,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))); set rm1 = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))); set r3 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2); set s3 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50; then A298: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21; then r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < r2 by XREAL_1:44, XREAL_1:139; then A299: r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A209, XXREAL_0:2; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17; then A300: ((G * ((i + 1),1)) `1) - ((min (r,(((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) 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: r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A295, A300, XXREAL_0:2; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17; then A302: ((G * (1,j)) `2) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) <= ((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by XREAL_1:6; reconsider q0 = |[(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ; A303: ( q0 `1 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) 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: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50; then A306: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21; then s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > s2 by XREAL_1:29, XREAL_1:139; then A307: s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A210, XXREAL_0:2; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then A308: ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A298, SQUARE_1:15; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A306, SQUARE_1:15; then A309: (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 ) by XREAL_1:63; then sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^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 s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A295, A302, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( (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 Int (cell (G,i,j)) by A206, GOBOARD6:26; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A313, XBOOLE_0:def_4; ::_thesis: verum end; caseA314: ( r2 = (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) set s3 = s2; set rl1 = ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1); set rm1 = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))); set r3 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2); reconsider q0 = |[(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),s2]| 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: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50; then A317: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21; then A318: r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < r2 by XREAL_1:44, XREAL_1:139; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17; then A319: ((G * ((i + 1),1)) `1) - ((min (r,(((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) 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 r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A314, A319, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( (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 Int (cell (G,i,j)) 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 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 by XREAL_1:63; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then (0 ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) <= (0 ^2) + ((r / 2) ^2) by A317, SQUARE_1:15; then A323: sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (0 ^2)) <= sqrt (((r / 2) ^2) + (0 ^2)) by A322, SQUARE_1:26; A324: ( q0 `1 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 ) 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 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - s2) ^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 (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A320, XBOOLE_0:def_4; ::_thesis: verum end; caseA328: ( r2 = (G * ((i + 1),1)) `1 & s2 = (G * (1,(j + 1))) `2 ) ; ::_thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 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,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))); set rm1 = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))); set r3 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2); set s3 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50; then A331: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21; then r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < r2 by XREAL_1:44, XREAL_1:139; then A332: r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A209, XXREAL_0:2; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17; then A333: ((G * ((i + 1),1)) `1) - ((min (r,(((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) 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: r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A328, A333, XXREAL_0:2; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17; then A335: ((G * (1,(j + 1))) `2) - ((min (r,(((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) 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; (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then A340: ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A331, SQUARE_1:15; reconsider q0 = |[(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ; A341: ( q0 `1 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) by EUCLID:52; reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22; reconsider v0 = u0 as Element of REAL 2 ; A342: ( r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) = (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 & s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) = (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50; then A344: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21; then s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < s2 by XREAL_1:44, XREAL_1:139; then A345: s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A211, XXREAL_0:2; (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17; then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A344, SQUARE_1:15; then A346: (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by A340, XREAL_1:7; ( 0 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 ) by XREAL_1:63; then sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A346, SQUARE_1:26; then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 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 s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A328, A335, XXREAL_0:2; then u0 in { |[r1,s1]| where r1, s1 is Real : ( (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 Int (cell (G,i,j)) by A206, GOBOARD6:26; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A347, XBOOLE_0:def_4; ::_thesis: verum end; end; end; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ; ::_thesis: verum end; end; end; hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ; ::_thesis: verum end; hence ( not p in G0 or Int (cell (G,i,j)) meets G0 ) by XBOOLE_0:def_7; ::_thesis: verum end; hence x in Cl (Int (cell (G,i,j))) by PRE_TOPC:def_7; ::_thesis: verum end; ( Cl (Int (cell (G,i,j))) c= Cl (cell (G,i,j)) & cell (G,i,j) is closed ) by Th33, PRE_TOPC:19, TOPS_1:16; then Cl (Int (cell (G,i,j))) c= cell (G,i,j) by PRE_TOPC:22; hence cell (G,i,j) = Cl (Int (cell (G,i,j))) by A2, XBOOLE_0:def_10; ::_thesis: verum end;