let L be gcdDomain; :: thesis: for x, y being Element of L
for u, v being a_gcd of x,y holds u is_associated_to v
let p, q be Element of L; :: thesis: for u, v being a_gcd of p,q holds u is_associated_to v
let u, v be a_gcd of p,q; :: thesis: u is_associated_to v
A: ( u divides p & u divides q ) by defGCD;
( v divides p & v divides q ) by defGCD;
hence u is_associated_to v by A, defGCD; :: thesis: verum