let A be non degenerated commutative Ring; :: thesis: for I being Ideal of A holds
( I is primary iff ( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds
y in sqrt I ) ) )
let I be Ideal of A; :: thesis: ( I is primary iff ( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds
y in sqrt I ) ) )
( I <> [#] A & ( for a1, a2 being Element of A st a1 * a2 in I & not a1 in I holds
a2 in sqrt I ) implies I is primary )

proof

assume A1: ( I <> [#] A & ( for a1, a2 being Element of A st a1 * a2 in I & not a1 in I holds
a2 in sqrt I ) ) ; :: thesis: I is primary
then A2: I is quasi-primary ;
I is proper by A1;
hence I is primary by A2; :: thesis: verum

end;

hence ( I is primary iff ( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds
y in sqrt I ) ) ) by Def4; :: thesis: verum