---

Step * 1 1 of Lemma member-approx-type


1. T : Type
2. x : Base
3. x = x ∈ approx-type(T)
4. [%2] : λ2x y.approx-per(T;x;y) x x
⊢ ↓∃t:Base. ((x ≤ t) ∧ (t ∈ T))
BY
{ (Unhide THEN RepUR ``so_lambda`` -1 THEN D -1 THEN D -2 THEN D 0 THEN Trivial) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  Base
3.  x  =  x
4.  [\%2]  :  \mlambda{}\msubtwo{}x  y.approx-per(T;x;y)  x  x
\mvdash{}  \mdownarrow{}\mexists{}t:Base.  ((x  \mleq{}  t)  \mwedge{}  (t  \mmember{}  T))


By

---

Latex:
(Unhide  THEN  RepUR  ``so\_lambda``  -1  THEN  D  -1  THEN  D  -2  THEN  D  0  THEN  Trivial)

---

Home Index