let G be addGroup; :: thesis: - (0_ G) = 0_ G
(- (0_ G)) + (0_ G) = 0_ G by Def5;
hence - (0_ G) = 0_ G by Def4; :: thesis: verum