---

Step * 1 of Lemma sg-inv-op


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  (x\^{}-1  x)  \mequiv{}  (x\^{}-1  (1  x))  BY
              (RWO  "sg-id-op"  0  THEN  Auto))

---

Home Index