---

Step * 1 of Lemma is-above-subtype


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))
BY
{ (With ⌜y⌝ (D 0)⋅ THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  A  \msubseteq{}r  B
4.  [a]  :  A
5.  [z]  :  Base
6.  y  :  Base@i
7.  y  =  a@i
8.  y  \mleq{}  z@i
\mvdash{}  \mexists{}y:Base.  ((y  =  a)  \mwedge{}  (y  \mleq{}  z))


By

---

Latex:
(With  \mkleeneopen{}y\mkleeneclose{}  (D  0)\mcdot{}  THEN  Try  (Complete  (Auto)))

---

Home Index