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

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