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