for a, b being Element of Gauss_INT_Ring
for aa, bb being G_INTEG st a = aa & b = bb & aa is_associated_to bb holds
a is_associated_to b