---

Step * of Lemma poset-cat-ob_subtype

∀[I,J:Cname List].  cat-ob(poset-cat(I)) ⊆r cat-ob(poset-cat(J)) supposing nameset(J) ⊆r nameset(I)
BY
{ (RepUR ``cat-ob poset-cat`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I,J:Cname  List].    cat-ob(poset-cat(I))  \msubseteq{}r  cat-ob(poset-cat(J))  supposing  nameset(J)  \msubseteq{}r  nameset(I)


By

---

Latex:
(RepUR  ``cat-ob  poset-cat``  0  THEN  Auto)

---

Home Index