---

Step * 1 of Lemma bottom-member-approx-type


1. T : Type
2. T
⊢ ↓∃t:Base. ((⊥ ≤ t) ∧ (t ∈ T))
BY
{ (UseWitness ⌜Ax⌝⋅ THEN RenameVar `t' (-1) THEN (PointwiseFunctionalityForEquality (-1) THENA Auto)) }

1
1. T : Type
2. t : Base
3. t1 : Base
4. t = t1 ∈ T
⊢ Ax = Ax ∈ (↓∃t:Base. ((⊥ ≤ t) ∧ (t ∈ T)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  T
\mvdash{}  \mdownarrow{}\mexists{}t:Base.  ((\mbot{}  \mleq{}  t)  \mwedge{}  (t  \mmember{}  T))


By

---

Latex:
(UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  RenameVar  `t'  (-1)  THEN  (PointwiseFunctionalityForEquality  (-1)  THENA  Auto))

---

Home Index