let X be set ; :: thesis: bool X is Filter of (BoolePoset X)
bool X c= the carrier of (BoolePoset X) by WAYBEL_7:2;
then reconsider A = bool X as non empty Subset of (BoolePoset X) ;
A1: now :: thesis: for x, y being set st x in A & y in A holds
x /\ y in A
let x, y be set ; :: thesis: ( x in A & y in A implies x /\ y in A )
assume ( x in A & y in A ) ; :: thesis: x /\ y in A
then x /\ y c= X /\ X by XBOOLE_1:27;
hence x /\ y in A ; :: thesis: verum
end;
for x, y being set st x c= y & y c= X & x in A holds
y in A ;
then A is upper by WAYBEL_7:7;
hence bool X is Filter of (BoolePoset X) by A1, WAYBEL_7:9; :: thesis: verum