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