theorem :: GOBOARD6:69

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