theorem Th27: :: CAYLDICK:27

for N being non empty ConjNormAlgStr
for a, b being Element of N st N is add-associative & N is right_zeroed & N is right_complementable holds
- <%a,b%> = <%(- a),(- b)%>