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

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