theorem :: GOBOARD6:67

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