let i be Integer; :: thesis: ( i <> 1 & i <> - 1 & not i is prime & not - i is prime implies multiples i misses SetPrimes )
assume that
A1: i <> 1 and
A2: i <> - 1 and
A3: not i is prime and
A4: not - i is prime ; :: thesis: multiples i misses SetPrimes
assume multiples i meets SetPrimes ; :: thesis: contradiction
then consider x being object such that
A5: x in multiples i and
A6: x in SetPrimes by XBOOLE_0:3;
reconsider m = x as Multiple of i by A5, Th61;
A7: i divides m by Def15;
A8: m is prime by A6, NEWTON:def 6;

per cases ( i >= 0 or i < 0 ) ;

suppose i >= 0 ; :: thesis: contradiction

then i in NAT by INT_1:3;
hence contradiction by A1, A3, A8, Def15; :: thesis: verum

end;

suppose i < 0 ; :: thesis: contradiction

then - i in NAT by INT_1:3;
then ( - i = 1 or - i = x ) by A7, A8, INT_2:10;
hence contradiction by A2, A4, A6, NEWTON:def 6; :: thesis: verum

end;

end;