---

Step * 2 of Lemma equipollent-nsub


1. n : ℕ
2. m : ℕ
3. ℕn ~ ℕm
⊢ n = m ∈ ℤ
BY
{ xxx(Assert ℕm ~ ℕn BY
            (RelRST THEN Auto))xxx }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  \mBbbN{}n  \msim{}  \mBbbN{}m
\mvdash{}  n  =  m


By

---

Latex:
xxx(Assert  \mBbbN{}m  \msim{}  \mBbbN{}n  BY
                    (RelRST  THEN  Auto))xxx

---

Home Index