let a be Integer; :: thesis: ( a divides 0 & 1 divides a & - 1 divides a )
thus a divides 0 :: thesis: ( 1 divides a & - 1 divides a )

proof

0 = a * 0 ;
hence a divides 0 by INT_1:def 9; :: thesis: verum

end;

thus 1 divides a :: thesis: - 1 divides a

proof

a = 1 * a ;
hence 1 divides a by INT_1:def 9; :: thesis: verum

end;

a = (- 1) * (- a) ;
hence - 1 divides a by INT_1:def 9; :: thesis: verum