:: deftheorem defines -primary IDEAL_2:def 6 :
for A being non degenerated commutative Ring
for P, Q being Ideal of A holds
( Q is P -primary iff sqrt Q = P );