theorem :: INT_2:8

for a being Integer holds
( a divides - a & - a divides a ) by Lm1;