theorem :: GROUP_1:43

for G being Group
for h being Element of G st ord h = 1 holds
h = 1_ G