theorem :: CAYLDICK:26

for N being non empty ConjNormAlgStr
for a, b being Element of N st <%a,b%> is left_complementable & <%a,b%> is right_add-cancelable holds
- <%a,b%> = <%(- a),(- b)%>