theorem Th25: :: GROUP_1:26

for G being Group
for h being Element of G holds h |^ 1 = h