:: deftheorem defines nilrad TOPZARI1:def 13 :
for A being non degenerated commutative Ring holds nilrad A = { a where a is nilpotent Element of A : verum } ;