for r1, r2, s being Real holds
( not abs (r1 - r2) > s or r1 + s < r2 or r2 + s < r1 )

for r, s being Real holds
( abs (r - s) = 0 iff r = s )

for n being Nat
for p, p1, q being Point of (TOP-REAL n) st p + p1 = q + p1 holds
p = q

for n being Nat
for p, p1, q being Point of (TOP-REAL n) st p1 + p = p1 + q holds
p = q by Th3;

for p1, p, q being Point of (TOP-REAL 2) st p1 in LSeg p,q & p `1 = q `1 holds
p1 `1 = q `1

for p1, p, q being Point of (TOP-REAL 2) st p1 in LSeg p,q & p `2 = q `2 holds
p1 `2 = q `2

for n being Nat
for p, q being Point of (TOP-REAL n) holds (1 / 2) * (p + q) in LSeg p,q

for p, q, p1 being Point of (TOP-REAL 2) st p `1 = q `1 & q `1 = p1 `1 & p `2 <= q `2 & q `2 <= p1 `2 holds
q in LSeg p,p1

for p, q, p1 being Point of (TOP-REAL 2) st p `1 <= q `1 & q `1 <= p1 `1 & p `2 = q `2 & q `2 = p1 `2 holds
q in LSeg p,p1

for D being non empty set
for i, j being Nat
for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds
[i,j] in Indices M

for i, j being Nat
for G being Go-board st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
(1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1))) = (1 / 2) * ((G * i,(j + 1)) + (G * (i + 1),j))

for f being non empty FinSequence of (TOP-REAL 2)
for k being Nat st LSeg f,k is horizontal holds
ex j being Nat st
( 1 <= j & j <= width (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg f,k holds
p `2 = ((GoB f) * 1,j) `2 ) )

for f being non empty FinSequence of (TOP-REAL 2)
for k being Nat st LSeg f,k is vertical holds
ex i being Nat st
( 1 <= i & i <= len (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg f,k holds
p `1 = ((GoB f) * i,1) `1 ) )

for f being non empty FinSequence of (TOP-REAL 2)
for i, j being Nat st f is special & i <= len (GoB f) & j <= width (GoB f) holds
Int (cell (GoB f),i,j) misses L~ f

for i, j being Nat
for G being Go-board st 1 <= i & i <= len G & 1 <= j & j + 2 <= width G holds
(LSeg (G * i,j),(G * i,(j + 1))) /\ (LSeg (G * i,(j + 1)),(G * i,(j + 2))) = {(G * i,(j + 1))}

for i, j being Nat
for G being Go-board st 1 <= i & i + 2 <= len G & 1 <= j & j <= width G holds
(LSeg (G * i,j),(G * (i + 1),j)) /\ (LSeg (G * (i + 1),j),(G * (i + 2),j)) = {(G * (i + 1),j)}

for i, j being Nat
for G being Go-board st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
(LSeg (G * i,j),(G * i,(j + 1))) /\ (LSeg (G * i,(j + 1)),(G * (i + 1),(j + 1))) = {(G * i,(j + 1))}

for i, j being Nat
for G being Go-board st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
(LSeg (G * i,(j + 1)),(G * (i + 1),(j + 1))) /\ (LSeg (G * (i + 1),j),(G * (i + 1),(j + 1))) = {(G * (i + 1),(j + 1))}

for i, j being Nat
for G being Go-board st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
(LSeg (G * i,j),(G * (i + 1),j)) /\ (LSeg (G * i,j),(G * i,(j + 1))) = {(G * i,j)}

for i, j being Nat
for G being Go-board st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
(LSeg (G * i,j),(G * (i + 1),j)) /\ (LSeg (G * (i + 1),j),(G * (i + 1),(j + 1))) = {(G * (i + 1),j)}

for G being Go-board
for i1, j1, i2, j2 being Nat st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2 + 1 <= width G & LSeg (G * i1,j1),(G * i1,(j1 + 1)) meets LSeg (G * i2,j2),(G * i2,(j2 + 1)) holds
( i1 = i2 & abs (j1 - j2) <= 1 )

for G being Go-board
for i1, j1, i2, j2 being Nat st 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg (G * i1,j1),(G * (i1 + 1),j1) meets LSeg (G * i2,j2),(G * (i2 + 1),j2) holds
( j1 = j2 & abs (i1 - i2) <= 1 )

for G being Go-board
for i1, j1, i2, j2 being Nat st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg (G * i1,j1),(G * i1,(j1 + 1)) meets LSeg (G * i2,j2),(G * (i2 + 1),j2) holds
( ( i1 = i2 or i1 = i2 + 1 ) & ( j1 = j2 or j1 + 1 = j2 ) )

for G being Go-board
for i1, j1, i2, j2 being Nat st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2 + 1 <= width G & LSeg (G * i1,j1),(G * i1,(j1 + 1)) meets LSeg (G * i2,j2),(G * i2,(j2 + 1)) & not ( j1 = j2 & LSeg (G * i1,j1),(G * i1,(j1 + 1)) = LSeg (G * i2,j2),(G * i2,(j2 + 1)) ) & not ( j1 = j2 + 1 & (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * i2,(j2 + 1))) = {(G * i1,j1)} ) holds
( j1 + 1 = j2 & (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * i2,(j2 + 1))) = {(G * i2,j2)} )

for G being Go-board
for i1, j1, i2, j2 being Nat st 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg (G * i1,j1),(G * (i1 + 1),j1) meets LSeg (G * i2,j2),(G * (i2 + 1),j2) & not ( i1 = i2 & LSeg (G * i1,j1),(G * (i1 + 1),j1) = LSeg (G * i2,j2),(G * (i2 + 1),j2) ) & not ( i1 = i2 + 1 & (LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)} ) holds
( i1 + 1 = i2 & (LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i2,j2)} )

for G being Go-board
for i1, j1, i2, j2 being Nat st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg (G * i1,j1),(G * i1,(j1 + 1)) meets LSeg (G * i2,j2),(G * (i2 + 1),j2) & not ( j1 = j2 & (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)} ) holds
( j1 + 1 = j2 & (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,(j1 + 1))} )

for i1, j1, i2, j2 being Nat
for G being Go-board st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2 + 1 <= width G & (1 / 2) * ((G * i1,j1) + (G * i1,(j1 + 1))) in LSeg (G * i2,j2),(G * i2,(j2 + 1)) holds
( i1 = i2 & j1 = j2 )

for i1, j1, i2, j2 being Nat
for G being Go-board st 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in LSeg (G * i2,j2),(G * (i2 + 1),j2) holds
( i1 = i2 & j1 = j2 )

for i1, j1 being Nat
for G being Go-board st 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G holds
for i2, j2 being Nat holds
( not 1 <= i2 or not i2 <= len G or not 1 <= j2 or not j2 + 1 <= width G or not (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in LSeg (G * i2,j2),(G * i2,(j2 + 1)) )

for i1, j1 being Nat
for G being Go-board st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G holds
for i2, j2 being Nat holds
( not 1 <= i2 or not i2 + 1 <= len G or not 1 <= j2 or not j2 <= width G or not (1 / 2) * ((G * i1,j1) + (G * i1,(j1 + 1))) in LSeg (G * i2,j2),(G * (i2 + 1),j2) )

for i being Nat
for f being non empty standard FinSequence of (TOP-REAL 2) st i in dom f & i + 1 in dom f holds
f /. i <> f /. (i + 1)

for f being standard non constant special_circular_sequence ex i being Nat st
( i in dom f & (f /. i) `1 <> (f /. 1) `1 )

for f being standard non constant special_circular_sequence ex i being Nat st
( i in dom f & (f /. i) `2 <> (f /. 1) `2 )

for f being standard non constant special_circular_sequence holds len (GoB f) > 1

for f being standard non constant special_circular_sequence holds width (GoB f) > 1

for f being standard non constant special_circular_sequence holds len f > 4

for f being circular s.c.c. FinSequence of (TOP-REAL 2) st len f > 4 holds
for i, j being Nat st 1 <= i & i < j & j < len f holds
f /. i <> f /. j

for f being standard non constant special_circular_sequence
for i, j being Nat st 1 <= i & i < j & j < len f holds
f /. i <> f /. j

for f being standard non constant special_circular_sequence
for i, j being Nat st 1 < i & i < j & j <= len f holds
f /. i <> f /. j

for f being standard non constant special_circular_sequence
for i being Nat st 1 < i & i <= len f & f /. i = f /. 1 holds
i = len f

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

for i, j being Nat
for f being standard non constant 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 )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

for i, j being Nat
for f being standard non constant special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & LSeg ((GoB f) * i,(j + 1)),((GoB f) * (i + 1),(j + 1)) c= L~ f & LSeg ((GoB f) * (i + 1),(j + 1)),((GoB f) * (i + 1),j) c= L~ f & not ( f /. 1 = (GoB f) * (i + 1),(j + 1) & ( ( f /. 2 = (GoB f) * i,(j + 1) & f /. ((len f) -' 1) = (GoB f) * (i + 1),j ) or ( f /. 2 = (GoB f) * (i + 1),j & f /. ((len f) -' 1) = (GoB f) * i,(j + 1) ) ) ) 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,(j + 1) & f /. (k + 2) = (GoB f) * (i + 1),j ) or ( f /. k = (GoB f) * (i + 1),j & f /. (k + 2) = (GoB f) * i,(j + 1) ) ) )

for i, j being Nat
for f being standard non constant special_circular_sequence st 1 <= i & i + 1 < len (GoB f) & 1 <= j & j <= width (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 & not ( f /. 1 = (GoB f) * (i + 1),j & ( ( f /. 2 = (GoB f) * i,j & f /. ((len f) -' 1) = (GoB f) * (i + 2),j ) or ( f /. 2 = (GoB f) * (i + 2),j & f /. ((len f) -' 1) = (GoB f) * i,j ) ) ) holds
ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),j & ( ( f /. k = (GoB f) * i,j & f /. (k + 2) = (GoB f) * (i + 2),j ) or ( f /. k = (GoB f) * (i + 2),j & f /. (k + 2) = (GoB f) * i,j ) ) )

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

for i, j being Nat
for f being standard non constant 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 ) ) )

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

for i, j being Nat
for f being standard non constant special_circular_sequence st 1 <= i & i < 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 + 1),(j + 2)) c= L~ f holds
not LSeg ((GoB f) * i,(j + 1)),((GoB f) * (i + 1),(j + 1)) c= L~ f

for j, i being Nat
for f being standard non constant 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

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