Theorem LT-8. Uniqueness of the meet operation in LT. If ∧, ∨, and · are binary operations such that both ⟨L; ∨, ∧⟩ and ⟨L; ∨, ·⟩ are lattices, then x ∧ y = x · y.

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

4 x ∧ y = y ∧ x 5 (x ∧ y) ∧ z = x ∧ (y ∧ z) 9 x ∨ y = y ∨ x 12 x ∧ (x ∨ y) = x 14 x ∨ (x ∧ y) = x 18 x · y = y · x 19 (x · y) · z = x · (y · z) 21 x · (x ∨ y) = x 23 x ∨ (x · y) = x 25 A ∧ B ≠ A · B

33  x ∧ (y ∨ x) = x  [9 → 12]
37  (x ∨ y) ∧ x = x  [4 → 12]
41  (x ∧ y) ∨ (x ∧ (y ∧ z)) = x ∧ y  [5 → 14]
43  x ∨ (y ∧ x) = x  [4 → 14]
45  (x ∧ y) ∨ x = x  [9 → 14]
47  x · (y ∨ x) = x  [9 → 21]
49  (x ∨ y) · x = x  [18 → 21]
66  x ∨ (y · x) = x  [18 → 23]
70  (x · y) ∨ x = x  [9 → 23]
74  B ∧ A ≠ A · B  [4 → 25]
83  (x ∨ y) ∧ y = y  [4 → 33]
110  (x ∧ y) ∨ y = y  [9 → 43]
126  x · (y · (z ∨ (x · y))) = x · y  [19 → 47]
133,132 x · (x ∧ y) = x ∧ y  [45 → 49]
167  x ∧ (x · y) = x · y  [70 → 37]
171  x ∧ (y · x) = y · x  [66 → 83]
188,187 x · (y ∧ x) = y ∧ x  [110 → 49]
456  (x ∧ y) ∨ (x ∧ (y · z)) = x ∧ y  [167 → 41]
8044  (x ∧ y) ∨ (y · x) = x ∧ y  [171 → 456]
8185  x ∧ y = y · x  [8044 → 126 :133,188]
8187  □  [8185,74]