:: deftheorem defines Ideals TOPZARI1:def 4 :
for A being non degenerated commutative Ring
for J being proper Ideal of A
for f being Element of A holds Ideals (A,J,f) = { I where I is Subset of A : ( I is proper Ideal of A & J c= I & I /\ (multClSet (J,f)) = {} ) } ;