Lemma DUAL-BA-7. Dual BA 3-basis, existence of 0 and 1.

\{ \begin{matrix}\{(SD-dist)\} \\ y + (x · (y · z)) = y \\ ((x · y) + (y · z)) + y = y \\ (x + x′) · y = y \\ y · (x + (y + z)) = y \\ ((x + y) · (y + z)) · y = y \\ (x · x′) + y = y \end{matrix} \} ⇒ \{ \begin{matrix}x + x′ = y + y′ \\ x · x′ = y · y′ \end{matrix} \} .

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

2 B + B′ = A + A′, B · B′ = A · A′ → □ 3 (x · y) + ((y · z) + (z · x)) = (x + y) · ((y + z) · (z + x)) 5 x + (y · (x · z)) = x 7 ((x · y) + (y · z)) + y = y 10,9 (x + x′) · y = y 11 x · (y + (x + z)) = x 15 (x · x′) + y = y

22,21  (x · x′)′ · y = y  [15 → 9]
28,27  x + (x · y) = x  [9 → 5]
37  x + x = x  [9 → 7 :28]
43  (x · y) + y = y  [5 → 7]
49  x · (y + x) = x  [37 → 11]
55  x · (x + y) = x  [43 → 11]
69  (x · y) · x = x · y  [27 → 49]
150,149 (x · x′)′ + y = (x · x′)′  [55 → 21, flip]
152,151 x + (y · y′)′ = (y · y′)′  [49 → 21, flip]
155  (x · (y · y′)′) + z = z + x  [21 → 3 :28,152,150,22,22]
158  x + y = (y · (z · z′)′) + x  [flip 155]
160,159 x · (y · y′)′ = x  [21 → 69 :22]
163  x · (y + y′) = x  [9 → 69 :10]
165  x + y = y + x  [158 :160]
182  x + (y · y′) = x  [15 → 165, flip]
286  x + x′ = y + y′  [9 → 163]
293  x · x′ = y · y′  [15 → 182]
726  □  [2,286,293]