In Birkhoff an l-group G is defined as a group that is also a poset and in which group translation is isotone: \begin{gather*} x\leq y\implies a+x+b\leq a+y+b\;\forall a,x,y,b\in G, \end{gather*} and in which any two elements have a glb and lub. Such G apparently satisfies \begin{gather*} a+(x\vee y)=(a+x)\vee(a+y) \end{gather*} and though I see $(a+x)\vee(a+y)\leq a+(x\vee y)$ I don't know how to get the reverse inclusion from the definition above.
1 Answer
$\begingroup$
$\endgroup$
Let us single out the inequality you already established: \begin{equation} \label{dist-ineq} (a + x) \vee (a + y) \leq a + (x \vee y)\tag{$\star$} \end{equation}
Now, \begin{align} x \vee y &= (-a) + a + (x \vee y)\\ &\geq (-a) + ((a + x) \vee (a + y)) \tag{$\because\star$}\\ &\geq ((-a) + a + x) \vee ((-a) + a + y) \tag{$\because\star$}\\ &= x \vee y. \end{align} This implies that all inequalities above are, indeed, equalities; in particular, $$(-a) + a + (x \vee y) = (-a) + ((a + x) \vee (a + y)),$$ or, summing $a$, $$a + (x \vee y) = (a + x) \vee (a + y).$$
