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