theorem Th65: :: IDEAL_1:65

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 * r) + (b * s)) where r, s is Element of R : verum }