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 q holds
q % ({x} -Ideal) in PRIMARY (A,p)
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 q holds
q % ({x} -Ideal) in PRIMARY (A,p)
let q be Ideal of A; :: thesis: for x being Element of A st q in PRIMARY (A,p) & not x in q holds
q % ({x} -Ideal) in PRIMARY (A,p)
let x be Element of A; :: thesis: ( q in PRIMARY (A,p) & not x in q implies q % ({x} -Ideal) in PRIMARY (A,p) )
assume A1: q in PRIMARY (A,p) ; :: thesis: ( x in q or q % ({x} -Ideal) in PRIMARY (A,p) )
set I = {x} -Ideal ;
consider q1 being primary Ideal of A such that
A2: q1 = q and
A3: q1 is p -primary by A1;
set M = { a where a is Element of A : a * ({x} -Ideal) c= q } ;
reconsider J = q % ({x} -Ideal) as Ideal of A ;
( not x in q implies q % ({x} -Ideal) in PRIMARY (A,p) )

proof

assume A4: not x in q ; :: thesis: q % ({x} -Ideal) in PRIMARY (A,p)
not 1. A in q % ({x} -Ideal)

proof

assume 1. A in q % ({x} -Ideal) ; :: thesis: contradiction
then 1. A in { a where a is Element of A : a * ({x} -Ideal) c= q } by IDEAL_1:def 23;
then consider y1 being Element of A such that
A6: 1. A = y1 and
A7: y1 * ({x} -Ideal) c= q ;
{x} -Ideal c= q by A7, A6, IDEAL_1:71;
hence contradiction by A4, IDEAL_1:66; :: thesis: verum

end;

then A9: q % ({x} -Ideal) is proper ;
for y being Element of A st y in q % ({x} -Ideal) holds
y in p

proof

let y be Element of A; :: thesis: ( y in q % ({x} -Ideal) implies y in p )
assume y in q % ({x} -Ideal) ; :: thesis: y in p
then y in { a where a is Element of A : a * ({x} -Ideal) c= q } by IDEAL_1:def 23;
then consider y1 being Element of A such that
A11: y1 = y and
A12: y1 * ({x} -Ideal) c= q ;
x in {x} -Ideal by IDEAL_1:66;
then A14: y1 * x in { (y1 * i) where i is Element of A : i in {x} -Ideal } ;
y1 * x in y1 * ({x} -Ideal) by A14, IDEAL_1:def 18;
hence y in p by A11, A3, Th33, A4, A2, A12; :: thesis: verum

end;

then A16: q % ({x} -Ideal) c= p ;
A17: p = sqrt (q % ({x} -Ideal)) by A16, TOPZARI1:25, A3, A2, A9, TOPZARI1:21, IDEAL_1:85;
set Q = q % ({x} -Ideal);
reconsider Q = q % ({x} -Ideal) as proper Ideal of A by A9;
A18: for a, b being Element of A st a * b in Q & not b in p holds
a in Q

proof

let a, b be Element of A; :: thesis: ( a * b in Q & not b in p implies a in Q )
assume A19: ( a * b in Q & not b in p ) ; :: thesis: a in Q
then a * b in { a where a is Element of A : a * ({x} -Ideal) c= q } by IDEAL_1:def 23;
then consider ab1 being Element of A such that
A20: ab1 = a * b and
A21: ab1 * ({x} -Ideal) c= q1 by A2;
A22: for i being Element of A st i in {x} -Ideal holds
a * i in q1

proof

let i be Element of A; :: thesis: ( i in {x} -Ideal implies a * i in q1 )
assume i in {x} -Ideal ; :: thesis: a * i in q1
then ab1 * i in { (ab1 * i1) where i1 is Element of A : i1 in {x} -Ideal } ;
then A24: ab1 * i in ab1 * ({x} -Ideal) by IDEAL_1:def 18;
(a * b) * i = (i * a) * b by GROUP_1:def 3;
hence a * i in q1 by A3, Def4, A20, A21, A24, A19; :: thesis: verum

end;

a * ({x} -Ideal) c= q

proof

for z being object st z in a * ({x} -Ideal) holds
z in q1

proof

let z be object ; :: thesis: ( z in a * ({x} -Ideal) implies z in q1 )
assume z in a * ({x} -Ideal) ; :: thesis: z in q1
then z in { (a * i1) where i1 is Element of A : i1 in {x} -Ideal } by IDEAL_1:def 18;
then consider i0 being Element of A such that
A27: z = a * i0 and
A28: i0 in {x} -Ideal ;
thus z in q1 by A27, A28, A22; :: thesis: verum

end;

hence a * ({x} -Ideal) c= q by A2; :: thesis: verum

end;

then a in { y where y is Element of A : y * ({x} -Ideal) c= q } ;
hence a in Q by IDEAL_1:def 23; :: thesis: verum

end;

reconsider Q = Q as primary Ideal of A by A18, A17, Th45;
Q is p -primary by A17;
hence q % ({x} -Ideal) in PRIMARY (A,p) ; :: thesis: verum

end;

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