let G be addGroup; :: thesis: for g, h being Element of G st - h = - g holds
h = g
let g, h be Element of G; :: thesis: ( - h = - g implies h = g )
assume - h = - g ; :: thesis: h = g
then A1: h + (- g) = 0_ G by Def5;
g + (- g) = 0_ G by Def5;
hence h = g by A1, Th6; :: thesis: verum