for p, q being Element of (Polynom-Ring F) holds p gcd q = q gcd p ;
hence for p, q being Element of (Polynom-Ring F) holds p gcd q = q gcd p ; :: thesis: verum