# Singleton of Power Set less Empty Set is Minimal Subset

## Theorem

Let $S$ be a set which is non-empty.

Let $\CC = \powerset S \setminus \O$, that is, the power set of $S$ without the empty set.

Let $x \in S$.

Then $\set x$ is a minimal element of the ordered structure $\struct {\CC, \subseteq}$.

## Proof

Let $y \in \CC$ such that $y \subseteq \set x$.

We have that $\O \notin \CC$.

Therefore:

$\exists z \in S: z \in y$

But as $y \subseteq \set x$ it follows that:

$z \in \set x$

and so by definition of singleton:

$z = x$

and so:

$y = \set x$

and so:

$y = x$

Thus, by definition, $\set x$ is a minimal element of $\struct {\CC, \subseteq}$.

$\blacksquare$