let X be non empty set ; :: thesis: for cF being Filter of X holds cF is proper Filter of (BoolePoset X)
let cF be Filter of X; :: thesis: cF is proper Filter of (BoolePoset X)
reconsider cF = cF as non empty Subset of (BooleLatt X) by LATTICE3:def 1;
reconsider cF = cF as Filter of (BoolePoset X) by CARDFIL2:73, CARDFIL2:75;
not {} in cF by CARD_FIL:def 1;
then not Bottom (BoolePoset X) in cF by YELLOW_1:18;
hence cF is proper Filter of (BoolePoset X) by WAYBEL_7:4; :: thesis: verum