---

Step * of Lemma subtype_rel_transitivity

No Annotations
∀[A,B,C:Type].  (A ⊆r C) supposing ((B ⊆r C) and (A ⊆r B))
BY
{ Auto }

1
1. A : Type
2. B : Type
3. C : Type
4. A ⊆r B
5. B ⊆r C
⊢ A ⊆r C

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B,C:Type].    (A  \msubseteq{}r  C)  supposing  ((B  \msubseteq{}r  C)  and  (A  \msubseteq{}r  B))


By

---

Latex:
Auto

---

Home Index