\chapter{Comparing the Sizes of Sets}

\begin{definition}\label{def:jgogkg}
We define $\mname{inj}$ to be ${\uniddcgcg X Y f .  {{({\unicdcdadad u \in {X} .  {{{f}~{u}} \in {Y}}})}\unicdcdcdhd{({\unicdcdadad u v \in {X} .  {{{{f}~{u}}={{f}~{v}}}\unicdbdjdcd{{u}={v}}}})}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{o}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 264b04a8ece7fd74ec4abb7dd2111104a2e6cde7f392363afe4acca8d5faa416 \\
Pure Object Address: & TMQsS5cocdJLxvSrfwFrtyVb2HtH4sHnoSq \\
Theory Object Id: & 442958a234e56cda2843c516d8ba0be921c19f4486af20ea18cd78e0b5587a8e \\
Theory Object Address: & TMEtNCh6NfJv35kUGcgFB52zooWEchr4mq3
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:dhfhchkg}
We define $\mname{surj}$ to be ${\uniddcgcg X Y f .  {{({\unicdcdadad u \in {X} .  {{{f}~{u}} \in {Y}}})}\unicdcdcdhd{({\unicdcdadad w \in {Y} .  {\unicdcdaddd u \in {X} .  {{{f}~{u}}={w}}}})}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{o}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 4b68e472ec71f7c8cd275af0606dbbc2f78778d7cbcc9491f000ebf01bcd894c \\
Pure Object Address: & TMcR6n2BpcwoiDwRhTtfhBS2wRexeumPoBF \\
Theory Object Id: & f022f92791e019fecb8ae163b387436a5af8f1fc86e8403db0d2add2d326d2cc \\
Theory Object Address: & TMSbXiP7EjGYNy1Jeo9r2YG6YXA8qunsPXV
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:cgjgkg}
We define $\mname{bij}$ to be
$$
\begin{array}{c}
\uniddcgcg X Y f .  {({\unicdcdadad u \in {X} .  {{{f}~{u}} \in {Y}}})} \\
\unicdcdcdhd{({\unicdcdadad u v \in {X} .  {{{{f}~{u}}={{f}~{v}}}\unicdbdjdcd{{u}={v}}}})} \\
\unicdcdcdhd ({\unicdcdadad w \in {Y} .  {\unicdcdaddd u \in {X} .  {{{f}~{u}}={w}}}})
\end{array}
$$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{o}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 76bef6a46d22f680befbd3f5ca179f517fb6d2798abc5cd2ebbbc8753d137948 \\
Pure Object Address: & TMWBv3fDiJHG6PbQ5p9tmBynBsCvJmYFGXN \\
Theory Object Id: & f7d93b7e704e3215ae66ae7c330f283bc8b4b71850013429da3d75d7ab6ee432 \\
Theory Object Address: & TMWitYCyjoeiXGg1451hhTG6x1DmSshpEsw
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
bijI
\end{verbatim}
\begin{theorem}\label{thm:cgjgkgje}
$$
\begin{array}{c}
\unicdcdadad X Y .  \unicdcdadad f : {{\iota}\unicdbdjdcd{\iota}} .  {({\unicdcdadad u \in {X} .  {{{f}~{u}} \in {Y}}})}\unicdbdjdcd{({\unicdcdadad u v \in {X} .  {{{{f}~{u}}={{f}~{v}}}\unicdbdjdcd{{u}={v}}}})}\\\unicdbdjdcd{{({\unicdcdadad w \in {Y} .  {\unicdcdaddd u \in {X} .  {{{f}~{u}}={w}}}})}\unicdbdjdcd{{{{\mname{bij}}~{X}}~{Y}}~{f}}}.
\end{array}
$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a9064fdc226bed9225585cb4f2610b131c0a14aad760bfeb55112ab19f50c269 \\
Pure Prop Address: & TMVtA5kA7XycdNhnjcWoD7YH6yuuhkFVjMt \\
Theory Prop Id: & 3229f986ac1acb74b9c25702305e679c33fee187075ba5e7e5521402a44407f4 \\
Theory Prop Address: & TMHZ6dKwiqgD43Q9CKokQdMMtyUWTqNe73b
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
bijE
\end{verbatim}
\begin{theorem}\label{thm:cgjgkgfe}
$$
\begin{array}{c}
\unicdcdadad X Y .  \unicdcdadad f : {{\iota}\unicdbdjdcd{\iota}} .  {{{{\mname{bij}}~{X}}~{Y}}~{f}}\unicdbdjdcd\unicdcdadad p : {o} .\\  ({{({\unicdcdadad u \in {X} .  {{{f}~{u}} \in {Y}}})}\unicdbdjdcd{{({\unicdcdadad u v \in {X} .  {{{{f}~{u}}={{f}~{v}}}\unicdbdjdcd{{u}={v}}}})}\unicdbdjdcd{{({\unicdcdadad w \in {Y} .  {\unicdcdaddd u \in {X} .  {{{f}~{u}}={w}}}})}\unicdbdjdcd{p}}}})\\
\unicdbdjdcd{p}.
\end{array}
$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2cf2785657b7836bb8cf1988ba517c500841f4597e31341232a8e4ae9a2ac11b \\
Pure Prop Address: & TMPhihHJHHFvCn9A4dYL5TQ6pqHpkEvceX8 \\
Theory Prop Id: & cf075922dfef18d341a5a232bb48285fa39e11a63b966fd9557f7bbc707557bc \\
Theory Prop Address: & TMVhokQU6h9PfVvoAJ7Se6F6yDdFRx38gX3
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:jgoggh}
$\mname{inv}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 896fa967e973688effc566a01c68f328848acd8b37e857ad23e133fdd4a50463 \\
Pure Object Address: & TMYsHRgQQXjN5d3YZ2sLdp9j73Hd4HiYRei \\
Theory Object Id: & f3a0156f444b33934c3c28ed4b3f22eae35078c37c1e0c9f4f931d3c1e1c9266 \\
Theory Object Address: & TMNXEs7Lfg3PCmc11RhANqjcTXio2UJSNhw
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
surj_rinv
\end{verbatim}
\begin{theorem}\label{thm:dhfhchkgpfchjgoggh}
$${\unicdcdadad X Y .  {\unicdcdadad f : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad w \in {Y} .  {\unicdcdaddd u \in {X} .  {{{f}~{u}}={w}}}})}\unicdbdjdcd{\unicdcdadad y \in {Y} .  {{{{{{\mname{inv}}~{X}}~{f}}~{y}} \in {X}}\unicdcdcdhd{{{f}~{({{{{\mname{inv}}~{X}}~{f}}~{y}})}}={y}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ebf3718d5c90ac32637e5ff7de771588bd899f20728aac1c034cc4575a9f2bd5 \\
Pure Prop Address: & TMdfPpzpdtB7VwgaPueTNcMshHsVs117kuo \\
Theory Prop Id: & 6489d2e57f0dee884152f4a33ad50d245f1c35dc285ca99ba09b67a783f89c93 \\
Theory Prop Address: & TMVFndmdYppMYsHoVKPEwfE1yfNTP6HYsK6
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
inj_linv
\end{verbatim}
\begin{theorem}\label{thm:jgogkgpfmgjgoggh} $${\unicdcdadad X Y .  {\unicdcdadad f : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad u v \in {X} .  {{{{f}~{u}}={{f}~{v}}}\unicdbdjdcd{{u}={v}}}})}\unicdbdjdcd{\unicdcdadad x \in {X} .  {{{{{\mname{inv}}~{X}}~{f}}~{({{f}~{x}})}}={x}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f9fc2fb6cfb4eb217cfd90f255fb35b64bd1729aa515ae6c662014a80909baf4 \\
Pure Prop Address: & TMEuKQvRXDUoH8sLbTA8MpzpoVNt2Uo41RH \\
Theory Prop Id: & 74870e1df65b0cc2ae2c71c585c9735524f602fc82ed42ac4a046496a20db8bd \\
Theory Prop Address: & TMTFjNxnxSQzmggpMN48iCzGFGMZ6u5HUUU
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
bij_inv
\end{verbatim}
\begin{theorem}\label{thm:cgjgkgpfjgoggh} ${\unicdcdadad X Y .  {\unicdcdadad f : {{\iota}\unicdbdjdcd{\iota}} .  {{{{{\mname{bij}}~{X}}~{Y}}~{f}}\unicdbdjdcd{{{{\mname{bij}}~{Y}}~{X}}~{({{{\mname{inv}}~{X}}~{f}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ff1332269c5993981bc337566181eb6a5ac760b35f3e8f90eed0abf70ebc7c17 \\
Pure Prop Address: & TMRvnWitWbimHQFYgNtor4w8xmFZq6WVJT5 \\
Theory Prop Id: & 69c53767bc4248c32eca1d3c840bc6ee0513e90488a4e3d38dba20033986cce4 \\
Theory Prop Address: & TMYU31Q8vC6ff6UyuWLEMF43Pms8CHUmb2x
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
bij_comp
\end{verbatim}
\begin{theorem}\label{thm:cgjgkgpfdgpgngah} ${\unicdcdadad X Y Z : {\iota} .  {\unicdcdadad f g : {{\iota}\unicdbdjdcd{\iota}} .  {{{{{\mname{bij}}~{X}}~{Y}}~{f}}\unicdbdjdcd{{{{{\mname{bij}}~{Y}}~{Z}}~{g}}\unicdbdjdcd{{{{\mname{bij}}~{X}}~{Z}}~{({\uniddcgcg x .  {{g}~{({{f}~{x}})}}})}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & abf85117d4cc5830f8c4e2302319f45ffb293b1c89044d95312722edcc59ebda \\
Pure Prop Address: & TMbJ4RHULgz1EDJb4kgryxvfAijajbPaBWZ \\
Theory Prop Id: & 4c90458f330b4d7cdc780aefbd2a209237607b7b0ce813a26728e290eaf8ae8e \\
Theory Prop Address: & TMMeMmBNYFCGY7zJTLg49As2Zm5US2hziHm
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
bij_id
\end{verbatim}
\begin{theorem}\label{thm:cgjgkgpfjgeg} ${\unicdcdadad X .  {{{{\mname{bij}}~{X}}~{X}}~{({\uniddcgcg x .  {x}})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a8cefb4071a07310e8c514fb13ecd4fb64481818a12472770c065383dc391c08 \\
Pure Prop Address: & TMKDAnvGLshjhnT7DcuJYqVH8EphuBsUUcs \\
Theory Prop Id: & 707f370beec6bb62870cc94c9fa8f45ced6eaaf202ba0af81dab213981d7b6a9 \\
Theory Prop Address: & TMFbyfnRF5QWxotLuNUgJzCGP2XV6QZ4y1c
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
bij_inj
\end{verbatim}
\begin{theorem}\label{thm:cgjgkgpfjgogkg} ${\unicdcdadad X Y .  {\unicdcdadad f : {{\iota}\unicdbdjdcd{\iota}} .  {{{{{\mname{bij}}~{X}}~{Y}}~{f}}\unicdbdjdcd{{{{\mname{inj}}~{X}}~{Y}}~{f}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e3635e28871703e7f8247d1db9057e8a348d2ccd04747dd154febb02a37f9401 \\
Pure Prop Address: & TMMrgAbiSR6cnvcK7CVfGRP9kNu67vN98ZP \\
Theory Prop Id: & 00097cfdcf04769f3acdf746b6155be23b2782a6c12e002b03fecfc4ed998644 \\
Theory Prop Address: & TMRRNL1K8TWBDtgrjqzbQBsxYHZsqGCVu11
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
bij_surj
\end{verbatim}
\begin{theorem}\label{thm:cgjgkgpfdhfhchkg} ${\unicdcdadad X Y .  {\unicdcdadad f : {{\iota}\unicdbdjdcd{\iota}} .  {{{{{\mname{bij}}~{X}}~{Y}}~{f}}\unicdbdjdcd{{{{\mname{surj}}~{X}}~{Y}}~{f}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e7a049991e8ce73cb9d2cde3714035b3bfd567ffd29a6588380d6afe28d0d422 \\
Pure Prop Address: & TMZ1Df2XJMAY4VQtRKyVeYTrjgp9uNrkat1 \\
Theory Prop Id: & 7fa9a5a19214ed9b46b7c2672858b7198b12a117652c2884ba242b0d3023bb78 \\
Theory Prop Address: & TMK69KkYqvqjbC3pgQQ4xrkBTDfGpX9dhLN
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
inj_surj_bij
\end{verbatim}
\begin{theorem}\label{thm:jgogkgpfdhfhchkgpfcgjgkg} ${\unicdcdadad X Y .  {\unicdcdadad f : {{\iota}\unicdbdjdcd{\iota}} .  {{{{{\mname{inj}}~{X}}~{Y}}~{f}}\unicdbdjdcd{{{{{\mname{surj}}~{X}}~{Y}}~{f}}\unicdbdjdcd{{{{\mname{bij}}~{X}}~{Y}}~{f}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ccff0258f3d7f02dbb9c92e1c2c588c500749a613923b0ece6497a2266072218 \\
Pure Prop Address: & TMZSLNi3XSR9xpWQPVMJxKdbpuqMGcXGcTa \\
Theory Prop Id: & de895fd8c8d353a1a3e58226dea93e0bcab39207eaea6f1bd63ca76728da5443 \\
Theory Prop Address: & TMKfqwemEJSEU94d4EWk9R5Z9o4KFevVF79
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
surj_inv_inj
\end{verbatim}
\begin{theorem}\label{thm:dhfhchkgpfjgogghpfjgogkg} ${\unicdcdadad X Y .  {\unicdcdadad f : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad y \in {Y} .  {\unicdcdaddd x \in {X} .  {{{f}~{x}}={y}}}})}\unicdbdjdcd{{{{\mname{inj}}~{Y}}~{X}}~{({{{\mname{inv}}~{X}}~{f}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ea4775ce7b91dca8fcab0b476c6da12b3812e7c3bb1c40ac217ef8ec4f7e2421 \\
Pure Prop Address: & TMMfpEoFj9egg8ymZiXFBa7mqr6V1aAyR52 \\
Theory Prop Id: & dde3b90d9180ac2126f48d3f539c000ff8f515f94358c02d782de14599dfd8e8 \\
Theory Prop Address: & TMYyJkfwSTRDidng9k7W8zBoQ7M964PoQu8
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:bgehmgfgbgdhehah}
We define $\mname{atleastp}$ to be ${\uniddcgcg X Y : {\iota} .  {\unicdcdaddd f : {{\iota}\unicdbdjdcd{\iota}} .  {{{{\mname{inj}}~{X}}~{Y}}~{f}}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 9bb9c2b375cb29534fc7413011613fb9ae940d1603e3c4bebd1b23c164c0c6f7 \\
Pure Object Address: & TMdn3jbiRnktYr3yHQk9h3fe2hNUWwmbigq \\
Theory Object Id: & 13545c645a339da15781ed2b2b387176e9241a5497e95448eb000efd67f60842 \\
Theory Object Address: & TMVULsv3UtPX7zQrujvLPr8j5YcesgYNBcQ
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:fgbhfhjgah}
We define $\mname{equip}$ to be ${\uniddcgcg X Y : {\iota} .  {\unicdcdaddd f : {{\iota}\unicdbdjdcd{\iota}} .  {{{{\mname{bij}}~{X}}~{Y}}~{f}}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & eb44199255e899126f4cd0bbf8cf2f5222a90aa4da547822cd6d81c671587877 \\
Pure Object Address: & TMQwX3qjReYJVk5GFFSX3Mc3FXLfVZVK9kz \\
Theory Object Id: & 7f2bf6cf81f51f17f6ce5c2dbf188c600cd671933bce98176ab19c48014cea47 \\
Theory Object Address: & TMLBEa2WvRd6EvHsbywWEHTnGKb6kqvBVtd
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
equip_ref
\end{verbatim}
\begin{theorem}\label{thm:fgbhfhjgahpfchfggg} ${\unicdcdadad X .  {{{\mname{equip}}~{X}}~{X}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & cc7e804a09044eda808398af78c405e10d681cf2d3ebd1e427405bb3a0f82f4b \\
Pure Prop Address: & TMYk6cm3eVPFH29r4U5oDKnwrrdfovk75q8 \\
Theory Prop Id: & c41fb1856e522372cc47cfb80303fc14cb2d9b7b560c6fbb7b1e6aa94caf89c4 \\
Theory Prop Address: & TMXscfQQ6JtEo6wQ2rvbuRae4u8ghd3TmK3
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
equip_sym
\end{verbatim}
\begin{theorem}\label{thm:fgbhfhjgahpfdhjhng} ${\unicdcdadad X Y .  {{{{\mname{equip}}~{X}}~{Y}}\unicdbdjdcd{{{\mname{equip}}~{Y}}~{X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f289541b211153f721f213a25c59969aa4873f985ed3dadb265f68134c24c94e \\
Pure Prop Address: & TMY2oL6NVAFGfyVKFHZtMwxnebWdEANu4RE \\
Theory Prop Id: & 272f04ef14a36c414e4557b20a0d2296a32dc853b3ed7c4ee2a194386feabcb3 \\
Theory Prop Address: & TMP5Vsiypad2yczNmG9eU243SqUyrcsGC6w
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
equip_tra
\end{verbatim}
\begin{theorem}\label{thm:fgbhfhjgahpfehchbg} ${\unicdcdadad X Y Z .  {{{{\mname{equip}}~{X}}~{Y}}\unicdbdjdcd{{{{\mname{equip}}~{Y}}~{Z}}\unicdbdjdcd{{{\mname{equip}}~{X}}~{Z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 322bfbeb779343f7873d6478ed537f6d26e801c3b1dbd29367976be6a6a8cd1e \\
Pure Prop Address: & TMP3Pyh4cMndHz7KEMSUcuThjZ8NUECDxnz \\
Theory Prop Id: & d616c1609dd61f5c209c6cb476fcba79031210d81c19459ab45828203b68f961 \\
Theory Prop Address: & TMMPNzj7ZfCkfZFdbzZMRPAohztBSpmcrY9
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:ggjgogjgehfg}
We define $\mname{finite}$ to be ${\uniddcgcg X .  {\unicdcdaddd n \in {\mname{omega}} .  {{{\mname{equip}}~{X}}~{n}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 04632dc85b4cfa9259234453a2464a187d6dfd480455b14e1e0793500164a7e3 \\
Pure Object Address: & TMTx9uDMYWFe7F4kG1CvRU871EPE4S3LaMV \\
Theory Object Id: & 4c54a587d9d6957aacb640a264f675f93a1254e92f4c6f7aad082ab5a4350c68 \\
Theory Object Address: & TMFKGVLZA5xtkoBs7Z7ZUYc2RvcSeaNRv3v
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:jgogggjgogjgehfg}
We define $\mname{infinite}$ to be ${\uniddcgcg X .  {\preoh{{{\mname{finite}}~{X}}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 313e7b5980d710cf22f2429583d0c3b8404586d75758ffcab45219ac373fbc58 \\
Pure Object Address: & TMasuVNeN4ZSGDYVEGFs8RGYS2DpDeugNiN \\
Theory Object Id: & fad8eaad083b98f773fe61e7e4c9c8e42ee4b7b5b96a8a831500e0f2097c3ccf \\
Theory Object Address: & TMUDie5EKa9EaiBtjwiXwQDYd6oF2q9cCbx
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
KnasterTarski_set
\end{verbatim}
\begin{theorem}\label{thm:leogbgdhehfgchefbgchdhlgjgpfdhfgeh}
$$\begin{array}{c}
\unicdcdadad A .  \unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {({\unicdcdadad U \in {{\mname{Power}}~{A}} .  {{{F}~{U}} \in {{\mname{Power}}~{A}}}})}\unicdbdjdcd\\
{{({\unicdcdadad U V \in {{\mname{Power}}~{A}} .  {{{U} \subseteq {V}}\unicdbdjdcd{{{F}~{U}} \subseteq {{F}~{V}}}}})}\unicdbdjdcd{\unicdcdaddd Y \in {{\mname{Power}}~{A}} .  {{{F}~{Y}}={Y}}}}.
\end{array}
$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2ffb9f17db9abba2e99cdc9e9ea64f507ea8b974c232ad295e4047e204a3c2df \\
Pure Prop Address: & TMGYc2cyt576aoAHoJnf5fmecWDttyfoAEA \\
Theory Prop Id: & 31ef9df03eb42ad3c6e310449b514b042b286ecbe91fd6d663ff0cb8c38f9bcc \\
Theory Prop Address: & TMVA6dF8zyCJrTc6aSsUANd7jk3viaeNZ4W
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
image_In_Power
\end{verbatim}
\begin{theorem}\label{thm:jgngbghgfgpfjeogpfafpghhfgch} $${\unicdcdadad A B .  {\unicdcdadad f : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x \in {A} .  {{{f}~{x}} \in {B}}})}\unicdbdjdcd{\unicdcdadad U \in {{\mname{Power}}~{A}} .  {{\{{{f}~{x}}|x \in {U}\}} \in {{\mname{Power}}~{B}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6799e88e9e80af6a6d035ad42a185bfe8562bd1a6140b5c7d8848156518b59f1 \\
Pure Prop Address: & TMbqTvjYLewp4gH2vMecz4sa5m85ihte7rH \\
Theory Prop Id: & 43ed06ac181dbddeb1e0701aeafd6b2b48bdf7da7d513e9c557e99bbc7534b05 \\
Theory Prop Address: & TMXRAfJAyZSv2buTnY3cuenqyFKCq8KC47T
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
image_monotone
\end{verbatim}
\begin{theorem}\label{thm:jgngbghgfgpfngpgogpgehpgogfg} ${\unicdcdadad f : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad U V .  {{{U} \subseteq {V}}\unicdbdjdcd{{\{{{f}~{x}}|x \in {U}\}} \subseteq {\{{{f}~{x}}|x \in {V}\}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ac6fe8101f40a432ad82f07e1e2665c922b286ef3145bb1445a03166259e236f \\
Pure Prop Address: & TMP3hoEqEfoP9GJwJnrLJ876qGy57htpeFQ \\
Theory Prop Id: & f923c6e98034954cfdec182ed28c5f254354e531c01861ce39d38a6191a03629 \\
Theory Prop Address: & TMHKKD8maX4Ek8ApzVty5uJ6NuWSzXkpFib
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminus_In_Power
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhpfjeogpfafpghhfgch} ${\unicdcdadad A U .  {{{A}\unicdcdbdgd{U}} \in {{\mname{Power}}~{A}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 062275a787c47ab2b1e0a2473d1970002748ce7a53f286abe400bbb934df521c \\
Pure Prop Address: & TMS4pSRxLA1Dbq2igDLXVVHw7nhdRCiv3XJ \\
Theory Prop Id: & f503e1c5ae49a7f07828b518f3acefa7e8740424fa3207093249cc6306769e3f \\
Theory Prop Address: & TMPhrNAZaW4G1fJTosqoVHur2BY9wXz7Crc
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminus_antimonotone
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhpfbgogehjgngpgogpgehpgogfg} ${\unicdcdadad A U V .  {{{U} \subseteq {V}}\unicdbdjdcd{{{A}\unicdcdbdgd{V}} \subseteq {{A}\unicdcdbdgd{U}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 67bd0e5333f721c6c4ebed67eb48fac3aaa4d7c9e31ecd29eebad8127a29bc85 \\
Pure Prop Address: & TMKx1CgcNCpQuzLmEaWfsvEuHkFTPgSbL1D \\
Theory Prop Id: & f9b735ec697563f76b4bf8db58fac77a909244fe1f67ee2c99fdd5259caf0064 \\
Theory Prop Address: & TMYUDtXjxfZhhgoCHvxoyj1yVnZ2NwE1zoN
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
SchroederBernstein
\end{verbatim}
\begin{theorem}\label{thm:dfdgigchpgfgegfgchcefgchogdhehfgjgog} ${\unicdcdadad A B .  {\unicdcdadad f g : {{\iota}\unicdbdjdcd{\iota}} .  {{{{{\mname{inj}}~{A}}~{B}}~{f}}\unicdbdjdcd{{{{{\mname{inj}}~{B}}~{A}}~{g}}\unicdbdjdcd{{{\mname{equip}}~{A}}~{B}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e247a892fd3a3a3c6729106e07939389d6cba1af2c7dab631e4a1a2ad18cba2b \\
Pure Prop Address: & TMNErsk8ZdnQDMxX11dVnP6drZGGGUKRnT7 \\
Theory Prop Id: & 03a2cd1c8a567976a696d45296506a96202d6ef88ed050e5bd0781df51d7b9b4 \\
Theory Prop Address: & TMajcAjnmAvQnwV59Qj54uAcCt6LNS6kuqZ
\end{tabular}
\end{center}

\end{theorem}
