let A be non degenerated commutative Ring; :: thesis: for Q being primary Ideal of A holds
( sqrt Q is prime & ( for P being prime Ideal of A st Q c= P holds
sqrt Q c= P ) )
let Q be primary Ideal of A; :: thesis: ( sqrt Q is prime & ( for P being prime Ideal of A st Q c= P holds
sqrt Q c= P ) )
for x, y being Element of A holds
( not x * y in sqrt Q or x in sqrt Q or y in sqrt Q )

proof

set M = { a where a is Element of A : ex n being Element of NAT st a |^ n in Q } ;
let x, y be Element of A; :: thesis: ( not x * y in sqrt Q or x in sqrt Q or y in sqrt Q )
assume x * y in sqrt Q ; :: thesis: ( x in sqrt Q or y in sqrt Q )
then x * y in { a where a is Element of A : ex n being Element of NAT st a |^ n in Q } by IDEAL_1:def 24;
then consider z being Element of A such that
A2: z = x * y and
A3: ex n being Element of NAT st z |^ n in Q ;
consider n1 being Element of NAT such that
A4: z |^ n1 in Q by A3;
A5: (x |^ n1) * (y |^ n1) in Q by A4, A2, BINOM:9;
( x in sqrt Q or y in sqrt Q )

proof

per cases ( x |^ n1 in Q or y |^ n1 in sqrt Q ) by A5, Def4;

suppose x |^ n1 in Q ; :: thesis: ( x in sqrt Q or y in sqrt Q )

then x in { a where a is Element of A : ex n being Element of NAT st a |^ n in Q } ;
hence ( x in sqrt Q or y in sqrt Q ) by IDEAL_1:def 24; :: thesis: verum

end;

suppose y |^ n1 in sqrt Q ; :: thesis: ( x in sqrt Q or y in sqrt Q )

then y |^ n1 in { a where a is Element of A : ex n being Element of NAT st a |^ n in Q } by IDEAL_1:def 24;
then consider y1 being Element of A such that
A9: y1 = y |^ n1 and
A10: ex m being Element of NAT st y1 |^ m in Q ;
consider m1 being Element of NAT such that
A11: y1 |^ m1 in Q by A10;
reconsider n2 = n1 * m1 as Element of NAT ;
A12: y |^ n2 in Q by A9, A11, BINOM:11;
y in { a where a is Element of A : ex n being Element of NAT st a |^ n in Q } by A12;
hence ( x in sqrt Q or y in sqrt Q ) by IDEAL_1:def 24; :: thesis: verum

end;

end;

end;

hence ( x in sqrt Q or y in sqrt Q ) ; :: thesis: verum

end;

then A14: sqrt Q is quasi-prime ;
consider P being prime Ideal of A such that
A15: Q c= P by TOPZARI1:9;
P c< [#] A ;
then A17: sqrt Q is proper by A15, TOPZARI1:25, XBOOLE_1:59;
for P being prime Ideal of A st Q c= P holds
sqrt Q c= P

proof

let P be prime Ideal of A; :: thesis: ( Q c= P implies sqrt Q c= P )
assume Q c= P ; :: thesis: sqrt Q c= P
then P in { p where p is prime Ideal of A : Q c= p } ;
then P in PrimeIdeals (A,Q) by TOPZARI1:def 12;
then A19: meet (PrimeIdeals (A,Q)) c= P by SETFAM_1:3;
reconsider Q = Q as proper Ideal of A ;
thus sqrt Q c= P by A19, TOPZARI1:18; :: thesis: verum

end;

hence ( sqrt Q is prime & ( for P being prime Ideal of A st Q c= P holds
sqrt Q c= P ) ) by A14, A17; :: thesis: verum