---

Step * of Lemma equipollent-subtract-one

∀a:ℕ. ∀i:ℕa.  {x:ℕa| ¬(x = i ∈ ℕa)}  ~ ℕa - 1
BY
{ xxx(Auto THEN BLemma `equipollent-subtract`  THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}.  \mforall{}i:\mBbbN{}a.    \{x:\mBbbN{}a|  \mneg{}(x  =  i)\}    \msim{}  \mBbbN{}a  -  1


By

---

Latex:
xxx(Auto  THEN  BLemma  `equipollent-subtract`    THEN  Auto)xxx

---

Home Index