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

proof

assume a divides 1 ; :: thesis: ( a = 1 or a = - 1 )
then consider b being Integer such that
A3: 1 = a * b by INT_1:def 9;
thus ( a = 1 or a = - 1 ) by A3, INT_1:22; :: thesis: verum

end;

( 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 9;
hence ( a = 1 or a = - 1 ) by INT_1:23; :: thesis: verum

end;

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