:: deftheorem defines | MMLQUERY:def 2 :
for X being set
for O being Operation of X
for L being List of X holds L | O = union { (x . O) where x is Element of X : x in L } ;