theorem :: IDEAL_1:67

for R being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr
for A being non empty Subset of R
for a being Element of R st a in A -Ideal holds
{a} -Ideal c= A -Ideal