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