:: deftheorem Def21 defines filtering MMLQUERY:def 21 :
for X being set
for O being Operation of X holds
( O is filtering iff O c= id X );