for R being gcdDomain
for Amp, Amp9 being AmpleSet of R
for x, y being Element of R st x,y are_canonical_wrt Amp holds
x,y are_canonical_wrt Amp9