let R be non degenerated commutative Ring; :: thesis: ( R is reduced iff nilrad R = {(0. R)} )
H: nilrad R = { a where a is nilpotent Element of R : verum } by TOPZARI1:def 13;

A: now :: thesis: ( R is reduced implies nilrad R = {(0. R)} )

assume B: R is reduced ; :: thesis: nilrad R = {(0. R)}

C: now :: thesis: for o being object st o in nilrad R holds
o in {(0. R)}

let o be object ; :: thesis: ( o in nilrad R implies o in {(0. R)} )
assume o in nilrad R ; :: thesis: o in {(0. R)}
then consider a being nilpotent Element of R such that
D: o = a by H;
a is zero by B;
hence o in {(0. R)} by D, TARSKI:def 1; :: thesis: verum

end;

now :: thesis: for o being object st o in {(0. R)} holds
o in nilrad R

let o be object ; :: thesis: ( o in {(0. R)} implies o in nilrad R )
assume o in {(0. R)} ; :: thesis: o in nilrad R
then o = 0. R by TARSKI:def 1;
hence o in nilrad R by H; :: thesis: verum

end;

hence nilrad R = {(0. R)} by C, TARSKI:2; :: thesis: verum

end;

now :: thesis: ( nilrad R = {(0. R)} implies R is reduced )

assume B: nilrad R = {(0. R)} ; :: thesis: R is reduced

now :: thesis: for a being Element of R st a <> 0. R holds
not a is nilpotent

let a be Element of R; :: thesis: ( a <> 0. R implies not a is nilpotent )
assume a <> 0. R ; :: thesis: not a is nilpotent
then not a in nilrad R by B, TARSKI:def 1;
hence not a is nilpotent by H; :: thesis: verum

end;

hence R is reduced ; :: thesis: verum

end;

hence ( R is reduced iff nilrad R = {(0. R)} ) by A; :: thesis: verum