theorem :: GCD_1:26

for R being commutative domRing-like Ring
for Amp being AmpleSet of R
for a being Element of R holds
( a in Amp iff a = NF (a,Amp) ) by Def9;