let a be Integer; :: thesis: ( a divides - a & - a divides a )
- a = a * (- 1) ;
hence a divides - a by INT_1:def 3; :: thesis: - a divides a
a = (- a) * (- 1) ;
hence - a divides a by INT_1:def 3; :: thesis: verum