Theorem TC-2. TC with an identity element satisfies RC.

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

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

15  x · y = y · x  [2,3,5,3,5]
40  C_{4} · C_{1} = C_{2} · C_{3}  [2,15,9,15,7, flip]
77  E · C_{1} = C_{2} · F  [2,11,15,40,1]
212  C_{2} · F = C_{1} · E  [15 → 77, flip]
214  □  [212,13]