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