\chapter{Zermelo's Well-Ordering Theorem}
\section{Zermelo1908}\label{kffgchngfgmgpgbdjdadid}\begin{definition}\label{def:kffgchngfgmgpghfpe}
$\mname{ZermeloWO}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 36a362f5d7e56550e98a38468fb4fc4d70ea17f4707cfdd2f69fc2cce37a9643 \\
Pure Object Address: & TMYCW3jauecphYdjePotuDSXP7ZXkfAzLaT \\
Theory Object Id: & e62050256ab27fb78004baab27aff9e7e88265df5714b6aeafcd573b2e7015f0 \\
Theory Object Address: & TMZVEYfCFAjoTjAywDY2bSVjv6eXC6FdX5Z
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
ZermeloWO_Eps
\end{verbatim}
\begin{theorem}\label{thm:kffgchngfgmgpghfpepffeahdh} ${\unicdcdadad a : {\iota} .  {{({{\mname{Eps\_i}}~{({{\mname{ZermeloWO}}~{a}})}})}={a}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 967f2b509c968b55983160582bb89f4b3b392cdb74bd3014ddadec13cba49a90 \\
Pure Prop Address: & TMaCPTLDmtonLabJKS8VNg2KpQHWXLBoNXU \\
Theory Prop Id: & 56530eac409ade83907328e28fb11e3478cc0f4637d0fbe97f076524758f297c \\
Theory Prop Address: & TMTxzfNoxPLisqEQk9tTQ8t7JzkFz1bXCit
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ZermeloWO_ref
\end{verbatim}
\begin{theorem}\label{thm:kffgchngfgmgpghfpepfchfggg} ${{\mname{reflexive}}~{\mname{ZermeloWO}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0debc67241d3f1b73ddcdb9242748e16c0a306dd4c5bd3be38285ce4c810b221 \\
Pure Prop Address: & TMZLFAPmHBxLwpqpQcE1qZeY2pPcfX3QVi5 \\
Theory Prop Id: & 3087155d06daaf3f9264297022e0ed58f4b93c8b8bfbbeb282039734efef904e \\
Theory Prop Address: & TMUkjTCw2R4W9Puur76M31DHpHBxtkcez6n
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ZermeloWO_lin
\end{verbatim}
\begin{theorem}\label{thm:kffgchngfgmgpghfpepfmgjgog} ${{\mname{linear}}~{\mname{ZermeloWO}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 79880f17e3e9a931262c694b18e962541b3131893ba53d44229166cd1edc06ee \\
Pure Prop Address: & TMJkDnfbxikrHuEoUB2KH59QL83E8yZkNdP \\
Theory Prop Id: & feb13fbc27d9aae829703d3a69e71d745f6bbb8008d16029b663316db4a0f0ca \\
Theory Prop Address: & TMMBkNPnE1Xevjyn43F624QPHNDG2eYWp52
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ZermeloWO_tra
\end{verbatim}
\begin{theorem}\label{thm:kffgchngfgmgpghfpepfehchbg} ${{\mname{transitive}}~{\mname{ZermeloWO}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9206e3397ca8b9ed09881d5cb76cc80df1ee726499d1f8f1b5c1780d5e9f59ba \\
Pure Prop Address: & TMSnBoLW5VjgRKasiFgj55RonswXagBwUxF \\
Theory Prop Id: & 0cbc46f560bfdfcf23991ad12021c892678d58d3e631d71ff5bab43ce776b5a2 \\
Theory Prop Address: & TMSyNvgsZEkSPxH6fbpbuyr29yGLQk1uE2K
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ZermeloWO_antisym
\end{verbatim}
\begin{theorem}\label{thm:kffgchngfgmgpghfpepfbgogehjgdhjhng} ${{\mname{antisymmetric}}~{\mname{ZermeloWO}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & db152b33b6ab9a13d674d4d926a9099a24633405bb2ac4113622a3bc701b6e86 \\
Pure Prop Address: & TMVoZux2uwtDAmhKY3JNavcVyuWpiLWkQ53 \\
Theory Prop Id: & 6e0efdc62d566eec4426eae46854f865abce0b3abf2038f5022a0c3129893eee \\
Theory Prop Address: & TMdx1hkuD9K2Mfu17Z1gRygw4fnFG42CyZi
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ZermeloWO_partialorder
\end{verbatim}
\begin{theorem}\label{thm:kffgchngfgmgpghfpepfahbgchehjgbgmgpgchegfgch} ${{\mname{partialorder}}~{\mname{ZermeloWO}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0656f9a90963b7a76e123603eb83d8b92e386a909153edb2d3e6bfed1e801d65 \\
Pure Prop Address: & TMYe2evtB7V2D59AgeiBdZxBgksb6og2GHV \\
Theory Prop Id: & 3499fde0183fea1cebe20732bc7ad2cb75fe284d9e4d45f292274921f510f343 \\
Theory Prop Address: & TMPx6RFHGz7VtFGVUwqZbmtdXG9SYpYHcfG
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ZermeloWO_totalorder
\end{verbatim}
\begin{theorem}\label{thm:kffgchngfgmgpghfpepfehpgehbgmgpgchegfgch} ${{\mname{totalorder}}~{\mname{ZermeloWO}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 88ef7c493983ed7becf7f9e7c5dd717b8b1ad11361f29a5250e8aea67ebb6d56 \\
Pure Prop Address: & TMQi6BX2vtRo2UJyxGGrvkYy62BsS4n19XS \\
Theory Prop Id: & d20df0c3bde7031c1b562bdbbd689604af6728a5b9c1130cdd7fd5a07e1cef0d \\
Theory Prop Address: & TMcqRgmAfxGTPiCTYL27ftCtLTjGab61vAE
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ZermeloWO_wo
\end{verbatim}
\begin{theorem}\label{thm:kffgchngfgmgpghfpepfhhpg} ${\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{({\unicdcdaddd x : {\iota} .  {{p}~{x}}})}\unicdbdjdcd{\unicdcdaddd x : {\iota} .  {{{p}~{x}}\unicdcdcdhd{\unicdcdadad y : {\iota} .  {{{p}~{y}}\unicdbdjdcd{{{\mname{ZermeloWO}}~{x}}~{y}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7e38ffca0702338d27fa602350391a1c15520286ef30a841a14806771c076a95 \\
Pure Prop Address: & TMSRd1JSF4kWdSSvoi4w2eq61nrH7PDF95s \\
Theory Prop Id: & 321d3a35eac90f0ec080d2b70a9efa74fb4cb4002111c116f5cd2d55be9418e2 \\
Theory Prop Address: & TMLKb3jsZ1LNt1giMEWqCcJ48ttSzxEektg
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:kffgchngfgmgpghfpedhehchjgdgeh}
We define $\mname{ZermeloWOstrict}$ to be ${\uniddcgcg a b : {\iota} .  {{{{\mname{ZermeloWO}}~{a}}~{b}}\unicdcdcdhd{{a}\unicdcdgdad{b}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & e5853602d8dd42d777476c1c7de48c7bfc9c98bfa80a1e39744021305a32f462 \\
Pure Object Address: & TMNLYaDifZ1BU7nW96xprhzT7ZrQZLkjzMb \\
Theory Object Id: & cef2db95ff08afb8db1745dfd6898d6e39064f4098ca0acb0061eafac129c1b4 \\
Theory Object Address: & TMTjf9r8y9UHsnCWkcHJQd5ZgraPrRuvcnA
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
ZermeloWOstrict_trich
\end{verbatim}
\begin{theorem}\label{thm:kffgchngfgmgpghfpedhehchjgdgehpfehchjgdgig} ${{\mname{trichotomous\_or}}~{\mname{ZermeloWOstrict}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 157b48f20feb46068f0f2aca7b452a507ead7d12b83628b031a51c5f14ce0e37 \\
Pure Prop Address: & TMGSAsnBLMuRws587dr7obynuEWa3KPPuiL \\
Theory Prop Id: & ee31d14ab8f6580d4d2449c878828d85530f8e2efa920c10cbcd5cc992f53766 \\
Theory Prop Address: & TMJCGmPXs5syPbHaK8NokgLMNiDtwNKeZYH
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ZermeloWOstrict_stricttotalorder
\end{verbatim}
\begin{theorem}\label{thm:kffgchngfgmgpghfpedhehchjgdgehpfdhehchjgdgehehpgehbgmgpgchegfgch} ${{\mname{stricttotalorder}}~{\mname{ZermeloWOstrict}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 56f948bc4585b5f5c01ab14c1def7e85a8b8a620235ac296d35a8d94e34c7b1e \\
Pure Prop Address: & TMYR5UnFMSJLwv3HU9FtTvsT9LpzdoKVbZ3 \\
Theory Prop Id: & c2537c16e167c192e2f11d7811816cd1fa923138f2630e88388223d36fa49e70 \\
Theory Prop Address: & TMLePQqfgDYUVPqeJYmRyjMFNhntRXwDCMy
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ZermeloWOstrict_wo
\end{verbatim}
\begin{theorem}\label{thm:kffgchngfgmgpghfpedhehchjgdgehpfhhpg}
  $$
  \begin{array}{c}
    \unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {({\unicdcdaddd x : {\iota} .  {{p}~{x}}})}\unicdbdjdcd\\
    \unicdcdaddd x : {\iota} .  {{{p}~{x}}\unicdcdcdhd{\unicdcdadad y : {\iota} .  {{{{p}~{y}}\unicdcdcdhd{{y}\unicdcdgdad{x}}}\unicdbdjdcd{{{\mname{ZermeloWOstrict}}~{x}}~{y}}}}}.
  \end{array}
$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d7160045949b81cdd599a4103fed7b65d41988baaee1332de79e879bbbfb0dcf \\
Pure Prop Address: & TMVwVvUZQVTnP3hnKczqoHkD8Zxt76L7hq4 \\
Theory Prop Id: & 458f09e17af7e183e42d050a345d94c93e451920cc3aa0f15d74c38ff9645ca4 \\
Theory Prop Address: & TMEvCCPnMvJRotk1TMESMYoU6fL8ARNf8cG
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Zermelo_WO
\end{verbatim}
\begin{theorem}\label{thm:kffgchngfgmgpgpfhfpe}
  $$
  \begin{array}{c}
    \unicdcdaddd r : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{\mname{totalorder}}~{r}}\unicdcdcdhd\\
                 {({\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{({\unicdcdaddd x : {\iota} .  {{p}~{x}}})}\unicdbdjdcd{\unicdcdaddd x : {\iota} .  {{{p}~{x}}\unicdcdcdhd{\unicdcdadad y : {\iota} .  {{{p}~{y}}\unicdbdjdcd{{{r}~{x}}~{y}}}}}}}})}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d37c8533f52315f30dedfc2fe79f9a6c647286dec8db8cfc0917eb94b01c80f2 \\
Pure Prop Address: & TMTrdxnBmgaKrgsRSyEtgvNwTWRhUzG7QEW \\
Theory Prop Id: & 3b56530ad7e26682eefc8e7eaf7c2e18d87597abef3ce1d4dd28adb08a1bab16 \\
Theory Prop Address: & TMXrj7GDDD1CizwhmhqkHEbXjtQ236xfNTd
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Zermelo_WO_strict
\end{verbatim}
\begin{theorem}\label{thm:kffgchngfgmgpgpfhfpepfdhehchjgdgeh}
  $$
  \begin{array}{c}
    \unicdcdaddd r : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{\mname{stricttotalorder}}~{r}}\unicdcdcdhd\\
                 {({\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{({\unicdcdaddd x : {\iota} .  {{p}~{x}}})}\unicdbdjdcd{\unicdcdaddd x : {\iota} .  {{{p}~{x}}\unicdcdcdhd{\unicdcdadad y : {\iota} .  {{{{p}~{y}}\unicdcdcdhd{{y}\unicdcdgdad{x}}}\unicdbdjdcd{{{r}~{x}}~{y}}}}}}}})}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 77cb5b1b3db7a63607bc9d07653bc63fb19f0a5a2226c66935ac1668becd94cf \\
Pure Prop Address: & TMGPaaZebUwDYiYk1ANGBmfqMyyCg7WMmg5 \\
Theory Prop Id: & 57f61ff6fb48481c18b75895db9d64e93f2f58e90b52ec3ec4e59d1efa68cd83 \\
Theory Prop Address: & TMSPtM5ooeGZYBnjiKvH9mKzYtMVNv3LDSW
\end{tabular}
\end{center}

\end{theorem}
