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