let X be set ; :: thesis: {X} is Filter of (BoolePoset X)

now :: thesis: for c being object st c in {X} holds
c in the carrier of (BoolePoset X)

let c be object ; :: thesis: ( c in {X} implies c in the carrier of (BoolePoset X) )
assume c in {X} ; :: thesis: c in the carrier of (BoolePoset X)
then c = X by TARSKI:def 1;
then c is Element of (BoolePoset X) by WAYBEL_8:26;
hence c in the carrier of (BoolePoset X) ; :: thesis: verum

end;

then reconsider A = {X} as non empty Subset of (BoolePoset X) by TARSKI:def 3;
for x, y being set st x c= y & y c= X & x in A holds
y in A

proof

let x, y be set ; :: thesis: ( x c= y & y c= X & x in A implies y in A )
assume that
A1: ( x c= y & y c= X ) and
A2: x in A ; :: thesis: y in A
x = X by A2, TARSKI:def 1;
then y = X by A1;
hence y in A by TARSKI:def 1; :: thesis: verum

end;

then A3: A is upper by WAYBEL_7:7;

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 = X & y = X ) by TARSKI:def 1;
hence x /\ y in A by TARSKI:def 1; :: thesis: verum

end;

hence {X} is Filter of (BoolePoset X) by A3, WAYBEL_7:9; :: thesis: verum