:: deftheorem Def6 defines right_cell GOBOARD5:def 6 :
for f being standard special_circular_sequence
for k being Nat st 1 <= k & k + 1 <= len f holds
for b₃ being Subset of (TOP-REAL 2) holds
( b₃ = right_cell (f,k) iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b₃ = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b₃ = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b₃ = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b₃ = cell ((GoB f),(i1 -' 1),j2) ) );