let X be set ; :: thesis: for F being filtering Operation of X holds NOT (NOT F) = F
let F be filtering Operation of X; :: thesis: NOT (NOT F) = F
thus NOT (NOT F) = id (X \ (dom (NOT F))) by Th5
.= id (X \ (dom (id (X \ (dom F))))) by Th5
.= id (X \ (X \ (dom F))) by RELAT_1:45
.= id (X /\ (dom F)) by XBOOLE_1:48
.= id (dom F) by XBOOLE_1:28
.= F by Th20 ; :: thesis: verum