---

Step * of Lemma is-above-axiom-general

∀[T:Type]. ∀[z:Base]. z ~ Ax supposing is-above(T;Ax;z) supposing T ⊆r Base
BY
{ ((Unfold `is-above` 0 THEN Auto) THEN RepeatFor 2 (D -1) THEN HypSubst' (-2) (-1)) }

1
1. T : Type
2. T ⊆r Base
3. z : Base
4. y : Base
5. y = Ax ∈ T
6. Ax ≤ z
⊢ z = Ax ∈ Base

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[z:Base].  z  \msim{}  Ax  supposing  is-above(T;Ax;z)  supposing  T  \msubseteq{}r  Base


By

---

Latex:
((Unfold  `is-above`  0  THEN  Auto)  THEN  RepeatFor  2  (D  -1)  THEN  HypSubst'  (-2)  (-1))

---

Home Index