let R be non empty right_complementable Abelian add-associative right_zeroed left-distributive left_unital left_zeroed doubleLoopStr ; :: thesis: for I being non empty add-closed left-ideal Subset of R
for J being Subset of R
for K being non empty Subset of R st J c= I holds
I /\ (J + K) = J + (I /\ K)
let I be non empty add-closed left-ideal Subset of R; :: thesis: for J being Subset of R
for K being non empty Subset of R st J c= I holds
I /\ (J + K) = J + (I /\ K)
let J be Subset of R; :: thesis: for K being non empty Subset of R st J c= I holds
I /\ (J + K) = J + (I /\ K)
let K be non empty Subset of R; :: thesis: ( J c= I implies I /\ (J + K) = J + (I /\ K) )
assume A1: J c= I ; :: thesis: I /\ (J + K) = J + (I /\ K)

A2: now

let u be set ; :: thesis: ( u in J + (I /\ K) implies u in I /\ (J + K) )
assume u in J + (I /\ K) ; :: thesis: u in I /\ (J + K)
then consider j, ik being Element of R such that
A3: u = j + ik and
A4: j in J and
A5: ik in I /\ K ;
A6: ex z being Element of R st
( z = ik & z in I & z in K ) by A5;
then reconsider k' = ik as Element of K ;
u = j + k' by A3;
then A7: u in J + K by A4;
reconsider j' = j as Element of I by A1, A4;
reconsider i' = ik as Element of I by A6;
u = j' + i' by A3;
then u in I by Def1;
hence u in I /\ (J + K) by A7; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in I /\ (J + K) implies u in J + (I /\ K) )
assume u in I /\ (J + K) ; :: thesis: u in J + (I /\ K)
then consider v being Element of R such that
A8: u = v and
A9: v in I and
A10: v in J + K ;
consider j, k being Element of R such that
A11: v = j + k and
A12: j in J and
A13: k in K by A10;
reconsider j' = j as Element of I by A1, A12;
- j' in I by Th13;
then (j' + k) + (- j') in I by A9, A11, Def1;
then (j' + (- j')) + k in I by RLVECT_1:def 6;
then (0. R) + k in I by RLVECT_1:16;
then k in I by ALGSTR_1:def 5;
then k in I /\ K by A13;
hence u in J + (I /\ K) by A8, A11, A12; :: thesis: verum

end;

hence I /\ (J + K) = J + (I /\ K) by A2, TARSKI:2; :: thesis: verum