for f being non constant standard special_circular_sequence
for i1, j1, i2, j2 being Nat st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & i1,j1,i2,j2 are_adjacent holds
( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) )