Proof. Let be any model of the equations from this theorem. is idempotent because of identities Idem1) and Idem2).
At first, we define the relation ∼ as iff and .
Now, we will prove that the ∼ relation is an equivalence relation on .
Let . We have from Idem1), and by definition of ∼, this implies .
Let . if and if . This is obvious from the definition of the relation ∼.
Let
be such that
and
. Then, we have
,
,
and
. From this we obtain the following:
From identities (
1) and (
2) follows
. Analogously, we obtain
, so
. We can see that the relation ∼ satisfies reflectivity (R), symmetricity (S) and transitivity (T), so the relation ∼ is an equivalence relation.
Next, we show that the relation ∼ is a congruence on algebra . First, we are showing compatibility with the operation ∧. Therefore, we need to show that, if , then and for every .
Let
such that
. Then, we have
The proof that is completely analogous; we simply flip letters a and b, so we prove that . From Comm) follows that and similarly that . Thus, from the transitivity of the relation ∼, we obtain . With this, we show the compatibility of the relation ∼ with the operation ∧.
The next step is showing compatibility of ∼ with the operation d. We need to show that, if , , , then .
Let
be such that
,
and
. Then, we have
Once again, the proof that is completely analogous; we simply need to flip , and .
Hence, we have seen that and , that is , which gives us the compatibility of ∼ with d.
Now the identities Idem1), Comm), Assoc1), and Assoc2) imply that ∼ is a semilattice. From the definition of the relation ∼ follows that the operation ∧ is the second projection on each ∼ class. Taken together with that fact, Mal) implies that d is Mal’cev on each ∼ class. Therefore, is an SMB algebra. On the other hand, the base identities are easily verifiable in each SMB algebra. □
In the following three lemmas, we trim down the equational base we found in Theorem 2.
We summarize the results we proved so far.
With this theorem, we have significantly reduced the equational base, but can we remove any other identity? Maybe the identity Comp1), but we can not eliminate any others. The following algebras shown in Cayley tables satisfy all but one identity.