:: deftheorem Def9 defines NF GCD_1:def 9 :
for R being non empty well-unital associative multLoopStr
for Amp being AmpleSet of R
for x, b₄ being Element of R holds
( b₄ = NF (x,Amp) iff ( b₄ in Amp & b₄ is_associated_to x ) );