Theorem GEO-2. Desargues configuration on a cubic curve.

\{ \begin{matrix}x · y = y · x \\ x · (y · x) = y \end{matrix} \} =(gL)⇒ \{[ \begin{matrix}A · P = O \\ B · Q = O \\ C · R = O \\ P · Q = W \\ P · R = V \\ Q · R = U \\ A · B = W \\ A · C = V \\ B · C = U \\ U · V = W \end{matrix} ] → [ \begin{matrix}A · A = O · O \\ B · B = O · O \\ C · C = O · O \\ P · P = O · O \\ Q · Q = O · O \\ R · R = O · O \\ U · U = O · O \\ V · V = O · O \\ W · W = O · O \end{matrix} ]\} .

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

1 x = x 2 O · O = A · A, O · O = B · B, O · O = C · C, P · P = O · O,

Q · Q = O · O, R · R = O · O, U · U = O · O,

V · V = O · O, W · W = O · O → □

3 x · y = y · x 4 x · (y · x) = y 7,6 A · P = O 9,8 B · Q = O 11,10 C · R = O 12 P · Q = W 14 P · R = V 16 Q · R = U 18 A · B = W 21,20 A · C = V 23,22 B · C = U 24 U · V = W

26  (x · y) · z = z · (y · x)  [3 → 3]
27  x · (y · z) = (z · y) · x  [3 → 3]
28  P · A = O  [3 → 6]
33,32  R · C = O  [3 → 10]
38  Q · W = P  [12 → 4]
43,42  Q · O = B  [8 → 4]
44  P · O = A  [6 → 4]
46  (x · y) · x = y  [4 → 4]
48  x · (x · y) = y  [3 → 4]
50  (x · y) · y = x  [3 → 4]
54  R · V = P  [14 → 4]
58  R · U = Q  [16 → 4]
60  B · A = W  [3 → 18]
62  B · W = A  [18 → 4]
64  C · A = V  [3 → 20]

69,68  C · B = U  [3 → 22]
71,70  C · U = B  [22 → 4]
73,72  V · U = W  [3 → 24]
75,74  V · W = U  [24 → 4]
77,76  A · O = P  [28 → 4]
81,80  C · O = R  [32 → 4]
86  (x · y) · (z · u) = (u · z) · (y · x)  [3 → 26]
88  (x · (y · z)) · (z · y) = x  [4 → 26, flip]
102  W · Q = P  [3 → 38]
123,122 V · R = P  [3 → 54]
125,124 V · P = R  [54 → 4]
134 U · R = Q [3 → 58]
139,138 A · W = B  [60 → 4]
140  W · B = A  [3 → 62]
150  V · C = A  [64 → 46]
161,160 B · U = C  [68 → 4]
163,162 W · V = U  [72 → 46]
169,168 ((x · y) · z) · ((z · (y · x)) · u) = u  [27 → 48]
194  (x · y) · (z · u) = (x · z) · (y · u)  [(gL) 86]
196  (V · x) · (C · y) = A · (x · y)  [150 → 194, flip]
640,639 (V · x) · y = A · (x · (C · y))  [48 → 196]
646,645 U · U = A · A  [140 → 196 :75,69]
647  W · O = A · Q  [134 → 196 :73,11]
651  U · (C · Q) = O  [102 → 196 :75,7]
653  P · B = A · Q  [58 → 196 :123,71]
658,657 R · R = A · A  [44 → 196 :125,81]
659 P · (C · C) = P [32 → 196 :123,77]

666 O · O = A · A, O · O = B · B, O · O = C · C, P · P = O · O,

Q · Q = O · O, V · V = O · O, W · W = O · O → □

[2 :658,646]

676  U · (A · A) = U  [645 → 48]
690  W · (A · Q) = O  [647 → 48]
710  O · (Q · C) = U  [651 → 88]
715  O · (C · Q) = U  [651 → 50]
733  (A · Q) · B = P  [653 → 50]
736,735 P · (A · Q) = B  [653 → 48]
738,737 (A · Q) · P = B  [653 → 46]
763,762 P · P = C · C  [659 → 48]

764 O · O = A · A, O · O = B · B, O · O = C · C, Q · Q = O · O,

V · V = O · O, W · W = O · O → □  [666 :763]
801  W · (A · x) = U · (C · x)  [651 → 690 :(gL)]
811  U · (C · C) = U  [160 → 801 :161,21,163, flip]
816,815 W · x = U · (C · (A · x))  [48 → 801]

827 O · O = A · A, O · O = B · B, O · O = C · C, Q · Q = O · O,

¿  V · V = O · O → □  [764 :816,139,69,646]

951  B · (Q · A) = P  [27 → 733]
1034  U · (x · C) = O · (x · Q)  [715 → 811 :(gL)]
1036,1035 U · (C · x) = O · (Q · x)  [710 → 811 :(gL)]
1038,1037 x · (C · C) = x · (A · A)  [676 → 811 :(gL)]
1087  O · (Q · Q) = O  [651 :1036]
1099  P · (A · A) = P  [659 :1038]
1112,1111 C · C = A · A  [762 → 168 :763,1038,169, flip]

1121 O · O = A · A, O · O = B · B, Q · Q = O · O,

V · V = O · O → □  [827 :1112]
1123,1122 P · P = A · A  [762 :1112]
1131,1130 O · O = A · A  [737 → 1034 :738,23,646,9, flip]

1158 B · B = A · A, Q · Q = A · A, V · V = A · A → □

[1121 :1131,1131,1131,1131 :1, flip]

1234,1233 Q · Q = A · A  [1087 → 48 :1131, flip]
1252  B · B = A · A, V · V = A · A → □  [1158 :1234 :1]
1253  B · (Q · x) = P · (A · x)  [951 → 1099 :(gL), flip]
1266,1265 B · B = A · A  [32 → 1253 :33,43,77,1123]
1282  V · V = A · A → □  [1252 :1266 :1]
1441  (A · (V · (C · x))) · x = A · A → □  [50 → 1282 :640]
1449  A · A = A · A → □  [735 → 1441 :736,69,73,139,1266]
1450  □  [1449,3]