theorem :: INT_2:14

for a being Integer st ( a = 1 or a = - 1 ) holds
( a divides 1 & a divides - 1 ) by Lm5;