---

Step * of Lemma equipollent-subtract

∀a,b:ℕ.  ∀[P:ℕa ⟶ ℙ]. ({x:ℕa| P[x]}  ~ ℕb ⇒ {x:ℕa| ¬P[x]}  ~ ℕa - b)
BY
{ xxx(Auto THEN FLemma `equipollent_inversion` [-1] THEN Auto)xxx }

1
1. a : ℕ
2. b : ℕ
3. [P] : ℕa ⟶ ℙ
4. {x:ℕa| P[x]}  ~ ℕb
5. ℕb ~ {x:ℕa| P[x]} 
⊢ {x:ℕa| ¬P[x]}  ~ ℕa - b

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbN{}.    \mforall{}[P:\mBbbN{}a  {}\mrightarrow{}  \mBbbP{}].  (\{x:\mBbbN{}a|  P[x]\}    \msim{}  \mBbbN{}b  {}\mRightarrow{}  \{x:\mBbbN{}a|  \mneg{}P[x]\}    \msim{}  \mBbbN{}a  -  b)


By

---

Latex:
xxx(Auto  THEN  FLemma  `equipollent\_inversion`  [-1]  THEN  Auto)xxx

---

Home Index