Theorem WAL-4. A short single axiom for WAL.

We use the same majority polynomial and axiom schema as in Thm. LT-12, and we use the two additional absorption laws of Lem. WAL-3. When the axiom is written in terms of ∧ and ∨, it has length 75, with 6 variables:

(((x ∧ y) ∨ (y ∧ (x ∨ y))) ∧ z) ∨ (((x ∧ (((y ∧ x_{1}) ∨ (x_{2} ∧ y))∨
y)) ∨ (((y ∧ (((y ∨ x_{1}) ∧ (x_{2} ∨ y)) ∧ y)) ∨ (u ∧ (y ∨ (((y ∨ x_{1})∧
(x_{2} ∨ y)) ∧ y)))) ∧ (x ∨ (((y ∧ x_{1}) ∨ (x_{2} ∧ y)) ∨ y)))) ∧ (((x∧
y) ∨ (y ∧ (x ∨ y))) ∨ z)) = y.