:: deftheorem defines \& MMLQUERY:def 3 :
for X being set
for O being Operation of X
for L being List of X holds L \& O = meet { (x . O) where x is Element of X : x in L } ;