---

Step * of Lemma int_seg_subtype_nat

∀[a,b:ℤ].  {a..b-} ⊆r ℕ supposing 0 ≤ a
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].    \{a..b\msupminus{}\}  \msubseteq{}r  \mBbbN{}  supposing  0  \mleq{}  a


By

---

Latex:
Auto

---

Home Index