:: deftheorem defines WHEREeq MMLQUERY:def 5 :
for X being set
for O being Operation of X
for L being List of X
for O2 being Operation of X holds L WHEREeq (O,O2) = { x where x is Element of X : ( card (x . O) = card (x . O2) & x in L ) } ;