:: deftheorem Def5 defines Char RING_3:def 5 :
for R being Ring
for b₂ being Nat holds
( b₂ = Char R iff ( ( b₂ '*' (1. R) = 0. R & b₂ <> 0 & ( for m being positive Nat st m < b₂ holds
m '*' (1. R) <> 0. R ) ) or ( b₂ = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) );