theorem :: GOBOARD8:25

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,1)) + ((GoB f) * ((i + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|)) misses L~ f