let A be non degenerated commutative Ring; :: thesis: for p being prime Ideal of A
for q being Ideal of A
for x being Element of A st q in PRIMARY (A,p) & not x in p holds
q % ({x} -Ideal) = q
let p be prime Ideal of A; :: thesis: for q being Ideal of A
for x being Element of A st q in PRIMARY (A,p) & not x in p holds
q % ({x} -Ideal) = q
let q be Ideal of A; :: thesis: for x being Element of A st q in PRIMARY (A,p) & not x in p holds
q % ({x} -Ideal) = q
let x be Element of A; :: thesis: ( q in PRIMARY (A,p) & not x in p implies q % ({x} -Ideal) = q )
assume A1: q in PRIMARY (A,p) ; :: thesis: ( x in p or q % ({x} -Ideal) = q )
set I = {x} -Ideal ;
set M = { a where a is Element of A : a * ({x} -Ideal) c= q } ;
consider Q being primary Ideal of A such that
A2: Q = q and
A3: Q is p -primary by A1;
( not x in p implies q % ({x} -Ideal) = q )

proof

assume A4: not x in p ; :: thesis: q % ({x} -Ideal) = q
A5: for o being object st o in q % ({x} -Ideal) holds
o in q

proof

let o be object ; :: thesis: ( o in q % ({x} -Ideal) implies o in q )
assume o in q % ({x} -Ideal) ; :: thesis: o in q
then o in { a where a is Element of A : a * ({x} -Ideal) c= q } by IDEAL_1:def 23;
then consider o1 being Element of A such that
A7: o1 = o and
A8: o1 * ({x} -Ideal) c= q ;
x in {x} -Ideal by IDEAL_1:66;
then o1 * x in { (o1 * i1) where i1 is Element of A : i1 in {x} -Ideal } ;
then o1 * x in o1 * ({x} -Ideal) by IDEAL_1:def 18;
hence o in q by A7, Def4, A2, A3, A4, A8; :: thesis: verum

end;

q % ({x} -Ideal) c= q by A5;
hence q % ({x} -Ideal) = q by IDEAL_1:85; :: thesis: verum

end;

hence ( x in p or q % ({x} -Ideal) = q ) ; :: thesis: verum