let i1, i2, j1, j2 be Element of NAT ; :: thesis: ( i1,j1,i2,j2 are_adjacent2 implies i1 + 1,j1 + 1,i2 + 1,j2 + 1 are_adjacent2 )
assume i1,j1,i2,j2 are_adjacent2 ; :: thesis: i1 + 1,j1 + 1,i2 + 1,j2 + 1 are_adjacent2
then ( ( i1,i2 are_adjacent1 & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent1 ) ) by Def2;
then ( ( i1 + 1,i2 + 1 are_adjacent1 & j1 + 1 = j2 + 1 ) or ( i1 + 1 = i2 + 1 & j1 + 1,j2 + 1 are_adjacent1 ) ) by Th1;
hence i1 + 1,j1 + 1,i2 + 1,j2 + 1 are_adjacent2 by Def2; :: thesis: verum