theorem Th79: :: IDEAL_1:79

for R being non empty add-cancelable right_zeroed distributive left_zeroed doubleLoopStr
for I being non empty add-closed right-ideal Subset of R
for J being non empty add-closed left-ideal Subset of R holds I *' J c= I /\ J