for R being non empty add-cancelable Abelian add-associative right_zeroed distributive left_unital associative commutative left_zeroed doubleLoopStr
for I being non empty add-closed left-ideal right-ideal Subset of R
for J being non empty add-closed left-ideal Subset of R st I,J are_co-prime holds
I *' J = I /\ J