Theorem TC-13. Cancellative medial algebras satisfy TC.

\{ \begin{matrix}(x · y) · (z · u) = (x · z) · (y · u) \\ cancellation \end{matrix} \} ⇒ TC.

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

2 x · y = z, x · u = z → y = u 4 (x · y) · (z · u) = (x · z) · (y · u) 5 C_{3} · A = C_{2} · B 7 C_{3} · D = C_{1} · B 9 C_{2} · D = C_{1} · A → □

14  (x · y) · (C_{2} · B) = (x · C_{3}) · (y · A)  [5 → 4]
17  (x · C_{3}) · (y · A) = (x · y) · (C_{2} · B)  [flip 14]
18  (x · y) · (C_{1} · B) = (x · C_{3}) · (y · D)  [7 → 4]
101  (x · C_{3}) · (y · D) = (x · C_{1}) · (y · B)  [4 → 18, flip]
235  C_{2} · D = C_{1} · A  [2,17,101, flip]
237  □  [235,9]