theorem :: GOBOARD6:71

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