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 DEFFILT, XBOOLE_1:36;
hence O1 c= id X by XBOOLE_1:1; :: according to MMLQUERY:def 21 :: thesis: verum