diff --git a/set.mm b/set.mm
index c5d6656d2c..01049094be 100644
--- a/set.mm
+++ b/set.mm
@@ -201714,7 +201714,7 @@ be used in an extensible structure (slots must be positive integers).
     neeq12i mpbir ) ABCZADCZEFFFGZEFTHFFFIJJKLMRFSTNOPQ $.
 
   $( The slot for the orthocomplementation is not the slot for the order in an
-     extensible structure.  Formerly part of proof for ~  thlle .  (Contributed
+     extensible structure.  Formerly part of proof for ~ thlle .  (Contributed
      by AV, 11-Nov-2024.) $)
   plendxnocndx $p |- ( le ` ndx ) =/= ( oc ` ndx ) $=
     ( cnx cple cfv coc wne cc0 cdc 10re 1nn0 0nn0 1nn declt ltneii plendx ocndx
@@ -201964,7 +201964,7 @@ be used in an extensible structure (slots must be positive integers).
     $.
 
   $( The index of the slot for the "less than or equal to" ordering is not the
-     index of other slots.   Formerly part of proof for ~ prstcleval .
+     index of other slots.  Formerly part of proof for ~ prstcleval .
      (Contributed by AV, 12-Nov-2024.) $)
   slotsdifplendx2 $p |- ( ( le ` ndx ) =/= ( comp ` ndx )
                        /\ ( le ` ndx ) =/= ( Hom ` ndx ) ) $=
@@ -201974,7 +201974,7 @@ be used in an extensible structure (slots must be positive integers).
     UERSUF $.
 
   $( The index of the slot for the orthocomplementation is not the index of
-     other slots.   Formerly part of proof for ~ prstcocval .  (Contributed by
+     other slots.  Formerly part of proof for ~ prstcocval .  (Contributed by
      AV, 12-Nov-2024.) $)
   slotsdifocndx $p |- ( ( oc ` ndx ) =/= ( comp ` ndx )
                      /\ ( oc ` ndx ) =/= ( Hom ` ndx ) ) $=
@@ -259299,7 +259299,7 @@ U C_ ( N ` { X } ) ) -> ( U = ( N ` { X } ) \/ U = { .0. } ) ) $=
     $( Obsolete proof of ~ srasca as of 12-Nov-2024.  The set of scalars of a
        subring algebra.  (Contributed by Stefan O'Rear, 27-Nov-2014.)  (Revised
        by Mario Carneiro, 12-Nov-2015.)  (Revised by Thierry Arnoux,
-       16-Jun-2019.) (Proof modification is discouraged.)
+       16-Jun-2019.)  (Proof modification is discouraged.)
        (New usage is discouraged.) $)
     srascaOLD $p |- ( ph -> ( W |`s S ) = ( Scalar ` A ) ) $=
       ( cvv cress co csca cfv wceq cnx cop csts scaid wne c5 c6 c0 wa cvsca cip
@@ -265301,7 +265301,7 @@ S C_ ( ._|_ ` ( ._|_ ` S ) ) ) $=
 
       $( Obsolete proof of ~ thlbas as of 11-Nov-2024.  Base set of the Hilbert
          lattice of closed subspaces.  (Contributed by Mario Carneiro,
-         25-Oct-2015.) (Proof modification is discouraged.)
+         25-Oct-2015.)  (Proof modification is discouraged.)
          (New usage is discouraged.) $)
       thlbasOLD $p |- C = ( Base ` K ) $=
         ( cvv wcel cbs cfv wceq cnx ccss eqid wne c1 1nn0 fveq2d fvprc eqtrid
@@ -265331,7 +265331,7 @@ S C_ ( ._|_ ` ( ._|_ ` S ) ) ) $=
 
         $( Obsolete proof of ~ thlle as of 11-Nov-2024.  Ordering on the
            Hilbert lattice of closed subspaces.  (Contributed by Mario
-           Carneiro, 25-Oct-2015.) (Proof modification is discouraged.)
+           Carneiro, 25-Oct-2015.)  (Proof modification is discouraged.)
            (New usage is discouraged.) $)
         thlleOLD $p |- .<_ = ( le ` K ) $=
           ( vx vy cvv wcel cple cfv wceq wne c1 c0 ccss cnx coc cocv csts pleid
@@ -278493,8 +278493,8 @@ represented as an element of (the base set of) ` ( ( 1 ... n ) Mat R ) ` .
       UFUGUHUIUJUPAUSKABURCDEFGURUKULUMUN $.
 
     $( The matrix ring has the same scalar multiplication as its underlying
-       linear structure.  (Contributed by Stefan O'Rear, 4-Sep-2015.)
-       (Proof shortened by AV, 12-Nov-2024.) $)
+       linear structure.  (Contributed by Stefan O'Rear, 4-Sep-2015.)  (Proof
+       shortened by AV, 12-Nov-2024.) $)
     matvsca $p |- ( ( N e. Fin /\ R e. V ) -> ( .s ` G ) = ( .s ` A ) ) $=
       ( cfn wcel wa cvsca cfv cnx cmulr cotp cmmul co cop csts vscaid setsnid
       vscandxnmulrndx eqid matval fveq2d eqtr4id ) DHIBEIJZCKLCMNLZBDDDOPQZRSQZ
@@ -317944,7 +317944,6 @@ the base set to the (extended) reals and which is nonnegative, symmetric
     setsms.d $e |- ( ph -> D = ( ( dist ` M ) |` ( X X. X ) ) ) $.
     setsms.k $e |- ( ph -> K =
       ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) ) $.
-
     $( The base set of a constructed metric space.  (Contributed by Mario
        Carneiro, 28-Aug-2015.)  (Proof shortened by AV, 12-Nov-2024.) $)
     setsmsbas $p |- ( ph -> X = ( Base ` K ) ) $=
@@ -405020,7 +405019,6 @@ and angles (6 parts).  This is often the actual textbook definition of
       ttgval.m $e |- .- = ( -g ` H ) $.
       ttgval.s $e |- .x. = ( .s ` H ) $.
       ttgval.i $e |- I = ( Itv ` G ) $.
-
       $( Define a function to augment a subcomplex Hilbert space with
          betweenness and a line definition.  (Contributed by Thierry Arnoux,
          25-Mar-2019.)  (Proof shortened by AV, 9-Nov-2024.) $)
@@ -785222,7 +785220,7 @@ mean the category of preordered sets (classes).  However, "ProsetToCat"
 
       $( Obsolete proof of ~ prstcleval as of 12-Nov-2024.  Value of the
          less-than-or-equal-to relation is unchanged.  (Contributed by Zhi
-         Wang, 20-Sep-2024.) (Proof modification is discouraged.)
+         Wang, 20-Sep-2024.)  (Proof modification is discouraged.)
          (New usage is discouraged.) $)
       prstclevalOLD $p |- ( ph -> .<_ = ( le ` C ) ) $=
         ( cple cfv cnx wne c1 cc0 cdc c5 10re 1nn0 0nn0 5nn c4 pleid cco nngt0i