theorem Th20: :: GOBOARD6:20

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