Theorem GEO-1. Tangent construction.

\{x · (y · x) = y\} =(gL)⇒ \{[ \begin{matrix}A_{1} · A_{2} = Q \\ B_{1} · B_{2} = R \\ A_{1} · B_{1} = S \\ A_{2} · B_{2} = S \end{matrix} ] → S · S = Q · R\} .

(In the statement of the theorem, A_{1}, A_{2}, B_{1}, B_{2}, P, Q, R are variables; in the proof below, they are Skolem constants.)

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

1 S · S ≠ Q · R 3 x · (y · x) = y 4 A_{1} · A_{2} = Q 5 B_{1} · B_{2} = R 6 A_{1} · B_{1} = S 7 A_{2} · B_{2} = S

13  (x · y) · x = y  [3 → 3]
18  A_{2} · Q = A_{1}  [4 → 3]
25  B_{2} · R = B_{1}  [5 → 3]
32  B_{1} · S = A_{1}  [6 → 3]
40  B_{2} · S = A_{2}  [7 → 3]
134  (B_{2} · R) · S = A_{1}  [25 → 32]
171  (B_{2} · S) · Q = A_{1}  [40 → 18]
1849  (x · S) · Q = (x · R) · S  [134 → 171 :(gL)]
2161  (Q · R) · S = S  [13 → 1849, flip]
6976  S · S = Q · R  [2161 → 3]
6977  □  [6976,1]