Theorem TC-5. TC with a weak identity element satisfies RC (2).

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

Proof (found by Otter 3.0.4 on gyro at 74.62 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) · e = x 6,5 e · (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 → □

14  (((x · y) · e) · e) · z = (((x · z) · e) · e) · y  [2,1,3,1,3]
18,17  (((C_{2} · x) · e) · e) · A = (((C_{1} · B) · e) · e) · x  [2,1,3,9,3]
33  x · (e · (e · y)) = ((y · e) · e) · (e · (e · (x · e)))  [2,5,1,5,3]
36  (((e · x) · e) · e) · (e · (e · (y · e))) = y · x  [2,1,3,5,1]
293  (((e · E) · e) · e) · A = (((e · B) · e) · e) · F  [2,11,36,7,36]

418,417 (((e · E) · e) · e) · (e · (e · (C_{1} · B))) = (((C_{2} · F) · e) · e) · B

[2,36,17,36,293 :4,6,4, flip]

423 (((C_{2} · F) · e) · e) · B = (((C_{1} · B) · e) · e) · E

[2,33,17,293,293 :4,6,18,418, flip]

515  C_{2} · F = C_{1} · E  [2,3,14,3,423 :4,4, flip]
517  □  [515,13]