theorem tA: :: REALALG2:26

for R being 0 -characteristic domRing
for a being Element of R holds
( - a = a iff a = 0. R )