:: deftheorem Def10 defines - RLVECT_1:def 10 :
for V being non empty addLoopStr
for v being Element of V st V is add-associative & V is right_zeroed & V is right_complementable holds
for b₃ being Element of the carrier of V holds
( b₃ = - v iff v + b₃ = 0. V );