let A be non degenerated commutative Ring; :: thesis:
let I, J be proper Ideal of A; :: thesis:
assume that
A1: ( I c= J & J c= sqrt I ) and
A2: for x, y being Element of A st x * y in I & not x in I holds
y in J ; :: thesis:
for x, y being Element of A st x * y in I & not x in I holds
y in sqrt I by A1, A2;
then A3: I is primary by Def4;
sqrt I c= J

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in sqrt I ; :: thesis:
then reconsider x0 = x as Element of sqrt I ;
consider m being Nat such that
A5: ( m in { n where n is Element of NAT : not x0 |^ n in I } & x0 |^ (m + 1) in I ) by Th43;
consider m0 being Element of NAT such that
A6: ( m0 = m & not x0 |^ m0 in I ) by A5;

end;

reconsider x0 = x0 as Element of A ;
x0 |^ (m + 1) = (x0 |^ m) * (x0 |^ 1) by BINOM:10
.= (x0 |^ m) * x0 by BINOM:8 ;
hence x in J by A2, A5, A6; :: thesis:

end;