let a be Integer; :: thesis: ( ( not a divides 1 & not a divides - 1 ) or a = 1 or a = - 1 )
A1: ( not a divides 1 or a = 1 or a = - 1 )

proof

assume a divides 1 ; :: thesis: ( a = 1 or a = - 1 )
then ex b being Integer st 1 = a * b by INT_1:def 3;
hence ( a = 1 or a = - 1 ) by INT_1:9; :: thesis: verum

end;

A2: ( not a divides - 1 or a = 1 or a = - 1 )

proof

assume a divides - 1 ; :: thesis: ( a = 1 or a = - 1 )
then ex b being Integer st - 1 = a * b by INT_1:def 3;
hence ( a = 1 or a = - 1 ) by INT_1:10; :: thesis: verum

end;

assume ( a divides 1 or a divides - 1 ) ; :: thesis: ( a = 1 or a = - 1 )
hence ( a = 1 or a = - 1 ) by A1, A2; :: thesis: verum