---

Step * 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
{ ((RWO "sg-assoc" 0 THENA Auto) THEN (RW (AddrC [2;2] (RevLemmaC `sg-assoc`)) 0 THENA Auto)) }

1
1. sg : s-Group
2. x : Point
3. y : Point
⊢ ((x (y y^-1)) x^-1) ≡ 1

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "sg-assoc"  0  THENA  Auto)  THEN  (RW  (AddrC  [2;2]  (RevLemmaC  `sg-assoc`))  0  THENA  Auto))

---

Home Index