diff --git a/Reference Manual/theory.tex b/Reference Manual/theory.tex index 632a5774a0e00df8322dcd703f9013fff7b6ff91..5817ba5b543ac0917edc889e5744d434fdb4818c 100644 --- a/Reference Manual/theory.tex +++ b/Reference Manual/theory.tex @@ -43,8 +43,8 @@ This is however not a convenient definition. In practice, all infinite axiomatiz \begin{axz}[extensionality]\label{axz:extensionality} $\forall x, y. (\forall z. z \in x \iff z \in y) \iff (x = y)$ \end{axz} - \begin{axz}[extensionality]\label{axz:subset} - $\forall x, y. x\subset y \iff \forall z. z \in x iff z \in y$ + \begin{axz}[subset]\label{axz:subset} + $\forall x, y. x\subset y \iff \forall z. z \in x \iff z \in y$ \end{axz} \begin{axz}[pair]\label{axz:pair} $\forall x, y, z. (z \in (x, y)) \iff ((x \in y) \lor (y \in z))$