Definition 1

The relation denoted by $(\forall z)((z \in x) \Rightarrow (z \in y))$, in which only the letters $x$ and $y$ appear, is written in one of the following ways : $x \subset y$, $y \supset x$, "$x$ is contained in $y$", "$y$ contains $x$", "$x$ is a subset of $y$". The relation "not $(x \subset y)$" is written $x \not\subset y$ or $y \not\supset x$.

In accordance with the conventions mentioned in Chapter I, § 1, no. 1, this definition entails the following metamathematical convention. Let $T$ and $U$ be assemblies; if we substitute $T$ for $x$ and $U$ for $y$ in the assembly $x \subset y$, we obtain an assembly which is denoted by $T \subset U$; if we denote by $\mathbf{x}$, $\mathbf{y}$ letters which are distinct from $x$, $y$ and distinct from each other, and which appear neither in $T$ nor in $U$, the assembly $T \subset U$ is then identical with $(T|\mathbf{x})(U|\mathbf{y})(\mathbf{x}|x)(\mathbf{y}|y)(x \subset y)$ and hence by CS8, CS9 (Chapter I, § 4, no. 1), and CS5 (Chapter I, § 1, no. 2) with $(\forall z)((z \in T) \Rightarrow (z \in U))$, provided that $z$ is a letter which appears neither in $T$ nor in $U$.

From now on, whenever we state a mathematical definition, we shall not mention the metamathematical convention which it entails.

CS12. Let $T$, $U$, $V$ be assemblies and let $x$ be a letter. Then the assembly $(V|x)(T \subset U)$ is identical with $(V|x)T \subset (V|x)U$.

This follows immediately from CS9 (Chapter I, § 4, no. 1) and CS5 (Chapter I, § 1, no. 2).

CF13. If $T$ and $U$ are terms, $T \subset U$ is a relation.

This follows immediately from CF8 (Chapter I, § 1, no. 4).

¶ Every relation of the form $T \subset U$ (where $T$ and $U$ are terms) is called an inclusion relation.

From now on we shall no longer write down explicitly the criteria of substitution and the formative criteria which should follow the definitions. It should be noted, however, that these criteria will often be used implicitly in proofs.

To prove the relation $x \subset y$ in a theory $\mathscr{T}$, it is enough, by C27 (Chapter I, § 4, no. 1), to prove that $z \in y$ in the theory obtained by adjoining $z \in x$ to the axioms of $\mathscr{T}$, where $z$ is a letter distinct from $x$, $y$ and the constants of the theory. In pratice we say "let $z$ be an element of $x$", and we attempt to prove $z \in y$.