From a55b8364488abfd40bd1c01856024646f42b3bb2 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Mon, 6 Jan 2025 09:32:44 +0100
Subject: [PATCH] rewrap

---
 set.mm | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/set.mm b/set.mm
index eb5809c9a3..f6b4118204 100644
--- a/set.mm
+++ b/set.mm
@@ -30373,8 +30373,8 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
     cbvrexfw.5 $e |- ( x = y -> ( ph <-> ps ) ) $.
     $( Rule used to change bound variables, using implicit substitution.
        Version of ~ cbvrexf with a disjoint variable condition, which does not
-       require ~ ax-13 .  For a version not dependent on ~ ax-11 and ax-12,
-       see ~ cbvrexvw .  (Contributed by FL, 27-Apr-2008.)  Avoid ~ ax-10 ,
+       require ~ ax-13 .  For a version not dependent on ~ ax-11 and ax-12, see
+       ~ cbvrexvw .  (Contributed by FL, 27-Apr-2008.)  Avoid ~ ax-10 ,
        ~ ax-13 .  (Revised by Gino Giotto, 10-Jan-2024.) $)
     cbvrexfw $p |- ( E. x e. A ph <-> E. y e. A ps ) $=
       ( wrex wn wral nfn weq notbid cbvralfw ralnex 3bitr3i con4bii ) ACEKZBDEK
@@ -30511,8 +30511,8 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
     $d z x A $.  $d y A $.  $d z y ph $.  $d x y $.
     $( Change bound variable by using a substitution.  Version of ~ cbvralsv
        with a disjoint variable condition, which does not require ~ ax-13 .
-       (Contributed by NM, 20-Nov-2005.)  Avoid ~ ax-13 .  (Revised by Gino Giotto,
-       10-Jan-2024.) $)
+       (Contributed by NM, 20-Nov-2005.)  Avoid ~ ax-13 .  (Revised by Gino
+       Giotto, 10-Jan-2024.) $)
     cbvralsvw $p |- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) $=
       ( vz wral wsb nfv nfs1v sbequ12 cbvralw sbequ bitri ) ABDFABEGZEDFABCGZCD
       FANBEDAEHABEIABEJKNOECDNCHOEHAECBLKM $.
@@ -30523,8 +30523,8 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
     $d z x A $.  $d y z ph $.  $d y A $.  $d x y $.
     $( Change bound variable by using a substitution.  Version of ~ cbvrexsv
        with a disjoint variable condition, which does not require ~ ax-13 .
-       (Contributed by NM, 2-Mar-2008.)  Avoid ~ ax-13 .  (Revised by Gino Giotto,
-       10-Jan-2024.) $)
+       (Contributed by NM, 2-Mar-2008.)  Avoid ~ ax-13 .  (Revised by Gino
+       Giotto, 10-Jan-2024.) $)
     cbvrexsvw $p |- ( E. x e. A ph <-> E. y e. A [ y / x ] ph ) $=
       ( vz wrex wsb nfv nfs1v sbequ12 cbvrexw sbequ bitri ) ABDFABEGZEDFABCGZCD
       FANBEDAEHABEIABEJKNOECDNCHOEHAECBLKM $.