let A be non degenerated commutative Ring; :: thesis: for I being Ideal of A holds I c= sqrt I
let I be Ideal of A; :: thesis: I c= sqrt I
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in I or x in sqrt I )
assume A1: x in I ; :: thesis: x in sqrt I
then reconsider x = x as Element of A ;
x |^ 1 in I by A1, BINOM:8;
then x in { a where a is Element of A : ex n being Element of NAT st a |^ n in I } ;
hence x in sqrt I by IDEAL_1:def 24; :: thesis: verum