theorem :: GOBOARD6:73

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