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