let G be addGroup; :: thesis: for h being Element of G st - h = 0_ G holds
h = 0_ G
let h be Element of G; :: thesis: ( - h = 0_ G implies h = 0_ G )
- (0_ G) = 0_ G by Th8;
hence ( - h = 0_ G implies h = 0_ G ) ; :: thesis: verum