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