for R being non empty add-cancelable Abelian add-associative right_zeroed distributive associative commutative left_zeroed doubleLoopStr
for I, J being non empty right-ideal Subset of R holds (I + J) *' (I /\ J) c= I *' J