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 )

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

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 I or not Y in dual I )
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;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

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