for F being Field
for p, q being Polynomial of F holds
( p gcd q divides p & p gcd q divides q & ( for r being Polynomial of F st r divides p & r divides q holds
r divides p gcd q ) )