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