let A be non degenerated commutative Ring; :: thesis: for I being Ideal of A holds
( sqrt I = [#] A iff I = [#] A )
let I be Ideal of A; :: thesis: ( sqrt I = [#] A iff I = [#] A )
thus ( sqrt I = [#] A implies I = [#] A ) :: thesis: ( I = [#] A implies sqrt I = [#] A )

proof

assume sqrt I = [#] A ; :: thesis: I = [#] A
then 1. A in sqrt I ;
then 1. A in { a where a is Element of A : ex n being Element of NAT st a |^ n in I } by IDEAL_1:def 24;
then consider o1 being Element of A such that
A3: o1 = 1. A and
A4: ex n being Element of NAT st o1 |^ n in I ;
consider m1 being Element of NAT such that
A5: o1 |^ m1 in I by A4;
A6: o1 |^ m1 = 1. A by A3, TOPZARI1:2;
not I is proper by A5, A6, IDEAL_1:19;
hence I = [#] A ; :: thesis: verum

end;

thus ( I = [#] A implies sqrt I = [#] A ) by TOPZARI1:20; :: thesis: verum