---

Step * 1 of Lemma metric-subspace_wf


1. X : Type
2. d : metric(X)
3. A : Type
⊢ strong-subtype(A;X) ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  A  :  Type
\mvdash{}  strong-subtype(A;X)  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index