let G be non empty addMagma ; :: thesis: for A, B, C being Subset of G holds A + (B /\ C) c= (A + B) /\ (A + C)
let A, B, C be Subset of G; :: thesis: A + (B /\ C) c= (A + B) /\ (A + C)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A + (B /\ C) or x in (A + B) /\ (A + C) )
assume x in A + (B /\ C) ; :: thesis: x in (A + B) /\ (A + C)
then consider g1, g2 being Element of G such that
A1: ( x = g1 + g2 & g1 in A ) and
A2: g2 in B /\ C ;
g2 in C by A2, XBOOLE_0:def 4;
then A3: x in A + C by A1;
g2 in B by A2, XBOOLE_0:def 4;
then x in A + B by A1;
hence x in (A + B) /\ (A + C) by A3; :: thesis: verum