let A be non degenerated commutative Ring; :: thesis: for I being Ideal of A
for p being prime Ideal of A st I c= p holds
sqrt I c= p
let I be Ideal of A; :: thesis: for p being prime Ideal of A st I c= p holds
sqrt I c= p
let p be prime Ideal of A; :: thesis: ( I c= p implies sqrt I c= p )
assume A1: I c= p ; :: thesis: sqrt I c= p
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in sqrt I or s in p )
assume A2: s in sqrt I ; :: thesis: s in p
then reconsider s = s as Element of A ;
s in { a where a is Element of A : ex n being Element of NAT st a |^ n in I } by A2, IDEAL_1:def 24;
then consider s1 being Element of A such that
A3: s1 = s and
A4: ex n being Element of NAT st s1 |^ n in I ;
consider n1 being Element of NAT such that
A5: s1 |^ n1 in I by A4;
n1 <> 0

proof

assume n1 = 0 ; :: thesis: contradiction
then s1 |^ n1 = 1_ A by BINOM:8;
hence contradiction by A1, A5, IDEAL_1:19; :: thesis: verum

end;

then reconsider n1 = n1 as non zero Nat ;
s1 |^ n1 in p by A1, A5;
hence s in p by A3, Th23; :: thesis: verum