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