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