let T be non empty TopSpace; :: thesis: for F being Filter of the carrier of T ex F1 being proper Filter of (BoolePoset the carrier of T) st F = F1
let F be Filter of the carrier of T; :: thesis: ex F1 being proper Filter of (BoolePoset the carrier of T) st F = F1
reconsider F1 = F as non empty Subset of (BooleLatt the carrier of T) by LATTICE3:def 1;
A1: F1 is Filter of (BoolePoset the carrier of T) by Th33, Th35;
not {} in F by CARD_FIL:def 1;
then not Bottom (BoolePoset the carrier of T) in F1 by YELLOW_1:18;
then F1 is proper ;
hence ex F1 being proper Filter of (BoolePoset the carrier of T) st F = F1 by A1; :: thesis: verum