let O1 be Operation of X; :: thesis: ( O1 = F1 OR F2 implies O1 is filtering )

assume A1: O1 = F1 OR F2 ; :: thesis: O1 is filtering

( F1 c= id X & F2 c= id X ) by Def21;

hence O1 c= id X by A1, XBOOLE_1:8; :: according to MMLQUERY:def 21 :: thesis: verum

assume A1: O1 = F1 OR F2 ; :: thesis: O1 is filtering

( F1 c= id X & F2 c= id X ) by Def21;

hence O1 c= id X by A1, XBOOLE_1:8; :: according to MMLQUERY:def 21 :: thesis: verum