theorem gcd1: :: RING_4:49

for L being gcdDomain
for x, y being Element of L
for u, v being a_gcd of x,y holds u is_associated_to v