let O1 be Operation of X; :: thesis: ( O1 = F BUTNOT O implies O1 is filtering )
assume O1 = F BUTNOT O ; :: thesis: O1 is filtering
then ( O1 c= F & F c= id X ) by Def21, XBOOLE_1:36;
hence O1 c= id X ; :: according to MMLQUERY:def 21 :: thesis: verum