:: deftheorem Def6 defines add_inverse GROUP_1A:def 5 :
for G being addGroup
for b₂ being UnOp of G holds
( b₂ = add_inverse G iff for h being Element of G holds b₂ . h = - h );