let A be non degenerated commutative Ring; :: thesis: for Q being proper Ideal of A st ( for x, y being Element of A st x * y in Q & not y in sqrt Q holds
x in Q ) holds
( Q is primary & sqrt Q is prime )
let Q be proper Ideal of A; :: thesis: ( ( for x, y being Element of A st x * y in Q & not y in sqrt Q holds
x in Q ) implies ( Q is primary & sqrt Q is prime ) )
assume A3: for x, y being Element of A st x * y in Q & not y in sqrt Q holds
x in Q ; :: thesis: ( Q is primary & sqrt Q is prime )
not 1. A in sqrt Q by TOPZARI1:3;
then sqrt Q is proper ;
then reconsider P = sqrt Q as proper Ideal of A ;
reconsider Q = Q as proper Ideal of A ;
A2: ( Q c= P & P c= sqrt Q ) by TOPZARI1:20;
for x, y being Element of A st x * y in Q & not x in Q holds
y in P by A3;
hence ( Q is primary & sqrt Q is prime ) by A2, Th44; :: thesis: verum