theorem Th31: :: GROUP_1:32

for G being Group
for h being Element of G holds h |^ (- 1) = h "