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