let a be Integer; :: thesis: for p being Prime st a gcd p = 1 holds
not p divides a
let p be Prime; :: thesis: ( a gcd p = 1 implies not p divides a )
assume A1: a gcd p = 1 ; :: thesis: not p divides a
assume p divides a ; :: thesis: contradiction
then p divides p gcd a by INT_2:def 2;
then p = 1 by A1, WSIERP_1:15;
hence contradiction by INT_2:def 4; :: thesis: verum