for R being non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr
for I, J being non empty add-closed left-ideal Subset of R holds (I + J) *' (I /\ J) c= I /\ J