Theorem LT-4. The distributive law implies its dual in lattice theory.

\{ \begin{matrix}LT \\ x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z) \end{matrix} \} ⇒ \{x ∨ (y ∧ z) = (x ∨ y) ∧ (x ∨ z)\}.

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

4 x ∧ y = y ∧ x 6,5 (x ∧ y) ∧ z = x ∧ (y ∧ z) 9 x ∨ y = y ∨ x 10 (x ∨ y) ∨ z = x ∨ (y ∨ z) 12 x ∧ (x ∨ y) = x 14 x ∨ (x ∧ y) = x 16 x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z)

17 (x ∧ y) ∨ (x ∧ z) = x ∧ (y ∨ z) [flip 16]

19 A ∨ (B ∧ C) ≠ (A ∨ B) ∧ (A ∨ C)

20  x ∧ (y ∨ x) = x  [9 → 12]
22  (x ∨ y) ∧ x = x  [4 → 12]
35  x ∨ (y ∧ x) = x  [4 → 14]
39  x ∧ (y ∧ x) = x ∧ y  [14 → 20 :6]
53  (x ∧ y) ∨ y = y  [9 → 35]
55  x ∨ ((y ∧ x) ∨ z) = x ∨ z  [35 → 10, flip]
70  (x ∨ (y ∨ z)) ∧ (x ∨ y) = x ∨ y  [10 → 22]
91,90  x ∨ ((x ∨ y) ∧ z) = (x ∨ y) ∧ (x ∨ z)  [22 → 17]
145  A ∨ (C ∧ B) ≠ (A ∨ B) ∧ (A ∨ C)  [4 → 19]
346,345 x ∨ (y ∧ (x ∨ z)) = x ∨ (y ∧ z)  [17 → 55]
502,501 (x ∨ y) ∧ (x ∨ (z ∧ y)) = x ∨ (z ∧ y)  [53 → 70]
816  x ∨ (y ∧ z) = (x ∨ z) ∧ (x ∨ y)  [39 → 90 :91,346,502, flip]
818  □  [816,145]