Theorem TC-1. TC quasigroups satisfy RC.

\{ \begin{matrix}TC \\ quasigroup \end{matrix} \} ⇒ RC.

Proof (found by Otter 3.0.4 on gyro at 5.22 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 x · (x\y) = y 6,5 x\(x · y) = y 7 (x/y) · y = x 11 C_{4} · A = C_{3} · B 13 C_{2} · A = C_{1} · B 15 C_{4} · F = C_{3} · E 17 C_{2} · F = C_{1} · E → □

31  C_{4} · (C_{3}\x) = (x/A) · B  [2,3,7,1,11, flip]
85  C_{2} · (C_{1}\x) = (x/A) · B  [2,3,7,1,13, flip]
1078  C_{2} · F = C_{1} · E  [2,15,3,31,85 :6, flip]
1080  □  [1078,17]