:: deftheorem Def5 defines - GROUP_1A:def 4 :
for G being addGroup
for h, b₃ being Element of G holds
( b₃ = - h iff ( h + b₃ = 0_ G & b₃ + h = 0_ G ) );