let R be non empty add-cancelable Abelian add-associative right_zeroed distributive left_unital associative commutative left_zeroed doubleLoopStr ; :: thesis: 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
let I be non empty add-closed left-ideal right-ideal Subset of R; :: thesis: for J being non empty add-closed left-ideal Subset of R st I,J are_co-prime holds
I *' J = I /\ J
let J be non empty add-closed left-ideal Subset of R; :: thesis: ( I,J are_co-prime implies I *' J = I /\ J )
A1: I *' J c= I /\ J by Th79;
assume I,J are_co-prime ; :: thesis: I *' J = I /\ J
then A2: I /\ J c= (I + J) *' (I /\ J) by Th83;
(I + J) *' (I /\ J) c= I *' J by Th81;
then I /\ J c= I *' J by A2;
hence I *' J = I /\ J by A1; :: thesis: verum