for R being domRing
for a, b being Element of R st a is irreducible & b is_associated_to a holds
b is irreducible