---

Step * of Lemma groupoid-inv_wf

∀[G:Groupoid]. ∀[x,y:cat-ob(cat(G))]. ∀[x_y:cat-arrow(cat(G)) x y].  (groupoid-inv(G;x;y;x_y) ∈ cat-arrow(cat(G)) y x)
BY
{ ((ProveWfLemma THEN D 1) THEN All (RepUR ``groupoid-cat``) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[G:Groupoid].  \mforall{}[x,y:cat-ob(cat(G))].  \mforall{}[x$_{y}$:cat-arrow(cat(G))  x  y].
    (groupoid-inv(G;x;y;x$_{y}$)  \mmember{}  cat-arrow(cat(G))  y  x)


By

---

Latex:
((ProveWfLemma  THEN  D  1)  THEN  All  (RepUR  ``groupoid-cat``)  THEN  Auto)

---

Home Index