theorem :: GOBOARD6:85

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 ((((1 / 2) * ((G * (1,j)) + (G * (1,(j + 1))))) - |[1,0]|),p) meets Int (cell (G,0,j))