theorem :: GROUP_2:15
for G being non empty multMagma
for A, B, C being Subset of G holds (A /\ B) * C c= (A * C) /\ (B * C)