theorem Th23: :: GOBOARD6:23

for j being Nat
for G being Go-board st 1 <= j & j < width G holds
Int (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 ) }