---

Step * of Lemma name-morph_subtype

∀[I,J,A,B:Cname List].
  (name-morph(I;J) ⊆r name-morph(A;B)) supposing ((nameset(A) ⊆r nameset(I)) and (nameset(J) ⊆r nameset(B)))
BY
{ Auto }

1
1. I : Cname List
2. J : Cname List
3. A : Cname List
4. B : Cname List
5. nameset(J) ⊆r nameset(B)
6. nameset(A) ⊆r nameset(I)
⊢ name-morph(I;J) ⊆r name-morph(A;B)

---

Latex:

---

Latex:
\mforall{}[I,J,A,B:Cname  List].
    (name-morph(I;J)  \msubseteq{}r  name-morph(A;B))  supposing 
          ((nameset(A)  \msubseteq{}r  nameset(I))  and 
          (nameset(J)  \msubseteq{}r  nameset(B)))


By

---

Latex:
Auto

---

Home Index