---

Step * of Lemma equipollent-one

∀[A:Type]. ∀a:A. {x:A| x = a ∈ A}  ~ ℕ1
BY
{ xxx(Auto THEN (BLemma `equipollent-one-iff` THEN Auto) THEN With ⌜a⌝ (D 0)⋅ THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}a:A.  \{x:A|  x  =  a\}    \msim{}  \mBbbN{}1


By

---

Latex:
xxx(Auto  THEN  (BLemma  `equipollent-one-iff`  THEN  Auto)  THEN  With  \mkleeneopen{}a\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)xxx

---

Home Index