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

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