theorem :: GOBOARD6:64

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