let n be Nat; :: thesis: ( n <> 1 implies for m being Multiple of n st m is prime holds
m = n )
assume A1: n <> 1 ; :: thesis: for m being Multiple of n st m is prime holds
m = n
let m be Multiple of n; :: thesis: ( m is prime implies m = n )
assume A2: m is prime ; :: thesis: m = n
( m = n or m = - n ) by A1, A2, Th59;
hence m = n by A2; :: thesis: verum