for R being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr
for I being non empty add-closed right-ideal Subset of R
for J being Subset of R holds (I % J) *' J c= I