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 Th2;
then F \ {{} } = F by ZFMISC_1:65;
hence F = a_filter (a_net F) by Th14; :: thesis: verum