for X being set
for L1, L2 being List of X
for O being Operation of X st L1 <> {} & L2 <> {} holds
(L1 OR L2) \& O = (L1 \& O) AND (L2 \& O)