theorem Th30: :: NIVEN:32

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