Singleton of Set is Filter in Lattice of Power Set

Theorem

Let $X$ be a set.

Let $L = \struct {\powerset X, \cup, \cap, \subseteq}$ be an inclusion lattice of power set of $X$.

Then $\set X$ is a filter on $L$.

Proof

By Singleton is Directed and Filtered Subset:

$\set X$ is filtered.

We will prove that

$\set X$ is an upper section.

Let $x \in \set X$, $y \in \powerset X$ such that:

$x \subseteq y$

By definition of singleton:

$x = X$

By definition of power set:

$y \subseteq X$

By definition of set equality:

$y = X$

Thus:

$y \in \set X$

$\Box$

Thus by definition of filter in ordered set:

$\set X$ is a filter.

$\blacksquare$

Sources

• Mizar article WAYBEL16:12