---

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


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "sg-assoc"  0  THENA  Auto)
  THEN  (RWO    "sg-op-id"  0  THENA  Auto)
  THEN  (RWO  "sg-assoc<"  0  THENA  Auto)
  THEN  (RWO    "4"  0  THENA  Auto))

---

Home Index