---

Step * of Lemma sg-inv-unique

∀[sg:s-Group]. ∀[x,y:Point].  x^-1 ≡ y supposing (x y) ≡ 1
BY
{ Auto }

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

---

Latex:

---

Latex:
\mforall{}[sg:s-Group].  \mforall{}[x,y:Point].    x\^{}-1  \mequiv{}  y  supposing  (x  y)  \mequiv{}  1


By

---

Latex:
Auto

---

Home Index