theorem Th3: :: REALSET2:3

for F being AbGroup
for a being Element of F ex b being Element of F st
( a + b = 0. F & b + a = 0. F )