theorem :: MMLQUERY:28

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