let p, q be natural number ; :: thesis: ( p is prime & q is prime & not p,q are_relative_prime implies p = q )
assume A1: ( p is prime & q is prime ) ; :: thesis: ( p,q are_relative_prime or p = q )
assume not p,q are_relative_prime ; :: thesis: p = q
then A2: p gcd q <> 1 by Def4;
( p gcd q divides p & p gcd q divides q ) by Def3;
then ( p gcd q = p & p gcd q = q ) by A1, A2, Def5;
hence p = q ; :: thesis: verum