theorem Th1: :: TDGROUP:1

for a being Element of G_Real ex b being Element of G_Real st b + b = a