theorem :: MMLQUERY:21

for X being set
for L being List of X
for O, O1 being Operation of X holds L WHEREgt (O,O1) c= L WHERE O