let A be non degenerated commutative Ring; :: thesis: for J being proper Ideal of A holds sqrt J = meet (PrimeIdeals (A,J))
let J be proper Ideal of A; :: thesis: sqrt J = meet (PrimeIdeals (A,J))
for x being object st x in sqrt J holds
x in meet (PrimeIdeals (A,J))

proof

let x be object ; :: thesis: ( x in sqrt J implies x in meet (PrimeIdeals (A,J)) )
assume x in sqrt J ; :: thesis: x in meet (PrimeIdeals (A,J))
then x 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 y being Element of A such that
A2: y = x and
A3: ex n being Element of NAT st y |^ n in J ;
consider k being Element of NAT such that
A4: y |^ k in J by A3;
y in meet (PrimeIdeals (A,J))

proof

for Y being set st Y in PrimeIdeals (A,J) holds
y in Y

proof

let Y be set ; :: thesis: ( Y in PrimeIdeals (A,J) implies y in Y )
( Y in PrimeIdeals (A,J) implies y in Y )

proof

assume Y in PrimeIdeals (A,J) ; :: thesis: y in Y
then consider Y1 being prime Ideal of A such that
A6: Y1 = Y and
A7: J c= Y1 ;
reconsider k = k as non zero Nat by A4, A7, Lm24;
y |^ k in Y1 by A4, A7;
hence y in Y by A6, Th23; :: thesis: verum

end;

hence ( Y in PrimeIdeals (A,J) implies y in Y ) ; :: thesis: verum

end;

hence y in meet (PrimeIdeals (A,J)) by SETFAM_1:def 1; :: thesis: verum

end;

hence x in meet (PrimeIdeals (A,J)) by A2; :: thesis: verum

end;

then A9: sqrt J c= meet (PrimeIdeals (A,J)) ;
set N1 = meet (PrimeIdeals (A,J));
for x being object st not x in sqrt J holds
not x in meet (PrimeIdeals (A,J))

proof

let x be object ; :: thesis: ( not x in sqrt J implies not x in meet (PrimeIdeals (A,J)) )
assume A10: not x in sqrt J ; :: thesis: not x in meet (PrimeIdeals (A,J))

per cases ( x in A or not x in A ) ;

suppose x in A ; :: thesis: not x in meet (PrimeIdeals (A,J))

then reconsider x1 = x as Element of A ;
consider p being prime Ideal of A such that
A12: not x1 in p and
A13: J c= p by A10, Th9;
p in PrimeIdeals (A,J) by A13;
hence not x in meet (PrimeIdeals (A,J)) by A12, SETFAM_1:def 1; :: thesis: verum

end;

suppose A15: not x in A ; :: thesis: not x in meet (PrimeIdeals (A,J))

not x in meet (PrimeIdeals (A,J))

proof

assume A16: x in meet (PrimeIdeals (A,J)) ; :: thesis: contradiction
consider m being prime Ideal of A such that
A17: J c= m by Th11;
m in PrimeIdeals (A,J) by A17;
then x in m by A16, SETFAM_1:def 1;
hence contradiction by A15; :: thesis: verum

end;

hence not x in meet (PrimeIdeals (A,J)) ; :: thesis: verum

end;

end;

end;

then meet (PrimeIdeals (A,J)) c= sqrt J ;
hence sqrt J = meet (PrimeIdeals (A,J)) by A9; :: thesis: verum