theorem Th27: :: GOBOARD7:27

for i1, j1 being Nat
for G being Go-board st 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G holds
for i2, j2 being Nat holds
( not 1 <= i2 or not i2 <= len G or not 1 <= j2 or not j2 + 1 <= width G or not (1 / 2) * ((G * (i1,j1)) + (G * ((i1 + 1),j1))) in LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1)))) )