diff --git a/test/fast/regression/setEuclid_test.tla b/test/fast/regression/setEuclid_test.tla
index 06289415..5ca05c17 100644
--- a/test/fast/regression/setEuclid_test.tla
+++ b/test/fast/regression/setEuclid_test.tla
@@ -361,7 +361,10 @@ THEOREM Inv /\ Next => Inv'
 (*|*)   BY <3>1, <3>2
     <2>3. CorrectTermination'
       <3>1. Cardinality (S) = 1 => S = {CHOOSE t \in S : TRUE}
-        BY CardThm DEF Inv, TypeOK
+        <4> Cardinality (S) = 1 => \E x \in S : S = {x}
+          BY CardThm DEF Inv, TypeOK
+        <4> QED
+          BY Zenon
       <3>2. Cardinality (S) = 1 => GCD (S) = CHOOSE t \in S : TRUE
         BY <3>1, GCD2 DEF Inv, TypeOK
       <3> QED