Theorem WAL-2. Uniqueness of the meet operation in WAL. If ⟨S; ∨, ∧⟩ and ⟨S; ∨, ·⟩ are both weakly associative lattices, then x ∧ y = x · y.

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

2 x ∧ x = x 4 x ∧ y = y ∧ x 5 ((x ∨ y) ∧ (z ∨ y)) ∧ y = y 7 x ∨ x = x 9 x ∨ y = y ∨ x 10 ((x ∧ y) ∨ (z ∧ y)) ∨ y = y 12 x · x = x 14 x · y = y · x 15 ((x ∨ y) · (z ∨ y)) · y = y 17 ((x · y) ∨ (z · y)) ∨ y = y 19 A ∧ B ≠ A · B

28  (x ∨ y) ∧ y = y  [2 → 5]
33  (x ∨ y) ∧ x = x  [9 → 28]
35  x ∧ (y ∨ x) = x  [4 → 28]
45  (x ∧ y) ∨ y = y  [7 → 10]
51  x ∧ (x ∨ y) = x  [4 → 33]
59  (x ∧ y) ∨ x = x  [4 → 45]
61  x ∨ (y ∧ x) = x  [9 → 45]
83  (x ∨ y) · y = y  [12 → 15]
89  x ∨ (x ∧ y) = x  [9 → 59]
96,95  (x ∨ y) ∨ x = x ∨ y  [51 → 61]
99  ((x ∨ (y ∧ z)) · z) · (y ∧ z) = y ∧ z  [61 → 15]
125  x ∨ (y · x) = x  [83 → 17 :96]
153  x ∨ (x · y) = x  [14 → 125]
161  ((x ∨ (y · z)) ∧ z) ∧ (y · z) = y · z  [125 → 5]
199  (x · y) ∧ x = x · y  [153 → 35]
748,747 (x · y) · (x ∧ y) = x ∧ y  [89 → 99]
1042,1041 (x ∧ y) ∧ (x · y) = x ∧ y  [747 → 199 :748]
1471  x ∧ y = x · y  [153 → 161 :1042]
1473  □  [1471,19]