let G be addGroup; :: thesis: for g, h being Element of G holds - (h + g) = (- g) + (- h)
let g, h be Element of G; :: thesis: - (h + g) = (- g) + (- h)
((- g) + (- h)) + (h + g) = (((- g) + (- h)) + h) + g by RLVECT_1:def 3
.= ((- g) + ((- h) + h)) + g by RLVECT_1:def 3
.= ((- g) + (0_ G)) + g by Def5
.= (- g) + g by Def4
.= 0_ G by Def5 ;
hence - (h + g) = (- g) + (- h) by Th11; :: thesis: verum