theorem :: IDEAL_1:92

for R being non empty add-cancelable right_zeroed well-unital distributive associative 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 sqrt (I *' J) = sqrt (I /\ J)