for R being non empty left_unital left_zeroed doubleLoopStr
for I, J being non empty Subset of R st I,J are_co-prime holds
I /\ J c= (I + J) *' (I /\ J)