let X be set ; :: thesis:

let c be object ; :: thesis:
assume c in {X} ; :: thesis:
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:

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

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

end;

then A3: A is upper by WAYBEL_7:7;

let x, y be set ; :: thesis:
assume ( x in A & y in A ) ; :: thesis:
then ( x = X & y = X ) by TARSKI:def 1;
hence x /\ y in A by TARSKI:def 1; :: thesis:

end;

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