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