let i1, i2, j1, j2 be Nat; :: thesis: ( i1,j1,i2,j2 are_adjacent implies i1 + 1,j1 + 1,i2 + 1,j2 + 1 are_adjacent )
assume i1,j1,i2,j2 are_adjacent ; :: thesis: i1 + 1,j1 + 1,i2 + 1,j2 + 1 are_adjacent
then ( ( i1,i2 are_adjacent & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent ) ) ;
then ( ( i1 + 1,i2 + 1 are_adjacent & j1 + 1 = j2 + 1 ) or ( i1 + 1 = i2 + 1 & j1 + 1,j2 + 1 are_adjacent ) ) ;
hence i1 + 1,j1 + 1,i2 + 1,j2 + 1 are_adjacent ; :: thesis: verum