for X being set
for L1, L2 being List of X
for O being Operation of X
for n being Nat st n <> 0 & L1 c= L2 holds
L1 WHEREeq (O,n) c= L2 WHERE O