let G be Group; :: thesis: for h being Element of G st ord h = 1 holds
h = 1_ G
let h be Element of G; :: thesis: ( ord h = 1 implies h = 1_ G )
assume A1: ord h = 1 ; :: thesis: h = 1_ G
then not h is being_of_order_0 by Def11;
then h |^ 1 = 1_ G by A1, Def11;
hence h = 1_ G by Th25; :: thesis: verum