theorem Th13: :: INT_2:13

for a being Integer holds
( ( not a divides 1 & not a divides - 1 ) or a = 1 or a = - 1 ) by INT_1:9, INT_1:10;