theorem :: EC_PF_2:6

for K being Field
for a1, a2 being Element of K st a1 = - a2 holds
- a1 = a2