Then
\begin{equation}
\emptyset \subseteq X
\end{equation}

Result R7
on D13: Empty set

Empty set is subset of every set

Formulation 2

Let $X$ be a D11: Set such that

Let $\emptyset$ be the D13: Empty set.

(i) | $\mathcal{P}(X)$ is the D80: Power set of $X$ |

Then
\begin{equation}
\emptyset \in \mathcal{P}(X)
\end{equation}

Proofs

If $X = \emptyset$, then the claim follows from R125: Subset relation is reflexive.

Consider then the case $X \neq \emptyset$. For $\emptyset$*not* to be a subset of $X$ would require the existence of an element of $\emptyset$ that does not belong to $X$. If such an element were to exist, that would imply that $\emptyset$ is not empty, which is a contradiction. Hence, such element does not exist and therefore $\emptyset$ is a subset of $X$.

Consider then the case $X \neq \emptyset$. For $\emptyset$