An effect algebrais a system $(E,\oplus , 0, 1)$ consisting of a set $E$ with two special elements $0, 1 \in E$, called the zero and the unit, and with a partially defined binary operation $\oplus$ satisfying the following conditions for all $p, q, r\in E$.
(E1)(Commutative law) If $p⊕q$ is defined, then $q⊕p$ is defined and $p⊕q=q⊕p$.
(E2)(Associative law) If $p⊕q$ is defined and $(p⊕q) ⊕r$ is defined, then $q⊕r$ and $p⊕(q⊕r)$ are defined and $p⊕(q⊕r) =(p⊕q) ⊕r$.
(E3)(Orthosupplement law) For every $p\in E$ there exists a unique $q\in E$ such that $p⊕q$ is defined and $p⊕q=1$.
(E4)(Zero-one law) If $p⊕1$ is defined, then $p=0$.
Let $(E, ⊕, 0, 1)$ be an effect algebra. Define a binary relation on $E$ by $a \leqslant b$ if for some $c \in E$, $c ⊕a = b$.
A difference poset (D-poset) is a system $(P,\leqslant , \ominus ,0,1)$ consisting of a partially ordered set $P$ with the least element $0$ and the greatest $1$ and a partially defined binary operation $\ominus$ satisfying the following conditions for all $a, b, c\in P$.
(D1) $b\ominus a$ is defined if and only if $a\leqslant b$;
(D2) $a\ominus 0 =a$;
(D3)If $a\leqslant b\leqslant c$, then $c\ominus b \leqslant c\ominus a$ and $(c\ominus a)\ominus (c\ominus b) =b\ominus a$.
I want to prove that if $(P,\leqslant ,\ominus ,0,1)$ is a D-poset, then $(P,⊕,0,1)$ is an effect algebra in which $a ⊕b := c$ if and only if $b \leqslant c$ and $c\ominus b = a$.
But my probelm is that if $p\oplus q$ is defined, I don't know how to show that $q\oplus p$ is defined.
Given that $p \oplus q = r$, we have $$q \leq r \quad\text{and}\quad r \ominus q = p.$$
Now if we prove that $p \leq r$ and $r \ominus p = q$, then $q \oplus p$ is defined (and equals $p \oplus q$).
From $0 \leq q \leq r$ we get $$p = r \ominus q \leq r \ominus 0 = r,$$ using (D2) and (D3). Also, from $0 \leq q \leq r$ we get $$(r \ominus 0) \ominus (r \ominus q) = q \ominus 0,$$ which again, using (D2) and (D3), yields $$r \ominus (r \ominus q) = q$$ or $$r \ominus p = q,$$ since $r \ominus q = p.$