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