:: deftheorem Def12 defines gcd GCD_1:def 12 :
for R being non empty well-unital associative gcd-like multLoopStr
for Amp being AmpleSet of R
for x, y, b₅ being Element of R holds
( b₅ = gcd (x,y,Amp) iff ( b₅ in Amp & b₅ divides x & b₅ divides y & ( for z being Element of R st z divides x & z divides y holds
z divides b₅ ) ) );