GroupTheoryExample.txt

HYPOTHESIS:

V x. Eq[x, x]
V x. V y. Eq[x, y] -> Eq[y, x]
V x. V y. V z. (Eq[x, y] & Eq[y, z]) -> Eq[x, z]

V x. V y. V z. Eq[times(x, times(y, z)), times(times(x, y), z)]
V x. Eq[times(x, One), x] & Eq[times(One, x), x]
V x. E y. Eq[times(x, y), One]

Inverse[x, y] <-> Eq[times(x, y), One] & Eq[times(y, x), One]

CONCLUSION:

Inverse[x, y] & Inverse[x, z] -> Eq[y, z]