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:64;
F \ {{} } = a_filter (a_net F) by Th14;
hence ( B in F iff a_net F is_eventually_in B ) by A1, Th11; :: thesis: verum