let A be non degenerated commutative Ring; :: thesis: for p being Ideal of A st p is prime holds
p is primary
let p be Ideal of A; :: thesis: ( p is prime implies p is primary )
assume p is prime ; :: thesis: p is primary
then reconsider p = p as prime Ideal of A ;
for x, y being Element of A holds
( not x * y in p or x in p or y in sqrt p )
proof
let x, y be Element of A; :: thesis: ( not x * y in p or x in p or y in sqrt p )
assume x * y in p ; :: thesis: ( x in p or y in sqrt p )
then A3: ( x in p or y in p ) by RING_1:def 1;
p c= sqrt p by TOPZARI1:20;
hence ( x in p or y in sqrt p ) by A3; :: thesis: verum
end;
hence p is primary by Def4; :: thesis: verum