:: deftheorem Def20 defines \& MMLQUERY:def 20 :
for X being set
for O1, O2, b₄ being Operation of X holds
( b₄ = O1 \& O2 iff for L being List of X holds L | b₄ = union { ((x . O1) \& O2) where x is Element of X : x in L } );