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 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
A3: ( u = v & v in I & v in J + K ) ;
consider j, k being Element of R such that
A4: ( v = j + k & j in J & k in K ) by A3;
reconsider j' = j as Element of I by A1, A4;
- j' in I by Th13;
then (j' + k) + (- j') in I by A3, A4, 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 A4;
hence u in J + (I /\ K) by A3, A4; :: thesis: verum

end;

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
A5: ( u = j + ik & j in J & ik in I /\ K ) ;
consider z being Element of R such that
A6: ( z = ik & z in I & z in K ) by A5;
reconsider i' = ik as Element of I by A6;
reconsider k' = ik as Element of K by A6;
reconsider j' = j as Element of I by A1, A5;
u = j' + i' by A5;
then A7: u in I by Def1;
u = j + k' by A5;
then u in J + K by A5;
hence u in I /\ (J + K) by A7; :: thesis: verum

end;

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