let T be non empty 1-sorted ; :: thesis: for F being proper Filter of (BoolePoset ([#] T)) holds F = a_filter (a_net F)
let F be proper Filter of (BoolePoset ([#] T)); :: thesis: F = a_filter (a_net F)
not {} in F by Th1;
then F \ {{}} = F by ZFMISC_1:57;
hence F = a_filter (a_net F) by Th13; :: thesis: verum