---

Step * of Lemma poset-cat-arrow_subtype

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

---

Latex:

---

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


By

---

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

---

Home Index