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