:: deftheorem defines is_associated_to GCD_1:def 3 :
for R being non empty multLoopStr
for x, y being Element of R holds
( x is_associated_to y iff ( x divides y & y divides x ) );