:: deftheorem Def5 defines " GROUP_1:def 5 :
for G being Group
for h, b₃ being Element of G holds
( b₃ = h " iff ( h * b₃ = 1_ G & b₃ * h = 1_ G ) );