theorem :: GOBOARD8:29

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