:: deftheorem defGCD defines -gcd RING_4:def 10 :
for L being non empty multMagma
for x, y, z being Element of L holds
( z is x,y -gcd iff ( z divides x & z divides y & ( for r being Element of L st r divides x & r divides y holds
r divides z ) ) );