---

Step * 2 1 1 of Lemma equipollent-nsub


1. n : ℕ
2. m : ℕ
3. ℕn ~ ℕm
4. ℕm ~ ℕn
5. n ≤ m
6. m ≤ n
⊢ n = m ∈ ℤ
BY
{ xxxAutoxxx }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  \mBbbN{}n  \msim{}  \mBbbN{}m
4.  \mBbbN{}m  \msim{}  \mBbbN{}n
5.  n  \mleq{}  m
6.  m  \mleq{}  n
\mvdash{}  n  =  m


By

---

Latex:
xxxAutoxxx

---

Home Index