let A be non degenerated commutative Ring; :: thesis: for J being proper Ideal of A holds not 1. A in sqrt J
let J be proper Ideal of A; :: thesis: not 1. A in sqrt J
assume 1. A in sqrt J ; :: thesis: contradiction
then 1. A in { a where a is Element of A : ex n being Element of NAT st a |^ n in J } by IDEAL_1:def 24;
then consider a being Element of A such that
A3: 1. A = a and
A4: ex n being Element of NAT st a |^ n in J ;
consider n1 being Element of NAT such that
A5: a |^ n1 in J by A4;
1. A = a |^ n1 by A3, Lm4;
hence contradiction by IDEAL_1:19, A5; :: thesis: verum