:: deftheorem Def1 defines right_cell GOBRD13:def 2 :
for f being FinSequence of (TOP-REAL 2)
for G being Go-board
for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
for b₄ being Subset of (TOP-REAL 2) holds
( b₄ = right_cell (f,k,G) iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b₄ = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b₄ = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b₄ = cell (G,i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b₄ = cell (G,(i1 -' 1),j2) ) );