let A be non degenerated commutative Ring; :: thesis: for I being Ideal of A
for p being prime Ideal of A st sqrt I c= p holds
I c= p
let I be Ideal of A; :: thesis: for p being prime Ideal of A st sqrt I c= p holds
I c= p
let p be prime Ideal of A; :: thesis: ( sqrt I c= p implies I c= p )
assume A1: sqrt I c= p ; :: thesis: I c= p
I c= sqrt I by Th30;
hence I c= p by A1; :: thesis: verum