let T be non empty 1-sorted ; :: thesis: for F being Filter of (BoolePoset ([#] T))
for A being non empty Subset of T holds
( A in F iff a_net F is_eventually_in A )
let F be Filter of (BoolePoset ([#] T)); :: thesis: for A being non empty Subset of T holds
( A in F iff a_net F is_eventually_in A )
let B be non empty Subset of T; :: thesis: ( B in F iff a_net F is_eventually_in B )
A1: ( B in F iff B in F \ {{}} ) by ZFMISC_1:56;
F \ {{}} = a_filter (a_net F) by Th13;
hence ( B in F iff a_net F is_eventually_in B ) by A1, Th10; :: thesis: verum