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