for A being Abelian addGroup
for a, b being Element of A holds - (a + b) = (- a) + (- b) by Th16;