let i, j be Nat; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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 :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: 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; :: thesis: 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 ) } ; :: according to XBOOLE_0:def 10 :: thesis: { |[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 :: thesis: 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 ; :: thesis: ( 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 ) } ; :: thesis: 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; :: thesis: 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) ; :: thesis: verum