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 )

then not Y ` in F by SETFAM_1:def 7;

hence Y in F by Def7; :: thesis: verum

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
not Y in dual F
; :: thesis: Y in F
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;then not Y ` in F by Th6;

hence not Y in dual F by SETFAM_1:def 7; :: thesis: verum

then not Y ` in F by SETFAM_1:def 7;

hence Y in F by Def7; :: thesis: verum