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