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