:: deftheorem Def7 defines Am GCD_1:def 7 :
for R being non empty well-unital associative multLoopStr
for b₂ being non empty Subset of R holds
( b₂ is Am of R iff ( ( for a being Element of R ex z being Element of b₂ st z is_associated_to a ) & ( for x, y being Element of b₂ st x <> y holds
x is_not_associated_to y ) ) );