let A be non degenerated commutative Ring; :: thesis: nilrad A = sqrt {(0. A)}
set N = { a where a is Element of A : ex n being Element of NAT st a |^ n in {(0. A)} } ;
A1: for a being object st a in nilrad A holds
a in sqrt {(0. A)}

proof

let a be object ; :: thesis: ( a in nilrad A implies a in sqrt {(0. A)} )
assume a in nilrad A ; :: thesis: a in sqrt {(0. A)}
then consider s being nilpotent Element of A such that
A3: s = a ;
thus a in sqrt {(0. A)} by A3, Lm25; :: thesis: verum

end;

for a being object st a in sqrt {(0. A)} holds
a in nilrad A

proof

let a be object ; :: thesis: ( a in sqrt {(0. A)} implies a in nilrad A )
assume a in sqrt {(0. A)} ; :: thesis: a in nilrad A
then a in { a where a is Element of A : ex n being Element of NAT st a |^ n in {(0. A)} } by IDEAL_1:def 24;
then consider s being Element of A such that
A7: ( s = a & ex n being Element of NAT st s |^ n in {(0. A)} ) ;
consider n being Element of NAT such that
A8: s |^ n in {(0. A)} by A7;
A9: s |^ n = 0. A by A8, TARSKI:def 1;
n is non zero Nat by A8, Lm26;
then s is nilpotent by A9;
hence a in nilrad A by A7; :: thesis: verum

end;

hence nilrad A = sqrt {(0. A)} by A1, TARSKI:2; :: thesis: verum