diff --git a/Bookshelf/Apostol.tex b/Bookshelf/Apostol.tex
index 901b2f2..4aa6c6a 100644
--- a/Bookshelf/Apostol.tex
+++ b/Bookshelf/Apostol.tex
@@ -32,7 +32,7 @@ The \textbf{characteristic function} of $S$ is the function $\mathcal{X}_S$ such
 
 \begin{definition}
 
-  \lean{Common/Set/Basic}{Set.characteristic}
+  \lean*{Common/Set/Basic}{Set.characteristic}
 
 \end{definition}
 
@@ -49,7 +49,7 @@ Such a number $B$ is also known as the \textbf{greatest lower bound}.
 
 \begin{definition}
 
-  \lean{Mathlib/Order/Bounds/Basic}{IsGLB}
+  \lean*{Mathlib/Order/Bounds/Basic}{IsGLB}
 
 \end{definition}
 
@@ -148,7 +148,7 @@ A collection of points satisfying \eqref{sec:partition-eq1} is called a
 
 \begin{definition}
 
-  \lean{Common/Set/Partition}{Set.Partition}
+  \lean*{Common/Set/Partition}{Set.Partition}
 
 \end{definition}
 
@@ -180,7 +180,7 @@ That is to say, for each $k = 1, 2, \ldots, n$, there is a real number $s_k$
 
 \begin{definition}
 
-  \lean{Common/Geometry/StepFunction}{Geometry.StepFunction}
+  \lean*{Common/Geometry/StepFunction}{Geometry.StepFunction}
 
 \end{definition}
 
@@ -197,7 +197,7 @@ Such a number $B$ is also known as the \textbf{least upper bound}.
 
 \begin{definition}
 
-  \lean{Mathlib/Order/Bounds/Basic}{IsLUB}
+  \lean*{Mathlib/Order/Bounds/Basic}{IsLUB}
 
 \end{definition}
 
@@ -224,7 +224,7 @@ Every nonempty set $S$ of real numbers which is bounded above has a supremum;
 
 \begin{axiom}
 
-  \lean{Mathlib/Data/Real/Basic}{Real.exists\_isLUB}
+  \lean*{Mathlib/Data/Real/Basic}{Real.exists\_isLUB}
 
 \end{axiom}
 
@@ -676,7 +676,7 @@ For each set $S$ in $\mathscr{M}$, we have $a(S) \geq 0$.
 
 \begin{axiom}
 
-  \leanp{Common/Geometry/Area}{Nonnegative-Property}
+  \leanp*{Common/Geometry/Area}{Nonnegative-Property}
     {Nonnegative Property}
 
 \end{axiom}
@@ -689,7 +689,7 @@ If $S$ and $T$ are in $\mathscr{M}$, then $S \cup T$ and $S \cap T$ are in
 
 \begin{axiom}
 
-  \leanp{Common/Geometry/Area}{Additive-Property}
+  \leanp*{Common/Geometry/Area}{Additive-Property}
     {Additive Property}
 
 \end{axiom}
@@ -702,7 +702,7 @@ If $S$ and $T$ are in $\mathscr{M}$ with $S \subseteq T$, then $T - S$ is in
 
 \begin{axiom}
 
-  \leanp{Common/Geometry/Area}{Difference-Property}
+  \leanp*{Common/Geometry/Area}{Difference-Property}
     {Difference Property}
 
 \end{axiom}
@@ -715,7 +715,7 @@ If a set $S$ is in $\mathscr{M}$ and if $T$ is congruent to $S$, then $T$ is
 
 \begin{axiom}
 
-  \leanp{Common/Geometry/Area}{Invariance-Under-Congruence}
+  \leanp*{Common/Geometry/Area}{Invariance-Under-Congruence}
     {Invariance Under Congruence}
 
 \end{axiom}
@@ -728,7 +728,7 @@ If the edges of $R$ have lengths $h$ and $k$, then $a(R) = hk$.
 
 \begin{axiom}
 
-  \leanp{Common/Geometry/Area}{Choice-of-Scale}
+  \leanp*{Common/Geometry/Area}{Choice-of-Scale}
     {Choice of Scale}
 
 \end{axiom}
@@ -748,7 +748,7 @@ If there is one and only one number $c$ which satisfies the inequalities
 
 \begin{axiom}
 
-  \leanp{Common/Geometry/Area}{Exhaustion-Property}
+  \leanp*{Common/Geometry/Area}{Exhaustion-Property}
     {Exhaustion Property}
 
 \end{axiom}
diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex
index 7c5074c..e376759 100644
--- a/Bookshelf/Enderton/Set.tex
+++ b/Bookshelf/Enderton/Set.tex
@@ -17,12 +17,18 @@
 \chapter{Reference}%
 \label{chap:reference}
 
-\section{\partial{Empty Set Axiom}}%
+\section{\defined{Empty Set Axiom}}%
 \label{ref:empty-set-axiom}
 
 There is a set having no members:
   $$\exists B, \forall x, x \not\in B.$$
 
+\begin{axiom}
+
+  \lean*{Mathlib/Init/Set}{Set.emptyCollection}
+
+\end{axiom}
+
 \section{\defined{Extensionality Axiom}}%
 \label{ref:extensionality-axiom}
 
@@ -32,23 +38,43 @@ If two sets have exactly the same members, then they are equal:
 
 \begin{axiom}
 
-  \lean{Mathlib/Init/Set}{Set.ext}
+  \lean*{Mathlib/Init/Set}{Set.ext}
 
 \end{axiom}
 
-\section{\partial{Pair Set}}%
+\section{\defined{Pair Set}}%
 \label{ref:pair-set}
 
 For any sets $u$ and $v$, the \textbf{pair set $\{u, v\}$} is the set whose
   only members are $u$ and $v$.
 
-\section{\partial{Pairing Axiom}}%
+\begin{definition}
+
+  \ % Add space
+
+  \lean*{Mathlib/Init/Set}{Set.insert}
+
+  \lean*{Mathlib/Init/Set}{Set.singleton}
+
+\end{definition}
+
+\section{\defined{Pairing Axiom}}%
 \label{ref:pairing-axiom}
 
 For any sets $u$ and $v$, there is a set having as members just $u$ and $v$:
   $$\forall u, \forall v, \exists B, \forall x,
       (x \in B \iff x = u \text{ or } x = v).$$
 
+\begin{axiom}
+
+  \ % Add space
+
+  \lean*{Mathlib/Init/Set}{Set.insert}
+
+  \lean*{Mathlib/Init/Set}{Set.singleton}
+
+\end{axiom}
+
 \section{\defined{Power Set}}%
 \label{ref:power-set}
 
@@ -57,31 +83,49 @@ For any set $a$, the \textbf{power set $\powerset{a}$} is the set whose members
 
 \begin{definition}
 
-  \lean{Mathlib/Init/Set}{Set.powerset}
+  \lean*{Mathlib/Init/Set}{Set.powerset}
 
 \end{definition}
 
-\section{\partial{Power Set Axiom}}%
+\section{\defined{Power Set Axiom}}%
 \label{ref:power-set-axiom}
 
 For any set $a$, there is a set whose members are exactly the subsets of $a$:
   $$\forall a, \exists B, \forall x, (x \in B \iff x \subseteq a).$$
 
-\section{\partial{Subset Axioms}}%
+\begin{axiom}
+
+  \lean*{Mathlib/Init/Set}{Set.powerset}
+
+\end{axiom}
+
+\section{\defined{Subset Axioms}}%
 \label{ref:subset-axioms}
 
 For each formula $\phi$ not containing $B$, the following is an axiom:
   $$\forall t_1, \cdots \forall t_k, \forall c,
       \exists B, \forall x, (x \in B \iff x \in c \land \phi).$$
 
-\section{\partial{Union Axiom}}%
+\begin{axiom}
+
+  \lean*{Mathlib/Init/Set}{Set.Subset}
+
+\end{axiom}
+
+\section{\defined{Union Axiom}}%
 \label{ref:union-axiom}
 
 For any set $A$, there exists a set $B$ whose elements are exactly the members
   of the members of $A$:
   $$\forall A, \exists B, \forall x \left[ x \in B \iff (\exists b \in A) x \in b \right]$$
 
-\section{\partial{Union Axiom, Preliminary Form}}%
+\begin{axiom}
+
+  \lean*{Mathlib/Data/Set/Lattice}{Set.sUnion}
+
+\end{axiom}
+
+\section{\defined{Union Axiom, Preliminary Form}}%
 \label{ref:union-axiom-preliminary-form}
 
 For any sets $a$ and $b$, there is a set whose members are those sets belonging
@@ -89,6 +133,12 @@ For any sets $a$ and $b$, there is a set whose members are those sets belonging
   $$\forall a, \forall b, \exists B, \forall x,
       (x \in B \iff x \in a \text{ or } x \in b).$$
 
+\begin{axiom}
+
+  \lean*{Mathlib/Init/Set}{Set.union}
+
+\end{axiom}
+
 \endgroup
 
 \chapter{Introduction}%