---

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


1. sg : s-Group
2. x : Point
3. (x x^-1) ≡ 1
4. (x^-1 x) ≡ ((x^-1 x) (x^-1 x))
⊢ (x^-1 x) ≡ 1
BY
{ (MoveToConcl (-1) THEN (GenConclTerm ⌜(x^-1 x)⌝⋅ THENA Auto) THEN All Thin) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-1)  THEN  (GenConclTerm  \mkleeneopen{}(x\^{}-1  x)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Thin)

---

Home Index