theorem :: GOBOARD8:31

for f being non constant standard special_circular_sequence
for j being Nat st 1 <= j & j + 2 <= width (GoB f) holds
LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,(j + 1))) + ((GoB f) * (1,(j + 2))))) - |[1,0]|)) misses L~ f