theorem :: IDEAL_1:76

for R being non empty add-cancelable Abelian add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr
for a, b being Element of R holds {a,b} -Ideal = ({a} -Ideal) + ({b} -Ideal)