theorem Th73: :: IDEAL_1:73

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