theorem :: GOBOARD8:28

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