theorem Th74: :: IDEAL_1:74

for R being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr
for I, J being non empty right-ideal Subset of R holds J c= I + J