add in newlines

metamath · Feb 4, 2025 · 8335085 · 8335085
1 parent 9d69e69
commit 8335085
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/set.mm b/set.mm
@@ -60195,6 +60195,7 @@ singleton of the first member (with no sethood assumptions on ` B ` ).
       BDEFHIJRACDGFKST $.
   $}
 
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Well-ordered induction
@@ -80164,6 +80165,7 @@ Power Set ( ~ ax-pow ).  (Contributed by Mario Carneiro, 20-May-2013.)
       AEUANPPABQACDETRS $.
   $}
 
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Induction on cross products
@@ -80952,6 +80954,7 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
     $}
   $}
 
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Ordering Ordinal Sequences