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