:: deftheorem Def6 defines inverse_op GROUP_1:def 6 :
for G being Group
for b₂ being UnOp of G holds
( b₂ = inverse_op G iff for h being Element of G holds b₂ . h = h " );