let X be set ; :: thesis: for F1, F2 being filtering Operation of X holds NOT (F1 AND F2) = (NOT F1) OR (NOT F2)
let F1, F2 be filtering Operation of X; :: thesis: NOT (F1 AND F2) = (NOT F1) OR (NOT F2)
A1: ( F1 = id (dom F1) & F2 = id (dom F2) ) by Th45;
NOT (F1 AND F2) = id (X \ (dom (F1 AND F2))) by Th37
.= id (X \ (dom (id ((dom F1) AND (dom F2))))) by A1, SYSREL:14
.= id (X \ ((dom F1) AND (dom F2))) by RELAT_1:45
.= id ((X \ (dom F1)) \/ (X \ (dom F2))) by XBOOLE_1:54
.= (id (X \ (dom F1))) \/ (id (X \ (dom F2))) by SYSREL:14
.= (NOT F1) \/ (id (X \ (dom F2))) by Th37 ;
hence NOT (F1 AND F2) = (NOT F1) OR (NOT F2) by Th37; :: thesis: verum