:: deftheorem defines CharSet RING_3:def 7 :
for R being Ring holds CharSet R = { n where n is positive Nat : n '*' (1. R) = 0. R } ;