set G = G_Real ;
let a be Element of G_Real; :: thesis: ex b being Element of G_Real st b + b = a
reconsider a = a as Element of REAL ;
reconsider b9 = a / 2 as Element of REAL by XREAL_0:def 1;
consider b being Element of G_Real such that
A1: b = b9 ;
b + b = a by A1;
hence ex b being Element of G_Real st b + b = a ; :: thesis: verum