---

Step * of Lemma add-member-int_seg1

∀[k,m,n,x:ℤ].  uiff(k + x ∈ {m..n-};x ∈ {m - k..n - k-})
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[k,m,n,x:\mBbbZ{}].    uiff(k  +  x  \mmember{}  \{m..n\msupminus{}\};x  \mmember{}  \{m  -  k..n  -  k\msupminus{}\})


By

---

Latex:
Auto

---

Home Index