---

Step * of Lemma add-member-int_seg2

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index