for i1, i2 being Nat st i1,i2 are_adjacent holds
i1 + 1,i2 + 1 are_adjacent ;