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