for R being comRing
for a, b being Element of R holds
( a is_associated_to b iff {a} -Ideal = {b} -Ideal ) by div1;