theorem Th58: :: GOBOARD7:58

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