theorem :: GOBOARD6:86

for j being Nat
for p being Point of (TOP-REAL 2)
for G being Go-board st 1 <= j & j + 1 <= width G holds
LSeg (p,(((1 / 2) * ((G * ((len G),j)) + (G * ((len G),(j + 1))))) + |[1,0]|)) meets Int (cell (G,(len G),j))