let X be non empty set ; :: thesis: for Y being Subset of X

for F being Filter of X st Y in F holds

not X \ Y in F

let Y be Subset of X; :: thesis: for F being Filter of X st Y in F holds

not X \ Y in F

let F be Filter of X; :: thesis: ( Y in F implies not X \ Y in F )

assume A1: Y in F ; :: thesis: not X \ Y in F

assume X \ Y in F ; :: thesis: contradiction

then A2: Y /\ (X \ Y) in F by A1, Def1;

Y misses X \ Y by XBOOLE_1:79;

then {} in F by A2;

hence contradiction by Def1; :: thesis: verum

for F being Filter of X st Y in F holds

not X \ Y in F

let Y be Subset of X; :: thesis: for F being Filter of X st Y in F holds

not X \ Y in F

let F be Filter of X; :: thesis: ( Y in F implies not X \ Y in F )

assume A1: Y in F ; :: thesis: not X \ Y in F

assume X \ Y in F ; :: thesis: contradiction

then A2: Y /\ (X \ Y) in F by A1, Def1;

Y misses X \ Y by XBOOLE_1:79;

then {} in F by A2;

hence contradiction by Def1; :: thesis: verum