let X be infinite set ; :: thesis: for F being being_ultrafilter Filter of X
for Y being Subset of X holds
( Y in F iff not Y in dual F )
let F be being_ultrafilter Filter of X; :: thesis: for Y being Subset of X holds
( Y in F iff not Y in dual F )
let Y be Subset of X; :: thesis: ( Y in F iff not Y in dual F )
thus ( Y in F implies not Y in dual F ) :: thesis: ( not Y in dual F implies Y in F )

proof

assume Y in F ; :: thesis: not Y in dual F
then not Y ` in F by Th6;
hence not Y in dual F by SETFAM_1:def 7; :: thesis: verum

end;

assume not Y in dual F ; :: thesis: Y in F
then not Y ` in F by SETFAM_1:def 7;
hence Y in F by Def7; :: thesis: verum