---

Step * of Lemma equipollent-nsub

∀n,m:ℕ.  (n = m ∈ ℤ ⇐⇒ ℕn ~ ℕm)
BY
{ xxxAutoxxx }

1
1. n : ℕ
2. m : ℕ
3. n = m ∈ ℤ
⊢ ℕn ~ ℕm

2
1. n : ℕ
2. m : ℕ
3. ℕn ~ ℕm
⊢ n = m ∈ ℤ

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbN{}.    (n  =  m  \mLeftarrow{}{}\mRightarrow{}  \mBbbN{}n  \msim{}  \mBbbN{}m)


By

---

Latex:
xxxAutoxxx

---

Home Index