for F being Field
for p, q being Element of (Polynom-Ring F) holds
( p gcd q divides p & p gcd q divides q & ( for r being Element of (Polynom-Ring F) st r divides p & r divides q holds
r divides p gcd q ) ) by defGCD;