Theorem QLT-2. The distributive law implies its dual in QLT.

\{ \begin{matrix}QLT \\ 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 7.28 seconds).

2 x ∧ x = x 4 x ∧ y = y ∧ x 5 (x ∧ y) ∧ z = x ∧ (y ∧ z) 8,7 x ∨ x = x 9 x ∨ y = y ∨ x 11,10 (x ∨ y) ∨ z = x ∨ (y ∨ z) 14 (x ∨ (y ∧ z)) ∧ (x ∨ y) = x ∨ (y ∧ z) 16 x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z)

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

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

23  x ∧ (x ∧ y) = x ∧ y  [2 → 5, flip]
30  x ∨ (x ∨ y) = x ∨ y  [7 → 10, flip]
43,42  x ∨ (y ∨ x) = x ∨ y  [9 → 30]
51,50  x ∨ (y ∨ (x ∨ z)) = x ∨ (y ∨ z)  [42 → 10 :11,11, flip]
58  (x ∨ ((x ∨ y) ∧ z)) ∧ (x ∨ y) = x ∨ ((x ∨ y) ∧ z)  [30 → 14]
108  x ∨ (x ∧ y) = x ∧ (x ∨ y)  [2 → 17]
116  x ∧ (y ∨ (x ∧ z)) = x ∧ (y ∨ z)  [23 → 17 :18, flip]
122,121 (x ∧ y) ∨ x = x ∧ (y ∨ x)  [2 → 17]
123  x ∧ (y ∨ z) = x ∧ (z ∨ y)  [9 → 17 :18]
163  A ∨ (C ∧ B) ≠ (A ∨ B) ∧ (A ∨ C)  [4 → 19]

181,180 (x ∨ (y ∧ z)) ∧ (x ∨ (y ∧ (z ∨ y))) = x ∨ (y ∧ z)

[14 → 108 :8,11,51,122, flip]

183  x ∨ (y ∧ x) = x ∧ (x ∨ y)  [4 → 108]
226  (x ∨ y) ∧ z = z ∧ (y ∨ x)  [4 → 123]
230  x ∧ (y ∨ z) = (z ∨ y) ∧ x  [flip 226]
916,915 (x ∨ (y ∧ z)) ∧ y = y ∧ (x ∨ z)  [4 → 116]
918,917 x ∨ ((x ∨ y) ∧ z) = (x ∨ y) ∧ (x ∨ z)  [58 :916, flip]
919  x ∨ (y ∧ (z ∨ x)) = x ∨ (y ∧ z)  [116 → 183 :11,18,43,11,122,181]
1440  x ∨ (y ∧ z) = (x ∨ z) ∧ (x ∨ y)  [230 → 919 :918, flip]
1442  □  [1440,163]