:: deftheorem Def1 defines - ALGSTR_2:def 1 :
for L being non empty left_add-cancelable add-right-invertible addLoopStr
for a, b₃ being Element of L holds
( b₃ = - a iff a + b₃ = 0. L );