let R be comRing; :: thesis: for I being Ideal of R
for a being Element of R st a in I holds
{a} -Ideal c= I
let I be Ideal of R; :: thesis: for a being Element of R st a in I holds
{a} -Ideal c= I
let a be Element of R; :: thesis: ( a in I implies {a} -Ideal c= I )
assume AS: a in I ; :: thesis: {a} -Ideal c= I
now :: thesis: for x being Element of R st x in {a} -Ideal holds
x in I
let x be Element of R; :: thesis: ( x in {a} -Ideal implies x in I )
assume A: x in {a} -Ideal ; :: thesis: x in I
{a} -Ideal = { (a * r) where r is Element of R : verum } by IDEAL_1:64;
then ex r being Element of R st x = a * r by A;
hence x in I by AS, IDEAL_1:def 2; :: thesis: verum
end;
hence {a} -Ideal c= I ; :: thesis: verum