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 that
A1: Y in F and
A2: Y in dual F ; :: thesis: contradiction
Y ` in F by A2, SETFAM_1:def 7;
then A3: (Y `) /\ Y in F by A1, Def1;
Y ` misses Y by XBOOLE_1:79;
then {} X in F by A3;
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 that
A4: Y in I and
A5: Y in dual I ; :: thesis: contradiction
Y ` in I by A5, SETFAM_1:def 7;
then (Y `) \/ Y in I by A4, Def2;
then [#] X in I by SUBSET_1:10;
hence contradiction by Def2; :: thesis: verum