theorem Th31: :: NIVEN:33

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for z0, z1 being Element of L holds - <%z0,z1%> = <%(- z0),(- z1)%>