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

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