theorem :: MMLQUERY:17

for X being set
for L1, L2 being List of X
for O, O1, O2, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds
L1 WHEREge (O,O2) c= L2 WHEREge (O3,O1)