---

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


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO    "sg-assoc<"  (-1)  THENA  Auto)  THEN  (RWW  "sg-op-inv  sg-op-id"  (-1)  THENA  Auto))

---

Home Index