let i, j be Integer; :: thesis: ( i <> - 1 & i <> 1 & i divides j implies not i divides j + 1 )
assume A1: ( i <> - 1 & i <> 1 ) ; :: thesis: ( not i divides j or not i divides j + 1 )
assume ( i divides j & i divides j + 1 ) ; :: thesis: contradiction
then i divides (j + 1) - j by INT_5:1;
hence contradiction by A1, INT_2:13; :: thesis: verum