theorem :: MMLQUERY:22

for X being set
for L1, L2 being List of X
for O1, O2 being Operation of X st O1 c= O2 & L1 c= L2 holds
L1 WHERE O1 c= L2 WHERE O2