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