theorem Th64: :: IDEAL_1:64

for R being non empty add-cancelable add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr
for a being Element of R holds {a} -Ideal = { (a * r) where r is Element of R : verum }