theorem Th49: :: GOBOARD6:49

for j being Nat
for G being Go-board st 1 <= j & j < width G holds
LSeg ((((1 / 2) * ((G * (1,j)) + (G * (1,(j + 1))))) - |[1,0]|),((G * (1,(j + 1))) - |[1,0]|)) c= (Int (cell (G,0,j))) \/ {((G * (1,(j + 1))) - |[1,0]|)}