let A be non degenerated commutative Ring; :: thesis: for I being Ideal of A
for J being proper Ideal of A st I c= J holds
sqrt I c= sqrt J
let I be Ideal of A; :: thesis: for J being proper Ideal of A st I c= J holds
sqrt I c= sqrt J
let J be proper Ideal of A; :: thesis: ( I c= J implies sqrt I c= sqrt J )
assume A1: I c= J ; :: thesis: sqrt I c= sqrt J
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in sqrt I or s in sqrt J )
assume A2: s in sqrt I ; :: thesis: s in sqrt J
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 in { a where a is Element of A : ex n being Element of NAT st a |^ n in J } by A1, A5;
hence s in sqrt J by A3, IDEAL_1:def 24; :: thesis: verum