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