let R be non empty add-cancelable Abelian add-associative right_zeroed associative commutative distributive left_unital 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 Th82;
assume I,J are_co-prime ; :: thesis: I *' J = I /\ J
then A2: I /\ J c= (I + J) *' (I /\ J) by Th86;
(I + J) *' (I /\ J) c= I *' J by Th84;
then I /\ J c= I *' J by A2, XBOOLE_1:1;
hence I *' J = I /\ J by A1, XBOOLE_0:def 10; :: thesis: verum