diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md
index 193a7fe36..ec91c8904 100644
--- a/src/plfa/part2/Lambda.lagda.md
+++ b/src/plfa/part2/Lambda.lagda.md
@@ -791,7 +791,7 @@ It can be illustrated as follows:
                P
 
 Here `L`, `M`, `N` are universally quantified while `P`
-is existentially quantified.  If each line stands for zero
+is existentially quantified.  If each of the four lines in the figure above stands for zero
 or more reduction steps, this is called confluence,
 while if the top two lines stand for a single reduction
 step and the bottom two stand for zero or more reduction