:: deftheorem defines is_associated_to GAUSSINT:def 21 :
for x, y being G_INTEG holds
( x is_associated_to y iff ( x Divides y & y Divides x ) );