Theorem TC-4. TC with a weak identity element satisfies RC (1).

\{ \begin{matrix}TC \\ (x · e) · e = x \\ e · (e · x) = x \end{matrix} \} ⇒ RC.

Proof (found by Otter 3.0.4 on gyro at 55.76 seconds).

1 x = x 2 x · y = z, u · v = z, x · w = v_{6}, v_{7} · v = v_{6} → u · w = v_{7} · y 4,3 (x · e) · e = x 6,5 e · (e · x) = x 7 C_{4} · A = C_{3} · B 9 C_{2} · A = C_{1} · B 11 C_{4} · F = C_{3} · E 13 C_{2} · F = C_{1} · E → □

20  ((e · x) · e) · (e · (y · e)) = y · x  [2,1,3,5,1]
22  x · y = ((e · y) · e) · (e · (x · e))  [2,5,1,1,3]
39  ((e · E) · e) · A = ((e · B) · e) · F  [2,11,20,7,20]
60  ((e · E) · e) · (e · (C_{1} · e)) = C_{2} · F  [2,20,9,1,39, flip]
70  C_{2} · F = C_{1} · E  [22 → 60 :6,4,4,6, flip]
72  □  [70,13]