diff --git a/src/graph-theory/complete-bipartite-graphs.lagda.md b/src/graph-theory/complete-bipartite-graphs.lagda.md
index c51345aeda..1b255ce9ff 100644
--- a/src/graph-theory/complete-bipartite-graphs.lagda.md
+++ b/src/graph-theory/complete-bipartite-graphs.lagda.md
@@ -34,7 +34,7 @@ consisting of:
 - The finite set of vertices is the
   [coproduct type](univalent-combinatorics.coproduct-types.md) `X + Y`.
 - Given an [unordered pair](foundation.unordered-pairs.md) `f : I → X + Y` of
-  vertices, an the finite type of edges on the unordered pair `(I , f)` is given
+  vertices, the finite type of edges on the unordered pair `(I , f)` is given
   by
 
   ```text