for a being Element of G_Real st a + a = 0. G_Real holds
a = 0. G_Real ;