theorem :: GOBOARD7:61

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