A 4-basis for lattice theory (LT) in terms of join (v) and meet (^).
x v (y v z) = y v (x v z). % AJ
x ^ (y ^ z) = y ^ (x ^ z). % AM
x v (x ^ y) = x. % B1
x ^ (x v y) = x. % B2
Note that this basis is self-dual (that is, the dual of each member
is also a member).
A more standard basis for lattice theory is the 6-basis (also self-dual) consisting of B1, B2, and the commutativity and associativity of meet and join. Deriving commutativity of join (or of meet) from the 4-basis above shows that it is equivalent to the 6-basis. Here is an Otter proof of commutativity (idempotence is also proved).
otter < LT1.in > LT1.out
The following two Mace2 jobs show independence of the LT 4-basis.
mace2 -N6 -p < LTa.in > LTa.out
mace2 -N6 -p < LTb.in > LTb.out