---

Step * 1 of Lemma cat_ob_op_lemma


1. C : SmallCategory@i'
⊢ cat-ob(op-cat(C)) ~ cat-ob(C)
BY
{ ((D -1 THEN RepeatFor 3 (D -2)) THEN RepUR ``cat-ob op-cat`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory@i'
\mvdash{}  cat-ob(op-cat(C))  \msim{}  cat-ob(C)


By

---

Latex:
((D  -1  THEN  RepeatFor  3  (D  -2))  THEN  RepUR  ``cat-ob  op-cat``  0  THEN  Auto)

---

Home Index