let X be non empty set ; :: thesis: for F being proper Filter of (BoolePoset X) holds F is Filter of X
let F be proper Filter of (BoolePoset X); :: thesis: F is Filter of X
A1: F is with_non-empty_elements
proof
assume not F is with_non-empty_elements ; :: thesis: contradiction
then Bottom (BoolePoset X) in F by YELLOW_1:18;
hence contradiction by WAYBEL_7:4; :: thesis: verum
end;
reconsider F = F as non empty Subset of (BooleLatt X) ;
thus F is Filter of X by A1, Th34, Th35; :: thesis: verum