diff --git a/inputs/lecture_03.tex b/inputs/lecture_03.tex
index f9ae783..4517255 100644
--- a/inputs/lecture_03.tex
+++ b/inputs/lecture_03.tex
@@ -41,7 +41,8 @@ all condensation points are accumulation points.
     Fix $A \subseteq \R$ closed.
     We want to see that $A$ is at most countable
     or there is some perfect $P \subseteq A$.
-    Let $P \coloneqq  \{x \in \R | x \text{ is a condensation point of $A$}\}$.
+    Let
+    \[P \coloneqq  \{x \in \R | x \text{ is a condensation point of $A$}\}.\]
     Since $A $ is closed, $P \subseteq A$.
 
     \begin{claim}
diff --git a/inputs/lecture_04.tex b/inputs/lecture_04.tex
index 05005a2..641184f 100644
--- a/inputs/lecture_04.tex
+++ b/inputs/lecture_04.tex
@@ -9,7 +9,7 @@
 $\ZFC$ stands for
 \begin{itemize}
     \item \textsc{Zermelo}’s axioms (1905), % crises around 19000
-    \item \vocab{Fraenkel}'s axioms,
+    \item \textsc{Fraenkel}'s axioms,
     \item the axiom of choice.
 \end{itemize}
 \begin{notation}
diff --git a/inputs/lecture_08.tex b/inputs/lecture_08.tex
index 6685ed5..b0e5747 100644
--- a/inputs/lecture_08.tex
+++ b/inputs/lecture_08.tex
@@ -18,74 +18,74 @@ has the following axioms:
 \begin{axiom}[Extensionality]
     \yalabel{Axiom of Extensionality}{(Ext)}{ax:bg:ext}
     \[
-    \forall x, y. \left( x = y \iff \left( \forall z.~(z \in x \iff z \in y \right)  \right).
-    \] 
+    \forall x.~\forall  y.~ \left( x = y \iff \left( \forall z.~(z \in x \iff z \in y \right)  \right).
+    \]
 \end{axiom}
 \begin{axiom}[Foundation]
     \yalabel{Axiom of Foundation}{(Fund)}{ax:bg:fund}
     \[
-    \forall x .(x \neq \emptyset \implies \exists  y \in x . y \cap x = \emptyset).
-    \] 
+    \forall x .~(x \neq \emptyset \implies \exists  y \in x .~ y \cap x = \emptyset).
+    \]
 \end{axiom}
 
 \begin{axiom}[Pairing]
     \yalabel{Axiom of Pairing}{(Pair)}{ax:bg:pair}
     \[
-    \forall x \forall  y \exists  z . z = \{x,y\}.
-    \] 
+    \forall x.~\forall y . ~\exists  z .~ z = \{x,y\}.
+    \]
 \end{axiom}
 
 \begin{axiom}[Union]
     \yalabel{Axiom of Union}{(Union)}{ax:bg:union}
     \[
-    \forall  x \exists  y .~ y = \bigcup x.
-    \] 
+    \forall  x .~\exists  y .~ y = \bigcup x.
+    \]
 \end{axiom}
 \begin{axiom}[Power]
     \yalabel{Powerset Axiom}{(Pow)}{ax:bg:pow}
     \[
-    \forall x \exists  y .~ y = \cP(x).
-    \] 
+    \forall x .~\exists  y .~ y = \cP(x).
+    \]
 \end{axiom}
 
 \begin{axiom}[Infinity]
     \yalabel{Axiom of Infinity}{(Infinity)}{ax:bg:inf}
     \[
-    \exists  x . ~(\emptyset \in x \land \left( \forall y \in x .~y \cup \{y\}  \in x \right)).
-    \] 
+    \exists x .~(\emptyset \in x \land \left( \forall y \in x .~y \cup \{y\}  \in x \right)).
+    \]
 \end{axiom}
 
 Together with the following axioms for classes:
 
 \begin{axiom}[Extensionality for classes]
     \[
-        \forall X \forall  Y \left( \forall  x(x \in X \iff y \in X) \implies X = Y).
-    \] 
+        \forall X .~\forall  Y.~ \left( \forall  x.~(x \in X \iff x \in Y) \implies X = Y\right).
+    \]
 \end{axiom}
 
 \begin{axiom}
     Every set is a class:
     \[
-    \forall  x \exists X. x = X.
-    \] 
+    \forall  x.~ \exists X.~ x = X.
+    \]
 \end{axiom}
 \begin{axiom}
     Every element of a class is a set:
     \[
-        \forall X \exists Y.~(X \in Y \to  \exists x.~x = X).
-    \] 
+        \forall X .~\exists Y.~(X \in Y \to  \exists x.~x = X).
+    \]
 \end{axiom}
 \begin{axiom}[Replacement]
     \yalabel{Axiom of Replacement}{(Rep)}{ax:bg:rep}
 
-    If $F$ is a function and inf $a $ is a set,
-    then $F"a$ is a set.
+    If $F$ is a function and $a$ is a set,
+    then $F\,''a$ is a set.
 \end{axiom}
 Here a \vocab[Class function]{(class) function} is a class
 consisting of pairs $(x,y)$,
 such that for every  $x$ there is at most one $y$
 with $(x,y) \in F$.
-Furthermore $F"a \coloneqq  \{y : \exists  x \in  a .~(x,y) \in F\}$.
+Furthermore $F\,''a \coloneqq  \{y : \exists  x \in  a .~(x,y) \in F\}$.
 
 \begin{remark}
     Note that we didn't need to use an axiom schema,
@@ -94,10 +94,9 @@ Furthermore $F"a \coloneqq  \{y : \exists  x \in  a .~(x,y) \in F\}$.
 
 \begin{axiom}[Comprehension]
     \yalabel{Axiom of Comprehension}{(Comp)}{ax:bg:comp}
-
     \[
-    \forall X_1 \ldots \forall X_k .~\exists Y ( \forall  x .~x \in Y \iff \phi(x,X_1,\ldots, X_k))
-    \] 
+    \forall X_1 .~\ldots \forall X_k .~\exists Y.~ ( \forall  x .~x \in Y \iff \phi(x,X_1,\ldots, X_k))
+    \]
     where $\phi(x, X_1, \ldots, X_k)$
     is a formula which contains exactly $X_1, \ldots, X_k, x$
     as free variables,
diff --git a/logic.sty b/logic.sty
index 9b5efa9..be7a7fa 100644
--- a/logic.sty
+++ b/logic.sty
@@ -113,6 +113,8 @@
 \DeclareSimpleMathOperator{HOD}
 \DeclareSimpleMathOperator{OD}
 \DeclareSimpleMathOperator{AC}
+\newcommand{\AxC}{\yarefs{ax:c}}
+\newcommand{\AxSep}{\yarefs{ax:sep}} % Separation
 \newcommand{\Choice}{\yarefs{ax:c}}
 % \DeclareSimpleMathOperator{Choice}
 % \DeclareSimpleMathOperator{Fund}