:: deftheorem Def6 defines -characteristic RING_3:def 6 :
for n being Nat
for R being Ring holds
( R is n -characteristic iff Char R = n );