diff --git a/changes-set.txt b/changes-set.txt
index 1b1a7bfa7..977191d5a 100644
--- a/changes-set.txt
+++ b/changes-set.txt
@@ -92,6 +92,7 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+ 5-Jan-25 rabss3d   [same]      moved from TA's mathbox to main set.mm
  4-Jan-25 ralimda   ---         obsolete - use ralimdaa instead
  3-Jan-25 srgi      srgdilem
  2-Jan-25 pr2nelem  enpr2
diff --git a/set.mm b/set.mm
index efe99fcfc..9cb521000 100644
--- a/set.mm
+++ b/set.mm
@@ -38330,6 +38330,16 @@ technically classes despite morally (and provably) being sets, like ` 1 `
       ( crab cv wcel wa cab df-rab ssab2 eqsstri ) ABCDBECFAGBHCABCIABCJK $.
   $}
 
+  ${
+    $d x A $.  $d x B $.  $d x ph $.
+    rabss3d.1 $e |- ( ( ph /\ ( x e. A /\ ps ) ) -> x e. B ) $.
+    $( Subclass law for restricted abstraction.  (Contributed by Thierry
+       Arnoux, 25-Sep-2017.) $)
+    rabss3d $p |- ( ph -> { x e. A | ps } C_ { x e. B | ps } ) $=
+      ( crab nfv nfrab1 cv wcel wa simprr jca ex rabid 3imtr4g ssrd ) ACBCDGZBC
+      EGZACHBCDIBCEIACJZDKZBLZUAEKZBLZUASKUATKAUCUEAUCLUDBFAUBBMNOBCDPBCEPQR $.
+  $}
+
   ${
     $d A x $.
     ssrab3.1 $e |- B = { x e. A | ph } $.
@@ -472279,16 +472289,6 @@ Class abstractions (a.k.a. class builders)
     ( csn wss wcel c0 wceq wo sssn snnzg neneqd pm2.21d sneqrg jaod imp sylan2b
     ) ADZBDZEACFZRGHZRSHZIZABHZRBJTUCUDTUAUDUBTUAUDTRGACKLMABCNOPQ $.
 
-  ${
-    $d x A $.  $d x B $.  $d x ph $.
-    rabss3d.1 $e |- ( ( ph /\ ( x e. A /\ ps ) ) -> x e. B ) $.
-    $( Subclass law for restricted abstraction.  (Contributed by Thierry
-       Arnoux, 25-Sep-2017.) $)
-    rabss3d $p |- ( ph -> { x e. A | ps } C_ { x e. B | ps } ) $=
-      ( crab nfv nfrab1 cv wcel wa simprr jca ex rabid 3imtr4g ssrd ) ACBCDGZBC
-      EGZACHBCDIBCEIACJZDKZBLZUAEKZBLZUASKUATKAUCUEAUCLUDBFAUBBMNOBCDPBCEPQR $.
-  $}
-
   $( Intersection with an intersection.  (Contributed by Thierry Arnoux,
      27-Dec-2016.) $)
   inin $p |- ( A i^i ( A i^i B ) ) = ( A i^i B ) $=
@@ -755171,6 +755171,239 @@ that every function in the sequence can have a different (partial)
 $( End $[ set-mbox-ss.mm $] $)
 
 
+$( Begin $[ set-mbox-et.mm $] $)
+$( Skip $[ set-main.mm $] $)
+$(
+#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
+  Mathbox for Ender Ting
+#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
+$)
+
+
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Increasing sequences and subsequences
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+  ${
+    $( Less-than class is never reflexive.  (Contributed by Ender Ting,
+       22-Nov-2024.)  Prefer to specify theorem domain and then apply ~ ltnri .
+       (New usage is discouraged.) $)
+    et-ltneverrefl $p |- -. A < A $=
+      ( cxr wcel clt wbr wn xrltnr cop opelxp1 con3i ltrelxr sseli nsyl sylnibr
+      cxp df-br pm2.61i ) ABZCZAADZEZFAGSFZAAHZTCZUAUBUCRROZCZUDUFSAARRIJTUEUCK
+      LMAATPNQ $.
+  $}
+
+  ${
+    $( Alternative proof that equality is left-Euclidean, using ~ ax7 directly
+       instead of utility theorems; done for practice.  (Contributed by Ender
+       Ting, 21-Dec-2024.) $)
+    et-equeucl $p |- ( x = z -> ( y = z -> x = y ) ) $=
+      ( weq wi equid ax7 com12 ax-mp syl ) ACDZCADZBCDZABDZEAADZKLEAFKOLACAGHIM
+      LNMCBDZLNEBBDZMPEBFMQPBCBGHILPNCABGHJHJ $.
+  $}
+
+  ${
+    $( The square root of a negative number is not a real number.  (Contributed
+       by Ender Ting, 5-Jan-2025.) $)
+    et-sqrtnegnre $p |- ( ( A e. RR /\ A < 0 ) -> -. ( sqrt ` A ) e. RR ) $=
+      ( cr wcel cc0 clt wbr wa cle wi csqrt cfv simpr 0red ltnled biimpd impcom
+      wn id jcnd ancoms c2 cexp co wceq recn sqsqrtd sqge0 breq2 syl2imc nsyl )
+      ABZCZADZEFZGULUMAHZFZIZAJKZUKCZUNULUQQUNULGULUPUNULLULUNUPQZULUNUTULAUMUL
+      RULMNOPSTULURUAUBUCZAUDZUSUMVAUOFZUPULAAUEUFURUGVBVCUPVAAUMUOUHOUIUJ $.
+  $}
+
+  ${
+    $d B t $.  $d T t $.  $d k t $.
+    natlocalincr.1 $e |- A. k e. ( 0 ..^ T ) A. t e. ( 1 ..^ ( T + 1 ) ) ( k <
+                         t -> ( B ` k ) < ( B ` t ) ) $.
+    $( Global monotonicity on half-open range implies local monotonicity.
+       (Contributed by Ender Ting, 22-Nov-2024.) $)
+    natlocalincr $p |- A. k e. ( 0 ..^ T ) ( B ` k ) < ( B ` ( k + 1 ) ) $=
+      ( cv cfv c1 caddc co clt wbr cc0 cfzo wcel wex wi wral ralimi cz wceq rsp
+      ovex isseti fzoaddel mpan2 0p1e1 oveq1i eleqtrdi eleq1 syl5ibrcom ralimia
+      1z imim1d mp2b cr elfzoelz zre ltp1 3syl breq2 ax-2 syl5com breq2d biimpd
+      fveq2 a2i rspec eximdv mpi ax5e syl rgen ) DFZBGZVNHIJZBGZKLZDMCNJZVNVSOZ
+      VRAPZVRVTAFZVPUAZAPWAAVPVNHIUCUDVTWCVRAWCVRQZDVSWCVNWBKLZVOWBBGZKLZQZQZDV
+      SRZWCWGQZDVSRWDDVSRWHAHCHIJZNJZRZDVSRWBWMOZWHQZDVSRWJEWNWPDVSWHAWMUBSWPWI
+      DVSVTWCWOWHVTWOWCVPWMOVTVPMHIJZWLNJZWMVTHTOVPWROUMVNMCHUEUFWQHWLNUGUHUIWB
+      VPWMUJUKUNULUOWIWKDVSVTWCWEQWIWKVTWEWCVNVPKLZVTVNTOVNUPOWSVNMCUQVNURVNUSU
+      TWBVPVNKVAUKWCWEWGVBVCULWKWDDVSWCWGVRWCWGVRWCWFVQVOKWBVPBVFVDVEVGSUOVHVIV
+      JVRAVKVLVM $.
+  $}
+
+  ${
+    $d B a b k $.  $d T a k t $.  $d T a b k $.
+    natglobalincr.1 $e |- A. k e. ( 0 ..^ T ) ( B ` k ) < ( B ` ( k + 1 ) ) $.
+    natglobalincr.2 $e |- T e. ZZ $.
+    $( Local monotonicity on half-open integer range implies global
+       monotonicity.  (Contributed by Ender Ting, 23-Nov-2024.) $)
+    natglobalincr $p |- A. k e. ( 0 ..^ T ) A. t e. ( ( k + 1 ) ... T ) ( B ` k
+                        ) < ( B ` t ) $=
+      ( cv cfv clt wbr cc0 co wcel cz cle w3a wceq fveq2 cxr syl va vb c1 caddc
+      cfz wb elfzoelz peano2zd elfz1 sylancl breq2d rspec cop cxp df-br ltrelxr
+      cfzo sseli sylbi opelxp1 3ad2ant3 opelxp2 0red cr simp1 zre 3syl peano2re
+      simp21 zred elfzole1 ltp1d wa wi id leltletr mp2and 3ad2ant1 simp22 letrd
+      3jca 0zd a1i elfzo mpd3an23 fvoveq1 breq12d vtoclri syl6bir simp3 xrlttrd
+      simp23 elfzoel2 elfzop1le2 fzindd sylbida rgen2 ) DGZBHZAGZBHZIJZDAKCUQLZ
+      WRUCUDLZCUELZWRXCMZWTXEMZWTNMXDWTOJWTCOJPZXBXFXDNMCNMZXGXHUFXFWRWRKCUGZUH
+      ZFWTXDCUIUJXFWSUAGZBHZIJWSXDBHZIJZWSUBGZBHZIJZWSXPUCUDLZBHZIJXBUAUBWTXDCX
+      LXDQXMXNWSIXLXDBRUKXLXPQXMXQWSIXLXPBRUKXLXSQXMXTWSIXLXSBRUKXLWTQXMXAWSIXL
+      WTBRUKXODXCEULXFXPNMZXDXPOJZXPCIJZPZXRPZWSXQXTXRXFWSSMZYDXRWSXQUMZSSUNZMZ
+      YFXRYGIMYIWSXQIUOIYHYGUPURUSZWSXQSSUTTVAXRXFXQSMZYDXRYIYKYJWSXQSSVBTVAYEX
+      QXTIJZXQXTUMZYHMZXTSMYEKXPOJZYCYLYEKXDXPYEVCYEWRVDMZXDVDMZYEXFWRNMZYPXFYD
+      XRVEXJWRVFZVGWRVHZTYEXPXFYAYBYCXRVIZVJXFYDKXDOJZXRXFKWROJZWRXDIJZUUBWRKCV
+      KXFYRUUDXJYRWRYSVLTXFKVDMZYPYQPZUUCUUDVMUUBVNXFYRYPUUFXJYSYPUUEYPYQYPVCYP
+      VOYTWAVGKWRXDVPTVQVRXFYAYBYCXRVSVTXFYAYBYCXRWLYEYAYOYCVMZYLVNUUAYAUUGXPXC
+      MZYLYAKNMXIUUHUUGUFYAWBXIYAFWCXPKCWDWEXOYLDXPXCWRXPQWSXQXNXTIWRXPBRWRXPUC
+      BUDWFWGEWHWITVQZYLYMIMYNXQXTIUOIYHYMUPURUSXQXTSSVBVGXFYDXRWJUUIWKXKWRKCWM
+      WRKCWNWOWPWQ $.
+  $}
+
+  $c UpWord $.
+
+  $( Extend class notation to include the set of strictly increasing
+     sequences. $)
+  cupword $a class UpWord S $.
+
+  ${
+    $d S k w $.
+
+    ${
+      $( Strictly increasing sequence is a sequence, adjacent elements of which
+         increase.  (Contributed by Ender Ting, 19-Nov-2024.) $)
+      df-upword $a |- UpWord S = { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # `
+      w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) } $.
+    $}
+
+    ${
+      $( Empty set is an increasing sequence for every range.  (Contributed by
+         Ender Ting, 19-Nov-2024.) $)
+      upwordnul $p |- (/) e. UpWord S $=
+        ( vw vk c0 cv wcel cfv c1 co wbr cc0 chash cmin wceq wi cvv wb ax-mp cz
+        cle cword caddc clt cfzo wral wa cab cupword wal 0ex elab6g wrd0 eleq1a
+        fveq2 hash0 eqtrdi oveq1d 0red lem1d eqbrtrd eqeltrdi 1zzd zsubcld fzon
+        0z sylancr mpbid rzal syl jca mpgbir df-upword eleqtrri ) DBEZAUAZFZCEZ
+        VNGVQHUBIVNGUCJZCKVNLGZHMIZUDIZUEZUFZBUGZAUHDWDFZVNDNZWCOZBDPFWEWGBUIQU
+        JWCBDPUKRWFVPWBDVOFWFVPOAULDVOVNUMRWFWADNZWBWFVTKTJZWHWFVTKHMIKTWFVSKHM
+        WFVSDLGKVNDLUNUOUPZUQWFKWFURUSUTWFKSFVTSFWIWHQVEWFVSHWFVSKSWJVEVAWFVBVC
+        KVTVDVFVGVRCWAVHVIVJVKBACVLVM $.
+    $}
+
+    ${
+      $d A w $.
+
+      $( Any increasing sequence is a sequence.  (Contributed by Ender Ting,
+         19-Nov-2024.) $)
+      upwordisword $p |- ( A e. UpWord S -> A e. Word S ) $=
+        ( vw vk cv cword wcel cupword eleq1 cfv c1 caddc clt wbr cc0 chash cmin
+        co cfzo wral wa df-upword abeq2i simplbi vtoclga ) CEZBFZGZAUGGCABHZUFA
+        UGIUFUIGUHDEZUFJUJKZLRUFJMNDOUFPJUKQRSRTZUHULUACUICBDUBUCUDUE $.
+    $}
+
+    ${
+      singoutnword.1 $e |- A e. _V $.
+      $( Singleton with character out of range ` V ` is not a word for that
+         range.  (Contributed by Ender Ting, 21-Nov-2024.) $)
+      singoutnword $p |- ( -. A e. V -> -. <" A "> e. Word V ) $=
+        ( cs1 cword wcel cc0 cfv cvv wceq s1fv ax-mp c0 wne s1nz fstwrdne mpan2
+        eqeltrrid con3i ) ADZBEFZABFUAAGTHZBAIZFUBAJCAUCKLUATMNUBBFAOBTPQRS $.
+    $}
+
+    ${
+      singoutnupword.1 $e |- A e. _V $.
+      $( Singleton with character out of range ` S ` is not an increasing
+         sequence for that range.  (Contributed by Ender Ting, 22-Nov-2024.) $)
+      singoutnupword $p |- ( -. A e. S -> -. <" A "> e. UpWord S ) $=
+        ( wcel wn cs1 cword cupword singoutnword upwordisword nsyl ) ABDEAFZBGD
+        LBHDABCILBJK $.
+    $}
+
+    ${
+      $d A w $.
+      upwordsing.1 $e |- A e. S $.
+      $( Singleton is an increasing sequence for any compatible range.
+         (Contributed by Ender Ting, 21-Nov-2024.) $)
+      upwordsing $p |- <" A "> e. UpWord S $=
+        ( vw vk cs1 cv cword wcel cfv c1 caddc clt wbr cc0 chash cmin cfzo wceq
+        co wral wa cab cupword wi wal wb s1cl elab6g mp2b eleq1a c0 fveq2 s1len
+        oveq1d oveq1i 1m1e0 eqtri eqtrdi oveq2d fzo0 syl jca df-upword eleqtrri
+        rzal mpgbir ) AFDGBHIEGDGJEGKLTDGJMNEODGPJKQTRTUAUBDUCBUDAFDGBHIEGDGJEG
+        KLTDGJMNEODGPJKQTRTUAUBDUCIDGAFSDGBHIEGDGJEGKLTDGJMNEODGPJKQTRTUAUBUEDA
+        BIAFBHIAFDGBHIEGDGJEGKLTDGJMNEODGPJKQTRTUAUBDUCIDGAFSDGBHIEGDGJEGKLTDGJ
+        MNEODGPJKQTRTUAUBUEDUFUGCABUHDGBHIEGDGJEGKLTDGJMNEODGPJKQTRTUAUBDAFBHUI
+        UJDGAFSDGBHIEGDGJEGKLTDGJMNEODGPJKQTRTUAABIAFBHIDGAFSDGBHIUECABUHAFBHDG
+        UKUJDGAFSODGPJKQTRTULSEGDGJEGKLTDGJMNEODGPJKQTRTUADGAFSODGPJKQTRTOORTUL
+        DGAFSDGPJKQTOORDGAFSDGPJKQTAFPJKQTODGAFSDGPJAFPJKQDGAFPUMUOAFPJKQTKKQTO
+        AFPJKKQAUNUPUQURUSUTOVAUSEGDGJEGKLTDGJMNEODGPJKQTRTVFVBVCVGDBEVDVE $.
+    $}
+
+    ${
+      $d S t $.
+      upwordsseti.1 $e |- S e. _V $.
+      $( Strictly increasing sequences with a set given for range form a set.
+         (Contributed by Ender Ting, 21-Nov-2024.) $)
+      upwordsseti $p |- UpWord S e. _V $=
+        ( vt cupword cword wrdexi cv upwordisword ssriv ssexi ) ADZAEZABFCKLCGA
+        HIJ $.
+    $}
+
+    ${
+      $d A b k $.  $d S b k $.
+      tworepnotupword.1 $e |- A e. _V $.
+      $( Word of two matching characters is never an increasing sequence.
+         (Contributed by Ender Ting, 22-Nov-2024.) $)
+      tworepnotupword $p |- -. ( <" A "> ++ <" A "> ) e. UpWord S $=
+        ( vb vk co wcel wn wceq cfv c1 caddc clt wbr cc0 chash cmin cfzo ax-mp
+        cz cs1 cconcat cupword ovex cv wral wrex wa wex isseti wi 0z ccat2s1len
+        c0ex c2 oveq1i 2m1e1 eqtri eqeltri breqtrri fzolb mpbir3an eleq1a fveq2
+        1z 0lt1 oveq1d oveq2d eleq2d syl5ibr et-ltneverrefl fveq1 cvv ccat2s1p1
+        eqtrdi 1e0p1 fveq2i ccat2s1p2 eqtr3i breq12d mtbiri fvoveq1 biimpd jcad
+        con3d syl5com eximdv mpi nfre1 rspe exlimi rexnal sylib cword df-upword
+        syl abeq2i simprbi nsyl eleq1 mtbid vtocle ) AUAZXCUBFZBUCZGZHDXDXCXCUB
+        UDDUEZXDIZXGXEGZXFXHEUEZXGJZXJKLFXGJZMNZEOXGPJZKQFZRFZUFZXIXHXMHZEXPUGZ
+        XQHXHXJXPGZXRUHZEUIZXSXHXJOIZEUIYBEOUNUJXHYCYAEXHYCXTXRYCXTXHXJOXDPJZKQ
+        FZRFZGZOYFGZYCYGUKYHOTGYETGOYEMNULYEKTYEUOKQFKYDUOKQAAUMUPUQURZVEUSOKYE
+        MVFYIUTOYEVAVBOYFXJVCSXHXPYFXJXHXOYEORXHXNYDKQXGXDPVDVGVHVIVJXHOXGJZOKL
+        FZXGJZMNZHYCXRXHYMAAMNAVKXHYJAYLAMXHYJOXDJZAOXGXDVLAVMGZYNAICVMAAVNSVOX
+        HYLYKXDJZAYKXGXDVLKXDJZYPAKYKXDVPVQYOYQAICVMAAVRSVSVOVTWAYCXMYMYCXMYMYC
+        XKYJXLYLMXJOXGVDXJOKXGLWBVTWCWEWFWDWGWHYAXSEXREXPWIXREXPWJWKWPXMEXPWLWM
+        XIXGBWNGZXQYRXQUHDXEDBEWOWQWRWSXGXDXEWTXAXB $.
+    $}
+
+    ${
+      $d S a $.  $d T a $.
+      $( There is a finite number of strictly increasing sequences over finite
+         alphabet.  (Contributed by Ender Ting, 5-Jan-2024.) $)
+      upwrdfi $p |- ( S e. Fin -> { a e. UpWord S | ( # ` a ) = T } e. Fin ) $=
+        ( cfn wcel cv chash cfv wceq cword crab cupword wrdnfi wss upwordisword
+        wtru ad2antrl rabss3d mptru ssfi mpan2 syl ) ADZECFZGHBIZCAJZKZUCEZUECA
+        LZKZUCEZCBAMUHUJUGNZUKULPZUECUIUFUDUIEUDUFEUMUEUDAOQRSUGUJTUAUB $.
+    $}
+  $}
+
+  $(
+    This theorem will show that a given distribution in RR may be satisfied by
+    a relatively short sequence of value transfers.
+    ${
+      paysd.1 $e |- ( ph -> A e. Fin ) $.
+      paysd.2 $e |- ( ph -> B : A --> RR ) $.
+      paysd.3 $e |- ( ph -> sum_ k e. A ( B ` k ) = 0 ) $.
+      paysd.4 $e |- ( ph -> C = (/) ) $.
+      paysd $p |- ( ph -> ( C e. Word ( ( A X. A ) X. RR ) /\ ( # ` C ) <_ ( #
+        ` A ) ) ) $= ( cxp cr cword wcel chash cfv cle wbr c0 wrd0 a1i eqeltrd
+        cc0 wceq fveq2 hash0 eqtrdi syl cfn cn0 hashcl nn0ge0d eqbrtrd jca )
+        ACBBFGFZHZICJZKZBULKZLZMACNZUKEUPUKIAUJOPQAUMRZUNU
+        OACUPSZUMUQSEURUMUPULKUQCUPULTUAUBUCAUNABUDIUNUEID BUFUCUGUHUI $.
+    $}
+  $)
+
+$( (End of Ender Ting's mathbox.) $)
+$( End $[ set-mbox-et.mm $] $)
+
+
 $( Begin $[ set-mbox-ju.mm $] $)
 $( Skip $[ set-main.mm $] $)
 $(
@@ -791262,191 +791495,4 @@ to Davis and Putnam (1960).  (Contributed by David A. Wheeler,
 $( End $[ set-mbox-kz.mm $] $)
 
 
-$( Begin $[ set-mbox-et.mm $] $)
-$( Skip $[ set-main.mm $] $)
-$(
-#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
-  Mathbox for Ender Ting
-#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
-$)
-
-
-$(
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
-  Increasing sequences and subsequences
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
-$)
-
-  ${
-    $( Less-than class is never reflexive.  (Contributed by Ender Ting,
-       22-Nov-2024.)  Prefer to specify theorem domain and then apply ~ ltnri .
-       (New usage is discouraged.) $)
-    et-ltneverrefl $p |- -. A < A $=
-      ( cxr wcel clt wbr wn xrltnr cop opelxp1 con3i ltrelxr sseli nsyl sylnibr
-      cxp df-br pm2.61i ) ABZCZAADZEZFAGSFZAAHZTCZUAUBUCRROZCZUDUFSAARRIJTUEUCK
-      LMAATPNQ $.
-  $}
-
-  ${
-    $d B t $.  $d T t $.  $d k t $.
-    natlocalincr.1 $e |- A. k e. ( 0 ..^ T ) A. t e. ( 1 ..^ ( T + 1 ) ) ( k <
-                         t -> ( B ` k ) < ( B ` t ) ) $.
-    $( Global monotonicity on half-open range implies local monotonicity.
-       (Contributed by Ender Ting, 22-Nov-2024.) $)
-    natlocalincr $p |- A. k e. ( 0 ..^ T ) ( B ` k ) < ( B ` ( k + 1 ) ) $=
-      ( cv cfv c1 caddc co clt wbr cc0 cfzo wcel wex wi wral ralimi cz wceq rsp
-      ovex isseti fzoaddel mpan2 0p1e1 oveq1i eleqtrdi eleq1 syl5ibrcom ralimia
-      1z imim1d mp2b cr elfzoelz zre ltp1 3syl breq2 ax-2 syl5com breq2d biimpd
-      fveq2 a2i rspec eximdv mpi ax5e syl rgen ) DFZBGZVNHIJZBGZKLZDMCNJZVNVSOZ
-      VRAPZVRVTAFZVPUAZAPWAAVPVNHIUCUDVTWCVRAWCVRQZDVSWCVNWBKLZVOWBBGZKLZQZQZDV
-      SRZWCWGQZDVSRWDDVSRWHAHCHIJZNJZRZDVSRWBWMOZWHQZDVSRWJEWNWPDVSWHAWMUBSWPWI
-      DVSVTWCWOWHVTWOWCVPWMOVTVPMHIJZWLNJZWMVTHTOVPWROUMVNMCHUEUFWQHWLNUGUHUIWB
-      VPWMUJUKUNULUOWIWKDVSVTWCWEQWIWKVTWEWCVNVPKLZVTVNTOVNUPOWSVNMCUQVNURVNUSU
-      TWBVPVNKVAUKWCWEWGVBVCULWKWDDVSWCWGVRWCWGVRWCWFVQVOKWBVPBVFVDVEVGSUOVHVIV
-      JVRAVKVLVM $.
-  $}
-
-  ${
-    $d B a b k $.  $d T a k t $.  $d T a b k $.
-    natglobalincr.1 $e |- A. k e. ( 0 ..^ T ) ( B ` k ) < ( B ` ( k + 1 ) ) $.
-    natglobalincr.2 $e |- T e. ZZ $.
-    $( Local monotonicity on half-open integer range implies global
-       monotonicity.  (Contributed by Ender Ting, 23-Nov-2024.) $)
-    natglobalincr $p |- A. k e. ( 0 ..^ T ) A. t e. ( ( k + 1 ) ... T ) ( B ` k
-                        ) < ( B ` t ) $=
-      ( cv cfv clt wbr cc0 co wcel cz cle w3a wceq fveq2 cxr syl va vb c1 caddc
-      cfz wb elfzoelz peano2zd elfz1 sylancl breq2d rspec cop cxp df-br ltrelxr
-      cfzo sseli sylbi opelxp1 3ad2ant3 opelxp2 0red cr simp1 zre 3syl peano2re
-      simp21 zred elfzole1 ltp1d wa wi id leltletr mp2and 3ad2ant1 simp22 letrd
-      3jca 0zd a1i elfzo mpd3an23 fvoveq1 breq12d vtoclri syl6bir simp3 xrlttrd
-      simp23 elfzoel2 elfzop1le2 fzindd sylbida rgen2 ) DGZBHZAGZBHZIJZDAKCUQLZ
-      WRUCUDLZCUELZWRXCMZWTXEMZWTNMXDWTOJWTCOJPZXBXFXDNMCNMZXGXHUFXFWRWRKCUGZUH
-      ZFWTXDCUIUJXFWSUAGZBHZIJWSXDBHZIJZWSUBGZBHZIJZWSXPUCUDLZBHZIJXBUAUBWTXDCX
-      LXDQXMXNWSIXLXDBRUKXLXPQXMXQWSIXLXPBRUKXLXSQXMXTWSIXLXSBRUKXLWTQXMXAWSIXL
-      WTBRUKXODXCEULXFXPNMZXDXPOJZXPCIJZPZXRPZWSXQXTXRXFWSSMZYDXRWSXQUMZSSUNZMZ
-      YFXRYGIMYIWSXQIUOIYHYGUPURUSZWSXQSSUTTVAXRXFXQSMZYDXRYIYKYJWSXQSSVBTVAYEX
-      QXTIJZXQXTUMZYHMZXTSMYEKXPOJZYCYLYEKXDXPYEVCYEWRVDMZXDVDMZYEXFWRNMZYPXFYD
-      XRVEXJWRVFZVGWRVHZTYEXPXFYAYBYCXRVIZVJXFYDKXDOJZXRXFKWROJZWRXDIJZUUBWRKCV
-      KXFYRUUDXJYRWRYSVLTXFKVDMZYPYQPZUUCUUDVMUUBVNXFYRYPUUFXJYSYPUUEYPYQYPVCYP
-      VOYTWAVGKWRXDVPTVQVRXFYAYBYCXRVSVTXFYAYBYCXRWLYEYAYOYCVMZYLVNUUAYAUUGXPXC
-      MZYLYAKNMXIUUHUUGUFYAWBXIYAFWCXPKCWDWEXOYLDXPXCWRXPQWSXQXNXTIWRXPBRWRXPUC
-      BUDWFWGEWHWITVQZYLYMIMYNXQXTIUOIYHYMUPURUSXQXTSSVBVGXFYDXRWJUUIWKXKWRKCWM
-      WRKCWNWOWPWQ $.
-  $}
-
-  $c UpWord $.
-
-  $( Extend class notation to include the set of strictly increasing
-     sequences. $)
-  cupword $a class UpWord S $.
-
-  ${
-    $d S k w $.
-
-    ${
-      $( Strictly increasing sequence is a sequence, adjacent elements of which
-         increase.  (Contributed by Ender Ting, 19-Nov-2024.) $)
-      df-upword $a |- UpWord S = { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # `
-      w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) } $.
-    $}
-
-    ${
-      $( Empty set is an increasing sequence for every range.  (Contributed by
-         Ender Ting, 19-Nov-2024.) $)
-      upwordnul $p |- (/) e. UpWord S $=
-        ( vw vk c0 cv wcel cfv c1 co wbr cc0 chash cmin wceq wi cvv wb ax-mp cz
-        cle cword caddc clt cfzo wral wa cab cupword wal 0ex elab6g wrd0 eleq1a
-        fveq2 hash0 eqtrdi oveq1d 0red lem1d eqbrtrd eqeltrdi 1zzd zsubcld fzon
-        0z sylancr mpbid rzal syl jca mpgbir df-upword eleqtrri ) DBEZAUAZFZCEZ
-        VNGVQHUBIVNGUCJZCKVNLGZHMIZUDIZUEZUFZBUGZAUHDWDFZVNDNZWCOZBDPFWEWGBUIQU
-        JWCBDPUKRWFVPWBDVOFWFVPOAULDVOVNUMRWFWADNZWBWFVTKTJZWHWFVTKHMIKTWFVSKHM
-        WFVSDLGKVNDLUNUOUPZUQWFKWFURUSUTWFKSFVTSFWIWHQVEWFVSHWFVSKSWJVEVAWFVBVC
-        KVTVDVFVGVRCWAVHVIVJVKBACVLVM $.
-    $}
-
-    ${
-      $d A w $.
-
-      $( Any increasing sequence is a sequence.  (Contributed by Ender Ting,
-         19-Nov-2024.) $)
-      upwordisword $p |- ( A e. UpWord S -> A e. Word S ) $=
-        ( vw vk cv cword wcel cupword eleq1 cfv c1 caddc clt wbr cc0 chash cmin
-        co cfzo wral wa df-upword abeq2i simplbi vtoclga ) CEZBFZGZAUGGCABHZUFA
-        UGIUFUIGUHDEZUFJUJKZLRUFJMNDOUFPJUKQRSRTZUHULUACUICBDUBUCUDUE $.
-    $}
-
-    ${
-      singoutnword.1 $e |- A e. _V $.
-      $( Singleton with character out of range ` V ` is not a word for that
-         range.  (Contributed by Ender Ting, 21-Nov-2024.) $)
-      singoutnword $p |- ( -. A e. V -> -. <" A "> e. Word V ) $=
-        ( cs1 cword wcel cc0 cfv cvv wceq s1fv ax-mp c0 wne s1nz fstwrdne mpan2
-        eqeltrrid con3i ) ADZBEFZABFUAAGTHZBAIZFUBAJCAUCKLUATMNUBBFAOBTPQRS $.
-    $}
-
-    ${
-      singoutnupword.1 $e |- A e. _V $.
-      $( Singleton with character out of range ` S ` is not an increasing
-         sequence for that range.  (Contributed by Ender Ting, 22-Nov-2024.) $)
-      singoutnupword $p |- ( -. A e. S -> -. <" A "> e. UpWord S ) $=
-        ( wcel wn cs1 cword cupword singoutnword upwordisword nsyl ) ABDEAFZBGD
-        LBHDABCILBJK $.
-    $}
-
-    ${
-      $d A w $.
-      upwordsing.1 $e |- A e. S $.
-      $( Singleton is an increasing sequence for any compatible range.
-         (Contributed by Ender Ting, 21-Nov-2024.) $)
-      upwordsing $p |- <" A "> e. UpWord S $=
-        ( vw vk cs1 cv cword wcel cfv c1 caddc clt wbr cc0 chash cmin cfzo wceq
-        co wral wa cab cupword wi wal wb s1cl elab6g mp2b eleq1a c0 fveq2 s1len
-        oveq1d oveq1i 1m1e0 eqtri eqtrdi oveq2d fzo0 syl jca df-upword eleqtrri
-        rzal mpgbir ) AFDGBHIEGDGJEGKLTDGJMNEODGPJKQTRTUAUBDUCBUDAFDGBHIEGDGJEG
-        KLTDGJMNEODGPJKQTRTUAUBDUCIDGAFSDGBHIEGDGJEGKLTDGJMNEODGPJKQTRTUAUBUEDA
-        BIAFBHIAFDGBHIEGDGJEGKLTDGJMNEODGPJKQTRTUAUBDUCIDGAFSDGBHIEGDGJEGKLTDGJ
-        MNEODGPJKQTRTUAUBUEDUFUGCABUHDGBHIEGDGJEGKLTDGJMNEODGPJKQTRTUAUBDAFBHUI
-        UJDGAFSDGBHIEGDGJEGKLTDGJMNEODGPJKQTRTUAABIAFBHIDGAFSDGBHIUECABUHAFBHDG
-        UKUJDGAFSODGPJKQTRTULSEGDGJEGKLTDGJMNEODGPJKQTRTUADGAFSODGPJKQTRTOORTUL
-        DGAFSDGPJKQTOORDGAFSDGPJKQTAFPJKQTODGAFSDGPJAFPJKQDGAFPUMUOAFPJKQTKKQTO
-        AFPJKKQAUNUPUQURUSUTOVAUSEGDGJEGKLTDGJMNEODGPJKQTRTVFVBVCVGDBEVDVE $.
-    $}
-
-    ${
-      $d S t $.
-      upwordsseti.1 $e |- S e. _V $.
-      $( Strictly increasing sequences with a set given for range form a set.
-         (Contributed by Ender Ting, 21-Nov-2024.) $)
-      upwordsseti $p |- UpWord S e. _V $=
-        ( vt cupword cword wrdexi cv upwordisword ssriv ssexi ) ADZAEZABFCKLCGA
-        HIJ $.
-    $}
-
-    ${
-      $d A b k $.  $d S b k $.
-      tworepnotupword.1 $e |- A e. _V $.
-      $( Word of two matching characters is never an increasing sequence.
-         (Contributed by Ender Ting, 22-Nov-2024.) $)
-      tworepnotupword $p |- -. ( <" A "> ++ <" A "> ) e. UpWord S $=
-        ( vb vk co wcel wn wceq cfv c1 caddc clt wbr cc0 chash cmin cfzo ax-mp
-        cz cs1 cconcat cupword ovex cv wral wrex wa wex isseti wi 0z ccat2s1len
-        c0ex c2 oveq1i 2m1e1 eqtri eqeltri breqtrri fzolb mpbir3an eleq1a fveq2
-        1z 0lt1 oveq1d oveq2d eleq2d syl5ibr et-ltneverrefl fveq1 cvv ccat2s1p1
-        eqtrdi 1e0p1 fveq2i ccat2s1p2 eqtr3i breq12d mtbiri fvoveq1 biimpd jcad
-        con3d syl5com eximdv mpi nfre1 rspe exlimi rexnal sylib cword df-upword
-        syl abeq2i simprbi nsyl eleq1 mtbid vtocle ) AUAZXCUBFZBUCZGZHDXDXCXCUB
-        UDDUEZXDIZXGXEGZXFXHEUEZXGJZXJKLFXGJZMNZEOXGPJZKQFZRFZUFZXIXHXMHZEXPUGZ
-        XQHXHXJXPGZXRUHZEUIZXSXHXJOIZEUIYBEOUNUJXHYCYAEXHYCXTXRYCXTXHXJOXDPJZKQ
-        FZRFZGZOYFGZYCYGUKYHOTGYETGOYEMNULYEKTYEUOKQFKYDUOKQAAUMUPUQURZVEUSOKYE
-        MVFYIUTOYEVAVBOYFXJVCSXHXPYFXJXHXOYEORXHXNYDKQXGXDPVDVGVHVIVJXHOXGJZOKL
-        FZXGJZMNZHYCXRXHYMAAMNAVKXHYJAYLAMXHYJOXDJZAOXGXDVLAVMGZYNAICVMAAVNSVOX
-        HYLYKXDJZAYKXGXDVLKXDJZYPAKYKXDVPVQYOYQAICVMAAVRSVSVOVTWAYCXMYMYCXMYMYC
-        XKYJXLYLMXJOXGVDXJOKXGLWBVTWCWEWFWDWGWHYAXSEXREXPWIXREXPWJWKWPXMEXPWLWM
-        XIXGBWNGZXQYRXQUHDXEDBEWOWQWRWSXGXDXEWTXAXB $.
-    $}
-  $}
-
-$( (End of Ender Ting's mathbox.) $)
-$( End $[ set-mbox-et.mm $] $)
-
 $( End $[ set-mbox.mm $] $)