let A be non degenerated commutative Ring; :: thesis: for a being Element of A st a is nilpotent holds
a in sqrt {(0. A)}
let a be Element of A; :: thesis: ( a is nilpotent implies a in sqrt {(0. A)} )
set N = { a where a is Element of A : ex n being Element of NAT st a |^ n in {(0. A)} } ;
assume a is nilpotent ; :: thesis: a in sqrt {(0. A)}
then consider n being non zero Nat such that
A2: a |^ n = 0. A ;
A3: {(0. A)} = {(0. A)} -Ideal by IDEAL_1:47;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
reconsider s = a as Element of A ;
s |^ n in {(0. A)} by A2, A3, IDEAL_1:66;
then a in { a where a is Element of A : ex n being Element of NAT st a |^ n in {(0. A)} } ;
hence a in sqrt {(0. A)} by IDEAL_1:def 24; :: thesis: verum