let X be non empty set ; :: thesis: for F being Filter of X
for I being Ideal of X holds
( ( for Y being Subset of X holds
( not Y in F or not Y in dual F ) ) & ( for Y being Subset of X holds
( not Y in I or not Y in dual I ) ) )
let F be Filter of X; :: thesis: for I being Ideal of X holds
( ( for Y being Subset of X holds
( not Y in F or not Y in dual F ) ) & ( for Y being Subset of X holds
( not Y in I or not Y in dual I ) ) )
let I be Ideal of X; :: thesis: ( ( for Y being Subset of X holds
( not Y in F or not Y in dual F ) ) & ( for Y being Subset of X holds
( not Y in I or not Y in dual I ) ) )
thus for Y being Subset of X holds
( not Y in F or not Y in dual F ) :: thesis: for Y being Subset of X holds
( not Y in I or not Y in dual I )

proof

let Y be Subset of X; :: thesis: ( not Y in F or not Y in dual F )
assume A1: ( Y in F & Y in dual F ) ; :: thesis: contradiction
then Y ` in F by SETFAM_1:def 8;
then A2: (Y ` ) /\ Y in F by A1, Def1;
Y ` misses Y by XBOOLE_1:79;
then {} X in F by A2, XBOOLE_0:def 7;
hence contradiction by Def1; :: thesis: verum

end;

let Y be Subset of X; :: thesis: ( not Y in I or not Y in dual I )
assume A3: ( Y in I & Y in dual I ) ; :: thesis: contradiction
then Y ` in I by SETFAM_1:def 8;
then (Y ` ) \/ Y in I by A3, Def2;
then [#] X in I by SUBSET_1:25;
hence contradiction by Def2; :: thesis: verum