let i1, i2 be Element of NAT ; :: thesis: ( i1,i2 are_adjacent1 implies i1 + 1,i2 + 1 are_adjacent1 )
assume i1,i2 are_adjacent1 ; :: thesis: i1 + 1,i2 + 1 are_adjacent1
then ( i2 = i1 + 1 or i1 = i2 + 1 ) by Def1;
hence i1 + 1,i2 + 1 are_adjacent1 by Def1; :: thesis: verum