let p, q be Nat; :: thesis: ( p is prime & q is prime & not p,q are_coprime implies p = q )
assume that
A1: p is prime and
A2: q is prime ; :: thesis: ( p,q are_coprime or p = q )
A3: p gcd q divides q by Def2;
assume not p,q are_coprime ; :: thesis: p = q
then A4: p gcd q <> 1 ;
p gcd q divides p by Def2;
then p gcd q = p by A1, A4;
hence p = q by A2, A4, A3; :: thesis: verum