:: deftheorem defines | MMLQUERY:def 19 :
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₄ = (L | O1) | O2 );