:: deftheorem defines WHERE MMLQUERY:def 4 :
for X being set
for O being Operation of X
for L being List of X holds L WHERE O = { x where x is Element of X : ex y being Element of X st
( x,y in O & x in L ) } ;