diff --git a/discouraged b/discouraged
index 15c191c62a..5aa53aae2f 100644
--- a/discouraged
+++ b/discouraged
@@ -15412,6 +15412,7 @@ New usage of "flddivrng" is discouraged (2 uses).
 New usage of "fldhmsubcALTV" is discouraged (0 uses).
 New usage of "fnexALT" is discouraged (0 uses).
 New usage of "fnmpt2ovdOLD" is discouraged (0 uses).
+New usage of "footexALT" is discouraged (0 uses).
 New usage of "fresisonOLD" is discouraged (0 uses).
 New usage of "frgrwopreglem5ALT" is discouraged (0 uses).
 New usage of "funadj" is discouraged (4 uses).
@@ -18897,6 +18898,7 @@ Proof modification of "fimaxreOLD" is discouraged (172 steps).
 Proof modification of "fiminreOLD" is discouraged (312 steps).
 Proof modification of "fnexALT" is discouraged (111 steps).
 Proof modification of "fnmpt2ovdOLD" is discouraged (219 steps).
+Proof modification of "footexALT" is discouraged (2161 steps).
 Proof modification of "frege10" is discouraged (27 steps).
 Proof modification of "frege100" is discouraged (31 steps).
 Proof modification of "frege101" is discouraged (49 steps).
diff --git a/set.mm b/set.mm
index 788f4def3c..5764c6fcea 100644
--- a/set.mm
+++ b/set.mm
@@ -386667,9 +386667,10 @@ are congruent (CPCTC), focusing on a specific segment.  (Contributed
       $d a b d p ph q x y z $.
       foot.x $e |- ( ph -> C e. P ) $.
       foot.y $e |- ( ph -> -. C e. A ) $.
-      $( Lemma for ~ foot : existence part.  (Contributed by Thierry Arnoux,
-         19-Oct-2019.) $)
-      footex $p |- ( ph -> E. x e. A ( C L x ) ( perpG ` G ) A ) $=
+      $( Alternative version of ~ footex which minimization requires a notably
+         long time.  (Contributed by Thierry Arnoux, 19-Oct-2019.)
+         (New usage is discouraged.)  (Proof modification is discouraged.) $)
+      footexALT $p |- ( ph -> E. x e. A ( C L x ) ( perpG ` G ) A ) $=
         ( co wcel adantr va vb vy vp vz vq vd wceq wne cperpg cfv wbr wrex cmir
         cv eqid cstrkg ad3antrrr ad2antrr ad6antr simplr simprr eqcomd midexlem
         simp-4r simp-6r simprl ad4antr simp-5r simprd simp-7r ad10antr simp-11r
@@ -386751,6 +386752,132 @@ are congruent (CPCTC), focusing on a specific segment.  (Contributed
         VIUVHVAYOYPUVCUDUUODYTEUVEFGHUVFIJKLMUXDUXGVUOUUNUVAUUTVAUXOVUAUVBUUPUU
         SVBVDYPUUNUCYTDEFGIUUAYTJKLUXFVUEUYTUYTUXNYOYPAUAUBCEFGHJLMNOYQYR $.
 
+      ${
+        footexlem.e $e |- ( ph -> E e. P ) $.
+        footexlem.f $e |- ( ph -> F e. P ) $.
+        footexlem.r $e |- ( ph -> R e. P ) $.
+        footexlem.x $e |- ( ph -> X e. P ) $.
+        footexlem.y $e |- ( ph -> Y e. P ) $.
+        footexlem.z $e |- ( ph -> Z e. P ) $.
+        footexlem.d $e |- ( ph -> D e. P ) $.
+        footexlem.1 $e |- ( ph -> A = ( E L F ) ) $.
+        footexlem.2 $e |- ( ph -> E =/= F ) $.
+        footexlem.3 $e |- ( ph -> E e. ( F I Y ) ) $.
+        footexlem.4 $e |- ( ph -> ( E .- Y ) = ( E .- C ) ) $.
+        footexlem.5 $e |- ( ph -> C = ( ( ( pInvG ` G ) ` R ) ` Y ) ) $.
+        footexlem.6 $e |- ( ph -> Y e. ( E I Z ) ) $.
+        footexlem.7 $e |- ( ph -> ( Y .- Z ) = ( Y .- R ) ) $.
+        footexlem.q $e |- ( ph -> Q e. P ) $.
+        footexlem.8 $e |- ( ph -> Y e. ( R I Q ) ) $.
+        footexlem.9 $e |- ( ph -> ( Y .- Q ) = ( Y .- E ) ) $.
+        footexlem.10 $e |- ( ph -> Y e. ( ( ( ( pInvG ` G ) ` Z ) ` Q ) I D ) )
+          $.
+        footexlem.11 $e |- ( ph -> ( Y .- D ) = ( Y .- C ) ) $.
+        footexlem.12 $e |- ( ph -> D = ( ( ( pInvG ` G ) ` X ) ` C ) ) $.
+        $( Lemma for ~ footex (Contributed by Thierry Arnoux, 19-Oct-2019.)
+           (Revised by Thierry Arnoux, 1-Jul-2023.) $)
+        footexlem1 $p |- ( ph -> X e. A ) $=
+          ( co eqcomd cmir cfv wne wcel wn necomd btwnlng3 lncom nelne2 syl2anc
+          eleqtrrd eqnetrrd eqid mirinv necon3bid mpbid tgcgrneq mirbtwn oveq1d
+          mircl tgbtwnouttr2 tgbtwncom cs3 crag ccgrg oveq2d eqtrd israg mpbird
+          wceq tgcgrcomlr eqtr2d tglinerflx1 axtgcgrrflx axtg5seg trgcgr ragcgr
+          ragcom eqidd krippen tglinethru ) ANOPLVEBAEJKLOPNQSTUAUIUJUHAOGOPEJK
+          MQRSUAUIUGUIUJAOPMVEOGMVEURVFZAGOAOGJVGVHZVHZVHZOVIGOVIACXKOUPAOCAOBV
+          JCBVJVKZOCVIAOHILVEZBAEJKLHIOQSTUAUEUFUIUMAEJKLIHOQSTUAUFUEUIAHIUMVLU
+          NVMVNULVQZUDOCBVOVPVLVRAXKOGOAGOEXIJKLXJMQRSTXIVSZUAUGXJVSZUIVTWAWBZV
+          LWCZAEJKLPONQSTUAUJUIUHAOPXRVLAFFPXIVHZVHZOEXICDJKLXSMNXIVHZPNQRSTXOU
+          AXSVSZYAVSUSAPEXIJKLXSMFQRSTXOUAUJYBUSWFUIUCUKUJUHACOFEJKMQRSUAUCUIUS
+          ACGOFEJKMQRSUAUCUGUIUSXQAGXKOKVECOKVEAGOEXIJKLXJMQRSTXOUAUGXPUIWDACXK
+          OKUPWEVQUTWGWHVBAOPFWIJWJVHZVJOFMVEZOXTMVEWPAFPOEXIJKLMQRSTXOUAUSUJUI
+          AHGOFEJWKVHZXIPOJKLMQRSTXOUAUEUGUIYEVSZUSUJUIAHGOWIYCVJHOMVEZHXKMVEZW
+          PAYGHCMVEZYHUOACXKHMUPWLWMAHGOEXIJKLMQRSTXOUAUEUGUIWNWOAHGOFEYEPOJMQR
+          YFUAUEUGUIUSUJUIAGHPFEJKMQRSUAUGUEUJUSAHOPEHJKMFFOGQRSUAUSUIUGUEUIUJU
+          EUSAOFACHOFEJKMQRSUAUCUEUIUSAYDOHMVEZCHMVEVAAHOHCEJKMQRSUAUEUIUEUCUOW
+          QWRAHCAHBVJXLHCVIAHXMBAEHIJKLQSTUAUEUFUMWSULVQZUDHCBVOVPZVLWCVLAGOFEJ
+          KMQRSUAUGUIUSUTWHUQAOFOHEJKMQRSUAUIUSUIUEVAWQXHAEJKMFHQRSUAUSUEWTAYDY
+          JVAVFZXAWQAOGOPEJKMQRSUAUIUGUIUJXHWQYMXBXCXDAOPFEXIJKLMQRSTXOUAUIUJUS
+          WNWBAODMVEOCMVEVCVFAXTXEVDXFVMVNABEOPJKLQSTUAUIUJXRXRUBXNAPHOLVEBAEJK
+          LHOPQSTUAUEUIUJAHCHOEJKMQRSUAUEUCUEUIAYGYIUOVFYLWCZUQVMABEHOJKLQSTUAU
+          EUIYNYNUBYKXNXGVQXGVQ $.
+
+        $( Lemma for ~ footex (Contributed by Thierry Arnoux, 19-Oct-2019.)
+           (Revised by Thierry Arnoux, 1-Jul-2023.) $)
+        footexlem2 $p |- ( ph -> ( C L X ) ( perpG ` G ) A ) $=
+          ( co wcel wn wne footexlem1 nelne2 syl2anc tgelrnln tglinerflx2 elind
+          necomd tglinerflx1 btwnlng3 lncom eleqtrrd wceq wa cmir cstrkg adantr
+          eqid crag eqidd simpr s3eqd mircl tgcgrcomlr eqtr2d tgcgrneq eqnetrrd
+          cfv cs3 mirinv necon3bid mirbtwn oveq1d tgbtwnouttr2 tgbtwncom oveq2d
+          mpbid ccgrg eqtrd mpbird eqcomd axtg5seg trgcgr ragcgr ragcom neeqtrd
+          israg axtgcgrrflx mircgr eleqtrd orcd ragcol eqeltrd btwncolg3 neneqd
+          wo ragflat pm2.65da neqned ragperp ) ACNLVEZBECJKLMONQRSTUAAEJKLCNQST
+          UAUCUHANCANBVFCBVFVGZNCVHABCDEFGHIJKLMNOPQRSTUAUBUCUDUEUFUGUHUIUJUKUL
+          UMUNUOUPUQURUSUTVAVBVCVDVIZUDNCBVJVKVOZVLUBAYHBNAECNJKLQSTUAUCUHYKVMY
+          JVNAECNJKLQSTUAUCUHYKVPAOHILVEZBAEJKLHIOQSTUAUEUFUIUMAEJKLIHOQSTUAUFU
+          EUIAHIUMVOUNVQVRULVSZYKAONAONVTZOGVTZAYNWAZHOGEJWBWOZJKLMQRSTYQWEZAJW
+          CVFYNUAWDZAHEVFYNUEWDZAOEVFYNUIWDZAGEVFYNUGWDZYPGOHEYQJKLMQRSTYRYSUUB
+          UUAYTYPCOHGEYQJKLMQRSTYRYSACEVFYNUCWDZUUAYTUUBYPCOHWPCNHWPJWFWOZYPCOH
+          HCNYPCWGAYNWHZYPHWGWIYPHNCEYQJKLMQRSTYRYSYTANEVFYNUHWDZUUCYPPNCHEYQJK
+          LMQRSTYRYSAPEVFYNUJWDZUUFUUCYTAPNCWPUUDVFZYNAUUHPCMVEZPCNYQWOWOZMVEZV
+          TAUUIPDMVEUUKACPDPEJKMQRSUAUCUJUKUJAFPYQWOZWOZODEPJKMPFOCQRSUAUSUIUCA
+          PEYQJKLUULMFQRSTYRUAUJUULWEZUSWJZUIUKUJUJAOFACHOFEJKMQRSUAUCUEUIUSAOF
+          MVEZOHMVEZCHMVEVAAHOHCEJKMQRSUAUEUIUEUCUOWKWLAHCAHBVFYIHCVHZAHYLBAEHI
+          JKLQSTUAUEUFUMVPULVSUDHCBVJVKZVOWMVOZACOFEJKMQRSUAUCUIUSACGOFEJKMQRSU
+          AUCUGUIUSAOGYQWOZWOZOVHGOVHACUVBOUPAOCAOBVFYIOCVHYMUDOCBVJVKVOZWNAUVB
+          OGOAGOEYQJKLUVAMQRSTYRUAUGUVAWEZUIWQWRXDZAGUVBOKVECOKVEAGOEYQJKLUVAMQ
+          RSTYRUAUGUVDUIWSACUVBOKUPWTVSZUTXAXBVBAOFOUUMEJKMQRSUAUIUSUIUUOAOPFWP
+          UUDVFUUPOUUMMVEVTAFPOEYQJKLMQRSTYRUAUSUJUIAHGOFEJXEWOZYQPOJKLMQRSTYRU
+          AUEUGUIUVGWEZUSUJUIAHGOWPUUDVFZHOMVEZHUVBMVEZVTAUVJHCMVEZUVKUOACUVBHM
+          UPXCXFAHGOEYQJKLMQRSTYRUAUEUGUIXNXGZAHGOFEUVGPOJMQRUVHUAUEUGUIUSUJUIA
+          GHPFEJKMQRSUAUGUEUJUSAHOPEHJKMFFOGQRSUAUSUIUGUEUIUJUEUSUUTAGOFEJKMQRS
+          UAUGUIUSUTXBUQAOFOHEJKMQRSUAUIUSUIUEVAWKAOPMVEZOGMVEURXHZAEJKMFHQRSUA
+          USUEXOAUUPUUQVAXHZXIWKAOGOPEJKMQRSUAUIUGUIUJUVOWKUVPXJXKXLAOPFEYQJKLM
+          QRSTYRUAUIUJUSXNXDWKAODMVEZOCMVEZVCXHZAPFPUUMEJKMQRSUAUJUSUJUUOAPUUMM
+          VEPFMVEAPFEYQJKLUULMQRSTYRUAUJUUNUSXPXHWKAUVNWGXIWKADUUJPMVDXCXFAPNCE
+          YQJKLMQRSTYRUAUJUHUCXNXGWDYPPONAPOVHYNAOPAOGOPEJKMQRSUAUIUGUIUJUVOAGO
+          UVEVOZWMVOWDUUEXMYPPNHLVEZVFNHVTYPPOHLVEUWAYPEJKLOHPQSTYSUUAYTUUGYPHO
+          YPHCHOEJKMQRSYSYTUUCYTUUAAUVLUVJVTYNAUVJUVLUOXHZWDAUURYNUUSWDWMVOAPHO
+          LVEVFYNAEJKLHOPQSTUAUEUIUJAHCHOEJKMQRSUAUEUCUEUIUWBUUSWMUQVQWDVRYPONH
+          LUUEWTXQXRXSXLXTACOVHYNUVCWDACOGLVEVFYOYCYNAEJKLOGCQTSUAUIUGUCACGOEJK
+          MQRSUAUCUGUIUVFXBYAWDXSXLAUVIYNUVMWDYDYPOGAOGVHYNUVTWDYBYEYFAONCEYQJK
+          LMQRSTYRUAUIUHUCAONCWPUUDVFUVROUUJMVEZVTAUVRUVQUWCUVSADUUJOMVDXCXFAON
+          CEYQJKLMQRSTYRUAUIUHUCXNXGXLYG $.
+      $}
+
+      $( From a point ` C ` outside of a line ` A ` , there exists a point
+         ` x ` on ` A ` such that ` ( C L x ) ` is perpendicular to ` A ` .
+         This point is unique, see ~ foot .  (Contributed by Thierry Arnoux,
+         19-Oct-2019.)  (Revised by Thierry Arnoux, 1-Jul-2023.) $)
+      footex $p |- ( ph -> E. x e. A ( C L x ) ( perpG ` G ) A ) $=
+        ( co wa wcel va vb vy vp vz vq vd cv wceq wne cperpg cfv wrex cmir eqid
+        wbr cstrkg ad5antr ad2antrr ad6antr simplr simp-4r midexlem crn ad9antr
+        simprr eqcomd adantr ad3antrrr ad10antr simp-7r simprl simpllr simp-11r
+        wn simpld simp-9r simp-5r simplrl footexlem1 footexlem2 reximssdv mircl
+        simprd axtgsegcon r19.29a tgisline r19.29vva ) ACUAUHZUBUHZHRUIZWIWJUJZ
+        SZDBUHZHRCFUKULUPZBCUMZUAUBEEAWIETZSZWJETZSZWMSZWIWJUCUHZGRTZWIXBIRWIDI
+        RUIZSZWPUCEXAXBETZSZXESZDXBUDUHZFUNULZULZULUIZWPUDEXHXIETZSZXLSZXBWIUEU
+        HZGRTZXBXPIRXBXIIRUIZSZWPUEEXOXPETZSZXSSZXBXIUFUHZGRTZXBYCIRXBWIIRUIZSZ
+        WPUFEYBYCETZSZYFSZXBYCXPXJULZULZUGUHZGRTZXBYLIRZXBDIRZUIZSZWPUGEYIYLETZ
+        SZYQSZYLDWNXJULZULUIZWOBCEYTBDYLXBEXJFGHUUAIJKLMXJUOZYIFUQTZYRYQYBUUDYG
+        YFXOUUDXTXSXHUUDXMXLAUUDWQWSWMXFXENURZUSZUSZUSZUSUUAUOYIDETZYRYQXHUUIXM
+        XLXTXSYGYFAUUIWQWSWMXFXEPURZUTZUSZYIYRYQVAYIXFYRYQYBXFYGYFXOXFXTXSXAXFX
+        EXMXLVBZUSZUSZUSYTYNYOYSYMYPVFZVGVCYTWNETZUUBSZSZCDYLEYCXIWIWJFGHIWNXBX
+        PJKLMYBUUDYGYFYRYQUURUUGURZXHCHVDTZXMXLXTXSYGYFYRYQUURAUVAWQWSWMXFXEOUR
+        VEZYTUUIUURUULVHZYTDCTVOZUURXAUVDXFXEXMXLXTXSYGYFYRYQAUVDWQWSWMQVIVJVHZ
+        YBWQYGYFYRYQUURXOWQXTXSAWQWSWMXFXEXMXLVKZUSZURZYTWSUURXAWSXFXEXMXLXTXSY
+        GYFYRYQWRWSWMVAZVJVHZYBXMYGYFYRYQUURXHXMXLXTXSVBZURZYTUUQUUBVLZYBXFYGYF
+        YRYQUURUUNURZXOXTXSYGYFYRYQUURVKZYIYRYQUURVMZYTWKUURYTWKWLWTWMXFXEXMXLX
+        TXSYGYFYRYQVNZVPVHZYTWLUURYTWKWLUVQWDVHZYTXCUURYTXCXDXGXEXMXLXTXSYGYFYR
+        YQVQZVPVHZYTXDUURYTXCXDUVTWDVHZYTXLUURXNXLXTXSYGYFYRYQVKVHZYTXQUURYTXQX
+        RYAXSYGYFYRYQVRZVPVHZYTXRUURYTXQXRUWDWDVHZYBYGYFYRYQUURVRZYTYDUURYTYDYE
+        YHYFYRYQVMZVPVHZYTYEUURYTYDYEUWHWDVHZYSYMYPUURVSZYTYPUURUUPVHZYTUUQUUBV
+        FZVTUUSCDYLEYCXIWIWJFGHIWNXBXPJKLMUUTUVBUVCUVEUVHUVJUVLUVMUVNUVOUVPUVRU
+        VSUWAUWBUWCUWEUWFUWGUWIUWJUWKUWLUWMWAWBYIUGXBDEFGIYKXBJKLUUHYIXPEXJFGHY
+        JIYCJKLMUUCUUHXOXTXSYGYFVBYJUOYBYGYFVAWCUUOUUOUUKWEWFYBUFXBWIEFGIXIXBJK
+        LUUGUVKUUNUUNUVGWEWFXOUEXBXIEFGIWIXBJKLUUFUVFUUMUUMXHXMXLVAWEWFXHUDXBDW
+        IEXJFGHXKIJKLMUUCUUEXKUOXAXFXEVAUUJAWQWSWMXFXEVRXGXCXDVFVCWFXAUCWIDEFGI
+        WJWIJKLAUUDWQWSWMNVIUVIAWQWSWMVMZUWNAUUIWQWSWMPVIWEWFAUAUBCEFGHJLMNOWGW
+        H $.
+
       $( From a point ` C ` outside of a line ` A ` , there exists a unique
          point ` x ` on ` A ` such that ` ( C L x ) ` is perpendicular to
          ` A ` .  That point is called the foot from ` C ` on ` A ` .  Theorem