:: deftheorem defines are_co-prime GCD_1:def 14 :
for R being non empty well-unital associative gcd-like multLoopStr
for x, y being Element of R holds
( x,y are_co-prime iff ex Amp being AmpleSet of R st gcd (x,y,Amp) = 1. R );