for i1, i2, j1, j2 being Nat st i1,j1,i2,j2 are_adjacent & 1 <= i1 & 1 <= i2 & 1 <= j1 & 1 <= j2 holds
i1 -' 1,j1 -' 1,i2 -' 1,j2 -' 1 are_adjacent by Th2;