theorem XZ: :: REALALG2:11

for F being Field
for a being non zero Element of F holds (- a) " = - (a ")