for R being gcdDomain
for Amp being AmpleSet of R
for x, y being Element of R st x,y are_co-prime holds
gcd (x,y,Amp) = 1. R