---

Step * of Lemma is-above-int

∀[n:ℤ]. ∀[z:Base].  z = n ∈ ℤ supposing is-above(ℤ;n;z)
BY
{ (Auto THEN RepeatFor 2 (D -1)) }

1
1. n : ℤ
2. z : Base
3. y : Base
4. y = n ∈ ℤ
5. y ≤ z
⊢ z = n ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[z:Base].    z  =  n  supposing  is-above(\mBbbZ{};n;z)


By

---

Latex:
(Auto  THEN  RepeatFor  2  (D  -1))

---

Home Index