let A be non degenerated commutative Ring; :: thesis: for q being Ideal of A
for x being Element of A st x in q holds
q % ({x} -Ideal) = [#] A
let q be Ideal of A; :: thesis: for x being Element of A st x in q holds
q % ({x} -Ideal) = [#] A
let x be Element of A; :: thesis: ( x in q implies q % ({x} -Ideal) = [#] A )
set I = {x} -Ideal ;
( x in q implies q % ({x} -Ideal) = [#] A )

proof

assume A2: x in q ; :: thesis: q % ({x} -Ideal) = [#] A
1. A in q % ({x} -Ideal)

proof

q = q -Ideal by IDEAL_1:44;
then A4: {x} -Ideal c= q by A2, IDEAL_1:67;
(1. A) * ({x} -Ideal) c= q by A4, IDEAL_1:71;
then 1. A in { a where a is Element of A : a * ({x} -Ideal) c= q } ;
hence 1. A in q % ({x} -Ideal) by IDEAL_1:def 23; :: thesis: verum

end;

then not q % ({x} -Ideal) is proper by IDEAL_1:19;
hence q % ({x} -Ideal) = [#] A ; :: thesis: verum

end;

hence ( x in q implies q % ({x} -Ideal) = [#] A ) ; :: thesis: verum