:: deftheorem defines PRIMARY IDEAL_2:def 7 :
for A being non degenerated commutative Ring holds PRIMARY A = { I where I is primary Ideal of A : verum } ;