---

Step * of Lemma partial-strong-subtype-base

∀[T:Type]. ((T ⊆r Base) ⇒ strong-subtype(partial(T);Base))
BY
{ (Auto THEN D 0) }

1
1. T : Type
2. T ⊆r Base
⊢ partial(T) ⊆r Base

2
1. T : Type
2. T ⊆r Base
3. partial(T) ⊆r Base
⊢ {b:Base| ∃a:partial(T). (b = a ∈ Base)}  ⊆r partial(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  ((T  \msubseteq{}r  Base)  {}\mRightarrow{}  strong-subtype(partial(T);Base))


By

---

Latex:
(Auto  THEN  D  0)

---

Home Index