:: deftheorem NIL1 defines reduced FIELD_16:def 5 :
for R being Ring holds
( R is reduced iff for a being nilpotent Element of R holds a = 0. R );