for i1, i2, j1, j2 being Nat st i1,j1,i2,j2 are_adjacent holds
i1 + 1,j1 + 1,i2 + 1,j2 + 1 are_adjacent