let i, j be Nat; for G being Go-board st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
cell (G,i,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 & (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) }
let G be Go-board; ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G implies cell (G,i,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 & (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } )
set A = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 & (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } ;
assume A1:
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G )
; cell (G,i,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 & (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) }
now for p being object st p in cell (G,i,j) holds
p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 & (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } let p be
object ;
( p in cell (G,i,j) implies p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 & (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } )assume A2:
p in cell (
G,
i,
j)
;
p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 & (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } then reconsider q =
p as
Point of
(TOP-REAL 2) ;
A3:
(
(G * (i,j)) `2 <= q `2 &
q `2 <= (G * (i,(j + 1))) `2 )
by A1, A2, Th17;
A4:
p = |[(q `1),(q `2)]|
by EUCLID:53;
(
(G * (i,j)) `1 <= q `1 &
q `1 <= (G * ((i + 1),j)) `1 )
by A1, A2, Th17;
hence
p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 & (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) }
by A4, A3;
verum end;
hence
cell (G,i,j) c= { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 & (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) }
; XBOOLE_0:def 10 { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 & (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } c= cell (G,i,j)
now for p being object st p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 & (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } holds
p in cell (G,i,j)let p be
object ;
( p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 & (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } implies p in cell (G,i,j) )assume
p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 & (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) }
;
p in cell (G,i,j)then consider r,
s being
Real such that A5:
|[r,s]| = p
and A6:
(
(G * (i,j)) `1 <= r &
r <= (G * ((i + 1),j)) `1 &
(G * (i,j)) `2 <= s &
s <= (G * (i,(j + 1))) `2 )
;
reconsider q =
p as
Point of
(TOP-REAL 2) by A5;
(
r = q `1 &
s = q `2 )
by A5, EUCLID:52;
hence
p in cell (
G,
i,
j)
by A1, A6, Th17;
verum end;
hence
{ |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 & (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } c= cell (G,i,j)
; verum