let X be set ; :: thesis: bool X is Filter of (BoolePoset X)
bool X c= the carrier of (BoolePoset X) by WAYBEL_7:4;
then reconsider A = bool X as non empty Subset of (BoolePoset X) ;
for x, y being set st x c= y & y c= X & x in A holds
y in A ;
then A1: A is upper by WAYBEL_7:11;

now

let x, y be set ; :: thesis: ( x in A & y in A implies x /\ y in A )
assume that
A2: x in A and
A3: y in A ; :: thesis: x /\ y in A
x /\ y c= X /\ X by A2, A3, XBOOLE_1:27;
hence x /\ y in A ; :: thesis: verum

end;

hence bool X is Filter of (BoolePoset X) by A1, WAYBEL_7:13; :: thesis: verum