diff --git a/src/cat/cat/cat-func.tex b/src/cat/cat/cat-func.tex
index 25d5980..67b3b1e 100644
--- a/src/cat/cat/cat-func.tex
+++ b/src/cat/cat/cat-func.tex
@@ -3,7 +3,7 @@
 
 \begin{definition}[Category]
 \label{definition:category}
-    A \textbf{category} $\catc$ is a collection of objects $\obj{\catc}$, such that for any $A, B, C \in \obj{\catc}$, there exists sets $\mor{A, B}$, $\mor{B, C}$, and a composition law
+    A \textbf{category} $\catc$ is a collection of objects $\obj{\catc}$, such that for any $A, B, C \in \obj{\catc}$, there exist sets $\mor{A, B}$, $\mor{B, C}$, and a composition law
     \[
     \mor{A, B} \times \mor{B, C} \to \mor{A, C}
     \]
diff --git a/src/fa/lc/compact.tex b/src/fa/lc/compact.tex
index 68a5ba6..66cdb63 100644
--- a/src/fa/lc/compact.tex
+++ b/src/fa/lc/compact.tex
@@ -33,7 +33,6 @@
 \end{definition}
 
 
-
 \begin{lemma}
 \label{lemma:extremal-face}
     Let $E$ be a locally convex space over $\real$, $K \subset E$ be non-empty and compact, and $\phi \in E^*$. Let $\alpha = \sup\bracs{\dpn{x, \phi}{E}|x \in K}$, then $A = \bracs{\phi = \alpha} \cap K$ is a non-empty extreme subset of $K$. 
diff --git a/src/fa/tvs/vector-function.tex b/src/fa/tvs/vector-function.tex
index a15b126..b989776 100644
--- a/src/fa/tvs/vector-function.tex
+++ b/src/fa/tvs/vector-function.tex
@@ -27,7 +27,7 @@
 
     (T) $\Rightarrow$ (B): Let $f \in \cf$, $S \in \sigma$ and $U \subset F \times F$ be a symmetric entourage, then $E(S, U)(0)$ is a neighbourhood of $0$ with respect to the $\sigma$-uniform topology. By (TVS2), there exists $\lambda > 0$ such that $f \in \lambda E(S, U)(0)$. In which case, for any $x \in S$, $\lambda^{-1}f(x) \in U(0)$ and $f(x) \in \lambda U(0)$. Thus $f(S) \subset \lambda U(0)$, and $f(S)$ is bounded.
 
-    (T) $\Rightarrow$ (B): Let $f, g \in \cf$, $\lambda, \lambda' \in K$, and $S \in \sigma$, then for any $x \in X$,
+    (B) $\Rightarrow$ (T): Let $f, g \in \cf$, $\lambda, \lambda' \in K$, and $S \in \sigma$, then for any $x \in X$,
     \begin{align*}
     \lambda f(x) - \lambda' g(x) &= \lambda f(x) - \lambda' f(x) + \lambda' f(x) - \lambda' g(x) \\
     &= (\lambda - \lambda')f(x) + \lambda' (f(x) - g(x))
diff --git a/src/topology/main/baire.tex b/src/topology/main/baire.tex
index c7037ff..05019d4 100644
--- a/src/topology/main/baire.tex
+++ b/src/topology/main/baire.tex
@@ -16,7 +16,7 @@
 \begin{proof}
     $(1) \Rightarrow (2)$: Let $\seq{A_n} \subset 2^X$ be closed with empty interior, then $\seq{A_n}$ are nowhere dense. Hence $\bigcup_{n \in \nat^+}A_n \subsetneq X$.
 
-    $(2) \Rightarrow (3)$: For each $n \in \natp$, let $A_n = U_n^c$, then $A_n$ is closed. For any $\emptyset U \subset A_n$ open, $U \cap U_n \ne \emptyset$ by density of $U_n$, so $A_n$ has empty interior.
+    $(2) \Rightarrow (3)$: For each $n \in \natp$, let $A_n = U_n^c$, then $A_n$ is closed. For any $\emptyset \ne U \subset A_n$ open, $U \cap U_n \ne \emptyset$ by density of $U_n$, so $A_n$ has empty interior.
 
     Suppose that $\bigcap_{n \in \natp}U_n$ is not dense, then there exists $\emptyset \ne V \subset X$ open such that $\bigcup_{n \in \natp}A_n \supset V$, which contradicts the fact that $\bigcup_{n \in \natp}A_n$ has non-empty interior.
 
diff --git a/src/topology/main/cube.tex b/src/topology/main/cube.tex
index ff15a3d..174991f 100644
--- a/src/topology/main/cube.tex
+++ b/src/topology/main/cube.tex
@@ -69,7 +69,7 @@
     \mathcal{S} = \bracsn{(E, F) \in \mathcal{B}^2 | \ol{E} \subset F}
     \]
 
-    By \hyperref[Urysohn's Lemma]{lemma:urysohn}, for each $(E, F) \in \mathcal{S}$, there exists $f_{EF} \in C(X; [0, 1])$ such that $f|_E = 1$ and $f|_{F^c} = 0$. For any $x \in X$ and $U \in \cn^o_X(x)$, there exists $E, F \in \mathcal{B}$ such that $x \in E \subset \ol{E} \subset F \subset U$. Thus $f_{EF}(x) = 1$ and $f_{EF}|_{U^c} = 0$. Therefore
+    By \hyperref[Urysohn's Lemma]{lemma:urysohn}, for each $(E, F) \in \mathcal{S}$, there exists $f_{EF} \in C(X; [0, 1])$ such that $f_{EF}|_E = 1$ and $f_{EF}|_{F^c} = 0$. For any $x \in X$ and $U \in \cn^o_X(x)$, there exists $E, F \in \mathcal{B}$ such that $x \in E \subset \ol{E} \subset F \subset U$. Thus $f_{EF}(x) = 1$ and $f_{EF}|_{U^c} = 0$. Therefore
     \[
     \cf = \bracsn{f_{EF}|(E, F) \in \mathcal{S}} \subset C(X; [0, 1])
     \]