---

Step * 1 1 of Lemma sg-inv-of-op


1. sg : s-Group
2. x : Point
3. y : Point
⊢ ((x (y y^-1)) x^-1) ≡ 1
BY
{ (RWW "sg-inv-op sg-op-inv sg-op-id sg-id-op" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  sg  :  s-Group
2.  x  :  Point
3.  y  :  Point
\mvdash{}  ((x  (y  y\^{}-1))  x\^{}-1)  \mequiv{}  1


By

---

Latex:
(RWW  "sg-inv-op  sg-op-inv  sg-op-id  sg-id-op"  0  THEN  Auto)

---

Home Index