let X be set ; :: thesis: for F being filtering Operation of X holds F OR (NOT F) = id X
let F be filtering Operation of X; :: thesis: F OR (NOT F) = id X
( dom (F OR (NOT F)) = X & F OR (NOT F) c= id X ) by Th50, Def21;
hence F OR (NOT F) = id X by SYSREL:17; :: thesis: verum