:: deftheorem Def1 defines % IDEAL_2:def 1 :
for A being non degenerated commutative Ring
for I being Ideal of A
for b₃ being Function of (bool the carrier of A),(bool the carrier of A) holds
( b₃ = % I iff for x being Subset of A holds b₃ . x = x % I );