diff --git a/set.mm b/set.mm
index 8eea80042a..02434ba8b6 100644
--- a/set.mm
+++ b/set.mm
@@ -22035,7 +22035,7 @@ proposition with a distinct variable (closed form of ~ nfsb4 ).
     $d x y ps $.  $d t y $.
     2sbiev.1 $e |- ( ( x = t /\ y = u ) -> ( ph <-> ps ) ) $.
     $( Conversion of double implicit substitution to explicit substitution.
-       See ~ 2sbievw for variant with extra disjoint variables, but based on
+       See ~ 2sbievw for a variant with extra disjoint variables, but based on
        fewer axioms.  (Contributed by AV, 29-Jul-2023.) $)
     2sbiev $p |- ( [ t / x ] [ u / y ] ph <-> ps ) $=
       ( wsb nfv weq sbiedv sbie ) ADEHBCFBCICFJABDEGKL $.