Step * of Lemma poset-cat-ob_subtype

[I,J:Cname List].  cat-ob(poset-cat(I)) ⊆cat-ob(poset-cat(J)) supposing nameset(J) ⊆nameset(I)
BY
(RepUR ``cat-ob poset-cat`` 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