\chapter{Ordinals}

\begin{definition}\label{def:pgchegjgogbgmg}
We define $\mname{ordinal}$ to be ${\uniddcgcg \alpha : {\iota} .  {{{\mname{TransSet}}~{\alpha}}\unicdcdcdhd{\unicdcdadad \beta \in {\alpha} .  {{\mname{TransSet}}~{\beta}}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & ee28d96500ca4c012f9306ed26fad3b20524e7a89f9ac3210c88be4e6a7aed23 \\
Pure Object Address: & TMMUuqYqPdrVu6cDtXgARhaXmQ84ZrMXG6P \\
Theory Object Id: & 53ee8f616e489e1965c33226035b0df42058ce50fbf01e6172cdf3b427f5a693 \\
Theory Object Address: & TMJ4CnbKugQJ97k3pfeF56M78Ug4AubAWjZ
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:pgchegjgogbgmgpfefchbgogdhdffgeh} ${\unicdcdadad \alpha : {\iota} .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{{\mname{TransSet}}~{\alpha}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0dbaa3d497ea2fe357d7cdf6de2639b3f4cf815ee1d613eaddc6fb305b46de56 \\
Pure Prop Address: & TMdzYsAgm9hgqSggzyEMmMw5w6aRH1fmS1D \\
Theory Prop Id: & c9e708b22b5dc60c895eed22a527c202e52f14066b2f95ce8df1cb630eb1df7e \\
Theory Prop Address: & TMXHSD7yBJJjNhye2R2DtR5uPTVLTRGPMVo
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfjeogpfefchbgogdhdffgeh} ${\unicdcdadad \alpha : {\iota} .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{\unicdcdadad \beta \in {\alpha} .  {{\mname{TransSet}}~{\beta}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f4e77fe3f77ebff8ff08239d5f4175451624803d11b0018e85f316c34806264c \\
Pure Prop Address: & TMYKCKb2mgJ361o53ZDmr4bqCotaiAa9UMT \\
Theory Prop Id: & cc1f55fe1800e237a0d36d0f295ac28bf748b236473d1e1f9caf5515be62a995 \\
Theory Prop Address: & TMXH96JbZ5RRa3chjsLwakm9MEVpiN5ygZV
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpffengahehjh} ${{\mname{ordinal}}~{\mname{Empty}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ce6bea11043bbd03d9af274f7b824c53be0840dd9f324cd7c9afc0d4f811b316 \\
Pure Prop Address: & TMHjHTkWmLerJqJCyfCzQ2x3bAbjxupX5rN \\
Theory Prop Id: & 7d95d14b163c311c6050bb25900b2f0e05a1fb83c01aacb93a1b6cf03a658823 \\
Theory Prop Address: & TMcRLhPoJiCW9i4Gg3Z8GVhyHi3DGQmpBpx
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfiefgchfgeg} ${\unicdcdadad \alpha : {\iota} .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{\unicdcdadad \beta \in {\alpha} .  {{\mname{ordinal}}~{\beta}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a7e78b55af56fd38debe61d4cf2ccd6512ff509a33690ff7bcb062d67233a307 \\
Pure Prop Address: & TMYATDhQjyWwu2denmfYctz9jzc5T6pvxDY \\
Theory Prop Id: & 43b0f3ddbec2adab900eae39d5c70d5f8e32937abf8669f79ab503a2cba3c688 \\
Theory Prop Address: & TMNMsaVbc4QJAjitEJmAT3A6577bnGUMenX
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:efchbgogdhdffgehpfpgchegdhfhdgdg} ${\unicdcdadad X : {\iota} .  {{{\mname{TransSet}}~{X}}\unicdbdjdcd{{\mname{TransSet}}~{({{\mname{ordsucc}}~{X}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fc215771da05b7091bde93e8fd1dbf94168ddb5e1c68f7934a03aeb58f1ebd07 \\
Pure Prop Address: & TMds6RBqX4EBdbVb2jzpQF4BGu62TbmQW6S \\
Theory Prop Id: & ebf9e34c8261f406aaf9188564b534bc4eee97dba2e5fafb75b1f972cbc9d365 \\
Theory Prop Address: & TMTZpuHkdymxGmLoep6QY3LRhQf6Nr8Myhy
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfpgchegdhfhdgdg} ${\unicdcdadad \alpha : {\iota} .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{{\mname{ordinal}}~{({{\mname{ordsucc}}~{\alpha}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0ba97fa745a108db180034344887cefa8fa42aa10e94eb93ee5f6ba8a383902a \\
Pure Prop Address: & TMNpPkbjLapq9BtN9phPiFFNbRzuB8jfTRk \\
Theory Prop Id: & ab0f7f2be575c7979819df5a27b6d7276069f61fd5ec603b15b317dca63b3e76 \\
Theory Prop Address: & TMbVvz6WT788KucEJn9rQE17f9WVYDdtwv7
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfahpfpgchegjgogbgmg} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{{\mname{ordinal}}~{n}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 274fc409055bdbb382e1defb45f54a49e7f797ab883d97e76722ddad8971f35d \\
Pure Prop Address: & TMKFEu7wFJqZoMviwrZLpLaCP1QjLcwtCwk \\
Theory Prop Id: & 47cd49a599f17ace658f9f1d538502f51cde62c8cd2d997a51ce938eecd15d70 \\
Theory Prop Address: & TMR9b86LuWgjhZL4m5yEvQhHdYU1YcYRkn3
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfbd} ${{\mname{ordinal}}~{1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c94d41f958c74e02ac9b04ef1997708d28df66c7d56e3a98177bfa3ef526a409 \\
Pure Prop Address: & TMT3Q25U1Ux1eVUUm1s1FeitpAvwbXTk1dm \\
Theory Prop Id: & e325a502344d5146d6b51df0408cd431c99b978bd785e7aebd69d0cbd1d3630a \\
Theory Prop Address: & TMLMkFbUXyMVHafQwFnHAFJwHJiUL8uizu8
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfcd} ${{\mname{ordinal}}~{2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a570756c9f8d8069da7f0920bf81bd27397ddff102f6b7444e080f7bed3390ff \\
Pure Prop Address: & TMFLbGodmA7UJer5TihfdxoFBgHSxZjK3cY \\
Theory Prop Id: & e64a0df795b030c5c40d39ceceb101d04488a3dbf090fae286e8f8e284d9727b \\
Theory Prop Address: & TMEjrJXdnsbDexBJZRJysy6hDoZye5ffvEX
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgngfghgbgpfefchbgogdhdffgeh} ${{\mname{TransSet}}~{\mname{omega}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8e89e66d9788201a152dc0d2e564bf2e428e165c4c240da4dd210f8f102b0b9b \\
Pure Prop Address: & TMNtK2hop4HkuAGDS35C3HQG1M44NKe3USF \\
Theory Prop Id: & c79e752f422afbb22e542dfbd0d6ee1f417aa6fe06a04b74efbecce1e0b036e0 \\
Theory Prop Address: & TMKTjT9CEwmv6ZQwdPQWnn1MRx5wxzNZP5R
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgngfghgbgpfpgchegjgogbgmg} ${{\mname{ordinal}}~{\mname{omega}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3d621a0d65590ab57c57a1848257b5fa064c0e3a4847bb476e17a549b2bb1179 \\
Pure Prop Address: & TMEhcpuAFpHXHFSKrZU9N7ytoAc1KYSKfwJ \\
Theory Prop Id: & 177484ec90afd915b52f7e111ce39d29114b2d0f97fd75908b5de1e8b5a405b4 \\
Theory Prop Address: & TMdVAnxzLqF7mrAcYCABmsfnfihincw4N1F
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegdhfhdgdgpfpgngfghgbgpfpgchegjgogbgmg} ${{\mname{ordinal}}~{({{\mname{ordsucc}}~{\mname{omega}}})}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 66659c006c982a0ac99ea4ff01a85f6f4ff5c6737431c0032276450048e05cdf \\
Pure Prop Address: & TMPkd9dTQz5vTvQaDf2GPn1vNYBQR6FCxTM \\
Theory Prop Id: & ecfad7b774257cdf70613958fe3477637a520ac37c9c970c486229116833e51e \\
Theory Prop Address: & TMF6YnnSCpzaZf1K8mSGfwFbrQh9ZW2n7Y9
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:efchbgogdhdffgehpfpgchegdhfhdgdgpfjeogpfdffhcgbh} ${\unicdcdadad X : {\iota} .  {{{\mname{TransSet}}~{X}}\unicdbdjdcd{\unicdcdadad x \in {X} .  {{{\mname{ordsucc}}~{x}} \subseteq {X}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d5d88203bb9e4f58e19b53c1e5a62f15aedc32de8c5bc76e2580367c4174de4d \\
Pure Prop Address: & TMLQBckdoSFHRuVFwGbGbuRrp1fdK4R87ov \\
Theory Prop Id: & 3c2e4593e300f67b32ba028952543ba0dd7e523521087467b0174ba873c292af \\
Theory Prop Address: & TMTRBiP8XXTzUuthK3uDUFLV6ZLsiJDuXee
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfpgchegdhfhdgdgpfjeogpfdffhcgbh} ${\unicdcdadad \alpha .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{\unicdcdadad \beta \in {\alpha} .  {{{\mname{ordsucc}}~{\beta}} \subseteq {\alpha}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 57345e9c93f2215aa2812d32af6e5102ec8faa4224750fe0e5a65c9f1afcd5ff \\
Pure Prop Address: & TMQpZgVSt9a4G3EQn5TNVzeb9wssdHKNW7u \\
Theory Prop Id: & b00304a76db0c730b04afb1cf7ab4e339ad984c2397a5aa9dfcbe8b7ff5fbb77 \\
Theory Prop Address: & TMaxmykHWjhaXzn1rWbPuqhxTLTTER9wNAp
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfehchjgdgigpgehpgngjhpfpgch} ${\unicdcdadad \alpha \beta : {\iota} .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{{{\mname{ordinal}}~{\beta}}\unicdbdjdcd{{{{\alpha} \in {\beta}}\unicdcdcdid{{\alpha}={\beta}}}\unicdcdcdid{{\beta} \in {\alpha}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 078a34fdf9fecc3740d32b870c8d09ccc0128f7642e5b75098ade0d1089ece30 \\
Pure Prop Address: & TMFhw4k9MkF4Xj6fGtXNVWovjCfNEDFgiCV \\
Theory Prop Id: & 21f2d68bdab52d51a33741771dbbe589a47a82c6a747d3f27f2c6e7e7fb46323 \\
Theory Prop Address: & TMQiHm6s7fQpsV7SnBFtLZFvEeXFV9nDbmm
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfjeogpfpechpfdffhcgbh} ${\unicdcdadad \alpha \beta .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{{{\mname{ordinal}}~{\beta}}\unicdbdjdcd{{{\alpha} \in {\beta}}\unicdcdcdid{{\beta} \subseteq {\alpha}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 70fe0df6b00a9a1cdc3d97c6a8ed1db39034d341a16f8a30bddebf8a0a8b8e4f \\
Pure Prop Address: & TMU41PmuGiADNxp6RQqwepi4ZBaznh8t8Dy \\
Theory Prop Id: & 7b99b0def95577474ca6a6371ba472b8ef499bf320c511f3b539db9524a87727 \\
Theory Prop Address: & TMUy7ee37ThdPDzbRspVTZUkthgdjtEyQYb
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfmgjgogfgbgch} ${\unicdcdadad \alpha \beta .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{{{\mname{ordinal}}~{\beta}}\unicdbdjdcd{{{\alpha} \subseteq {\beta}}\unicdcdcdid{{\beta} \subseteq {\alpha}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3f30a55f5c77831d749f6727a93c5a8bce525eb93957884747af3b16fd2817dc \\
Pure Prop Address: & TMPY4A7R7aYy2invvHTTAywc1usxqJAm5u8 \\
Theory Prop Id: & 3b1fce49dbbdca0b438f6709b0e0a85233faa824682dcf5ed3f74df3c3bb6ea0 \\
Theory Prop Address: & TMM2dfXndDyhGP7QGpLd2hvEgv48peHsWcx
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfpgchegdhfhdgdgpfjeogpffgbh} ${\unicdcdadad \alpha \beta .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{{{\beta} \in {\alpha}}\unicdbdjdcd{{{{\mname{ordsucc}}~{\beta}} \in {\alpha}}\unicdcdcdid{{\alpha}={{\mname{ordsucc}}~{\beta}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 500378eb85429ae7b33a80121ead8cda752628caffbde51467158317d0e18d74 \\
Pure Prop Address: & TMHGn9G1ExDEjiH1MPhwk1Vyodkz876yMRi \\
Theory Prop Id: & 0c19e771defd6f69e7d104285ac72cf1f7b2cf9c9100d4849916879cb6681814 \\
Theory Prop Address: & TMVF297QZUVVpWRs4i96ncxvbVNynLTkL7q
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfmgjgngpfpgchpfdhfhdgdg} ${\unicdcdadad \alpha .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{{({\unicdcdadad \beta \in {\alpha} .  {{{\mname{ordsucc}}~{\beta}} \in {\alpha}}})}\unicdcdcdid{({\unicdcdaddd \beta \in {\alpha} .  {{\alpha}={{\mname{ordsucc}}~{\beta}}}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4450c013030397143dd5b0c0a5fc68ccac288751c8cd230b4f4abcdeec1c5c6d \\
Pure Prop Address: & TMankcEMnZXFAP8cvcfDqwi1HBKu5b8txfW \\
Theory Prop Id: & a12697d237d0a645eb8cbf1e70cd0b6d46292c225e8a36a42a59dbe9350e27f6 \\
Theory Prop Address: & TMLRGTTc9BqSSZNBMbxF34StFhkCfsPU8B7
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfpgchegdhfhdgdgpfjeog} ${\unicdcdadad \alpha .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{\unicdcdadad \beta \in {\alpha} .  {{{\mname{ordsucc}}~{\beta}} \in {{\mname{ordsucc}}~{\alpha}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f4b1ed473dc1d1af402cb8a1a56b16920553d37b8b365cf4e72a74e2467668f7 \\
Pure Prop Address: & TMZQdYrrW7LPMeUbwQJGaSaWYZJ342j6TLR \\
Theory Prop Id: & 8ab1dc0a15cde7e11ff2fda7e5194042b72dc495121dbe98a3cb9d5f23df0650 \\
Theory Prop Address: & TMF2GA2skuyQZS3EhFZYEwjYb1i5V7CiuYY
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfffogjgpgog} ${\unicdcdadad X .  {{({\unicdcdadad x \in {X} .  {{\mname{ordinal}}~{x}}})}\unicdbdjdcd{{\mname{ordinal}}~{({{\mname{Union}}~{X}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c733ee1a1d9fd2449e70663578b0382c3bccae896c32e0ec362f1494fda06c3e \\
Pure Prop Address: & TMW1Z5hkuor8TPuLNVR1zbiXXaoiAEs63WD \\
Theory Prop Id: & 8f2519b0a9c7cdd7d42c73a6733e14191e924dccd043f97339e7ea377d746f2b \\
Theory Prop Address: & TMJhDobuvDdYqLTuiL9wE7gzst4xAaHHwqt
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfggbgngfhogjgpgog} ${\unicdcdadad X .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x \in {X} .  {{\mname{ordinal}}~{({{F}~{x}})}}})}\unicdbdjdcd{{\mname{ordinal}}~{({\unicdcddedd _{x \in {X}}{{F}~{x}}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fc035982e0d1f528e70c7a7b191727c9d3afc3eb8cde8f6cf06880f52db2e3d4 \\
Pure Prop Address: & TMU1RzbEJzVnikGUeRHDEeJKZdU2gv4Lu9U \\
Theory Prop Id: & b3f1e1ecfee50fc6903bc622a5d3170a7e8f834e8b8e4cd173ce0c699d33d141 \\
Theory Prop Address: & TMNBvDL5kWic9wxjPXEkTh7WAf3f2AnJ1NW
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfcgjgogjgogehfgchdhfgdgeh} ${\unicdcdadad \alpha \beta .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{{{\mname{ordinal}}~{\beta}}\unicdbdjdcd{{\mname{ordinal}}~{({{\alpha}\unicdcdcdjd{\beta}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 43d507cd3ab7cd23861b8705272c6f88b7930ceecde12dab179ead328e6a2cd6 \\
Pure Prop Address: & TMGAFLa8mQYJ6L1kp1WKCNwaY3YrMwPqad2 \\
Theory Prop Id: & 0253282876aaa86e7cea3ea89459e20513307e9d2b9ffe1cc2ba50b357bbb4a9 \\
Theory Prop Address: & TMQLySje1TXDy7YnSUR855qqzweodR4BBbP
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfcgjgogfhogjgpgog} ${\unicdcdadad \alpha \beta .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{{{\mname{ordinal}}~{\beta}}\unicdbdjdcd{{\mname{ordinal}}~{({{\alpha}\unicdcdcdbg{\beta}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 861ae3bbc499b574608e38df76236c43f8ff5f552de1d70b9002feb31d7edc87 \\
Pure Prop Address: & TMWj1DiEDHWbFoRK4tceGziMDSzNMjXvATC \\
Theory Prop Id: & b24989c4f74b8369768af389e0867d9ae88d987aae3abe7414441666572cf91a \\
Theory Prop Address: & TMb8JjtU8NrQYjHW2dN4KBHmc6dZLD8tX2H
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfdffgah} ${\unicdcdadad \alpha .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{({\unicdcdadad \beta \in {\alpha} .  {\unicdcdadad \gamma \in {\beta} .  {{{p}~{\beta}}\unicdbdjdcd{{p}~{\gamma}}}}})}\unicdbdjdcd{{\mname{ordinal}}~{\{\beta \in {\alpha}|{{p}~{\beta}}\}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9c0d4265c1c0802cb20047122fd9d5c097bbab37a60f64d593b6a44e1bd26859 \\
Pure Prop Address: & TMMc3fJbFMyUS6zszTmv9rSMmYJS2mMJVFh \\
Theory Prop Id: & b5f69f338e4258431a3a6159a38976e853cda2445044d06e4ed0a660100c1a65 \\
Theory Prop Address: & TMHv1MoXTBWSqnddBfw56ZCoB3HkEABQP52
\end{tabular}
\end{center}

\end{theorem}
