theorem Th40: :: GOBOARD7:40

for i, j being Nat
for f being constant standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j <= width (GoB f) & (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j))) in L~ f holds
ex k being Nat st
( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) )