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