---

Step * of Lemma equipollent-int_seg-shift

∀n:ℤ. ∀m:ℕ.  {n..n + m-} ~ ℕm
BY
{ (Auto THEN (RWO  "equipollent-int_seg" 0 THEN Auto) THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbZ{}.  \mforall{}m:\mBbbN{}.    \{n..n  +  m\msupminus{}\}  \msim{}  \mBbbN{}m


By

---

Latex:
(Auto  THEN  (RWO    "equipollent-int\_seg"  0  THEN  Auto)  THEN  AutoSplit)

---

Home Index