Theorem 1

The relation $(\forall x)(x \notin X)$ is functional in X.

For the relation $(\forall x)(x \notin X)$ implies $(\forall Y)(X \subset Y)$; by virtue of the axiom of extent, the relation $(\forall x)(x \notin X)$ is therefore single-valued in X. On the other hand, the relation $(\forall x)(x \notin \complement_Y Y)$ is true, which proves that $(\exists X)(\forall x)(x \notin X)$ is true.

¶ The term $\tau_x((\forall x)(x \notin X))$ corresponding to this functional relation is represented by the functional symbol $\emptyset$, and is called the empty set [^1]; the relation $(\forall x)(x \notin X)$, which is equivalent to $X = \emptyset$, is read as follows: "*the set* X is empty". We have the theorems $x \notin \emptyset$, $\emptyset \subset X$, $\complement_X X = \emptyset$, $\complement_X \emptyset = X$. The relation $X \subset \emptyset$ is equivalent to $X = \emptyset$. If $R\{x\}$ is a relation, the relation $(\forall x)((x \in \emptyset) \Rightarrow R\{x\})$ is true.