theorem :: MMLQUERY:15

for X being set
for L1, L2 being List of X
for O1, O2 being Operation of X
for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHEREle (O2,n) c= L2 WHEREle (O1,m)