---

Step * of Lemma is-above-subtype

∀[A,B:Type].  ∀[a:A]. ∀[z:Base].  (is-above(A;a;z) ⇒ is-above(B;a;z)) supposing A ⊆r B
BY
{ ((Auto THEN ParallelLast) THEN ExRepD) }

1
1. [A] : Type
2. [B] : Type
3. A ⊆r B
4. [a] : A
5. [z] : Base
6. y : Base@i
7. y = a ∈ A@i
8. y ≤ z@i
⊢ ∃y:Base. ((y = a ∈ B) ∧ (y ≤ z))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    \mforall{}[a:A].  \mforall{}[z:Base].    (is-above(A;a;z)  {}\mRightarrow{}  is-above(B;a;z))  supposing  A  \msubseteq{}r  B


By

---

Latex:
((Auto  THEN  ParallelLast)  THEN  ExRepD)

---

Home Index