theorem Th8: :: MMLQUERY:8

for X being set
for L1, L2 being List of X
for O being Operation of X
for n being Nat st L1 c= L2 holds
L1 WHEREgt (O,n) c= L2 WHERE O